Theory Poly_Types

theory Poly_Types
imports Types
theory Poly_Types imports Types begin

subsection "Type Variables"

datatype ty = Ity | Rty | TV nat

text{* Everything else remains the same. *}

type_synonym tyenv = "vname => ty"

inductive atyping :: "tyenv => aexp => ty => bool"
  ("(1_/ \<turnstile>p/ (_ :/ _))" [50,0,50] 50)
where
"Γ \<turnstile>p Ic i : Ity" |
"Γ \<turnstile>p Rc r : Rty" |
"Γ \<turnstile>p V x : Γ x" |
"Γ \<turnstile>p a1 : τ ==> Γ \<turnstile>p a2 : τ ==> Γ \<turnstile>p Plus a1 a2 : τ"

inductive btyping :: "tyenv => bexp => bool" (infix "\<turnstile>p" 50)
where
"Γ \<turnstile>p Bc v" |
"Γ \<turnstile>p b ==> Γ \<turnstile>p Not b" |
"Γ \<turnstile>p b1 ==> Γ \<turnstile>p b2 ==> Γ \<turnstile>p And b1 b2" |
"Γ \<turnstile>p a1 : τ ==> Γ \<turnstile>p a2 : τ ==> Γ \<turnstile>p Less a1 a2"

inductive ctyping :: "tyenv => com => bool" (infix "\<turnstile>p" 50) where
"Γ \<turnstile>p SKIP" |
"Γ \<turnstile>p a : Γ(x) ==> Γ \<turnstile>p x ::= a" |
"Γ \<turnstile>p c1 ==> Γ \<turnstile>p c2 ==> Γ \<turnstile>p c1;;c2" |
"Γ \<turnstile>p b ==> Γ \<turnstile>p c1 ==> Γ \<turnstile>p c2 ==> Γ \<turnstile>p IF b THEN c1 ELSE c2" |
"Γ \<turnstile>p b ==> Γ \<turnstile>p c ==> Γ \<turnstile>p WHILE b DO c"

fun type :: "val => ty" where
"type (Iv i) = Ity" |
"type (Rv r) = Rty"

definition styping :: "tyenv => state => bool" (infix "\<turnstile>p" 50)
where "Γ \<turnstile>p s  <->  (∀x. type (s x) = Γ x)"

fun tsubst :: "(nat => ty) => ty => ty" where
"tsubst S (TV n) = S n" |
"tsubst S t = t"


subsection{* Typing is Preserved by Substitution *}

lemma subst_atyping: "E \<turnstile>p a : t ==> tsubst S o E \<turnstile>p a : tsubst S t"
apply(induction rule: atyping.induct)
apply(auto intro: atyping.intros)
done

lemma subst_btyping: "E \<turnstile>p (b::bexp) ==> tsubst S o E \<turnstile>p b"
apply(induction rule: btyping.induct)
apply(auto intro: btyping.intros)
apply(drule subst_atyping[where S=S])
apply(drule subst_atyping[where S=S])
apply(simp add: o_def btyping.intros)
done

lemma subst_ctyping: "E \<turnstile>p (c::com) ==> tsubst S o E \<turnstile>p c"
apply(induction rule: ctyping.induct)
apply(auto intro: ctyping.intros)
apply(drule subst_atyping[where S=S])
apply(simp add: o_def ctyping.intros)
apply(drule subst_btyping[where S=S])
apply(simp add: o_def ctyping.intros)
apply(drule subst_btyping[where S=S])
apply(simp add: o_def ctyping.intros)
done

end