# HG changeset patch
# User nipkow
# Date 990009085 -7200
# Node ID 1d3d110c456e124cdc161b22f2d6b3b9de6bdc6d
# Parent  acd83fa66e92b1acbd6ea69b9aa9c106368aaad9
welltyping -> wt_step

diff -r acd83fa66e92 -r 1d3d110c456e src/HOL/MicroJava/BV/JVM.thy
--- a/src/HOL/MicroJava/BV/JVM.thy	Mon May 14 09:58:22 2001 +0200
+++ b/src/HOL/MicroJava/BV/JVM.thy	Wed May 16 12:31:25 2001 +0200
@@ -208,13 +208,13 @@
   have 
     "\<exists>ts\<in>list (length bs) (states G maxs maxr).
          ?start <=[JVMType.le G maxs maxr] ts \<and>
-         welltyping (JVMType.le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs ! pc) pc) ts"
+         wt_step (JVMType.le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs ! pc) pc) ts"
     by (unfold is_bcv_def) auto
 
   then obtain phi' where
     l: "phi' \<in> list (length bs) (states G maxs maxr)" and
     s: "?start <=[JVMType.le G maxs maxr] phi'" and
-    w: "welltyping (JVMType.le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs ! pc) pc) phi'"
+    w: "wt_step (JVMType.le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs ! pc) pc) phi'"
     by blast
    
   hence dynamic:
@@ -231,7 +231,7 @@
   
   with instrs w
   have "phi' ! 0 \<noteq> Err"
-    by (unfold welltyping_def) simp
+    by (unfold wt_step_def) simp
 
   with instrs l
   have phi0: "OK (map ok_val phi' ! 0) = phi' ! 0"
@@ -380,7 +380,7 @@
   qed         
 
   from dynamic
-  have "welltyping (le G maxs ?maxr) Err (exec G maxs rT bs) ?succs ?phi"
+  have "wt_step (le G maxs ?maxr) Err (exec G maxs rT bs) ?succs ?phi"
     by (simp add: dynamic_wt_def JVM_le_Err_conv)
   
   with start 1 2 is_bcv
diff -r acd83fa66e92 -r 1d3d110c456e src/HOL/MicroJava/BV/Kildall.thy
--- a/src/HOL/MicroJava/BV/Kildall.thy	Mon May 14 09:58:22 2001 +0200
+++ b/src/HOL/MicroJava/BV/Kildall.thy	Wed May 16 12:31:25 2001 +0200
@@ -349,7 +349,7 @@
       pres_type step n A; bounded succs n; 
       mono r step n A |]
   ==> is_bcv r T step succs n A (kildall r f step succs)"
-apply(unfold is_bcv_def welltyping_def)
+apply(unfold is_bcv_def wt_step_def)
 apply(insert kildall_properties[of A])
 apply(simp add:stables_def)
 apply clarify
diff -r acd83fa66e92 -r 1d3d110c456e src/HOL/MicroJava/BV/Typing_Framework.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework.thy	Mon May 14 09:58:22 2001 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework.thy	Wed May 16 12:31:25 2001 +0200
@@ -29,11 +29,11 @@
            => nat => 's set => ('s list => 's list) => bool"
 "is_bcv r T step succs n A bcv == !ss : list n A.
    (!p<n. (bcv ss)!p ~= T) =
-   (? ts: list n A. ss <=[r] ts & welltyping r T step succs ts)"
+   (? ts: list n A. ss <=[r] ts & wt_step r T step succs ts)"
 
- welltyping ::
+ wt_step ::
 "'s ord => 's => (nat => 's => 's) => (nat => nat list) => 's list => bool"
-"welltyping r T step succs ts ==
+"wt_step r T step succs ts ==
  !p<size(ts). ts!p ~= T & stable r step succs ts p"
 
 end
diff -r acd83fa66e92 -r 1d3d110c456e src/HOL/MicroJava/BV/Typing_Framework_err.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Mon May 14 09:58:22 2001 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Wed May 16 12:31:25 2001 +0200
@@ -13,7 +13,7 @@
 
 dynamic_wt :: "'s ord => (nat => 's err => 's err) => (nat => nat list) => 
                's err list => bool"
-"dynamic_wt r step succs ts == welltyping (Err.le r) Err step succs ts"
+"dynamic_wt r step succs ts == wt_step (Err.le r) Err step succs ts"
 
 static_wt :: "'s ord => (nat => 's => bool) => 
               (nat => 's => 's) => (nat => nat list) =>  's list => bool"
@@ -55,7 +55,7 @@
 
   from wt lp
   have [intro?]: "!!p. p < length ts ==> ts ! p ~= Err" 
-    by (unfold dynamic_wt_def welltyping_def) simp
+    by (unfold dynamic_wt_def wt_step_def) simp
 
   show app: "app p (map ok_val ts ! p)"
   proof -
@@ -67,7 +67,7 @@
     obtain s where
       OKp:  "ts ! p = OK s" and
       less: "err_step app step p (ts ! p) <=_(Err.le r) ts ! q"
-      by (unfold dynamic_wt_def welltyping_def stable_def) 
+      by (unfold dynamic_wt_def wt_step_def stable_def) 
          (auto iff: not_Err_eq)
 
     from lp b q
@@ -96,7 +96,7 @@
     obtain s where
       OKp:  "ts ! p = OK s" and
       less: "err_step app step p (ts ! p) <=_(Err.le r) ts ! q"
-      by (unfold dynamic_wt_def welltyping_def stable_def) 
+      by (unfold dynamic_wt_def wt_step_def stable_def) 
          (auto iff: not_Err_eq)
 
     from lp b q
@@ -117,7 +117,7 @@
 lemma static_imp_dynamic:
   "[| static_wt r app step succs ts; bounded succs (size ts) |] 
   ==> dynamic_wt r (err_step app step) succs (map OK ts)"
-proof (unfold dynamic_wt_def welltyping_def, intro strip, rule conjI)
+proof (unfold dynamic_wt_def wt_step_def, intro strip, rule conjI)
   assume bounded: "bounded succs (size ts)"
   assume static:  "static_wt r app step succs ts"
   fix p assume "p < length (map OK ts)"