Theory Kildall_1

(*  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 := τ ⊔⇘f⇙ τ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] ⨆⇘f⇙ 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 ⊔⇘f⇙ ss!a] ∈ nlists n A" by (simp add: closedD)
  moreover
  with l have "p < length (ss[a := b ⊔⇘f⇙ ss!a])" by simp
  ultimately
  have "?P (ss[a := b ⊔⇘f⇙ 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 [⊑⇘r⇙] ys ⟶ p < size xs ⟶  
   x ⊑⇘r⇙ ys!p ⟶ x∈A ⟶ xs[p := x ⊔⇘f⇙ xs!p] [⊑⇘r⇙] 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 ⊑⇘r⇙ ts!p ∧ t ∈ A ∧ p < size ts"  "ss [⊑⇘r⇙] ts"
  shows "merges f ps ss [⊑⇘r⇙] ts"
(*<*)
proof -
  { fix t ts ps
    have
    "⋀qs. ⟦set ts ⊆ A; ∀(p,t)∈set ps. t ⊑⇘r⇙ ts!p ∧ t ∈ A ∧ p< size ts ⟧ ⟹
    set qs ⊆ set ps  ⟶ 
    (∀ss. set ss ⊆ A ⟶ ss [⊑⇘r⇙] ts ⟶ merges f qs ss [⊑⇘r⇙] 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