Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
corrected symbol for casting relation
authoroheimb
Wed, 05 Jul 2000 10:28:29 +0200
changeset 9246 91423cd08c6f
parent 9245 428385c4bc50
child 9247 ad9f986616de
corrected symbol for casting relation
src/HOL/MicroJava/J/JTypeSafe.ML file | annotate | diff | comparison | revisions
src/HOL/MicroJava/J/TypeRel.ML file | annotate | diff | comparison | revisions
src/HOL/MicroJava/J/TypeRel.thy file | annotate | diff | comparison | revisions
src/HOL/MicroJava/J/WellType.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/MicroJava/J/JTypeSafe.ML	Tue Jul 04 15:58:11 2000 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.ML	Wed Jul 05 10:28:29 2000 +0200
@@ -30,7 +30,7 @@
 qed "NewC_conforms";
 
 Goalw [cast_ok_def]
- "\\<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> \
+ "\\<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> \
 \ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T'";
 by( case_tac1 "v = Null" 1);
 by(  Asm_full_simp_tac 1);
--- a/src/HOL/MicroJava/J/TypeRel.ML	Tue Jul 04 15:58:11 2000 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.ML	Wed Jul 05 10:28:29 2000 +0200
@@ -117,14 +117,14 @@
 
 val prove_cast_lemma = prove_typerel_lemma [] cast.elim;
 
-val cast_RefT = prove_typerel "G\\<turnstile>RefT R\\<Rightarrow>? T \\<Longrightarrow> \\<exists>t. T=RefT t" 
+val cast_RefT = prove_typerel "G\\<turnstile>RefT R\\<preceq>? T \\<Longrightarrow> \\<exists>t. T=RefT t" 
 	[prove_typerel_lemma [widen_RefT] cast.elim 
-	"G\\<turnstile>S\\<Rightarrow>? T \\<Longrightarrow> S=RefT R \\<longrightarrow> (\\<exists>t. T=RefT t)"];
+	"G\\<turnstile>S\\<preceq>? T \\<Longrightarrow> S=RefT R \\<longrightarrow> (\\<exists>t. T=RefT t)"];
 
-val cast_RefT2 = prove_typerel "G\\<turnstile>S\\<Rightarrow>? RefT R \\<Longrightarrow> \\<exists>t. S=RefT t" 
+val cast_RefT2 = prove_typerel "G\\<turnstile>S\\<preceq>? RefT R \\<Longrightarrow> \\<exists>t. S=RefT t" 
 	[prove_typerel_lemma [widen_RefT2] cast.elim 
-	"G\\<turnstile>S\\<Rightarrow>? T \\<Longrightarrow> T=RefT R \\<longrightarrow> (\\<exists>t. S=RefT t)"];
+	"G\\<turnstile>S\\<preceq>? T \\<Longrightarrow> T=RefT R \\<longrightarrow> (\\<exists>t. S=RefT t)"];
 
-val cast_PrimT2 = prove_typerel "G\\<turnstile>S\\<Rightarrow>? PrimT pt \\<Longrightarrow> G\\<turnstile>S\\<preceq>PrimT pt" 
- [prove_cast_lemma "G\\<turnstile>S\\<Rightarrow>? T \\<Longrightarrow> T=PrimT pt \\<longrightarrow> G\\<turnstile>S\\<preceq>PrimT pt"];
+val cast_PrimT2 = prove_typerel "G\\<turnstile>S\\<preceq>? PrimT pt \\<Longrightarrow> G\\<turnstile>S\\<preceq>PrimT pt" 
+ [prove_cast_lemma "G\\<turnstile>S\\<preceq>? T \\<Longrightarrow> T=PrimT pt \\<longrightarrow> G\\<turnstile>S\\<preceq>PrimT pt"];
 
--- a/src/HOL/MicroJava/J/TypeRel.thy	Tue Jul 04 15:58:11 2000 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Wed Jul 05 10:28:29 2000 +0200
@@ -17,13 +17,13 @@
   subcls1	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<prec>C1_"	 [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)
+  cast		:: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool"       ("_\\<turnstile>_\\<preceq>? _"[71,71,71] 70)
 
 translations
   	"G\\<turnstile>C \\<prec>C1 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"
+	"G\\<turnstile>S \\<preceq>?  T" == "(S,T) \\<in> cast    G"
 
 defs
 
@@ -69,8 +69,8 @@
   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\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class D \\<Rightarrow>? Class C"
+inductive "cast G" intrs (* casting conversion, cf. 5.5 / 5.1.5 *)
+  widen	 "G\\<turnstile>S\\<preceq>T   \\<Longrightarrow> G\\<turnstile>      S \\<preceq>? T"
+  subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class D \\<preceq>? Class C"
 
 end
--- a/src/HOL/MicroJava/J/WellType.thy	Tue Jul 04 15:58:11 2000 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy	Wed Jul 05 10:28:29 2000 +0200
@@ -96,7 +96,7 @@
 
   (* cf. 15.15 *)
   Cast	"\\<lbrakk>E\\<turnstile>e\\<Colon>T;
-	  prg E\\<turnstile>T\\<Rightarrow>? T'\\<rbrakk> \\<Longrightarrow>
+	  prg E\\<turnstile>T\\<preceq>? T'\\<rbrakk> \\<Longrightarrow>
 						 E\\<turnstile>Cast T' e\\<Colon>T'"
 
   (* cf. 15.7.1 *)
isabelle