293 done |
305 done |
294 |
306 |
295 (* The all_prs and ex_prs should be proved for the instance... *) |
307 (* The all_prs and ex_prs should be proved for the instance... *) |
296 ML {* |
308 ML {* |
297 fun r_mk_comb_tac_fset ctxt = |
309 fun r_mk_comb_tac_fset ctxt = |
298 r_mk_comb_tac ctxt @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
310 r_mk_comb_tac ctxt @{typ "'a list"} @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
299 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}) |
311 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}) |
300 *} |
312 *} |
301 |
313 |
302 |
314 |
303 ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *} |
315 ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *} |
304 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
316 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
305 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
317 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
|
318 |
|
319 ML {* val rty = @{typ "'a list"} *} |
|
320 |
|
321 ML {* |
|
322 fun r_mk_comb_tac_fset ctxt = |
|
323 r_mk_comb_tac ctxt rty @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
|
324 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}) |
|
325 *} |
|
326 |
306 |
327 |
307 ML {* trm_r *} |
328 ML {* trm_r *} |
308 prove list_induct_tr: trm_r |
329 prove list_induct_tr: trm_r |
309 apply (atomize(full)) |
330 apply (atomize(full)) |
310 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
331 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
337 done |
358 done |
338 |
359 |
339 lemma id_apply2 [simp]: "id x \<equiv> x" |
360 lemma id_apply2 [simp]: "id x \<equiv> x" |
340 by (simp add: id_def) |
361 by (simp add: id_def) |
341 |
362 |
342 ML {* |
|
343 val lpis = @{thm LAMBDA_PRS} OF [@{thm QUOTIENT_fset}, @{thm IDENTITY_QUOTIENT}]; |
|
344 val lpist = @{thm "HOL.sym"} OF [lpis]; |
|
345 val lam_prs = MetaSimplifier.rewrite_rule [@{thm id_apply2}] lpist |
|
346 *} |
|
347 |
|
348 text {* the proper way to do it *} |
|
349 ML {* |
|
350 fun findabs rty tm = |
|
351 case tm of |
|
352 Abs(_, T, b) => |
|
353 let |
|
354 val b' = subst_bound ((Free ("x", T)), b); |
|
355 val tys = findabs rty b' |
|
356 val ty = fastype_of tm |
|
357 in if needs_lift rty ty then (ty :: tys) else tys |
|
358 end |
|
359 | f $ a => (findabs rty f) @ (findabs rty a) |
|
360 | _ => [] |
|
361 *} |
|
362 |
|
363 ML {* val quot = @{thm QUOTIENT_fset} *} |
363 ML {* val quot = @{thm QUOTIENT_fset} *} |
364 ML {* val abs = findabs @{typ "'a list"} (prop_of (atomize_thm @{thm list_induct_hol4})) *} |
364 ML {* val abs = findabs @{typ "'a list"} (prop_of (atomize_thm @{thm list_induct_hol4})) *} |
365 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
365 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
366 |
366 |
367 ML {* |
367 ML {* |
368 fun simp_lam_prs lthy thm = |
368 fun simp_lam_prs lthy thm = |
369 simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm) |
369 simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm) |
370 handle _ => thm |
370 handle _ => thm |
371 *} |
371 *} |
372 |
372 |
373 ML {* val m2_t' = eqsubst_thm @{context} [lam_prs] @{thm m2_t} *} |
373 ML {* val m2_t' = simp_lam_prs @{context} @{thm m2_t} *} |
374 |
374 |
375 ML {* val ithm = simp_allex_prs @{context} quot m2_t' *} |
375 ML {* val ithm = simp_allex_prs @{context} quot m2_t' *} |
376 ML fset_defs_sym |
|
377 |
376 |
378 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *} |
377 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *} |
379 ML {* ObjectLogic.rulify rthm *} |
378 ML {* ObjectLogic.rulify rthm *} |
380 |
379 |
381 |
380 |
421 ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context} *} |
421 ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context} *} |
422 ML {* |
422 ML {* |
423 val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
423 val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
424 val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); |
424 val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); |
425 *} |
425 *} |
|
426 |
426 prove rg |
427 prove rg |
427 apply(atomize(full)) |
428 apply(atomize(full)) |
428 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
429 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
429 apply (auto) |
430 done |
430 done |
431 |
431 |
432 ML {* val ind_r_t = |
432 ML {* val (g, thm, othm) = |
|
433 Toplevel.program (fn () => |
433 Toplevel.program (fn () => |
434 repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
434 repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
435 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
435 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
436 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}) |
436 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}) |
437 ) |
437 ) |
438 *} |
438 *} |
439 ML {* |
439 ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t *} |
440 fun tac2 ctxt = |
|
441 (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm])) |
|
442 THEN' (rtac othm); *} |
|
443 (* ML {* val cthm = Goal.prove @{context} [] [] g (fn x => tac2 (#context x) 1); |
|
444 *} *) |
|
445 |
|
446 ML {* |
|
447 val ind_r_t2 = |
|
448 Toplevel.program (fn () => |
|
449 repabs_eq2 @{context} (g, thm, othm) |
|
450 ) |
|
451 *} |
|
452 ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t2 *} |
|
453 lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1" |
440 lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1" |
454 apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10) |
441 apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10) |
455 done |
442 done |
456 |
443 |
457 ML {* val ind_r_l1 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l *} |
444 ML {* val ind_r_l1 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l *} |
458 ML {* val ind_r_l2 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l1 *} |
445 ML {* val ind_r_l2 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l1 *} |
459 ML {* val ind_r_l3 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l2 *} |
446 ML {* val ind_r_l3 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l2 *} |
460 ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *} |
447 ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *} |
461 ML {* val ind_r_a = simp_allex_prs @{context} ind_r_l4 *} |
448 ML {* val ind_r_a = simp_allex_prs @{context} quot ind_r_l4 *} |
462 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *} |
449 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *} |
463 ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *} |
450 ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *} |
464 |
451 ML {* val ind_r_d = repeat_eqsubst_thm @{context} fset_defs_sym ind_r_a1 *} |
465 |
|
466 ML {* hd fset_defs_sym *} |
|
467 ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a1 *} |
|
468 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} |
452 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} |
469 ML {* ObjectLogic.rulify ind_r_s *} |
453 ML {* ObjectLogic.rulify ind_r_s *} |
470 |
454 |
471 ML {* |
455 ML {* |
472 fun lift thm = |
456 fun lift thm = |
473 let |
457 let |
474 val ind_r_a = atomize_thm thm; |
458 val ind_r_a = atomize_thm thm; |
475 val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context}; |
459 val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context}; |
476 val (g, t, ot) = |
460 val ind_r_t = |
477 repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
461 repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
478 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
462 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
479 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp} @ @{thms ho_all_prs ho_ex_prs}); |
463 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}); |
480 val ind_r_t = repabs_eq2 @{context} (g, t, ot); |
|
481 val ind_r_l = simp_lam_prs @{context} ind_r_t; |
464 val ind_r_l = simp_lam_prs @{context} ind_r_t; |
482 val ind_r_a = simp_allex_prs @{context} ind_r_l; |
465 val ind_r_a = simp_allex_prs @{context} quot ind_r_l; |
483 val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a; |
466 val ind_r_d = repeat_eqsubst_thm @{context} fset_defs_sym ind_r_a; |
484 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 |
485 in |
468 in |
486 ObjectLogic.rulify ind_r_s |
469 ObjectLogic.rulify ind_r_s |
487 end |
470 end |
488 *} |
471 *} |
489 ML fset_defs |
472 ML fset_defs |
|
473 |
|
474 lemma eq_r: "a = b \<Longrightarrow> a \<approx> b" |
|
475 by (simp add: list_eq_refl) |
490 |
476 |
491 |
477 |
492 ML {* lift @{thm m2} *} |
478 ML {* lift @{thm m2} *} |
493 ML {* lift @{thm m1} *} |
479 ML {* lift @{thm m1} *} |
494 ML {* lift @{thm list_eq.intros(4)} *} |
480 ML {* lift @{thm list_eq.intros(4)} *} |
495 ML {* lift @{thm list_eq.intros(5)} *} |
481 ML {* lift @{thm list_eq.intros(5)} *} |
496 ML {* lift @{thm card1_suc} *} |
482 ML {* lift @{thm card1_suc} *} |
497 (* ML {* lift @{thm append_assoc} *} *) |
483 ML {* lift @{thm map_append} *} |
498 |
484 ML {* lift @{thm eq_r[OF append_assoc]} *} |
499 thm |
485 |
|
486 thm |
500 |
487 |
501 |
488 |
502 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
489 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
503 notation ( output) "Trueprop" ("#_" [1000] 1000) |
490 notation ( output) "Trueprop" ("#_" [1000] 1000) |
504 |
491 |