43150

1 
theory Poly_Types imports Types begin


2 


3 
subsection "Type Variables"


4 


5 
datatype ty = Ity  Rty  TV nat


6 


7 
text{* Everything else remains the same. *}


8 

45212

9 
type_synonym tyenv = "vname \<Rightarrow> ty"

43150

10 


11 
inductive atyping :: "tyenv \<Rightarrow> aexp \<Rightarrow> ty \<Rightarrow> bool"


12 
("(1_/ \<turnstile>p/ (_ :/ _))" [50,0,50] 50)


13 
where


14 
"\<Gamma> \<turnstile>p Ic i : Ity" 


15 
"\<Gamma> \<turnstile>p Rc r : Rty" 


16 
"\<Gamma> \<turnstile>p V x : \<Gamma> x" 


17 
"\<Gamma> \<turnstile>p a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile>p a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile>p Plus a1 a2 : \<tau>"


18 


19 
inductive btyping :: "tyenv \<Rightarrow> bexp \<Rightarrow> bool" (infix "\<turnstile>p" 50)


20 
where

45200

21 
"\<Gamma> \<turnstile>p Bc v" 

43150

22 
"\<Gamma> \<turnstile>p b \<Longrightarrow> \<Gamma> \<turnstile>p Not b" 


23 
"\<Gamma> \<turnstile>p b1 \<Longrightarrow> \<Gamma> \<turnstile>p b2 \<Longrightarrow> \<Gamma> \<turnstile>p And b1 b2" 


24 
"\<Gamma> \<turnstile>p a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile>p a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile>p Less a1 a2"


25 


26 
inductive ctyping :: "tyenv \<Rightarrow> com \<Rightarrow> bool" (infix "\<turnstile>p" 50) where


27 
"\<Gamma> \<turnstile>p SKIP" 


28 
"\<Gamma> \<turnstile>p a : \<Gamma>(x) \<Longrightarrow> \<Gamma> \<turnstile>p x ::= a" 


29 
"\<Gamma> \<turnstile>p c1 \<Longrightarrow> \<Gamma> \<turnstile>p c2 \<Longrightarrow> \<Gamma> \<turnstile>p c1;c2" 


30 
"\<Gamma> \<turnstile>p b \<Longrightarrow> \<Gamma> \<turnstile>p c1 \<Longrightarrow> \<Gamma> \<turnstile>p c2 \<Longrightarrow> \<Gamma> \<turnstile>p IF b THEN c1 ELSE c2" 


31 
"\<Gamma> \<turnstile>p b \<Longrightarrow> \<Gamma> \<turnstile>p c \<Longrightarrow> \<Gamma> \<turnstile>p WHILE b DO c"


32 


33 
fun type :: "val \<Rightarrow> ty" where


34 
"type (Iv i) = Ity" 


35 
"type (Rv r) = Rty"


36 


37 
definition styping :: "tyenv \<Rightarrow> state \<Rightarrow> bool" (infix "\<turnstile>p" 50)


38 
where "\<Gamma> \<turnstile>p s \<longleftrightarrow> (\<forall>x. type (s x) = \<Gamma> x)"


39 


40 
fun tsubst :: "(nat \<Rightarrow> ty) \<Rightarrow> ty \<Rightarrow> ty" where


41 
"tsubst S (TV n) = S n" 


42 
"tsubst S t = t"


43 


44 


45 
subsection{* Typing is Preserved by Substitution *}


46 


47 
lemma subst_atyping: "E \<turnstile>p a : t \<Longrightarrow> tsubst S \<circ> E \<turnstile>p a : tsubst S t"

45015

48 
apply(induction rule: atyping.induct)

43150

49 
apply(auto intro: atyping.intros)


50 
done


51 


52 
lemma subst_btyping: "E \<turnstile>p (b::bexp) \<Longrightarrow> tsubst S \<circ> E \<turnstile>p b"

45015

53 
apply(induction rule: btyping.induct)

43150

54 
apply(auto intro: btyping.intros)


55 
apply(drule subst_atyping[where S=S])


56 
apply(drule subst_atyping[where S=S])


57 
apply(simp add: o_def btyping.intros)


58 
done


59 


60 
lemma subst_ctyping: "E \<turnstile>p (c::com) \<Longrightarrow> tsubst S \<circ> E \<turnstile>p c"

45015

61 
apply(induction rule: ctyping.induct)

43150

62 
apply(auto intro: ctyping.intros)


63 
apply(drule subst_atyping[where S=S])


64 
apply(simp add: o_def ctyping.intros)


65 
apply(drule subst_btyping[where S=S])


66 
apply(simp add: o_def ctyping.intros)


67 
apply(drule subst_btyping[where S=S])


68 
apply(simp add: o_def ctyping.intros)


69 
done


70 


71 
end
