66 |
66 |
67 method match_test' = |
67 method match_test' = |
68 (match conclusion in |
68 (match conclusion in |
69 "P \<and> Q" for P Q \<Rightarrow> |
69 "P \<and> Q" for P Q \<Rightarrow> |
70 \<open>print_term P, print_term Q, rule conjI[where P="P" and Q="Q"]; assumption\<close> |
70 \<open>print_term P, print_term Q, rule conjI[where P="P" and Q="Q"]; assumption\<close> |
71 \<bar> "H" for H \<Rightarrow> \<open>print_term H\<close> |
71 \<bar> "H" for H \<Rightarrow> \<open>print_term H\<close>) |
72 ) |
|
73 |
72 |
74 text \<open>Solves goal\<close> |
73 text \<open>Solves goal\<close> |
75 lemma "P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q" |
74 lemma "P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q" |
76 apply match_test' |
75 apply match_test' |
77 done |
76 done |
147 done |
146 done |
148 |
147 |
149 |
148 |
150 subsection \<open>Demo\<close> |
149 subsection \<open>Demo\<close> |
151 |
150 |
152 method solve methods m = (m; fail) |
|
153 |
|
154 named_theorems intros and elims and subst |
151 named_theorems intros and elims and subst |
155 |
152 |
156 method prop_solver declares intros elims subst = |
153 method prop_solver declares intros elims subst = |
157 (assumption | |
154 (assumption | |
158 rule intros | erule elims | |
155 rule intros | erule elims | |
159 subst subst | subst (asm) subst | |
156 subst subst | subst (asm) subst | |
160 (erule notE; solve \<open>prop_solver\<close>))+ |
157 (erule notE; solves \<open>prop_solver\<close>))+ |
161 |
158 |
162 lemmas [intros] = |
159 lemmas [intros] = |
163 conjI |
160 conjI |
164 impI |
161 impI |
165 disjCI |
162 disjCI |
213 lemma "(\<forall>x. P x) \<and> (\<forall>x. Q x) \<Longrightarrow> (\<forall>x. P x \<and> Q x)" |
210 lemma "(\<forall>x. P x) \<and> (\<forall>x. Q x) \<Longrightarrow> (\<forall>x. P x \<and> Q x)" |
214 and "\<exists>x. P x \<longrightarrow> (\<forall>x. P x)" |
211 and "\<exists>x. P x \<longrightarrow> (\<forall>x. P x)" |
215 and "(\<exists>x. \<forall>y. R x y) \<longrightarrow> (\<forall>y. \<exists>x. R x y)" |
212 and "(\<exists>x. \<forall>y. R x y) \<longrightarrow> (\<forall>y. \<exists>x. R x y)" |
216 by fol_solver+ |
213 by fol_solver+ |
217 |
214 |
|
215 |
|
216 text \<open> |
|
217 Eisbach_Tools provides the catch method, which catches run-time method |
|
218 errors. In this example the OF attribute throws an error when it can't |
|
219 compose H with A, forcing H to be re-bound to different members of imps |
|
220 until it succeeds. |
|
221 \<close> |
|
222 |
|
223 lemma |
|
224 assumes imps: "A \<Longrightarrow> B" "A \<Longrightarrow> C" "B \<Longrightarrow> D" |
|
225 assumes A: "A" |
|
226 shows "B \<and> C" |
|
227 apply (rule conjI) |
|
228 apply ((match imps in H:"_ \<Longrightarrow> _" \<Rightarrow> \<open>catch \<open>rule H[OF A], print_fact H\<close> \<open>print_fact H, fail\<close>\<close>)+) |
|
229 done |
|
230 |
|
231 text \<open> |
|
232 Eisbach_Tools provides the curry and uncurry attributes. This is useful |
|
233 when the number of premises of a thm isn't known statically. The pattern |
|
234 @{term "P \<Longrightarrow> Q"} matches P against the major premise of a thm, and Q is the |
|
235 rest of the premises with the conclusion. If we first uncurry, then @{term |
|
236 "P \<Longrightarrow> Q"} will match P with the conjunction of all the premises, and Q with |
|
237 the final conclusion of the rule. |
|
238 \<close> |
|
239 |
|
240 lemma |
|
241 assumes imps: "A \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> C" "E \<Longrightarrow> D \<Longrightarrow> A" |
|
242 shows "(A \<longrightarrow> B \<longrightarrow> C) \<and> (D \<longrightarrow> C)" |
|
243 by (match imps[uncurry] in H[curry]:"_ \<Longrightarrow> C" (cut, multi) \<Rightarrow> |
|
244 \<open>match H in "E \<Longrightarrow> _" \<Rightarrow> \<open>fail\<close> |
|
245 \<bar> _ \<Rightarrow> \<open>simp add: H\<close>\<close>) |
|
246 |
218 end |
247 end |