src/HOL/MicroJava/J/TypeRel.thy
changeset 10042 7164dc0d24d8
parent 9348 f495dba0cb07
child 10061 fe82134773dc
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -9,15 +9,15 @@
     1.4  TypeRel = Decl +
     1.5  
     1.6  consts
     1.7 -  subcls1	:: "'c prog \\<Rightarrow> (cname \\<times> cname) set"  (* subclass *)
     1.8 -  widen 	:: "'c prog \\<Rightarrow> (ty    \\<times> ty   ) set"  (* widening *)
     1.9 -  cast		:: "'c prog \\<Rightarrow> (cname \\<times> cname) set"  (* casting *)
    1.10 +  subcls1	:: "'c prog => (cname \\<times> cname) set"  (* subclass *)
    1.11 +  widen 	:: "'c prog => (ty    \\<times> ty   ) set"  (* widening *)
    1.12 +  cast		:: "'c prog => (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> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>? _"[71,71,71] 70)
    1.19 +  subcls1	:: "'c prog => [cname, cname] => bool" ("_\\<turnstile>_\\<prec>C1_"	 [71,71,71] 70)
    1.20 +  subcls	:: "'c prog => [cname, cname] => bool" ("_\\<turnstile>_\\<preceq>C _"	 [71,71,71] 70)
    1.21 +  widen		:: "'c prog => [ty   , ty   ] => bool" ("_\\<turnstile>_\\<preceq>_"  [71,71,71] 70)
    1.22 +  cast		:: "'c prog => [cname, cname] => bool" ("_\\<turnstile>_\\<preceq>? _"[71,71,71] 70)
    1.23  
    1.24  translations
    1.25    	"G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
    1.26 @@ -28,23 +28,23 @@
    1.27  defs
    1.28  
    1.29    (* direct subclass, cf. 8.1.3 *)
    1.30 -  subcls1_def	"subcls1 G \\<equiv> {(C,D). \\<exists>c. class G C = Some c \\<and> fst c = Some D}"
    1.31 +  subcls1_def	"subcls1 G == {(C,D). \\<exists>c. class G C = Some c \\<and> fst c = Some D}"
    1.32    
    1.33  consts
    1.34  
    1.35 -  method	:: "'c prog \\<times> cname \\<Rightarrow> ( sig   \\<leadsto> cname \\<times> ty \\<times> 'c)"
    1.36 -  field	:: "'c prog \\<times> cname \\<Rightarrow> ( vname \\<leadsto> cname \\<times> ty)"
    1.37 -  fields	:: "'c prog \\<times> cname \\<Rightarrow> ((vname \\<times> cname) \\<times>  ty) list"
    1.38 +  method	:: "'c prog \\<times> cname => ( sig   \\<leadsto> cname \\<times> ty \\<times> 'c)"
    1.39 +  field	:: "'c prog \\<times> cname => ( vname \\<leadsto> cname \\<times> ty)"
    1.40 +  fields	:: "'c prog \\<times> cname => ((vname \\<times> cname) \\<times>  ty) list"
    1.41  
    1.42  constdefs       (* auxiliary relations for recursive definitions below *)
    1.43  
    1.44    subcls1_rel	:: "(('c prog \\<times> cname) \\<times> ('c prog \\<times> cname)) set"
    1.45 - "subcls1_rel \\<equiv> {((G,C),(G',C')). G = G' \\<and>  wf ((subcls1 G)^-1) \\<and>  G\\<turnstile>C'\\<prec>C1C}"
    1.46 + "subcls1_rel == {((G,C),(G',C')). G = G' \\<and>  wf ((subcls1 G)^-1) \\<and>  G\\<turnstile>C'\\<prec>C1C}"
    1.47  
    1.48  (* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *)
    1.49  recdef method "subcls1_rel"
    1.50 - "method (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None \\<Rightarrow> empty
    1.51 -                   | Some (sc,fs,ms) \\<Rightarrow> (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> 
    1.52 + "method (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None => empty
    1.53 +                   | Some (sc,fs,ms) => (case sc of None => empty | Some D => 
    1.54                                             if is_class G D then method (G,D) 
    1.55                                                             else arbitrary) \\<oplus>
    1.56                                             map_of (map (\\<lambda>(s,  m ). 
    1.57 @@ -53,25 +53,25 @@
    1.58  
    1.59  (* list of fields of a class, including inherited and hidden ones *)
    1.60  recdef fields  "subcls1_rel"
    1.61 - "fields (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None \\<Rightarrow> arbitrary
    1.62 -                   | Some (sc,fs,ms) \\<Rightarrow> map (\\<lambda>(fn,ft). ((fn,C),ft)) fs@
    1.63 -                                           (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow> 
    1.64 + "fields (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None => arbitrary
    1.65 +                   | Some (sc,fs,ms) => map (\\<lambda>(fn,ft). ((fn,C),ft)) fs@
    1.66 +                                           (case sc of None => [] | Some D => 
    1.67                                             if is_class G D then fields (G,D) 
    1.68                                                             else arbitrary))
    1.69                    else arbitrary)"
    1.70  defs
    1.71  
    1.72 -  field_def "field \\<equiv> map_of o (map (\\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
    1.73 +  field_def "field == map_of o (map (\\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
    1.74  
    1.75  inductive "widen G" intrs (*widening, viz. method invocation conversion, cf. 5.3
    1.76  			     i.e. sort of syntactic subtyping *)
    1.77    refl	             "G\\<turnstile>      T \\<preceq> T" 	 (* identity conv., cf. 5.1.1 *)
    1.78 -  subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class C \\<preceq> Class D"
    1.79 +  subcls "G\\<turnstile>C\\<preceq>C D ==> G\\<turnstile>Class C \\<preceq> Class D"
    1.80    null	             "G\\<turnstile>     NT \\<preceq> RefT R"
    1.81  
    1.82  inductive "cast G" intrs (* casting conversion, cf. 5.5 / 5.1.5 *)
    1.83                           (* left out casts on primitve types    *)
    1.84 -  widen	 "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>C \\<preceq>? D"
    1.85 -  subcls "G\\<turnstile>D\\<preceq>C C \\<Longrightarrow> G\\<turnstile>C \\<preceq>? D"
    1.86 +  widen	 "G\\<turnstile>C\\<preceq>C D ==> G\\<turnstile>C \\<preceq>? D"
    1.87 +  subcls "G\\<turnstile>D\\<preceq>C C ==> G\\<turnstile>C \\<preceq>? D"
    1.88  
    1.89  end