# HG changeset patch
# User oheimb
# Date 947093227 -3600
# Node ID de9fae0cdfdebff622cd7a8b51ea480636b51d6c
# Parent  2dda3e88d23f88c1b5f3df1ae2cff7a4d4901f24
improved symbol for subcls relation

diff -r 2dda3e88d23f -r de9fae0cdfde src/HOL/MicroJava/J/Conform.ML
--- a/src/HOL/MicroJava/J/Conform.ML	Wed Jan 05 16:13:05 2000 +0100
+++ b/src/HOL/MicroJava/J/Conform.ML	Wed Jan 05 18:27:07 2000 +0100
@@ -55,7 +55,7 @@
 (K [Asm_full_simp_tac 1]);
 
 val conf_obj_AddrI = prove_goalw thy [conf_def]
- "\\<And>G. \\<lbrakk>h a = Some (C,fs); G\\<turnstile>Class C\\<preceq>Class D\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>Addr a\\<Colon>\\<preceq>Class D" 
+ "\\<And>G. \\<lbrakk>h a = Some (C,fs); G\\<turnstile>Class C\\<preceq> Class D\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>Addr a\\<Colon>\\<preceq> Class D" 
 (K [Asm_full_simp_tac 1]);
 
 Goalw [conf_def] "is_type G T \\<longrightarrow> G,h\\<turnstile>default_val T\\<Colon>\\<preceq>T";
@@ -116,8 +116,8 @@
 	Step_tac 1,
 	 Auto_tac]);
 
-val non_np_objD = prove_goal thy "\\<And>G. \\<lbrakk>a' \\<noteq> Null; G,h\\<turnstile>a'\\<Colon>\\<preceq>Class C; C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> \
-\ (\\<exists>a C' fs. a' = Addr a \\<and>  h a = Some (C',fs) \\<and>  G\\<turnstile>Class C'\\<preceq>Class C)" 
+val non_np_objD = prove_goal thy "\\<And>G. \\<lbrakk>a' \\<noteq> Null; G,h\\<turnstile>a'\\<Colon>\\<preceq> Class C; C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> \
+\ (\\<exists>a C' fs. a' = Addr a \\<and>  h a = Some (C',fs) \\<and>  G\\<turnstile>Class C'\\<preceq> Class C)" 
 	(K[fast_tac (HOL_cs addDs [non_npD]) 1]);
 
 Goal "a' \\<noteq> Null \\<longrightarrow> wf_prog wf_mb G \\<longrightarrow> G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT t \\<longrightarrow>\
diff -r 2dda3e88d23f -r de9fae0cdfde src/HOL/MicroJava/J/JTypeSafe.ML
--- a/src/HOL/MicroJava/J/JTypeSafe.ML	Wed Jan 05 16:13:05 2000 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.ML	Wed Jan 05 18:27:07 2000 +0100
@@ -45,7 +45,7 @@
 qed "Cast_conf";
 
 Goal "\\<lbrakk> wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (h,l)\\<Colon>\\<preceq>(G,lT); \
-\    x' = None \\<longrightarrow> G,h\\<turnstile>a'\\<Colon>\\<preceq>Class C; np a' x' = None \\<rbrakk> \\<Longrightarrow> \
+\    x' = None \\<longrightarrow> G,h\\<turnstile>a'\\<Colon>\\<preceq> Class C; np a' x' = None \\<rbrakk> \\<Longrightarrow> \
 \ G,h\\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))\\<Colon>\\<preceq>ft";
 by( dtac np_NoneD 1);
 by( etac conjE 1);
@@ -67,7 +67,7 @@
 \   (G, lT)\\<turnstile>v\\<Colon>T'; G\\<turnstile>T'\\<preceq>ft; \
 \   (G, lT)\\<turnstile>aa\\<Colon>Class C; \
 \   field (G,C) fn = Some (fd, ft); h''\\<le>|h'; \
-\   x' = None \\<longrightarrow> G,h'\\<turnstile>a'\\<Colon>\\<preceq>Class C; h'\\<le>|h; \
+\   x' = None \\<longrightarrow> G,h'\\<turnstile>a'\\<Colon>\\<preceq> Class C; h'\\<le>|h; \
 \   (h, l)\\<Colon>\\<preceq>(G, lT); G,h\\<turnstile>x\\<Colon>\\<preceq>T'; np a' x' = None\\<rbrakk> \\<Longrightarrow> \
 \ h''\\<le>|h(a\\<mapsto>(c,(fs((fn,fd)\\<mapsto>x)))) \\<and>  \
 \ (h(a\\<mapsto>(c,(fs((fn,fd)\\<mapsto>x)))), l)\\<Colon>\\<preceq>(G, lT) \\<and>  \
@@ -131,7 +131,7 @@
 \ (G, lT)\\<turnstile>blk\\<surd> \\<longrightarrow>  h\\<le>|xi \\<and>  (xi, xl)\\<Colon>\\<preceq>(G, lT); \
 \ \\<forall>lT. (xi, xl)\\<Colon>\\<preceq>(G, lT) \\<longrightarrow> (\\<forall>T. (G, lT)\\<turnstile>res\\<Colon>T \\<longrightarrow> \
 \         xi\\<le>|h' \\<and> (h', xj)\\<Colon>\\<preceq>(G, lT) \\<and> (x' = None \\<longrightarrow> G,h'\\<turnstile>v\\<Colon>\\<preceq>T)); \
-\ G,xh\\<turnstile>a'\\<Colon>\\<preceq>Class C \\<rbrakk> \\<Longrightarrow> \
+\ G,xh\\<turnstile>a'\\<Colon>\\<preceq> Class C \\<rbrakk> \\<Longrightarrow> \
 \ xc\\<le>|h' \\<and> (h', l)\\<Colon>\\<preceq>(G, lT) \\<and>  (x' = None \\<longrightarrow> G,h'\\<turnstile>v\\<Colon>\\<preceq>rTa)";
 by( dtac (insertI1 RSN (2,(equalityD2 RS subsetD))) 1);
 by( dtac (max_spec2appl_meths RS appl_methsD) 1);
diff -r 2dda3e88d23f -r de9fae0cdfde src/HOL/MicroJava/J/TypeRel.ML
--- a/src/HOL/MicroJava/J/TypeRel.ML	Wed Jan 05 16:13:05 2000 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.ML	Wed Jan 05 18:27:07 2000 +0100
@@ -95,8 +95,8 @@
 val widen_Class_NullT = prove_typerel "G\\<turnstile>Class C\\<preceq>RefT NullT \\<Longrightarrow> R" 
  [prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S=Class C \\<longrightarrow> T=RefT NullT \\<longrightarrow> R"];
 
-val widen_Class_Class = prove_typerel "G\\<turnstile>Class C\\<preceq>Class cm \\<Longrightarrow> G\\<turnstile>C\\<prec>C cm"
-[ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = Class C \\<longrightarrow> T = Class cm \\<longrightarrow> G\\<turnstile>C\\<prec>C cm"];
+val widen_Class_Class = prove_typerel "G\\<turnstile>Class C\\<preceq> Class cm \\<Longrightarrow> G\\<turnstile>C\\<preceq>C cm"
+[ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = Class C \\<longrightarrow> T = Class cm \\<longrightarrow> G\\<turnstile>C\\<preceq>C cm"];
 
 Goal "G\\<turnstile>S\\<preceq>U \\<Longrightarrow> \\<forall>T. G\\<turnstile>U\\<preceq>T \\<longrightarrow> G\\<turnstile>S\\<preceq>T";
 by( etac widen.induct 1);
diff -r 2dda3e88d23f -r de9fae0cdfde src/HOL/MicroJava/J/TypeRel.thy
--- a/src/HOL/MicroJava/J/TypeRel.thy	Wed Jan 05 16:13:05 2000 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Wed Jan 05 18:27:07 2000 +0100
@@ -15,13 +15,13 @@
 
 syntax
   subcls1	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<prec>C1_"	 [71,71,71] 70)
-  subcls	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<prec>C _"	 [71,71,71] 70)
+  subcls	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>C _"	 [71,71,71] 70)
   widen		:: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool"       ("_\\<turnstile>_\\<preceq>_"  [71,71,71] 70)
   cast		:: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool"       ("_\\<turnstile>_\\<Rightarrow>? _"[71,71,71] 70)
 
 translations
   	"G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
-	"G\\<turnstile>C \\<prec>C  D" == "(C,D) \\<in> (subcls1 G)^*"
+	"G\\<turnstile>C \\<preceq>C  D" == "(C,D) \\<in> (subcls1 G)^*"
 	"G\\<turnstile>S \\<preceq>   T" == "(S,T) \\<in> widen   G"
 	"G\\<turnstile>S \\<Rightarrow>?  T" == "(S,T) \\<in> cast    G"
 
@@ -66,11 +66,11 @@
 inductive "widen G" intrs (*widening, viz. method invocation conversion, cf. 5.3
 			     i.e. sort of syntactic subtyping *)
   refl	              "G\\<turnstile>      T \\<preceq> T" 	 (* identity conv., cf. 5.1.1 *)
-  subcls "G\\<turnstile>C\\<prec>C D \\<Longrightarrow> G\\<turnstile>Class C \\<preceq> Class D"
+  subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class C \\<preceq> Class D"
   null	              "G\\<turnstile>     NT \\<preceq> RefT R"
 
 inductive "cast G" intrs (* casting / narr.ref. conversion, cf. 5.5 / 5.1.5 *)
   widen	 "G\\<turnstile>S\\<preceq>T  \\<Longrightarrow> G\\<turnstile>      S \\<Rightarrow>? T"
-  subcls "G\\<turnstile>C\\<prec>C D \\<Longrightarrow> G\\<turnstile>Class D \\<Rightarrow>? Class C"
+  subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class D \\<Rightarrow>? Class C"
 
 end
diff -r 2dda3e88d23f -r de9fae0cdfde src/HOL/MicroJava/J/WellForm.ML
--- a/src/HOL/MicroJava/J/WellForm.ML	Wed Jan 05 16:13:05 2000 +0100
+++ b/src/HOL/MicroJava/J/WellForm.ML	Wed Jan 05 18:27:07 2000 +0100
@@ -140,7 +140,7 @@
  "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> field (G,Object) = empty" (K [Asm_simp_tac 1]);
 Addsimps [field_Object];
 
-Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> G\\<turnstile>C\\<prec>C Object";
+Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> G\\<turnstile>C\\<preceq>C Object";
 by(etac subcls1_induct 1);
 by(  atac 1);
 by( Fast_tac 1);
@@ -152,7 +152,7 @@
 	"\\<And>sig. wf_mhead G sig rT \\<Longrightarrow> is_type G rT"
 	(K [split_all_tac 1, Auto_tac]);
 
-Goal "\\<lbrakk>wf_prog wf_mb G; is_class G C\\<rbrakk> \\<Longrightarrow> G\\<turnstile>Class C\\<preceq>Class Object";
+Goal "\\<lbrakk>wf_prog wf_mb G; is_class G C\\<rbrakk> \\<Longrightarrow> G\\<turnstile>Class C\\<preceq> Class Object";
 by(rtac widen.subcls 1);	
 by(eatac subcls_C_Object 1 1);
 qed "widen_Class_Object";
@@ -166,7 +166,7 @@
 qed_spec_mp "fields_mono";
 
 Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
-\ \\<forall>((fn,fd),fT)\\<in>set (fields (G,C)). G\\<turnstile>Class C\\<preceq>Class fd";
+\ \\<forall>((fn,fd),fT)\\<in>set (fields (G,C)). G\\<turnstile>Class C\\<preceq> Class fd";
 by( etac subcls1_induct 1);
 by(   atac 1);
 by(  Asm_simp_tac 1);
@@ -189,7 +189,7 @@
 qed "widen_fields_defpl'";
 
 Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G; ((fn,fd),fT) \\<in> set (fields (G,C))\\<rbrakk> \\<Longrightarrow> \
-\ G\\<turnstile>Class C\\<preceq>Class fd";
+\ G\\<turnstile>Class C\\<preceq> Class fd";
 by( datac widen_fields_defpl' 1 1);
 (*###################*)
 by( dtac bspec 1);
@@ -227,7 +227,7 @@
 qed "rtranclD";
 
 Goal
-"\\<lbrakk>wf_prog wf_mb G; G\\<turnstile>Class C'\\<preceq>Class C; map_of(fields (G,C )) f = Some ft\\<rbrakk> \\<Longrightarrow> \
+"\\<lbrakk>wf_prog wf_mb G; G\\<turnstile>Class C'\\<preceq> Class C; map_of(fields (G,C )) f = Some ft\\<rbrakk> \\<Longrightarrow> \
 \                          map_of (fields (G,C')) f = Some ft";
 by( dtac widen_Class_Class 1);
 by( dtac rtranclD 1);
@@ -246,11 +246,11 @@
 (K [rtac table_map_Some 1, Asm_full_simp_tac 1]);
 
 val widen_cfs_fields = prove_goal thy "\\<And>X. \\<lbrakk>field (G,C) fn = Some (fd, fT);\
-\  G\\<turnstile>Class C'\\<preceq>Class C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> map_of (fields (G,C')) (fn, fd) = Some fT" (K[
+\  G\\<turnstile>Class C'\\<preceq> Class C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> map_of (fields (G,C')) (fn, fd) = Some fT" (K[
 fast_tac (HOL_cs addIs [widen_fields_mono, cfs_fields_lemma]) 1]);
 
 Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,C) sig = Some (md,mh,m)\
-\  \\<longrightarrow> G\\<turnstile>Class C\\<preceq>Class md \\<and> wf_mdecl wf_mb G md (sig,(mh,m))";
+\  \\<longrightarrow> G\\<turnstile>Class C\\<preceq> Class md \\<and> wf_mdecl wf_mb G md (sig,(mh,m))";
 by( case_tac "is_class G C" 1);
 by(  forw_inst_tac [("C","C")] method_rec 2);
 by(    asm_full_simp_tac (simpset() addsimps [is_class_def] 
@@ -278,7 +278,7 @@
 by( Asm_full_simp_tac 1);
 qed_spec_mp "method_wf_mdecl";
 
-Goal "\\<lbrakk>G\\<turnstile>T\\<prec>C T'; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
+Goal "\\<lbrakk>G\\<turnstile>T\\<preceq>C T'; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
 \  \\<forall>D rT b. method (G,T') sig = Some (D,rT ,b) \\<longrightarrow>\
 \ (\\<exists>D' rT' b'. method (G,T) sig = Some (D',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT)";
 by( dtac rtranclD 1);
@@ -313,7 +313,7 @@
 
 
 Goal
- "\\<lbrakk> G\\<turnstile>Class C\\<preceq>Class D; wf_prog wf_mb G; \
+ "\\<lbrakk> G\\<turnstile>Class C\\<preceq> Class D; wf_prog wf_mb G; \
 \    method (G,D) sig = Some (md, rT, b) \\<rbrakk> \
 \ \\<Longrightarrow> \\<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
 by(auto_tac (claset() addSDs [widen_Class_Class]
diff -r 2dda3e88d23f -r de9fae0cdfde src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Wed Jan 05 16:13:05 2000 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy	Wed Jan 05 18:27:07 2000 +0100
@@ -36,7 +36,7 @@
 	(\\<forall>m\\<in>set ms. wf_mdecl wf_mb G C m) \\<and>  unique ms \\<and>
 	(case sc of None \\<Rightarrow> C = Object
          | Some D \\<Rightarrow>
-             is_class G D \\<and>  \\<not>  G\\<turnstile>D\\<prec>C C \\<and>
+             is_class G D \\<and>  \\<not>  G\\<turnstile>D\\<preceq>C C \\<and>
              (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
                  method(G,D) sig = Some(D',rT',b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))"
 
diff -r 2dda3e88d23f -r de9fae0cdfde src/HOL/MicroJava/J/WellType.ML
--- a/src/HOL/MicroJava/J/WellType.ML	Wed Jan 05 16:13:05 2000 +0100
+++ b/src/HOL/MicroJava/J/WellType.ML	Wed Jan 05 18:27:07 2000 +0100
@@ -5,7 +5,7 @@
 *)
 
 Goal
-"\\<lbrakk> method (G,C) sig = Some (md,rT,b); wf_prog wf_mb G; G\\<turnstile>Class T''\\<preceq>Class C\\<rbrakk>\
+"\\<lbrakk> method (G,C) sig = Some (md,rT,b); wf_prog wf_mb G; G\\<turnstile>Class T''\\<preceq> Class C\\<rbrakk>\
 \ \\<Longrightarrow> \\<exists>md' rT' b'. method (G,T'') sig = Some (md',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
 by( forward_tac [widen_Class_RefT] 1);
 by( etac exE 1);
@@ -18,9 +18,9 @@
 
 
 Goal
-"\\<lbrakk>method (G,C) sig = Some (md,rT,b); G\\<turnstile>Class T''\\<preceq>Class C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
+"\\<lbrakk>method (G,C) sig = Some (md,rT,b); G\\<turnstile>Class T''\\<preceq> Class C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
 \ \\<exists>T' rT' b. method (G,T'') sig = Some (T',rT',b) \\<and> \
-\ G\\<turnstile>rT'\\<preceq>rT \\<and> G\\<turnstile>Class T''\\<preceq>Class T' \\<and> wf_mhead G sig rT' \\<and> wf_mb G T' (sig,rT',b)";
+\ G\\<turnstile>rT'\\<preceq>rT \\<and> G\\<turnstile>Class T''\\<preceq> Class T' \\<and> wf_mhead G sig rT' \\<and> wf_mb G T' (sig,rT',b)";
 by( datac widen_methd 2 1);
 by( Clarsimp_tac 1);
 by( dtac method_wf_mdecl 1);