164 |
164 |
165 fun inst t = subst_bounds (rev qs, t) |
165 fun inst t = subst_bounds (rev qs, t) |
166 val gs = map inst pre_gs |
166 val gs = map inst pre_gs |
167 val lhs = inst pre_lhs |
167 val lhs = inst pre_lhs |
168 val rhs = inst pre_rhs |
168 val rhs = inst pre_rhs |
169 |
169 |
170 val cqs = map (cterm_of thy) qs |
170 val cqs = map (cterm_of thy) qs |
171 val ags = map (assume o cterm_of thy) gs |
171 val ags = map (assume o cterm_of thy) gs |
172 |
172 |
173 val case_hyp = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs)))) |
173 val case_hyp = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs)))) |
174 in |
174 in |
175 ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs, |
175 ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs, |
176 cqs = cqs, ags = ags, case_hyp = case_hyp } |
176 cqs = cqs, ags = ags, case_hyp = case_hyp } |
177 end |
177 end |
178 |
178 |
179 |
179 |
180 (* lowlevel term function *) |
180 (* lowlevel term function *) |
181 fun abstract_over_list vs body = |
181 fun abstract_over_list vs body = |
182 let |
182 let |
183 exception SAME; |
183 exception SAME; |
322 let |
322 let |
323 val Globals {h, y, x, fvar, ...} = globals |
323 val Globals {h, y, x, fvar, ...} = globals |
324 val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei |
324 val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei |
325 val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej |
325 val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej |
326 |
326 |
327 val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} |
327 val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} |
328 = mk_clause_context x ctxti cdescj |
328 = mk_clause_context x ctxti cdescj |
329 |
329 |
330 val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj' |
330 val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj' |
331 val compat = get_compat_thm thy compat_store i j cctxi cctxj |
331 val compat = get_compat_thm thy compat_store i j cctxi cctxj |
332 val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj |
332 val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj |
333 |
333 |
334 val RLj_import = |
334 val RLj_import = |
335 RLj |> fold forall_elim cqsj' |
335 RLj |> fold forall_elim cqsj' |
336 |> fold Thm.elim_implies agsj' |
336 |> fold Thm.elim_implies agsj' |
337 |> fold Thm.elim_implies Ghsj' |
337 |> fold Thm.elim_implies Ghsj' |
338 |
338 |
339 val y_eq_rhsj'h = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h)))) |
339 val y_eq_rhsj'h = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h)))) |
464 HOLogic.mk_Trueprop (Gvar $ lhs $ rhs) |
464 HOLogic.mk_Trueprop (Gvar $ lhs $ rhs) |
465 |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs |
465 |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs |
466 |> fold_rev (curry Logic.mk_implies) gs |
466 |> fold_rev (curry Logic.mk_implies) gs |
467 |> fold_rev Logic.all (fvar :: qs) |
467 |> fold_rev Logic.all (fvar :: qs) |
468 end |
468 end |
469 |
469 |
470 val G_intros = map2 mk_GIntro clauses RCss |
470 val G_intros = map2 mk_GIntro clauses RCss |
471 |
471 |
472 val (GIntro_thms, (G, G_elim, G_induct, lthy)) = |
472 val (GIntro_thms, (G, G_elim, G_induct, lthy)) = |
473 FundefInductiveWrap.inductive_def G_intros ((dest_Free Gvar, NoSyn), lthy) |
473 FundefInductiveWrap.inductive_def G_intros ((dest_Free Gvar, NoSyn), lthy) |
474 in |
474 in |
475 ((G, GIntro_thms, G_elim, G_induct), lthy) |
475 ((G, GIntro_thms, G_elim, G_induct), lthy) |
476 end |
476 end |
477 |
477 |
478 |
478 |
479 |
479 |
480 fun define_function fdefname (fname, mixfix) domT ranT G default lthy = |
480 fun define_function fdefname (fname, mixfix) domT ranT G default lthy = |
481 let |
481 let |
482 val f_def = |
482 val f_def = |
483 Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $ |
483 Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $ |
484 Abs ("y", ranT, G $ Bound 1 $ Bound 0)) |
484 Abs ("y", ranT, G $ Bound 1 $ Bound 0)) |
485 |> Syntax.check_term lthy |
485 |> Syntax.check_term lthy |
486 |
486 |
487 val ((f, (_, f_defthm)), lthy) = |
487 val ((f, (_, f_defthm)), lthy) = |
488 LocalTheory.define Thm.internalK ((function_name fname, mixfix), ((fdefname, []), f_def)) lthy |
488 LocalTheory.define Thm.internalK ((Name.binding (function_name fname), mixfix), ((Name.binding fdefname, []), f_def)) lthy |
489 in |
489 in |
490 ((f, f_defthm), lthy) |
490 ((f, f_defthm), lthy) |
491 end |
491 end |
492 |
492 |
493 |
493 |
505 |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |
505 |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |
506 (* "!!qs xs. CS ==> G => (r, lhs) : R" *) |
506 (* "!!qs xs. CS ==> G => (r, lhs) : R" *) |
507 |
507 |
508 val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss |
508 val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss |
509 |
509 |
510 val (RIntro_thmss, (R, R_elim, _, lthy)) = |
510 val (RIntro_thmss, (R, R_elim, _, lthy)) = |
511 fold_burrow FundefInductiveWrap.inductive_def R_intross ((dest_Free Rvar, NoSyn), lthy) |
511 fold_burrow FundefInductiveWrap.inductive_def R_intross ((dest_Free Rvar, NoSyn), lthy) |
512 in |
512 in |
513 ((R, RIntro_thmss, R_elim), lthy) |
513 ((R, RIntro_thmss, R_elim), lthy) |
514 end |
514 end |
515 |
515 |
516 |
516 |
517 fun fix_globals domT ranT fvar ctxt = |
517 fun fix_globals domT ranT fvar ctxt = |
518 let |
518 let |
519 val ([h, y, x, z, a, D, P, Pbool],ctxt') = |
519 val ([h, y, x, z, a, D, P, Pbool],ctxt') = |
520 Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt |
520 Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt |
521 in |
521 in |
522 (Globals {h = Free (h, domT --> ranT), |
522 (Globals {h = Free (h, domT --> ranT), |
523 y = Free (y, ranT), |
523 y = Free (y, ranT), |
524 x = Free (x, domT), |
524 x = Free (x, domT), |
544 end |
544 end |
545 |
545 |
546 |
546 |
547 |
547 |
548 (********************************************************** |
548 (********************************************************** |
549 * PROVING THE RULES |
549 * PROVING THE RULES |
550 **********************************************************) |
550 **********************************************************) |
551 |
551 |
552 fun mk_psimps thy globals R clauses valthms f_iff graph_is_function = |
552 fun mk_psimps thy globals R clauses valthms f_iff graph_is_function = |
553 let |
553 let |
554 val Globals {domT, z, ...} = globals |
554 val Globals {domT, z, ...} = globals |
555 |
555 |
556 fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm = |
556 fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm = |
557 let |
557 let |
558 val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *) |
558 val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *) |
559 val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *) |
559 val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *) |
560 in |
560 in |
561 ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward)) |
561 ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward)) |
562 |> (fn it => it COMP graph_is_function) |
562 |> (fn it => it COMP graph_is_function) |
563 |> implies_intr z_smaller |
563 |> implies_intr z_smaller |
564 |> forall_intr (cterm_of thy z) |
564 |> forall_intr (cterm_of thy z) |
565 |> (fn it => it COMP valthm) |
565 |> (fn it => it COMP valthm) |
566 |> implies_intr lhs_acc |
566 |> implies_intr lhs_acc |
567 |> asm_simplify (HOL_basic_ss addsimps [f_iff]) |
567 |> asm_simplify (HOL_basic_ss addsimps [f_iff]) |
568 |> fold_rev (implies_intr o cprop_of) ags |
568 |> fold_rev (implies_intr o cprop_of) ags |
569 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
569 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
570 end |
570 end |
571 in |
571 in |
583 |
583 |
584 fun mk_partial_induct_rule thy globals R complete_thm clauses = |
584 fun mk_partial_induct_rule thy globals R complete_thm clauses = |
585 let |
585 let |
586 val Globals {domT, x, z, a, P, D, ...} = globals |
586 val Globals {domT, x, z, a, P, D, ...} = globals |
587 val acc_R = mk_acc domT R |
587 val acc_R = mk_acc domT R |
588 |
588 |
589 val x_D = assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x))) |
589 val x_D = assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x))) |
590 val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a)) |
590 val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a)) |
591 |
591 |
592 val D_subset = cterm_of thy (Logic.all x |
592 val D_subset = cterm_of thy (Logic.all x |
593 (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x)))) |
593 (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x)))) |
594 |
594 |
595 val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *) |
595 val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *) |
596 Logic.all x |
596 Logic.all x |
597 (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), |
597 (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), |
598 Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x), |
598 Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x), |
599 HOLogic.mk_Trueprop (D $ z))))) |
599 HOLogic.mk_Trueprop (D $ z))))) |
600 |> cterm_of thy |
600 |> cterm_of thy |
601 |
601 |
602 |
602 |
603 (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) |
603 (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) |
604 val ihyp = Term.all domT $ Abs ("z", domT, |
604 val ihyp = Term.all domT $ Abs ("z", domT, |
605 Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), |
605 Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), |
606 HOLogic.mk_Trueprop (P $ Bound 0))) |
606 HOLogic.mk_Trueprop (P $ Bound 0))) |
607 |> cterm_of thy |
607 |> cterm_of thy |
608 |
608 |
609 val aihyp = assume ihyp |
609 val aihyp = assume ihyp |
610 |
610 |
611 fun prove_case clause = |
611 fun prove_case clause = |
612 let |
612 let |
613 val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs, |
613 val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs, |
614 qglr = (oqs, _, _, _), ...} = clause |
614 qglr = (oqs, _, _, _), ...} = clause |
615 |
615 |
616 val case_hyp_conv = K (case_hyp RS eq_reflection) |
616 val case_hyp_conv = K (case_hyp RS eq_reflection) |
617 local open Conv in |
617 local open Conv in |
618 val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D |
618 val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D |
619 val sih = fconv_rule (binder_conv (arg1_conv (arg_conv (arg_conv case_hyp_conv))) ctxt) aihyp |
619 val sih = fconv_rule (binder_conv (arg1_conv (arg_conv (arg_conv case_hyp_conv))) ctxt) aihyp |
620 end |
620 end |
621 |
621 |
622 fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = |
622 fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = |
623 sih |> forall_elim (cterm_of thy rcarg) |
623 sih |> forall_elim (cterm_of thy rcarg) |
624 |> Thm.elim_implies llRI |
624 |> Thm.elim_implies llRI |
625 |> fold_rev (implies_intr o cprop_of) CCas |
625 |> fold_rev (implies_intr o cprop_of) CCas |
626 |> fold_rev (forall_intr o cterm_of thy o Free) RIvs |
626 |> fold_rev (forall_intr o cterm_of thy o Free) RIvs |
627 |
627 |
628 val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *) |
628 val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *) |
629 |
629 |
630 val step = HOLogic.mk_Trueprop (P $ lhs) |
630 val step = HOLogic.mk_Trueprop (P $ lhs) |
631 |> fold_rev (curry Logic.mk_implies o prop_of) P_recs |
631 |> fold_rev (curry Logic.mk_implies o prop_of) P_recs |
632 |> fold_rev (curry Logic.mk_implies) gs |
632 |> fold_rev (curry Logic.mk_implies) gs |
633 |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs)) |
633 |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs)) |
634 |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |
634 |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |
635 |> cterm_of thy |
635 |> cterm_of thy |
636 |
636 |
637 val P_lhs = assume step |
637 val P_lhs = assume step |
638 |> fold forall_elim cqs |
638 |> fold forall_elim cqs |
639 |> Thm.elim_implies lhs_D |
639 |> Thm.elim_implies lhs_D |
640 |> fold Thm.elim_implies ags |
640 |> fold Thm.elim_implies ags |
641 |> fold Thm.elim_implies P_recs |
641 |> fold Thm.elim_implies P_recs |
642 |
642 |
643 val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x)) |
643 val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x)) |
644 |> Conv.arg_conv (Conv.arg_conv case_hyp_conv) |
644 |> Conv.arg_conv (Conv.arg_conv case_hyp_conv) |
645 |> symmetric (* P lhs == P x *) |
645 |> symmetric (* P lhs == P x *) |
646 |> (fn eql => equal_elim eql P_lhs) (* "P x" *) |
646 |> (fn eql => equal_elim eql P_lhs) (* "P x" *) |
647 |> implies_intr (cprop_of case_hyp) |
647 |> implies_intr (cprop_of case_hyp) |
648 |> fold_rev (implies_intr o cprop_of) ags |
648 |> fold_rev (implies_intr o cprop_of) ags |
649 |> fold_rev forall_intr cqs |
649 |> fold_rev forall_intr cqs |
650 in |
650 in |
651 (res, step) |
651 (res, step) |
652 end |
652 end |
653 |
653 |
654 val (cases, steps) = split_list (map prove_case clauses) |
654 val (cases, steps) = split_list (map prove_case clauses) |
655 |
655 |
656 val istep = complete_thm |
656 val istep = complete_thm |
657 |> Thm.forall_elim_vars 0 |
657 |> Thm.forall_elim_vars 0 |
658 |> fold (curry op COMP) cases (* P x *) |
658 |> fold (curry op COMP) cases (* P x *) |
659 |> implies_intr ihyp |
659 |> implies_intr ihyp |
660 |> implies_intr (cprop_of x_D) |
660 |> implies_intr (cprop_of x_D) |
661 |> forall_intr (cterm_of thy x) |
661 |> forall_intr (cterm_of thy x) |
662 |
662 |
663 val subset_induct_rule = |
663 val subset_induct_rule = |
664 acc_subset_induct |
664 acc_subset_induct |
665 |> (curry op COMP) (assume D_subset) |
665 |> (curry op COMP) (assume D_subset) |
666 |> (curry op COMP) (assume D_dcl) |
666 |> (curry op COMP) (assume D_dcl) |
667 |> (curry op COMP) (assume a_D) |
667 |> (curry op COMP) (assume a_D) |
668 |> (curry op COMP) istep |
668 |> (curry op COMP) istep |
692 |
692 |
693 |
693 |
694 (* FIXME: This should probably use fixed goals, to be more reliable and faster *) |
694 (* FIXME: This should probably use fixed goals, to be more reliable and faster *) |
695 fun mk_domain_intro thy (Globals {domT, ...}) R R_cases clause = |
695 fun mk_domain_intro thy (Globals {domT, ...}) R R_cases clause = |
696 let |
696 let |
697 val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...}, |
697 val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...}, |
698 qglr = (oqs, _, _, _), ...} = clause |
698 qglr = (oqs, _, _, _), ...} = clause |
699 val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs) |
699 val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs) |
700 |> fold_rev (curry Logic.mk_implies) gs |
700 |> fold_rev (curry Logic.mk_implies) gs |
701 |> cterm_of thy |
701 |> cterm_of thy |
702 in |
702 in |
703 Goal.init goal |
703 Goal.init goal |
704 |> (SINGLE (resolve_tac [accI] 1)) |> the |
704 |> (SINGLE (resolve_tac [accI] 1)) |> the |
705 |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1)) |> the |
705 |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1)) |> the |
706 |> (SINGLE (CLASIMPSET auto_tac)) |> the |
706 |> (SINGLE (CLASIMPSET auto_tac)) |> the |
707 |> Goal.conclude |
707 |> Goal.conclude |
708 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
708 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
719 fun mk_nest_term_case thy globals R' ihyp clause = |
719 fun mk_nest_term_case thy globals R' ihyp clause = |
720 let |
720 let |
721 val Globals {x, z, ...} = globals |
721 val Globals {x, z, ...} = globals |
722 val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree, |
722 val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree, |
723 qglr=(oqs, _, _, _), ...} = clause |
723 qglr=(oqs, _, _, _), ...} = clause |
724 |
724 |
725 val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp |
725 val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp |
726 |
726 |
727 fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = |
727 fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = |
728 let |
728 let |
729 val used = map (fn (ctx,thm) => FundefCtxTree.export_thm thy ctx thm) (u @ sub) |
729 val used = map (fn (ctx,thm) => FundefCtxTree.export_thm thy ctx thm) (u @ sub) |
730 |
730 |
731 val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs) |
731 val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs) |
732 |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *) |
732 |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *) |
733 |> FundefCtxTree.export_term (fixes, assumes) |
733 |> FundefCtxTree.export_term (fixes, assumes) |
734 |> fold_rev (curry Logic.mk_implies o prop_of) ags |
734 |> fold_rev (curry Logic.mk_implies o prop_of) ags |
735 |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |
735 |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |
736 |> cterm_of thy |
736 |> cterm_of thy |
737 |
737 |
738 val thm = assume hyp |
738 val thm = assume hyp |
739 |> fold forall_elim cqs |
739 |> fold forall_elim cqs |
740 |> fold Thm.elim_implies ags |
740 |> fold Thm.elim_implies ags |
741 |> FundefCtxTree.import_thm thy (fixes, assumes) |
741 |> FundefCtxTree.import_thm thy (fixes, assumes) |
742 |> fold Thm.elim_implies used (* "(arg, lhs) : R'" *) |
742 |> fold Thm.elim_implies used (* "(arg, lhs) : R'" *) |
743 |
743 |
744 val z_eq_arg = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (z, arg)))) |
744 val z_eq_arg = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (z, arg)))) |
745 |
745 |
746 val acc = thm COMP ih_case |
746 val acc = thm COMP ih_case |
747 val z_acc_local = acc |
747 val z_acc_local = acc |
748 |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (K (symmetric (z_eq_arg RS eq_reflection))))) |
748 |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (K (symmetric (z_eq_arg RS eq_reflection))))) |
749 |
749 |
750 val ethm = z_acc_local |
750 val ethm = z_acc_local |
751 |> FundefCtxTree.export_thm thy (fixes, |
751 |> FundefCtxTree.export_thm thy (fixes, |
752 z_eq_arg :: case_hyp :: ags @ assumes) |
752 z_eq_arg :: case_hyp :: ags @ assumes) |
753 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
753 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
754 |
754 |
755 val sub' = sub @ [(([],[]), acc)] |
755 val sub' = sub @ [(([],[]), acc)] |
756 in |
756 in |
764 |
764 |
765 fun mk_nest_term_rule thy globals R R_cases clauses = |
765 fun mk_nest_term_rule thy globals R R_cases clauses = |
766 let |
766 let |
767 val Globals { domT, x, z, ... } = globals |
767 val Globals { domT, x, z, ... } = globals |
768 val acc_R = mk_acc domT R |
768 val acc_R = mk_acc domT R |
769 |
769 |
770 val R' = Free ("R", fastype_of R) |
770 val R' = Free ("R", fastype_of R) |
771 |
771 |
772 val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))) |
772 val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))) |
773 val inrel_R = Const ("FunDef.in_rel", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel |
773 val inrel_R = Const ("FunDef.in_rel", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel |
774 |
774 |
775 val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name "Wellfounded.wfP"}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *) |
775 val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name "Wellfounded.wfP"}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *) |
776 |
776 |
777 (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *) |
777 (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *) |
778 val ihyp = Term.all domT $ Abs ("z", domT, |
778 val ihyp = Term.all domT $ Abs ("z", domT, |
779 Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x), |
779 Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x), |
780 HOLogic.mk_Trueprop (acc_R $ Bound 0))) |
780 HOLogic.mk_Trueprop (acc_R $ Bound 0))) |
781 |> cterm_of thy |
781 |> cterm_of thy |
782 |
782 |
783 val ihyp_a = assume ihyp |> Thm.forall_elim_vars 0 |
783 val ihyp_a = assume ihyp |> Thm.forall_elim_vars 0 |
784 |
784 |
785 val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x)) |
785 val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x)) |
786 |
786 |
787 val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[]) |
787 val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[]) |
788 in |
788 in |
789 R_cases |
789 R_cases |
790 |> forall_elim (cterm_of thy z) |
790 |> forall_elim (cterm_of thy z) |
791 |> forall_elim (cterm_of thy x) |
791 |> forall_elim (cterm_of thy x) |
839 fun mk_trsimp clause psimp = |
839 fun mk_trsimp clause psimp = |
840 let |
840 let |
841 val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, qs, gs, lhs, rhs, ...}, ...} = clause |
841 val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, qs, gs, lhs, rhs, ...}, ...} = clause |
842 val thy = ProofContext.theory_of ctxt |
842 val thy = ProofContext.theory_of ctxt |
843 val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs |
843 val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs |
844 |
844 |
845 val trsimp = Logic.list_implies(gs, HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *) |
845 val trsimp = Logic.list_implies(gs, HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *) |
846 val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *) |
846 val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *) |
847 fun simp_default_tac ss = asm_full_simp_tac (ss addsimps [default_thm, Let_def]) |
847 fun simp_default_tac ss = asm_full_simp_tac (ss addsimps [default_thm, Let_def]) |
848 in |
848 in |
849 Goal.prove ctxt [] [] trsimp |
849 Goal.prove ctxt [] [] trsimp |
850 (fn _ => |
850 (fn _ => |
851 rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1 |
851 rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1 |
852 THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1 |
852 THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1 |
853 THEN (SIMPSET' simp_default_tac 1) |
853 THEN (SIMPSET' simp_default_tac 1) |
854 THEN (etac not_acc_down 1) |
854 THEN (etac not_acc_down 1) |
855 THEN ((etac R_cases) THEN_ALL_NEW (SIMPSET' simp_default_tac)) 1) |
855 THEN ((etac R_cases) THEN_ALL_NEW (SIMPSET' simp_default_tac)) 1) |
860 end |
860 end |
861 |
861 |
862 |
862 |
863 fun prepare_fundef config defname [((fname, fT), mixfix)] abstract_qglrs lthy = |
863 fun prepare_fundef config defname [((fname, fT), mixfix)] abstract_qglrs lthy = |
864 let |
864 let |
865 val FundefConfig {domintros, tailrec, default=default_str, ...} = config |
865 val FundefConfig {domintros, tailrec, default=default_str, ...} = config |
866 |
866 |
867 val fvar = Free (fname, fT) |
867 val fvar = Free (fname, fT) |
868 val domT = domain_type fT |
868 val domT = domain_type fT |
869 val ranT = range_type fT |
869 val ranT = range_type fT |
870 |
870 |
871 val default = Syntax.parse_term lthy default_str |
871 val default = Syntax.parse_term lthy default_str |
872 |> TypeInfer.constrain fT |> Syntax.check_term lthy |
872 |> TypeInfer.constrain fT |> Syntax.check_term lthy |
873 |
873 |
874 val (globals, ctxt') = fix_globals domT ranT fvar lthy |
874 val (globals, ctxt') = fix_globals domT ranT fvar lthy |
875 |
875 |
876 val Globals { x, h, ... } = globals |
876 val Globals { x, h, ... } = globals |
877 |
877 |
878 val clauses = map (mk_clause_context x ctxt') abstract_qglrs |
878 val clauses = map (mk_clause_context x ctxt') abstract_qglrs |
879 |
879 |
880 val n = length abstract_qglrs |
880 val n = length abstract_qglrs |
881 |
881 |
882 fun build_tree (ClauseContext { ctxt, rhs, ...}) = |
882 fun build_tree (ClauseContext { ctxt, rhs, ...}) = |
883 FundefCtxTree.mk_tree (fname, fT) h ctxt rhs |
883 FundefCtxTree.mk_tree (fname, fT) h ctxt rhs |
884 |
884 |
885 val trees = map build_tree clauses |
885 val trees = map build_tree clauses |
886 val RCss = map find_calls trees |
886 val RCss = map find_calls trees |
887 |
887 |
888 val ((G, GIntro_thms, G_elim, G_induct), lthy) = |
888 val ((G, GIntro_thms, G_elim, G_induct), lthy) = |
889 PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy |
889 PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy |
890 |
890 |
891 val ((f, f_defthm), lthy) = |
891 val ((f, f_defthm), lthy) = |
892 PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy |
892 PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy |
893 |
893 |
894 val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss |
894 val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss |
895 val trees = map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f) trees |
895 val trees = map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f) trees |
896 |
896 |
897 val ((R, RIntro_thmss, R_elim), lthy) = |
897 val ((R, RIntro_thmss, R_elim), lthy) = |
898 PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy |
898 PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy |
899 |
899 |
900 val (_, lthy) = |
900 val (_, lthy) = |
901 LocalTheory.abbrev Syntax.mode_default ((dom_name defname, NoSyn), mk_acc domT R) lthy |
901 LocalTheory.abbrev Syntax.mode_default ((Name.binding (dom_name defname), NoSyn), mk_acc domT R) lthy |
902 |
902 |
903 val newthy = ProofContext.theory_of lthy |
903 val newthy = ProofContext.theory_of lthy |
904 val clauses = map (transfer_clause_ctx newthy) clauses |
904 val clauses = map (transfer_clause_ctx newthy) clauses |
905 |
905 |
906 val cert = cterm_of (ProofContext.theory_of lthy) |
906 val cert = cterm_of (ProofContext.theory_of lthy) |
916 |
916 |
917 val mk_trsimps = mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses |
917 val mk_trsimps = mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses |
918 |
918 |
919 fun mk_partial_rules provedgoal = |
919 fun mk_partial_rules provedgoal = |
920 let |
920 let |
921 val newthy = theory_of_thm provedgoal (*FIXME*) |
921 val newthy = theory_of_thm provedgoal (*FIXME*) |
922 |
922 |
923 val (graph_is_function, complete_thm) = |
923 val (graph_is_function, complete_thm) = |
924 provedgoal |
924 provedgoal |
925 |> Conjunction.elim |
925 |> Conjunction.elim |
926 |> apfst (Thm.forall_elim_vars 0) |
926 |> apfst (Thm.forall_elim_vars 0) |
927 |
927 |
928 val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff) |
928 val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff) |
929 |
929 |
930 val psimps = PROFILE "Proving simplification rules" (mk_psimps newthy globals R xclauses values f_iff) graph_is_function |
930 val psimps = PROFILE "Proving simplification rules" (mk_psimps newthy globals R xclauses values f_iff) graph_is_function |
931 |
931 |
932 val simple_pinduct = PROFILE "Proving partial induction rule" |
932 val simple_pinduct = PROFILE "Proving partial induction rule" |
933 (mk_partial_induct_rule newthy globals R complete_thm) xclauses |
933 (mk_partial_induct_rule newthy globals R complete_thm) xclauses |
934 |
934 |
935 |
935 |
936 val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule newthy globals R R_elim) xclauses |
936 val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule newthy globals R R_elim) xclauses |
937 |
937 |
938 val dom_intros = if domintros |
938 val dom_intros = if domintros |
939 then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro newthy globals R R_elim)) xclauses) |
939 then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro newthy globals R R_elim)) xclauses) |
940 else NONE |
940 else NONE |
941 val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE |
941 val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE |
942 |
942 |
943 in |
943 in |
944 FundefResult {fs=[f], G=G, R=R, cases=complete_thm, |
944 FundefResult {fs=[f], G=G, R=R, cases=complete_thm, |
945 psimps=psimps, simple_pinducts=[simple_pinduct], |
945 psimps=psimps, simple_pinducts=[simple_pinduct], |
946 termination=total_intro, trsimps=trsimps, |
946 termination=total_intro, trsimps=trsimps, |
947 domintros=dom_intros} |
947 domintros=dom_intros} |
948 end |
948 end |
949 in |
949 in |
950 ((f, goalstate, mk_partial_rules), lthy) |
950 ((f, goalstate, mk_partial_rules), lthy) |
951 end |
951 end |
952 |
952 |
953 |
953 |
954 |
|
955 |
|
956 end |
954 end |