src/HOL/MicroJava/J/TypeRel.thy
changeset 8011 d14c4e9e9c8e
child 8034 6fc37b5c5e98
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Thu Nov 11 12:23:45 1999 +0100
     1.3 @@ -0,0 +1,76 @@
     1.4 +(*  Title:      HOL/MicroJava/J/TypeRel.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     David von Oheimb
     1.7 +    Copyright   1999 Technische Universitaet Muenchen
     1.8 +
     1.9 +The relations between Java types
    1.10 +*)
    1.11 +
    1.12 +TypeRel = Prog +
    1.13 +
    1.14 +consts
    1.15 +  subcls1	:: "'c prog \\<Rightarrow> (cname \\<times> cname) set" (*        subclass *)
    1.16 +  widen,				 	    (*        widening *)
    1.17 +  cast		:: "'c prog \\<Rightarrow> (ty \\<times> ty) set"	    (*        casting *)
    1.18 +
    1.19 +syntax
    1.20 +  subcls1	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<prec>C1_"	 [71,71,71] 70)
    1.21 +  subcls	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<prec>C _"	 [71,71,71] 70)
    1.22 +  widen		:: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool"       ("_\\<turnstile>_\\<preceq>_"  [71,71,71] 70)
    1.23 +  cast		:: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool"       ("_\\<turnstile>_\\<Rightarrow>? _"[71,71,71] 70)
    1.24 +
    1.25 +translations
    1.26 +  	"G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
    1.27 +	"G\\<turnstile>C \\<prec>C  D" == "(C,D) \\<in> (subcls1 G)^+"
    1.28 +	"G\\<turnstile>S \\<preceq>   T" == "(S,T) \\<in> widen   G"
    1.29 +	"G\\<turnstile>S \\<Rightarrow>?  T" == "(S,T) \\<in> cast    G"
    1.30 +
    1.31 +defs
    1.32 +
    1.33 +  (* direct subclass, cf. 8.1.3 *)
    1.34 +  subcls1_def	"subcls1 G \\<equiv> {(C,D). \\<exists>c. class G C = Some c \\<and> fst c = Some D}"
    1.35 +  
    1.36 +consts
    1.37 +
    1.38 +  cmethd	:: "'c prog \\<times> cname \\<Rightarrow> ( sig   \\<leadsto> cname \\<times> ty \\<times> 'c)"
    1.39 +  cfield	:: "'c prog \\<times> cname \\<Rightarrow> ( vname \\<leadsto> cname \\<times> ty)"
    1.40 +  fields	:: "'c prog \\<times> cname \\<Rightarrow> ((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 +
    1.47 +(* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *)
    1.48 +recdef cmethd "subcls1_rel"
    1.49 + "cmethd (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None \\<Rightarrow> empty
    1.50 +                   | Some (sc,fs,ms) \\<Rightarrow> (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> 
    1.51 +                                           if is_class G D then cmethd (G,D) 
    1.52 +                                                           else arbitrary) \\<oplus>
    1.53 +                                           map_of (map (\\<lambda>(s,  m ). 
    1.54 +                                                        (s,(C,m))) ms))
    1.55 +                  else arbitrary)"
    1.56 +
    1.57 +(* list of fields of a class, including inherited and hidden ones *)
    1.58 +recdef fields  "subcls1_rel"
    1.59 + "fields (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None \\<Rightarrow> arbitrary
    1.60 +                   | Some (sc,fs,ms) \\<Rightarrow> map (\\<lambda>(fn,ft). ((fn,C),ft)) fs@
    1.61 +                                           (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow> 
    1.62 +                                           if is_class G D then fields (G,D) 
    1.63 +                                                           else arbitrary))
    1.64 +                  else arbitrary)"
    1.65 +defs
    1.66 +
    1.67 +  cfield_def "cfield \\<equiv> map_of o (map (\\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
    1.68 +
    1.69 +inductive "widen G" intrs (*widening, viz. method invocation conversion, cf. 5.3
    1.70 +			     i.e. sort of syntactic subtyping *)
    1.71 +  refl	              "G\\<turnstile>      T \\<preceq> T" 	 (* identity conv., cf. 5.1.1 *)
    1.72 +  subcls "G\\<turnstile>C\\<prec>C D \\<Longrightarrow> G\\<turnstile>Class C \\<preceq> Class D"
    1.73 +  null	              "G\\<turnstile>     NT \\<preceq> RefT R"
    1.74 +
    1.75 +inductive "cast G" intrs (* casting / narr.ref. conversion, cf. 5.5 / 5.1.5 *)
    1.76 +  widen	 "G\\<turnstile>S\\<preceq>T  \\<Longrightarrow> G\\<turnstile>      S \\<Rightarrow>? T"
    1.77 +  subcls "G\\<turnstile>C\\<prec>C D \\<Longrightarrow> G\\<turnstile>Class D \\<Rightarrow>? Class C"
    1.78 +
    1.79 +end