472 - Ball (Respects ?E) ?P = All ?P |
472 - Ball (Respects ?E) ?P = All ?P |
473 - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q |
473 - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q |
474 |
474 |
475 *) |
475 *) |
476 |
476 |
477 lemma my_equiv_res_forallR: |
|
478 fixes P::"'a \<Rightarrow> bool" |
|
479 fixes Q::"'b \<Rightarrow> bool" |
|
480 assumes b: "(All Q) \<longrightarrow> (All P)" |
|
481 shows "(All Q) \<longrightarrow> Ball (Respects E) P" |
|
482 using b by auto |
|
483 |
|
484 lemma my_equiv_res_forallL: |
|
485 fixes P::"'a \<Rightarrow> bool" |
|
486 fixes Q::"'b \<Rightarrow> bool" |
|
487 assumes a: "EQUIV E" |
|
488 assumes b: "(All Q) \<longrightarrow> (All P)" |
|
489 shows "Ball (Respects E) P \<longrightarrow> (All P)" |
|
490 using a b |
|
491 unfolding EQUIV_def |
|
492 by (metis IN_RESPECTS) |
|
493 |
|
494 lemma my_equiv_res_existsR: |
|
495 fixes P::"'a \<Rightarrow> bool" |
|
496 fixes Q::"'b \<Rightarrow> bool" |
|
497 assumes a: "EQUIV E" |
|
498 and b: "(Ex Q) \<longrightarrow> (Ex P)" |
|
499 shows "(Ex Q) \<longrightarrow> Bex (Respects E) P" |
|
500 using a b |
|
501 unfolding EQUIV_def |
|
502 by (metis IN_RESPECTS) |
|
503 |
|
504 lemma my_equiv_res_existsL: |
|
505 fixes P::"'a \<Rightarrow> bool" |
|
506 fixes Q::"'b \<Rightarrow> bool" |
|
507 assumes b: "(Ex Q) \<longrightarrow> (Ex P)" |
|
508 shows "Bex (Respects E) Q \<longrightarrow> (Ex P)" |
|
509 using b |
|
510 by (auto) |
|
511 |
|
512 lemma universal_twice: |
477 lemma universal_twice: |
513 assumes *: "\<And>x. (P x \<longrightarrow> Q x)" |
478 assumes *: "\<And>x. (P x \<longrightarrow> Q x)" |
514 shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)" |
479 shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)" |
515 using * by auto |
480 using * by auto |
516 |
481 |
529 |> cat_lines |
494 |> cat_lines |
530 val _ = tracing (s ^ "\n" ^ prems_str) |
495 val _ = tracing (s ^ "\n" ^ prems_str) |
531 in |
496 in |
532 Seq.single thm |
497 Seq.single thm |
533 end |
498 end |
534 |
499 |
535 fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))] |
500 fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))] |
536 *} |
|
537 |
|
538 ML {* |
|
539 fun REGULARIZE_tac' lthy rel_refl rel_eqv = |
|
540 (REPEAT1 o FIRST1) |
|
541 [(K (print_tac "start")) THEN' (K no_tac), |
|
542 DT lthy "1" (rtac rel_refl), |
|
543 DT lthy "2" atac, |
|
544 DT lthy "3" (rtac @{thm universal_twice}), |
|
545 DT lthy "4" (rtac @{thm impI} THEN' atac), |
|
546 DT lthy "5" (rtac @{thm implication_twice}), |
|
547 DT lthy "6" (rtac @{thm my_equiv_res_forallR}), |
|
548 DT lthy "7" (rtac (rel_eqv RS @{thm my_equiv_res_existsR})), |
|
549 (* For a = b \<longrightarrow> a \<approx> b *) |
|
550 DT lthy "8" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), |
|
551 DT lthy "9" (rtac @{thm RIGHT_RES_FORALL_REGULAR})] |
|
552 *} |
501 *} |
553 |
502 |
554 ML {* |
503 ML {* |
555 fun regularize_tac ctxt rel_eqv rel_refl = |
504 fun regularize_tac ctxt rel_eqv rel_refl = |
556 (ObjectLogic.full_atomize_tac) THEN' |
505 (ObjectLogic.full_atomize_tac) THEN' |
557 REPEAT_ALL_NEW (FIRST' [ |
506 REPEAT_ALL_NEW (FIRST' |
558 rtac rel_refl, |
507 [(K (print_tac "start")) THEN' (K no_tac), |
559 atac, |
|
560 rtac @{thm universal_twice}, |
|
561 rtac @{thm impI} THEN' atac, |
|
562 rtac @{thm implication_twice}, |
|
563 EqSubst.eqsubst_tac ctxt [0] |
|
564 [(@{thm equiv_res_forall} OF [rel_eqv]), |
|
565 (@{thm equiv_res_exists} OF [rel_eqv])], |
|
566 (* For a = b \<longrightarrow> a \<approx> b *) |
|
567 (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), |
|
568 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
|
569 ]); |
|
570 *} |
|
571 |
|
572 ML {* |
|
573 fun regularize_tac ctxt rel_eqv rel_refl = |
|
574 (ObjectLogic.full_atomize_tac) THEN' |
|
575 REPEAT_ALL_NEW (FIRST' |
|
576 [(K (print_tac "start")) THEN' (K no_tac), |
|
577 DT ctxt "1" (rtac rel_refl), |
508 DT ctxt "1" (rtac rel_refl), |
578 DT ctxt "2" atac, |
509 DT ctxt "2" atac, |
579 DT ctxt "3" (rtac @{thm universal_twice}), |
510 DT ctxt "3" (rtac @{thm universal_twice}), |
580 DT ctxt "4" (rtac @{thm impI} THEN' atac), |
511 DT ctxt "4" (rtac @{thm impI} THEN' atac), |
581 DT ctxt "5" (rtac @{thm implication_twice}), |
512 DT ctxt "5" (rtac @{thm implication_twice}), |
586 DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), |
517 DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), |
587 DT ctxt "8" (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
518 DT ctxt "8" (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
588 ]); |
519 ]); |
589 *} |
520 *} |
590 |
521 |
591 thm RIGHT_RES_FORALL_REGULAR |
522 lemma move_forall: "(\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)) \<Longrightarrow> ((\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y))" |
|
523 by auto |
|
524 |
|
525 lemma move_exists: "((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))" |
|
526 by auto |
|
527 |
|
528 lemma [mono]: "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)" |
|
529 by blast |
|
530 |
|
531 lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P" |
|
532 by auto |
|
533 |
|
534 lemma ball_respects_refl: |
|
535 fixes P Q::"'a \<Rightarrow> bool" |
|
536 and x::"'a" |
|
537 assumes a: "EQUIV R2" |
|
538 and b: "\<And>f. Q (f x) \<longrightarrow> P (f x)" |
|
539 shows "(Ball (Respects (R1 ===> R2)) (\<lambda>f. Q (f x)) \<longrightarrow> All (\<lambda>f. P (f x)))" |
|
540 apply(rule impI) |
|
541 apply(rule allI) |
|
542 apply(drule_tac x="\<lambda>y. f x" in bspec) |
|
543 apply(simp add: Respects_def IN_RESPECTS) |
|
544 apply(rule impI) |
|
545 using a EQUIV_REFL_SYM_TRANS[of "R2"] |
|
546 apply(simp add: REFL_def) |
|
547 using b |
|
548 apply(simp) |
|
549 done |
|
550 |
|
551 lemma bex_respects_refl: |
|
552 fixes P Q::"'a \<Rightarrow> bool" |
|
553 and x::"'a" |
|
554 assumes a: "EQUIV R2" |
|
555 and b: "\<And>f. P (f x) \<longrightarrow> Q (f x)" |
|
556 shows "(Ex (\<lambda>f. P (f x))) \<longrightarrow> (Bex (Respects (R1 ===> R2)) (\<lambda>f. Q (f x)))" |
|
557 apply(rule impI) |
|
558 apply(erule exE) |
|
559 thm bexI |
|
560 apply(rule_tac x="\<lambda>y. f x" in bexI) |
|
561 using b |
|
562 apply(simp) |
|
563 apply(simp add: Respects_def IN_RESPECTS) |
|
564 apply(rule impI) |
|
565 using a EQUIV_REFL_SYM_TRANS[of "R2"] |
|
566 apply(simp add: REFL_def) |
|
567 done |
|
568 |
|
569 (* FIXME: OPTION_EQUIV, PAIR_EQUIV, ... *) |
|
570 ML {* |
|
571 fun equiv_tac rel_eqvs = |
|
572 REPEAT_ALL_NEW(FIRST' [ |
|
573 FIRST' (map rtac rel_eqvs), |
|
574 rtac @{thm IDENTITY_EQUIV}, |
|
575 rtac @{thm LIST_EQUIV} |
|
576 ]) |
|
577 *} |
|
578 |
|
579 ML {* |
|
580 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) |
|
581 *} |
|
582 |
|
583 ML {* |
|
584 fun regularize_tac ctxt rel_eqvs rel_refl = |
|
585 let |
|
586 val subs1 = map (fn x => @{thm equiv_res_forall} OF [x]) rel_eqvs |
|
587 val subs2 = map (fn x => @{thm equiv_res_exists} OF [x]) rel_eqvs |
|
588 val subs = map (fn x => @{thm eq_reflection} OF [x]) (subs1 @ subs2) |
|
589 in |
|
590 (ObjectLogic.full_atomize_tac) THEN' |
|
591 (simp_tac ((Simplifier.context ctxt empty_ss) addsimps subs)) |
|
592 THEN' |
|
593 REPEAT_ALL_NEW (FIRST' [ |
|
594 (rtac @{thm RIGHT_RES_FORALL_REGULAR}), |
|
595 (rtac @{thm LEFT_RES_EXISTS_REGULAR}), |
|
596 (resolve_tac (Inductive.get_monos ctxt)), |
|
597 (rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
|
598 (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])), |
|
599 rtac @{thm move_forall}, |
|
600 rtac @{thm move_exists}, |
|
601 (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl) |
|
602 ]) |
|
603 end |
|
604 *} |
592 |
605 |
593 section {* Injections of REP and ABSes *} |
606 section {* Injections of REP and ABSes *} |
594 |
607 |
595 (* |
608 (* |
596 Injecting REPABS means: |
609 Injecting REPABS means: |
1283 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1292 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1284 val aps = find_aps (prop_of rthm') (term_of concl) |
1293 val aps = find_aps (prop_of rthm') (term_of concl) |
1285 in |
1294 in |
1286 rtac rule THEN' RANGE [ |
1295 rtac rule THEN' RANGE [ |
1287 rtac rthm', |
1296 rtac rthm', |
1288 regularize_tac lthy rel_eqv rel_refl, |
1297 regularize_tac lthy [rel_eqv] rel_refl, |
1289 REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms), |
1298 REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms), |
1290 clean_tac lthy quot defs reps_same absrep aps |
1299 clean_tac lthy quot defs reps_same absrep aps |
1291 ] |
1300 ] |
1292 end 1) lthy |
1301 end 1) lthy |
1293 *} |
1302 *} |