353 val tac = |
353 val tac = |
354 (compose_tac (false, lpi, 2)) THEN_ALL_NEW |
354 (compose_tac (false, lpi, 2)) THEN_ALL_NEW |
355 (quotient_tac quot); |
355 (quotient_tac quot); |
356 val gc = Drule.strip_imp_concl (cprop_of lpi); |
356 val gc = Drule.strip_imp_concl (cprop_of lpi); |
357 val t = Goal.prove_internal [] gc (fn _ => tac 1) |
357 val t = Goal.prove_internal [] gc (fn _ => tac 1) |
358 val _ = tracing (Syntax.string_of_term @{context} (prop_of t)) |
358 val ts = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t |
|
359 val te = @{thm eq_reflection} OF [ts] |
|
360 val _ = tracing (Syntax.string_of_term @{context} (term_of ctrm)); |
|
361 val _ = tracing (Syntax.string_of_term @{context} (term_of (Thm.lhs_of te))); |
|
362 val insts = matching_prs (ProofContext.theory_of ctxt) (term_of ctrm) (term_of (Thm.lhs_of te)); |
|
363 val ti = Drule.instantiate insts te; |
|
364 val _ = tracing (Syntax.string_of_term @{context} (term_of (cprop_of ti))); |
359 in |
365 in |
360 Conv.rewr_conv (eq_reflection OF [t]) ctrm |
366 Conv.rewr_conv (eq_reflection OF [ti]) ctrm |
361 end |
367 end |
362 | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm |
368 | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm |
363 | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm |
369 | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm |
364 | _ => Conv.all_conv ctrm |
370 | _ => Conv.all_conv ctrm |
365 *} |
|
366 |
|
367 ML {* |
|
368 lambda_prs_conv @{context} quot |
|
369 *} |
371 *} |
370 |
372 |
371 ML {* |
373 ML {* |
372 fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) => |
374 fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) => |
373 CONVERSION |
375 CONVERSION |
374 (Conv.params_conv ~1 (fn ctxt => |
376 (Conv.params_conv ~1 (fn ctxt => |
375 (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv |
377 (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv |
376 Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) |
378 Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) |
377 *} |
379 *} |
378 |
380 |
379 (* |
381 ML {* |
380 ML {* |
382 val ctrm = @{cterm "((ABS_fset ---> id) ---> id) (\<lambda>x. id ((REP_fset ---> id) x))"} |
381 lambda_prs_conv @{context} quot |
383 val pat = @{cpat "((ABS_fset ---> id) ---> id) (\<lambda>x. ?f ((REP_fset ---> id) x))"} |
382 @{cterm "((ABS_fset ---> id) ---> id) (\<lambda>x\<Colon>'a list \<Rightarrow> bool. id ((f ((REP_fset ---> id) x) ((REP_fset ---> id) x))))"} |
384 *} |
383 *} |
385 |
384 |
386 ML {* matching_prs @{theory} (term_of pat) (term_of ctrm); *} |
385 ML {* |
387 |
386 @{cterm "((ABS_fset ---> id) ---> id) |
388 ML {* |
387 (\<lambda>P. |
389 lambda_prs_conv @{context} quot ctrm |
388 All ((REP_fset ---> id) |
390 *} |
389 (\<lambda>list. |
391 |
|
392 |
|
393 ML {* |
|
394 val t = @{thm LAMBDA_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT] IDENTITY_QUOTIENT]} |
|
395 val te = @{thm eq_reflection} OF [t] |
|
396 val ts = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] te |
|
397 val tl = Thm.lhs_of ts |
|
398 *} |
|
399 |
|
400 ML {* val inst = matching_prs @{theory} (term_of tl) (term_of ctrm); *} |
|
401 |
|
402 ML {* val trm = @{cterm "(((ABS_fset ---> id) ---> id) (\<lambda>(P\<Colon>('a list \<Rightarrow> bool)). |
|
403 All ((REP_fset ---> id) (\<lambda>(list\<Colon>('a list)). |
390 (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset [])) \<longrightarrow> |
404 (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset [])) \<longrightarrow> |
391 (\<forall>a. All ((REP_fset ---> id) |
405 True \<longrightarrow> (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset list))))))"} *} |
392 (\<lambda>list. |
406 |
393 (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset list)) \<longrightarrow> |
407 ML {* |
394 (ABS_fset ---> id) ((REP_fset ---> id) P) |
408 lambda_prs_conv @{context} quot trm |
395 (REP_fset (ABS_fset (a # REP_fset (ABS_fset list))))))) \<longrightarrow> |
409 *} |
396 (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset list)))))"} |
410 |
397 |
411 |
398 *} |
412 |
399 *) |
413 (*ML {* val trm = @{cterm "(((ABS_fset ---> id) ---> id) (\<lambda>(?P\<Colon>('a list \<Rightarrow> bool)). (g (id P)"} *} *) |
|
414 |
|
415 |
400 |
416 |
401 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
417 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
402 apply(tactic {* procedure_tac @{thm list.induct} @{context} 1 *}) |
418 apply(tactic {* procedure_tac @{thm list.induct} @{context} 1 *}) |
403 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
419 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
404 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) |
420 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) |
405 apply(tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *}) |
421 apply(tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *}) |
406 oops |
422 apply(tactic {* lambda_prs_tac @{context} quot 1 *}) |
407 |
423 |
408 (* |
424 |
|
425 ML_prf {* Subgoal.focus @{context} 1 (#goal (Isar.goal ())) *} |
|
426 |
|
427 apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *}) |
|
428 |
|
429 |
409 thm LAMBDA_PRS |
430 thm LAMBDA_PRS |
410 apply(tactic {* EqSubst.eqsubst_tac @{context} [0] @{thms LAMBDA_PRS} 1 *}) |
431 apply(tactic {* EqSubst.eqsubst_tac @{context} [0] @{thms LAMBDA_PRS} 1 *}) |
411 |
432 |
412 apply(tactic {* (lambda_prs_tac @{context} quot) 1 *}) |
433 apply(tactic {* (lambda_prs_tac @{context} quot) 1 *}) |
413 |
434 |
414 apply(tactic {* REPEAT_ALL_NEW (lambda_prs_tac @{context} quot) 1 *}) |
435 apply(tactic {* REPEAT_ALL_NEW (lambda_prs_tac @{context} quot) 1 *}) |
415 |
436 |
416 apply(tactic {* clean_tac @{context} quot defs reps_same 1 *}) |
437 apply(tactic {* clean_tac @{context} quot defs reps_same 1 *}) |
417 apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *}) |
438 apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *}) |
418 ML {* lift_thm_fset @{context} @{thm list.induct} *} |
439 ML {* lift_thm_fset @{context} @{thm list.induct} *} |
419 ML {* lift_thm_g_fset @{context} @{thm list.induct} @{term "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"} *}*) |
440 ML {* lift_thm_g_fset @{context} @{thm list.induct} @{term "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"} *} |
420 |
441 |
421 |
442 |
422 lemma "\<forall>f x xa. fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
443 |
|
444 |
|
445 thm map_append |
|
446 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
423 apply(tactic {* procedure_tac @{thm map_append} @{context} 1 *}) |
447 apply(tactic {* procedure_tac @{thm map_append} @{context} 1 *}) |
424 oops |
448 apply(tactic {* prepare_tac 1 *}) |
425 |
449 thm map_append |
426 |
450 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) |
427 lemma "fmap f (FUNION (x::'b fset) (y::'b fset)) = FUNION (fmap f x) (fmap f y)" |
451 done |
428 apply(tactic {* procedure_tac @{thm map_append} @{context} 1 *}) |
452 |
429 oops |
|
430 |
453 |
431 |
454 |
432 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" |
455 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" |
433 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) |
456 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) |
434 done |
457 done |
436 ML {* atomize_thm @{thm fold1.simps(2)} *} |
459 ML {* atomize_thm @{thm fold1.simps(2)} *} |
437 (*ML {* lift_thm_g_fset @{context} @{thm fold1.simps(2)} @{term "FOLD f g (z::'b) (INSERT a x) = |
460 (*ML {* lift_thm_g_fset @{context} @{thm fold1.simps(2)} @{term "FOLD f g (z::'b) (INSERT a x) = |
438 (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"} *}*) |
461 (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"} *}*) |
439 |
462 |
440 |
463 |
441 |
464 *) |
442 ML {* lift_thm_g_fset @{context} @{thm map_append} @{term "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"} *} |
465 ML {* lift_thm_g_fset @{context} @{thm map_append} @{term "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"} *} |
443 |
466 |
444 |
467 |
445 ML {* cterm_of @{theory} (atomize_goal @{theory} @{term "\<forall>x xa a. x = xa \<Longrightarrow> INSERT a x = INSERT a xa"}) *} |
468 ML {* cterm_of @{theory} (atomize_goal @{theory} @{term "\<forall>x xa a. x = xa \<Longrightarrow> INSERT a x = INSERT a xa"}) *} |
446 |
469 |
447 |
470 |
448 ML {* lift_thm_fset @{context} @{thm map_append} *} |
471 ML {* lift_thm_fset @{context} @{thm map_append} *} |
449 |
472 |
450 |
473 |
451 |
474 (* |
452 apply(tactic {* procedure_tac @{thm m1} @{context} 1 *}) |
475 apply(tactic {* procedure_tac @{thm m1} @{context} 1 *}) |
453 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
476 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
454 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) |
477 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) |
455 apply(tactic {* clean_tac @{context} quot defs reps_same 1 *}) |
478 apply(tactic {* clean_tac @{context} quot defs reps_same 1 *}) |
456 apply(tactic {* TRY' (REPEAT_ALL_NEW (allex_prs_tac @{context} quot)) 1 *}) |
479 apply(tactic {* TRY' (REPEAT_ALL_NEW (allex_prs_tac @{context} quot)) 1 *}) |
457 apply(tactic {* TRY' (REPEAT_ALL_NEW (lambda_prs_tac @{context} quot)) 1 *}) |
480 apply(tactic {* TRY' (REPEAT_ALL_NEW (lambda_prs_tac @{context} quot)) 1 *}) |
458 ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *} |
481 ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *} |
459 apply(tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1*}) |
482 apply(tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1*}) |
460 apply(tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *}) |
483 apply(tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *}) |
461 |
484 *) |
462 |
485 |
463 |
486 |
464 |
487 |
465 (*ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *}*) |
488 (*ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *}*) |
466 |
489 |