1.1 --- a/src/HOL/MicroJava/BV/BVSpec.thy Thu Nov 18 12:12:39 1999 +0100
1.2 +++ b/src/HOL/MicroJava/BV/BVSpec.thy Fri Nov 19 16:30:52 1999 +0100
1.3 @@ -22,7 +22,7 @@
1.4 pc+1 < max_pc \\<and>
1.5 idx < length LT \\<and>
1.6 (\\<exists>ts. (LT ! idx) = Some ts \\<and>
1.7 - G \\<turnstile> phi ! (pc+1) >>>= (ts # ST , LT)))"
1.8 + G \\<turnstile> (ts # ST , LT) <=s phi ! (pc+1)))"
1.9
1.10 "wt_LS (Store idx) G phi max_pc pc =
1.11 (let (ST,LT) = phi ! pc
1.12 @@ -30,19 +30,19 @@
1.13 pc+1 < max_pc \\<and>
1.14 idx < length LT \\<and>
1.15 (\\<exists>ts ST'. ST = ts # ST' \\<and>
1.16 - G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT[idx:=Some ts])))"
1.17 + G \\<turnstile> (ST' , LT[idx:=Some ts]) <=s phi ! (pc+1)))"
1.18
1.19 "wt_LS (Bipush i) G phi max_pc pc =
1.20 (let (ST,LT) = phi ! pc
1.21 in
1.22 pc+1 < max_pc \\<and>
1.23 - G \\<turnstile> phi ! (pc+1) >>>= ((PrimT Integer) # ST , LT))"
1.24 + G \\<turnstile> ((PrimT Integer) # ST , LT) <=s phi ! (pc+1))"
1.25
1.26 "wt_LS (Aconst_null) G phi max_pc pc =
1.27 (let (ST,LT) = phi ! pc
1.28 in
1.29 pc+1 < max_pc \\<and>
1.30 - G \\<turnstile> phi ! (pc+1) >>>= (NT # ST , LT))"
1.31 + G \\<turnstile> (NT # ST , LT) <=s phi ! (pc+1))"
1.32
1.33 consts
1.34 wt_MO :: "[manipulate_object,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
1.35 @@ -55,7 +55,7 @@
1.36 (\\<exists>T oT ST'. cfield (G,C) F = Some(C,T) \\<and>
1.37 ST = oT # ST' \\<and>
1.38 G \\<turnstile> oT \\<preceq> (Class C) \\<and>
1.39 - G \\<turnstile> phi ! (pc+1) >>>= (T # ST' , LT)))"
1.40 + G \\<turnstile> (T # ST' , LT) <=s phi ! (pc+1)))"
1.41
1.42 "wt_MO (Putfield F C) G phi max_pc pc =
1.43 (let (ST,LT) = phi ! pc
1.44 @@ -67,7 +67,7 @@
1.45 ST = vT # oT # ST' \\<and>
1.46 G \\<turnstile> oT \\<preceq> (Class C) \\<and>
1.47 G \\<turnstile> vT \\<preceq> T \\<and>
1.48 - G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT)))"
1.49 + G \\<turnstile> (ST' , LT) <=s phi ! (pc+1)))"
1.50
1.51
1.52 consts
1.53 @@ -78,7 +78,7 @@
1.54 in
1.55 pc+1 < max_pc \\<and>
1.56 is_class G C \\<and>
1.57 - G \\<turnstile> phi ! (pc+1) >>>= ((Class C) # ST , LT))"
1.58 + G \\<turnstile> ((Class C) # ST , LT) <=s phi ! (pc+1))"
1.59
1.60 consts
1.61 wt_CH :: "[check_object,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
1.62 @@ -89,7 +89,7 @@
1.63 pc+1 < max_pc \\<and>
1.64 is_class G C \\<and>
1.65 (\\<exists>rt ST'. ST = RefT rt # ST' \\<and>
1.66 - G \\<turnstile> phi ! (pc+1) >>>= (Class C # ST' , LT)))"
1.67 + G \\<turnstile> (Class C # ST' , LT) <=s phi ! (pc+1)))"
1.68
1.69 consts
1.70 wt_OS :: "[op_stack,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
1.71 @@ -99,35 +99,35 @@
1.72 in
1.73 \\<exists>ts ST'. pc+1 < max_pc \\<and>
1.74 ST = ts # ST' \\<and>
1.75 - G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT))"
1.76 + G \\<turnstile> (ST' , LT) <=s phi ! (pc+1))"
1.77
1.78 "wt_OS Dup G phi max_pc pc =
1.79 (let (ST,LT) = phi ! pc
1.80 in
1.81 pc+1 < max_pc \\<and>
1.82 (\\<exists>ts ST'. ST = ts # ST' \\<and>
1.83 - G \\<turnstile> phi ! (pc+1) >>>= (ts # ts # ST' , LT)))"
1.84 + G \\<turnstile> (ts # ts # ST' , LT) <=s phi ! (pc+1)))"
1.85
1.86 "wt_OS Dup_x1 G phi max_pc pc =
1.87 (let (ST,LT) = phi ! pc
1.88 in
1.89 pc+1 < max_pc \\<and>
1.90 (\\<exists>ts1 ts2 ST'. ST = ts1 # ts2 # ST' \\<and>
1.91 - G \\<turnstile> phi ! (pc+1) >>>= (ts1 # ts2 # ts1 # ST' , LT)))"
1.92 + G \\<turnstile> (ts1 # ts2 # ts1 # ST' , LT) <=s phi ! (pc+1)))"
1.93
1.94 "wt_OS Dup_x2 G phi max_pc pc =
1.95 (let (ST,LT) = phi ! pc
1.96 in
1.97 pc+1 < max_pc \\<and>
1.98 (\\<exists>ts1 ts2 ts3 ST'. ST = ts1 # ts2 # ts3 # ST' \\<and>
1.99 - G \\<turnstile> phi ! (pc+1) >>>= (ts1 # ts2 # ts3 # ts1 # ST' , LT)))"
1.100 + G \\<turnstile> (ts1 # ts2 # ts3 # ts1 # ST' , LT) <=s phi ! (pc+1)))"
1.101
1.102 "wt_OS Swap G phi max_pc pc =
1.103 (let (ST,LT) = phi ! pc
1.104 in
1.105 pc+1 < max_pc \\<and>
1.106 (\\<exists>ts ts' ST'. ST = ts' # ts # ST' \\<and>
1.107 - G \\<turnstile> phi ! (pc+1) >>>= (ts # ts' # ST' , LT)))"
1.108 + G \\<turnstile> (ts # ts' # ST' , LT) <=s phi ! (pc+1)))"
1.109
1.110 consts
1.111 wt_BR :: "[branch,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
1.112 @@ -137,13 +137,13 @@
1.113 in
1.114 pc+1 < max_pc \\<and> (nat(int pc+branch)) < max_pc \\<and>
1.115 (\\<exists>ts ts' ST'. ST = ts # ts' # ST' \\<and> ts = ts' \\<and>
1.116 - G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT) \\<and>
1.117 - G \\<turnstile> phi ! (nat(int pc+branch)) >>>= (ST' , LT)))"
1.118 + G \\<turnstile> (ST' , LT) <=s phi ! (pc+1) \\<and>
1.119 + G \\<turnstile> (ST' , LT) <=s phi ! (nat(int pc+branch))))"
1.120 "wt_BR (Goto branch) G phi max_pc pc =
1.121 (let (ST,LT) = phi ! pc
1.122 in
1.123 (nat(int pc+branch)) < max_pc \\<and>
1.124 - G \\<turnstile> phi ! (nat(int pc+branch)) >>>= (ST , LT))"
1.125 + G \\<turnstile> (ST , LT) <=s phi ! (nat(int pc+branch)))"
1.126
1.127 consts
1.128 wt_MI :: "[meth_inv,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
1.129 @@ -156,7 +156,7 @@
1.130 length apTs = length fpTs \\<and>
1.131 (\\<forall>(aT,fT)\\<in>set(zip apTs fpTs). G \\<turnstile> aT \\<preceq> fT) \\<and>
1.132 (\\<exists>D rT b. cmethd (G,C) (mn,fpTs) = Some(D,rT,b) \\<and>
1.133 - G \\<turnstile> phi ! (pc+1) >>>= (rT # ST' , LT))))"
1.134 + G \\<turnstile> (rT # ST' , LT) <=s phi ! (pc+1))))"
1.135
1.136 constdefs
1.137 wt_MR :: "[jvm_prog,ty,method_type,p_count] \\<Rightarrow> bool"
1.138 @@ -183,7 +183,7 @@
1.139 constdefs
1.140 wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \\<Rightarrow> bool"
1.141 "wt_start G C pTs mxl phi \\<equiv>
1.142 - G \\<turnstile> phi!0 >>>= ([],(Some(Class C))#((map Some pTs))@(replicate mxl None))"
1.143 + G \\<turnstile> ([],(Some(Class C))#((map Some pTs))@(replicate mxl None)) <=s phi!0"
1.144
1.145
1.146 wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] \\<Rightarrow> bool"
2.1 --- a/src/HOL/MicroJava/BV/Convert.ML Thu Nov 18 12:12:39 1999 +0100
2.2 +++ b/src/HOL/MicroJava/BV/Convert.ML Fri Nov 19 16:30:52 1999 +0100
2.3 @@ -9,32 +9,32 @@
2.4 [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = PrimT x \\<longrightarrow> T = PrimT x"];
2.5 Addsimps [widen_PrimT_conv1];
2.6
2.7 -Goalw [sup_ty_opt_def] "(G \\<turnstile> any >= None) = (any = None)";
2.8 +Goalw [sup_ty_opt_def] "(G \\<turnstile> None <=o any) = (any = None)";
2.9 by(simp_tac (simpset() addsplits [option.split]) 1);
2.10 qed "anyConvNone";
2.11 Addsimps [anyConvNone];
2.12
2.13 -Goalw [sup_ty_opt_def] "(G \\<turnstile> Some ty >= Some ty') = (G \\<turnstile> ty' \\<preceq> ty)";
2.14 +Goalw [sup_ty_opt_def] "(G \\<turnstile> Some ty' <=o Some ty) = (G \\<turnstile> ty' \\<preceq> ty)";
2.15 by(Simp_tac 1);
2.16 qed "SomeanyConvSome";
2.17 Addsimps [SomeanyConvSome];
2.18
2.19 Goal
2.20 -"(G \\<turnstile> X >= Some(PrimT Integer)) = (X=None \\<or> (X=Some(PrimT Integer)))";
2.21 +"(G \\<turnstile> Some(PrimT Integer) <=o X) = (X=None \\<or> (X=Some(PrimT Integer)))";
2.22 by (simp_tac (simpset() setloop (split_tac [ty.split,option.split]) addsimps [sup_ty_opt_def]) 1);
2.23 qed "sup_PTS_eq";
2.24
2.25
2.26
2.27 Goal
2.28 -"CFS \\<turnstile> XT >>= [] = (XT=[])";
2.29 +"CFS \\<turnstile> [] <=l XT = (XT=[])";
2.30 by (case_tac "XT=[]" 1);
2.31 by (asm_simp_tac (simpset() addsimps [sup_loc_def]) 1);
2.32 by (fast_tac (claset() addss (simpset() addsimps [sup_loc_def,neq_Nil_conv])) 1);
2.33 qed "sup_loc_Nil";
2.34
2.35 Goal
2.36 -"CFS \\<turnstile> XT >>= (Y#YT) = (\\<exists>X XT'. XT=X#XT' \\<and> CFS \\<turnstile> X>=Y \\<and> CFS \\<turnstile> XT'>>=YT)";
2.37 +"CFS \\<turnstile> (Y#YT) <=l XT = (\\<exists>X XT'. XT=X#XT' \\<and> CFS \\<turnstile> Y <=o X \\<and> CFS \\<turnstile> YT <=l XT')";
2.38 by (case_tac "XT=[]" 1);
2.39 by (asm_simp_tac (simpset() addsimps [sup_loc_def]) 1);
2.40 by (fast_tac (claset() addss (simpset() addsimps [sup_loc_def,neq_Nil_conv])) 1);
3.1 --- a/src/HOL/MicroJava/BV/Convert.thy Thu Nov 18 12:12:39 1999 +0100
3.2 +++ b/src/HOL/MicroJava/BV/Convert.thy Fri Nov 19 16:30:52 1999 +0100
3.3 @@ -15,19 +15,19 @@
3.4
3.5 constdefs
3.6
3.7 - sup_ty_opt :: "['code prog,ty option,ty option] \\<Rightarrow> bool" ("_ \\<turnstile>_ >= _")
3.8 - "G \\<turnstile> a >= a' \\<equiv>
3.9 + sup_ty_opt :: "['code prog,ty option,ty option] \\<Rightarrow> bool" ("_ \\<turnstile>_ <=o _")
3.10 + "G \\<turnstile> a' <=o a \\<equiv>
3.11 case a of
3.12 None \\<Rightarrow> True
3.13 | Some t \\<Rightarrow> case a' of
3.14 None \\<Rightarrow> False
3.15 | Some t' \\<Rightarrow> G \\<turnstile> t' \\<preceq> t"
3.16
3.17 - sup_loc :: "['code prog,locvars_type,locvars_type] \\<Rightarrow> bool" ("_ \\<turnstile> _ >>= _" [71,71] 70)
3.18 - "G \\<turnstile> LT >>= LT' \\<equiv> (length LT=length LT') \\<and> (\\<forall>(t,t')\\<in>set (zip LT LT'). G \\<turnstile> t >= t')"
3.19 + sup_loc :: "['code prog,locvars_type,locvars_type] \\<Rightarrow> bool" ("_ \\<turnstile> _ <=l _" [71,71] 70)
3.20 + "G \\<turnstile> LT <=l LT' \\<equiv> (length LT=length LT') \\<and> (\\<forall>(t,t')\\<in>set (zip LT LT'). G \\<turnstile> t <=o t')"
3.21
3.22
3.23 - sup_state :: "['code prog,state_type,state_type] \\<Rightarrow> bool" ("_ \\<turnstile> _ >>>= _" [71,71] 70)
3.24 - "G \\<turnstile> s >>>= s' \\<equiv> G \\<turnstile> map Some (fst s) >>= map Some (fst s') \\<and> G \\<turnstile> snd s >>= snd s'"
3.25 + sup_state :: "['code prog,state_type,state_type] \\<Rightarrow> bool" ("_ \\<turnstile> _ <=s _" [71,71] 70)
3.26 + "G \\<turnstile> s <=s s' \\<equiv> G \\<turnstile> map Some (fst s) <=l map Some (fst s') \\<and> G \\<turnstile> snd s <=l snd s'"
3.27
3.28 end
4.1 --- a/src/HOL/MicroJava/BV/Correct.ML Thu Nov 18 12:12:39 1999 +0100
4.2 +++ b/src/HOL/MicroJava/BV/Correct.ML Fri Nov 19 16:30:52 1999 +0100
4.3 @@ -62,14 +62,14 @@
4.4
4.5
4.6 Goal
4.7 -"wf_prog wt G \\<Longrightarrow> approx_val G h val us \\<longrightarrow> G \\<turnstile> us' >= us \\<longrightarrow> approx_val G h val us'";
4.8 +"wf_prog wt G \\<Longrightarrow> approx_val G h val us \\<longrightarrow> G \\<turnstile> us <=o us' \\<longrightarrow> approx_val G h val us'";
4.9 by (asm_simp_tac (simpset() addsimps [sup_PTS_eq,approx_val_def] addsplits [option.split,val_.split,ty.split]) 1);
4.10 by(blast_tac (claset() addIs [conf_widen]) 1);
4.11 qed_spec_mp "approx_val_imp_approx_val_sup";
4.12
4.13
4.14 Goal
4.15 -"\\<lbrakk> wf_prog wt G; approx_loc G hp loc LT; idx < length LT ; val = loc ! idx ; G \\<turnstile> at >= LT ! idx \\<rbrakk> \
4.16 +"\\<lbrakk> wf_prog wt G; approx_loc G hp loc LT; idx < length LT ; val = loc ! idx ; G \\<turnstile> LT ! idx <=o at\\<rbrakk> \
4.17 \\\<Longrightarrow> approx_val G hp val at";
4.18 by (fast_tac (claset() addIs [approx_val_imp_approx_val_sup] addss (simpset() addsimps
4.19 [split_def,approx_loc_def,all_set_conv_all_nth])) 1);
4.20 @@ -104,7 +104,7 @@
4.21
4.22
4.23 Goalw [sup_loc_def,approx_loc_def]
4.24 -"wf_prog wt G \\<Longrightarrow> approx_loc G hp lvars lt \\<longrightarrow> G \\<turnstile> lt' >>= lt \\<longrightarrow> approx_loc G hp lvars lt'";
4.25 +"wf_prog wt G \\<Longrightarrow> approx_loc G hp lvars lt \\<longrightarrow> G \\<turnstile> lt <=l lt' \\<longrightarrow> approx_loc G hp lvars lt'";
4.26 by (auto_tac (claset() , simpset() addsimps [all_set_conv_all_nth,split_def]));
4.27 by (auto_tac (claset() addEs [approx_val_imp_approx_val_sup] , simpset()));
4.28 qed_spec_mp "approx_loc_imp_approx_loc_sup";
4.29 @@ -154,7 +154,7 @@
4.30
4.31
4.32 Goalw [approx_stk_def]
4.33 -"wf_prog wt G \\<Longrightarrow> approx_stk G hp lvars st \\<longrightarrow> G \\<turnstile> (map Some st') >>= (map Some st) \\<longrightarrow> approx_stk G hp lvars st'";
4.34 +"wf_prog wt G \\<Longrightarrow> approx_stk G hp lvars st \\<longrightarrow> G \\<turnstile> (map Some st) <=l (map Some st') \\<longrightarrow> approx_stk G hp lvars st'";
4.35 by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup]) 1);
4.36 qed_spec_mp "approx_stk_imp_approx_stk_sup";
4.37