Theory TypeRel

Up to index of Isabelle/HOL/MicroJava

(*  Title:      HOL/MicroJava/J/TypeRel.thy
    ID:         $Id: TypeRel.thy,v 1.10 2000/10/03 16:44:19 wenzelm Exp $
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen

The relations between Java types
*)

TypeRel = Decl +

consts
  subcls1 :: "'c prog => (cname × cname) set"  (* subclass *)
  widen   :: "'c prog => (ty    × ty   ) set"  (* widening *)
  cast    :: "'c prog => (cname × cname) set"  (* casting *)

syntax
  subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70)
  subcls  :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _" [71,71,71] 70)
  widen   :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq> _" [71,71,71] 70)
  cast    :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>? _" [71,71,71] 70)

syntax (HTML)
  subcls1 :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C1 _" [71,71,71] 70)
  subcls  :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C _" [71,71,71] 70)
  widen   :: "'c prog => [ty   , ty   ] => bool" ("_ |- _ <= _" [71,71,71] 70)
  cast    :: "'c prog => [cname, cname] => bool" ("_ |- _ <=? _" [71,71,71] 70)

translations
  "G\<turnstile>C \<prec>C1 D" == "(C,D) \<in> subcls1 G"
  "G\<turnstile>C \<preceq>C  D" == "(C,D) \<in> (subcls1 G)^*"
  "G\<turnstile>S \<preceq>   T" == "(S,T) \<in> widen   G"
  "G\<turnstile>C \<preceq>?  D" == "(C,D) \<in> cast    G"

defs

  (* direct subclass, cf. 8.1.3 *)
  subcls1_def   "subcls1 G == {(C,D). \<exists>c. class G C = Some c \<and> fst c = Some D}"
  
consts

  method        :: "'c prog × cname => ( sig   \<leadsto> cname × ty × 'c)"
  field :: "'c prog × cname => ( vname \<leadsto> cname × ty)"
  fields        :: "'c prog × cname => ((vname × cname) ×  ty) list"

constdefs       (* auxiliary relations for recursive definitions below *)

  subcls1_rel   :: "(('c prog × cname) × ('c prog × cname)) set"
 "subcls1_rel == {((G,C),(G',C')). G = G' \<and>  wf ((subcls1 G)^-1) \<and>  G\<turnstile>C'\<prec>C1C}"

(* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *)
recdef method "subcls1_rel"
 "method (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None => empty
                   | Some (sc,fs,ms) => (case sc of None => empty | Some D => 
                                           if is_class G D then method (G,D) 
                                                           else arbitrary) ++
                                           map_of (map (\<lambda>(s,  m ). 
                                                        (s,(C,m))) ms))
                  else arbitrary)"

(* list of fields of a class, including inherited and hidden ones *)
recdef fields  "subcls1_rel"
 "fields (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None => arbitrary
                   | Some (sc,fs,ms) => map (\<lambda>(fn,ft). ((fn,C),ft)) fs@
                                           (case sc of None => [] | Some D => 
                                           if is_class G D then fields (G,D) 
                                                           else arbitrary))
                  else arbitrary)"
defs

  field_def "field == map_of o (map (\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"

inductive "widen G" intrs (*widening, viz. method invocation conversion, cf. 5.3
                             i.e. sort of syntactic subtyping *)
  refl               "G\<turnstile>      T \<preceq> T"        (* identity conv., cf. 5.1.1 *)
  subcls "G\<turnstile>C\<preceq>C D ==> G\<turnstile>Class C \<preceq> Class D"
  null               "G\<turnstile>     NT \<preceq> RefT R"

inductive "cast G" intrs (* casting conversion, cf. 5.5 / 5.1.5 *)
                         (* left out casts on primitve types    *)
  widen  "G\<turnstile>C\<preceq>C D ==> G\<turnstile>C \<preceq>? D"
  subcls "G\<turnstile>D\<preceq>C C ==> G\<turnstile>C \<preceq>? D"

end

theorem finite_subcls1:

  finite (subcls1 G)

theorem subcls_is_class:

  (C, D) : (subcls1 G)^+ ==> is_class G C

theorem wf_rel_lemma:

  wf {((A, x), B, y). A = B & wf (R A) & (x, y) : R A}

theorem wf_subcls1_rel:

  wf subcls1_rel

theorem widen_PrimT_RefT:

  G |- PrimT pT <= RefT rT = False

theorem widen_RefT:

  G |- RefT R <= T ==> EX t. T = RefT t

theorem widen_RefT2:

  G |- S <= RefT R ==> EX t. S = RefT t

theorem widen_Class:

  G |- Class C <= T ==> EX D. T = Class D

theorem widen_Class_NullT:

  G |- Class C <= NT = False

theorem widen_Class_Class:

  G |- Class C <= Class D = G |- C <=C D

theorem widen_trans:

  [| G |- S <= U; G |- U <= T |] ==> G |- S <= T