--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Thu Sep 21 18:58:25 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Thu Sep 21 19:25:57 2000 +0200
@@ -7,11 +7,13 @@
programs.
*)
-header "Type Safety Proof"
+header "BV Type Safety Proof"
theory BVSpecTypeSafe = Correct:
-lemmas defs1 = sup_state_def correct_state_def correct_frame_def wt_instr_def step_def
+lemmas defs1 = sup_state_def correct_state_def correct_frame_def
+ wt_instr_def step_def
+
lemmas [simp del] = split_paired_All
lemma wt_jvm_prog_impl_wt_instr_cor:
@@ -25,17 +27,18 @@
lemma Load_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxl,ins);
- ins!pc = Load idx;
- wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
- Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
- G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+ method (G,C) sig = Some (C,rT,maxl,ins);
+ ins!pc = Load idx;
+ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
+ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons)
apply (rule conjI)
apply (rule approx_loc_imp_approx_val_sup)
apply simp+
-apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
+apply (blast intro: approx_stk_imp_approx_stk_sup
+ approx_loc_imp_approx_loc_sup)
done
lemma Store_correct:
@@ -49,7 +52,8 @@
apply (clarsimp simp add: defs1 map_eq_Cons)
apply (rule conjI)
apply (blast intro: approx_stk_imp_approx_stk_sup)
-apply (blast intro: approx_loc_imp_approx_loc_subst approx_loc_imp_approx_loc_sup)
+apply (blast intro: approx_loc_imp_approx_loc_subst
+ approx_loc_imp_approx_loc_sup)
done
@@ -60,14 +64,15 @@
lemma Bipush_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxl,ins);
- ins!pc = Bipush i;
- wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
- Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
- G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+ method (G,C) sig = Some (C,rT,maxl,ins);
+ ins!pc = Bipush i;
+ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
+ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 approx_val_def sup_PTS_eq map_eq_Cons)
-apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
+apply (blast intro: approx_stk_imp_approx_stk_sup
+ approx_loc_imp_approx_loc_sup)
done
lemma NT_subtype_conv:
@@ -87,21 +92,23 @@
lemma Aconst_null_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxl,ins);
- ins!pc = Aconst_null;
- wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
- Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
- G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+ method (G,C) sig = Some (C,rT,maxl,ins);
+ ins!pc = Aconst_null;
+ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
+ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons)
apply (rule conjI)
apply (force simp add: approx_val_Null NT_subtype_conv)
-apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
+apply (blast intro: approx_stk_imp_approx_stk_sup
+ approx_loc_imp_approx_loc_sup)
done
lemma Cast_conf2:
- "[|wf_prog ok G; G,h\<turnstile>v::\<preceq>RefT rt; cast_ok G C h v; G\<turnstile>Class C\<preceq>T; is_class G C|]
+ "[| wf_prog ok G; G,h\<turnstile>v::\<preceq>RefT rt; cast_ok G C h v;
+ G\<turnstile>Class C\<preceq>T; is_class G C|]
==> G,h\<turnstile>v::\<preceq>T"
apply (unfold cast_ok_def)
apply (frule widen_Class)
@@ -115,14 +122,15 @@
lemma Checkcast_correct:
"[| wf_prog wt G;
- method (G,C) sig = Some (C,rT,maxl,ins);
- ins!pc = Checkcast D;
- wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
- Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
- G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+ method (G,C) sig = Some (C,rT,maxl,ins);
+ ins!pc = Checkcast D;
+ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
+ Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
+ G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons raise_xcpt_def approx_val_def)
-apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup Cast_conf2)
+apply (blast intro: approx_stk_imp_approx_stk_sup
+ approx_loc_imp_approx_loc_sup Cast_conf2)
done
@@ -134,7 +142,8 @@
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs1 raise_xcpt_def map_eq_Cons approx_val_def split: option.split)
+apply (clarsimp simp add: defs1 raise_xcpt_def map_eq_Cons approx_val_def
+ split: option.split)
apply (frule conf_widen)
apply assumption+
apply (drule conf_RefTD)
@@ -143,7 +152,8 @@
apply (drule widen_cfs_fields)
apply assumption+
apply (force intro: conf_widen simp add: hconf_def oconf_def lconf_def)
-apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
+apply (blast intro: approx_stk_imp_approx_stk_sup
+ approx_loc_imp_approx_loc_sup)
done
lemma Putfield_correct:
@@ -162,11 +172,14 @@
apply assumption
apply (drule conf_RefTD)
apply clarsimp
-apply (blast intro: sup_heap_update_value approx_stk_imp_approx_stk_sup_heap
- approx_stk_imp_approx_stk_sup
- approx_loc_imp_approx_loc_sup_heap approx_loc_imp_approx_loc_sup
- hconf_imp_hconf_field_update
- correct_frames_imp_correct_frames_field_update conf_widen dest: widen_cfs_fields)
+apply (blast
+ intro:
+ sup_heap_update_value approx_stk_imp_approx_stk_sup_heap
+ approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup_heap
+ approx_loc_imp_approx_loc_sup hconf_imp_hconf_field_update
+ correct_frames_imp_correct_frames_field_update conf_widen
+ dest:
+ widen_cfs_fields)
done
lemma collapse_paired_All:
@@ -181,15 +194,18 @@
Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ;
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: NT_subtype_conv approx_val_def conf_def
- fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def defs1
+apply (clarsimp simp add: NT_subtype_conv approx_val_def conf_def defs1
+ fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def
split: option.split)
apply (force dest!: iffD1 [OF collapse_paired_All]
- intro: sup_heap_newref approx_stk_imp_approx_stk_sup_heap approx_stk_imp_approx_stk_sup
- approx_loc_imp_approx_loc_sup_heap approx_loc_imp_approx_loc_sup
- hconf_imp_hconf_newref correct_frames_imp_correct_frames_newref
- correct_init_obj simp add: NT_subtype_conv approx_val_def conf_def
- fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def defs1
+ intro: sup_heap_newref approx_stk_imp_approx_stk_sup_heap
+ approx_stk_imp_approx_stk_sup
+ approx_loc_imp_approx_loc_sup_heap
+ approx_loc_imp_approx_loc_sup
+ hconf_imp_hconf_newref correct_frames_imp_correct_frames_newref
+ correct_init_obj
+ simp add: NT_subtype_conv approx_val_def conf_def defs1
+ fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def
split: option.split)
done
@@ -366,7 +382,8 @@
by (simp add: wt_start_def sup_state_def)
have r: "approx_loc G hp (replicate mxl' arbitrary) (replicate mxl' Err)"
- by (simp add: approx_loc_def approx_val_Err list_all2_def set_replicate_conv_if)
+ by (simp add: approx_loc_def approx_val_Err
+ list_all2_def set_replicate_conv_if)
from wfprog mD
have "G \<turnstile> Class D \<preceq> Class D''"
@@ -463,7 +480,8 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1)
-apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
+apply (fast intro: approx_loc_imp_approx_loc_sup
+ approx_stk_imp_approx_stk_sup)
done
@@ -476,7 +494,8 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1)
-apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
+apply (fast intro: approx_loc_imp_approx_loc_sup
+ approx_stk_imp_approx_stk_sup)
done
lemma Pop_correct:
@@ -488,7 +507,8 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1)
-apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
+apply (fast intro: approx_loc_imp_approx_loc_sup
+ approx_stk_imp_approx_stk_sup)
done
lemma Dup_correct:
@@ -500,7 +520,9 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons)
-apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
+apply (force intro: approx_stk_imp_approx_stk_sup
+ approx_val_imp_approx_val_sup
+ approx_loc_imp_approx_loc_sup
simp add: defs1 map_eq_Cons)
done
@@ -513,7 +535,9 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons)
-apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
+apply (force intro: approx_stk_imp_approx_stk_sup
+ approx_val_imp_approx_val_sup
+ approx_loc_imp_approx_loc_sup
simp add: defs1 map_eq_Cons)
done
@@ -526,7 +550,9 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons)
-apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
+apply (force intro: approx_stk_imp_approx_stk_sup
+ approx_val_imp_approx_val_sup
+ approx_loc_imp_approx_loc_sup
simp add: defs1 map_eq_Cons)
done
@@ -539,7 +565,9 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons)
-apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
+apply (force intro: approx_stk_imp_approx_stk_sup
+ approx_val_imp_approx_val_sup
+ approx_loc_imp_approx_loc_sup
simp add: defs1 map_eq_Cons)
done
@@ -552,7 +580,9 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
==> G,phi \<turnstile>JVM state'\<surd>"
apply (clarsimp simp add: defs1 map_eq_Cons approx_val_def conf_def)
-apply (blast intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup)
+apply (blast intro: approx_stk_imp_approx_stk_sup
+ approx_val_imp_approx_val_sup
+ approx_loc_imp_approx_loc_sup)
done
@@ -572,10 +602,11 @@
prefer 9
apply (blast intro: Return_correct)
apply (unfold wt_jvm_prog_def)
-apply (fast intro: Load_correct Store_correct Bipush_correct Aconst_null_correct
- Checkcast_correct Getfield_correct Putfield_correct New_correct
- Goto_correct Ifcmpeq_correct Pop_correct Dup_correct
- Dup_x1_correct Dup_x2_correct Swap_correct IAdd_correct)+
+apply (fast intro:
+ Load_correct Store_correct Bipush_correct Aconst_null_correct
+ Checkcast_correct Getfield_correct Putfield_correct New_correct
+ Goto_correct Ifcmpeq_correct Pop_correct Dup_correct
+ Dup_x1_correct Dup_x2_correct Swap_correct IAdd_correct)+
done
@@ -627,11 +658,14 @@
theorem BV_correct_initial:
-"[| wt_jvm_prog G phi; G \<turnstile> s0 -jvm-> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>|]
- ==> approx_stk G hp stk (fst (the (((phi C) sig) ! pc))) \<and> approx_loc G hp loc (snd (the (((phi C) sig) ! pc)))"
+"[| wt_jvm_prog G phi;
+ G \<turnstile> s0 -jvm-> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>|]
+==> approx_stk G hp stk (fst (the (((phi C) sig) ! pc))) \<and>
+ approx_loc G hp loc (snd (the (((phi C) sig) ! pc)))"
apply (drule BV_correct)
apply assumption+
-apply (simp add: correct_state_def correct_frame_def split_def split: option.splits)
+apply (simp add: correct_state_def correct_frame_def split_def
+ split: option.splits)
done
end
--- a/src/HOL/MicroJava/BV/Convert.thy Thu Sep 21 18:58:25 2000 +0200
+++ b/src/HOL/MicroJava/BV/Convert.thy Thu Sep 21 19:25:57 2000 +0200
@@ -40,11 +40,13 @@
(* lifts a relation to option with None as bottom element *)
lift_bottom :: "('a => 'b => bool) => ('a option => 'b option => bool)"
- "lift_bottom P a' a == case a' of
- None => True
- | Some t' => (case a of None => False | Some t => P t' t)"
+ "lift_bottom P a' a ==
+ case a' of
+ None => True
+ | Some t' => (case a of None => False | Some t => P t' t)"
- sup_ty_opt :: "['code prog,ty err,ty err] => bool" ("_ \<turnstile> _ <=o _" [71,71] 70)
+ sup_ty_opt :: "['code prog,ty err,ty err] => bool"
+ ("_ \<turnstile> _ <=o _" [71,71] 70)
"sup_ty_opt G == lift_top (\<lambda>t t'. G \<turnstile> t \<preceq> t')"
sup_loc :: "['code prog,locvars_type,locvars_type] => bool"
@@ -53,17 +55,22 @@
sup_state :: "['code prog,state_type,state_type] => bool"
("_ \<turnstile> _ <=s _" [71,71] 70)
- "G \<turnstile> s <=s s' == (G \<turnstile> map Ok (fst s) <=l map Ok (fst s')) \<and> G \<turnstile> snd s <=l snd s'"
+ "G \<turnstile> s <=s s' ==
+ (G \<turnstile> map Ok (fst s) <=l map Ok (fst s')) \<and> G \<turnstile> snd s <=l snd s'"
sup_state_opt :: "['code prog,state_type option,state_type option] => bool"
("_ \<turnstile> _ <=' _" [71,71] 70)
"sup_state_opt G == lift_bottom (\<lambda>t t'. G \<turnstile> t <=s t')"
syntax (HTML output)
- sup_ty_opt :: "['code prog,ty err,ty err] => bool" ("_ |- _ <=o _")
- sup_loc :: "['code prog,locvars_type,locvars_type] => bool" ("_ |- _ <=l _" [71,71] 70)
- sup_state :: "['code prog,state_type,state_type] => bool" ("_ |- _ <=s _" [71,71] 70)
- sup_state_opt :: "['code prog,state_type option,state_type option] => bool" ("_ |- _ <=' _" [71,71] 70)
+ sup_ty_opt :: "['code prog,ty err,ty err] => bool"
+ ("_ |- _ <=o _")
+ sup_loc :: "['code prog,locvars_type,locvars_type] => bool"
+ ("_ |- _ <=l _" [71,71] 70)
+ sup_state :: "['code prog,state_type,state_type] => bool"
+ ("_ |- _ <=s _" [71,71] 70)
+ sup_state_opt :: "['code prog,state_type option,state_type option] => bool"
+ ("_ |- _ <=' _" [71,71] 70)
lemma not_Err_eq [iff]:
@@ -80,7 +87,7 @@
by (simp add: lift_top_def split: err.splits)
lemma lift_top_trans [trans]:
- "[| !!x y z. [| P x y; P y z |] ==> P x z; lift_top P x y; lift_top P y z |]
+ "[| !!x y z. [| P x y; P y z |] ==> P x z; lift_top P x y; lift_top P y z |]
==> lift_top P x z"
proof -
assume [trans]: "!!x y z. [| P x y; P y z |] ==> P x z"
@@ -141,7 +148,8 @@
by (simp add: lift_bottom_def split: option.splits)
lemma lift_bottom_trans [trans]:
- "[| !!x y z. [| P x y; P y z |] ==> P x z; lift_bottom P x y; lift_bottom P y z |]
+ "[| !!x y z. [| P x y; P y z |] ==> P x z;
+ lift_bottom P x y; lift_bottom P y z |]
==> lift_bottom P x z"
proof -
assume [trans]: "!!x y z. [| P x y; P y z |] ==> P x z"
@@ -286,8 +294,8 @@
theorem all_nth_sup_loc:
- "\<forall>b. length a = length b --> (\<forall> n. n < length a --> (G \<turnstile> (a!n) <=o (b!n))) -->
- (G \<turnstile> a <=l b)" (is "?P a")
+ "\<forall>b. length a = length b --> (\<forall> n. n < length a --> (G \<turnstile> (a!n) <=o (b!n)))
+ --> (G \<turnstile> a <=l b)" (is "?P a")
proof (induct a)
show "?P []" by simp
--- a/src/HOL/MicroJava/BV/Correct.thy Thu Sep 21 18:58:25 2000 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy Thu Sep 21 19:25:57 2000 +0200
@@ -6,27 +6,29 @@
The invariant for the type safety proof.
*)
-header "Type Safety Invariant"
+header "BV Type Safety Invariant"
theory Correct = BVSpec:
constdefs
- approx_val :: "[jvm_prog,aheap,val,ty err] => bool"
-"approx_val G h v any == case any of Err => True | Ok T => G,h\<turnstile>v::\<preceq>T"
+ approx_val :: "[jvm_prog,aheap,val,ty err] => bool"
+ "approx_val G h v any == case any of Err => True | Ok T => G,h\<turnstile>v::\<preceq>T"
- approx_loc :: "[jvm_prog,aheap,val list,locvars_type] => bool"
-"approx_loc G hp loc LT == list_all2 (approx_val G hp) loc LT"
+ approx_loc :: "[jvm_prog,aheap,val list,locvars_type] => bool"
+ "approx_loc G hp loc LT == list_all2 (approx_val G hp) loc LT"
+
+ approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] => bool"
+ "approx_stk G hp stk ST == approx_loc G hp stk (map Ok ST)"
- approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] => bool"
-"approx_stk G hp stk ST == approx_loc G hp stk (map Ok ST)"
+ correct_frame :: "[jvm_prog,aheap,state_type,nat,bytecode] => frame => bool"
+ "correct_frame G hp == \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc).
+ approx_stk G hp stk ST \<and> approx_loc G hp loc LT \<and>
+ pc < length ins \<and> length loc=length(snd sig)+maxl+1"
- correct_frame :: "[jvm_prog,aheap,state_type,nat,bytecode] => frame => bool"
-"correct_frame G hp == \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc).
- approx_stk G hp stk ST \<and> approx_loc G hp loc LT \<and>
- pc < length ins \<and> length loc=length(snd sig)+maxl+1"
-
- correct_frame_opt :: "[jvm_prog,aheap,state_type option,nat,bytecode] => frame => bool"
-"correct_frame_opt G hp s == case s of None => \<lambda>maxl ins f. False | Some t => correct_frame G hp t"
+ correct_frame_opt :: "[jvm_prog,aheap,state_type option,nat,bytecode]
+ => frame => bool"
+ "correct_frame_opt G hp s ==
+ case s of None => \<lambda>maxl ins f. False | Some t => correct_frame G hp t"
consts
@@ -75,7 +77,7 @@
apply clarsimp
apply (drule newref_None 1) back
apply simp
-.
+done
lemma sup_heap_update_value:
"hp a = Some (C,od') ==> hp \<le>| hp (a \<mapsto> (C,od))"
@@ -93,14 +95,15 @@
by (auto intro: null simp add: approx_val_def)
lemma approx_val_imp_approx_val_assConvertible [rule_format]:
- "wf_prog wt G ==> approx_val G hp v (Ok T) --> G\<turnstile> T\<preceq>T' --> approx_val G hp v (Ok T')"
+ "wf_prog wt G ==> approx_val G hp v (Ok T) --> G\<turnstile> T\<preceq>T'
+ --> approx_val G hp v (Ok T')"
by (cases T) (auto intro: conf_widen simp add: approx_val_def)
lemma approx_val_imp_approx_val_sup_heap [rule_format]:
"approx_val G hp v at --> hp \<le>| hp' --> approx_val G hp' v at"
apply (simp add: approx_val_def split: err.split)
apply (blast intro: conf_hext)
-.
+done
lemma approx_val_imp_approx_val_heap_update:
"[|hp a = Some obj'; G,hp\<turnstile> v::\<preceq>T; obj_ty obj = obj_ty obj'|]
@@ -108,24 +111,28 @@
by (cases v, auto simp add: obj_ty_def conf_def)
lemma approx_val_imp_approx_val_sup [rule_format]:
- "wf_prog wt G ==> (approx_val G h v us) --> (G \<turnstile> us <=o us') --> (approx_val G h v us')"
+ "wf_prog wt G ==> (approx_val G h v us) --> (G \<turnstile> us <=o us')
+ --> (approx_val G h v us')"
apply (simp add: sup_PTS_eq approx_val_def split: err.split)
apply (blast intro: conf_widen)
-.
+done
lemma approx_loc_imp_approx_val_sup:
- "[|wf_prog wt G; approx_loc G hp loc LT; idx < length LT; v = loc!idx; G \<turnstile> LT!idx <=o at|]
+ "[| wf_prog wt G; approx_loc G hp loc LT; idx < length LT;
+ v = loc!idx; G \<turnstile> LT!idx <=o at |]
==> approx_val G hp v at"
apply (unfold approx_loc_def)
apply (unfold list_all2_def)
-apply (auto intro: approx_val_imp_approx_val_sup simp add: split_def all_set_conv_all_nth)
-.
+apply (auto intro: approx_val_imp_approx_val_sup
+ simp add: split_def all_set_conv_all_nth)
+done
(** approx_loc **)
lemma approx_loc_Cons [iff]:
- "approx_loc G hp (s#xs) (l#ls) = (approx_val G hp s l \<and> approx_loc G hp xs ls)"
+ "approx_loc G hp (s#xs) (l#ls) =
+ (approx_val G hp s l \<and> approx_loc G hp xs ls)"
by (simp add: approx_loc_def)
lemma assConv_approx_stk_imp_approx_loc [rule_format]:
@@ -136,25 +143,27 @@
apply (clarsimp simp add: all_set_conv_all_nth)
apply (rule approx_val_imp_approx_val_assConvertible)
apply auto
-.
+done
lemma approx_loc_imp_approx_loc_sup_heap [rule_format]:
- "\<forall>lvars. approx_loc G hp lvars lt --> hp \<le>| hp' --> approx_loc G hp' lvars lt"
+ "\<forall>lvars. approx_loc G hp lvars lt --> hp \<le>| hp'
+ --> approx_loc G hp' lvars lt"
apply (unfold approx_loc_def list_all2_def)
apply (cases lt)
apply simp
apply clarsimp
apply (rule approx_val_imp_approx_val_sup_heap)
apply auto
-.
+done
lemma approx_loc_imp_approx_loc_sup [rule_format]:
- "wf_prog wt G ==> approx_loc G hp lvars lt --> G \<turnstile> lt <=l lt' --> approx_loc G hp lvars lt'"
+ "wf_prog wt G ==> approx_loc G hp lvars lt --> G \<turnstile> lt <=l lt'
+ --> approx_loc G hp lvars lt'"
apply (unfold sup_loc_def approx_loc_def list_all2_def)
apply (auto simp add: all_set_conv_all_nth)
apply (auto elim: approx_val_imp_approx_val_sup)
-.
+done
lemma approx_loc_imp_approx_loc_subst [rule_format]:
@@ -162,18 +171,19 @@
--> (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))"
apply (unfold approx_loc_def list_all2_def)
apply (auto dest: subsetD [OF set_update_subset_insert] simp add: zip_update)
-.
+done
lemmas [cong] = conj_cong
lemma approx_loc_append [rule_format]:
"\<forall>L1 l2 L2. length l1=length L1 -->
- approx_loc G hp (l1@l2) (L1@L2) = (approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)"
+ approx_loc G hp (l1@l2) (L1@L2) =
+ (approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)"
apply (unfold approx_loc_def list_all2_def)
apply simp
apply blast
-.
+done
lemmas [cong del] = conj_cong
@@ -184,7 +194,7 @@
"approx_stk G hp (rev s) (rev t) = approx_stk G hp s t"
apply (unfold approx_stk_def approx_loc_def list_all2_def)
apply (auto simp add: zip_rev sym [OF rev_map])
-.
+done
lemma approx_stk_rev:
"approx_stk G hp (rev s) t = approx_stk G hp s (rev t)"
@@ -192,7 +202,8 @@
lemma approx_stk_imp_approx_stk_sup_heap [rule_format]:
- "\<forall>lvars. approx_stk G hp lvars lt --> hp \<le>| hp' --> approx_stk G hp' lvars lt"
+ "\<forall>lvars. approx_stk G hp lvars lt --> hp \<le>| hp'
+ --> approx_stk G hp' lvars lt"
by (auto intro: approx_loc_imp_approx_loc_sup_heap simp add: approx_stk_def)
lemma approx_stk_imp_approx_stk_sup [rule_format]:
@@ -229,7 +240,7 @@
apply (unfold oconf_def lconf_def)
apply (simp add: map_of_map)
apply (force intro: defval_conf dest: map_of_SomeD is_type_fields)
-.
+done
lemma oconf_imp_oconf_field_update [rule_format]:
@@ -243,7 +254,7 @@
apply (unfold oconf_def lconf_def)
apply simp
apply (fast intro: conf_hext sup_heap_newref)
-.
+done
lemma oconf_imp_oconf_heap_update [rule_format]:
@@ -252,7 +263,7 @@
apply (unfold oconf_def lconf_def)
apply simp
apply (force intro: approx_val_imp_approx_val_heap_update)
-.
+done
(** hconf **)
@@ -262,7 +273,7 @@
"hp x = None --> G\<turnstile>h hp\<surd> --> G,hp\<turnstile>obj\<surd> --> G\<turnstile>h hp(newref hp\<mapsto>obj)\<surd>"
apply (simp add: hconf_def)
apply (fast intro: oconf_imp_oconf_heap_newref)
-.
+done
lemma hconf_imp_hconf_field_update [rule_format]:
"map_of (fields (G, oT)) (F, D) = Some T \<and> hp oloc = Some(oT,fs) \<and>
@@ -270,7 +281,7 @@
apply (simp add: hconf_def)
apply (force intro: oconf_imp_oconf_heap_update oconf_imp_oconf_field_update
simp add: obj_ty_def)
-.
+done
(** correct_frames **)
@@ -297,7 +308,7 @@
apply simp
apply (rule sup_heap_update_value)
apply simp
-.
+done
lemma correct_frames_imp_correct_frames_newref [rule_format]:
"\<forall>rT C sig. hp x = None --> correct_frames G hp phi rT sig frs \<and> oconf G hp obj
@@ -318,7 +329,7 @@
apply simp
apply (rule sup_heap_newref)
apply simp
-.
+done
end
--- a/src/HOL/MicroJava/J/Eval.thy Thu Sep 21 18:58:25 2000 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy Thu Sep 21 19:25:57 2000 +0200
@@ -15,113 +15,115 @@
exec :: "java_mb prog => (xstate \\<times> stmt \\<times> xstate) set"
syntax
- eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "("_\\<turnstile>_ -_\\<succ>_-> _"[51,82,82,82,82]81)
+ eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
+ ("_\\<turnstile>_ -_\\<succ>_-> _"[51,82,82,82,82]81)
evals:: "[java_mb prog,xstate,expr list,
- val list,xstate] => bool "("_\\<turnstile>_ -_[\\<succ>]_-> _"[51,82,51,51,82]81)
- exec :: "[java_mb prog,xstate,stmt, xstate] => bool "("_\\<turnstile>_ -_-> _" [51,82,82, 82]81)
+ val list,xstate] => bool "
+ ("_\\<turnstile>_ -_[\\<succ>]_-> _"[51,82,51,51,82]81)
+ exec :: "[java_mb prog,xstate,stmt, xstate] => bool "
+ ("_\\<turnstile>_ -_-> _" [51,82,82, 82]81)
translations
"G\\<turnstile>s -e \\<succ> v-> (x,s')" <= "(s, e, v, x, s') \\<in> eval G"
- "G\\<turnstile>s -e \\<succ> v-> s' " == "(s, e, v, s' ) \\<in> eval G"
+ "G\\<turnstile>s -e \\<succ> v-> s' " == "(s, e, v, s') \\<in> eval G"
"G\\<turnstile>s -e[\\<succ>]v-> (x,s')" <= "(s, e, v, x, s') \\<in> evals G"
- "G\\<turnstile>s -e[\\<succ>]v-> s' " == "(s, e, v, s' ) \\<in> evals G"
- "G\\<turnstile>s -c -> (x,s')" <= "(s, c, x, s') \\<in> exec G"
- "G\\<turnstile>s -c -> s' " == "(s, c, s') \\<in> exec G"
+ "G\\<turnstile>s -e[\\<succ>]v-> s' " == "(s, e, v, s') \\<in> evals G"
+ "G\\<turnstile>s -c -> (x,s')" <= "(s, c, x, s') \\<in> exec G"
+ "G\\<turnstile>s -c -> s' " == "(s, c, s') \\<in> exec G"
inductive "eval G" "evals G" "exec G" intrs
(* evaluation of expressions *)
(* cf. 15.5 *)
- XcptE "G\\<turnstile>(Some xc,s) -e\\<succ>arbitrary-> (Some xc,s)"
+ XcptE "G\\<turnstile>(Some xc,s) -e\\<succ>arbitrary-> (Some xc,s)"
(* cf. 15.8.1 *)
- NewC "[|h = heap s; (a,x) = new_Addr h;
- h'= h(a\\<mapsto>(C,init_vars (fields (G,C))))|] ==>
- G\\<turnstile>Norm s -NewC C\\<succ>Addr a-> c_hupd h' (x,s)"
+ NewC "[| h = heap s; (a,x) = new_Addr h;
+ h'= h(a\\<mapsto>(C,init_vars (fields (G,C)))) |] ==>
+ G\\<turnstile>Norm s -NewC C\\<succ>Addr a-> c_hupd h' (x,s)"
(* cf. 15.15 *)
- Cast "[|G\\<turnstile>Norm s0 -e\\<succ>v-> (x1,s1);
- x2=raise_if (\\<not> cast_ok G C (heap s1) v) ClassCast x1|] ==>
- G\\<turnstile>Norm s0 -Cast C e\\<succ>v-> (x2,s1)"
+ Cast "[| G\\<turnstile>Norm s0 -e\\<succ>v-> (x1,s1);
+ x2 = raise_if (\\<not> cast_ok G C (heap s1) v) ClassCast x1 |] ==>
+ G\\<turnstile>Norm s0 -Cast C e\\<succ>v-> (x2,s1)"
(* cf. 15.7.1 *)
- Lit "G\\<turnstile>Norm s -Lit v\\<succ>v-> Norm s"
+ Lit "G\\<turnstile>Norm s -Lit v\\<succ>v-> Norm s"
- BinOp "[|G\\<turnstile>Norm s -e1\\<succ>v1-> s1;
- G\\<turnstile>s1 -e2\\<succ>v2-> s2;
- v = (case bop of Eq => Bool (v1 = v2)
- | Add => Intg (the_Intg v1 + the_Intg v2))|] ==>
- G\\<turnstile>Norm s -BinOp bop e1 e2\\<succ>v-> s2"
+ BinOp "[| G\\<turnstile>Norm s -e1\\<succ>v1-> s1;
+ G\\<turnstile>s1 -e2\\<succ>v2-> s2;
+ v = (case bop of Eq => Bool (v1 = v2)
+ | Add => Intg (the_Intg v1 + the_Intg v2)) |] ==>
+ G\\<turnstile>Norm s -BinOp bop e1 e2\\<succ>v-> s2"
(* cf. 15.13.1, 15.2 *)
- LAcc "G\\<turnstile>Norm s -LAcc v\\<succ>the (locals s v)-> Norm s"
+ LAcc "G\\<turnstile>Norm s -LAcc v\\<succ>the (locals s v)-> Norm s"
(* cf. 15.25.1 *)
- LAss "[|G\\<turnstile>Norm s -e\\<succ>v-> (x,(h,l));
- l' = (if x = None then l(va\\<mapsto>v) else l)|] ==>
- G\\<turnstile>Norm s -va::=e\\<succ>v-> (x,(h,l'))"
+ LAss "[| G\\<turnstile>Norm s -e\\<succ>v-> (x,(h,l));
+ l' = (if x = None then l(va\\<mapsto>v) else l) |] ==>
+ G\\<turnstile>Norm s -va::=e\\<succ>v-> (x,(h,l'))"
(* cf. 15.10.1, 15.2 *)
- FAcc "[|G\\<turnstile>Norm s0 -e\\<succ>a'-> (x1,s1);
- v = the (snd (the (heap s1 (the_Addr a'))) (fn,T))|] ==>
- G\\<turnstile>Norm s0 -{T}e..fn\\<succ>v-> (np a' x1,s1)"
+ FAcc "[| G\\<turnstile>Norm s0 -e\\<succ>a'-> (x1,s1);
+ v = the (snd (the (heap s1 (the_Addr a'))) (fn,T)) |] ==>
+ G\\<turnstile>Norm s0 -{T}e..fn\\<succ>v-> (np a' x1,s1)"
(* cf. 15.25.1 *)
- FAss "[|G\\<turnstile> Norm s0 -e1\\<succ>a'-> (x1,s1); a = the_Addr a';
- G\\<turnstile>(np a' x1,s1) -e2\\<succ>v -> (x2,s2);
- h = heap s2; (c,fs) = the (h a);
- h' = h(a\\<mapsto>(c,(fs((fn,T)\\<mapsto>v))))|] ==>
- G\\<turnstile>Norm s0 -{T}e1..fn:=e2\\<succ>v-> c_hupd h' (x2,s2)"
+ FAss "[| G\\<turnstile> Norm s0 -e1\\<succ>a'-> (x1,s1); a = the_Addr a';
+ G\\<turnstile>(np a' x1,s1) -e2\\<succ>v -> (x2,s2);
+ h = heap s2; (c,fs) = the (h a);
+ h' = h(a\\<mapsto>(c,(fs((fn,T)\\<mapsto>v)))) |] ==>
+ G\\<turnstile>Norm s0 -{T}e1..fn:=e2\\<succ>v-> c_hupd h' (x2,s2)"
(* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
- Call "[|G\\<turnstile>Norm s0 -e\\<succ>a'-> s1; a = the_Addr a';
- G\\<turnstile>s1 -ps[\\<succ>]pvs-> (x,(h,l)); dynT = fst (the (h a));
- (md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs));
- G\\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\\<mapsto>]pvs)(This\\<mapsto>a'))) -blk-> s3;
- G\\<turnstile> s3 -res\\<succ>v -> (x4,s4)|] ==>
- G\\<turnstile>Norm s0 -e..mn({pTs}ps)\\<succ>v-> (x4,(heap s4,l))"
+ Call "[| G\\<turnstile>Norm s0 -e\\<succ>a'-> s1; a = the_Addr a';
+ G\\<turnstile>s1 -ps[\\<succ>]pvs-> (x,(h,l)); dynT = fst (the (h a));
+ (md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs));
+ G\\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\\<mapsto>]pvs)(This\\<mapsto>a'))) -blk-> s3;
+ G\\<turnstile> s3 -res\\<succ>v -> (x4,s4) |] ==>
+ G\\<turnstile>Norm s0 -e..mn({pTs}ps)\\<succ>v-> (x4,(heap s4,l))"
(* evaluation of expression lists *)
(* cf. 15.5 *)
- XcptEs "G\\<turnstile>(Some xc,s) -e[\\<succ>]arbitrary-> (Some xc,s)"
+ XcptEs "G\\<turnstile>(Some xc,s) -e[\\<succ>]arbitrary-> (Some xc,s)"
(* cf. 15.11.??? *)
- Nil
- "G\\<turnstile>Norm s0 -[][\\<succ>][]-> Norm s0"
+ Nil "G\\<turnstile>Norm s0 -[][\\<succ>][]-> Norm s0"
(* cf. 15.6.4 *)
- Cons "[|G\\<turnstile>Norm s0 -e \\<succ> v -> s1;
- G\\<turnstile> s1 -es[\\<succ>]vs-> s2|] ==>
- G\\<turnstile>Norm s0 -e#es[\\<succ>]v#vs-> s2"
+ Cons "[| G\\<turnstile>Norm s0 -e \\<succ> v -> s1;
+ G\\<turnstile> s1 -es[\\<succ>]vs-> s2 |] ==>
+ G\\<turnstile>Norm s0 -e#es[\\<succ>]v#vs-> s2"
(* execution of statements *)
(* cf. 14.1 *)
- XcptS "G\\<turnstile>(Some xc,s) -s0-> (Some xc,s)"
+ XcptS "G\\<turnstile>(Some xc,s) -s0-> (Some xc,s)"
(* cf. 14.5 *)
- Skip "G\\<turnstile>Norm s -Skip-> Norm s"
+ Skip "G\\<turnstile>Norm s -Skip-> Norm s"
(* cf. 14.7 *)
- Expr "[|G\\<turnstile>Norm s0 -e\\<succ>v-> s1|] ==>
- G\\<turnstile>Norm s0 -Expr e-> s1"
+ Expr "[| G\\<turnstile>Norm s0 -e\\<succ>v-> s1 |] ==>
+ G\\<turnstile>Norm s0 -Expr e-> s1"
(* cf. 14.2 *)
- Comp "[|G\\<turnstile>Norm s0 -s -> s1;
- G\\<turnstile> s1 -t -> s2|] ==>
- G\\<turnstile>Norm s0 -(s;; t)-> s2"
+ Comp "[| G\\<turnstile>Norm s0 -s -> s1;
+ G\\<turnstile> s1 -t -> s2|] ==>
+ G\\<turnstile>Norm s0 -(s;; t)-> s2"
(* cf. 14.8.2 *)
- Cond "[|G\\<turnstile>Norm s0 -e \\<succ>v-> s1;
- G\\<turnstile> s1 -(if the_Bool v then s else t)-> s2|] ==>
- G\\<turnstile>Norm s0 -(If(e) s Else t)-> s2"
+ Cond "[| G\\<turnstile>Norm s0 -e \\<succ>v-> s1;
+ G\\<turnstile> s1 -(if the_Bool v then s else t)-> s2|] ==>
+ G\\<turnstile>Norm s0 -(If(e) s Else t)-> s2"
(* cf. 14.10, 14.10.1 *)
- Loop "[|G\\<turnstile>Norm s0 -(If(e) (s;; While(e) s) Else Skip)-> s1|] ==>
- G\\<turnstile>Norm s0 -(While(e) s)-> s1"
+ Loop "[| G\\<turnstile>Norm s0 -(If(e) (s;; While(e) s) Else Skip)-> s1 |] ==>
+ G\\<turnstile>Norm s0 -(While(e) s)-> s1"
end
--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy Thu Sep 21 18:58:25 2000 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy Thu Sep 21 19:25:57 2000 +0200
@@ -9,7 +9,8 @@
JVMExecInstr = JVMInstructions + JVMState +
consts
-exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, cname, sig, p_count, frame list] => jvm_state"
+ exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars,
+ cname, sig, p_count, frame list] => jvm_state"
primrec
"exec_instr (Load idx) G hp stk vars Cl sig pc frs =
(None, hp, ((vars ! idx) # stk, vars, Cl, sig, pc+1)#frs)"
@@ -63,9 +64,9 @@
xp' = raise_xcpt (oref=Null) NullPointer;
dynT = fst(the(hp(the_Addr oref)));
(dc,mh,mxl,c)= the (method (G,dynT) (mn,ps));
- frs' = if xp'=None
- then [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)]
- else []
+ frs' = if xp'=None then
+ [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)]
+ else []
in
(xp', hp, frs'@(drop (n+1) stk, vars, Cl, sig, pc+1)#frs))"
@@ -84,11 +85,13 @@
(None, hp, (hd stk # stk, vars, Cl, sig, pc+1)#frs)"
"exec_instr Dup_x1 G hp stk vars Cl sig pc frs =
- (None, hp, (hd stk # hd (tl stk) # hd stk # (tl (tl stk)), vars, Cl, sig, pc+1)#frs)"
+ (None, hp, (hd stk # hd (tl stk) # hd stk # (tl (tl stk)),
+ vars, Cl, sig, pc+1)#frs)"
"exec_instr Dup_x2 G hp stk vars Cl sig pc frs =
- (None, hp, (hd stk # hd (tl stk) # (hd (tl (tl stk))) # hd stk # (tl (tl (tl stk))),
- vars, Cl, sig, pc+1)#frs)"
+ (None, hp,
+ (hd stk # hd (tl stk) # (hd (tl (tl stk))) # hd stk # (tl (tl (tl stk))),
+ vars, Cl, sig, pc+1)#frs)"
"exec_instr Swap G hp stk vars Cl sig pc frs =
(let (val1,val2) = (hd stk,hd (tl stk))
@@ -98,7 +101,8 @@
"exec_instr IAdd G hp stk vars Cl sig pc frs =
(let (val1,val2) = (hd stk,hd (tl stk))
in
- (None, hp, (Intg ((the_Intg val1)+(the_Intg val2))#(tl (tl stk)), vars, Cl, sig, pc+1)#frs))"
+ (None, hp, (Intg ((the_Intg val1)+(the_Intg val2))#(tl (tl stk)),
+ vars, Cl, sig, pc+1)#frs))"
"exec_instr (Ifcmpeq i) G hp stk vars Cl sig pc frs =
(let (val1,val2) = (hd stk, hd (tl stk));