Theory SemilatAlg

(*  Title:      HOL/MicroJava/BV/SemilatAlg.thy
    ID:         $Id: SemilatAlg.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Gerwin Klein
    Copyright   2002 Technische Universitaet Muenchen
*)

header {* \isaheader{More on Semilattices} *}

theory SemilatAlg = Typing_Framework:

(*<*)
syntax
  lesubstep_type :: "(nat × 's) set => 's ord => (nat × 's) set => bool"
                    ("(_ /{<='__} _)" [50, 0, 51] 50)
(*>*)
syntax (xsymbols)
  lesubstep_type :: "(nat × 's) set => 's ord => (nat × 's) set => bool"
                    ("(_ /{\<sqsubseteq>_} _)" [50, 0, 51] 50)
constdefs 
  lesubstep_type :: "(nat × 's) set => 's ord => (nat × 's) set => bool"
  "A {\<sqsubseteq>r} B ≡ ∀(p,τ) ∈ A. ∃τ'. (p,τ') ∈ B ∧ τ \<sqsubseteq>r τ'"

consts
  pluslussub :: "'a list => ('a => 'a => 'a) => 'a => 'a" 
(*<*)
syntax 
  pluslussub :: "'a list => ('a => 'a => 'a) => 'a => 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
(*>*)
syntax (xsymbols)
  pluslussub :: "'a list => ('a => 'a => 'a) => 'a => 'a" ("(_ /\<Squnion>_ _)" [65, 0, 66] 65)
primrec
  "[] \<Squnion>f y = y"
  "(x#xs) \<Squnion>f y = xs \<Squnion>f (x \<squnion>f y)"

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

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

  mono :: "'s ord => 's step_type => nat => 's set => bool"
  "mono r step n A ≡ 
  ∀τ p τ'. τ ∈ A ∧ p<n ∧ τ \<sqsubseteq>r τ' --> set (step p τ) {\<sqsubseteq>r} set (step p τ')"

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

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

lemma lesubstep_union:
  "[| A1 {\<sqsubseteq>r} B1; A2 {\<sqsubseteq>r} B2 |] ==> A1 ∪ A2 {\<sqsubseteq>r} B1 ∪ B2"
  (*<*) 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 \<sqsubseteq>r t |] ==> set (step p s) {\<sqsubseteq>r} 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 \<sqsubseteq>r x) ==> A {\<sqsubseteq>r} A"
(*<*) by (unfold lesubstep_type_def) auto (*>*)

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


lemma list_update_le_listI [rule_format]:
  "set xs ⊆ A --> set ys ⊆ A --> xs [\<sqsubseteq>r] ys --> p < size xs -->  
   x \<sqsubseteq>r ys!p --> semilat(A,r,f) --> x∈A --> 
   xs[p := x \<squnion>f xs!p] [\<sqsubseteq>r] ys"
(*<*)
  apply (unfold Listn.le_def lesub_def semilat_def)
  apply (simp add: list_all2_conv_all_nth nth_list_update)
  done
(*>*)


lemma plusplus_closed: includes semilat shows
  "!!y. [| set x ⊆ A; y ∈ A|] ==> x \<Squnion>f y ∈ A"
(*<*)
proof (induct x)
  show "!!y. y ∈ A ==> [] \<Squnion>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 \<Squnion>f y ∈ A"
  from xs obtain x: "x ∈ A" and "set xs ⊆ A" by simp
  from x y have "x \<squnion>f y ∈ A" ..
  with xs have "xs \<Squnion>f (x \<squnion>f y) ∈ A" by - (rule IH)
  thus "x#xs \<Squnion>f y ∈ A" by simp
qed
(*>*)

lemma (in semilat) pp_ub2:
 "!!y. [| set x ⊆ A; y ∈ A|] ==> y \<sqsubseteq>r x \<Squnion>f y"
(*<*)
proof (induct x)
  from semilat show "!!y. y \<sqsubseteq>r [] \<Squnion>f 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
  assume "!!y. [|set l ⊆ A; y ∈ A|] ==> y \<sqsubseteq>r l \<Squnion>f y"
  hence IH: "!!y. y ∈ A ==> y \<sqsubseteq>r l \<Squnion>f y" .

  from a y have "y \<sqsubseteq>r a \<squnion>f y" ..
  also from a y have "a \<squnion>f y ∈ A" ..
  hence "(a \<squnion>f y) \<sqsubseteq>r l \<Squnion>f (a \<squnion>f y)" by (rule IH)
  finally have "y \<sqsubseteq>r l \<Squnion>f (a \<squnion>f y)" .
  thus "y \<sqsubseteq>r (a#l) \<Squnion>f y" by simp
qed
(*>*)


lemma (in semilat) pp_ub1:
shows "!!y. [|set ls ⊆ A; y ∈ A; x ∈ set ls|] ==> x \<sqsubseteq>r ls \<Squnion>f y"
(*<*)
proof (induct ls)
  show "!!y. x ∈ set [] ==> x \<sqsubseteq>r [] \<Squnion>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 \<sqsubseteq>r ls \<Squnion>f y"
  hence IH: "!!y. x ∈ set ls ==> y ∈ A ==> x \<sqsubseteq>r ls \<Squnion>f y" .

  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 \<sqsubseteq>r s \<squnion>f y" ..
    also from s y have "s \<squnion>f y ∈ A" ..
    with ls have "(s \<squnion>f y) \<sqsubseteq>r ls \<Squnion>f (s \<squnion>f y)" by (rule pp_ub2)
    finally have "s \<sqsubseteq>r ls \<Squnion>f (s \<squnion>f y)" .
    with xs have "x \<sqsubseteq>r ls \<Squnion>f (s \<squnion>f y)" by simp
  } 
  moreover {
    assume "x ∈ set ls"
    hence "!!y. y ∈ A ==> x \<sqsubseteq>r ls \<Squnion>f y" by (rule IH)
    moreover from s y have "s \<squnion>f y ∈ A" ..
    ultimately have "x \<sqsubseteq>r ls \<Squnion>f (s \<squnion>f y)" .
  }
  ultimately 
  have "x \<sqsubseteq>r ls \<Squnion>f (s \<squnion>f y)" by blast
  thus "x \<sqsubseteq>r (s#ls) \<Squnion>f y" by simp
qed
(*>*)


lemma (in semilat) pp_lub:
  assumes "z ∈ A"
  shows 
  "!!y. y ∈ A ==> set xs ⊆ A ==> ∀x ∈ set xs. x \<sqsubseteq>r z ==> y \<sqsubseteq>r z ==> xs \<Squnion>f y \<sqsubseteq>r z"
(*<*)
proof (induct xs)
  fix y assume "y \<sqsubseteq>r z" thus "[] \<Squnion>f y \<sqsubseteq>r 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 \<sqsubseteq>r z"
  then obtain "l \<sqsubseteq>r z" and lsz: "∀x ∈ set ls. x \<sqsubseteq>r z" by auto
  assume "y \<sqsubseteq>r z" have "l \<squnion>f y \<sqsubseteq>r z" ..  
  moreover
  from l y have "l \<squnion>f y ∈ A" ..
  moreover
  assume "!!y. y ∈ A ==> set ls ⊆ A ==> ∀x ∈ set ls. x \<sqsubseteq>r z ==> y \<sqsubseteq>r z
          ==> ls \<Squnion>f y \<sqsubseteq>r z"
  ultimately
  have "ls \<Squnion>f (l \<squnion>f y) \<sqsubseteq>r z" using ls lsz by -
  thus "(l#ls) \<Squnion>f y \<sqsubseteq>r z" by simp
qed
(*>*)


lemma ub1': includes semilat
shows "[|∀(p,s) ∈ set S. s ∈ A; y ∈ A; (a,b) ∈ set S|] 
  ==> b \<sqsubseteq>r map snd [(p', t')∈S. p' = a] \<Squnion>f y" 
(*<*)
proof -
  let "b \<sqsubseteq>r ?map \<Squnion>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' \<squnion>f ss ! q = ss ! q ==>
   (map snd [(p', t')∈ S. p' = q] \<Squnion>f ss ! q) = ss ! q"
(*<*)
apply (induct S)
apply auto 
done
(*>*)


end