src/HOL/MicroJava/J/TypeRel.thy
author kleing
Fri Sep 22 16:28:53 2000 +0200 (2000-09-22)
changeset 10061 fe82134773dc
parent 10042 7164dc0d24d8
child 10138 412a3ced6efd
permissions -rw-r--r--
added HTML syntax; added spaces in normal syntax for better documents
     1 (*  Title:      HOL/MicroJava/J/TypeRel.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     Copyright   1999 Technische Universitaet Muenchen
     5 
     6 The relations between Java types
     7 *)
     8 
     9 TypeRel = Decl +
    10 
    11 consts
    12   subcls1 :: "'c prog => (cname \\<times> cname) set"  (* subclass *)
    13   widen   :: "'c prog => (ty    \\<times> ty   ) set"  (* widening *)
    14   cast    :: "'c prog => (cname \\<times> cname) set"  (* casting *)
    15 
    16 syntax
    17   subcls1 :: "'c prog => [cname, cname] => bool" ("_ \\<turnstile> _ \\<prec>C1 _" [71,71,71] 70)
    18   subcls  :: "'c prog => [cname, cname] => bool" ("_ \\<turnstile> _ \\<preceq>C _" [71,71,71] 70)
    19   widen   :: "'c prog => [ty   , ty   ] => bool" ("_ \\<turnstile> _ \\<preceq> _" [71,71,71] 70)
    20   cast    :: "'c prog => [cname, cname] => bool" ("_ \\<turnstile> _ \\<preceq>? _" [71,71,71] 70)
    21 
    22 syntax (HTML)
    23   subcls1 :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C1 _" [71,71,71] 70)
    24   subcls  :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C _" [71,71,71] 70)
    25   widen   :: "'c prog => [ty   , ty   ] => bool" ("_ |- _ <= _" [71,71,71] 70)
    26   cast    :: "'c prog => [cname, cname] => bool" ("_ |- _ <=? _" [71,71,71] 70)
    27 
    28 translations
    29   "G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
    30   "G\\<turnstile>C \\<preceq>C  D" == "(C,D) \\<in> (subcls1 G)^*"
    31   "G\\<turnstile>S \\<preceq>   T" == "(S,T) \\<in> widen   G"
    32   "G\\<turnstile>C \\<preceq>?  D" == "(C,D) \\<in> cast    G"
    33 
    34 defs
    35 
    36   (* direct subclass, cf. 8.1.3 *)
    37   subcls1_def	"subcls1 G == {(C,D). \\<exists>c. class G C = Some c \\<and> fst c = Some D}"
    38   
    39 consts
    40 
    41   method	:: "'c prog \\<times> cname => ( sig   \\<leadsto> cname \\<times> ty \\<times> 'c)"
    42   field	:: "'c prog \\<times> cname => ( vname \\<leadsto> cname \\<times> ty)"
    43   fields	:: "'c prog \\<times> cname => ((vname \\<times> cname) \\<times>  ty) list"
    44 
    45 constdefs       (* auxiliary relations for recursive definitions below *)
    46 
    47   subcls1_rel	:: "(('c prog \\<times> cname) \\<times> ('c prog \\<times> cname)) set"
    48  "subcls1_rel == {((G,C),(G',C')). G = G' \\<and>  wf ((subcls1 G)^-1) \\<and>  G\\<turnstile>C'\\<prec>C1C}"
    49 
    50 (* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *)
    51 recdef method "subcls1_rel"
    52  "method (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None => empty
    53                    | Some (sc,fs,ms) => (case sc of None => empty | Some D => 
    54                                            if is_class G D then method (G,D) 
    55                                                            else arbitrary) \\<oplus>
    56                                            map_of (map (\\<lambda>(s,  m ). 
    57                                                         (s,(C,m))) ms))
    58                   else arbitrary)"
    59 
    60 (* list of fields of a class, including inherited and hidden ones *)
    61 recdef fields  "subcls1_rel"
    62  "fields (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None => arbitrary
    63                    | Some (sc,fs,ms) => map (\\<lambda>(fn,ft). ((fn,C),ft)) fs@
    64                                            (case sc of None => [] | Some D => 
    65                                            if is_class G D then fields (G,D) 
    66                                                            else arbitrary))
    67                   else arbitrary)"
    68 defs
    69 
    70   field_def "field == map_of o (map (\\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
    71 
    72 inductive "widen G" intrs (*widening, viz. method invocation conversion, cf. 5.3
    73 			     i.e. sort of syntactic subtyping *)
    74   refl	             "G\\<turnstile>      T \\<preceq> T" 	 (* identity conv., cf. 5.1.1 *)
    75   subcls "G\\<turnstile>C\\<preceq>C D ==> G\\<turnstile>Class C \\<preceq> Class D"
    76   null	             "G\\<turnstile>     NT \\<preceq> RefT R"
    77 
    78 inductive "cast G" intrs (* casting conversion, cf. 5.5 / 5.1.5 *)
    79                          (* left out casts on primitve types    *)
    80   widen	 "G\\<turnstile>C\\<preceq>C D ==> G\\<turnstile>C \\<preceq>? D"
    81   subcls "G\\<turnstile>D\\<preceq>C C ==> G\\<turnstile>C \\<preceq>? D"
    82 
    83 end