--- a/src/HOL/MicroJava/BV/Kildall.thy Wed Feb 21 15:21:15 2001 +0100
+++ b/src/HOL/MicroJava/BV/Kildall.thy Thu Feb 22 10:18:41 2001 +0100
@@ -8,7 +8,7 @@
header "Kildall's Algorithm"
-theory Kildall = DFA_Framework:
+theory Kildall = DFA_Framework + While_Combinator:
constdefs
pres_type :: "(nat => 's => 's) => nat => 's set => bool"
@@ -19,8 +19,8 @@
!s p t. s : A & p < n & s <=_r t --> step p s <=_r step p t"
consts
- iter :: "('s sl * (nat => 's => 's) * (nat => nat list))
- * 's list * nat set => 's list"
+ iter :: "'s sl \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> 's) \<Rightarrow> (nat \<Rightarrow> nat list) \<Rightarrow>
+ 's list \<Rightarrow> nat set \<Rightarrow> 's list"
propa :: "'s binop => nat list => 's => 's list => nat set => 's list * nat set"
primrec
@@ -29,18 +29,14 @@
w' = (if u = ss!q then w else insert q w)
in propa f qs t (ss[q := u]) w')"
-recdef iter
- "same_fst (%((A,r,f),step,succs). semilat(A,r,f) & acc r)
- (%((A,r,f),step,succs).
- {(ss',ss) . ss <[r] ss'} <*lex*> finite_psubset)"
-"iter(((A,r,f),step,succs),ss,w) =
- (if semilat(A,r,f) & acc r & (!p:w. p < size ss) &
- bounded succs (size ss) & set ss <= A & pres_type step (size ss) A
- then if w={} then ss
- else let p = SOME p. p : w
- in iter(((A,r,f),step,succs),
- propa f (succs p) (step p (ss!p)) ss (w-{p}))
- else arbitrary)"
+defs iter_def:
+"\<lbrakk> semilat Arf; acc(fst(snd Arf)); !p:w. p < size ss; bounded succs (size ss);
+ set ss <= fst Arf; pres_type step (size ss) (fst Arf) \<rbrakk> \<Longrightarrow>
+ iter Arf step succs ss w ==
+ fst(while (%(ss,w). w \<noteq> {})
+ (%(ss,w). let p = SOME p. p : w
+ in propa (snd(snd Arf)) (succs p) (step p (ss!p)) ss (w-{p}))
+ (ss,w))"
constdefs
unstables ::
@@ -51,7 +47,7 @@
kildall :: "'s sl => (nat => 's => 's) => (nat => nat list)
=> 's list => 's list"
"kildall Arf step succs ss ==
- iter((Arf,step,succs),ss,unstables (snd(snd Arf)) step succs ss)"
+ iter Arf step succs ss (unstables (snd(snd Arf)) step succs ss)"
consts merges :: "'s binop => 's => nat list => 's list => 's list"
primrec
@@ -206,92 +202,6 @@
(** iter **)
-recdef_tc iter_wf: iter (1)
- apply (rule wf_same_fst)+
- apply (simp add: split_tupled_all lesssub_def)
- apply (rule wf_lex_prod)
- prefer 2
- apply (rule wf_finite_psubset)
- apply clarify
- apply (drule (1) semilatDorderI [THEN acc_le_listI])
- apply (simp only: acc_def lesssub_def)
- done
-
-lemma inter_tc_lemma:
- "[| semilat(A,r,f); ss : list n A; t:A; ! q:set qs. q < n; p:w |] ==>
- ss <[r] merges f t qs ss |
- merges f t qs ss = ss & {q. q:set qs & t +_f ss!q ~= ss!q} Un (w-{p}) < w"
- 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)
- apply (simp cong add: conj_cong add: le_iff_plus_unchanged [symmetric])
- apply (blast intro!: psubsetI elim: equalityE)
- apply simp
- done
-
-recdef_tc iter_tc: iter (2)
- apply (simp add: same_fst_def pres_type_def)
- apply (clarify del: disjCI)
- apply (subgoal_tac "(@p. p:w) : w")
- prefer 2
- apply (fast intro: someI)
- apply (subgoal_tac "ss : list (size ss) A")
- prefer 2
- apply (blast intro!: listI)
- apply (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss")
- prefer 2
- apply (blast dest: boundedD)
- apply (rotate_tac 1)
- apply (simp del: listE_length
- add: decomp_propa finite_psubset_def inter_tc_lemma bounded_nat_set_is_finite)
- done
-
-lemma iter_induct:
- "(!!A r f step succs ss w.
- (!p. p = (@ p. p : w) & w ~= {} & semilat(A,r,f) & acc r &
- (!p:w. p < length ss) & bounded succs (length ss) &
- set ss <= A & pres_type step (length ss) A
- --> P A r f step succs (merges f (step p (ss!p)) (succs p) ss)
- ({q. q:set(succs p) & step p (ss!p) +_f ss!q ~= ss!q} Un (w-{p})))
- ==> P A r f step succs ss w) ==> P A r f step succs ss w"
-proof -
- case antecedent
- show ?thesis
- apply (rule_tac P = P in iter_tc [THEN iter_wf [THEN iter.induct]])
- apply (rule antecedent)
- apply clarify
- apply simp
- apply (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss")
- apply (rotate_tac -1)
- apply (simp add: decomp_propa)
- apply (subgoal_tac "(@p. p:w) : w")
- apply (blast dest: boundedD)
- apply (fast intro: someI)
- done
-qed
-
-lemma iter_unfold:
- "[| semilat(A,r,f); acc r; set ss <= A; pres_type step (length ss) A;
- bounded succs (size ss); !p:w. p<size ss |] ==>
- iter(((A,r,f),step,succs),ss,w) =
- (if w={} then ss
- else let p = SOME p. p : w
- in iter(((A,r,f),step,succs),merges f (step p (ss!p)) (succs p) ss,
- {q. q:set(succs p) & step p (ss!p) +_f ss!q ~= ss!q} Un (w-{p})))"
- apply (rule iter_tc [THEN iter_wf [THEN iter.simps [THEN trans]]])
- apply simp
- apply (rule impI)
- apply (subst decomp_propa)
- apply (subgoal_tac "(@p. p:w) : w")
- apply (blast dest: boundedD)
- apply (fast intro: someI)
- apply simp
- done
-
lemma stable_pres_lemma:
"[| semilat (A,r,f); pres_type step n A; bounded succs n;
ss : list n A; p : w; ! q:w. q < n;
@@ -339,67 +249,109 @@
dest: pres_typeD boundedD)
done
+(*
ML_setup {*
Unify.trace_bound := 80;
Unify.search_bound := 90;
*}
+*)
-lemma iter_properties [rule_format]:
- "semilat(A,r,f) & acc r & pres_type step n A & mono r step n A &
- bounded succs n & (! p:w. p < n) & ss:list n A &
- (!p<n. p~:w --> stable r step succs ss p)
- --> iter(((A,r,f),step,succs),ss,w) : list n A &
- stables r step succs (iter(((A,r,f),step,succs),ss,w)) &
- ss <=[r] iter(((A,r,f),step,succs),ss,w) &
- (! ts:list n A.
- ss <=[r] ts & stables r step succs ts -->
- iter(((A,r,f),step,succs),ss,w) <=[r] ts)"
- apply (unfold stables_def)
- apply (rule_tac A = A and r = r and f = f and step = step and ss = ss and w = w in iter_induct)
- apply clarify
- apply (frule listE_length)
- apply hypsubst
- apply (subst iter_unfold)
- apply assumption
- apply assumption
- apply (simp (no_asm_simp))
- apply assumption
- apply assumption
- apply assumption
- apply (simp (no_asm_simp) del: listE_length)
+lemma termination_lemma:
+ "[| semilat(A,r,f); ss : list n A; t:A; ! q:set qs. q < n; p:w |] ==>
+ ss <[r] merges f t qs ss |
+ merges f t qs ss = ss & {q. q:set qs & t +_f ss!q ~= ss!q} Un (w-{p}) < w"
+ apply (unfold lesssub_def)
+ apply (simp (no_asm_simp) add: merges_incr)
apply (rule impI)
- apply (erule allE)
- apply (erule impE)
- apply (simp (no_asm_simp) del: listE_length)
- apply (subgoal_tac "(@p. p:w) : w")
- prefer 2
- apply (fast intro: someI)
- apply (subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A")
- prefer 2
- apply (blast intro: pres_typeD listE_nth_in)
- apply (erule impE)
- apply (simp (no_asm_simp) del: listE_length le_iff_plus_unchanged [symmetric])
- apply (rule conjI)
- apply (blast dest: boundedD)
- apply (rule conjI)
- apply (blast intro: merges_preserves_type dest: boundedD)
- apply clarify
- apply (blast intro!: stable_pres_lemma)
- apply (simp (no_asm_simp) del: listE_length)
- apply (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss")
- prefer 2
- apply (blast dest: boundedD)
- apply (subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A")
- prefer 2
- apply (blast intro: pres_typeD)
- apply (rule conjI)
- apply (blast intro!: merges_incr intro: le_list_trans)
- apply clarify
- apply (drule bspec, assumption, erule mp)
- apply (simp del: listE_length)
- apply (blast intro: merges_bounded_lemma)
+ apply (rule merges_same_conv [THEN iffD1, elim_format])
+ apply assumption+
+ defer
+ apply (rule sym, assumption)
+ apply (simp cong add: conj_cong add: le_iff_plus_unchanged [symmetric])
+ apply (blast intro!: psubsetI elim: equalityE)
+ apply simp
done
+lemma while_properties:
+ "\<lbrakk> semilat(A,r,f); acc r ; pres_type step n A; mono r step n A;
+ bounded succs n; \<forall>p\<in>w0. p < n; ss0 \<in> list n A;
+ \<forall>p<n. p \<notin> w0 \<longrightarrow> stable r step succs ss0 p \<rbrakk> \<Longrightarrow>
+ ss' = fst(while (%(ss,w). w \<noteq> {})
+ (%(ss,w). let p = SOME p. p \<in> w
+ in propa f (succs p) (step p (ss!p)) ss (w-{p})) (ss0,w0))
+ \<longrightarrow>
+ ss' \<in> list n A \<and> stables r step succs ss' \<and> ss0 <=[r] ss' \<and>
+ (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step succs ts \<longrightarrow> ss' <=[r] ts)"
+apply (unfold stables_def)
+apply (rule_tac P = "%(ss,w).
+ ss \<in> list n A \<and> (\<forall>p<n. p \<notin> w \<longrightarrow> stable r step succs ss p) \<and> ss0 <=[r] ss \<and>
+ (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step succs 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)
+
+(* Invariant holds initially: *)
+apply (simp add:stables_def)
+(* Invariant is preserved: *)
+apply(simp add: stables_def split_paired_all)
+apply(rename_tac ss w)
+apply(subgoal_tac "(SOME p. p \<in> w) \<in> w")
+ prefer 2; apply (fast intro: someI)
+apply(subgoal_tac "step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w)) \<in> A")
+ prefer 2; apply (blast intro: pres_typeD listE_nth_in dest: boundedD);
+ apply (subgoal_tac "\<forall>q\<in>set(succs (SOME p. p \<in> w)). q < size ss")
+ prefer 2; apply(clarsimp, blast dest!: boundedD)
+apply (subst decomp_propa)
+ apply blast
+apply simp
+apply (rule conjI)
+ apply (blast intro: merges_preserves_type dest: boundedD);
+apply (rule conjI)
+ apply (blast intro!: stable_pres_lemma)
+apply (rule conjI)
+ apply (blast intro!: merges_incr intro: le_list_trans)
+apply (rule conjI)
+ apply clarsimp
+ apply (best intro!: merges_bounded_lemma)
+apply (blast dest!: boundedD)
+
+(* Postcondition holds upon termination: *)
+apply(clarsimp simp add: stables_def split_paired_all)
+
+(* Well-foundedness of the termination relation: *)
+apply (rule wf_lex_prod)
+ apply (drule (1) semilatDorderI [THEN acc_le_listI])
+ apply (simp only: acc_def lesssub_def)
+apply (rule wf_finite_psubset)
+
+(* Loop decreases along termination relation: *)
+apply(simp add: stables_def split_paired_all)
+apply(rename_tac ss w)
+apply(subgoal_tac "(SOME p. p \<in> w) \<in> w")
+ prefer 2; apply (fast intro: someI)
+apply(subgoal_tac "step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w)) \<in> A")
+ prefer 2; apply (blast intro: pres_typeD listE_nth_in dest: boundedD);
+ apply (subgoal_tac "\<forall>q\<in>set(succs (SOME p. p \<in> w)). q < n")
+ prefer 2; apply(clarsimp, blast dest!: boundedD)
+apply (subst decomp_propa)
+ apply clarsimp
+apply clarify
+apply (simp del: listE_length
+ add: lex_prod_def finite_psubset_def decomp_propa termination_lemma
+ bounded_nat_set_is_finite)
+done
+
+lemma iter_properties:
+ "\<lbrakk> semilat(A,r,f); acc r ; pres_type step n A; mono r step n A;
+ bounded succs n; \<forall>p\<in>w0. p < n; ss0 \<in> list n A;
+ \<forall>p<n. p \<notin> w0 \<longrightarrow> stable r step succs ss0 p \<rbrakk> \<Longrightarrow>
+ iter (A,r,f) step succs ss0 w0 : list n A \<and>
+ stables r step succs (iter (A,r,f) step succs ss0 w0) \<and>
+ ss0 <=[r] iter (A,r,f) step succs ss0 w0 \<and>
+ (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step succs ts \<longrightarrow>
+ iter (A,r,f) step succs ss0 w0 <=[r] ts)"
+apply(simp add:iter_def listE_set del:Let_def)
+by(rule while_properties[THEN mp,OF _ _ _ _ _ _ _ _ refl])
lemma is_dfa_kildall:
"[| semilat(A,r,f); acc r; pres_type step n A;
@@ -409,7 +361,7 @@
apply clarify
apply simp
apply (rule iter_properties)
- apply (simp add: unstables_def stable_def)
+ apply (simp_all add: unstables_def stable_def)
apply (blast intro!: le_iff_plus_unchanged [THEN iffD2] listE_nth_in
dest: boundedD pres_typeD)
done