175 |
175 |
176 term map |
176 term map |
177 term fmap |
177 term fmap |
178 thm fmap_def |
178 thm fmap_def |
179 |
179 |
180 ML {* val fset_defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def fold_def} *} |
180 ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def fold_def} *} |
181 (* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *) |
181 ML {* val consts = lookup_quot_consts defs *} |
182 |
182 ML {* val defs_sym = add_lower_defs @{context} defs *} |
183 ML {* |
|
184 val consts = [@{const_name "Nil"}, @{const_name "Cons"}, |
|
185 @{const_name "membship"}, @{const_name "card1"}, |
|
186 @{const_name "append"}, @{const_name "fold1"}, |
|
187 @{const_name "map"}]; |
|
188 *} |
|
189 |
|
190 ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *} |
|
191 |
183 |
192 lemma memb_rsp: |
184 lemma memb_rsp: |
193 fixes z |
185 fixes z |
194 assumes a: "list_eq x y" |
186 assumes a: "list_eq x y" |
195 shows "(z memb x) = (z memb y)" |
187 shows "(z memb x) = (z memb y)" |
301 lemma map_append : |
293 lemma map_append : |
302 "(map f ((a::'a list) @ b)) \<approx> |
294 "(map f ((a::'a list) @ b)) \<approx> |
303 ((map f a) ::'a list) @ (map f b)" |
295 ((map f a) ::'a list) @ (map f b)" |
304 by simp (rule list_eq_refl) |
296 by simp (rule list_eq_refl) |
305 |
297 |
306 ML {* val rty = @{typ "'a list"} *} |
|
307 ML {* val qty = @{typ "'a fset"} *} |
298 ML {* val qty = @{typ "'a fset"} *} |
308 ML {* val rel = @{term "list_eq"} *} |
299 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
309 ML {* val rel_eqv = (#equiv_thm o hd) (quotdata_lookup @{context}) *} |
300 ML {* val (trans2, reps_same, quot) = lookup_quot_thms @{context} "fset" *} |
310 ML {* val rel_refl = @{thm list_eq_refl} *} |
301 |
311 ML {* val quot = @{thm QUOTIENT_fset} *} |
|
312 ML {* val rsp_thms = |
302 ML {* val rsp_thms = |
313 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} |
303 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} |
314 @ @{thms ho_all_prs ho_ex_prs} *} |
304 @ @{thms ho_all_prs ho_ex_prs} *} |
315 ML {* val trans2 = @{thm QUOT_TYPE_I_fset.R_trans2} *} |
305 |
316 ML {* val reps_same = @{thm QUOT_TYPE_I_fset.REPS_same} *} |
306 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} |
317 ML {* val defs = fset_defs *} |
|
318 (* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *) |
|
319 ML {* |
|
320 val consts = [@{const_name "Nil"}, @{const_name "Cons"}, |
|
321 @{const_name "membship"}, @{const_name "card1"}, |
|
322 @{const_name "append"}, @{const_name "fold1"}, |
|
323 @{const_name "map"}]; |
|
324 *} |
|
325 |
|
326 ML {* fun lift_thm_fset lthy t = |
|
327 lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t |
|
328 *} |
|
329 |
307 |
330 lemma eq_r: "a = b \<Longrightarrow> a \<approx> b" |
308 lemma eq_r: "a = b \<Longrightarrow> a \<approx> b" |
331 by (simp add: list_eq_refl) |
309 by (simp add: list_eq_refl) |
332 |
310 |
333 ML {* lift_thm_fset @{context} @{thm m1} *} |
311 ML {* lift_thm_fset @{context} @{thm m1} *} |
340 |
318 |
341 thm fold1.simps(2) |
319 thm fold1.simps(2) |
342 thm list.recs(2) |
320 thm list.recs(2) |
343 |
321 |
344 ML {* val ind_r_a = atomize_thm @{thm list.induct} *} |
322 ML {* val ind_r_a = atomize_thm @{thm list.induct} *} |
345 (* prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
323 (* prove {* build_regularize_goal ind_r_a rty rel @{context} *} |
346 ML_prf {* fun tac ctxt = |
324 ML_prf {* fun tac ctxt = |
347 (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
325 (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
348 [(@{thm equiv_res_forall} OF [@{thm equiv_list_eq}]), |
326 [(@{thm equiv_res_forall} OF [rel_eqv]), |
349 (@{thm equiv_res_exists} OF [@{thm equiv_list_eq}])])) THEN_ALL_NEW |
327 (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW |
350 (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN' |
328 (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN' |
351 (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt [])); *} |
329 (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt [])); *} |
352 apply (tactic {* tac @{context} 1 *}) *) |
330 apply (tactic {* tac @{context} 1 *}) *) |
353 ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context} *} |
331 ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv @{context} *} |
354 ML {* |
332 ML {* |
355 val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
333 val rt = build_repabs_term @{context} ind_r_r consts rty qty |
356 val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); |
334 val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); |
357 *} |
335 *} |
358 (*prove rg |
336 (*prove rg |
359 apply(atomize(full)) |
337 apply(atomize(full)) |
360 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
338 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
361 done*) |
339 done*) |
362 ML {* val ind_r_t = |
340 ML {* val ind_r_t = |
363 Toplevel.program (fn () => |
341 Toplevel.program (fn () => |
364 repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
342 repabs @{context} ind_r_r consts rty qty quot rel_refl trans2 rsp_thms |
365 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
|
366 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}) |
|
367 ) |
343 ) |
368 *} |
344 *} |
369 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *} |
345 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *} |
370 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
346 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
371 ML {* val ind_r_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms ind_r_t *} |
347 ML {* val ind_r_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms ind_r_t *} |