145 |
145 |
146 ML {* fun r_mk_comb_tac_intex lthy = r_mk_comb_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *} |
146 ML {* fun r_mk_comb_tac_intex lthy = r_mk_comb_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *} |
147 ML {* fun all_r_mk_comb_tac_intex lthy = all_r_mk_comb_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *} |
147 ML {* fun all_r_mk_comb_tac_intex lthy = all_r_mk_comb_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *} |
148 |
148 |
149 |
149 |
150 lemma cheat: "P" sorry |
|
151 |
|
152 lemma "PLUS a b = PLUS b a" |
150 lemma "PLUS a b = PLUS b a" |
153 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
151 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) |
154 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
152 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
155 prefer 2 |
153 prefer 2 |
156 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
154 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
176 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
174 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
177 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
175 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
178 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
176 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
179 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
177 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
180 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
178 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
181 apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) |
179 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
182 done |
180 done |
183 |
181 |
184 lemma plus_assoc_pre: |
182 lemma plus_assoc_pre: |
185 shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)" |
183 shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)" |
186 apply (cases i) |
184 apply (cases i) |
234 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
232 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
235 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
233 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
236 done |
234 done |
237 |
235 |
238 |
236 |
239 (* |
|
240 |
|
241 ML {* |
|
242 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = |
|
243 (REPEAT1 o FIRST1) |
|
244 [(K (print_tac "start")) THEN' (K no_tac), |
|
245 DT ctxt "1" (rtac trans_thm), |
|
246 DT ctxt "2" (LAMBDA_RES_TAC ctxt), |
|
247 DT ctxt "3" (ball_rsp_tac ctxt), |
|
248 DT ctxt "4" (bex_rsp_tac ctxt), |
|
249 DT ctxt "5" (FIRST' (map rtac rsp_thms)), |
|
250 DT ctxt "6" (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
|
251 DT ctxt "7" (rtac refl), |
|
252 DT ctxt "8" (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
|
253 DT ctxt "9" (Cong_Tac.cong_tac @{thm cong}), |
|
254 DT ctxt "A" (rtac @{thm ext}), |
|
255 DT ctxt "B" (rtac reflex_thm), |
|
256 DT ctxt "C" (atac), |
|
257 DT ctxt "D" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))), |
|
258 DT ctxt "E" (WEAK_LAMBDA_RES_TAC ctxt), |
|
259 DT ctxt "F" (CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))] |
|
260 *} |
|
261 |
|
262 ML {* |
|
263 inj_repabs_trm @{context} (reg_atrm, aqtrm) |
|
264 |> Syntax.check_term @{context} |
|
265 *} |
|
266 |
|
267 |
|
268 ML {* val my_goal = cterm_of @{theory} (mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm)) *} |
|
269 ML {* val yr_goal = cterm_of @{theory} (build_repabs_goal @{context} (@{thm testtest} OF [arthm]) consts rty qty) *} |
|
270 |
|
271 prove {* mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) *} |
|
272 apply(tactic {* ObjectLogic.full_atomize_tac 1 *}) |
|
273 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) |
|
274 done |
|
275 |
|
276 ML {* |
|
277 inj_repabs_trm @{context} (reg_atrm, aqtrm) |
|
278 |> Syntax.string_of_term @{context} |
|
279 |> writeln |
|
280 *} |
|
281 |
|
282 *) |
|
283 |
|
284 |
|