|
1 header "Small-Step Semantics of Commands" |
|
2 |
|
3 theory Small_Step imports Star Big_Step begin |
|
4 |
|
5 subsection "The transition relation" |
|
6 |
|
7 inductive |
|
8 small_step :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>" 55) |
|
9 where |
|
10 Assign: "(x ::= a, s) \<rightarrow> (SKIP, s(x := aval a s))" | |
|
11 |
|
12 Semi1: "(SKIP;c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" | |
|
13 Semi2: "(c\<^isub>1,s) \<rightarrow> (c\<^isub>1',s') \<Longrightarrow> (c\<^isub>1;c\<^isub>2,s) \<rightarrow> (c\<^isub>1';c\<^isub>2,s')" | |
|
14 |
|
15 IfTrue: "bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>1,s)" | |
|
16 IfFalse: "\<not>bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" | |
|
17 |
|
18 While: "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)" |
|
19 |
|
20 |
|
21 abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55) |
|
22 where "x \<rightarrow>* y == star small_step x y" |
|
23 |
|
24 subsection{* Executability *} |
|
25 |
|
26 code_pred small_step . |
|
27 |
|
28 values "{(c',map t [''x'',''y'',''z'']) |c' t. |
|
29 (''x'' ::= V ''z''; ''y'' ::= V ''x'', |
|
30 lookup[(''x'',3),(''y'',7),(''z'',5)]) \<rightarrow>* (c',t)}" |
|
31 |
|
32 |
|
33 subsection{* Proof infrastructure *} |
|
34 |
|
35 subsubsection{* Induction rules *} |
|
36 |
|
37 text{* The default induction rule @{thm[source] small_step.induct} only works |
|
38 for lemmas of the form @{text"a \<rightarrow> b \<Longrightarrow> \<dots>"} where @{text a} and @{text b} are |
|
39 not already pairs @{text"(DUMMY,DUMMY)"}. We can generate a suitable variant |
|
40 of @{thm[source] small_step.induct} for pairs by ``splitting'' the arguments |
|
41 @{text"\<rightarrow>"} into pairs: *} |
|
42 lemmas small_step_induct = small_step.induct[split_format(complete)] |
|
43 |
|
44 |
|
45 subsubsection{* Proof automation *} |
|
46 |
|
47 declare small_step.intros[simp,intro] |
|
48 |
|
49 text{* So called transitivity rules. See below. *} |
|
50 |
|
51 declare step[trans] step1[trans] |
|
52 |
|
53 lemma step2[trans]: |
|
54 "cs \<rightarrow> cs' \<Longrightarrow> cs' \<rightarrow> cs'' \<Longrightarrow> cs \<rightarrow>* cs''" |
|
55 by(metis refl step) |
|
56 |
|
57 declare star_trans[trans] |
|
58 |
|
59 text{* Rule inversion: *} |
|
60 |
|
61 inductive_cases SkipE[elim!]: "(SKIP,s) \<rightarrow> ct" |
|
62 thm SkipE |
|
63 inductive_cases AssignE[elim!]: "(x::=a,s) \<rightarrow> ct" |
|
64 thm AssignE |
|
65 inductive_cases SemiE[elim]: "(c1;c2,s) \<rightarrow> ct" |
|
66 thm SemiE |
|
67 inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<rightarrow> ct" |
|
68 inductive_cases WhileE[elim]: "(WHILE b DO c, s) \<rightarrow> ct" |
|
69 |
|
70 |
|
71 text{* A simple property: *} |
|
72 lemma deterministic: |
|
73 "cs \<rightarrow> cs' \<Longrightarrow> cs \<rightarrow> cs'' \<Longrightarrow> cs'' = cs'" |
|
74 apply(induct arbitrary: cs'' rule: small_step.induct) |
|
75 apply blast+ |
|
76 done |
|
77 |
|
78 |
|
79 subsection "Equivalence with big-step semantics" |
|
80 |
|
81 lemma star_semi2: "(c1,s) \<rightarrow>* (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow>* (c1';c2,s')" |
|
82 proof(induct rule: star_induct) |
|
83 case refl thus ?case by simp |
|
84 next |
|
85 case step |
|
86 thus ?case by (metis Semi2 star.step) |
|
87 qed |
|
88 |
|
89 lemma semi_comp: |
|
90 "\<lbrakk> (c1,s1) \<rightarrow>* (SKIP,s2); (c2,s2) \<rightarrow>* (SKIP,s3) \<rbrakk> |
|
91 \<Longrightarrow> (c1;c2, s1) \<rightarrow>* (SKIP,s3)" |
|
92 by(blast intro: star.step star_semi2 star_trans) |
|
93 |
|
94 text{* The following proof corresponds to one on the board where one would |
|
95 show chains of @{text "\<rightarrow>"} and @{text "\<rightarrow>*"} steps. This is what the |
|
96 also/finally proof steps do: they compose chains, implicitly using the rules |
|
97 declared with attribute [trans] above. *} |
|
98 |
|
99 lemma big_to_small: |
|
100 "cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)" |
|
101 proof (induct rule: big_step.induct) |
|
102 fix s show "(SKIP,s) \<rightarrow>* (SKIP,s)" by simp |
|
103 next |
|
104 fix x a s show "(x ::= a,s) \<rightarrow>* (SKIP, s(x := aval a s))" by auto |
|
105 next |
|
106 fix c1 c2 s1 s2 s3 |
|
107 assume "(c1,s1) \<rightarrow>* (SKIP,s2)" and "(c2,s2) \<rightarrow>* (SKIP,s3)" |
|
108 thus "(c1;c2, s1) \<rightarrow>* (SKIP,s3)" by (rule semi_comp) |
|
109 next |
|
110 fix s::state and b c0 c1 t |
|
111 assume "bval b s" |
|
112 hence "(IF b THEN c0 ELSE c1,s) \<rightarrow> (c0,s)" by simp |
|
113 also assume "(c0,s) \<rightarrow>* (SKIP,t)" |
|
114 finally show "(IF b THEN c0 ELSE c1,s) \<rightarrow>* (SKIP,t)" . --"= by assumption" |
|
115 next |
|
116 fix s::state and b c0 c1 t |
|
117 assume "\<not>bval b s" |
|
118 hence "(IF b THEN c0 ELSE c1,s) \<rightarrow> (c1,s)" by simp |
|
119 also assume "(c1,s) \<rightarrow>* (SKIP,t)" |
|
120 finally show "(IF b THEN c0 ELSE c1,s) \<rightarrow>* (SKIP,t)" . |
|
121 next |
|
122 fix b c and s::state |
|
123 assume b: "\<not>bval b s" |
|
124 let ?if = "IF b THEN c; WHILE b DO c ELSE SKIP" |
|
125 have "(WHILE b DO c,s) \<rightarrow> (?if, s)" by blast |
|
126 also have "(?if,s) \<rightarrow> (SKIP, s)" by (simp add: b) |
|
127 finally show "(WHILE b DO c,s) \<rightarrow>* (SKIP,s)" by auto |
|
128 next |
|
129 fix b c s s' t |
|
130 let ?w = "WHILE b DO c" |
|
131 let ?if = "IF b THEN c; ?w ELSE SKIP" |
|
132 assume w: "(?w,s') \<rightarrow>* (SKIP,t)" |
|
133 assume c: "(c,s) \<rightarrow>* (SKIP,s')" |
|
134 assume b: "bval b s" |
|
135 have "(?w,s) \<rightarrow> (?if, s)" by blast |
|
136 also have "(?if, s) \<rightarrow> (c; ?w, s)" by (simp add: b) |
|
137 also have "(c; ?w,s) \<rightarrow>* (SKIP,t)" by(rule semi_comp[OF c w]) |
|
138 finally show "(WHILE b DO c,s) \<rightarrow>* (SKIP,t)" by auto |
|
139 qed |
|
140 |
|
141 text{* Each case of the induction can be proved automatically: *} |
|
142 lemma "cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)" |
|
143 proof (induct rule: big_step.induct) |
|
144 case Skip show ?case by blast |
|
145 next |
|
146 case Assign show ?case by blast |
|
147 next |
|
148 case Semi thus ?case by (blast intro: semi_comp) |
|
149 next |
|
150 case IfTrue thus ?case by (blast intro: step) |
|
151 next |
|
152 case IfFalse thus ?case by (blast intro: step) |
|
153 next |
|
154 case WhileFalse thus ?case |
|
155 by (metis step step1 small_step.IfFalse small_step.While) |
|
156 next |
|
157 case WhileTrue |
|
158 thus ?case |
|
159 by(metis While semi_comp small_step.IfTrue step[of small_step]) |
|
160 qed |
|
161 |
|
162 lemma small1_big_continue: |
|
163 "cs \<rightarrow> cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t" |
|
164 apply (induct arbitrary: t rule: small_step.induct) |
|
165 apply auto |
|
166 done |
|
167 |
|
168 lemma small_big_continue: |
|
169 "cs \<rightarrow>* cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t" |
|
170 apply (induct rule: star.induct) |
|
171 apply (auto intro: small1_big_continue) |
|
172 done |
|
173 |
|
174 lemma small_to_big: "cs \<rightarrow>* (SKIP,t) \<Longrightarrow> cs \<Rightarrow> t" |
|
175 by (metis small_big_continue Skip) |
|
176 |
|
177 text {* |
|
178 Finally, the equivalence theorem: |
|
179 *} |
|
180 theorem big_iff_small: |
|
181 "cs \<Rightarrow> t = cs \<rightarrow>* (SKIP,t)" |
|
182 by(metis big_to_small small_to_big) |
|
183 |
|
184 |
|
185 subsection "Final configurations and infinite reductions" |
|
186 |
|
187 definition "final cs \<longleftrightarrow> \<not>(EX cs'. cs \<rightarrow> cs')" |
|
188 |
|
189 lemma finalD: "final (c,s) \<Longrightarrow> c = SKIP" |
|
190 apply(simp add: final_def) |
|
191 apply(induct c) |
|
192 apply blast+ |
|
193 done |
|
194 |
|
195 lemma final_iff_SKIP: "final (c,s) = (c = SKIP)" |
|
196 by (metis SkipE finalD final_def) |
|
197 |
|
198 text{* Now we can show that @{text"\<Rightarrow>"} yields a final state iff @{text"\<rightarrow>"} |
|
199 terminates: *} |
|
200 |
|
201 lemma big_iff_small_termination: |
|
202 "(EX t. cs \<Rightarrow> t) \<longleftrightarrow> (EX cs'. cs \<rightarrow>* cs' \<and> final cs')" |
|
203 by(simp add: big_iff_small final_iff_SKIP) |
|
204 |
|
205 text{* This is the same as saying that the absence of a big step result is |
|
206 equivalent with absence of a terminating small step sequence, i.e.\ with |
|
207 nontermination. Since @{text"\<rightarrow>"} is determininistic, there is no difference |
|
208 between may and must terminate. *} |
|
209 |
|
210 end |