equal
deleted
inserted
replaced
193 fun procedure_inst ctxt rtrm qtrm = |
193 fun procedure_inst ctxt rtrm qtrm = |
194 let |
194 let |
195 val thy = ProofContext.theory_of ctxt |
195 val thy = ProofContext.theory_of ctxt |
196 val rtrm' = HOLogic.dest_Trueprop rtrm |
196 val rtrm' = HOLogic.dest_Trueprop rtrm |
197 val qtrm' = HOLogic.dest_Trueprop qtrm |
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')) |
198 in |
200 in |
199 Drule.instantiate' [] |
201 Drule.instantiate' [] |
200 [SOME (cterm_of thy rtrm'), |
202 [SOME (cterm_of thy rtrm'), |
201 SOME (cterm_of thy (Syntax.check_term ctxt (REGULARIZE_trm ctxt rtrm' qtrm'))), |
203 SOME (cterm_of thy reg_goal), |
202 SOME (cterm_of thy (Syntax.check_term ctxt (inj_REPABS ctxt (rtrm', qtrm'))))] |
204 SOME (cterm_of thy inj_goal)] |
203 @{thm procedure} |
205 @{thm procedure} |
204 end |
206 end |
205 |
207 |
206 fun procedure_tac rthm = |
208 fun procedure_tac rthm = |
207 Subgoal.FOCUS (fn {context, concl, ...} => |
209 Subgoal.FOCUS (fn {context, concl, ...} => |
213 end) |
215 end) |
214 *} |
216 *} |
215 |
217 |
216 lemma "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
218 lemma "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
217 apply(tactic {* procedure_tac @{thm plus_assoc_pre} @{context} 1 *}) |
219 apply(tactic {* procedure_tac @{thm plus_assoc_pre} @{context} 1 *}) |
218 sorry |
220 thm FORALL_PRS |
|
221 prefer 3 |
|
222 (* phase 1 *) |
|
223 apply(subst FORALL_PRS[symmetric]) |
|
224 apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *}) |
|
225 apply(subst FORALL_PRS[symmetric]) |
|
226 apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *}) |
|
227 apply(subst FORALL_PRS[symmetric]) |
|
228 apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *}) |
|
229 apply(subst LAMBDA_PRS) |
|
230 apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *}) |
|
231 apply(fold id_def) |
|
232 apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *}) |
|
233 apply(subst LAMBDA_PRS) |
|
234 apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *}) |
|
235 apply(fold id_def) |
|
236 apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *}) |
|
237 apply(subst LAMBDA_PRS) |
|
238 apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *}) |
|
239 apply(fold id_def) |
|
240 apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *}) |
|
241 (* phase 2 *) |
|
242 ML_prf {* |
|
243 val lower = add_lower_defs @{context} @{thm PLUS_def} |
|
244 *} |
|
245 apply(tactic {* EqSubst.eqsubst_tac @{context} [0] lower 1*}) |
|
246 apply(tactic {* EqSubst.eqsubst_tac @{context} [0] lower 1*}) |
|
247 apply(tactic {* EqSubst.eqsubst_tac @{context} [0] lower 1*}) |
|
248 apply(tactic {* EqSubst.eqsubst_tac @{context} [0] lower 1*}) |
|
249 (* phase 3 *) |
|
250 apply(subst QUOT_TYPE_I_my_int.REPS_same) |
|
251 apply(rule refl) |
|
252 |
|
253 |
219 |
254 |
220 |
255 |
221 (* |
256 (* |
222 does not work. |
257 does not work. |
223 ML {* |
258 ML {* |