# HG changeset patch
# User oheimb
# Date 943025452 -3600
# Node ID 3e5ddca613dd19395f1e71a974203e3aa6f8d782
# Parent  2855e262129ccfd3a548b454e8a38ef45c6d843a
re-shaped and re-ordered conversion relations

diff -r 2855e262129c -r 3e5ddca613dd src/HOL/MicroJava/BV/BVSpec.thy
--- a/src/HOL/MicroJava/BV/BVSpec.thy	Thu Nov 18 12:12:39 1999 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Fri Nov 19 16:30:52 1999 +0100
@@ -22,7 +22,7 @@
 	 pc+1 < max_pc \\<and>
 	 idx < length LT \\<and>
 	 (\\<exists>ts. (LT ! idx) = Some ts \\<and> 
-	       G \\<turnstile> phi ! (pc+1) >>>= (ts # ST , LT)))"
+	       G \\<turnstile> (ts # ST , LT) <=s phi ! (pc+1)))"
 
 "wt_LS (Store idx) G phi max_pc pc =
 	(let (ST,LT) = phi ! pc
@@ -30,19 +30,19 @@
 	 pc+1 < max_pc \\<and>
 	 idx < length LT \\<and>
 	 (\\<exists>ts ST'. ST = ts # ST' \\<and>
-		   G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT[idx:=Some ts])))"
+		   G \\<turnstile> (ST' , LT[idx:=Some ts]) <=s phi ! (pc+1)))"
 
 "wt_LS (Bipush i) G phi max_pc pc =
 	(let (ST,LT) = phi ! pc
 	 in
 	 pc+1 < max_pc \\<and>
-	 G \\<turnstile> phi ! (pc+1) >>>= ((PrimT Integer) # ST , LT))"
+	 G \\<turnstile> ((PrimT Integer) # ST , LT) <=s phi ! (pc+1))"
 
 "wt_LS (Aconst_null) G phi max_pc pc =
 	(let (ST,LT) = phi ! pc
 	 in
 	 pc+1 < max_pc \\<and>
-	 G \\<turnstile> phi ! (pc+1) >>>= (NT # ST , LT))"
+	 G \\<turnstile> (NT # ST , LT) <=s phi ! (pc+1))"
 
 consts
  wt_MO	:: "[manipulate_object,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" 
@@ -55,7 +55,7 @@
 	 (\\<exists>T oT ST'. cfield (G,C) F = Some(C,T) \\<and>
                        ST = oT # ST' \\<and> 
 		       G \\<turnstile> oT \\<preceq> (Class C) \\<and>
-		       G \\<turnstile> phi ! (pc+1) >>>= (T # ST' , LT)))"
+		       G \\<turnstile> (T # ST' , LT) <=s phi ! (pc+1)))"
 
 "wt_MO (Putfield F C) G phi max_pc pc =
 	(let (ST,LT) = phi ! pc
@@ -67,7 +67,7 @@
              ST = vT # oT # ST' \\<and> 
              G \\<turnstile> oT \\<preceq> (Class C) \\<and>
 	     G \\<turnstile> vT \\<preceq> T  \\<and>
-             G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT)))"
+             G \\<turnstile> (ST' , LT) <=s phi ! (pc+1)))"
 
 
 consts 
@@ -78,7 +78,7 @@
 	 in
 	 pc+1 < max_pc \\<and>
 	 is_class G C \\<and>
-	 G \\<turnstile> phi ! (pc+1) >>>= ((Class C) # ST , LT))"
+	 G \\<turnstile> ((Class C) # ST , LT) <=s phi ! (pc+1))"
 
 consts
  wt_CH	:: "[check_object,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" 
@@ -89,7 +89,7 @@
 	 pc+1 < max_pc \\<and>
 	 is_class G C \\<and> 
 	 (\\<exists>rt ST'. ST = RefT rt # ST' \\<and>
-                   G \\<turnstile> phi ! (pc+1) >>>= (Class C # ST' , LT)))"
+                   G \\<turnstile> (Class C # ST' , LT) <=s phi ! (pc+1)))"
 
 consts 
  wt_OS	:: "[op_stack,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" 
@@ -99,35 +99,35 @@
 	 in
 	 \\<exists>ts ST'. pc+1 < max_pc \\<and>
 		ST = ts # ST' \\<and> 	 
-		G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT))"
+		G \\<turnstile> (ST' , LT) <=s phi ! (pc+1))"
 
 "wt_OS Dup G phi max_pc pc =
 	(let (ST,LT) = phi ! pc
 	 in
 	 pc+1 < max_pc \\<and>
 	 (\\<exists>ts ST'. ST = ts # ST' \\<and> 	 
-		   G \\<turnstile> phi ! (pc+1) >>>= (ts # ts # ST' , LT)))"
+		   G \\<turnstile> (ts # ts # ST' , LT) <=s phi ! (pc+1)))"
 
 "wt_OS Dup_x1 G phi max_pc pc =
 	(let (ST,LT) = phi ! pc
 	 in
 	 pc+1 < max_pc \\<and>
 	 (\\<exists>ts1 ts2 ST'. ST = ts1 # ts2 # ST' \\<and> 	 
-		   G \\<turnstile> phi ! (pc+1) >>>= (ts1 # ts2 # ts1 # ST' , LT)))"
+		   G \\<turnstile> (ts1 # ts2 # ts1 # ST' , LT) <=s phi ! (pc+1)))"
 
 "wt_OS Dup_x2 G phi max_pc pc =
 	(let (ST,LT) = phi ! pc
 	 in
 	 pc+1 < max_pc \\<and>
 	 (\\<exists>ts1 ts2 ts3 ST'. ST = ts1 # ts2 # ts3 # ST' \\<and> 	 
-		   G \\<turnstile> phi ! (pc+1) >>>= (ts1 # ts2 # ts3 # ts1 # ST' , LT)))"
+		   G \\<turnstile> (ts1 # ts2 # ts3 # ts1 # ST' , LT) <=s phi ! (pc+1)))"
 
 "wt_OS Swap G phi max_pc pc =
 	(let (ST,LT) = phi ! pc
 	 in
 	 pc+1 < max_pc \\<and>
 	 (\\<exists>ts ts' ST'. ST = ts' # ts # ST' \\<and> 	 
-		       G \\<turnstile> phi ! (pc+1) >>>= (ts # ts' # ST' , LT)))"
+		       G \\<turnstile> (ts # ts' # ST' , LT) <=s phi ! (pc+1)))"
 
 consts 
  wt_BR	:: "[branch,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" 
@@ -137,13 +137,13 @@
 	 in
 	 pc+1 < max_pc \\<and> (nat(int pc+branch)) < max_pc \\<and> 
 	 (\\<exists>ts ts' ST'. ST = ts # ts' # ST' \\<and>  ts = ts' \\<and>
-		       G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT) \\<and>
-		       G \\<turnstile> phi ! (nat(int pc+branch)) >>>= (ST' , LT)))"
+		       G \\<turnstile> (ST' , LT) <=s phi ! (pc+1) \\<and>
+		       G \\<turnstile> (ST' , LT) <=s phi ! (nat(int pc+branch))))"
 "wt_BR (Goto branch) G phi max_pc pc =
 	(let (ST,LT) = phi ! pc
 	 in
 	 (nat(int pc+branch)) < max_pc \\<and> 
-	 G \\<turnstile> phi ! (nat(int pc+branch)) >>>= (ST , LT))"
+	 G \\<turnstile> (ST , LT) <=s phi ! (nat(int pc+branch)))"
 
 consts
  wt_MI :: "[meth_inv,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" 
@@ -156,7 +156,7 @@
          length apTs = length fpTs \\<and>
          (\\<forall>(aT,fT)\\<in>set(zip apTs fpTs). G \\<turnstile> aT \\<preceq> fT) \\<and>
          (\\<exists>D rT b. cmethd (G,C) (mn,fpTs) = Some(D,rT,b) \\<and>
-         G \\<turnstile> phi ! (pc+1) >>>= (rT # ST' , LT))))"
+         G \\<turnstile> (rT # ST' , LT) <=s phi ! (pc+1))))"
 
 constdefs
  wt_MR	:: "[jvm_prog,ty,method_type,p_count] \\<Rightarrow> bool"
@@ -183,7 +183,7 @@
 constdefs
  wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \\<Rightarrow> bool"
  "wt_start G C pTs mxl phi \\<equiv> 
-    G \\<turnstile> phi!0 >>>= ([],(Some(Class C))#((map Some pTs))@(replicate mxl None))"
+    G \\<turnstile> ([],(Some(Class C))#((map Some pTs))@(replicate mxl None)) <=s phi!0"
 
 
  wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] \\<Rightarrow> bool"
diff -r 2855e262129c -r 3e5ddca613dd src/HOL/MicroJava/BV/Convert.ML
--- a/src/HOL/MicroJava/BV/Convert.ML	Thu Nov 18 12:12:39 1999 +0100
+++ b/src/HOL/MicroJava/BV/Convert.ML	Fri Nov 19 16:30:52 1999 +0100
@@ -9,32 +9,32 @@
  [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = PrimT x \\<longrightarrow> T = PrimT x"];
 Addsimps [widen_PrimT_conv1];
 
-Goalw [sup_ty_opt_def] "(G \\<turnstile> any >= None) = (any = None)";
+Goalw [sup_ty_opt_def] "(G \\<turnstile> None <=o any) = (any = None)";
 by(simp_tac (simpset() addsplits [option.split]) 1);
 qed "anyConvNone";
 Addsimps [anyConvNone];
 
-Goalw [sup_ty_opt_def] "(G \\<turnstile> Some ty >= Some ty') = (G \\<turnstile> ty' \\<preceq> ty)";
+Goalw [sup_ty_opt_def] "(G \\<turnstile> Some ty' <=o Some ty) = (G \\<turnstile> ty' \\<preceq> ty)";
 by(Simp_tac 1);
 qed "SomeanyConvSome";
 Addsimps [SomeanyConvSome];
 
 Goal
-"(G \\<turnstile> X >= Some(PrimT Integer)) = (X=None \\<or> (X=Some(PrimT Integer)))";
+"(G \\<turnstile> Some(PrimT Integer) <=o X) = (X=None \\<or> (X=Some(PrimT Integer)))";
 by (simp_tac (simpset() setloop (split_tac [ty.split,option.split]) addsimps [sup_ty_opt_def]) 1);
 qed "sup_PTS_eq";
 
 
 
 Goal
-"CFS \\<turnstile> XT >>= [] = (XT=[])";
+"CFS \\<turnstile> [] <=l XT = (XT=[])";
 by (case_tac "XT=[]" 1);
 by (asm_simp_tac (simpset() addsimps [sup_loc_def]) 1);
 by (fast_tac (claset() addss (simpset() addsimps [sup_loc_def,neq_Nil_conv])) 1);
 qed "sup_loc_Nil";
 
 Goal
-"CFS \\<turnstile> XT >>= (Y#YT) = (\\<exists>X XT'. XT=X#XT' \\<and> CFS \\<turnstile> X>=Y \\<and> CFS \\<turnstile> XT'>>=YT)";
+"CFS \\<turnstile> (Y#YT) <=l XT = (\\<exists>X XT'. XT=X#XT' \\<and> CFS \\<turnstile> Y <=o X \\<and> CFS \\<turnstile> YT <=l XT')";
 by (case_tac "XT=[]" 1);
 by (asm_simp_tac (simpset() addsimps [sup_loc_def]) 1);
 by (fast_tac (claset() addss (simpset() addsimps [sup_loc_def,neq_Nil_conv])) 1);
diff -r 2855e262129c -r 3e5ddca613dd src/HOL/MicroJava/BV/Convert.thy
--- a/src/HOL/MicroJava/BV/Convert.thy	Thu Nov 18 12:12:39 1999 +0100
+++ b/src/HOL/MicroJava/BV/Convert.thy	Fri Nov 19 16:30:52 1999 +0100
@@ -15,19 +15,19 @@
 
 constdefs
 
- sup_ty_opt :: "['code prog,ty option,ty option] \\<Rightarrow> bool" ("_ \\<turnstile>_ >= _")
- "G \\<turnstile> a >= a' \\<equiv>
+ sup_ty_opt :: "['code prog,ty option,ty option] \\<Rightarrow> bool" ("_ \\<turnstile>_ <=o _")
+ "G \\<turnstile> a' <=o a \\<equiv>
     case a of
       None \\<Rightarrow> True
     | Some t  \\<Rightarrow>  case a' of 
 		     None \\<Rightarrow> False
 		   | Some t' \\<Rightarrow> G \\<turnstile> t' \\<preceq> t" 
 
- sup_loc :: "['code prog,locvars_type,locvars_type] \\<Rightarrow> bool"	  ("_ \\<turnstile> _ >>= _"  [71,71] 70)
- "G \\<turnstile> LT >>= LT' \\<equiv> (length LT=length LT') \\<and> (\\<forall>(t,t')\\<in>set (zip LT LT'). G \\<turnstile> t >= t')"
+ sup_loc :: "['code prog,locvars_type,locvars_type] \\<Rightarrow> bool"	  ("_ \\<turnstile> _ <=l _"  [71,71] 70)
+ "G \\<turnstile> LT <=l LT' \\<equiv> (length LT=length LT') \\<and> (\\<forall>(t,t')\\<in>set (zip LT LT'). G \\<turnstile> t <=o t')"
 
 
- sup_state :: "['code prog,state_type,state_type] \\<Rightarrow> bool"	  ("_ \\<turnstile> _ >>>= _"  [71,71] 70)
- "G \\<turnstile> s >>>= s' \\<equiv> G \\<turnstile> map Some (fst s) >>= map Some (fst s') \\<and> G \\<turnstile> snd s >>= snd s'"
+ sup_state :: "['code prog,state_type,state_type] \\<Rightarrow> bool"	  ("_ \\<turnstile> _ <=s _"  [71,71] 70)
+ "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'"
 
 end
diff -r 2855e262129c -r 3e5ddca613dd src/HOL/MicroJava/BV/Correct.ML
--- a/src/HOL/MicroJava/BV/Correct.ML	Thu Nov 18 12:12:39 1999 +0100
+++ b/src/HOL/MicroJava/BV/Correct.ML	Fri Nov 19 16:30:52 1999 +0100
@@ -62,14 +62,14 @@
 
 
 Goal
-"wf_prog wt G \\<Longrightarrow> approx_val G h val us \\<longrightarrow> G \\<turnstile> us' >= us \\<longrightarrow> approx_val G h val us'";
+"wf_prog wt G \\<Longrightarrow> approx_val G h val us \\<longrightarrow> G \\<turnstile> us <=o us' \\<longrightarrow> approx_val G h val us'";
 by (asm_simp_tac (simpset() addsimps [sup_PTS_eq,approx_val_def] addsplits [option.split,val_.split,ty.split]) 1);
 by(blast_tac (claset() addIs [conf_widen]) 1);
 qed_spec_mp "approx_val_imp_approx_val_sup";
 
 
 Goal 
-"\\<lbrakk> wf_prog wt G; approx_loc G hp loc LT; idx < length LT ; val = loc ! idx ; G \\<turnstile> at >= LT ! idx \\<rbrakk> \
+"\\<lbrakk> wf_prog wt G; approx_loc G hp loc LT; idx < length LT ; val = loc ! idx ; G \\<turnstile> LT ! idx <=o at\\<rbrakk> \
 \\\<Longrightarrow> approx_val G hp val at";
 by (fast_tac (claset() addIs [approx_val_imp_approx_val_sup] addss (simpset() addsimps 
 	[split_def,approx_loc_def,all_set_conv_all_nth])) 1);
@@ -104,7 +104,7 @@
 
 
 Goalw [sup_loc_def,approx_loc_def]
-"wf_prog wt G \\<Longrightarrow> approx_loc G hp lvars lt \\<longrightarrow> G \\<turnstile> lt' >>= lt \\<longrightarrow> approx_loc G hp lvars lt'";
+"wf_prog wt G \\<Longrightarrow> approx_loc G hp lvars lt \\<longrightarrow> G \\<turnstile> lt <=l lt' \\<longrightarrow> approx_loc G hp lvars lt'";
 by (auto_tac (claset() , simpset() addsimps [all_set_conv_all_nth,split_def]));
 by (auto_tac (claset() addEs [approx_val_imp_approx_val_sup] , simpset()));
 qed_spec_mp "approx_loc_imp_approx_loc_sup";
@@ -154,7 +154,7 @@
 
 
 Goalw [approx_stk_def]
-"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'";
+"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'";
 by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup])  1);
 qed_spec_mp "approx_stk_imp_approx_stk_sup";