# HG changeset patch
# User nipkow
# Date 983273322 -3600
# Node ID 10a307328d2ca97732dece8f6788682b7a994959
# Parent  0476c6e07bca395f43caa9e88797649957f87123
kildall now via while and therefore executable!

diff -r 0476c6e07bca -r 10a307328d2c src/HOL/MicroJava/BV/Kildall.thy
--- a/src/HOL/MicroJava/BV/Kildall.thy	Mon Feb 26 16:36:53 2001 +0100
+++ b/src/HOL/MicroJava/BV/Kildall.thy	Tue Feb 27 12:28:42 2001 +0100
@@ -19,7 +19,7 @@
  !s p t. s : A & p < n & s <=_r t --> step p s <=_r step p t"
 
 consts
- iter :: "'s sl \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> 's) \<Rightarrow> (nat \<Rightarrow> nat list) \<Rightarrow>
+ iter :: "'s binop \<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"
 
@@ -30,12 +30,10 @@
                           in propa f qs t (ss[q := u]) w')"
 
 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 ==
+"iter f 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}))
+                     in propa f (succs p) (step p (ss!p)) ss (w-{p}))
            (ss,w))"
 
 constdefs
@@ -44,10 +42,9 @@
 "unstables f step succs ss ==
  {p. p < size ss & (? q:set(succs p). step p (ss!p) +_f ss!q ~= ss!q)}"
 
- kildall :: "'s sl => (nat => 's => 's) => (nat => nat list)
+ kildall :: "'s binop => (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)"
+"kildall f step succs ss == iter f step succs ss (unstables f step succs ss)"
 
 consts merges :: "'s binop => 's => nat list => 's list => 's list"
 primrec
@@ -249,13 +246,6 @@
                dest: pres_typeD boundedD)
   done
 
-(*
-ML_setup {*
-Unify.trace_bound := 80;
-Unify.search_bound := 90;
-*}
-*)
-
 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 | 
@@ -345,21 +335,20 @@
   "\<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>
+  iter f step succs ss0 w0 : list n A \<and>
+  stables r step succs (iter f step succs ss0 w0) \<and>
+  ss0 <=[r] iter 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)
+                 iter f step succs ss0 w0 <=[r] ts)"
+apply(simp add:iter_def 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; 
      mono r step n A; bounded succs n|] 
-  ==> is_dfa r (kildall (A,r,f) step succs) step succs n A"
+  ==> is_dfa r (kildall f step succs) step succs n A"
   apply (unfold is_dfa_def kildall_def)
   apply clarify
-  apply simp
   apply (rule iter_properties)
   apply (simp_all add: unstables_def stable_def)
   apply (blast intro!: le_iff_plus_unchanged [THEN iffD2] listE_nth_in
@@ -370,7 +359,7 @@
   "[| semilat(A,r,f); acc r; top r T; 
       pres_type step n A; bounded succs n; 
       mono r step n A |]
-  ==> is_bcv r T step succs n A (kildall (A,r,f) step succs)"
+  ==> is_bcv r T step succs n A (kildall f step succs)"
   apply (intro is_bcv_dfa is_dfa_kildall semilatDorderI)
   apply assumption+
   done