corrected symbol for casting relation
authoroheimb
Wed Jul 05 10:28:29 2000 +0200 (2000-07-05)
changeset 924691423cd08c6f
parent 9245 428385c4bc50
child 9247 ad9f986616de
corrected symbol for casting relation
src/HOL/MicroJava/J/JTypeSafe.ML
src/HOL/MicroJava/J/TypeRel.ML
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/MicroJava/J/WellType.thy
     1.1 --- a/src/HOL/MicroJava/J/JTypeSafe.ML	Tue Jul 04 15:58:11 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.ML	Wed Jul 05 10:28:29 2000 +0200
     1.3 @@ -30,7 +30,7 @@
     1.4  qed "NewC_conforms";
     1.5  
     1.6  Goalw [cast_ok_def]
     1.7 - "\\<lbrakk> wf_prog wf_mb G; G,h\\<turnstile>v\\<Colon>\\<preceq>Tb; G\\<turnstile>Tb\\<Rightarrow>? T'; cast_ok G T' h v\\<rbrakk> \
     1.8 + "\\<lbrakk> wf_prog wf_mb G; G,h\\<turnstile>v\\<Colon>\\<preceq>Tb; G\\<turnstile>Tb\\<preceq>? T'; cast_ok G T' h v\\<rbrakk> \
     1.9  \ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T'";
    1.10  by( case_tac1 "v = Null" 1);
    1.11  by(  Asm_full_simp_tac 1);
     2.1 --- a/src/HOL/MicroJava/J/TypeRel.ML	Tue Jul 04 15:58:11 2000 +0200
     2.2 +++ b/src/HOL/MicroJava/J/TypeRel.ML	Wed Jul 05 10:28:29 2000 +0200
     2.3 @@ -117,14 +117,14 @@
     2.4  
     2.5  val prove_cast_lemma = prove_typerel_lemma [] cast.elim;
     2.6  
     2.7 -val cast_RefT = prove_typerel "G\\<turnstile>RefT R\\<Rightarrow>? T \\<Longrightarrow> \\<exists>t. T=RefT t" 
     2.8 +val cast_RefT = prove_typerel "G\\<turnstile>RefT R\\<preceq>? T \\<Longrightarrow> \\<exists>t. T=RefT t" 
     2.9  	[prove_typerel_lemma [widen_RefT] cast.elim 
    2.10 -	"G\\<turnstile>S\\<Rightarrow>? T \\<Longrightarrow> S=RefT R \\<longrightarrow> (\\<exists>t. T=RefT t)"];
    2.11 +	"G\\<turnstile>S\\<preceq>? T \\<Longrightarrow> S=RefT R \\<longrightarrow> (\\<exists>t. T=RefT t)"];
    2.12  
    2.13 -val cast_RefT2 = prove_typerel "G\\<turnstile>S\\<Rightarrow>? RefT R \\<Longrightarrow> \\<exists>t. S=RefT t" 
    2.14 +val cast_RefT2 = prove_typerel "G\\<turnstile>S\\<preceq>? RefT R \\<Longrightarrow> \\<exists>t. S=RefT t" 
    2.15  	[prove_typerel_lemma [widen_RefT2] cast.elim 
    2.16 -	"G\\<turnstile>S\\<Rightarrow>? T \\<Longrightarrow> T=RefT R \\<longrightarrow> (\\<exists>t. S=RefT t)"];
    2.17 +	"G\\<turnstile>S\\<preceq>? T \\<Longrightarrow> T=RefT R \\<longrightarrow> (\\<exists>t. S=RefT t)"];
    2.18  
    2.19 -val cast_PrimT2 = prove_typerel "G\\<turnstile>S\\<Rightarrow>? PrimT pt \\<Longrightarrow> G\\<turnstile>S\\<preceq>PrimT pt" 
    2.20 - [prove_cast_lemma "G\\<turnstile>S\\<Rightarrow>? T \\<Longrightarrow> T=PrimT pt \\<longrightarrow> G\\<turnstile>S\\<preceq>PrimT pt"];
    2.21 +val cast_PrimT2 = prove_typerel "G\\<turnstile>S\\<preceq>? PrimT pt \\<Longrightarrow> G\\<turnstile>S\\<preceq>PrimT pt" 
    2.22 + [prove_cast_lemma "G\\<turnstile>S\\<preceq>? T \\<Longrightarrow> T=PrimT pt \\<longrightarrow> G\\<turnstile>S\\<preceq>PrimT pt"];
    2.23  
     3.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Tue Jul 04 15:58:11 2000 +0200
     3.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Wed Jul 05 10:28:29 2000 +0200
     3.3 @@ -17,13 +17,13 @@
     3.4    subcls1	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<prec>C1_"	 [71,71,71] 70)
     3.5    subcls	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>C _"	 [71,71,71] 70)
     3.6    widen		:: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool"       ("_\\<turnstile>_\\<preceq>_"  [71,71,71] 70)
     3.7 -  cast		:: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool"       ("_\\<turnstile>_\\<Rightarrow>? _"[71,71,71] 70)
     3.8 +  cast		:: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool"       ("_\\<turnstile>_\\<preceq>? _"[71,71,71] 70)
     3.9  
    3.10  translations
    3.11    	"G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
    3.12  	"G\\<turnstile>C \\<preceq>C  D" == "(C,D) \\<in> (subcls1 G)^*"
    3.13  	"G\\<turnstile>S \\<preceq>   T" == "(S,T) \\<in> widen   G"
    3.14 -	"G\\<turnstile>S \\<Rightarrow>?  T" == "(S,T) \\<in> cast    G"
    3.15 +	"G\\<turnstile>S \\<preceq>?  T" == "(S,T) \\<in> cast    G"
    3.16  
    3.17  defs
    3.18  
    3.19 @@ -69,8 +69,8 @@
    3.20    subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class C \\<preceq> Class D"
    3.21    null	              "G\\<turnstile>     NT \\<preceq> RefT R"
    3.22  
    3.23 -inductive "cast G" intrs (* casting / narr.ref. conversion, cf. 5.5 / 5.1.5 *)
    3.24 -  widen	 "G\\<turnstile>S\\<preceq>T  \\<Longrightarrow> G\\<turnstile>      S \\<Rightarrow>? T"
    3.25 -  subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class D \\<Rightarrow>? Class C"
    3.26 +inductive "cast G" intrs (* casting conversion, cf. 5.5 / 5.1.5 *)
    3.27 +  widen	 "G\\<turnstile>S\\<preceq>T   \\<Longrightarrow> G\\<turnstile>      S \\<preceq>? T"
    3.28 +  subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class D \\<preceq>? Class C"
    3.29  
    3.30  end
     4.1 --- a/src/HOL/MicroJava/J/WellType.thy	Tue Jul 04 15:58:11 2000 +0200
     4.2 +++ b/src/HOL/MicroJava/J/WellType.thy	Wed Jul 05 10:28:29 2000 +0200
     4.3 @@ -96,7 +96,7 @@
     4.4  
     4.5    (* cf. 15.15 *)
     4.6    Cast	"\\<lbrakk>E\\<turnstile>e\\<Colon>T;
     4.7 -	  prg E\\<turnstile>T\\<Rightarrow>? T'\\<rbrakk> \\<Longrightarrow>
     4.8 +	  prg E\\<turnstile>T\\<preceq>? T'\\<rbrakk> \\<Longrightarrow>
     4.9  						 E\\<turnstile>Cast T' e\\<Colon>T'"
    4.10  
    4.11    (* cf. 15.7.1 *)