# Theory Kildall_2

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

Kildall's algorithm.
*)

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

theory Kildall_2
imports SemilatAlg Kildall_1
begin

primrec propa :: "'s binop ⇒ (nat × 's) list ⇒ 's list ⇒ nat set ⇒ 's list * nat set"
where
"propa f []      τs w = (τs,w)"
| "propa f (q'#qs) τs w = (let (q,τ) = q';
u = τ ⊔⇘f⇙ τs!q;
w' = (if u = τs!q then w else insert q w)
in propa f qs (τs[q := u]) w')"

definition iter :: "'s binop ⇒ 's step_type ⇒
's list ⇒ nat set ⇒ 's list × nat set"
where
"iter f step τs w =
while (λ(τs,w). w ≠ {})
(λ(τs,w). let p = SOME p. p ∈ w
in propa f (step p (τs!p)) τs (w-{p}))
(τs,w)"

definition unstables :: "'s ord ⇒ 's step_type ⇒ 's list ⇒ nat set"
where
"unstables r step τs = {p. p < size τs ∧ ¬stable r step τs p}"

definition kildall :: "'s ord ⇒ 's binop ⇒ 's step_type ⇒ 's list ⇒ 's list"
where
"kildall r f step τs = fst(iter f step τs (unstables r step τs))"

(** propa **)
lemma (in Semilat) merges_incr_lemma:
"∀xs. xs ∈ nlists n A ⟶ (∀(p,x)∈set ps. p<size xs ∧ x ∈ A) ⟶ xs [⊑⇘r⇙] merges f ps xs"
apply (induct ps)
apply simp
apply(insert orderI)
apply (fastforce intro:le_list_refl')
apply simp
apply clarify
apply (rule order_trans)
defer
apply (erule list_update_incr)
apply simp+
done

(*>*)

lemma (in Semilat) merges_incr:
"⟦ xs ∈ nlists n A; ∀(p,x)∈set ps. p<size xs ∧ x ∈ A ⟧
⟹ xs [⊑⇘r⇙] merges f ps xs"
by (simp add: merges_incr_lemma)

lemma (in Semilat) merges_same_conv [rule_format]:
"(∀xs. xs ∈ nlists n A ⟶ (∀(p,x)∈set ps. p<size xs ∧ x∈A) ⟶
(merges f ps xs = xs) = (∀(p,x)∈set ps. x ⊑⇘r⇙ xs!p))"
(*<*)
apply (induct_tac ps)
apply simp
apply clarsimp
apply (rename_tac p x ps xs)
apply (rule iffI)
apply (rule context_conjI)
apply (subgoal_tac "xs[p := x ⊔⇘f⇙ xs!p] [⊑⇘r⇙] xs")
apply (fastforce dest!: le_listD)  ―‹apply (force dest!: le_listD simp add: nth_list_update) ›
apply (erule subst, rule merges_incr)
apply (blast intro!: nlistsE_set intro: closedD nlistsE_length [THEN nth_in])
apply clarify
apply (rule conjI)
apply simp
apply (blast dest: boundedD)
apply blast
apply clarify
apply (erule allE)
apply (erule impE)
apply assumption
apply (drule bspec)
apply assumption
apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2])
apply blast
apply clarify
apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2])
done
(*>*)

lemma decomp_propa:
"⋀ss w. (∀(q,t)∈set qs. q < size ss) ⟹
propa f qs ss w =
(merges f qs ss, {q. ∃t.(q,t)∈set qs ∧ t ⊔⇘f⇙ ss!q ≠ ss!q} ∪ w)"
(*<*)
apply (induct qs)
apply simp
apply (simp (no_asm))
apply clarify
apply simp
apply (rule conjI)
apply blast
apply (simp add: nth_list_update)
apply blast
done
(*>*)

lemma (in Semilat) stable_pres_lemma:
shows "⟦pres_type step n A; bounded step n;
ss ∈ nlists n A; p ∈ w; ∀q∈w. q < n;
∀q. q < n ⟶ q ∉ w ⟶ stable r step ss q; q < n;
∀s'. (q,s') ∈ set (step p (ss!p)) ⟶ s' ⊔⇘f⇙ ss!q = ss!q;
q ∉ w ∨ q = p ⟧
⟹ stable r step (merges f (step p (ss!p)) ss) q"
(*<*)
apply (unfold stable_def)
apply (subgoal_tac "∀s'. (q,s') ∈ set (step p (ss!p)) ⟶ s' : A")
prefer 2
apply clarify
apply (erule pres_typeD)
prefer 3 apply assumption
apply (rule nlistsE_nth_in)
apply assumption
apply simp
apply simp
apply simp
apply clarify
apply (subst nth_merges)
apply simp
apply (blast dest: boundedD)
apply assumption
apply clarify
apply (rule conjI)
apply (blast dest: boundedD)
apply (erule pres_typeD)
prefer 3 apply assumption
apply simp
apply simp
apply(subgoal_tac "q < length ss")
prefer 2 apply simp
apply (frule nth_merges [of q _ _ "step p (ss!p)"]) (* fixme: why does method subst not work?? *)
apply assumption
apply clarify
apply (rule conjI)
apply (blast dest: boundedD)
apply (erule pres_typeD)
prefer 3 apply assumption
apply simp
apply simp
apply (drule_tac P = "λx. (a, b) ∈ set (step q x)" in subst)
apply assumption

apply (simp add: plusplus_empty)
apply (cases "q ∈ w")
apply simp
apply (rule ub1')
apply (rule Semilat.intro)
apply (rule semilat)
apply clarify
apply (rule pres_typeD)
apply assumption
prefer 3 apply assumption
apply (blast intro: nlistsE_nth_in dest: boundedD)
apply (blast intro: pres_typeD dest: boundedD)
apply (blast intro: nlistsE_nth_in dest: boundedD)
apply assumption

apply simp
apply (erule allE, erule impE, assumption, erule impE, assumption)
apply (rule order_trans)
apply fastforce
defer
apply (rule pp_ub2)
apply simp
apply clarify
apply simp
apply (rule pres_typeD)
apply assumption
prefer 3
apply assumption
apply (blast intro: nlistsE_nth_in)
apply (blast)
apply (blast intro: nlistsE_nth_in dest: boundedD)
prefer 4
apply fastforce
apply (blast intro: nlistsE_nth_in dest: pres_typeD)
apply (blast intro: nlistsE_nth_in dest: boundedD)
apply(subgoal_tac "∀(q,t) ∈ set (step p (ss!p)). q < n ∧ t ∈ A")

apply (subgoal_tac "merges f (step p (ss!p)) ss ∈ nlists n A")
defer
apply (blast dest:merges_preserves_type)
defer
apply (subgoal_tac "a < n")
defer
apply (blast intro: nlistsE_nth_in  boundedD )
defer
apply (subgoal_tac "merges f (step p (ss ! p)) ss ! a =
map snd (filter (λ(p', t'). p' = a) (step p (ss ! p))) ⨆⇘f⇙ ss ! a")
apply (fastforce  dest: nlistsE_nth_in ) (* slow *)
apply (subgoal_tac "a < length ss")
apply (fastforce dest:nth_merges)
apply simp
apply (intro strip)
apply auto
defer
apply (auto intro:boundedD)
apply (fastforce intro: nlistsE_nth_in dest:pres_typeD)
done
(*>*)

lemma (in Semilat) merges_bounded_lemma:
"⟦ mono r step n A; bounded step n; pres_type step n A;
∀(p',s') ∈ set (step p (ss!p)). s' ∈ A; ss ∈ nlists n A; ts ∈ nlists n A; p < n;
ss [⊑⇩r] ts; ∀p. p < n ⟶ stable r step ts p ⟧
⟹ merges f (step p (ss!p)) ss [⊑⇩r] ts"
(*<*)
apply (unfold stable_def)
apply (rule merges_pres_le_ub)
apply simp
apply simp
prefer 2 apply assumption

apply clarsimp
apply (drule boundedD, assumption+)
apply (erule allE, erule impE, assumption)
apply (drule bspec, assumption)
apply simp

apply (drule monoD [of _ _ _ _ p "ss!p"  "ts!p"])
apply assumption
apply simp
apply (simp add: le_listD)

apply (drule lesub_step_typeD, assumption)
apply clarify
apply (drule bspec, assumption)
apply simp

apply (rule order_trans)
apply fastforce
apply simp
apply simp
apply simp
apply (auto intro:boundedD)

apply (blast intro: nlistsE_nth_in dest:pres_typeD)
done
(*>*)

(** iter **)
lemma termination_lemma: assumes "Semilat A r f"
shows "⟦ ss ∈ nlists n A; ∀(q,t)∈set qs. q<n ∧ t∈A; p∈w ⟧ ⟹
ss [⊏⇩r] merges f qs ss ∨
merges f qs ss = ss ∧ {q. ∃t. (q,t)∈set qs ∧ t ⊔⇘f⇙ ss!q ≠ ss!q} ∪ (w-{p}) ⊂ w"
(*<*) (is "PROP ?P")
proof -
interpret Semilat A r f by fact
show "PROP ?P"
apply(insert semilat)
apply (unfold lesssub_def)
apply (simp (no_asm_simp) add: merges_incr)
apply (rule impI)
apply (rule merges_same_conv [THEN iffD1, elim_format])
apply assumption+
defer
apply (rule sym, assumption)
defer apply simp
apply (subgoal_tac "∀q t. ¬((q, t) ∈ set qs ∧ t ⊔⇘f⇙ ss ! q ≠ ss ! q)")
apply (blast intro!: psubsetI elim: equalityE)
apply clarsimp
apply (drule bspec, assumption)
apply (drule bspec, assumption)
apply clarsimp
done
qed
(*>*)

end