291 lemma map_append : |
279 lemma map_append : |
292 "(map f ((a::'a list) @ b)) \<approx> |
280 "(map f ((a::'a list) @ b)) \<approx> |
293 ((map f a) ::'a list) @ (map f b)" |
281 ((map f a) ::'a list) @ (map f b)" |
294 by simp (rule list_eq_refl) |
282 by simp (rule list_eq_refl) |
295 |
283 |
296 thm list.induct |
284 ML {* val rty = @{typ "'a list"} *} |
297 lemma list_induct_hol4: |
285 ML {* val qty = @{typ "'a fset"} *} |
298 fixes P :: "'a list \<Rightarrow> bool" |
286 ML {* val rel = @{term "list_eq"} *} |
299 assumes a: "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))" |
287 ML {* val rel_eqv = (#equiv_thm o hd) (quotdata_lookup @{context}) *} |
300 shows "\<forall>l. (P l)" |
288 ML {* val rel_refl = @{thm list_eq_refl} *} |
301 using a |
289 ML {* val quot = @{thm QUOTIENT_fset} *} |
302 apply (rule_tac allI) |
290 ML {* val rsp_thms = |
303 apply (induct_tac "l") |
291 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} |
304 apply (simp) |
292 @ @{thms ho_all_prs ho_ex_prs} *} |
305 apply (metis) |
293 ML {* val trans2 = @{thm QUOT_TYPE_I_fset.R_trans2} *} |
306 done |
294 ML {* val reps_same = @{thm QUOT_TYPE_I_fset.REPS_same} *} |
307 |
295 ML {* val defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *} |
308 ML {* (atomize_thm @{thm list_induct_hol4}) *} |
296 (* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *) |
309 |
|
310 ML {* regularise (prop_of (atomize_thm @{thm list_induct_hol4})) @{typ "'a list"} @{term "op \<approx>"} @{context} *} |
|
311 |
|
312 prove list_induct_r: {* |
|
313 build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a list"} @{term "op \<approx>"} @{context} *} |
|
314 apply (simp only: equiv_res_forall[OF equiv_list_eq]) |
|
315 thm RIGHT_RES_FORALL_REGULAR |
|
316 apply (rule RIGHT_RES_FORALL_REGULAR) |
|
317 prefer 2 |
|
318 apply (assumption) |
|
319 apply (metis) |
|
320 done |
|
321 |
|
322 (* The all_prs and ex_prs should be proved for the instance... *) |
|
323 ML {* |
297 ML {* |
324 fun r_mk_comb_tac_fset ctxt = |
298 val consts = [@{const_name "Nil"}, @{const_name "Cons"}, |
325 r_mk_comb_tac ctxt @{typ "'a list"} @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
299 @{const_name "membship"}, @{const_name "card1"}, |
326 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}) |
300 @{const_name "append"}, @{const_name "fold1"}, |
327 *} |
301 @{const_name "map"}]; |
328 |
302 *} |
329 |
303 |
330 ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *} |
304 ML {* fun lift_thm_fset lthy t = |
331 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
305 lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t |
332 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
306 *} |
333 |
307 |
334 ML {* val rty = @{typ "'a list"} *} |
308 lemma eq_r: "a = b \<Longrightarrow> a \<approx> b" |
335 |
309 by (simp add: list_eq_refl) |
336 ML {* |
310 |
337 fun r_mk_comb_tac_fset ctxt = |
311 ML {* lift_thm_fset @{context} @{thm m1} *} |
338 r_mk_comb_tac ctxt rty @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
312 ML {* lift_thm_fset @{context} @{thm m2} *} |
339 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}) |
313 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *} |
340 *} |
314 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *} |
341 |
315 ML {* lift_thm_fset @{context} @{thm card1_suc} *} |
342 |
316 ML {* lift_thm_fset @{context} @{thm map_append} *} |
343 ML {* trm_r *} |
317 ML {* lift_thm_fset @{context} @{thm eq_r[OF append_assoc]} *} |
344 prove list_induct_tr: trm_r |
|
345 apply (atomize(full)) |
|
346 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
347 done |
|
348 |
|
349 prove list_induct_t: trm |
|
350 apply (simp only: list_induct_tr[symmetric]) |
|
351 apply (tactic {* rtac thm 1 *}) |
|
352 done |
|
353 |
|
354 thm m2 |
|
355 ML {* atomize_thm @{thm m2} *} |
|
356 |
|
357 prove m2_r_p: {* |
|
358 build_regularize_goal (atomize_thm @{thm m2}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
|
359 apply (simp add: equiv_res_forall[OF equiv_list_eq]) |
|
360 done |
|
361 |
|
362 ML {* val m2_r = @{thm m2_r_p} OF [atomize_thm @{thm m2}] *} |
|
363 ML {* val m2_t_g = build_repabs_goal @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *} |
|
364 ML {* val m2_t = build_repabs_term @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *} |
|
365 prove m2_t_p: m2_t_g |
|
366 apply (atomize(full)) |
|
367 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
368 done |
|
369 |
|
370 prove m2_t: m2_t |
|
371 apply (simp only: m2_t_p[symmetric]) |
|
372 apply (tactic {* rtac m2_r 1 *}) |
|
373 done |
|
374 |
|
375 lemma id_apply2 [simp]: "id x \<equiv> x" |
|
376 by (simp add: id_def) |
|
377 |
|
378 ML {* val quot = @{thm QUOTIENT_fset} *} |
|
379 ML {* val abs = findabs @{typ "'a list"} (prop_of (atomize_thm @{thm list_induct_hol4})) *} |
|
380 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
|
381 |
|
382 ML {* |
|
383 fun simp_lam_prs lthy thm = |
|
384 simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm) |
|
385 handle _ => thm |
|
386 *} |
|
387 |
|
388 ML {* val m2_t' = simp_lam_prs @{context} @{thm m2_t} *} |
|
389 |
|
390 ML {* val ithm = simp_allex_prs @{context} quot m2_t' *} |
|
391 |
|
392 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *} |
|
393 ML {* ObjectLogic.rulify rthm *} |
|
394 |
|
395 |
|
396 ML {* val card1_suc_a = atomize_thm @{thm card1_suc} *} |
|
397 |
|
398 prove card1_suc_r_p: {* |
|
399 build_regularize_goal (atomize_thm @{thm card1_suc}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
|
400 apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq]) |
|
401 done |
|
402 |
|
403 ML {* val card1_suc_r = @{thm card1_suc_r_p} OF [atomize_thm @{thm card1_suc}] *} |
|
404 ML {* val card1_suc_t_g = build_repabs_goal @{context} card1_suc_r consts @{typ "'a list"} @{typ "'a fset"} *} |
|
405 ML {* val card1_suc_t = build_repabs_term @{context} card1_suc_r consts @{typ "'a list"} @{typ "'a fset"} *} |
|
406 prove card1_suc_t_p: card1_suc_t_g |
|
407 apply (atomize(full)) |
|
408 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
409 done |
|
410 |
|
411 prove card1_suc_t: card1_suc_t |
|
412 apply (simp only: card1_suc_t_p[symmetric]) |
|
413 apply (tactic {* rtac card1_suc_r 1 *}) |
|
414 done |
|
415 |
|
416 ML {* val card1_suc_t_n = @{thm card1_suc_t} *} |
|
417 ML {* val card1_suc_t' = simp_lam_prs @{context} @{thm card1_suc_t} *} |
|
418 ML {* val ithm = simp_allex_prs @{context} quot card1_suc_t' *} |
|
419 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *} |
|
420 ML {* val qthm = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} rthm *} |
|
421 ML {* ObjectLogic.rulify qthm *} |
|
422 |
318 |
423 thm fold1.simps(2) |
319 thm fold1.simps(2) |
424 thm list.recs(2) |
320 thm list.recs(2) |
425 thm map_append |
|
426 |
321 |
427 ML {* val ind_r_a = atomize_thm @{thm list.induct} *} |
322 ML {* val ind_r_a = atomize_thm @{thm list.induct} *} |
428 (* prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
323 (* prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
429 ML_prf {* fun tac ctxt = |
324 ML_prf {* fun tac ctxt = |
430 (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
325 (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
436 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 @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context} *} |
437 ML {* |
332 ML {* |
438 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 @{typ "'a list"} @{typ "'a fset"} |
439 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); |
440 *} |
335 *} |
441 |
336 (*prove rg |
442 prove rg |
|
443 apply(atomize(full)) |
337 apply(atomize(full)) |
444 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 *}) |
445 done |
339 done*) |
446 |
|
447 ML {* val ind_r_t = |
340 ML {* val ind_r_t = |
448 Toplevel.program (fn () => |
341 Toplevel.program (fn () => |
449 repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
342 repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
450 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
343 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
451 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}) |
344 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}) |
452 ) |
345 ) |
453 *} |
346 *} |
454 ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t *} |
347 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *} |
|
348 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
|
349 ML {* val ind_r_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms ind_r_t *} |
455 lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1" |
350 lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1" |
456 apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10) |
351 apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10) |
457 done |
352 done |
458 |
353 |
459 ML {* val ind_r_l1 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l *} |
354 ML {* val ind_r_l1 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l *} |
461 ML {* val ind_r_l3 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l2 *} |
356 ML {* val ind_r_l3 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l2 *} |
462 ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *} |
357 ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *} |
463 ML {* val ind_r_a = simp_allex_prs @{context} quot ind_r_l4 *} |
358 ML {* val ind_r_a = simp_allex_prs @{context} quot ind_r_l4 *} |
464 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *} |
359 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *} |
465 ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *} |
360 ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *} |
466 ML {* val ind_r_d = repeat_eqsubst_thm @{context} fset_defs_sym ind_r_a1 *} |
361 ML {* val defs_sym = add_lower_defs @{context} defs *} |
|
362 ML {* val ind_r_d = repeat_eqsubst_thm @{context} defs_sym ind_r_a1 *} |
467 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} |
363 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} |
468 ML {* ObjectLogic.rulify ind_r_s *} |
364 ML {* ObjectLogic.rulify ind_r_s *} |
469 |
365 |
470 ML {* |
366 ML {* |
471 fun lift thm = |
367 fun lift_thm_fset_note name thm lthy = |
472 let |
|
473 val ind_r_a = atomize_thm thm; |
|
474 val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context}; |
|
475 val ind_r_t = |
|
476 repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
|
477 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
|
478 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}); |
|
479 val ind_r_l = simp_lam_prs @{context} ind_r_t; |
|
480 val ind_r_a = simp_allex_prs @{context} quot ind_r_l; |
|
481 val ind_r_d = repeat_eqsubst_thm @{context} fset_defs_sym ind_r_a; |
|
482 val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d |
|
483 in |
|
484 ObjectLogic.rulify ind_r_s |
|
485 end |
|
486 *} |
|
487 ML fset_defs |
|
488 |
|
489 lemma eq_r: "a = b \<Longrightarrow> a \<approx> b" |
|
490 by (simp add: list_eq_refl) |
|
491 |
|
492 |
|
493 ML {* lift @{thm m2} *} |
|
494 ML {* lift @{thm m1} *} |
|
495 ML {* lift @{thm list_eq.intros(4)} *} |
|
496 ML {* lift @{thm list_eq.intros(5)} *} |
|
497 ML {* lift @{thm card1_suc} *} |
|
498 ML {* lift @{thm map_append} *} |
|
499 ML {* lift @{thm eq_r[OF append_assoc]} *} |
|
500 |
|
501 thm |
|
502 |
|
503 |
|
504 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
|
505 notation ( output) "Trueprop" ("#_" [1000] 1000) |
|
506 |
|
507 (* |
|
508 ML {* |
|
509 fun lift_theorem_fset_aux thm lthy = |
|
510 let |
368 let |
511 val ((_, [novars]), lthy2) = Variable.import true [thm] lthy; |
369 val lifted_thm = lift_thm_fset lthy thm; |
512 val goal = build_repabs_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"}; |
|
513 val cgoal = cterm_of @{theory} goal; |
|
514 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal); |
|
515 val tac = transconv_fset_tac' @{context}; |
|
516 val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac); |
|
517 val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm))) |
|
518 val nthm2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same QUOT_TYPE_I_fset.thm10} nthm; |
|
519 val [nthm3] = ProofContext.export lthy2 lthy [nthm2] |
|
520 in |
|
521 nthm3 |
|
522 end |
|
523 *} |
|
524 *) |
|
525 |
|
526 (* |
|
527 ML {* lift_theorem_fset_aux @{thm m1} @{context} *} |
|
528 ML {* |
|
529 fun lift_theorem_fset name thm lthy = |
|
530 let |
|
531 val lifted_thm = lift_theorem_fset_aux thm lthy; |
|
532 val (_, lthy2) = note (name, lifted_thm) lthy; |
370 val (_, lthy2) = note (name, lifted_thm) lthy; |
533 in |
371 in |
534 lthy2 |
372 lthy2 |
535 end; |
373 end; |
536 *} |
374 *} |
537 *) |
375 |
538 |
376 local_setup {* |
539 local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *} |
377 lift_thm_fset_note @{binding "m1l"} @{thm m1} #> |
540 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *} |
378 lift_thm_fset_note @{binding "m2l"} @{thm m2} #> |
541 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *} |
379 lift_thm_fset_note @{binding "leqi4l"} @{thm list_eq.intros(4)} #> |
542 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *} |
380 lift_thm_fset_note @{binding "leqi5l"} @{thm list_eq.intros(5)} |
543 thm m1_lift |
381 *} |
544 thm leqi4_lift |
382 thm m1l |
545 thm leqi5_lift |
383 thm m2l |
546 thm m2_lift |
384 thm leqi4l |
547 ML {* @{thm card1_suc_r} OF [card1_suc_f] *} |
385 thm leqi5l |
548 (*ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"} |
|
549 (@{thm card1_suc_r} OF [card1_suc_f]) @{context}) *}*) |
|
550 (*local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*) |
|
551 |
|
552 thm leqi4_lift |
|
553 ML {* |
|
554 val (nam, typ) = hd (Term.add_vars (prop_of @{thm leqi4_lift}) []) |
|
555 val (_, l) = dest_Type typ |
|
556 val t = Type ("FSet.fset", l) |
|
557 val v = Var (nam, t) |
|
558 val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v) |
|
559 *} |
|
560 |
|
561 |
386 |
562 end |
387 end |