492 The function @{ML all_elims} takes a list of (certified) terms and instantiates |
492 The function @{ML all_elims} takes a list of (certified) terms and instantiates |
493 theorems of the form @{thm [source] all_elims_test}. For example we can instantiate |
493 theorems of the form @{thm [source] all_elims_test}. For example we can instantiate |
494 the quantifiers in this theorem with @{term a}, @{term b} and @{term c} as follows: |
494 the quantifiers in this theorem with @{term a}, @{term b} and @{term c} as follows: |
495 |
495 |
496 @{ML_matchresult_fake [display, gray] |
496 @{ML_matchresult_fake [display, gray] |
497 "let |
497 \<open>let |
498 val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}] |
498 val ctrms = [@{cterm "a::nat"}, @{cterm "b::nat"}, @{cterm "c::nat"}] |
499 val new_thm = all_elims ctrms @{thm all_elims_test} |
499 val new_thm = all_elims ctrms @{thm all_elims_test} |
500 in |
500 in |
501 pwriteln (pretty_thm_no_vars @{context} new_thm) |
501 pwriteln (pretty_thm_no_vars @{context} new_thm) |
502 end" |
502 end\<close> |
503 "P a b c"} |
503 \<open>P a b c\<close>} |
504 |
504 |
505 Note the difference with @{ML inst_spec_tac} from Page~\pageref{fun:instspectac}: |
505 Note the difference with @{ML inst_spec_tac} from Page~\pageref{fun:instspectac}: |
506 @{ML inst_spec_tac} is a tactic which operates on a goal state; in contrast |
506 @{ML inst_spec_tac} is a tactic which operates on a goal state; in contrast |
507 @{ML all_elims} operates on theorems. |
507 @{ML all_elims} operates on theorems. |
508 |
508 |
509 Similarly, the function @{ML imp_elims} eliminates preconditions from implications. |
509 Similarly, the function @{ML imp_elims} eliminates preconditions from implications. |
510 For example we can eliminate the preconditions \<open>A\<close> and \<open>B\<close> from |
510 For example we can eliminate the preconditions \<open>A\<close> and \<open>B\<close> from |
511 @{thm [source] imp_elims_test}: |
511 @{thm [source] imp_elims_test}: |
512 |
512 |
513 @{ML_matchresult_fake [display, gray] |
513 @{ML_matchresult_fake [display, gray] |
514 "let |
514 \<open>let |
515 val res = imp_elims @{thms imp_elims_test'} @{thm imp_elims_test} |
515 val res = imp_elims @{thms imp_elims_test'} @{thm imp_elims_test} |
516 in |
516 in |
517 pwriteln (pretty_thm_no_vars @{context} res) |
517 pwriteln (pretty_thm_no_vars @{context} res) |
518 end" |
518 end\<close> |
519 "C"} |
519 \<open>C\<close>} |
520 |
520 |
521 Now we set up the proof for the introduction rule as follows: |
521 Now we set up the proof for the introduction rule as follows: |
522 \<close> |
522 \<close> |
523 |
523 |
524 lemma fresh_Lam: |
524 lemma fresh_Lam: |
726 but we have to instantiate it appropriately. These instantiations |
726 but we have to instantiate it appropriately. These instantiations |
727 come from \<open>params1\<close> and \<open>prems2\<close>. We can determine |
727 come from \<open>params1\<close> and \<open>prems2\<close>. We can determine |
728 whether we are in the simple or complicated case by checking whether |
728 whether we are in the simple or complicated case by checking whether |
729 the topmost connective is an \<open>\<forall>\<close>. The premises in the simple |
729 the topmost connective is an \<open>\<forall>\<close>. The premises in the simple |
730 case cannot have such a quantification, since the first step |
730 case cannot have such a quantification, since the first step |
731 of @{ML "expand_tac"} was to ``rulify'' the lemma. |
731 of @{ML \<open>expand_tac\<close>} was to ``rulify'' the lemma. |
732 The premise of the complicated case must have at least one \<open>\<forall>\<close> |
732 The premise of the complicated case must have at least one \<open>\<forall>\<close> |
733 coming from the quantification over the \<open>preds\<close>. So |
733 coming from the quantification over the \<open>preds\<close>. So |
734 we can implement the following function |
734 we can implement the following function |
735 \<close> |
735 \<close> |
736 |
736 |
1009 Line 20 add further every introduction rule under its own name |
1009 Line 20 add further every introduction rule under its own name |
1010 (given by the user).\footnote{FIXME: what happens if the user did not give |
1010 (given by the user).\footnote{FIXME: what happens if the user did not give |
1011 any name.} Line 21 registers the induction principles. For this we have |
1011 any name.} Line 21 registers the induction principles. For this we have |
1012 to use some specific attributes. The first @{ML_ind case_names in Rule_Cases} |
1012 to use some specific attributes. The first @{ML_ind case_names in Rule_Cases} |
1013 corresponds to the case names that are used by Isar to reference the proof |
1013 corresponds to the case names that are used by Isar to reference the proof |
1014 obligations in the induction. The second @{ML "consumes 1" in Rule_Cases} |
1014 obligations in the induction. The second @{ML \<open>consumes 1\<close> in Rule_Cases} |
1015 indicates that the first premise of the induction principle (namely |
1015 indicates that the first premise of the induction principle (namely |
1016 the predicate over which the induction proceeds) is eliminated. |
1016 the predicate over which the induction proceeds) is eliminated. |
1017 |
1017 |
1018 This completes all the code and fits in with the ``front end'' described |
1018 This completes all the code and fits in with the ``front end'' described |
1019 in Section~\ref{sec:interface}.\footnote{FIXME: Describe @{ML Induct.induct_pred}. |
1019 in Section~\ref{sec:interface}.\footnote{FIXME: Describe @{ML Induct.induct_pred}. |