(* Title: HOL/MicroJava/DFA/Kildall.thy
Author: Tobias Nipkow, Gerwin Klein
Copyright 2000 TUM
*)
section \<open>Kildall's Algorithm \label{sec:Kildall}\<close>
theory Kildall
imports SemilatAlg "HOL-Library.While_Combinator"
begin
primrec propa :: "'s binop \ (nat \ 's) list \ 's list \ nat set \ 's list * nat set" where
"propa f [] ss w = (ss,w)"
| "propa f (q'#qs) ss w = (let (q,t) = q';
u = t +_f ss!q;
w' = (if u = ss!q then w else insert q w)
in propa f qs (ss[q := u]) w')"
definition iter :: "'s binop \ 's step_type \ 's list \ nat set \ 's list \ nat set" where
"iter f step ss w == while (%(ss,w). w \ {})
(%(ss,w). let p = SOME p. p \<in> w
in propa f (step p (ss!p)) ss (w-{p}))
(ss,w)"
definition unstables :: "'s ord \ 's step_type \ 's list \ nat set" where
"unstables r step ss == {p. p < size ss \ \stable r step ss p}"
definition kildall :: "'s ord \ 's binop \ 's step_type \ 's list \ 's list" where
"kildall r f step ss == fst(iter f step ss (unstables r step ss))"
primrec merges :: "'s binop \ (nat \ 's) list \ 's list \ 's list" where
"merges f [] ss = ss"
| "merges f (p'#ps) ss = (let (p,s) = p' in merges f ps (ss[p := s +_f ss!p]))"
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 t\A \ \
(merges f ps ss)!p = map snd [(p',t') \<leftarrow> 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\<in>A" and ps': "?steptype ps'"
by (cases p') auto
assume "\ss. p< length ss \ ss \ list n A \ ?steptype ps' \ ?P ss ps'"
from this [OF _ _ ps'] have IH: "\ss. ss \ list n A \ p < length ss \ ?P ss ps'" .
from ss ab
have "ss[a := b +_f ss!a] \ list n A" by (simp add: closedD)
moreover
from calculation 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]: "size(merges f ps ss) = size ss"
by (induct ps arbitrary: ss) auto
lemma (in Semilat) merges_preserves_type_lemma:
shows "\xs. xs \ list n A \ (\(p,x) \ set ps. p x\A)
\<longrightarrow> merges f ps xs \<in> list n A"
apply (insert closedI)
apply (unfold closed_def)
apply (induct_tac ps)
apply simp
apply clarsimp
done
lemma (in Semilat) merges_preserves_type [simp]:
"\ xs \ list n A; \(p,x) \ set ps. p x\A \
\<Longrightarrow> merges f ps xs \<in> list n A"
by (simp add: merges_preserves_type_lemma)
lemma (in Semilat) merges_incr_lemma:
"\xs. xs \ list n A \ (\(p,x)\set ps. p x \ A) \ xs <=[r] merges f ps xs"
apply (induct_tac 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 x \ A \
\<Longrightarrow> xs <=[r] merges f ps xs"
by (simp add: merges_incr_lemma)
lemma (in Semilat) merges_same_conv [rule_format]:
"(\xs. xs \ list n A \ (\(p,x)\set ps. p x\A) \
(merges f ps xs = xs) = (\<forall>(p,x)\<in>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 (drule_tac p = p in le_listD)
apply simp
apply simp
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 \<longrightarrow> x\<in>A \<longrightarrow> xs[p := x +_f xs!p] <=[r] ys"
apply(insert semilat)
apply (unfold 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" and "set ss <= A"
and "\(p,t)\set ps. t <=_r ts!p \ t \ A \ p < size ts" and "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 \<longrightarrow>
(\<forall>ss. set ss <= A \<longrightarrow> ss <=[r] ts \<longrightarrow> merges f qs ss <=[r] ts)"
apply (induct_tac qs)
apply simp
apply (simp (no_asm_simp))
apply clarify
apply (rotate_tac -2)
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
(** propa **)
lemma decomp_propa:
"\ss w. (\(q,t)\set qs. q < size ss) \
propa f qs ss w =
(merges f qs ss, {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un 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
(** iter **)
lemma (in Semilat) stable_pres_lemma:
shows "\pres_type step n A; bounded step n;
ss \<in> list n A; p \<in> w; \<forall>q\<in>w. q < n;
\<forall>q. q < n \<longrightarrow> q \<notin> w \<longrightarrow> stable r step ss q; q < n;
\<forall>s'. (q,s') \<in> set (step p (ss ! p)) \<longrightarrow> s' +_f ss ! q = ss ! q;
q \<notin> w \<or> q = p \<rbrakk>
\<Longrightarrow> 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 (simp add: plusplus_empty)
apply (cases "q \ w")
apply simp
apply (rule ub1')
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;
\<forall>(p',s') \<in> set (step p (ss!p)). s' \<in> A; ss \<in> list n A; ts \<in> list n A; p < n;
ss <=[r] ts; \<forall>p. p < n \<longrightarrow> stable r step ts p \<rbrakk>
\<Longrightarrow> 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 (blast intro: order_trans)
done
lemma termination_lemma:
assumes semilat: "semilat (A, r, f)"
shows "\ ss \ list n A; \(q,t)\set qs. q t\A; p\w \ \
ss <[r] merges f qs ss \<or>
merges f qs ss = ss \<and> {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un (w-{p}) < w" (is "PROP ?P")
proof -
interpret Semilat A r f using assms by (rule Semilat.intro)
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 elim: equalityE)
apply clarsimp
apply (drule bspec, assumption)
apply (drule bspec, assumption)
apply clarsimp
done
qed
lemma iter_properties[rule_format]:
assumes semilat: "semilat (A, r, f)"
shows "\ acc r ; pres_type step n A; mono r step n A;
bounded step n; \<forall>p\<in>w0. p < n; ss0 \<in> list n A;
\<forall>p<n. p \<notin> w0 \<longrightarrow> stable r step ss0 p \<rbrakk> \<Longrightarrow>
iter f step ss0 w0 = (ss',w')
\<longrightarrow>
ss' \ list n A \ stables r step ss' \ ss0 <=[r] ss' \
(\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss' <=[r] ts)"
(is "PROP ?P")
proof -
interpret Semilat A r f using assms by (rule Semilat.intro)
show "PROP ?P" apply(insert semilat)
apply (unfold iter_def stables_def)
apply (rule_tac P = "%(ss,w).
ss \<in> list n A \<and> (\<forall>p<n. p \<notin> w \<longrightarrow> stable r step ss p) \<and> ss0 <=[r] ss \<and>
(\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss <=[r] ts) \<and>
(\<forall>p\<in>w. p < n)" and
r = "{(ss',ss) . ss <[r] ss'} <*lex*> finite_psubset"
in while_rule)
\<comment> \<open>Invariant holds initially:\<close>
apply (simp add:stables_def)
\<comment> \<open>Invariant is preserved:\<close>
apply(simp add: stables_def split_paired_all)
apply(rename_tac ss w)
apply(subgoal_tac "(SOME p. p \ w) \ w")
prefer 2 apply (fast intro: someI)
apply(subgoal_tac "\(q,t) \ set (step (SOME p. p \ w) (ss ! (SOME p. p \ 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 simp
apply simp
apply (subst decomp_propa)
apply fast
apply simp
apply (rule conjI)
apply (rule merges_preserves_type)
apply blast
apply clarify
apply (rule conjI)
apply(clarsimp, fast 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)
\<comment> \<open>Postcondition holds upon termination:\<close>
apply(clarsimp simp add: stables_def split_paired_all)
\<comment> \<open>Well-foundedness of the termination relation:\<close>
apply (rule wf_lex_prod)
apply (insert orderI [THEN acc_le_listI])
apply (simp add: acc_def lesssub_def wfP_wf_eq [symmetric])
apply (rule wf_finite_psubset)
\<comment> \<open>Loop decreases along termination relation:\<close>
apply(simp add: stables_def split_paired_all)
apply(rename_tac ss w)
apply(subgoal_tac "(SOME p. p \ w) \ w")
prefer 2 apply (fast intro: someI)
apply(subgoal_tac "\(q,t) \ set (step (SOME p. p \ w) (ss ! (SOME p. p \ 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 (subst decomp_propa)
apply blast
apply clarify
apply (simp del: listE_length
add: lex_prod_def finite_psubset_def
bounded_nat_set_is_finite)
apply (rule termination_lemma)
apply assumption+
defer
apply assumption
apply clarsimp
done
qed
lemma kildall_properties:
assumes semilat: "semilat (A, r, f)"
shows "\ acc r; pres_type step n A; mono r step n A;
bounded step n; ss0 \<in> list n A \<rbrakk> \<Longrightarrow>
kildall r f step ss0 \<in> list n A \<and>
stables r step (kildall r f step ss0) \<and>
ss0 <=[r] kildall r f step ss0 \<and>
(\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow>
kildall r f step ss0 <=[r] ts)"
(is "PROP ?P")
proof -
interpret Semilat A r f using assms by (rule Semilat.intro)
show "PROP ?P"
apply (unfold kildall_def)
apply(case_tac "iter f step ss0 (unstables r step ss0)")
apply(simp)
apply (rule iter_properties)
apply (simp_all add: unstables_def stable_def)
apply (rule semilat)
done
qed
lemma is_bcv_kildall:
assumes semilat: "semilat (A, r, f)"
shows "\ acc r; top r T; pres_type step n A; bounded step n; mono r step n A \
\<Longrightarrow> is_bcv r T step n A (kildall r f step)"
(is "PROP ?P")
proof -
interpret Semilat A r f using assms by (rule Semilat.intro)
show "PROP ?P"
apply(unfold is_bcv_def wt_step_def)
apply(insert semilat kildall_properties[of A])
apply(simp add:stables_def)
apply clarify
apply(subgoal_tac "kildall r f step ss \ list n A")
prefer 2 apply (simp(no_asm_simp))
apply (rule iffI)
apply (rule_tac x = "kildall r f step ss" in bexI)
apply (rule conjI)
apply (blast)
apply (simp (no_asm_simp))
apply(assumption)
apply clarify
apply(subgoal_tac "kildall r f step ss!p <=_r ts!p")
apply simp
apply (blast intro!: le_listD less_lengthI)
done
qed
end
¤ Dauer der Verarbeitung: 0.4 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
