--- 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>\
--- 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);
--- 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);
--- 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
--- 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]
--- 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'))"
--- 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);