Theory TypeRel

(*  Title:       CoreC++
    ID:          $Id: TypeRel.thy,v 1.10 2007-07-11 10:07:49 stefanberghofer Exp $
    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 
*)


header {* \isaheader{The subtype relation} *}

theory TypeRel imports SubObj begin


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

abbreviation (xsymbols)
  widens :: "prog => ty list => ty list => bool"
    ("_ \<turnstile> _ [≤] _" [71,71,71] 70) where
  "widens P Ts Ts' ≡ list_all2 (widen P) Ts Ts'"

lemma [iff]: "(P \<turnstile> T ≤ Void) = (T = Void)"
by (auto elim: widen.cases)

lemma [iff]: "(P \<turnstile> T ≤ Boolean) = (T = Boolean)"
by (auto elim: widen.cases)

lemma [iff]: "(P \<turnstile> T ≤ Integer) = (T = Integer)"
by (auto elim: widen.cases)

lemma [iff]: "(P \<turnstile> Void ≤ T) = (T = Void)"
by (auto elim: widen.cases)

lemma [iff]: "(P \<turnstile> Boolean ≤ T) = (T = Boolean)"
by (auto elim: widen.cases)

lemma [iff]: "(P \<turnstile> Integer ≤ T) = (T = Integer)"
by (auto elim: widen.cases)


lemma [iff]: "(P \<turnstile> T ≤ NT) = (T = NT)"

apply(cases T) apply auto
apply (ind_cases "P \<turnstile> T ≤ NT" for T)
apply auto
done


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

end