Theory TypeRel
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