1 (* Title: Tools/induct.ML |
1 (* Title: Tools/induct.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Markus Wenzel, TU Muenchen |
3 Author: Markus Wenzel, TU Muenchen |
4 |
4 |
5 Proof by cases and induction. |
5 Proof by cases, induction, and coinduction. |
6 *) |
6 *) |
7 |
7 |
8 signature INDUCT_DATA = |
8 signature INDUCT_DATA = |
9 sig |
9 sig |
10 val cases_default: thm |
10 val cases_default: thm |
55 val inner_atomize_tac: int -> tactic |
55 val inner_atomize_tac: int -> tactic |
56 val rulified_term: thm -> theory * term |
56 val rulified_term: thm -> theory * term |
57 val rulify_tac: int -> tactic |
57 val rulify_tac: int -> tactic |
58 val internalize: int -> thm -> thm |
58 val internalize: int -> thm -> thm |
59 val guess_instance: thm -> int -> thm -> thm Seq.seq |
59 val guess_instance: thm -> int -> thm -> thm Seq.seq |
60 val cases_tac: Proof.context -> bool -> term option list list -> thm option -> |
60 val cases_tac: Proof.context -> term option list list -> thm option -> |
61 thm list -> int -> cases_tactic |
61 thm list -> int -> cases_tactic |
62 val induct_tac: Proof.context -> bool -> (string option * term) option list list -> |
62 val induct_tac: Proof.context -> (string option * term) option list list -> |
63 (string * typ) list list -> term option list -> thm list option -> thm list -> int -> |
63 (string * typ) list list -> term option list -> thm list option -> |
64 cases_tactic |
64 thm list -> int -> cases_tactic |
65 val coinduct_tac: Proof.context -> bool -> term option list -> term option list -> |
65 val coinduct_tac: Proof.context -> term option list -> term option list -> thm option -> |
66 thm option -> thm list -> int -> cases_tactic |
66 thm list -> int -> cases_tactic |
67 val setup: theory -> theory |
67 val setup: theory -> theory |
68 end; |
68 end; |
69 |
69 |
70 functor InductFun(Data: INDUCT_DATA): INDUCT = |
70 functor InductFun(Data: INDUCT_DATA): INDUCT = |
71 struct |
71 struct |
302 |
302 |
303 fun trace_rules _ kind [] = error ("Unable to figure out " ^ kind ^ " rule") |
303 fun trace_rules _ kind [] = error ("Unable to figure out " ^ kind ^ " rule") |
304 | trace_rules ctxt _ rules = Method.trace ctxt rules; |
304 | trace_rules ctxt _ rules = Method.trace ctxt rules; |
305 |
305 |
306 |
306 |
307 (* make_cases *) |
|
308 |
|
309 fun make_cases is_open rule = |
|
310 RuleCases.make_common is_open (Thm.theory_of_thm rule, Thm.prop_of rule); |
|
311 |
|
312 fun warn_open true = |
|
313 legacy_feature ("Open rule cases in proof method" ^ Position.str_of (Position.thread_data ())) |
|
314 | warn_open false = (); |
|
315 |
|
316 |
|
317 |
307 |
318 (** cases method **) |
308 (** cases method **) |
319 |
309 |
320 (* |
310 (* |
321 rule selection scheme: |
311 rule selection scheme: |
333 fun get_casesP ctxt (fact :: _) = find_casesP ctxt (Thm.concl_of fact) |
323 fun get_casesP ctxt (fact :: _) = find_casesP ctxt (Thm.concl_of fact) |
334 | get_casesP _ _ = []; |
324 | get_casesP _ _ = []; |
335 |
325 |
336 in |
326 in |
337 |
327 |
338 fun cases_tac ctxt is_open insts opt_rule facts = |
328 fun cases_tac ctxt insts opt_rule facts = |
339 let |
329 let |
340 val _ = warn_open is_open; |
|
341 val thy = ProofContext.theory_of ctxt; |
330 val thy = ProofContext.theory_of ctxt; |
342 val cert = Thm.cterm_of thy; |
331 val cert = Thm.cterm_of thy; |
343 |
332 |
344 fun inst_rule r = |
333 fun inst_rule r = |
345 if null insts then `RuleCases.get r |
334 if null insts then `RuleCases.get r |
357 in |
346 in |
358 fn i => fn st => |
347 fn i => fn st => |
359 ruleq |
348 ruleq |
360 |> Seq.maps (RuleCases.consume [] facts) |
349 |> Seq.maps (RuleCases.consume [] facts) |
361 |> Seq.maps (fn ((cases, (_, more_facts)), rule) => |
350 |> Seq.maps (fn ((cases, (_, more_facts)), rule) => |
362 CASES (make_cases is_open rule cases) |
351 CASES (RuleCases.make_common false (thy, Thm.prop_of rule) cases) |
363 (Method.insert_tac more_facts i THEN Tactic.rtac rule i) st) |
352 (Method.insert_tac more_facts i THEN Tactic.rtac rule i) st) |
364 end; |
353 end; |
365 |
354 |
366 end; |
355 end; |
367 |
356 |
573 fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact)) |
562 fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact)) |
574 | get_inductP _ _ = []; |
563 | get_inductP _ _ = []; |
575 |
564 |
576 in |
565 in |
577 |
566 |
578 fun induct_tac ctxt is_open def_insts arbitrary taking opt_rule facts = |
567 fun induct_tac ctxt def_insts arbitrary taking opt_rule facts = |
579 let |
568 let |
580 val _ = warn_open is_open; |
|
581 val thy = ProofContext.theory_of ctxt; |
569 val thy = ProofContext.theory_of ctxt; |
582 val cert = Thm.cterm_of thy; |
570 val cert = Thm.cterm_of thy; |
583 |
571 |
584 val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list; |
572 val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list; |
585 val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs; |
573 val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs; |
601 |> map_filter (RuleCases.mutual_rule ctxt) |
589 |> map_filter (RuleCases.mutual_rule ctxt) |
602 |> tap (trace_rules ctxt inductN o map #2) |
590 |> tap (trace_rules ctxt inductN o map #2) |
603 |> Seq.of_list |> Seq.maps (Seq.try inst_rule)); |
591 |> Seq.of_list |> Seq.maps (Seq.try inst_rule)); |
604 |
592 |
605 fun rule_cases rule = |
593 fun rule_cases rule = |
606 RuleCases.make_nested is_open (Thm.prop_of rule) (rulified_term rule); |
594 RuleCases.make_nested false (Thm.prop_of rule) (rulified_term rule); |
607 in |
595 in |
608 (fn i => fn st => |
596 (fn i => fn st => |
609 ruleq |
597 ruleq |
610 |> Seq.maps (RuleCases.consume (flat defs) facts) |
598 |> Seq.maps (RuleCases.consume (flat defs) facts) |
611 |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) => |
599 |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) => |
649 fun main_prop_of th = |
637 fun main_prop_of th = |
650 if RuleCases.get_consumes th > 0 then Thm.major_prem_of th else Thm.concl_of th; |
638 if RuleCases.get_consumes th > 0 then Thm.major_prem_of th else Thm.concl_of th; |
651 |
639 |
652 in |
640 in |
653 |
641 |
654 fun coinduct_tac ctxt is_open inst taking opt_rule facts = |
642 fun coinduct_tac ctxt inst taking opt_rule facts = |
655 let |
643 let |
656 val _ = warn_open is_open; |
|
657 val thy = ProofContext.theory_of ctxt; |
644 val thy = ProofContext.theory_of ctxt; |
658 val cert = Thm.cterm_of thy; |
645 val cert = Thm.cterm_of thy; |
659 |
646 |
660 fun inst_rule r = |
647 fun inst_rule r = |
661 if null inst then `RuleCases.get r |
648 if null inst then `RuleCases.get r |
675 |> Seq.maps (RuleCases.consume [] facts) |
662 |> Seq.maps (RuleCases.consume [] facts) |
676 |> Seq.maps (fn ((cases, (_, more_facts)), rule) => |
663 |> Seq.maps (fn ((cases, (_, more_facts)), rule) => |
677 guess_instance rule i st |
664 guess_instance rule i st |
678 |> Seq.map (rule_instance thy (burrow_options (Variable.polymorphic ctxt) taking)) |
665 |> Seq.map (rule_instance thy (burrow_options (Variable.polymorphic ctxt) taking)) |
679 |> Seq.maps (fn rule' => |
666 |> Seq.maps (fn rule' => |
680 CASES (make_cases is_open rule' cases) |
667 CASES (RuleCases.make_common false (thy, Thm.prop_of rule') cases) |
681 (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st))) |
668 (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st))) |
682 end; |
669 end; |
683 |
670 |
684 end; |
671 end; |
685 |
672 |
686 |
673 |
687 |
674 |
688 (** concrete syntax **) |
675 (** concrete syntax **) |
689 |
676 |
690 val openN = "open"; |
|
691 val arbitraryN = "arbitrary"; |
677 val arbitraryN = "arbitrary"; |
692 val takingN = "taking"; |
678 val takingN = "taking"; |
693 val ruleN = "rule"; |
679 val ruleN = "rule"; |
694 |
680 |
695 local |
681 local |
734 Scan.repeat1 (unless_more_args inst)) []; |
720 Scan.repeat1 (unless_more_args inst)) []; |
735 |
721 |
736 in |
722 in |
737 |
723 |
738 fun cases_meth src = |
724 fun cases_meth src = |
739 Method.syntax (Args.mode openN -- |
725 Method.syntax (Args.and_list (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) src |
740 (Args.and_list (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule)) src |
726 #> (fn ((insts, opt_rule), ctxt) => |
741 #> (fn ((is_open, (insts, opt_rule)), ctxt) => |
|
742 Method.METHOD_CASES (fn facts => |
727 Method.METHOD_CASES (fn facts => |
743 Seq.DETERM (HEADGOAL (cases_tac ctxt is_open insts opt_rule facts)))); |
728 Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts)))); |
744 |
729 |
745 fun induct_meth src = |
730 fun induct_meth src = |
746 Method.syntax (Args.mode openN -- |
731 Method.syntax (Args.and_list (Scan.repeat (unless_more_args def_inst)) -- |
747 (Args.and_list (Scan.repeat (unless_more_args def_inst)) -- |
732 (arbitrary -- taking -- Scan.option induct_rule)) src |
748 (arbitrary -- taking -- Scan.option induct_rule))) src |
733 #> (fn ((insts, ((arbitrary, taking), opt_rule)), ctxt) => |
749 #> (fn ((is_open, (insts, ((arbitrary, taking), opt_rule))), ctxt) => |
|
750 Method.RAW_METHOD_CASES (fn facts => |
734 Method.RAW_METHOD_CASES (fn facts => |
751 Seq.DETERM (HEADGOAL (induct_tac ctxt is_open insts arbitrary taking opt_rule facts)))); |
735 Seq.DETERM (HEADGOAL (induct_tac ctxt insts arbitrary taking opt_rule facts)))); |
752 |
736 |
753 fun coinduct_meth src = |
737 fun coinduct_meth src = |
754 Method.syntax (Args.mode openN -- |
738 Method.syntax (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule) src |
755 (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule)) src |
739 #> (fn (((insts, taking), opt_rule), ctxt) => |
756 #> (fn ((is_open, ((insts, taking), opt_rule)), ctxt) => |
|
757 Method.RAW_METHOD_CASES (fn facts => |
740 Method.RAW_METHOD_CASES (fn facts => |
758 Seq.DETERM (HEADGOAL (coinduct_tac ctxt is_open insts taking opt_rule facts)))); |
741 Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts)))); |
759 |
742 |
760 end; |
743 end; |
761 |
744 |
762 |
745 |
763 |
746 |