equal
deleted
inserted
replaced
191 apply(tactic {* procedure_tac @{thm plus_assoc_pre} @{context} 1 *}) |
191 apply(tactic {* procedure_tac @{thm plus_assoc_pre} @{context} 1 *}) |
192 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
192 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
193 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 *}) |
194 apply(tactic {* clean_tac @{context} quot @{thms PLUS_def} reps_same 1 *}) |
194 apply(tactic {* clean_tac @{context} quot @{thms PLUS_def} reps_same 1 *}) |
195 done |
195 done |
196 |
|
197 apply(tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *}) |
|
198 apply(tactic {* REPEAT_ALL_NEW (lambda_prs_tac @{context} quot) 1 *}) |
|
199 (* phase 2 *) |
|
200 ML_prf {* |
|
201 val lower = add_lower_defs @{context} @{thm PLUS_def} |
|
202 *} |
|
203 apply(tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1*}) |
|
204 apply(tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *}) |
|
205 done |
|
206 |
|
207 |
196 |
208 |
197 |
209 (* |
198 (* |
210 does not work. |
199 does not work. |
211 ML {* |
200 ML {* |
234 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} @{typ "my_int"} |
223 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} @{typ "my_int"} |
235 val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int" |
224 val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int" |
236 val consts = lookup_quot_consts defs |
225 val consts = lookup_quot_consts defs |
237 *} |
226 *} |
238 |
227 |
239 ML {* cprem_of *} |
|
240 |
228 |
241 ML {* |
229 ML {* |
242 mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) |
230 mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) |
243 |> Syntax.check_term @{context} |
231 |> Syntax.check_term @{context} |
244 *} |
232 *} |