Theory SemilatAlg

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

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

theory SemilatAlg
imports Typing_Framework
begin

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

primrec pluslussub :: "'a list => ('a => 'a => 'a) => 'a => 'a" 
where
  "pluslussub [] f y = y"
| "pluslussub (x#xs) f y = pluslussub xs f (x \<squnion>⇩f y)"
(*<*)
notation
  pluslussub  ("(_ /++'__ _)" [65, 1000, 66] 65)
(*>*)
notation (xsymbols)
  pluslussub  ("(_ /\<Squnion>⇘_⇙ _)" [65, 0, 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 ∧ τ \<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:
  "[| A⇣1 {\<sqsubseteq>⇘r⇙} B⇣1; A⇣2 {\<sqsubseteq>⇘r⇙} B⇣2 |] ==> A⇣1 ∪ A⇣2 {\<sqsubseteq>⇘r⇙} B⇣1 ∪ B⇣2"
  (*<*) 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)
  apply (simp add: lesub_def)
  done
(*>*)

lemma plusplus_closed: assumes "Semilat A r f" shows
  "!!y. [| set x ⊆ A; y ∈ A|] ==> x \<Squnion>⇘f⇙ y ∈ A"
(*<*)
proof (induct x)
  interpret Semilat A r f by fact
  show "!!y. y ∈ A ==> [] \<Squnion>⇘f⇙ 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 \<Squnion>⇘f⇙ y ∈ A"
  from xxs obtain x: "x ∈ A" and xs: "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"
  from this and x have 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"
  from this and ls have 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: "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 lz: "l \<sqsubseteq>⇘r⇙ z" and lsz: "∀x ∈ set ls. x \<sqsubseteq>⇘r⇙ z" by auto
  assume "y \<sqsubseteq>⇘r⇙ z" with lz have "l \<squnion>⇘f⇙ y \<sqsubseteq>⇘r⇙ z" using l y 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': assumes "Semilat A r f"
shows "[|∀(p,s) ∈ set S. s ∈ A; y ∈ A; (a,b) ∈ set S|] 
  ==> b \<sqsubseteq>⇘r⇙ map snd [(p', t') \<leftarrow> S. p' = a] \<Squnion>⇘f⇙ y" 
(*<*)
proof -
  interpret Semilat A r f by fact
  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') \<leftarrow> S. p' = q] \<Squnion>⇘f⇙ ss ! q) = ss ! q"
(*<*)
apply (induct S)
apply auto 
done
(*>*)


end