Theory SemilatAlg

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

section ‹More on Semilattices›

theory SemilatAlg
imports Typing_Framework
begin

definition lesubstep_type :: "(nat × 's) set  's ord  (nat × 's) set  bool"
    ("(_ /{⊑⇘_⇙} _)" [50, 0, 51] 50)
  where "A {⊑⇘r⇙} 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 τ) {⊑⇘r⇙} set (step p τ'))"

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

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

lemma lesubstep_union:
  " A1 {⊑⇘r⇙} B1; A2 {⊑⇘r⇙} B2   A1  A2 {⊑⇘r⇙} B1  B2"
  (*<*) by (auto simp add: lesubstep_type_def) (*>*)

lemma pres_typeD:
  " pres_type step n A; sA; 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; sA; s ⊑⇩r t   set (step p s) {⊑⇘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 ⊑⇩r x)  A {⊑⇘r⇙} A"
(*<*) by (unfold lesubstep_type_def) auto (*>*)

lemma lesub_step_typeD:
  "A {⊑⇘r⇙} 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)  xA  
   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 ⨆⇘fy  A"
(*<*)
proof (induct x)
  interpret Semilat A r f by fact
  show "y. y  A  [] ⨆⇘fy  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 ⨆⇘fy  A"
  from xxs obtain x: "x  A" and xs: "set xs  A" by simp
  from x y have "x ⊔⇘fy  A" ..
  with xs have "xs ⨆⇘f(x ⊔⇘fy)  A" by (rule IH)
  thus "x#xs ⨆⇘fy  A" by simp
qed
(*>*)

lemma (in Semilat) pp_ub2:
 "y.  set x  A; y  A  y ⊑⇘rx ⨆⇘fy"
(*<*)
proof (induct x)
  from semilat show "y. y ⊑⇘r[] ⨆⇘fy" 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 ⊑⇘rl ⨆⇘fy"
  from this and x have IH: "y. y  A  y ⊑⇘rl ⨆⇘fy" .

  from a y have "y ⊑⇘ra ⊔⇘fy" ..
  also from a y have "a ⊔⇘fy  A" ..
  hence "(a ⊔⇘fy) ⊑⇘rl ⨆⇘f(a ⊔⇘fy)" by (rule IH)
  finally have "y ⊑⇘rl ⨆⇘f(a ⊔⇘fy)" .
  thus "y ⊑⇘r(a#l) ⨆⇘fy" by simp
qed
(*>*)


lemma (in Semilat) pp_ub1:
shows "y. set ls  A; y  A; x  set ls  x ⊑⇘rls ⨆⇘fy"
(*<*)
proof (induct ls)
  show "y. x  set []  x ⊑⇘r[] ⨆⇘fy" 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 ⊑⇘rls ⨆⇘fy"
  from this and ls have IH: "y. x  set ls  y  A  x ⊑⇘rls ⨆⇘fy" .

  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 ⊑⇘rs ⊔⇘fy" ..
    also from s y have "s ⊔⇘fy  A" ..
    with ls have "(s ⊔⇘fy) ⊑⇘rls ⨆⇘f(s ⊔⇘fy)" by (rule pp_ub2)
    finally have "s ⊑⇘rls ⨆⇘f(s ⊔⇘fy)" .
    with xs have "x ⊑⇘rls ⨆⇘f(s ⊔⇘fy)" by simp
  } 
  moreover {
    assume "x  set ls"
    hence "y. y  A  x ⊑⇘rls ⨆⇘fy" by (rule IH)
    moreover from s y have "s ⊔⇘fy  A" ..
    ultimately have "x ⊑⇘rls ⨆⇘f(s ⊔⇘fy)" .
  }
  ultimately 
  have "x ⊑⇘rls ⨆⇘f(s ⊔⇘fy)" by blast
  thus "x ⊑⇘r(s#ls) ⨆⇘fy" by simp
qed
(*>*)


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


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


end