# Theory SemilatAlg

Up to index of Isabelle/HOL/HOL-MicroJava-skip_proofs

theory SemilatAlg
imports Typing_Framework Product
`(*  Title:      HOL/MicroJava/DFA/SemilatAlg.thy    Author:     Gerwin Klein    Copyright   2002 Technische Universitaet Muenchen*)header {* \isaheader{More on Semilattices} *}theory SemilatAlgimports Typing_Framework Productbegindefinition lesubstep_type :: "(nat × 's) list => 's ord => (nat × 's) list => bool"                    ("(_ /<=|_| _)" [50, 0, 51] 50) where  "x <=|r| y ≡ ∀(p,s) ∈ set x. ∃s'. (p,s') ∈ set y ∧ s <=_r s'"primrec plusplussub :: "'a list => ('a => 'a => 'a) => 'a => 'a" ("(_ /++'__ _)" [65, 1000, 66] 65) where  "[] ++_f y = y"| "(x#xs) ++_f y = xs ++_f (x +_f y)"definition bounded :: "'s step_type => nat => bool" where"bounded step n == !p<n. !s. !(q,t):set(step p s). q<n"  definition pres_type :: "'s step_type => nat => 's set => bool" where"pres_type step n A == ∀s∈A. ∀p<n. ∀(q,s')∈set (step p s). s' ∈ A"definition mono :: "'s ord => 's step_type => nat => 's set => bool" where"mono r step n A == ∀s p t. s ∈ A ∧ p < n ∧ s <=_r t --> step p s <=|r| step p t"lemma pres_typeD:  "[| pres_type step n A; s∈A; p<n; (q,s')∈set (step p s) |] ==> s' ∈ A"  by (unfold pres_type_def, blast)lemma monoD:  "[| mono r step n A; p < n; s∈A; s <=_r t |] ==> step p s <=|r| step p t"  by (unfold mono_def, blast)lemma boundedD:   "[| bounded step n; p < n; (q,t) : set (step p xs) |] ==> q < n"   by (unfold bounded_def, blast)lemma lesubstep_type_refl [simp, intro]:  "(!!x. x <=_r x) ==> x <=|r| x"  by (unfold lesubstep_type_def) autolemma lesub_step_typeD:  "a <=|r| b ==> (x,y) ∈ set a ==> ∃y'. (x, y') ∈ set b ∧ y <=_r y'"  by (unfold lesubstep_type_def) blastlemma list_update_le_listI [rule_format]:  "set xs <= A --> set ys <= A --> xs <=[r] ys --> p < size xs -->     x <=_r ys!p --> semilat(A,r,f) --> x∈A -->    xs[p := x +_f xs!p] <=[r] ys"  apply (unfold Listn.le_def lesub_def semilat_def)  apply (simp add: list_all2_conv_all_nth nth_list_update)  donelemma plusplus_closed: assumes "semilat (A, r, f)" shows  "!!y. [| set x ⊆ A; y ∈ A|] ==> x ++_f y ∈ A" (is "PROP ?P")proof -  interpret Semilat A r f using assms by (rule Semilat.intro)  show "PROP ?P" proof (induct x)    show "!!y. y ∈ A ==> [] ++_f y ∈ A" by simp    fix y x xs    assume y: "y ∈ A" and xs: "set (x#xs) ⊆ A"    assume IH: "!!y. [| set xs ⊆ A; y ∈ A|] ==> xs ++_f y ∈ A"    from xs obtain x: "x ∈ A" and xs': "set xs ⊆ A" by simp    from x y have "(x +_f y) ∈ A" ..    with xs' have "xs ++_f (x +_f y) ∈ A" by (rule IH)    thus "(x#xs) ++_f y ∈ A" by simp  qedqedlemma (in Semilat) pp_ub2: "!!y. [| set x ⊆ A; y ∈ A|] ==> y <=_r x ++_f y"proof (induct x)  from semilat show "!!y. y <=_r [] ++_f y" by simp    fix y a l  assume y:  "y ∈ A"  assume "set (a#l) ⊆ A"  then obtain a: "a ∈ A" and x: "set l ⊆ A" by simp  assume "!!y. [|set l ⊆ A; y ∈ A|] ==> y <=_r l ++_f y"  hence IH: "!!y. y ∈ A ==> y <=_r l ++_f y" using x .  from a y have "y <=_r a +_f y" ..  also from a y have "a +_f y ∈ A" ..  hence "(a +_f y) <=_r l ++_f (a +_f y)" by (rule IH)  finally have "y <=_r l ++_f (a +_f y)" .  thus "y <=_r (a#l) ++_f y" by simpqedlemma (in Semilat) pp_ub1:shows "!!y. [|set ls ⊆ A; y ∈ A; x ∈ set ls|] ==> x <=_r ls ++_f y"proof (induct ls)  show "!!y. x ∈ set [] ==> x <=_r [] ++_f y" by simp  fix y s ls  assume "set (s#ls) ⊆ A"  then obtain s: "s ∈ A" and ls: "set ls ⊆ A" by simp  assume y: "y ∈ A"   assume     "!!y. [|set ls ⊆ A; y ∈ A; x ∈ set ls|] ==> x <=_r ls ++_f y"  hence IH: "!!y. x ∈ set ls ==> y ∈ A ==> x <=_r ls ++_f y" using ls .  assume "x ∈ set (s#ls)"  then obtain xls: "x = s ∨ x ∈ set ls" by simp  moreover {    assume xs: "x = s"    from s y have "s <=_r s +_f y" ..    also from s y have "s +_f y ∈ A" ..    with ls have "(s +_f y) <=_r ls ++_f (s +_f y)" by (rule pp_ub2)    finally have "s <=_r ls ++_f (s +_f y)" .    with xs have "x <=_r ls ++_f (s +_f y)" by simp  }   moreover {    assume "x ∈ set ls"    hence "!!y. y ∈ A ==> x <=_r ls ++_f y" by (rule IH)    moreover from s y have "s +_f y ∈ A" ..    ultimately have "x <=_r ls ++_f (s +_f y)" .  }  ultimately   have "x <=_r ls ++_f (s +_f y)" by blast  thus "x <=_r (s#ls) ++_f y" by simpqedlemma (in Semilat) pp_lub:  assumes z: "z ∈ A"  shows   "!!y. y ∈ A ==> set xs ⊆ A ==> ∀x ∈ set xs. x <=_r z ==> y <=_r z ==> xs ++_f y <=_r z"proof (induct xs)  fix y assume "y <=_r z" thus "[] ++_f y <=_r z" by simpnext  fix y l ls assume y: "y ∈ A" and "set (l#ls) ⊆ A"  then obtain l: "l ∈ A" and ls: "set ls ⊆ A" by auto  assume "∀x ∈ set (l#ls). x <=_r z"  then obtain lz: "l <=_r z" and lsz: "∀x ∈ set ls. x <=_r z" by auto  assume "y <=_r z" with lz have "l +_f y <=_r z" using l y z ..  moreover  from l y have "l +_f y ∈ A" ..  moreover  assume "!!y. y ∈ A ==> set ls ⊆ A ==> ∀x ∈ set ls. x <=_r z ==> y <=_r z          ==> ls ++_f y <=_r z"  ultimately  have "ls ++_f (l +_f y) <=_r z" using ls lsz by -  thus "(l#ls) ++_f y <=_r z" by simpqedlemma ub1':  assumes "semilat (A, r, f)"  shows "[|∀(p,s) ∈ set S. s ∈ A; y ∈ A; (a,b) ∈ set S|]   ==> b <=_r map snd [(p', t')\<leftarrow>S. p' = a] ++_f y" proof -  interpret Semilat A r f using assms by (rule Semilat.intro)  let "b <=_r ?map ++_f y" = ?thesis  assume "y ∈ A"  moreover  assume "∀(p,s) ∈ set S. s ∈ A"  hence "set ?map ⊆ A" by auto  moreover  assume "(a,b) ∈ set S"  hence "b ∈ set ?map" by (induct S, auto)  ultimately  show ?thesis by - (rule pp_ub1)qed    lemma plusplus_empty:    "∀s'. (q, s') ∈ set S --> s' +_f ss ! q = ss ! q ==>   (map snd [(p', t') \<leftarrow> S. p' = q] ++_f ss ! q) = ss ! q"  by (induct S) auto end`