290 done |
290 done |
291 |
291 |
292 (* The all_prs and ex_prs should be proved for the instance... *) |
292 (* The all_prs and ex_prs should be proved for the instance... *) |
293 ML {* |
293 ML {* |
294 fun r_mk_comb_tac_fset ctxt = |
294 fun r_mk_comb_tac_fset ctxt = |
295 r_mk_comb_tac ctxt @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
295 r_mk_comb_tac ctxt @{typ "'a list"} @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
296 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}) |
296 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}) |
297 *} |
297 *} |
298 |
298 |
299 |
299 |
300 ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *} |
300 ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *} |
301 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
301 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
302 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
302 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
|
303 |
|
304 ML {* val rty = @{typ "'a list"} *} |
|
305 |
|
306 ML {* |
|
307 fun r_mk_comb_tac_fset ctxt = |
|
308 r_mk_comb_tac ctxt rty @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
|
309 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}) |
|
310 *} |
|
311 |
303 |
312 |
304 ML {* trm_r *} |
313 ML {* trm_r *} |
305 prove list_induct_tr: trm_r |
314 prove list_induct_tr: trm_r |
306 apply (atomize(full)) |
315 apply (atomize(full)) |
307 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
316 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
334 done |
343 done |
335 |
344 |
336 lemma id_apply2 [simp]: "id x \<equiv> x" |
345 lemma id_apply2 [simp]: "id x \<equiv> x" |
337 by (simp add: id_def) |
346 by (simp add: id_def) |
338 |
347 |
339 ML {* |
|
340 val lpis = @{thm LAMBDA_PRS} OF [@{thm QUOTIENT_fset}, @{thm IDENTITY_QUOTIENT}]; |
|
341 val lpist = @{thm "HOL.sym"} OF [lpis]; |
|
342 val lam_prs = MetaSimplifier.rewrite_rule [@{thm id_apply2}] lpist |
|
343 *} |
|
344 |
|
345 text {* the proper way to do it *} |
|
346 ML {* |
|
347 fun findabs rty tm = |
|
348 case tm of |
|
349 Abs(_, T, b) => |
|
350 let |
|
351 val b' = subst_bound ((Free ("x", T)), b); |
|
352 val tys = findabs rty b' |
|
353 val ty = fastype_of tm |
|
354 in if needs_lift rty ty then (ty :: tys) else tys |
|
355 end |
|
356 | f $ a => (findabs rty f) @ (findabs rty a) |
|
357 | _ => [] |
|
358 *} |
|
359 |
|
360 ML {* val quot = @{thm QUOTIENT_fset} *} |
348 ML {* val quot = @{thm QUOTIENT_fset} *} |
361 ML {* val abs = findabs @{typ "'a list"} (prop_of (atomize_thm @{thm list_induct_hol4})) *} |
349 ML {* val abs = findabs @{typ "'a list"} (prop_of (atomize_thm @{thm list_induct_hol4})) *} |
362 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
350 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
363 |
351 |
364 ML {* |
352 ML {* |
365 fun simp_lam_prs lthy thm = |
353 fun simp_lam_prs lthy thm = |
366 simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm) |
354 simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm) |
367 handle _ => thm |
355 handle _ => thm |
368 *} |
356 *} |
369 |
357 |
370 ML {* val m2_t' = eqsubst_thm @{context} [lam_prs] @{thm m2_t} *} |
358 ML {* val m2_t' = simp_lam_prs @{context} @{thm m2_t} *} |
371 |
359 |
372 ML {* val ithm = simp_allex_prs @{context} quot m2_t' *} |
360 ML {* val ithm = simp_allex_prs @{context} quot m2_t' *} |
373 ML fset_defs_sym |
|
374 |
361 |
375 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *} |
362 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *} |
376 ML {* ObjectLogic.rulify rthm *} |
363 ML {* ObjectLogic.rulify rthm *} |
377 |
364 |
378 |
365 |
403 ML {* val qthm = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} rthm *} |
390 ML {* val qthm = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} rthm *} |
404 ML {* ObjectLogic.rulify qthm *} |
391 ML {* ObjectLogic.rulify qthm *} |
405 |
392 |
406 thm fold1.simps(2) |
393 thm fold1.simps(2) |
407 thm list.recs(2) |
394 thm list.recs(2) |
408 |
395 thm map_append |
409 ML {* val ind_r_a = atomize_thm @{thm map_append} *} |
396 |
|
397 ML {* val ind_r_a = atomize_thm @{thm list_induct_hol4} *} |
410 (* prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
398 (* prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
411 ML_prf {* fun tac ctxt = |
399 ML_prf {* fun tac ctxt = |
412 (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
400 (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
413 [(@{thm equiv_res_forall} OF [@{thm equiv_list_eq}]), |
401 [(@{thm equiv_res_forall} OF [@{thm equiv_list_eq}]), |
414 (@{thm equiv_res_exists} OF [@{thm equiv_list_eq}])])) THEN_ALL_NEW |
402 (@{thm equiv_res_exists} OF [@{thm equiv_list_eq}])])) THEN_ALL_NEW |
418 ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context} *} |
406 ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context} *} |
419 ML {* |
407 ML {* |
420 val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
408 val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
421 val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); |
409 val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); |
422 *} |
410 *} |
|
411 |
423 prove rg |
412 prove rg |
424 apply(atomize(full)) |
413 apply(atomize(full)) |
425 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
414 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
426 apply (auto) |
|
427 done |
415 done |
428 |
416 |
429 ML {* val (g, thm, othm) = |
417 ML {* val (g, thm, othm) = |
430 Toplevel.program (fn () => |
418 Toplevel.program (fn () => |
431 repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
419 repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
432 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
420 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
433 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}) |
421 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}) |
434 ) |
422 ) |
435 *} |
423 *} |
|
424 |
436 ML {* |
425 ML {* |
437 fun tac2 ctxt = |
426 fun tac2 ctxt = |
438 (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm])) |
427 (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm])) |
439 THEN' (rtac othm); *} |
428 THEN' (rtac othm); *} |
440 (* ML {* val cthm = Goal.prove @{context} [] [] g (fn x => tac2 (#context x) 1); |
429 (* ML {* val cthm = Goal.prove @{context} [] [] g (fn x => tac2 (#context x) 1); |
453 |
442 |
454 ML {* val ind_r_l1 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l *} |
443 ML {* val ind_r_l1 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l *} |
455 ML {* val ind_r_l2 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l1 *} |
444 ML {* val ind_r_l2 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l1 *} |
456 ML {* val ind_r_l3 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l2 *} |
445 ML {* val ind_r_l3 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l2 *} |
457 ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *} |
446 ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *} |
458 ML {* val ind_r_a = simp_allex_prs @{context} ind_r_l4 *} |
447 ML {* val ind_r_a = simp_allex_prs @{context} quot ind_r_l4 *} |
459 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *} |
448 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *} |
460 ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *} |
449 ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *} |
461 |
|
462 |
|
463 ML {* hd fset_defs_sym *} |
|
464 ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a1 *} |
450 ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a1 *} |
465 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} |
451 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} |
466 ML {* ObjectLogic.rulify ind_r_s *} |
452 ML {* ObjectLogic.rulify ind_r_s *} |
467 |
453 |
468 ML {* |
454 ML {* |
474 repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
460 repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
475 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
461 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
476 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp} @ @{thms ho_all_prs ho_ex_prs}); |
462 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp} @ @{thms ho_all_prs ho_ex_prs}); |
477 val ind_r_t = repabs_eq2 @{context} (g, t, ot); |
463 val ind_r_t = repabs_eq2 @{context} (g, t, ot); |
478 val ind_r_l = simp_lam_prs @{context} ind_r_t; |
464 val ind_r_l = simp_lam_prs @{context} ind_r_t; |
479 val ind_r_a = simp_allex_prs @{context} ind_r_l; |
465 val ind_r_a = simp_allex_prs @{context} quot ind_r_l; |
480 val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a; |
466 val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a; |
481 val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d |
467 val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d |
482 in |
468 in |
483 ObjectLogic.rulify ind_r_s |
469 ObjectLogic.rulify ind_r_s |
484 end |
470 end |