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