(*  Title:      HOL/MicroJava/BV/Kildall.thy
    Author:     Tobias Nipkow, Gerwin Klein
    Copyright   2000 TUM

Kildall's algorithm.
*)

section ‹Kildall's Algorithm \label{sec:Kildall}›

theory Kildall_1
imports SemilatAlg
begin

primrec merges :: "'s binop → (nat × 's) list → 's list → 's list"
where
  "merges f [] τs = τs"
| "merges f (p'#ps) τs = (let (p,τ) = p' in merges f ps (τs[p := τ ⊔ τs!p]))"


lemmas [simp] = Let_def Semilat.le_iff_plus_unchanged [OF Semilat.intro, symmetric]


lemma (in Semilat) nth_merges:
 "∧ss. [p < length ss; ss ∈ nlists n A; ∀(p,t)∈set ps. p<n ∧ t∈A ] ==>
  (merges f ps ss)!p = map snd [(p',t') ← ps. p'=p] ⊔ ss!p"
  (is "∧ss. [_; _; ?steptype ps] ==> ?P ss ps")
(*<*)
proof (induct ps)
  show "∧ss. ?P ss []" by simp

  fix ss p' ps'
  assume ss: "ss ∈ nlists n A"
  assume l:  "p < length ss"
  assume "?steptype (p'#ps')"
  then obtain a b where
    p': "p'=(a,b)" and ab: "a<n" "b∈A" and ps': "?steptype ps'"
    by (cases p') auto
  assume "∧ss. p< length ss ==> ss ∈ nlists n A ==> ?steptype ps' ==> ?P ss ps'"
  hence IH: "∧ss. ss ∈ nlists n A ==> p < length ss ==> ?P ss ps'" using ps' by iprover

  from ss ab
  have "ss[a := b ⊔ ss!a] ∈ nlists n A" by (simp add: closedD)
  moreover
  with l have "p < length (ss[a := b ⊔ ss!a])" by simp
  ultimately
  have "?P (ss[a := b ⊔ ss!a]) ps'" by (rule IH)
  with p' l
  show "?P ss (p'#ps')" by simp
qed
(*>*)


(** merges **)

lemma length_merges [simp]:
  "∧ss. size(merges f ps ss) = size ss"
(*<*) by (induct ps, auto) (*>*)

lemma (in Semilat) merges_preserves_type_lemma:
shows "∀xs. xs ∈ nlists n A ⟶ (∀(p,x) ∈ set ps. p<n ∧ x∈A)
         ⟶ merges f ps xs ∈ nlists n A"
(*<*)
apply (insert closedI)
apply (unfold closed_def)
apply (induct ps)
 apply simp
apply clarsimp
done
(*>*)

lemma (in Semilat) merges_preserves_type [simp]:
 "[ xs ∈ nlists n A; ∀(p,x) ∈ set ps. p<n ∧ x∈A ]
  ==> merges f ps xs ∈ nlists n A"
by (simp add: merges_preserves_type_lemma)

lemma (in Semilat) list_update_le_listI [rule_format]:
  "set xs ⊆ A ⟶ set ys ⊆ A ⟶ xs [⊑] ys ⟶ p < size xs ⟶
   x ⊑ ys!p ⟶ x∈A ⟶ xs[p := x ⊔ xs!p] [⊑] ys"
(*<*)
  apply (insert semilat)
  apply (simp only: Listn.le_def lesub_def semilat_def)
  apply (simp add: list_all2_conv_all_nth nth_list_update)
  done
(*>*)

lemma (in Semilat) merges_pres_le_ub:
  assumes "set ts ⊆ A"  "set ss ⊆ A"
    "∀(p,t)∈set ps. t ⊑ ts!p ∧ t ∈ A ∧ p < size ts"  "ss [⊑] ts"
  shows "merges f ps ss [⊑] ts"
(*<*)
proof -
  { fix t ts ps
    have
    "∧qs. [set ts ⊆ A; ∀(p,t)∈set ps. t ⊑ ts!p ∧ t ∈ A ∧ p< size ts ] ==>
    set qs ⊆ set ps ⟶
    (∀ss. set ss ⊆ A ⟶ ss [⊑] ts ⟶ merges f qs ss [⊑] ts)"
    apply (induct_tac qs)
     apply simp
    apply (simp (no_asm_simp))
    apply clarify
    apply simp
    apply (erule allE, erule impE, erule_tac [2] mp)
     apply (drule bspec, assumption)
     apply (simp add: closedD)
    apply (drule bspec, assumption)
    apply (simp add: list_update_le_listI)
    done 
  } note this [dest]  
  from assms show ?thesis by blast
qed
(*>*)




end