139 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
139 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
140 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *} |
140 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *} |
141 ML {* val consts = lookup_quot_consts defs *} |
141 ML {* val consts = lookup_quot_consts defs *} |
142 |
142 |
143 ML {* |
143 ML {* |
144 fun lift_thm_my_int lthy t = |
|
145 lift_thm lthy qty ty_name rsp_thms defs t |
|
146 fun lift_thm_g_my_int lthy t g = |
|
147 lift_thm_goal lthy qty ty_name rsp_thms defs t g |
|
148 fun lift_tac_fset lthy t = |
144 fun lift_tac_fset lthy t = |
149 lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs |
145 lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs |
150 *} |
146 *} |
151 |
147 |
152 lemma "PLUS a b = PLUS b a" |
148 lemma "PLUS a b = PLUS b a" |
162 |
158 |
163 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" |
159 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" |
164 by (tactic {* lift_tac_fset @{context} @{thm plus_assoc_pre} 1 *}) |
160 by (tactic {* lift_tac_fset @{context} @{thm plus_assoc_pre} 1 *}) |
165 |
161 |
166 |
162 |
|
163 lemma ho_tst: "foldl my_plus x [] = x" |
|
164 apply simp |
|
165 done |
|
166 |
|
167 lemma "foldl PLUS x [] = x" |
|
168 apply (tactic {* lift_tac_fset @{context} @{thm ho_tst} 1 *}) |
|
169 prefer 3 |
|
170 apply(tactic {* clean_tac @{context} quot @{thms PLUS_def} reps_same 1 *}) |
|
171 sorry |
|
172 |
|
173 (* |
|
174 FIXME: All below is your construction code; mostly commented out as it |
|
175 does not work. |
|
176 *) |
|
177 |
167 ML {* |
178 ML {* |
168 mk_REGULARIZE_goal @{context} |
179 mk_REGULARIZE_goal @{context} |
169 @{term "\<forall>i j k. my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"} |
180 @{term "\<forall>i j k. my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"} |
170 @{term "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)"} |
181 @{term "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)"} |
171 |> Syntax.string_of_term @{context} |
182 |> Syntax.string_of_term @{context} |
172 |> writeln |
183 |> writeln |
173 *} |
184 *} |
174 |
|
175 |
|
176 ML {* |
|
177 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} @{typ "my_int"} |
|
178 val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int" |
|
179 *} |
|
180 |
|
181 |
185 |
182 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
186 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
183 apply(tactic {* procedure_tac @{thm plus_assoc_pre} @{context} 1 *}) |
187 apply(tactic {* procedure_tac @{thm plus_assoc_pre} @{context} 1 *}) |
184 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
188 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
185 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) |
189 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) |
186 apply(tactic {* clean_tac @{context} quot @{thms PLUS_def} reps_same 1 *}) |
190 apply(tactic {* clean_tac @{context} quot @{thms PLUS_def} reps_same 1 *}) |
187 done |
191 done |
188 |
192 |
189 |
193 |
190 (* |
194 (* |
191 does not work. |
195 |
192 ML {* |
196 ML {* |
193 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = |
197 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = |
194 (REPEAT1 o FIRST1) |
198 (REPEAT1 o FIRST1) |
195 [(K (print_tac "start")) THEN' (K no_tac), |
199 [(K (print_tac "start")) THEN' (K no_tac), |
196 DT ctxt "1" (rtac trans_thm), |
200 DT ctxt "1" (rtac trans_thm), |
207 DT ctxt "C" (atac), |
211 DT ctxt "C" (atac), |
208 DT ctxt "D" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))), |
212 DT ctxt "D" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))), |
209 DT ctxt "E" (WEAK_LAMBDA_RES_TAC ctxt), |
213 DT ctxt "E" (WEAK_LAMBDA_RES_TAC ctxt), |
210 DT ctxt "F" (CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))] |
214 DT ctxt "F" (CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))] |
211 *} |
215 *} |
212 *) |
|
213 |
|
214 ML {* |
|
215 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} @{typ "my_int"} |
|
216 val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int" |
|
217 val consts = lookup_quot_consts defs |
|
218 *} |
|
219 |
|
220 |
216 |
221 ML {* |
217 ML {* |
222 mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) |
218 mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) |
223 |> Syntax.check_term @{context} |
219 |> Syntax.check_term @{context} |
224 *} |
220 *} |
236 inj_REPABS @{context} (reg_atrm, aqtrm) |
232 inj_REPABS @{context} (reg_atrm, aqtrm) |
237 |> Syntax.string_of_term @{context} |
233 |> Syntax.string_of_term @{context} |
238 |> writeln |
234 |> writeln |
239 *} |
235 *} |
240 |
236 |
241 |
237 *) |
242 lemma ho_tst: "foldl my_plus x [] = x" |
238 |
243 apply simp |
239 |
244 done |
|
245 |
|
246 text {* Below is the construction site code used if things do not work *} |
|
247 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
|
248 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int" *} |
|
249 (* ML {* val consts = [@{const_name my_plus}] *}*) |
|
250 ML {* val consts = lookup_quot_consts defs *} |
|
251 ML {* val t_a = atomize_thm @{thm ho_tst} *} |
|
252 |
|
253 (* |
|
254 prove t_r: {* build_regularize_goal t_a rty rel @{context} *} |
|
255 ML_prf {* fun tac ctxt = |
|
256 (ObjectLogic.full_atomize_tac) THEN' |
|
257 REPEAT_ALL_NEW (FIRST' [ |
|
258 rtac rel_refl, |
|
259 atac, |
|
260 rtac @{thm universal_twice}, |
|
261 (rtac @{thm impI} THEN' atac), |
|
262 (*rtac @{thm equality_twice},*) |
|
263 EqSubst.eqsubst_tac ctxt [0] |
|
264 [(@{thm equiv_res_forall} OF [rel_eqv]), |
|
265 (@{thm equiv_res_exists} OF [rel_eqv])], |
|
266 (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl), |
|
267 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
|
268 ]);*} |
|
269 apply (atomize(full)) |
|
270 apply (tactic {* tac @{context} 1 *}) |
|
271 apply (auto) |
|
272 done |
|
273 ML {* val t_r = @{thm t_r} OF [t_a] *}*) |
|
274 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} |
|
275 ML {* |
|
276 val rt = build_repabs_term @{context} t_r consts rty qty |
|
277 val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); |
|
278 *} |
|
279 |
|
280 |
|
281 |
|
282 prove t_t: rg |
|
283 apply(atomize(full)) |
|
284 ML_prf {* fun r_mk_comb_tac_int lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} |
|
285 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_int @{context}) 1 *}) |
|
286 done |
|
287 ML {* val t_t = @{thm Pure.equal_elim_rule1} OF [@{thm t_t},t_r] *} |
|
288 ML {* val abs = findabs rty (prop_of t_a) *} |
|
289 ML {* val aps = findaps rty (prop_of t_a); *} |
|
290 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
|
291 |
|
292 (*ML {* val t_t = repabs @{context} @{thm t_r} consts rty qty quot rel_refl trans2 rsp_thms *}*) |
|
293 ML findallex |
|
294 ML {* val (alls, exs) = findallex @{context} rty qty (prop_of t_a) *} |
|
295 ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *} |
|
296 ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_t *} |
|
297 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_a *} |
|
298 ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *} |
|
299 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_l *} |
|
300 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
|
301 ML {* ObjectLogic.rulify t_r *} |
|
302 ML {* @{term "Trueprop"} *} |
|
303 |
|