--- 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
--- 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
--- 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
--- 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)"