--- a/src/HOL/MicroJava/J/TypeRel.thy Fri Jul 14 17:49:56 2000 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy Fri Jul 14 20:47:11 2000 +0200
@@ -9,21 +9,21 @@
TypeRel = Decl +
consts
- subcls1 :: "'c prog \\<Rightarrow> (cname \\<times> cname) set" (* subclass *)
- widen, (* widening *)
- cast :: "'c prog \\<Rightarrow> (ty \\<times> ty) set" (* casting *)
+ subcls1 :: "'c prog \\<Rightarrow> (cname \\<times> cname) set" (* subclass *)
+ widen :: "'c prog \\<Rightarrow> (ty \\<times> ty ) set" (* widening *)
+ cast :: "'c prog \\<Rightarrow> (cname \\<times> cname) set" (* casting *)
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>_\\<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>_\\<preceq>? _"[71,71,71] 70)
+ widen :: "'c prog \\<Rightarrow> [ty , ty ] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>_" [71,71,71] 70)
+ cast :: "'c prog \\<Rightarrow> [cname, cname] \\<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 \\<preceq>? T" == "(S,T) \\<in> cast G"
+ "G\\<turnstile>C \\<preceq>? D" == "(C,D) \\<in> cast G"
defs
@@ -65,12 +65,13 @@
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 *)
+ refl "G\\<turnstile> T \\<preceq> T" (* identity conv., cf. 5.1.1 *)
subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class C \\<preceq> Class D"
- null "G\\<turnstile> NT \\<preceq> RefT R"
+ null "G\\<turnstile> NT \\<preceq> RefT R"
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"
+ (* left out casts on primitve types *)
+ widen "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>C \\<preceq>? D"
+ subcls "G\\<turnstile>D\\<preceq>C C \\<Longrightarrow> G\\<turnstile>C \\<preceq>? D"
end