Theory TypeRel

(*  Title:       CoreC++

    Author:      Tobias Nipkow, Daniel Wasserrab 
    Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

    Extracted from the Jinja theory Common/TypeRel.thy by Tobias Nipkow 
*)

section ‹The subtype relation›

theory TypeRel imports SubObj begin


inductive
  widen   :: "prog  ty  ty  bool" ("_  _  _"   [71,71,71] 70)
  for P :: prog
where
  widen_refl[iff]: "P  T  T"
| widen_subcls:    "P  Path C to D unique  P  Class C  Class D"
| widen_null[iff]: "P  NT  Class C"

abbreviation
  widens :: "prog  ty list  ty list  bool"
    ("_  _ [≤] _" [71,71,71] 70) where
  "widens P Ts Ts'  list_all2 (widen P) Ts Ts'"

inductive_simps [iff]:
  "P  T  Void"
  "P  T  Boolean"
  "P  T  Integer"
  "P  Void  T"
  "P  Boolean  T"
  "P  Integer  T"
  "P  T  NT"

lemmas widens_refl [iff] = list_all2_refl [of "widen P", OF widen_refl] for P
lemmas widens_Cons [iff] = list_all2_Cons1 [of "widen P"] for P

end