185 experts only; feel free to ignore it. |
185 experts only; feel free to ignore it. |
186 |
186 |
187 While the first part is still a somewhat intelligible specification of the |
187 While the first part is still a somewhat intelligible specification of the |
188 concrete syntactic representation of our Hoare language, the actual ``ML |
188 concrete syntactic representation of our Hoare language, the actual ``ML |
189 drivers'' is quite involved. Just note that the we re-use the basic |
189 drivers'' is quite involved. Just note that the we re-use the basic |
190 quote/antiquote translations as already defined in Isabelle/Pure (see @{ML |
190 quote/antiquote translations as already defined in Isabelle/Pure (see \<^ML>\<open>Syntax_Trans.quote_tr\<close>, and \<^ML>\<open>Syntax_Trans.quote_tr'\<close>,). |
191 Syntax_Trans.quote_tr}, and @{ML Syntax_Trans.quote_tr'},). |
|
192 \<close> |
191 \<close> |
193 |
192 |
194 syntax |
193 syntax |
195 "_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)" |
194 "_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)" |
196 "_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b" ("\<acute>_" [1000] 1000) |
195 "_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b" ("\<acute>_" [1000] 1000) |
211 "WHILE b INV i DO c OD" \<rightharpoonup> "CONST While \<lbrace>b\<rbrace> i c" |
210 "WHILE b INV i DO c OD" \<rightharpoonup> "CONST While \<lbrace>b\<rbrace> i c" |
212 "WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD" |
211 "WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD" |
213 |
212 |
214 parse_translation \<open> |
213 parse_translation \<open> |
215 let |
214 let |
216 fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t |
215 fun quote_tr [t] = Syntax_Trans.quote_tr \<^syntax_const>\<open>_antiquote\<close> t |
217 | quote_tr ts = raise TERM ("quote_tr", ts); |
216 | quote_tr ts = raise TERM ("quote_tr", ts); |
218 in [(@{syntax_const "_quote"}, K quote_tr)] end |
217 in [(\<^syntax_const>\<open>_quote\<close>, K quote_tr)] end |
219 \<close> |
218 \<close> |
220 |
219 |
221 text \<open> |
220 text \<open> |
222 As usual in Isabelle syntax translations, the part for printing is more |
221 As usual in Isabelle syntax translations, the part for printing is more |
223 complicated --- we cannot express parts as macro rules as above. Don't look |
222 complicated --- we cannot express parts as macro rules as above. Don't look |
225 \<close> |
224 \<close> |
226 |
225 |
227 print_translation \<open> |
226 print_translation \<open> |
228 let |
227 let |
229 fun quote_tr' f (t :: ts) = |
228 fun quote_tr' f (t :: ts) = |
230 Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts) |
229 Term.list_comb (f $ Syntax_Trans.quote_tr' \<^syntax_const>\<open>_antiquote\<close> t, ts) |
231 | quote_tr' _ _ = raise Match; |
230 | quote_tr' _ _ = raise Match; |
232 |
231 |
233 val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"}); |
232 val assert_tr' = quote_tr' (Syntax.const \<^syntax_const>\<open>_Assert\<close>); |
234 |
233 |
235 fun bexp_tr' name ((Const (@{const_syntax Collect}, _) $ t) :: ts) = |
234 fun bexp_tr' name ((Const (\<^const_syntax>\<open>Collect\<close>, _) $ t) :: ts) = |
236 quote_tr' (Syntax.const name) (t :: ts) |
235 quote_tr' (Syntax.const name) (t :: ts) |
237 | bexp_tr' _ _ = raise Match; |
236 | bexp_tr' _ _ = raise Match; |
238 |
237 |
239 fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) = |
238 fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) = |
240 quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax_Trans.update_name_tr' f) |
239 quote_tr' (Syntax.const \<^syntax_const>\<open>_Assign\<close> $ Syntax_Trans.update_name_tr' f) |
241 (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts) |
240 (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts) |
242 | assign_tr' _ = raise Match; |
241 | assign_tr' _ = raise Match; |
243 in |
242 in |
244 [(@{const_syntax Collect}, K assert_tr'), |
243 [(\<^const_syntax>\<open>Collect\<close>, K assert_tr'), |
245 (@{const_syntax Basic}, K assign_tr'), |
244 (\<^const_syntax>\<open>Basic\<close>, K assign_tr'), |
246 (@{const_syntax Cond}, K (bexp_tr' @{syntax_const "_Cond"})), |
245 (\<^const_syntax>\<open>Cond\<close>, K (bexp_tr' \<^syntax_const>\<open>_Cond\<close>)), |
247 (@{const_syntax While}, K (bexp_tr' @{syntax_const "_While_inv"}))] |
246 (\<^const_syntax>\<open>While\<close>, K (bexp_tr' \<^syntax_const>\<open>_While_inv\<close>))] |
248 end |
247 end |
249 \<close> |
248 \<close> |
250 |
249 |
251 |
250 |
252 subsection \<open>Rules for single-step proof \label{sec:hoare-isar}\<close> |
251 subsection \<open>Rules for single-step proof \label{sec:hoare-isar}\<close> |