Quelle  SemilatAlg.thy

(*  Title:      HOL/MicroJava/BV/SemilatAlg.thy
    Author:     Gerwin Klein
    Copyright   2002 Technische Universitaet Muenchen
*)

section ‹More on Semilattices›

theory SemilatAlg
imports Typing_Framework_1
begin

definition lesubstep_type :: "(nat × 's) set ==> 's ord ==> (nat × 's) set ==> bool"
    (‹(_ /{⊑} _)› [50, 0, 51] 50)
  where "A {⊑} B ≡ ∀(p,τ) ∈ A. ∃τ'. (p,τ') ∈ B ∧ τ ⊑_r τ'"

notation (ASCII)
  lesubstep_type  (‹(_ /{<='__} _)› [50, 0, 51] 50)

primrec pluslussub :: "'a list ==> ('a ==> 'a ==> 'a) ==> 'a ==> 'a"  (‹(_ /⊔ _)› [65, 0, 66] 65)
where
  "pluslussub [] f y = y"
| "pluslussub (x#xs) f y = pluslussub xs f (x ⊔_f y)"
(*<*)
notation (ASCII)
  pluslussub  (‹(_ /++'__ _)› [65, 1000, 66] 65)
(*>*)

definition bounded :: "'s step_type ==> nat ==> bool"
where
  "bounded step n ⟷ (∀p<n. ∀τ. ∀(q,τ') ∈ set (step p τ). q<n)"

definition pres_type :: "'s step_type ==> nat ==> 's set ==> bool"
where
  "pres_type step n A ⟷ (∀τ∈A. ∀p<n. ∀(q,τ') ∈ set (step p τ). τ' ∈ A)"

definition mono :: "'s ord ==> 's step_type ==> nat ==> 's set ==> bool"
where
  "mono r step n A ⟷
    (∀τ p τ'. τ ∈ A ∧ p<n ∧ τ ⊑_r τ' ⟶ set (step p τ) {⊑} set (step p τ'))"

lemma [iff]: "{} {⊑} B" 
  (*<*) by (simp add: lesubstep_type_def) (*>*)

lemma [iff]: "(A {⊑} {}) = (A = {})"
  (*<*) by (cases "A={}") (auto simp add: lesubstep_type_def) (*>*)

lemma lesubstep_union:
  "[ A₁ {⊑} B₁; A₂ {⊑} B₂ ] ==> A₁ ∪ A₂ {⊑} B₁ ∪ B₂"
  (*<*) by (auto simp add: lesubstep_type_def) (*>*)

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 ] ==> set (step p s) {⊑} set (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) ==> A {⊑} A"
(*<*) by (unfold lesubstep_type_def) auto (*>*)

lemma lesub_step_typeD:
  "A {⊑} B ==> (x,y) ∈ A ==> ∃y'. (x, y') ∈ B ∧ y ⊑_r y'"
(*<*) by (unfold lesubstep_type_def) blast (*>*)


lemma 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 (simp only: Listn.le_def lesub_def semilat_def)
  apply (simp add: list_all2_conv_all_nth nth_list_update)
  done
(*>*)

lemma plusplus_closed: assumes "Semilat A r f" shows
  "∧y. [ set x ⊆ A; y ∈ A] ==> x ⊔ y ∈ A"
(*<*)
proof (induct x)
  interpret Semilat A r f by fact
  show "∧y. y ∈ A ==> [] ⊔ y ∈ A" by simp
  fix y x xs
  assume y: "y ∈ A" and xxs: "set (x#xs) ⊆ A"
  assume IH: "∧y. [ set xs ⊆ A; y ∈ A] ==> xs ⊔ y ∈ A"
  from xxs obtain x: "x ∈ A" and xs: "set xs ⊆ A" by simp
  from x y have "x ⊔ y ∈ A" ..
  with xs have "xs ⊔ (x ⊔ y) ∈ A" by (rule IH)
  thus "x#xs ⊔ y ∈ A" by simp
qed
(*>*)


lemma (in Semilat) pp_ub2:
 "∧y. [ set x ⊆ A; y ∈ A] ==> y ⊑ x ⊔ y"
(*<*)
  
proof (induct x)
  thm plusplus_closed[OF Semilat.intro, OF semilat]
  thm semilat_Def
  thm Semilat.intro
  fix y assume "y ∈ A" 
  with semilat show "y⊑ [] ⊔ y" by simp
  
  fix y a l assume y:  "y ∈ A" and "set (a#l) ⊆ A"
  then obtain a: "a ∈ A" and x: "set l ⊆ A" by simp

  from semilat x y have l_y_inA: "l ⊔ y ∈ A" by (auto dest: plusplus_closed[OF Semilat.intro, OF semilat])
  assume "∧y. [set l ⊆ A; y ∈ A] ==> y ⊑ l ⊔ y"
  from this and x have IH: "∧y. y ∈ A ==> y ⊑ l ⊔ y" .

  from a y have "a ⊔ y ∈ A" ..
  then have l_ay_inA: "l ⊔ ( a ⊔ y) ∈ A" using plusplus_closed[OF Semilat.intro, OF semilat] x  by auto 
    
  from a y have "y ⊑ a ⊔ y" ..
  also from a y have a_y_inA: "a ⊔ y ∈ A" ..
  hence "(a ⊔ y) ⊑ l ⊔ (a ⊔ y)" by (rule IH)
  finally have "y ⊑ l ⊔ (a ⊔ y)" using y a_y_inA l_ay_inA .
  thus "y ⊑ (a#l) ⊔ y" by simp
qed
(*>*)


lemma (in Semilat) pp_ub1:
shows "∧y. [set ls ⊆ A; y ∈ A; x ∈ set ls] ==> x ⊑ ls ⊔ y"
(*<*)
proof (induct ls)
  show "∧y. x ∈ set [] ==> x ⊑ [] ⊔ 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 ⊑ ls ⊔ y"
  from this and ls have IH: "∧y. x ∈ set ls ==> y ∈ A ==> x ⊑ ls ⊔ y" .

  from s y have s_y_inA: "s ⊔ y ∈ A" ..
  then have ls_sy_inA: "ls ⊔ (s ⊔ y) ∈ A"using plusplus_closed[OF Semilat.intro, OF semilat] ls  by auto 
  
  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 ⊑ s ⊔ y" ..
    also from ls s_y_inA have "(s ⊔ y) ⊑ ls ⊔ (s ⊔ y)" by (rule pp_ub2)
    finally have "s ⊑ ls ⊔ (s ⊔ y)" using s s_y_inA ls_sy_inA .
    with xs have "x ⊑ ls ⊔ (s ⊔ y)" by simp
  } 
  moreover {
    assume "x ∈ set ls"
    hence "∧y. y ∈ A ==> x ⊑ ls ⊔ y" by (rule IH)
    moreover from s y have "s ⊔ y ∈ A" ..
    ultimately have "x ⊑ ls ⊔ (s ⊔ y)" .
  }
  ultimately 
  have "x ⊑ ls ⊔ (s ⊔ y)" by blast
  thus "x ⊑ (s#ls) ⊔ y" by simp
qed
(*>*)


lemma (in Semilat) pp_lub:
  assumes z: "z ∈ A"
  shows 
  "∧y. y ∈ A ==> set xs ⊆ A ==> ∀x ∈ set xs. x ⊑ z ==> y ⊑ z ==> xs ⊔ y ⊑ z"
(*<*)
proof (induct xs)
  fix y assume "y ⊑ z" thus "[] ⊔ y ⊑ z" by simp
next
  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 ⊑ z"
  then obtain lz: "l ⊑ z" and lsz: "∀x ∈ set ls. x ⊑ z" by auto
  assume "y ⊑ z" with lz have "l ⊔ y ⊑ z" using l y z ..
  moreover
  from l y have "l ⊔ y ∈ A" ..
  moreover
  assume "∧y. y ∈ A ==> set ls ⊆ A ==> ∀x ∈ set ls. x ⊑ z ==> y ⊑ z
          ==> ls ⊔ y ⊑ z"
  ultimately
  have "ls ⊔ (l ⊔ y) ⊑ z" using ls lsz by -
  thus "(l#ls) ⊔ y ⊑ z" by simp
qed
(*>*)


lemma ub1': assumes "Semilat A r f"
shows "[∀(p,s) ∈ set S. s ∈ A; y ∈ A; (a,b) ∈ set S]
  ==> b ⊑ map snd [(p', t') ← S. p' = a] ⊔ y" 
(*<*)
proof -
  interpret Semilat A r f by fact
  let "b ⊑ ?map ⊔ 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' ⊔ ss ! q = ss ! q ==>
   (map snd [(p', t') ← S. p' = q] ⊔ ss ! q) = ss ! q"
(*<*)
apply (induct S)
apply auto 
done
(*>*)


end