author | haftmann |
Fri, 01 Nov 2013 18:51:14 +0100 | |
changeset 54230 | b1d955791529 |
parent 52046 | bc01725d7918 |
child 58249 | 180f1b3508ed |
permissions | -rw-r--r-- |
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" | |
|
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
45212
diff
changeset
|
29 |
"\<Gamma> \<turnstile>p c1 \<Longrightarrow> \<Gamma> \<turnstile>p c2 \<Longrightarrow> \<Gamma> \<turnstile>p c1;;c2" | |
43150 | 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 |