src/HOL/MicroJava/J/TypeRel.thy
author nipkow
Thu, 11 Nov 1999 12:23:45 +0100
changeset 8011 d14c4e9e9c8e
child 8034 6fc37b5c5e98
permissions -rw-r--r--
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/MicroJava/J/TypeRel.thy
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     2
    ID:         $Id$
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     3
    Author:     David von Oheimb
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     4
    Copyright   1999 Technische Universitaet Muenchen
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     5
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     6
The relations between Java types
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     7
*)
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     8
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     9
TypeRel = Prog +
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    10
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    11
consts
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    12
  subcls1	:: "'c prog \\<Rightarrow> (cname \\<times> cname) set" (*        subclass *)
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    13
  widen,				 	    (*        widening *)
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    14
  cast		:: "'c prog \\<Rightarrow> (ty \\<times> ty) set"	    (*        casting *)
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    15
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    16
syntax
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    17
  subcls1	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<prec>C1_"	 [71,71,71] 70)
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    18
  subcls	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<prec>C _"	 [71,71,71] 70)
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    19
  widen		:: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool"       ("_\\<turnstile>_\\<preceq>_"  [71,71,71] 70)
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    20
  cast		:: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool"       ("_\\<turnstile>_\\<Rightarrow>? _"[71,71,71] 70)
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    21
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    22
translations
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    23
  	"G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    24
	"G\\<turnstile>C \\<prec>C  D" == "(C,D) \\<in> (subcls1 G)^+"
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    25
	"G\\<turnstile>S \\<preceq>   T" == "(S,T) \\<in> widen   G"
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    26
	"G\\<turnstile>S \\<Rightarrow>?  T" == "(S,T) \\<in> cast    G"
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    27
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    28
defs
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    29
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    30
  (* direct subclass, cf. 8.1.3 *)
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    31
  subcls1_def	"subcls1 G \\<equiv> {(C,D). \\<exists>c. class G C = Some c \\<and> fst c = Some D}"
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    32
  
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    33
consts
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    34
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    35
  cmethd	:: "'c prog \\<times> cname \\<Rightarrow> ( sig   \\<leadsto> cname \\<times> ty \\<times> 'c)"
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    36
  cfield	:: "'c prog \\<times> cname \\<Rightarrow> ( vname \\<leadsto> cname \\<times> ty)"
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    37
  fields	:: "'c prog \\<times> cname \\<Rightarrow> ((vname \\<times> cname) \\<times>  ty) list"
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    38
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    39
constdefs       (* auxiliary relations for recursive definitions below *)
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    40
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    41
  subcls1_rel	:: "(('c prog \\<times> cname) \\<times> ('c prog \\<times> cname)) set"
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    42
 "subcls1_rel \\<equiv> {((G,C),(G',C')). G = G' \\<and>  wf ((subcls1 G)^-1) \\<and>  G\\<turnstile>C'\\<prec>C1C}"
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    43
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    44
(* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *)
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    45
recdef cmethd "subcls1_rel"
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    46
 "cmethd (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None \\<Rightarrow> empty
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    47
                   | Some (sc,fs,ms) \\<Rightarrow> (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> 
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    48
                                           if is_class G D then cmethd (G,D) 
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    49
                                                           else arbitrary) \\<oplus>
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    50
                                           map_of (map (\\<lambda>(s,  m ). 
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    51
                                                        (s,(C,m))) ms))
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    52
                  else arbitrary)"
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    53
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    54
(* list of fields of a class, including inherited and hidden ones *)
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    55
recdef fields  "subcls1_rel"
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    56
 "fields (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None \\<Rightarrow> arbitrary
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    57
                   | Some (sc,fs,ms) \\<Rightarrow> map (\\<lambda>(fn,ft). ((fn,C),ft)) fs@
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    58
                                           (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow> 
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    59
                                           if is_class G D then fields (G,D) 
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    60
                                                           else arbitrary))
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    61
                  else arbitrary)"
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    62
defs
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    63
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    64
  cfield_def "cfield \\<equiv> map_of o (map (\\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    65
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    66
inductive "widen G" intrs (*widening, viz. method invocation conversion, cf. 5.3
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    67
			     i.e. sort of syntactic subtyping *)
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    68
  refl	              "G\\<turnstile>      T \\<preceq> T" 	 (* identity conv., cf. 5.1.1 *)
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    69
  subcls "G\\<turnstile>C\\<prec>C D \\<Longrightarrow> G\\<turnstile>Class C \\<preceq> Class D"
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    70
  null	              "G\\<turnstile>     NT \\<preceq> RefT R"
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    71
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    72
inductive "cast G" intrs (* casting / narr.ref. conversion, cf. 5.5 / 5.1.5 *)
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    73
  widen	 "G\\<turnstile>S\\<preceq>T  \\<Longrightarrow> G\\<turnstile>      S \\<Rightarrow>? T"
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    74
  subcls "G\\<turnstile>C\\<prec>C D \\<Longrightarrow> G\\<turnstile>Class D \\<Rightarrow>? Class C"
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    75
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    76
end