456 val invsj = nth invs (j - 1) |
457 val invsj = nth invs (j - 1) |
457 |> map (fold Thm.forall_elim cqsj') |
458 |> map (fold Thm.forall_elim cqsj') |
458 |> map (fold Thm.elim_implies [case_hypj']) |
459 |> map (fold Thm.elim_implies [case_hypj']) |
459 |> map (fold Thm.elim_implies agsj') |
460 |> map (fold Thm.elim_implies agsj') |
460 |
461 |
461 val compat = get_compat_thm thy compat_store eqvtsi eqvtsj invsi invsj i j cctxi cctxj |
462 val compat = get_compat_thm ctxt compat_store eqvtsi eqvtsj invsi invsj i j cctxi cctxj |
462 |
463 |
463 in |
464 in |
464 (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *) |
465 (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *) |
465 |> Thm.implies_elim RLj_import |
466 |> Thm.implies_elim RLj_import |
466 (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *) |
467 (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *) |
467 |> (fn it => trans OF [it, compat]) |
468 |> (fn it => trans OF [it, compat]) |
468 (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *) |
469 (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *) |
469 |> (fn it => trans OF [y_eq_rhsj'h, it]) |
470 |> (fn it => trans OF [y_eq_rhsj'h, it]) |
470 (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *) |
471 (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *) |
471 |> fold_rev (Thm.implies_intr o cprop_of) Ghsj' |
472 |> fold_rev (Thm.implies_intr o Thm.cprop_of) Ghsj' |
472 |> fold_rev (Thm.implies_intr o cprop_of) agsj' |
473 |> fold_rev (Thm.implies_intr o Thm.cprop_of) agsj' |
473 (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *) |
474 (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *) |
474 |> Thm.implies_intr (cprop_of y_eq_rhsj'h) |
475 |> Thm.implies_intr (Thm.cprop_of y_eq_rhsj'h) |
475 |> Thm.implies_intr (cprop_of lhsi_eq_lhsj') |
476 |> Thm.implies_intr (Thm.cprop_of lhsi_eq_lhsj') |
476 |> fold_rev Thm.forall_intr (cterm_of thy h :: cqsj') |
477 |> fold_rev Thm.forall_intr (Thm.cterm_of ctxt h :: cqsj') |
477 end |
478 end |
478 |
479 |
479 (* nominal *) |
480 (* nominal *) |
480 fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses replems eqvtlems invlems |
481 fun mk_uniqueness_case ctxt |
481 clausei = |
482 globals G f ihyp ih_intro G_cases compat_store clauses replems eqvtlems invlems clausei = |
482 let |
483 let |
|
484 val thy = Proof_Context.theory_of ctxt |
|
485 |
483 val Globals {x, y, ranT, fvar, ...} = globals |
486 val Globals {x, y, ranT, fvar, ...} = globals |
484 val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei |
487 val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei |
485 val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs |
488 val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs |
486 |
489 |
487 val ih_intro_case = |
490 val ih_intro_case = |
488 full_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [case_hyp]) |
491 full_simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp]) |
489 ih_intro |
492 ih_intro |
490 |
493 |
491 fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = |
494 fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = |
492 (llRI RS ih_intro_case) |
495 (llRI RS ih_intro_case) |
493 |> fold_rev (Thm.implies_intr o cprop_of) CCas |
496 |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas |
494 |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs |
497 |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs |
495 |
498 |
496 val existence = fold (curry op COMP o prep_RC) RCs lGI |
499 val existence = fold (curry op COMP o prep_RC) RCs lGI |
497 |
500 |
498 val P = cterm_of thy (mk_eq (y, rhsC)) |
501 val P = Thm.cterm_of ctxt (mk_eq (y, rhsC)) |
499 val G_lhs_y = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y))) |
502 val G_lhs_y = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (G $ lhs $ y))) |
500 |
503 |
501 val unique_clauses = |
504 val unique_clauses = |
502 map2 (mk_uniqueness_clause thy globals compat_store eqvtlems invlems clausei) clauses replems |
505 map2 (mk_uniqueness_clause ctxt globals compat_store eqvtlems invlems clausei) clauses replems |
503 |
506 |
504 fun elim_implies_eta A AB = |
507 fun elim_implies_eta A AB = |
505 Thm.bicompose {flatten = false, match = true, incremented = false} (false, A, 0) 1 AB |
508 Thm.bicompose NONE {flatten = false, match = true, incremented = false} (false, A, 0) 1 AB |
506 |> Seq.list_of |> the_single |
509 |> Seq.list_of |> the_single |
507 |
510 |
508 val uniqueness = G_cases |
511 val uniqueness = G_cases |
509 |> Thm.forall_elim (cterm_of thy lhs) |
512 |> Thm.forall_elim (Thm.cterm_of ctxt lhs) |
510 |> Thm.forall_elim (cterm_of thy y) |
513 |> Thm.forall_elim (Thm.cterm_of ctxt y) |
511 |> Thm.forall_elim P |
514 |> Thm.forall_elim P |
512 |> Thm.elim_implies G_lhs_y |
515 |> Thm.elim_implies G_lhs_y |
513 |> fold elim_implies_eta unique_clauses |
516 |> fold elim_implies_eta unique_clauses |
514 |> Thm.implies_intr (cprop_of G_lhs_y) |
517 |> Thm.implies_intr (Thm.cprop_of G_lhs_y) |
515 |> Thm.forall_intr (cterm_of thy y) |
518 |> Thm.forall_intr (Thm.cterm_of ctxt y) |
516 |
519 |
517 val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *) |
520 val P2 = Thm.cterm_of ctxt (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *) |
518 |
521 |
519 val exactly_one = |
522 val exactly_one = |
520 ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)] |
523 ex1I |> instantiate' [SOME (Thm.ctyp_of ctxt ranT)] [SOME P2, SOME (Thm.cterm_of ctxt rhsC)] |
521 |> curry (op COMP) existence |
524 |> curry (op COMP) existence |
522 |> curry (op COMP) uniqueness |
525 |> curry (op COMP) uniqueness |
523 |> simplify |
526 |> simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp RS sym]) |
524 (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [case_hyp RS sym]) |
527 |> Thm.implies_intr (Thm.cprop_of case_hyp) |
525 |> Thm.implies_intr (cprop_of case_hyp) |
528 |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags |
526 |> fold_rev (Thm.implies_intr o cprop_of) ags |
|
527 |> fold_rev Thm.forall_intr cqs |
529 |> fold_rev Thm.forall_intr cqs |
528 |
530 |
529 val function_value = |
531 val function_value = |
530 existence |
532 existence |
531 |> Thm.implies_intr ihyp |
533 |> Thm.implies_intr ihyp |
532 |> Thm.implies_intr (cprop_of case_hyp) |
534 |> Thm.implies_intr (Thm.cprop_of case_hyp) |
533 |> Thm.forall_intr (cterm_of thy x) |
535 |> Thm.forall_intr (Thm.cterm_of ctxt x) |
534 |> Thm.forall_elim (cterm_of thy lhs) |
536 |> Thm.forall_elim (Thm.cterm_of ctxt lhs) |
535 |> curry (op RS) refl |
537 |> curry (op RS) refl |
536 in |
538 in |
537 (exactly_one, function_value) |
539 (exactly_one, function_value) |
538 end |
540 end |
539 |
541 |
540 |
542 |
541 (* nominal *) |
543 (* nominal *) |
542 fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim G_eqvt invariant f_def = |
544 fun prove_stuff ctxt |
|
545 globals G f R clauses complete compat compat_store G_elim G_eqvt invariant f_def = |
543 let |
546 let |
544 val Globals {h, domT, ranT, x, ...} = globals |
547 val Globals {h, domT, ranT, x, ...} = globals |
545 val thy = Proof_Context.theory_of ctxt |
|
546 |
548 |
547 (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *) |
549 (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *) |
548 val ihyp = Logic.all_const domT $ Abs ("z", domT, |
550 val ihyp = Logic.all_const domT $ Abs ("z", domT, |
549 Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), |
551 Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), |
550 HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $ |
552 HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $ |
551 Abs ("y", ranT, G $ Bound 1 $ Bound 0)))) |
553 Abs ("y", ranT, G $ Bound 1 $ Bound 0)))) |
552 |> cterm_of thy |
554 |> Thm.cterm_of ctxt |
553 |
555 |
554 val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0 |
556 val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0 |
555 val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex) |
557 val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex) |
556 val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un) |
558 val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un) |
557 |> instantiate' [] [NONE, SOME (cterm_of thy h)] |
559 |> instantiate' [] [NONE, SOME (Thm.cterm_of ctxt h)] |
558 val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at})) |
560 val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at})) |
559 val ih_inv = ihyp_thm RS (invariant COMP (f_def RS @{thm fundef_ex1_prop})) |
561 val ih_inv = ihyp_thm RS (invariant COMP (f_def RS @{thm fundef_ex1_prop})) |
560 |
562 |
561 val _ = trace_msg (K "Proving Replacement lemmas...") |
563 val _ = trace_msg (K "Proving Replacement lemmas...") |
562 val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses |
564 val repLemmas = map (mk_replacement_lemma ctxt h ih_elim) clauses |
563 |
565 |
564 val _ = trace_msg (K "Proving Equivariance lemmas...") |
566 val _ = trace_msg (K "Proving Equivariance lemmas...") |
565 val eqvtLemmas = map (mk_eqvt_lemma thy ih_eqvt) clauses |
567 val eqvtLemmas = map (mk_eqvt_lemma ctxt ih_eqvt) clauses |
566 |
568 |
567 val _ = trace_msg (K "Proving Invariance lemmas...") |
569 val _ = trace_msg (K "Proving Invariance lemmas...") |
568 val invLemmas = map (mk_invariant_lemma thy ih_inv) clauses |
570 val invLemmas = map (mk_invariant_lemma ctxt ih_inv) clauses |
569 |
571 |
570 val _ = trace_msg (K "Proving cases for unique existence...") |
572 val _ = trace_msg (K "Proving cases for unique existence...") |
571 val (ex1s, values) = |
573 val (ex1s, values) = |
572 split_list (map (mk_uniqueness_case thy globals G f |
574 split_list (map (mk_uniqueness_case ctxt globals G f |
573 ihyp ih_intro G_elim compat_store clauses repLemmas eqvtLemmas invLemmas) clauses) |
575 ihyp ih_intro G_elim compat_store clauses repLemmas eqvtLemmas invLemmas) clauses) |
574 |
576 |
575 val _ = trace_msg (K "Proving: Graph is a function") |
577 val _ = trace_msg (K "Proving: Graph is a function") |
576 val graph_is_function = complete |
578 val graph_is_function = complete |
577 |> Thm.forall_elim_vars 0 |
579 |> Thm.forall_elim_vars 0 |
578 |> fold (curry op COMP) ex1s |
580 |> fold (curry op COMP) ex1s |
579 |> Thm.implies_intr (ihyp) |
581 |> Thm.implies_intr ihyp |
580 |> Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x))) |
582 |> Thm.implies_intr (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_acc domT R $ x))) |
581 |> Thm.forall_intr (cterm_of thy x) |
583 |> Thm.forall_intr (Thm.cterm_of ctxt x) |
582 |> (fn it => Drule.compose (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *) |
584 |> (fn it => Drule.compose (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *) |
583 |> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it) |
585 |> (fn it => |
|
586 fold (Thm.forall_intr o Thm.cterm_of ctxt o Var) (Term.add_vars (Thm.prop_of it) []) it) |
584 |
587 |
585 val goalstate = |
588 val goalstate = |
586 Conjunction.intr (Conjunction.intr (Conjunction.intr graph_is_function complete) invariant) G_eqvt |
589 Conjunction.intr (Conjunction.intr (Conjunction.intr graph_is_function complete) invariant) G_eqvt |
587 |> Thm.close_derivation |
590 |> Thm.close_derivation |
588 |> Goal.protect 0 |
591 |> Goal.protect 0 |
589 |> fold_rev (Thm.implies_intr o cprop_of) compat |
592 |> fold_rev (Thm.implies_intr o Thm.cprop_of) compat |
590 |> Thm.implies_intr (cprop_of complete) |
593 |> Thm.implies_intr (Thm.cprop_of complete) |
591 |> Thm.implies_intr (cprop_of invariant) |
594 |> Thm.implies_intr (Thm.cprop_of invariant) |
592 |> Thm.implies_intr (cprop_of G_eqvt) |
595 |> Thm.implies_intr (Thm.cprop_of G_eqvt) |
593 in |
596 in |
594 (goalstate, values) |
597 (goalstate, values) |
595 end |
598 end |
596 |
599 |
597 (* wrapper -- restores quantifiers in rule specifications *) |
600 (* wrapper -- restores quantifiers in rule specifications *) |
598 fun inductive_def (binding as ((R, T), _)) intrs lthy = |
601 fun inductive_def (binding as ((R, T), _)) intrs lthy = |
599 let |
602 let |
600 val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) = |
603 val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) = |
601 lthy |
604 lthy |
602 |> Local_Theory.conceal |
605 |> Proof_Context.concealed |
603 |> Inductive.add_inductive_i |
606 |> Inductive.add_inductive_i |
604 {quiet_mode = true, |
607 {quiet_mode = true, |
605 verbose = ! trace, |
608 verbose = ! trace, |
606 alt_name = Binding.empty, |
609 alt_name = Binding.empty, |
607 coind = false, |
610 coind = false, |
706 domT = domT, |
709 domT = domT, |
707 ranT = ranT}, |
710 ranT = ranT}, |
708 ctxt') |
711 ctxt') |
709 end |
712 end |
710 |
713 |
711 fun inst_RC thy fvar f (rcfix, rcassm, rcarg) = |
714 fun inst_RC ctxt fvar f (rcfix, rcassm, rcarg) = |
712 let |
715 let |
713 fun inst_term t = subst_bound(f, abstract_over (fvar, t)) |
716 fun inst_term t = subst_bound(f, abstract_over (fvar, t)) |
714 in |
717 in |
715 (rcfix, map (Thm.assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg) |
718 (rcfix, map (Thm.assume o Thm.cterm_of ctxt o inst_term o Thm.prop_of) rcassm, inst_term rcarg) |
716 end |
719 end |
717 |
720 |
718 |
721 |
719 |
722 |
720 (********************************************************** |
723 (********************************************************** |
721 * PROVING THE RULES |
724 * PROVING THE RULES |
722 **********************************************************) |
725 **********************************************************) |
723 |
726 |
724 fun mk_psimps thy globals R clauses valthms f_iff graph_is_function = |
727 fun mk_psimps ctxt globals R clauses valthms f_iff graph_is_function = |
725 let |
728 let |
726 val Globals {domT, z, ...} = globals |
729 val Globals {domT, z, ...} = globals |
727 |
730 |
728 fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm = |
731 fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm = |
729 let |
732 let |
730 val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *) |
733 val lhs_acc = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *) |
731 val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *) |
734 val z_smaller = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *) |
732 in |
735 in |
733 ((Thm.assume z_smaller) RS ((Thm.assume lhs_acc) RS acc_downward)) |
736 ((Thm.assume z_smaller) RS ((Thm.assume lhs_acc) RS acc_downward)) |
734 |> (fn it => it COMP graph_is_function) |
737 |> (fn it => it COMP graph_is_function) |
735 |> Thm.implies_intr z_smaller |
738 |> Thm.implies_intr z_smaller |
736 |> Thm.forall_intr (cterm_of thy z) |
739 |> Thm.forall_intr (Thm.cterm_of ctxt z) |
737 |> (fn it => it COMP valthm) |
740 |> (fn it => it COMP valthm) |
738 |> Thm.implies_intr lhs_acc |
741 |> Thm.implies_intr lhs_acc |
739 |> asm_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [f_iff]) |
742 |> asm_simplify (put_simpset HOL_basic_ss ctxt addsimps [f_iff]) |
740 |> fold_rev (Thm.implies_intr o cprop_of) ags |
743 |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags |
741 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
744 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
742 end |
745 end |
743 in |
746 in |
744 map2 mk_psimp clauses valthms |
747 map2 mk_psimp clauses valthms |
745 end |
748 end |
749 |
752 |
750 |
753 |
751 val acc_subset_induct = @{thm predicate1I} RS @{thm accp_subset_induct} |
754 val acc_subset_induct = @{thm predicate1I} RS @{thm accp_subset_induct} |
752 |
755 |
753 |
756 |
754 fun mk_partial_induct_rule thy globals R complete_thm clauses = |
757 fun mk_partial_induct_rule ctxt globals R complete_thm clauses = |
755 let |
758 let |
756 val Globals {domT, x, z, a, P, D, ...} = globals |
759 val Globals {domT, x, z, a, P, D, ...} = globals |
757 val acc_R = mk_acc domT R |
760 val acc_R = mk_acc domT R |
758 |
761 |
759 val x_D = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x))) |
762 val x_D = Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (D $ x))) |
760 val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a)) |
763 val a_D = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (D $ a)) |
761 |
764 |
762 val D_subset = cterm_of thy (Logic.all x |
765 val D_subset = Thm.cterm_of ctxt (Logic.all x |
763 (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x)))) |
766 (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x)))) |
764 |
767 |
765 val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *) |
768 val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *) |
766 Logic.all x (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), |
769 Logic.all x (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), |
767 Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x), |
770 Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x), |
768 HOLogic.mk_Trueprop (D $ z))))) |
771 HOLogic.mk_Trueprop (D $ z))))) |
769 |> cterm_of thy |
772 |> Thm.cterm_of ctxt |
770 |
773 |
771 (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) |
774 (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) |
772 val ihyp = Logic.all_const domT $ Abs ("z", domT, |
775 val ihyp = Logic.all_const domT $ Abs ("z", domT, |
773 Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), |
776 Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), |
774 HOLogic.mk_Trueprop (P $ Bound 0))) |
777 HOLogic.mk_Trueprop (P $ Bound 0))) |
775 |> cterm_of thy |
778 |> Thm.cterm_of ctxt |
776 |
779 |
777 val aihyp = Thm.assume ihyp |
780 val aihyp = Thm.assume ihyp |
778 |
781 |
779 fun prove_case clause = |
782 fun prove_case clause = |
780 let |
783 let |
781 val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...}, |
784 val ClauseInfo {cdata = ClauseContext {ctxt = ctxt', qs, cqs, ags, gs, lhs, case_hyp, ...}, |
782 RCs, qglr = (oqs, _, _, _), ...} = clause |
785 RCs, qglr = (oqs, _, _, _), ...} = clause |
783 |
786 |
784 val case_hyp_conv = K (case_hyp RS eq_reflection) |
787 val case_hyp_conv = K (case_hyp RS eq_reflection) |
785 local open Conv in |
788 local open Conv in |
786 val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D |
789 val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D |
787 val sih = |
790 val sih = |
788 fconv_rule (Conv.binder_conv |
791 fconv_rule (Conv.binder_conv |
789 (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp |
792 (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt') aihyp |
790 end |
793 end |
791 |
794 |
792 fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih |
795 fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih |
793 |> Thm.forall_elim (cterm_of thy rcarg) |
796 |> Thm.forall_elim (Thm.cterm_of ctxt rcarg) |
794 |> Thm.elim_implies llRI |
797 |> Thm.elim_implies llRI |
795 |> fold_rev (Thm.implies_intr o cprop_of) CCas |
798 |> fold_rev (Thm.implies_intr o Thm.cprop_of) CCas |
796 |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs |
799 |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) RIvs |
797 |
800 |
798 val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *) |
801 val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *) |
799 |
802 |
800 val step = HOLogic.mk_Trueprop (P $ lhs) |
803 val step = HOLogic.mk_Trueprop (P $ lhs) |
801 |> fold_rev (curry Logic.mk_implies o prop_of) P_recs |
804 |> fold_rev (curry Logic.mk_implies o Thm.prop_of) P_recs |
802 |> fold_rev (curry Logic.mk_implies) gs |
805 |> fold_rev (curry Logic.mk_implies) gs |
803 |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs)) |
806 |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs)) |
804 |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |
807 |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |
805 |> cterm_of thy |
808 |> Thm.cterm_of ctxt |
806 |
809 |
807 val P_lhs = Thm.assume step |
810 val P_lhs = Thm.assume step |
808 |> fold Thm.forall_elim cqs |
811 |> fold Thm.forall_elim cqs |
809 |> Thm.elim_implies lhs_D |
812 |> Thm.elim_implies lhs_D |
810 |> fold Thm.elim_implies ags |
813 |> fold Thm.elim_implies ags |
811 |> fold Thm.elim_implies P_recs |
814 |> fold Thm.elim_implies P_recs |
812 |
815 |
813 val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x)) |
816 val res = |
|
817 Thm.cterm_of ctxt (HOLogic.mk_Trueprop (P $ x)) |
814 |> Conv.arg_conv (Conv.arg_conv case_hyp_conv) |
818 |> Conv.arg_conv (Conv.arg_conv case_hyp_conv) |
815 |> Thm.symmetric (* P lhs == P x *) |
819 |> Thm.symmetric (* P lhs == P x *) |
816 |> (fn eql => Thm.equal_elim eql P_lhs) (* "P x" *) |
820 |> (fn eql => Thm.equal_elim eql P_lhs) (* "P x" *) |
817 |> Thm.implies_intr (cprop_of case_hyp) |
821 |> Thm.implies_intr (Thm.cprop_of case_hyp) |
818 |> fold_rev (Thm.implies_intr o cprop_of) ags |
822 |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags |
819 |> fold_rev Thm.forall_intr cqs |
823 |> fold_rev Thm.forall_intr cqs |
820 in |
824 in |
821 (res, step) |
825 (res, step) |
822 end |
826 end |
823 |
827 |
841 |> Thm.implies_intr D_dcl |
845 |> Thm.implies_intr D_dcl |
842 |> Thm.implies_intr D_subset |
846 |> Thm.implies_intr D_subset |
843 |
847 |
844 val simple_induct_rule = |
848 val simple_induct_rule = |
845 subset_induct_rule |
849 subset_induct_rule |
846 |> Thm.forall_intr (cterm_of thy D) |
850 |> Thm.forall_intr (Thm.cterm_of ctxt D) |
847 |> Thm.forall_elim (cterm_of thy acc_R) |
851 |> Thm.forall_elim (Thm.cterm_of ctxt acc_R) |
848 |> assume_tac 1 |> Seq.hd |
852 |> atac 1 |> Seq.hd |
849 |> (curry op COMP) (acc_downward |
853 |> (curry op COMP) (acc_downward |
850 |> (instantiate' [SOME (ctyp_of thy domT)] |
854 |> (instantiate' [SOME (Thm.ctyp_of ctxt domT)] |
851 (map (SOME o cterm_of thy) [R, x, z])) |
855 (map (SOME o Thm.cterm_of ctxt) [R, x, z])) |
852 |> Thm.forall_intr (cterm_of thy z) |
856 |> Thm.forall_intr (Thm.cterm_of ctxt z) |
853 |> Thm.forall_intr (cterm_of thy x)) |
857 |> Thm.forall_intr (Thm.cterm_of ctxt x)) |
854 |> Thm.forall_intr (cterm_of thy a) |
858 |> Thm.forall_intr (Thm.cterm_of ctxt a) |
855 |> Thm.forall_intr (cterm_of thy P) |
859 |> Thm.forall_intr (Thm.cterm_of ctxt P) |
856 in |
860 in |
857 simple_induct_rule |
861 simple_induct_rule |
858 end |
862 end |
859 |
863 |
860 |
864 |
861 (* FIXME: broken by design *) |
865 (* FIXME: broken by design *) |
862 fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause = |
866 fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause = |
863 let |
867 let |
864 val thy = Proof_Context.theory_of ctxt |
|
865 val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...}, |
868 val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...}, |
866 qglr = (oqs, _, _, _), ...} = clause |
869 qglr = (oqs, _, _, _), ...} = clause |
867 val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs) |
870 val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs) |
868 |> fold_rev (curry Logic.mk_implies) gs |
871 |> fold_rev (curry Logic.mk_implies) gs |
869 |> cterm_of thy |
872 |> Thm.cterm_of ctxt |
870 in |
873 in |
871 Goal.init goal |
874 Goal.init goal |
872 |> (SINGLE (resolve_tac [accI] 1)) |> the |
875 |> (SINGLE (resolve_tac ctxt [accI] 1)) |> the |
873 |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1)) |> the |
876 |> (SINGLE (eresolve_tac ctxt [Thm.forall_elim_vars 0 R_cases] 1)) |> the |
874 |> (SINGLE (auto_tac ctxt)) |> the |
877 |> (SINGLE (auto_tac ctxt)) |> the |
875 |> Goal.conclude |
878 |> Goal.conclude |
876 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
879 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
877 end |
880 end |
878 |
881 |
882 |
885 |
883 val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule} |
886 val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule} |
884 val wf_in_rel = @{thm Fun_Def.wf_in_rel} |
887 val wf_in_rel = @{thm Fun_Def.wf_in_rel} |
885 val in_rel_def = @{thm Fun_Def.in_rel_def} |
888 val in_rel_def = @{thm Fun_Def.in_rel_def} |
886 |
889 |
887 fun mk_nest_term_case thy globals R' ihyp clause = |
890 fun mk_nest_term_case ctxt globals R' ihyp clause = |
888 let |
891 let |
889 val Globals {z, ...} = globals |
892 val Globals {z, ...} = globals |
890 val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree, |
893 val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree, |
891 qglr=(oqs, _, _, _), ...} = clause |
894 qglr=(oqs, _, _, _), ...} = clause |
892 |
895 |
893 val ih_case = |
896 val ih_case = |
894 full_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [case_hyp]) |
897 full_simplify (put_simpset HOL_basic_ss ctxt addsimps [case_hyp]) |
895 ihyp |
898 ihyp |
896 |
899 |
897 fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = |
900 fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = |
898 let |
901 let |
899 val used = (u @ sub) |
902 val used = (u @ sub) |
900 |> map (fn (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm) |
903 |> map (fn (ctx,thm) => Function_Context_Tree.export_thm ctxt ctx thm) |
901 |
904 |
902 val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs) |
905 val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs) |
903 |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *) |
906 |> fold_rev (curry Logic.mk_implies o Thm.prop_of) used (* additional hyps *) |
904 |> Function_Ctx_Tree.export_term (fixes, assumes) |
907 |> Function_Context_Tree.export_term (fixes, assumes) |
905 |> fold_rev (curry Logic.mk_implies o prop_of) ags |
908 |> fold_rev (curry Logic.mk_implies o Thm.prop_of) ags |
906 |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |
909 |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |
907 |> cterm_of thy |
910 |> Thm.cterm_of ctxt |
908 |
911 |
909 val thm = Thm.assume hyp |
912 val thm = Thm.assume hyp |
910 |> fold Thm.forall_elim cqs |
913 |> fold Thm.forall_elim cqs |
911 |> fold Thm.elim_implies ags |
914 |> fold Thm.elim_implies ags |
912 |> Function_Ctx_Tree.import_thm thy (fixes, assumes) |
915 |> Function_Context_Tree.import_thm ctxt (fixes, assumes) |
913 |> fold Thm.elim_implies used (* "(arg, lhs) : R'" *) |
916 |> fold Thm.elim_implies used (* "(arg, lhs) : R'" *) |
914 |
917 |
915 val z_eq_arg = HOLogic.mk_Trueprop (mk_eq (z, arg)) |
918 val z_eq_arg = HOLogic.mk_Trueprop (mk_eq (z, arg)) |
916 |> cterm_of thy |> Thm.assume |
919 |> Thm.cterm_of ctxt |> Thm.assume |
917 |
920 |
918 val acc = thm COMP ih_case |
921 val acc = thm COMP ih_case |
919 val z_acc_local = acc |
922 val z_acc_local = acc |
920 |> Conv.fconv_rule |
923 |> Conv.fconv_rule |
921 (Conv.arg_conv (Conv.arg_conv (K (Thm.symmetric (z_eq_arg RS eq_reflection))))) |
924 (Conv.arg_conv (Conv.arg_conv (K (Thm.symmetric (z_eq_arg RS eq_reflection))))) |
922 |
925 |
923 val ethm = z_acc_local |
926 val ethm = z_acc_local |
924 |> Function_Ctx_Tree.export_thm thy (fixes, |
927 |> Function_Context_Tree.export_thm ctxt (fixes, |
925 z_eq_arg :: case_hyp :: ags @ assumes) |
928 z_eq_arg :: case_hyp :: ags @ assumes) |
926 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
929 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
927 |
930 |
928 val sub' = sub @ [(([],[]), acc)] |
931 val sub' = sub @ [(([],[]), acc)] |
929 in |
932 in |
930 (sub', (hyp :: hyps, ethm :: thms)) |
933 (sub', (hyp :: hyps, ethm :: thms)) |
931 end |
934 end |
932 | step _ _ _ _ = raise Match |
935 | step _ _ _ _ = raise Match |
933 in |
936 in |
934 Function_Ctx_Tree.traverse_tree step tree |
937 Function_Context_Tree.traverse_tree step tree |
935 end |
938 end |
936 |
939 |
937 |
940 |
938 fun mk_nest_term_rule thy globals R R_cases clauses = |
941 fun mk_nest_term_rule ctxt globals R R_cases clauses = |
939 let |
942 let |
940 val Globals { domT, x, z, ... } = globals |
943 val Globals { domT, x, z, ... } = globals |
941 val acc_R = mk_acc domT R |
944 val acc_R = mk_acc domT R |
942 |
945 |
943 val R' = Free ("R", fastype_of R) |
946 val R' = Free ("R", fastype_of R) |
946 val inrel_R = Const (@{const_name Fun_Def.in_rel}, |
949 val inrel_R = Const (@{const_name Fun_Def.in_rel}, |
947 HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel |
950 HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel |
948 |
951 |
949 val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, |
952 val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, |
950 (domT --> domT --> boolT) --> boolT) $ R') |
953 (domT --> domT --> boolT) --> boolT) $ R') |
951 |> cterm_of thy (* "wf R'" *) |
954 |> Thm.cterm_of ctxt (* "wf R'" *) |
952 |
955 |
953 (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *) |
956 (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *) |
954 val ihyp = Logic.all_const domT $ Abs ("z", domT, |
957 val ihyp = Logic.all_const domT $ Abs ("z", domT, |
955 Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x), |
958 Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x), |
956 HOLogic.mk_Trueprop (acc_R $ Bound 0))) |
959 HOLogic.mk_Trueprop (acc_R $ Bound 0))) |
957 |> cterm_of thy |
960 |> Thm.cterm_of ctxt |
958 |
961 |
959 val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0 |
962 val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0 |
960 |
963 |
961 val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x)) |
964 val R_z_x = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (R $ z $ x)) |
962 |
965 |
963 val (hyps, cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([], []) |
966 val (hyps, cases) = fold (mk_nest_term_case ctxt globals R' ihyp_a) clauses ([], []) |
964 in |
967 in |
965 R_cases |
968 R_cases |
966 |> Thm.forall_elim (cterm_of thy z) |
969 |> Thm.forall_elim (Thm.cterm_of ctxt z) |
967 |> Thm.forall_elim (cterm_of thy x) |
970 |> Thm.forall_elim (Thm.cterm_of ctxt x) |
968 |> Thm.forall_elim (cterm_of thy (acc_R $ z)) |
971 |> Thm.forall_elim (Thm.cterm_of ctxt (acc_R $ z)) |
969 |> curry op COMP (Thm.assume R_z_x) |
972 |> curry op COMP (Thm.assume R_z_x) |
970 |> fold_rev (curry op COMP) cases |
973 |> fold_rev (curry op COMP) cases |
971 |> Thm.implies_intr R_z_x |
974 |> Thm.implies_intr R_z_x |
972 |> Thm.forall_intr (cterm_of thy z) |
975 |> Thm.forall_intr (Thm.cterm_of ctxt z) |
973 |> (fn it => it COMP accI) |
976 |> (fn it => it COMP accI) |
974 |> Thm.implies_intr ihyp |
977 |> Thm.implies_intr ihyp |
975 |> Thm.forall_intr (cterm_of thy x) |
978 |> Thm.forall_intr (Thm.cterm_of ctxt x) |
976 |> (fn it => Drule.compose (it, 2, wf_induct_rule)) |
979 |> (fn it => Drule.compose (it, 2, wf_induct_rule)) |
977 |> curry op RS (Thm.assume wfR') |
980 |> curry op RS (Thm.assume wfR') |
978 |> forall_intr_vars |
981 |> forall_intr_vars |
979 |> (fn it => it COMP allI) |
982 |> (fn it => it COMP allI) |
980 |> fold Thm.implies_intr hyps |
983 |> fold Thm.implies_intr hyps |
981 |> Thm.implies_intr wfR' |
984 |> Thm.implies_intr wfR' |
982 |> Thm.forall_intr (cterm_of thy R') |
985 |> Thm.forall_intr (Thm.cterm_of ctxt R') |
983 |> Thm.forall_elim (cterm_of thy (inrel_R)) |
986 |> Thm.forall_elim (Thm.cterm_of ctxt (inrel_R)) |
984 |> curry op RS wf_in_rel |
987 |> curry op RS wf_in_rel |
985 |> full_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [in_rel_def]) |
988 |> full_simplify (put_simpset HOL_basic_ss ctxt addsimps [in_rel_def]) |
986 |> Thm.forall_intr (cterm_of thy Rrel) |
989 |> Thm.forall_intr (Thm.cterm_of ctxt Rrel) |
987 end |
990 end |
988 |
991 |
989 |
992 |
990 |
993 |
991 (* nominal *) |
994 (* nominal *) |
1012 val clauses = map (mk_clause_context x ctxt') abstract_qglrs |
1015 val clauses = map (mk_clause_context x ctxt') abstract_qglrs |
1013 |
1016 |
1014 val n = length abstract_qglrs |
1017 val n = length abstract_qglrs |
1015 |
1018 |
1016 fun build_tree (ClauseContext { ctxt, rhs, ...}) = |
1019 fun build_tree (ClauseContext { ctxt, rhs, ...}) = |
1017 Function_Ctx_Tree.mk_tree (fname, fT) h ctxt rhs |
1020 Function_Context_Tree.mk_tree (fname, fT) h ctxt rhs |
1018 |
1021 |
1019 val trees = map build_tree clauses |
1022 val trees = map build_tree clauses |
1020 val RCss = map find_calls trees |
1023 val RCss = map find_calls trees |
1021 |
1024 |
1022 val ((G, GIntro_thms, G_elim, G_induct), lthy) = |
1025 val ((G, GIntro_thms, G_elim, G_induct), lthy) = |
1023 PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy |
1026 PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy |
1024 |
1027 |
1025 val ((f, (_, f_defthm)), lthy) = |
1028 val ((f, (_, f_defthm)), lthy) = |
1026 PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy |
1029 PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy |
1027 |
1030 |
1028 val RCss = map (map (inst_RC (Proof_Context.theory_of lthy) fvar f)) RCss |
1031 val RCss = map (map (inst_RC lthy fvar f)) RCss |
1029 val trees = map (Function_Ctx_Tree.inst_tree (Proof_Context.theory_of lthy) fvar f) trees |
1032 val trees = map (Function_Context_Tree.inst_tree lthy fvar f) trees |
1030 |
1033 |
1031 val ((R, RIntro_thmss, R_elim), lthy) = |
1034 val ((R, RIntro_thmss, R_elim), lthy) = |
1032 PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy |
1035 PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy |
1033 |
1036 |
1034 val (_, lthy) = |
1037 val (_, lthy) = |
1035 Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy |
1038 Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy |
1036 |
1039 |
1037 val newthy = Proof_Context.theory_of lthy |
1040 val newthy = Proof_Context.theory_of lthy |
1038 val clauses = map (transfer_clause_ctx newthy) clauses |
1041 val clauses = map (transfer_clause_ctx newthy) clauses |
1039 |
1042 |
1040 val cert = cterm_of (Proof_Context.theory_of lthy) |
1043 val cert = Thm.cterm_of lthy |
1041 |
1044 |
1042 val xclauses = PROFILE "xclauses" |
1045 val xclauses = PROFILE "xclauses" |
1043 (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees |
1046 (@{map 7} (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees |
1044 RCss GIntro_thms) RIntro_thmss |
1047 RCss GIntro_thms) RIntro_thmss |
1045 |
1048 |
1046 val complete = |
1049 val complete = |
1047 mk_completeness globals clauses abstract_qglrs |> cert |> Thm.assume |
1050 mk_completeness globals clauses abstract_qglrs |> cert |> Thm.assume |
1048 |
1051 |