12 |
12 |
13 chapter {* Solutions to Most Exercises\label{ch:solutions} *} |
13 chapter {* Solutions to Most Exercises\label{ch:solutions} *} |
14 |
14 |
15 text {* \solution{fun:revsum} *} |
15 text {* \solution{fun:revsum} *} |
16 |
16 |
17 ML{*fun rev_sum ((p as Const (@{const_name plus}, _)) $ t $ u) = |
17 ML{*fun rev_sum |
18 p $ u $ rev_sum t |
18 ((p as Const (@{const_name plus}, _)) $ t $ u) = p $ u $ rev_sum t |
19 | rev_sum t = t *} |
19 | rev_sum t = t *} |
20 |
20 |
21 text {* |
21 text {* |
22 An alternative solution using the function @{ML_ind mk_binop in HOLogic} is: |
22 An alternative solution using the function @{ML_ind mk_binop in HOLogic} is: |
23 *} |
23 *} |
25 ML{*fun rev_sum t = |
25 ML{*fun rev_sum t = |
26 let |
26 let |
27 fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u |
27 fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u |
28 | dest_sum u = [u] |
28 | dest_sum u = [u] |
29 in |
29 in |
30 foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t) |
30 foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t) |
31 end *} |
31 end *} |
32 |
32 |
33 text {* \solution{fun:makesum} *} |
33 text {* \solution{fun:makesum} *} |
34 |
34 |
35 ML{*fun make_sum t1 t2 = |
35 ML{*fun make_sum t1 t2 = |
36 HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *} |
36 HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *} |
37 |
37 |
38 |
38 |
39 text {* \solution{fun:makelist} *} |
39 text {* \solution{fun:makelist} *} |
40 |
40 |
41 ML{*fun mk_rev_upto i = |
41 ML{*fun mk_rev_upto i = |
141 shows "\<lbrakk>A \<longrightarrow> B; A; B \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" |
141 shows "\<lbrakk>A \<longrightarrow> B; A; B \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" |
142 by iprover |
142 by iprover |
143 |
143 |
144 lemma impE2: |
144 lemma impE2: |
145 shows "\<lbrakk>(C \<and> D) \<longrightarrow> B; C \<longrightarrow> (D \<longrightarrow>B) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" |
145 shows "\<lbrakk>(C \<and> D) \<longrightarrow> B; C \<longrightarrow> (D \<longrightarrow>B) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" |
146 by iprover |
146 and "\<lbrakk>(C \<or> D) \<longrightarrow> B; \<lbrakk>C \<longrightarrow> B; D \<longrightarrow> B\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" |
147 |
147 and "\<lbrakk>(C \<longrightarrow> D) \<longrightarrow> B; D \<longrightarrow> B \<Longrightarrow> C \<longrightarrow> D; B \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" |
148 lemma impE3: |
148 and "\<lbrakk>(C = D) \<longrightarrow> B; (C \<longrightarrow> D) \<longrightarrow> ((D \<longrightarrow> C) \<longrightarrow> B) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" |
149 shows "\<lbrakk>(C \<or> D) \<longrightarrow> B; \<lbrakk>C \<longrightarrow> B; D \<longrightarrow> B\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" |
149 by iprover+ |
150 by iprover |
|
151 |
|
152 lemma impE4: |
|
153 shows "\<lbrakk>(C \<longrightarrow> D) \<longrightarrow> B; D \<longrightarrow> B \<Longrightarrow> C \<longrightarrow> D; B \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" |
|
154 by iprover |
|
155 |
|
156 lemma impE5: |
|
157 shows "\<lbrakk>(C = D) \<longrightarrow> B; (C \<longrightarrow> D) \<longrightarrow> ((D \<longrightarrow> C) \<longrightarrow> B) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" |
|
158 by iprover |
|
159 |
150 |
160 text {* |
151 text {* |
161 Now the tactic which applies a single rule can be implemented |
152 Now the tactic which applies a single rule can be implemented |
162 as follows. |
153 as follows. |
163 *} |
154 *} |
164 |
155 |
165 ML %linenosgray{*val apply_tac = |
156 ML %linenosgray{*val apply_tac = |
166 let |
157 let |
167 val intros = [@{thm conjI}, @{thm disjI1}, @{thm disjI2}, |
158 val intros = @{thms conjI disjI1 disjI2 impI iffI} |
168 @{thm impI}, @{thm iffI}] |
159 val elims = @{thms FalseE conjE disjE iffE impE2} |
169 val elims = [@{thm FalseE}, @{thm conjE}, @{thm disjE}, @{thm iffE}, |
|
170 @{thm impE2}, @{thm impE3}, @{thm impE4}, @{thm impE5}] |
|
171 in |
160 in |
172 atac |
161 atac |
173 ORELSE' resolve_tac intros |
162 ORELSE' resolve_tac intros |
174 ORELSE' eresolve_tac elims |
163 ORELSE' eresolve_tac elims |
175 ORELSE' (etac @{thm impE1} THEN' atac) |
164 ORELSE' (etac @{thm impE1} THEN' atac) |