author | kleing |
Thu, 16 May 2013 13:49:18 +1000 | |
changeset 52021 | 59963cda805a |
parent 51513 | 7a2912282391 |
child 52046 | bc01725d7918 |
permissions | -rw-r--r-- |
43141 | 1 |
(* Author: Gerwin Klein, Tobias Nipkow *) |
2 |
||
3 |
theory Big_Step imports Com begin |
|
4 |
||
5 |
subsection "Big-Step Semantics of Commands" |
|
6 |
||
49191 | 7 |
text_raw{*\snip{BigStepdef}{0}{1}{% *} |
43141 | 8 |
inductive |
9 |
big_step :: "com \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55) |
|
10 |
where |
|
11 |
Skip: "(SKIP,s) \<Rightarrow> s" | |
|
12 |
Assign: "(x ::= a,s) \<Rightarrow> s(x := aval a s)" | |
|
47818 | 13 |
Seq: "\<lbrakk> (c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2; (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow> |
43141 | 14 |
(c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3" | |
15 |
||
16 |
IfTrue: "\<lbrakk> bval b s; (c\<^isub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> |
|
50054 | 17 |
(IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" | |
43141 | 18 |
IfFalse: "\<lbrakk> \<not>bval b s; (c\<^isub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> |
50054 | 19 |
(IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t" | |
43141 | 20 |
|
21 |
WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s" | |
|
22 |
WhileTrue: "\<lbrakk> bval b s\<^isub>1; (c,s\<^isub>1) \<Rightarrow> s\<^isub>2; (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3 \<rbrakk> \<Longrightarrow> |
|
50054 | 23 |
(WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
49191 | 24 |
text_raw{*}%endsnip*} |
43141 | 25 |
|
49191 | 26 |
text_raw{*\snip{BigStepEx}{1}{2}{% *} |
43141 | 27 |
schematic_lemma ex: "(''x'' ::= N 5; ''y'' ::= V ''x'', s) \<Rightarrow> ?t" |
47818 | 28 |
apply(rule Seq) |
43141 | 29 |
apply(rule Assign) |
30 |
apply simp |
|
31 |
apply(rule Assign) |
|
32 |
done |
|
49191 | 33 |
text_raw{*}%endsnip*} |
43141 | 34 |
|
35 |
thm ex[simplified] |
|
36 |
||
37 |
text{* We want to execute the big-step rules: *} |
|
38 |
||
39 |
code_pred big_step . |
|
40 |
||
41 |
text{* For inductive definitions we need command |
|
42 |
\texttt{values} instead of \texttt{value}. *} |
|
43 |
||
44923 | 44 |
values "{t. (SKIP, \<lambda>_. 0) \<Rightarrow> t}" |
43141 | 45 |
|
46 |
text{* We need to translate the result state into a list |
|
47 |
to display it. *} |
|
48 |
||
44036 | 49 |
values "{map t [''x''] |t. (SKIP, <''x'' := 42>) \<Rightarrow> t}" |
43141 | 50 |
|
44036 | 51 |
values "{map t [''x''] |t. (''x'' ::= N 2, <''x'' := 42>) \<Rightarrow> t}" |
43141 | 52 |
|
53 |
values "{map t [''x'',''y''] |t. |
|
54 |
(WHILE Less (V ''x'') (V ''y'') DO (''x'' ::= Plus (V ''x'') (N 5)), |
|
44036 | 55 |
<''x'' := 0, ''y'' := 13>) \<Rightarrow> t}" |
43141 | 56 |
|
57 |
||
58 |
text{* Proof automation: *} |
|
59 |
||
60 |
declare big_step.intros [intro] |
|
61 |
||
62 |
text{* The standard induction rule |
|
63 |
@{thm [display] big_step.induct [no_vars]} *} |
|
64 |
||
65 |
thm big_step.induct |
|
66 |
||
67 |
text{* A customized induction rule for (c,s) pairs: *} |
|
68 |
||
69 |
lemmas big_step_induct = big_step.induct[split_format(complete)] |
|
70 |
thm big_step_induct |
|
71 |
text {* |
|
72 |
@{thm [display] big_step_induct [no_vars]} |
|
73 |
*} |
|
74 |
||
75 |
||
76 |
subsection "Rule inversion" |
|
77 |
||
78 |
text{* What can we deduce from @{prop "(SKIP,s) \<Rightarrow> t"} ? |
|
79 |
That @{prop "s = t"}. This is how we can automatically prove it: *} |
|
80 |
||
51513 | 81 |
inductive_cases SkipE[elim!]: "(SKIP,s) \<Rightarrow> t" |
82 |
thm SkipE |
|
43141 | 83 |
|
84 |
text{* This is an \emph{elimination rule}. The [elim] attribute tells auto, |
|
85 |
blast and friends (but not simp!) to use it automatically; [elim!] means that |
|
86 |
it is applied eagerly. |
|
87 |
||
88 |
Similarly for the other commands: *} |
|
89 |
||
90 |
inductive_cases AssignE[elim!]: "(x ::= a,s) \<Rightarrow> t" |
|
91 |
thm AssignE |
|
47818 | 92 |
inductive_cases SeqE[elim!]: "(c1;c2,s1) \<Rightarrow> s3" |
93 |
thm SeqE |
|
43141 | 94 |
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<Rightarrow> t" |
95 |
thm IfE |
|
96 |
||
97 |
inductive_cases WhileE[elim]: "(WHILE b DO c,s) \<Rightarrow> t" |
|
98 |
thm WhileE |
|
99 |
text{* Only [elim]: [elim!] would not terminate. *} |
|
100 |
||
101 |
text{* An automatic example: *} |
|
102 |
||
103 |
lemma "(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> t \<Longrightarrow> t = s" |
|
104 |
by blast |
|
105 |
||
106 |
text{* Rule inversion by hand via the ``cases'' method: *} |
|
107 |
||
108 |
lemma assumes "(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> t" |
|
109 |
shows "t = s" |
|
110 |
proof- |
|
111 |
from assms show ?thesis |
|
112 |
proof cases --"inverting assms" |
|
113 |
case IfTrue thm IfTrue |
|
114 |
thus ?thesis by blast |
|
115 |
next |
|
116 |
case IfFalse thus ?thesis by blast |
|
117 |
qed |
|
118 |
qed |
|
119 |
||
44070 | 120 |
(* Using rule inversion to prove simplification rules: *) |
121 |
lemma assign_simp: |
|
122 |
"(x ::= a,s) \<Rightarrow> s' \<longleftrightarrow> (s' = s(x := aval a s))" |
|
123 |
by auto |
|
43141 | 124 |
|
125 |
subsection "Command Equivalence" |
|
126 |
||
127 |
text {* |
|
128 |
We call two statements @{text c} and @{text c'} equivalent wrt.\ the |
|
129 |
big-step semantics when \emph{@{text c} started in @{text s} terminates |
|
130 |
in @{text s'} iff @{text c'} started in the same @{text s} also terminates |
|
131 |
in the same @{text s'}}. Formally: |
|
132 |
*} |
|
49191 | 133 |
text_raw{*\snip{BigStepEquiv}{0}{1}{% *} |
43141 | 134 |
abbreviation |
135 |
equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" (infix "\<sim>" 50) where |
|
136 |
"c \<sim> c' == (\<forall>s t. (c,s) \<Rightarrow> t = (c',s) \<Rightarrow> t)" |
|
49191 | 137 |
text_raw{*}%endsnip*} |
43141 | 138 |
|
139 |
text {* |
|
140 |
Warning: @{text"\<sim>"} is the symbol written \verb!\ < s i m >! (without spaces). |
|
141 |
||
142 |
As an example, we show that loop unfolding is an equivalence |
|
143 |
transformation on programs: |
|
144 |
*} |
|
145 |
lemma unfold_while: |
|
146 |
"(WHILE b DO c) \<sim> (IF b THEN c; WHILE b DO c ELSE SKIP)" (is "?w \<sim> ?iw") |
|
147 |
proof - |
|
148 |
-- "to show the equivalence, we look at the derivation tree for" |
|
149 |
-- "each side and from that construct a derivation tree for the other side" |
|
150 |
{ fix s t assume "(?w, s) \<Rightarrow> t" |
|
151 |
-- "as a first thing we note that, if @{text b} is @{text False} in state @{text s}," |
|
152 |
-- "then both statements do nothing:" |
|
153 |
{ assume "\<not>bval b s" |
|
154 |
hence "t = s" using `(?w,s) \<Rightarrow> t` by blast |
|
155 |
hence "(?iw, s) \<Rightarrow> t" using `\<not>bval b s` by blast |
|
156 |
} |
|
157 |
moreover |
|
158 |
-- "on the other hand, if @{text b} is @{text True} in state @{text s}," |
|
159 |
-- {* then only the @{text WhileTrue} rule can have been used to derive @{text "(?w, s) \<Rightarrow> t"} *} |
|
160 |
{ assume "bval b s" |
|
161 |
with `(?w, s) \<Rightarrow> t` obtain s' where |
|
162 |
"(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto |
|
163 |
-- "now we can build a derivation tree for the @{text IF}" |
|
164 |
-- "first, the body of the True-branch:" |
|
47818 | 165 |
hence "(c; ?w, s) \<Rightarrow> t" by (rule Seq) |
43141 | 166 |
-- "then the whole @{text IF}" |
167 |
with `bval b s` have "(?iw, s) \<Rightarrow> t" by (rule IfTrue) |
|
168 |
} |
|
169 |
ultimately |
|
170 |
-- "both cases together give us what we want:" |
|
171 |
have "(?iw, s) \<Rightarrow> t" by blast |
|
172 |
} |
|
173 |
moreover |
|
174 |
-- "now the other direction:" |
|
175 |
{ fix s t assume "(?iw, s) \<Rightarrow> t" |
|
176 |
-- "again, if @{text b} is @{text False} in state @{text s}, then the False-branch" |
|
177 |
-- "of the @{text IF} is executed, and both statements do nothing:" |
|
178 |
{ assume "\<not>bval b s" |
|
179 |
hence "s = t" using `(?iw, s) \<Rightarrow> t` by blast |
|
180 |
hence "(?w, s) \<Rightarrow> t" using `\<not>bval b s` by blast |
|
181 |
} |
|
182 |
moreover |
|
183 |
-- "on the other hand, if @{text b} is @{text True} in state @{text s}," |
|
184 |
-- {* then this time only the @{text IfTrue} rule can have be used *} |
|
185 |
{ assume "bval b s" |
|
186 |
with `(?iw, s) \<Rightarrow> t` have "(c; ?w, s) \<Rightarrow> t" by auto |
|
47818 | 187 |
-- "and for this, only the Seq-rule is applicable:" |
43141 | 188 |
then obtain s' where |
189 |
"(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto |
|
190 |
-- "with this information, we can build a derivation tree for the @{text WHILE}" |
|
191 |
with `bval b s` |
|
192 |
have "(?w, s) \<Rightarrow> t" by (rule WhileTrue) |
|
193 |
} |
|
194 |
ultimately |
|
195 |
-- "both cases together again give us what we want:" |
|
196 |
have "(?w, s) \<Rightarrow> t" by blast |
|
197 |
} |
|
198 |
ultimately |
|
199 |
show ?thesis by blast |
|
200 |
qed |
|
201 |
||
202 |
text {* Luckily, such lengthy proofs are seldom necessary. Isabelle can |
|
203 |
prove many such facts automatically. *} |
|
204 |
||
45321 | 205 |
lemma while_unfold: |
43141 | 206 |
"(WHILE b DO c) \<sim> (IF b THEN c; WHILE b DO c ELSE SKIP)" |
207 |
by blast |
|
208 |
||
209 |
lemma triv_if: |
|
210 |
"(IF b THEN c ELSE c) \<sim> c" |
|
211 |
by blast |
|
212 |
||
213 |
lemma commute_if: |
|
214 |
"(IF b1 THEN (IF b2 THEN c11 ELSE c12) ELSE c2) |
|
215 |
\<sim> |
|
216 |
(IF b2 THEN (IF b1 THEN c11 ELSE c2) ELSE (IF b1 THEN c12 ELSE c2))" |
|
217 |
by blast |
|
218 |
||
51513 | 219 |
lemma sim_while_cong_aux: |
220 |
"(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> c \<sim> c' \<Longrightarrow> (WHILE b DO c',s) \<Rightarrow> t" |
|
221 |
apply(induction "WHILE b DO c" s t arbitrary: b c rule: big_step_induct) |
|
222 |
apply blast |
|
223 |
apply blast |
|
224 |
done |
|
225 |
||
226 |
lemma sim_while_cong: "c \<sim> c' \<Longrightarrow> WHILE b DO c \<sim> WHILE b DO c'" |
|
227 |
by (metis sim_while_cong_aux) |
|
228 |
||
52021
59963cda805a
explicitly state equivalence relation for sim; tweak syntax of sem_equiv
kleing
parents:
51513
diff
changeset
|
229 |
text {* Command equivalence is an equivalence relation, i.e.\ it is |
59963cda805a
explicitly state equivalence relation for sim; tweak syntax of sem_equiv
kleing
parents:
51513
diff
changeset
|
230 |
reflexive, symmetric, and transitive. Because we used an abbreviation |
59963cda805a
explicitly state equivalence relation for sim; tweak syntax of sem_equiv
kleing
parents:
51513
diff
changeset
|
231 |
above, Isabelle derives this automatically. *} |
59963cda805a
explicitly state equivalence relation for sim; tweak syntax of sem_equiv
kleing
parents:
51513
diff
changeset
|
232 |
|
59963cda805a
explicitly state equivalence relation for sim; tweak syntax of sem_equiv
kleing
parents:
51513
diff
changeset
|
233 |
lemma sim_refl: "c \<sim> c" by simp |
59963cda805a
explicitly state equivalence relation for sim; tweak syntax of sem_equiv
kleing
parents:
51513
diff
changeset
|
234 |
lemma sim_sym: "(c \<sim> c') = (c' \<sim> c)" by auto |
59963cda805a
explicitly state equivalence relation for sim; tweak syntax of sem_equiv
kleing
parents:
51513
diff
changeset
|
235 |
lemma sim_trans: "c \<sim> c' \<Longrightarrow> c' \<sim> c'' \<Longrightarrow> c \<sim> c''" by auto |
43141 | 236 |
|
237 |
subsection "Execution is deterministic" |
|
238 |
||
239 |
text {* This proof is automatic. *} |
|
49191 | 240 |
text_raw{*\snip{BigStepDeterministic}{0}{1}{% *} |
43141 | 241 |
theorem big_step_determ: "\<lbrakk> (c,s) \<Rightarrow> t; (c,s) \<Rightarrow> u \<rbrakk> \<Longrightarrow> u = t" |
45321 | 242 |
by (induction arbitrary: u rule: big_step.induct) blast+ |
49191 | 243 |
text_raw{*}%endsnip*} |
45321 | 244 |
|
43141 | 245 |
|
246 |
text {* |
|
247 |
This is the proof as you might present it in a lecture. The remaining |
|
248 |
cases are simple enough to be proved automatically: |
|
249 |
*} |
|
49191 | 250 |
text_raw{*\snip{BigStepDetLong}{0}{2}{% *} |
43141 | 251 |
theorem |
252 |
"(c,s) \<Rightarrow> t \<Longrightarrow> (c,s) \<Rightarrow> t' \<Longrightarrow> t' = t" |
|
45015 | 253 |
proof (induction arbitrary: t' rule: big_step.induct) |
43141 | 254 |
-- "the only interesting case, @{text WhileTrue}:" |
255 |
fix b c s s1 t t' |
|
256 |
-- "The assumptions of the rule:" |
|
257 |
assume "bval b s" and "(c,s) \<Rightarrow> s1" and "(WHILE b DO c,s1) \<Rightarrow> t" |
|
258 |
-- {* Ind.Hyp; note the @{text"\<And>"} because of arbitrary: *} |
|
259 |
assume IHc: "\<And>t'. (c,s) \<Rightarrow> t' \<Longrightarrow> t' = s1" |
|
260 |
assume IHw: "\<And>t'. (WHILE b DO c,s1) \<Rightarrow> t' \<Longrightarrow> t' = t" |
|
261 |
-- "Premise of implication:" |
|
262 |
assume "(WHILE b DO c,s) \<Rightarrow> t'" |
|
263 |
with `bval b s` obtain s1' where |
|
264 |
c: "(c,s) \<Rightarrow> s1'" and |
|
265 |
w: "(WHILE b DO c,s1') \<Rightarrow> t'" |
|
266 |
by auto |
|
267 |
from c IHc have "s1' = s1" by blast |
|
268 |
with w IHw show "t' = t" by blast |
|
269 |
qed blast+ -- "prove the rest automatically" |
|
49191 | 270 |
text_raw{*}%endsnip*} |
43141 | 271 |
|
272 |
end |