178 @{term "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)"} |
178 @{term "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)"} |
179 |> Syntax.string_of_term @{context} |
179 |> Syntax.string_of_term @{context} |
180 |> writeln |
180 |> writeln |
181 *} |
181 *} |
182 |
182 |
183 lemma procedure: |
|
184 assumes a: "A" |
|
185 and b: "A \<Longrightarrow> B" |
|
186 and c: "B = C" |
|
187 and d: "C = D" |
|
188 shows "D" |
|
189 using a b c d |
|
190 by simp |
|
191 |
|
192 ML {* |
|
193 fun procedure_inst ctxt rtrm qtrm = |
|
194 let |
|
195 val thy = ProofContext.theory_of ctxt |
|
196 val rtrm' = HOLogic.dest_Trueprop rtrm |
|
197 val qtrm' = HOLogic.dest_Trueprop qtrm |
|
198 val reg_goal = Syntax.check_term ctxt (REGULARIZE_trm ctxt rtrm' qtrm') |
|
199 val inj_goal = Syntax.check_term ctxt (inj_REPABS ctxt (reg_goal, qtrm')) |
|
200 in |
|
201 Drule.instantiate' [] |
|
202 [SOME (cterm_of thy rtrm'), |
|
203 SOME (cterm_of thy reg_goal), |
|
204 SOME (cterm_of thy inj_goal)] |
|
205 @{thm procedure} |
|
206 end |
|
207 |
|
208 fun procedure_tac rthm = |
|
209 Subgoal.FOCUS (fn {context, concl, ...} => |
|
210 let |
|
211 val rthm' = atomize_thm rthm |
|
212 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
|
213 in |
|
214 EVERY1 [rtac rule, rtac rthm'] |
|
215 end) |
|
216 *} |
|
217 |
183 |
218 ML {* |
184 ML {* |
219 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} @{typ "my_int"} |
185 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} @{typ "my_int"} |
220 val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int" |
186 val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int" |
221 *} |
187 *} |
222 |
188 |
223 (* FIXME: allex_prs and lambda_prs can be one function *) |
|
224 |
|
225 ML {* |
|
226 fun allex_prs_tac lthy quot = |
|
227 (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]}) |
|
228 THEN' (quotient_tac quot); |
|
229 *} |
|
230 |
|
231 ML {* |
|
232 fun lambda_prs_tac lthy quot = |
|
233 (EqSubst.eqsubst_tac lthy [0] @{thms LAMBDA_PRS} |
|
234 THEN' (RANGE [quotient_tac quot, quotient_tac quot])); |
|
235 *} |
|
236 |
|
237 ML {* |
|
238 fun clean_tac lthy quot defs reps_same = |
|
239 let |
|
240 val lower = flat (map (add_lower_defs lthy) defs) |
|
241 in |
|
242 (REPEAT_ALL_NEW (allex_prs_tac lthy quot)) THEN' |
|
243 (REPEAT_ALL_NEW (lambda_prs_tac lthy quot)) THEN' |
|
244 (REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower)) THEN' |
|
245 (simp_tac (HOL_ss addsimps [reps_same])) |
|
246 end |
|
247 *} |
|
248 |
189 |
249 lemma "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
190 lemma "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
250 apply(tactic {* procedure_tac @{thm plus_assoc_pre} @{context} 1 *}) |
191 apply(tactic {* procedure_tac @{thm plus_assoc_pre} @{context} 1 *}) |
251 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
192 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
252 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) |
193 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) |