1.1 --- a/src/HOL/MicroJava/BV/Kildall.thy	Mon Feb 26 16:36:53 2001 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/Kildall.thy	Tue Feb 27 12:28:42 2001 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4   !s p t. s : A & p < n & s <=_r t --> step p s <=_r step p t"
     1.5  
     1.6  consts
     1.7 - iter :: "'s sl \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> 's) \<Rightarrow> (nat \<Rightarrow> nat list) \<Rightarrow>
     1.8 + iter :: "'s binop \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> 's) \<Rightarrow> (nat \<Rightarrow> nat list) \<Rightarrow>
     1.9            's list \<Rightarrow> nat set \<Rightarrow> 's list"
    1.10   propa :: "'s binop => nat list => 's => 's list => nat set => 's list * nat set"
    1.11  
    1.12 @@ -30,12 +30,10 @@
    1.13                            in propa f qs t (ss[q := u]) w')"
    1.14  
    1.15  defs iter_def:
    1.16 -"\<lbrakk> semilat Arf; acc(fst(snd Arf)); !p:w. p < size ss; bounded succs (size ss);
    1.17 -   set ss <= fst Arf; pres_type step (size ss) (fst Arf) \<rbrakk> \<Longrightarrow>
    1.18 - iter Arf step succs ss w ==
    1.19 +"iter f step succs ss w ==
    1.20   fst(while (%(ss,w). w \<noteq> {})
    1.21             (%(ss,w). let p = SOME p. p : w
    1.22 -                     in propa (snd(snd Arf)) (succs p) (step p (ss!p)) ss (w-{p}))
    1.23 +                     in propa f (succs p) (step p (ss!p)) ss (w-{p}))
    1.24             (ss,w))"
    1.25  
    1.26  constdefs
    1.27 @@ -44,10 +42,9 @@
    1.28  "unstables f step succs ss ==
    1.29   {p. p < size ss & (? q:set(succs p). step p (ss!p) +_f ss!q ~= ss!q)}"
    1.30  
    1.31 - kildall :: "'s sl => (nat => 's => 's) => (nat => nat list)
    1.32 + kildall :: "'s binop => (nat => 's => 's) => (nat => nat list)
    1.33               => 's list => 's list"
    1.34 -"kildall Arf step succs ss ==
    1.35 - iter Arf step succs ss (unstables (snd(snd Arf)) step succs ss)"
    1.36 +"kildall f step succs ss == iter f step succs ss (unstables f step succs ss)"
    1.37  
    1.38  consts merges :: "'s binop => 's => nat list => 's list => 's list"
    1.39  primrec
    1.40 @@ -249,13 +246,6 @@
    1.41                 dest: pres_typeD boundedD)
    1.42    done
    1.43  
    1.44 -(*
    1.45 -ML_setup {*
    1.46 -Unify.trace_bound := 80;
    1.47 -Unify.search_bound := 90;
    1.48 -*}
    1.49 -*)
    1.50 -
    1.51  lemma termination_lemma:  
    1.52    "[| semilat(A,r,f); ss : list n A; t:A; ! q:set qs. q < n; p:w |] ==> 
    1.53        ss <[r] merges f t qs ss | 
    1.54 @@ -345,21 +335,20 @@
    1.55    "\<lbrakk> semilat(A,r,f); acc r ; pres_type step n A; mono r step n A;
    1.56       bounded succs n; \<forall>p\<in>w0. p < n; ss0 \<in> list n A;
    1.57       \<forall>p<n. p \<notin> w0 \<longrightarrow> stable r step succs ss0 p \<rbrakk> \<Longrightarrow>
    1.58 -  iter (A,r,f) step succs ss0 w0 : list n A \<and>
    1.59 -  stables r step succs (iter (A,r,f) step succs ss0 w0) \<and>
    1.60 -  ss0 <=[r] iter (A,r,f) step succs ss0 w0 \<and>
    1.61 +  iter f step succs ss0 w0 : list n A \<and>
    1.62 +  stables r step succs (iter f step succs ss0 w0) \<and>
    1.63 +  ss0 <=[r] iter f step succs ss0 w0 \<and>
    1.64    (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step succs ts \<longrightarrow>
    1.65 -                 iter (A,r,f) step succs ss0 w0 <=[r] ts)"
    1.66 -apply(simp add:iter_def listE_set del:Let_def)
    1.67 +                 iter f step succs ss0 w0 <=[r] ts)"
    1.68 +apply(simp add:iter_def del:Let_def)
    1.69  by(rule while_properties[THEN mp,OF _ _ _ _ _ _ _ _ refl])
    1.70  
    1.71  lemma is_dfa_kildall:
    1.72    "[| semilat(A,r,f); acc r; pres_type step n A; 
    1.73       mono r step n A; bounded succs n|] 
    1.74 -  ==> is_dfa r (kildall (A,r,f) step succs) step succs n A"
    1.75 +  ==> is_dfa r (kildall f step succs) step succs n A"
    1.76    apply (unfold is_dfa_def kildall_def)
    1.77    apply clarify
    1.78 -  apply simp
    1.79    apply (rule iter_properties)
    1.80    apply (simp_all add: unstables_def stable_def)
    1.81    apply (blast intro!: le_iff_plus_unchanged [THEN iffD2] listE_nth_in
    1.82 @@ -370,7 +359,7 @@
    1.83    "[| semilat(A,r,f); acc r; top r T; 
    1.84        pres_type step n A; bounded succs n; 
    1.85        mono r step n A |]
    1.86 -  ==> is_bcv r T step succs n A (kildall (A,r,f) step succs)"
    1.87 +  ==> is_bcv r T step succs n A (kildall f step succs)"
    1.88    apply (intro is_bcv_dfa is_dfa_kildall semilatDorderI)
    1.89    apply assumption+
    1.90    done