equal
deleted
inserted
replaced
54 For this we have to increase all other dangling de Bruijn indices by |
54 For this we have to increase all other dangling de Bruijn indices by |
55 \<open>-1\<close> to account for the deleted quantifier. An example is |
55 \<open>-1\<close> to account for the deleted quantifier. An example is |
56 as follows: |
56 as follows: |
57 |
57 |
58 @{ML_matchresult_fake [display,gray] |
58 @{ML_matchresult_fake [display,gray] |
59 "@{prop \"\<forall>x y z. P x = P z\"} |
59 \<open>@{prop "\<forall>x y z. P x = P z"} |
60 |> kill_trivial_quantifiers |
60 |> kill_trivial_quantifiers |
61 |> pretty_term @{context} |
61 |> pretty_term @{context} |
62 |> pwriteln" |
62 |> pwriteln\<close> |
63 "\<forall>x z. P x = P z"} |
63 \<open>\<forall>x z. P x = P z\<close>} |
64 \<close> |
64 \<close> |
65 |
65 |
66 |
66 |
67 |
67 |
68 text \<open>\solution{fun:makelist}\<close> |
68 text \<open>\solution{fun:makelist}\<close> |
109 By using \<open>#> fst\<close> in the last line, the function |
109 By using \<open>#> fst\<close> in the last line, the function |
110 @{ML scan_all} retruns a string, instead of the pair a parser would |
110 @{ML scan_all} retruns a string, instead of the pair a parser would |
111 normally return. For example: |
111 normally return. For example: |
112 |
112 |
113 @{ML_matchresult [display,gray] |
113 @{ML_matchresult [display,gray] |
114 "let |
114 \<open>let |
115 val input1 = (Symbol.explode \"foo bar\") |
115 val input1 = (Symbol.explode "foo bar") |
116 val input2 = (Symbol.explode \"foo (*test*) bar (*test*)\") |
116 val input2 = (Symbol.explode "foo (*test*) bar (*test*)") |
117 in |
117 in |
118 (scan_all input1, scan_all input2) |
118 (scan_all input1, scan_all input2) |
119 end" |
119 end\<close> |
120 "(\"foo bar\", \"foo (**test**) bar (**test**)\")"} |
120 \<open>("foo bar", "foo (**test**) bar (**test**)")\<close>} |
121 \<close> |
121 \<close> |
122 |
122 |
123 text \<open>\solution{ex:contextfree}\<close> |
123 text \<open>\solution{ex:contextfree}\<close> |
124 |
124 |
125 ML %grayML\<open>datatype expr = |
125 ML %grayML\<open>datatype expr = |
329 |
329 |
330 text \<open> |
330 text \<open> |
331 This function generates for example: |
331 This function generates for example: |
332 |
332 |
333 @{ML_matchresult_fake [display,gray] |
333 @{ML_matchresult_fake [display,gray] |
334 "pwriteln (pretty_term @{context} (term_tree 2))" |
334 \<open>pwriteln (pretty_term @{context} (term_tree 2))\<close> |
335 "(1 + 2) + (3 + 4)"} |
335 \<open>(1 + 2) + (3 + 4)\<close>} |
336 |
336 |
337 The next function constructs a goal of the form \<open>P \<dots>\<close> with a term |
337 The next function constructs a goal of the form \<open>P \<dots>\<close> with a term |
338 produced by @{ML term_tree} filled in. |
338 produced by @{ML term_tree} filled in. |
339 \<close> |
339 \<close> |
340 |
340 |
342 |
342 |
343 text \<open> |
343 text \<open> |
344 Note that the goal needs to be wrapped in a @{term "Trueprop"}. Next we define |
344 Note that the goal needs to be wrapped in a @{term "Trueprop"}. Next we define |
345 two tactics, \<open>c_tac\<close> and \<open>s_tac\<close>, for the conversion and simproc, |
345 two tactics, \<open>c_tac\<close> and \<open>s_tac\<close>, for the conversion and simproc, |
346 respectively. The idea is to first apply the conversion (respectively simproc) and |
346 respectively. The idea is to first apply the conversion (respectively simproc) and |
347 then prove the remaining goal using @{ML "cheat_tac" in Skip_Proof}. |
347 then prove the remaining goal using @{ML \<open>cheat_tac\<close> in Skip_Proof}. |
348 \<close> |
348 \<close> |
349 |
349 |
350 ML Skip_Proof.cheat_tac |
350 ML Skip_Proof.cheat_tac |
351 |
351 |
352 ML %grayML\<open>local |
352 ML %grayML\<open>local |