43150
|
1 |
header "A Typed Language"
|
|
2 |
|
|
3 |
theory Types imports Star Complex_Main begin
|
|
4 |
|
|
5 |
subsection "Arithmetic Expressions"
|
|
6 |
|
|
7 |
datatype val = Iv int | Rv real
|
|
8 |
|
|
9 |
type_synonym name = string
|
|
10 |
type_synonym state = "name \<Rightarrow> val"
|
|
11 |
|
|
12 |
datatype aexp = Ic int | Rc real | V name | Plus aexp aexp
|
|
13 |
|
|
14 |
inductive taval :: "aexp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool" where
|
|
15 |
"taval (Ic i) s (Iv i)" |
|
|
16 |
"taval (Rc r) s (Rv r)" |
|
|
17 |
"taval (V x) s (s x)" |
|
|
18 |
"taval a1 s (Iv i1) \<Longrightarrow> taval a2 s (Iv i2)
|
|
19 |
\<Longrightarrow> taval (Plus a1 a2) s (Iv(i1+i2))" |
|
44020
|
20 |
"taval a1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2)
|
43150
|
21 |
\<Longrightarrow> taval (Plus a1 a2) s (Rv(r1+r2))"
|
|
22 |
|
|
23 |
inductive_cases [elim!]:
|
|
24 |
"taval (Ic i) s v" "taval (Rc i) s v"
|
|
25 |
"taval (V x) s v"
|
|
26 |
"taval (Plus a1 a2) s v"
|
|
27 |
|
|
28 |
subsection "Boolean Expressions"
|
|
29 |
|
|
30 |
datatype bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp
|
|
31 |
|
|
32 |
inductive tbval :: "bexp \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> bool" where
|
|
33 |
"tbval (B bv) s bv" |
|
|
34 |
"tbval b s bv \<Longrightarrow> tbval (Not b) s (\<not> bv)" |
|
44020
|
35 |
"tbval b1 s bv1 \<Longrightarrow> tbval b2 s bv2 \<Longrightarrow> tbval (And b1 b2) s (bv1 & bv2)" |
|
|
36 |
"taval a1 s (Iv i1) \<Longrightarrow> taval a2 s (Iv i2) \<Longrightarrow> tbval (Less a1 a2) s (i1 < i2)" |
|
|
37 |
"taval a1 s (Rv r1) \<Longrightarrow> taval a2 s (Rv r2) \<Longrightarrow> tbval (Less a1 a2) s (r1 < r2)"
|
43150
|
38 |
|
|
39 |
subsection "Syntax of Commands"
|
|
40 |
(* a copy of Com.thy - keep in sync! *)
|
|
41 |
|
|
42 |
datatype
|
|
43 |
com = SKIP
|
|
44 |
| Assign name aexp ("_ ::= _" [1000, 61] 61)
|
|
45 |
| Semi com com ("_; _" [60, 61] 60)
|
|
46 |
| If bexp com com ("IF _ THEN _ ELSE _" [0, 0, 61] 61)
|
|
47 |
| While bexp com ("WHILE _ DO _" [0, 61] 61)
|
|
48 |
|
|
49 |
|
|
50 |
subsection "Small-Step Semantics of Commands"
|
|
51 |
|
|
52 |
inductive
|
|
53 |
small_step :: "(com \<times> state) \<Rightarrow> (com \<times> state) \<Rightarrow> bool" (infix "\<rightarrow>" 55)
|
|
54 |
where
|
|
55 |
Assign: "taval a s v \<Longrightarrow> (x ::= a, s) \<rightarrow> (SKIP, s(x := v))" |
|
|
56 |
|
|
57 |
Semi1: "(SKIP;c,s) \<rightarrow> (c,s)" |
|
|
58 |
Semi2: "(c1,s) \<rightarrow> (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow> (c1';c2,s')" |
|
|
59 |
|
|
60 |
IfTrue: "tbval b s True \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c1,s)" |
|
|
61 |
IfFalse: "tbval b s False \<Longrightarrow> (IF b THEN c1 ELSE c2,s) \<rightarrow> (c2,s)" |
|
|
62 |
|
|
63 |
While: "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)"
|
|
64 |
|
|
65 |
lemmas small_step_induct = small_step.induct[split_format(complete)]
|
|
66 |
|
|
67 |
subsection "The Type System"
|
|
68 |
|
|
69 |
datatype ty = Ity | Rty
|
|
70 |
|
|
71 |
type_synonym tyenv = "name \<Rightarrow> ty"
|
|
72 |
|
|
73 |
inductive atyping :: "tyenv \<Rightarrow> aexp \<Rightarrow> ty \<Rightarrow> bool"
|
|
74 |
("(1_/ \<turnstile>/ (_ :/ _))" [50,0,50] 50)
|
|
75 |
where
|
|
76 |
Ic_ty: "\<Gamma> \<turnstile> Ic i : Ity" |
|
|
77 |
Rc_ty: "\<Gamma> \<turnstile> Rc r : Rty" |
|
|
78 |
V_ty: "\<Gamma> \<turnstile> V x : \<Gamma> x" |
|
|
79 |
Plus_ty: "\<Gamma> \<turnstile> a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> Plus a1 a2 : \<tau>"
|
|
80 |
|
|
81 |
text{* Warning: the ``:'' notation leads to syntactic ambiguities,
|
|
82 |
i.e. multiple parse trees, because ``:'' also stands for set membership.
|
|
83 |
In most situations Isabelle's type system will reject all but one parse tree,
|
|
84 |
but will still inform you of the potential ambiguity. *}
|
|
85 |
|
|
86 |
inductive btyping :: "tyenv \<Rightarrow> bexp \<Rightarrow> bool" (infix "\<turnstile>" 50)
|
|
87 |
where
|
|
88 |
B_ty: "\<Gamma> \<turnstile> B bv" |
|
|
89 |
Not_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> Not b" |
|
|
90 |
And_ty: "\<Gamma> \<turnstile> b1 \<Longrightarrow> \<Gamma> \<turnstile> b2 \<Longrightarrow> \<Gamma> \<turnstile> And b1 b2" |
|
|
91 |
Less_ty: "\<Gamma> \<turnstile> a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> Less a1 a2"
|
|
92 |
|
|
93 |
inductive ctyping :: "tyenv \<Rightarrow> com \<Rightarrow> bool" (infix "\<turnstile>" 50) where
|
|
94 |
Skip_ty: "\<Gamma> \<turnstile> SKIP" |
|
|
95 |
Assign_ty: "\<Gamma> \<turnstile> a : \<Gamma>(x) \<Longrightarrow> \<Gamma> \<turnstile> x ::= a" |
|
|
96 |
Semi_ty: "\<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> c1;c2" |
|
|
97 |
If_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c1 \<Longrightarrow> \<Gamma> \<turnstile> c2 \<Longrightarrow> \<Gamma> \<turnstile> IF b THEN c1 ELSE c2" |
|
|
98 |
While_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> WHILE b DO c"
|
|
99 |
|
|
100 |
inductive_cases [elim!]:
|
|
101 |
"\<Gamma> \<turnstile> x ::= a" "\<Gamma> \<turnstile> c1;c2"
|
|
102 |
"\<Gamma> \<turnstile> IF b THEN c1 ELSE c2"
|
|
103 |
"\<Gamma> \<turnstile> WHILE b DO c"
|
|
104 |
|
|
105 |
subsection "Well-typed Programs Do Not Get Stuck"
|
|
106 |
|
|
107 |
fun type :: "val \<Rightarrow> ty" where
|
|
108 |
"type (Iv i) = Ity" |
|
|
109 |
"type (Rv r) = Rty"
|
|
110 |
|
|
111 |
lemma [simp]: "type v = Ity \<longleftrightarrow> (\<exists>i. v = Iv i)"
|
|
112 |
by (cases v) simp_all
|
|
113 |
|
|
114 |
lemma [simp]: "type v = Rty \<longleftrightarrow> (\<exists>r. v = Rv r)"
|
|
115 |
by (cases v) simp_all
|
|
116 |
|
|
117 |
definition styping :: "tyenv \<Rightarrow> state \<Rightarrow> bool" (infix "\<turnstile>" 50)
|
|
118 |
where "\<Gamma> \<turnstile> s \<longleftrightarrow> (\<forall>x. type (s x) = \<Gamma> x)"
|
|
119 |
|
|
120 |
lemma apreservation:
|
|
121 |
"\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> taval a s v \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> type v = \<tau>"
|
|
122 |
apply(induct arbitrary: v rule: atyping.induct)
|
|
123 |
apply (fastsimp simp: styping_def)+
|
|
124 |
done
|
|
125 |
|
|
126 |
lemma aprogress: "\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. taval a s v"
|
|
127 |
proof(induct rule: atyping.induct)
|
|
128 |
case (Plus_ty \<Gamma> a1 t a2)
|
|
129 |
then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2" by blast
|
|
130 |
show ?case
|
|
131 |
proof (cases v1)
|
|
132 |
case Iv
|
|
133 |
with Plus_ty(1,3,5) v show ?thesis
|
|
134 |
by(fastsimp intro: taval.intros(4) dest!: apreservation)
|
|
135 |
next
|
|
136 |
case Rv
|
|
137 |
with Plus_ty(1,3,5) v show ?thesis
|
|
138 |
by(fastsimp intro: taval.intros(5) dest!: apreservation)
|
|
139 |
qed
|
|
140 |
qed (auto intro: taval.intros)
|
|
141 |
|
|
142 |
lemma bprogress: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. tbval b s v"
|
|
143 |
proof(induct rule: btyping.induct)
|
|
144 |
case (Less_ty \<Gamma> a1 t a2)
|
|
145 |
then obtain v1 v2 where v: "taval a1 s v1" "taval a2 s v2"
|
|
146 |
by (metis aprogress)
|
|
147 |
show ?case
|
|
148 |
proof (cases v1)
|
|
149 |
case Iv
|
|
150 |
with Less_ty v show ?thesis
|
|
151 |
by (fastsimp intro!: tbval.intros(4) dest!:apreservation)
|
|
152 |
next
|
|
153 |
case Rv
|
|
154 |
with Less_ty v show ?thesis
|
|
155 |
by (fastsimp intro!: tbval.intros(5) dest!:apreservation)
|
|
156 |
qed
|
|
157 |
qed (auto intro: tbval.intros)
|
|
158 |
|
|
159 |
theorem progress:
|
|
160 |
"\<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> \<exists>cs'. (c,s) \<rightarrow> cs'"
|
|
161 |
proof(induct rule: ctyping.induct)
|
|
162 |
case Skip_ty thus ?case by simp
|
|
163 |
next
|
|
164 |
case Assign_ty
|
|
165 |
thus ?case by (metis Assign aprogress)
|
|
166 |
next
|
|
167 |
case Semi_ty thus ?case by simp (metis Semi1 Semi2)
|
|
168 |
next
|
|
169 |
case (If_ty \<Gamma> b c1 c2)
|
|
170 |
then obtain bv where "tbval b s bv" by (metis bprogress)
|
|
171 |
show ?case
|
|
172 |
proof(cases bv)
|
|
173 |
assume "bv"
|
|
174 |
with `tbval b s bv` show ?case by simp (metis IfTrue)
|
|
175 |
next
|
|
176 |
assume "\<not>bv"
|
|
177 |
with `tbval b s bv` show ?case by simp (metis IfFalse)
|
|
178 |
qed
|
|
179 |
next
|
|
180 |
case While_ty show ?case by (metis While)
|
|
181 |
qed
|
|
182 |
|
|
183 |
theorem styping_preservation:
|
|
184 |
"(c,s) \<rightarrow> (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<Gamma> \<turnstile> s'"
|
|
185 |
proof(induct rule: small_step_induct)
|
|
186 |
case Assign thus ?case
|
|
187 |
by (auto simp: styping_def) (metis Assign(1,3) apreservation)
|
|
188 |
qed auto
|
|
189 |
|
|
190 |
theorem ctyping_preservation:
|
|
191 |
"(c,s) \<rightarrow> (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> c'"
|
|
192 |
by (induct rule: small_step_induct) (auto simp: ctyping.intros)
|
|
193 |
|
|
194 |
abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)
|
|
195 |
where "x \<rightarrow>* y == star small_step x y"
|
|
196 |
|
|
197 |
theorem type_sound:
|
|
198 |
"(c,s) \<rightarrow>* (c',s') \<Longrightarrow> \<Gamma> \<turnstile> c \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> c' \<noteq> SKIP
|
|
199 |
\<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"
|
|
200 |
apply(induct rule:star_induct)
|
|
201 |
apply (metis progress)
|
|
202 |
by (metis styping_preservation ctyping_preservation)
|
|
203 |
|
|
204 |
end
|