Theory Poly_Types

subsection "Type Variables"

theory Poly_Types imports Types begin

datatype ty = Ity | Rty | TV nat

text‹Everything else remains the same.›

type_synonym tyenv = "vname  ty"

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

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

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

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

definition styping :: "tyenv  state  bool" (infix "⊢p" 50)
where "Γ ⊢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 ⊢p a : t  tsubst S  E ⊢p a : tsubst S t"
apply(induction rule: atyping.induct)
apply(auto intro: atyping.intros)
done

lemma subst_btyping: "E ⊢p (b::bexp)  tsubst S  E ⊢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 ⊢p (c::com)  tsubst S  E ⊢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