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 |
|
|
9 |
type_synonym tyenv = "name \<Rightarrow> ty"
|
|
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
|
|
21 |
"\<Gamma> \<turnstile>p B bv" |
|
|
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
|