# HG changeset patch
# User nipkow
# Date 982833521 -3600
# Node ID 56ab6a5ba351301a5e5d4b906dd1461e8ccc17da
# Parent  96a533d300a60a1fd3cf9cdd160aaee0eb09353e
recoded function iter with the help of the while-combinator.

diff -r 96a533d300a6 -r 56ab6a5ba351 src/HOL/MicroJava/BV/Kildall.thy
--- 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
diff -r 96a533d300a6 -r 56ab6a5ba351 src/HOL/MicroJava/BV/Semilat.thy
--- a/src/HOL/MicroJava/BV/Semilat.thy	Wed Feb 21 15:21:15 2001 +0100
+++ b/src/HOL/MicroJava/BV/Semilat.thy	Thu Feb 22 10:18:41 2001 +0100
@@ -195,8 +195,7 @@
 apply (case_tac "(y,x) : r^*")
  apply (case_tac "(y,x') : r^*")
   apply blast
- apply (blast intro: r_into_rtrancl elim: converse_rtranclE
-               dest: single_valuedD)
+ apply (blast elim: converse_rtranclE dest: single_valuedD)
 apply (rule exI)
 apply (rule conjI)
  apply (blast intro: rtrancl_into_rtrancl2 dest: single_valuedD)