Theory SemilatAlg

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

section ‹More on Semilattices›

theory SemilatAlg
imports Typing_Framework Product
begin

definition 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) auto

lemma lesub_step_typeD:
  "a ≤|r| b ⟹ (x,y) ∈ set a ⟹ ∃y'. (x, y') ∈ set 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 (unfold 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 ++_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
  qed
qed

lemma (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 simp
qed


lemma (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 simp
qed


lemma (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 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 <=_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 simp
qed


lemma 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')←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') ← S. p' = q] ++_f ss ! q) = ss ! q"
  by (induct S) auto 

end