# Theory Jinja.Kildall_1

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

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"

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