# Theory Kildall

(*  Title:      JinjaThreads/DFA/Kildall.thy
Author:     Tobias Nipkow, Gerwin Klein, Andreas Lochbihler

Kildall's algorithm.
*)

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

theory Kildall
imports SemilatAlg "../Basic/Auxiliary"
begin

locale Kildall_base =
fixes s_α :: "'w ⇒ nat set"
and s_empty :: "'w"
and s_is_empty :: "'w ⇒ bool"
and s_choose :: "'w ⇒ nat"
and s_remove :: "nat ⇒ 'w ⇒ 'w"
and s_insert :: "nat ⇒ 'w ⇒ 'w"
begin

primrec propa :: "'s binop ⇒ (nat × 's) list ⇒ 's list ⇒ 'w ⇒ 's list * 'w"
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 s_insert q w)
in propa f qs (τs[q := u]) w')"

definition iter :: "'s binop ⇒ 's step_type ⇒ 's list ⇒ 'w ⇒ 's list × 'w"
where
"iter f step τs w =
while (λ(τs,w). ¬ s_is_empty w)
(λ(τs,w). let p = s_choose w in propa f (step p (τs!p)) τs (s_remove p w))
(τs,w)"

definition unstables :: "'s ord ⇒ 's step_type ⇒ 's list ⇒ 'w"
where
"unstables r step τs = foldr s_insert (filter (λp. ¬stable r step τs p) [0..<size τs]) s_empty"

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

primrec t_α :: "'s list × 'w ⇒ 's list × nat set"
where "t_α (τs, w) = (τs, s_α w)"

end

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

locale Kildall =
Kildall_base +
assumes empty_spec [simp]: "s_α s_empty = {}"
and is_empty_spec [simp]: "s_is_empty A ⟷ s_α A = {}"
and choose_spec: "s_α A ≠ {} ⟹ s_choose A ∈ s_α A"
and remove_spec [simp]: "s_α (s_remove n A) = s_α A - {n}"
and insert_spec [simp]: "s_α (s_insert n A) = insert n (s_α A)"
begin

lemma s_α_foldr_s_insert:
"s_α (foldr s_insert xs A) = foldr insert xs (s_α A)"
by(induct xs arbitrary: A) simp_all

lemma unstables_spec [simp]: "s_α (unstables r step τs) = {p. p < size τs ∧ ¬stable r step τs p}"
proof -
have "{p. p < size τs ∧ ¬stable r step τs p} = foldr insert (filter (λp. ¬stable r step τs p) [0..<size τs]) {}"
unfolding foldr_insert_conv_set by auto
thus ?thesis by(simp add: unstables_def s_α_foldr_s_insert)
qed

end

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

lemma (in Semilat) nth_merges:
"⋀ss. ⟦p < length ss; ss ∈ list 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 ∈ list 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 ∈ list n A ⟹ ?steptype ps' ⟹ ?P ss ps'"
hence IH: "⋀ss. ss ∈ list n A ⟹ p < length ss ⟹ ?P ss ps'" using ps' by iprover

from ss ab
have "ss[a := b ⊔⇘f⇙ ss!a] ∈ list 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 ∈ list n A ⟶ (∀(p,x) ∈ set ps. p<n ∧ x∈A)
⟶ merges f ps xs ∈ list n A"
(*<*)
apply (insert closedI)
apply (unfold Semilat.closed_def)
apply (induct ps)
apply simp
apply clarsimp
done
(*>*)

lemma (in Semilat) merges_preserves_type [simp]:
"⟦ xs ∈ list n A; ∀(p,x) ∈ set ps. p<n ∧ x∈A ⟧
⟹ merges f ps xs ∈ list n A"

lemma (in Semilat) merges_incr_lemma:
"∀xs. xs ∈ list n A ⟶ (∀(p,x)∈set ps. p<size xs ∧ x ∈ A) ⟶ xs [⊑⇘r⇙] merges f ps xs"
(*<*)
apply (induct ps)
apply simp
apply simp
apply clarify
apply (rule order_trans)
apply simp
apply (erule list_update_incr)
apply simp
apply simp
apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
done
(*>*)

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

lemma (in Semilat) merges_same_conv [rule_format]:
"(∀xs. xs ∈ list 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 (force dest!: le_listD simp add: nth_list_update)
apply (erule subst, rule merges_incr)
apply (blast intro!: listE_set intro: closedD listE_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 (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)
apply (drule bspec, assumption)
done
} note this [dest]
from assms show ?thesis by blast
qed
(*>*)

context Kildall begin

subsection ‹@{term propa}›

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

end

lemma (in Semilat) stable_pres_lemma:
shows "⟦pres_type step n A; bounded step n;
ss ∈ list 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 listE_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 (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: listE_nth_in dest: boundedD)
apply (blast intro: pres_typeD dest: boundedD)
apply (blast intro: listE_nth_in dest: boundedD)
apply assumption

apply simp
apply (erule allE, erule impE, assumption, erule impE, assumption)
apply (rule order_trans)
apply simp
defer
apply (rule pp_ub2)(*
apply assumption*)
apply simp
apply clarify
apply simp
apply (rule pres_typeD)
apply assumption
prefer 3 apply assumption
apply (blast intro: listE_nth_in dest: boundedD)
apply (blast intro: pres_typeD dest: boundedD)
apply (blast intro: listE_nth_in dest: boundedD)
apply blast
done
(*>*)

lemma (in Semilat) merges_bounded_lemma:
"⟦ mono r step n A; bounded step n;
∀(p',s') ∈ set (step p (ss!p)). s' ∈ A; ss ∈ list n A; ts ∈ list 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 (drule lesub_step_typeD, assumption)
apply clarify
apply (drule bspec, assumption)
apply simp
apply (blast intro: order_trans)
done
(*>*)

lemma termination_lemma: assumes "Semilat A r f"
shows "⟦ ss ∈ list 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 (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
(*>*)

context Kildall_base begin

definition s_finite_psubset  :: "('w * 'w) set"
where "s_finite_psubset == {(A,B). s_α A < s_α B & finite (s_α B)}"

lemma s_finite_psubset_inv_image:
"s_finite_psubset = inv_image finite_psubset s_α"

lemma wf_s_finite_psubset [simp]: "wf s_finite_psubset"
unfolding s_finite_psubset_inv_image by simp

end

context Kildall begin

subsection ‹@{term iter}›

lemma iter_properties[rule_format]: assumes "Semilat A r f"
shows "⟦ acc A r; pres_type step n A; mono r step n A;
bounded step n; ∀p∈s_α w0. p < n; ss0 ∈ list n A;
∀p<n. p ∉ s_α w0 ⟶ stable r step ss0 p ⟧ ⟹
t_α (iter f step ss0 w0) = (ss',w')
⟶
ss' ∈ list n A ∧ stables r step ss' ∧ ss0 [⊑⇩r] ss' ∧
(∀ts∈list n A. ss0 [⊑⇩r] ts ∧ stables r step ts ⟶ ss' [⊑⇩r] ts)"
(*<*) (is "PROP ?P")
proof -
interpret Semilat A r f by fact
show "PROP ?P"
apply(insert semilat)
apply (unfold iter_def stables_def)
apply(unfold is_empty_spec)
apply (rule_tac P = "λ(ss,w).
ss ∈ list n A ∧ (∀p<n. p ∉ s_α w ⟶ stable r step ss p) ∧ ss0 [⊑⇩r] ss ∧
(∀ts∈list n A. ss0 [⊑⇩r] ts ∧ stables r step ts ⟶ ss [⊑⇩r] ts) ∧
(∀p∈ s_α w. p < n)" and
r = "{(ss',ss) . ss ∈ list n A ∧ ss' ∈ list n A ∧ ss [⊏⇩r] ss'} <*lex*> s_finite_psubset"
in while_rule)

― ‹Invariant holds initially:›

― ‹Invariant is preserved:›
apply(rename_tac ss w)
apply(subgoal_tac "s_choose w ∈ s_α w")
prefer 2 apply(erule choose_spec)
apply(subgoal_tac "∀(q,t) ∈ set (step (s_choose w) (ss ! (s_choose w))). q < length ss ∧ t ∈ A")
prefer 2
apply clarify
apply (rule conjI)
apply(clarsimp, blast dest!: boundedD)
apply (erule pres_typeD)
prefer 3
apply assumption
apply (erule listE_nth_in)
apply blast
apply blast
apply(subgoal_tac "(λ(ss, w).
ss ∈ list n A ∧
(∀p<n. p ∉ w ⟶ stable r step ss p) ∧
ss0 [⊑⇘r⇙] ss ∧
(∀ts∈list n A.
ss0 [⊑⇘r⇙] ts ∧ (∀p<n. stable r step ts p) ⟶ ss [⊑⇘r⇙] ts) ∧
(∀p∈w. p < n))
(t_α (propa f (step (s_choose w) (ss ! s_choose w)) ss
(s_remove (s_choose w) w)))")
apply(case_tac "propa f (step (s_choose w) (ss ! s_choose w)) ss (s_remove (s_choose w) w)")
apply(simp)
apply (subst decomp_propa)
apply blast
apply simp
apply (rule conjI)
apply (rule merges_preserves_type)
apply blast
apply clarify
apply (rule conjI)
apply(clarsimp, blast dest!: boundedD)
apply (erule pres_typeD)
prefer 3
apply assumption
apply (erule listE_nth_in)
apply blast
apply blast
apply (rule conjI)
apply clarify
apply (blast intro!: stable_pres_lemma)
apply (rule conjI)
apply (blast intro!: merges_incr intro: le_list_trans)
apply (rule conjI)
apply clarsimp
apply (blast intro!: merges_bounded_lemma)
apply (blast dest!: boundedD)

― ‹Postcondition holds upon termination:›

― ‹Well-foundedness of the termination relation:›
apply (rule wf_lex_prod)
apply (insert orderI [THEN acc_le_listI])
apply (simp only: acc_def lesssub_def)
apply (rule wf_s_finite_psubset)

― ‹Loop decreases along termination relation:›
apply(rename_tac ss w)
apply(subgoal_tac "s_choose w ∈ s_α w")
prefer 2 apply (erule choose_spec)
apply(subgoal_tac "∀(q,t) ∈ set (step (s_choose w) (ss ! (s_choose w))). q < length ss ∧ t ∈ A")
prefer 2
apply clarify
apply (rule conjI)
apply(clarsimp, blast dest!: boundedD)
apply (erule pres_typeD)
prefer 3
apply assumption
apply (erule listE_nth_in)
apply blast
apply blast
apply(subgoal_tac "(t_α (propa f (step (s_choose w) (ss ! s_choose w)) ss
(s_remove (s_choose w) w)),
ss, s_α w)
∈ {(ss', ss). ss ∈ list n A ∧ ss' ∈ list n A ∧ ss [⊏⇘r⇙] ss'} <*lex*> finite_psubset")
prefer 2
apply (subst decomp_propa)
apply blast
apply clarify
apply (simp del: listE_length
apply(subgoal_tac "merges f (step (s_choose w) (ss ! s_choose w)) ss ∈ list n A")
apply simp
apply (rule termination_lemma)
apply (rule assms)
apply assumption+
apply clarsimp
apply(case_tac "propa f (step (s_choose w) (ss ! s_choose w)) ss
(s_remove (s_choose w) w)")
done
qed
(*>*)

lemma kildall_properties: assumes "Semilat A r f"
shows "⟦ acc A r; pres_type step n A; mono r step n A;
bounded step n; ss0 ∈ list n A ⟧ ⟹
kildall r f step ss0 ∈ list n A ∧
stables r step (kildall r f step ss0) ∧
ss0 [⊑⇩r] kildall r f step ss0 ∧
(∀ts∈list n A. ss0 [⊑⇩r] ts ∧ stables r step ts ⟶
kildall r f step ss0 [⊑⇩r] ts)"
(*<*) (is "PROP ?P")
proof -
interpret Semilat A r f by fact
show "PROP ?P"
apply (unfold kildall_def)
apply(case_tac "iter f step ss0 (unstables r step ss0)")
apply(simp)
apply (rule iter_properties[where ?w0.0="unstables r step ss0"])
apply(rule assms)
apply (simp_all add: unstables_def stable_def s_α_foldr_s_insert foldr_insert_conv_set)
done
qed

lemma is_bcv_kildall: assumes "Semilat A r f"
shows "⟦ acc A r; top r T; pres_type step n A; bounded step n; mono r step n A ⟧
⟹ is_bcv r T step n A (kildall r f step)" (is "PROP ?P")
proof -
interpret Semilat A r f by fact
show "PROP ?P"
apply(unfold is_bcv_def wt_step_def)
apply(insert ‹Semilat A r f› semilat kildall_properties[of A])
apply clarify
apply(subgoal_tac "kildall r f step τs⇩0 ∈ list n A")
prefer 2 apply (simp(no_asm_simp))
apply (rule iffI)
apply (rule_tac x = "kildall r f step τs⇩0" in bexI)
apply (rule conjI)
apply (blast)
apply (simp  (no_asm_simp))
apply(assumption)
apply clarify
apply(subgoal_tac "kildall r f step τs⇩0!p <=_r τs!p")
apply simp
apply (blast intro!: le_listD less_lengthI)
done
qed
(*>*)

end

interpretation Kildall "set" "[]" "λxs. xs = []" "hd" "removeAll" "Cons"
by(unfold_locales) auto

lemmas kildall_code [code] =
kildall_def
Kildall_base.propa.simps
Kildall_base.iter_def
Kildall_base.unstables_def
Kildall_base.kildall_def

end