src/HOL/MicroJava/J/TypeRel.thy
changeset 9348 f495dba0cb07
parent 9346 297dcbf64526
child 10042 7164dc0d24d8
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Fri Jul 14 17:49:56 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Fri Jul 14 20:47:11 2000 +0200
     1.3 @@ -9,21 +9,21 @@
     1.4  TypeRel = Decl +
     1.5  
     1.6  consts
     1.7 -  subcls1	:: "'c prog \\<Rightarrow> (cname \\<times> cname) set" (*        subclass *)
     1.8 -  widen,				 	    (*        widening *)
     1.9 -  cast		:: "'c prog \\<Rightarrow> (ty \\<times> ty) set"	    (*        casting *)
    1.10 +  subcls1	:: "'c prog \\<Rightarrow> (cname \\<times> cname) set"  (* subclass *)
    1.11 +  widen 	:: "'c prog \\<Rightarrow> (ty    \\<times> ty   ) set"  (* widening *)
    1.12 +  cast		:: "'c prog \\<Rightarrow> (cname \\<times> cname) set"  (* casting *)
    1.13  
    1.14  syntax
    1.15    subcls1	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<prec>C1_"	 [71,71,71] 70)
    1.16    subcls	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>C _"	 [71,71,71] 70)
    1.17 -  widen		:: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool"       ("_\\<turnstile>_\\<preceq>_"  [71,71,71] 70)
    1.18 -  cast		:: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool"       ("_\\<turnstile>_\\<preceq>? _"[71,71,71] 70)
    1.19 +  widen		:: "'c prog \\<Rightarrow> [ty   , ty   ] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>_"  [71,71,71] 70)
    1.20 +  cast		:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>? _"[71,71,71] 70)
    1.21  
    1.22  translations
    1.23    	"G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
    1.24  	"G\\<turnstile>C \\<preceq>C  D" == "(C,D) \\<in> (subcls1 G)^*"
    1.25  	"G\\<turnstile>S \\<preceq>   T" == "(S,T) \\<in> widen   G"
    1.26 -	"G\\<turnstile>S \\<preceq>?  T" == "(S,T) \\<in> cast    G"
    1.27 +	"G\\<turnstile>C \\<preceq>?  D" == "(C,D) \\<in> cast    G"
    1.28  
    1.29  defs
    1.30  
    1.31 @@ -65,12 +65,13 @@
    1.32  
    1.33  inductive "widen G" intrs (*widening, viz. method invocation conversion, cf. 5.3
    1.34  			     i.e. sort of syntactic subtyping *)
    1.35 -  refl	              "G\\<turnstile>      T \\<preceq> T" 	 (* identity conv., cf. 5.1.1 *)
    1.36 +  refl	             "G\\<turnstile>      T \\<preceq> T" 	 (* identity conv., cf. 5.1.1 *)
    1.37    subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class C \\<preceq> Class D"
    1.38 -  null	              "G\\<turnstile>     NT \\<preceq> RefT R"
    1.39 +  null	             "G\\<turnstile>     NT \\<preceq> RefT R"
    1.40  
    1.41  inductive "cast G" intrs (* casting conversion, cf. 5.5 / 5.1.5 *)
    1.42 -  widen	 "G\\<turnstile>S\\<preceq>T   \\<Longrightarrow> G\\<turnstile>      S \\<preceq>? T"
    1.43 -  subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class D \\<preceq>? Class C"
    1.44 +                         (* left out casts on primitve types    *)
    1.45 +  widen	 "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>C \\<preceq>? D"
    1.46 +  subcls "G\\<turnstile>D\\<preceq>C C \\<Longrightarrow> G\\<turnstile>C \\<preceq>? D"
    1.47  
    1.48  end