improved symbol for subcls relation
authoroheimb
Wed Jan 05 18:27:07 2000 +0100 (2000-01-05)
changeset 8106de9fae0cdfde
parent 8105 2dda3e88d23f
child 8107 284d6a3c8bd2
improved symbol for subcls relation
src/HOL/MicroJava/J/Conform.ML
src/HOL/MicroJava/J/JTypeSafe.ML
src/HOL/MicroJava/J/TypeRel.ML
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/MicroJava/J/WellForm.ML
src/HOL/MicroJava/J/WellForm.thy
src/HOL/MicroJava/J/WellType.ML
     1.1 --- a/src/HOL/MicroJava/J/Conform.ML	Wed Jan 05 16:13:05 2000 +0100
     1.2 +++ b/src/HOL/MicroJava/J/Conform.ML	Wed Jan 05 18:27:07 2000 +0100
     1.3 @@ -55,7 +55,7 @@
     1.4  (K [Asm_full_simp_tac 1]);
     1.5  
     1.6  val conf_obj_AddrI = prove_goalw thy [conf_def]
     1.7 - "\\<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" 
     1.8 + "\\<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" 
     1.9  (K [Asm_full_simp_tac 1]);
    1.10  
    1.11  Goalw [conf_def] "is_type G T \\<longrightarrow> G,h\\<turnstile>default_val T\\<Colon>\\<preceq>T";
    1.12 @@ -116,8 +116,8 @@
    1.13  	Step_tac 1,
    1.14  	 Auto_tac]);
    1.15  
    1.16 -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> \
    1.17 -\ (\\<exists>a C' fs. a' = Addr a \\<and>  h a = Some (C',fs) \\<and>  G\\<turnstile>Class C'\\<preceq>Class C)" 
    1.18 +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> \
    1.19 +\ (\\<exists>a C' fs. a' = Addr a \\<and>  h a = Some (C',fs) \\<and>  G\\<turnstile>Class C'\\<preceq> Class C)" 
    1.20  	(K[fast_tac (HOL_cs addDs [non_npD]) 1]);
    1.21  
    1.22  Goal "a' \\<noteq> Null \\<longrightarrow> wf_prog wf_mb G \\<longrightarrow> G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT t \\<longrightarrow>\
     2.1 --- a/src/HOL/MicroJava/J/JTypeSafe.ML	Wed Jan 05 16:13:05 2000 +0100
     2.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.ML	Wed Jan 05 18:27:07 2000 +0100
     2.3 @@ -45,7 +45,7 @@
     2.4  qed "Cast_conf";
     2.5  
     2.6  Goal "\\<lbrakk> wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (h,l)\\<Colon>\\<preceq>(G,lT); \
     2.7 -\    x' = None \\<longrightarrow> G,h\\<turnstile>a'\\<Colon>\\<preceq>Class C; np a' x' = None \\<rbrakk> \\<Longrightarrow> \
     2.8 +\    x' = None \\<longrightarrow> G,h\\<turnstile>a'\\<Colon>\\<preceq> Class C; np a' x' = None \\<rbrakk> \\<Longrightarrow> \
     2.9  \ G,h\\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))\\<Colon>\\<preceq>ft";
    2.10  by( dtac np_NoneD 1);
    2.11  by( etac conjE 1);
    2.12 @@ -67,7 +67,7 @@
    2.13  \   (G, lT)\\<turnstile>v\\<Colon>T'; G\\<turnstile>T'\\<preceq>ft; \
    2.14  \   (G, lT)\\<turnstile>aa\\<Colon>Class C; \
    2.15  \   field (G,C) fn = Some (fd, ft); h''\\<le>|h'; \
    2.16 -\   x' = None \\<longrightarrow> G,h'\\<turnstile>a'\\<Colon>\\<preceq>Class C; h'\\<le>|h; \
    2.17 +\   x' = None \\<longrightarrow> G,h'\\<turnstile>a'\\<Colon>\\<preceq> Class C; h'\\<le>|h; \
    2.18  \   (h, l)\\<Colon>\\<preceq>(G, lT); G,h\\<turnstile>x\\<Colon>\\<preceq>T'; np a' x' = None\\<rbrakk> \\<Longrightarrow> \
    2.19  \ h''\\<le>|h(a\\<mapsto>(c,(fs((fn,fd)\\<mapsto>x)))) \\<and>  \
    2.20  \ (h(a\\<mapsto>(c,(fs((fn,fd)\\<mapsto>x)))), l)\\<Colon>\\<preceq>(G, lT) \\<and>  \
    2.21 @@ -131,7 +131,7 @@
    2.22  \ (G, lT)\\<turnstile>blk\\<surd> \\<longrightarrow>  h\\<le>|xi \\<and>  (xi, xl)\\<Colon>\\<preceq>(G, lT); \
    2.23  \ \\<forall>lT. (xi, xl)\\<Colon>\\<preceq>(G, lT) \\<longrightarrow> (\\<forall>T. (G, lT)\\<turnstile>res\\<Colon>T \\<longrightarrow> \
    2.24  \         xi\\<le>|h' \\<and> (h', xj)\\<Colon>\\<preceq>(G, lT) \\<and> (x' = None \\<longrightarrow> G,h'\\<turnstile>v\\<Colon>\\<preceq>T)); \
    2.25 -\ G,xh\\<turnstile>a'\\<Colon>\\<preceq>Class C \\<rbrakk> \\<Longrightarrow> \
    2.26 +\ G,xh\\<turnstile>a'\\<Colon>\\<preceq> Class C \\<rbrakk> \\<Longrightarrow> \
    2.27  \ xc\\<le>|h' \\<and> (h', l)\\<Colon>\\<preceq>(G, lT) \\<and>  (x' = None \\<longrightarrow> G,h'\\<turnstile>v\\<Colon>\\<preceq>rTa)";
    2.28  by( dtac (insertI1 RSN (2,(equalityD2 RS subsetD))) 1);
    2.29  by( dtac (max_spec2appl_meths RS appl_methsD) 1);
     3.1 --- a/src/HOL/MicroJava/J/TypeRel.ML	Wed Jan 05 16:13:05 2000 +0100
     3.2 +++ b/src/HOL/MicroJava/J/TypeRel.ML	Wed Jan 05 18:27:07 2000 +0100
     3.3 @@ -95,8 +95,8 @@
     3.4  val widen_Class_NullT = prove_typerel "G\\<turnstile>Class C\\<preceq>RefT NullT \\<Longrightarrow> R" 
     3.5   [prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S=Class C \\<longrightarrow> T=RefT NullT \\<longrightarrow> R"];
     3.6  
     3.7 -val widen_Class_Class = prove_typerel "G\\<turnstile>Class C\\<preceq>Class cm \\<Longrightarrow> G\\<turnstile>C\\<prec>C cm"
     3.8 -[ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = Class C \\<longrightarrow> T = Class cm \\<longrightarrow> G\\<turnstile>C\\<prec>C cm"];
     3.9 +val widen_Class_Class = prove_typerel "G\\<turnstile>Class C\\<preceq> Class cm \\<Longrightarrow> G\\<turnstile>C\\<preceq>C cm"
    3.10 +[ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = Class C \\<longrightarrow> T = Class cm \\<longrightarrow> G\\<turnstile>C\\<preceq>C cm"];
    3.11  
    3.12  Goal "G\\<turnstile>S\\<preceq>U \\<Longrightarrow> \\<forall>T. G\\<turnstile>U\\<preceq>T \\<longrightarrow> G\\<turnstile>S\\<preceq>T";
    3.13  by( etac widen.induct 1);
     4.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Wed Jan 05 16:13:05 2000 +0100
     4.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Wed Jan 05 18:27:07 2000 +0100
     4.3 @@ -15,13 +15,13 @@
     4.4  
     4.5  syntax
     4.6    subcls1	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<prec>C1_"	 [71,71,71] 70)
     4.7 -  subcls	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<prec>C _"	 [71,71,71] 70)
     4.8 +  subcls	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>C _"	 [71,71,71] 70)
     4.9    widen		:: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool"       ("_\\<turnstile>_\\<preceq>_"  [71,71,71] 70)
    4.10    cast		:: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool"       ("_\\<turnstile>_\\<Rightarrow>? _"[71,71,71] 70)
    4.11  
    4.12  translations
    4.13    	"G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
    4.14 -	"G\\<turnstile>C \\<prec>C  D" == "(C,D) \\<in> (subcls1 G)^*"
    4.15 +	"G\\<turnstile>C \\<preceq>C  D" == "(C,D) \\<in> (subcls1 G)^*"
    4.16  	"G\\<turnstile>S \\<preceq>   T" == "(S,T) \\<in> widen   G"
    4.17  	"G\\<turnstile>S \\<Rightarrow>?  T" == "(S,T) \\<in> cast    G"
    4.18  
    4.19 @@ -66,11 +66,11 @@
    4.20  inductive "widen G" intrs (*widening, viz. method invocation conversion, cf. 5.3
    4.21  			     i.e. sort of syntactic subtyping *)
    4.22    refl	              "G\\<turnstile>      T \\<preceq> T" 	 (* identity conv., cf. 5.1.1 *)
    4.23 -  subcls "G\\<turnstile>C\\<prec>C D \\<Longrightarrow> G\\<turnstile>Class C \\<preceq> Class D"
    4.24 +  subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class C \\<preceq> Class D"
    4.25    null	              "G\\<turnstile>     NT \\<preceq> RefT R"
    4.26  
    4.27  inductive "cast G" intrs (* casting / narr.ref. conversion, cf. 5.5 / 5.1.5 *)
    4.28    widen	 "G\\<turnstile>S\\<preceq>T  \\<Longrightarrow> G\\<turnstile>      S \\<Rightarrow>? T"
    4.29 -  subcls "G\\<turnstile>C\\<prec>C D \\<Longrightarrow> G\\<turnstile>Class D \\<Rightarrow>? Class C"
    4.30 +  subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class D \\<Rightarrow>? Class C"
    4.31  
    4.32  end
     5.1 --- a/src/HOL/MicroJava/J/WellForm.ML	Wed Jan 05 16:13:05 2000 +0100
     5.2 +++ b/src/HOL/MicroJava/J/WellForm.ML	Wed Jan 05 18:27:07 2000 +0100
     5.3 @@ -140,7 +140,7 @@
     5.4   "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> field (G,Object) = empty" (K [Asm_simp_tac 1]);
     5.5  Addsimps [field_Object];
     5.6  
     5.7 -Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> G\\<turnstile>C\\<prec>C Object";
     5.8 +Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> G\\<turnstile>C\\<preceq>C Object";
     5.9  by(etac subcls1_induct 1);
    5.10  by(  atac 1);
    5.11  by( Fast_tac 1);
    5.12 @@ -152,7 +152,7 @@
    5.13  	"\\<And>sig. wf_mhead G sig rT \\<Longrightarrow> is_type G rT"
    5.14  	(K [split_all_tac 1, Auto_tac]);
    5.15  
    5.16 -Goal "\\<lbrakk>wf_prog wf_mb G; is_class G C\\<rbrakk> \\<Longrightarrow> G\\<turnstile>Class C\\<preceq>Class Object";
    5.17 +Goal "\\<lbrakk>wf_prog wf_mb G; is_class G C\\<rbrakk> \\<Longrightarrow> G\\<turnstile>Class C\\<preceq> Class Object";
    5.18  by(rtac widen.subcls 1);	
    5.19  by(eatac subcls_C_Object 1 1);
    5.20  qed "widen_Class_Object";
    5.21 @@ -166,7 +166,7 @@
    5.22  qed_spec_mp "fields_mono";
    5.23  
    5.24  Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
    5.25 -\ \\<forall>((fn,fd),fT)\\<in>set (fields (G,C)). G\\<turnstile>Class C\\<preceq>Class fd";
    5.26 +\ \\<forall>((fn,fd),fT)\\<in>set (fields (G,C)). G\\<turnstile>Class C\\<preceq> Class fd";
    5.27  by( etac subcls1_induct 1);
    5.28  by(   atac 1);
    5.29  by(  Asm_simp_tac 1);
    5.30 @@ -189,7 +189,7 @@
    5.31  qed "widen_fields_defpl'";
    5.32  
    5.33  Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G; ((fn,fd),fT) \\<in> set (fields (G,C))\\<rbrakk> \\<Longrightarrow> \
    5.34 -\ G\\<turnstile>Class C\\<preceq>Class fd";
    5.35 +\ G\\<turnstile>Class C\\<preceq> Class fd";
    5.36  by( datac widen_fields_defpl' 1 1);
    5.37  (*###################*)
    5.38  by( dtac bspec 1);
    5.39 @@ -227,7 +227,7 @@
    5.40  qed "rtranclD";
    5.41  
    5.42  Goal
    5.43 -"\\<lbrakk>wf_prog wf_mb G; G\\<turnstile>Class C'\\<preceq>Class C; map_of(fields (G,C )) f = Some ft\\<rbrakk> \\<Longrightarrow> \
    5.44 +"\\<lbrakk>wf_prog wf_mb G; G\\<turnstile>Class C'\\<preceq> Class C; map_of(fields (G,C )) f = Some ft\\<rbrakk> \\<Longrightarrow> \
    5.45  \                          map_of (fields (G,C')) f = Some ft";
    5.46  by( dtac widen_Class_Class 1);
    5.47  by( dtac rtranclD 1);
    5.48 @@ -246,11 +246,11 @@
    5.49  (K [rtac table_map_Some 1, Asm_full_simp_tac 1]);
    5.50  
    5.51  val widen_cfs_fields = prove_goal thy "\\<And>X. \\<lbrakk>field (G,C) fn = Some (fd, fT);\
    5.52 -\  G\\<turnstile>Class C'\\<preceq>Class C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> map_of (fields (G,C')) (fn, fd) = Some fT" (K[
    5.53 +\  G\\<turnstile>Class C'\\<preceq> Class C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> map_of (fields (G,C')) (fn, fd) = Some fT" (K[
    5.54  fast_tac (HOL_cs addIs [widen_fields_mono, cfs_fields_lemma]) 1]);
    5.55  
    5.56  Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,C) sig = Some (md,mh,m)\
    5.57 -\  \\<longrightarrow> G\\<turnstile>Class C\\<preceq>Class md \\<and> wf_mdecl wf_mb G md (sig,(mh,m))";
    5.58 +\  \\<longrightarrow> G\\<turnstile>Class C\\<preceq> Class md \\<and> wf_mdecl wf_mb G md (sig,(mh,m))";
    5.59  by( case_tac "is_class G C" 1);
    5.60  by(  forw_inst_tac [("C","C")] method_rec 2);
    5.61  by(    asm_full_simp_tac (simpset() addsimps [is_class_def] 
    5.62 @@ -278,7 +278,7 @@
    5.63  by( Asm_full_simp_tac 1);
    5.64  qed_spec_mp "method_wf_mdecl";
    5.65  
    5.66 -Goal "\\<lbrakk>G\\<turnstile>T\\<prec>C T'; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
    5.67 +Goal "\\<lbrakk>G\\<turnstile>T\\<preceq>C T'; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
    5.68  \  \\<forall>D rT b. method (G,T') sig = Some (D,rT ,b) \\<longrightarrow>\
    5.69  \ (\\<exists>D' rT' b'. method (G,T) sig = Some (D',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT)";
    5.70  by( dtac rtranclD 1);
    5.71 @@ -313,7 +313,7 @@
    5.72  
    5.73  
    5.74  Goal
    5.75 - "\\<lbrakk> G\\<turnstile>Class C\\<preceq>Class D; wf_prog wf_mb G; \
    5.76 + "\\<lbrakk> G\\<turnstile>Class C\\<preceq> Class D; wf_prog wf_mb G; \
    5.77  \    method (G,D) sig = Some (md, rT, b) \\<rbrakk> \
    5.78  \ \\<Longrightarrow> \\<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
    5.79  by(auto_tac (claset() addSDs [widen_Class_Class]
     6.1 --- a/src/HOL/MicroJava/J/WellForm.thy	Wed Jan 05 16:13:05 2000 +0100
     6.2 +++ b/src/HOL/MicroJava/J/WellForm.thy	Wed Jan 05 18:27:07 2000 +0100
     6.3 @@ -36,7 +36,7 @@
     6.4  	(\\<forall>m\\<in>set ms. wf_mdecl wf_mb G C m) \\<and>  unique ms \\<and>
     6.5  	(case sc of None \\<Rightarrow> C = Object
     6.6           | Some D \\<Rightarrow>
     6.7 -             is_class G D \\<and>  \\<not>  G\\<turnstile>D\\<prec>C C \\<and>
     6.8 +             is_class G D \\<and>  \\<not>  G\\<turnstile>D\\<preceq>C C \\<and>
     6.9               (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
    6.10                   method(G,D) sig = Some(D',rT',b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))"
    6.11  
     7.1 --- a/src/HOL/MicroJava/J/WellType.ML	Wed Jan 05 16:13:05 2000 +0100
     7.2 +++ b/src/HOL/MicroJava/J/WellType.ML	Wed Jan 05 18:27:07 2000 +0100
     7.3 @@ -5,7 +5,7 @@
     7.4  *)
     7.5  
     7.6  Goal
     7.7 -"\\<lbrakk> method (G,C) sig = Some (md,rT,b); wf_prog wf_mb G; G\\<turnstile>Class T''\\<preceq>Class C\\<rbrakk>\
     7.8 +"\\<lbrakk> method (G,C) sig = Some (md,rT,b); wf_prog wf_mb G; G\\<turnstile>Class T''\\<preceq> Class C\\<rbrakk>\
     7.9  \ \\<Longrightarrow> \\<exists>md' rT' b'. method (G,T'') sig = Some (md',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
    7.10  by( forward_tac [widen_Class_RefT] 1);
    7.11  by( etac exE 1);
    7.12 @@ -18,9 +18,9 @@
    7.13  
    7.14  
    7.15  Goal
    7.16 -"\\<lbrakk>method (G,C) sig = Some (md,rT,b); G\\<turnstile>Class T''\\<preceq>Class C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
    7.17 +"\\<lbrakk>method (G,C) sig = Some (md,rT,b); G\\<turnstile>Class T''\\<preceq> Class C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
    7.18  \ \\<exists>T' rT' b. method (G,T'') sig = Some (T',rT',b) \\<and> \
    7.19 -\ 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)";
    7.20 +\ 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)";
    7.21  by( datac widen_methd 2 1);
    7.22  by( Clarsimp_tac 1);
    7.23  by( dtac method_wf_mdecl 1);