equal
deleted
inserted
replaced
211 |
211 |
212 The tactic will use the following helper function for instantiating universal |
212 The tactic will use the following helper function for instantiating universal |
213 quantifiers. |
213 quantifiers. |
214 *} |
214 *} |
215 |
215 |
216 ML{*fun inst_spec ctrm = |
216 ML %grayML{*fun inst_spec ctrm = |
217 let |
217 let |
218 val cty = ctyp_of_term ctrm |
218 val cty = ctyp_of_term ctrm |
219 in |
219 in |
220 Drule.instantiate' [SOME cty] [NONE, SOME ctrm] @{thm spec} |
220 Drule.instantiate' [SOME cty] [NONE, SOME ctrm] @{thm spec} |
221 end*} |
221 end*} |
225 and instantiates the @{text "?x"} in the theorem @{thm spec} with a given |
225 and instantiates the @{text "?x"} in the theorem @{thm spec} with a given |
226 @{ML_type cterm}. We call this helper function in the following |
226 @{ML_type cterm}. We call this helper function in the following |
227 tactic.\label{fun:instspectac}. |
227 tactic.\label{fun:instspectac}. |
228 *} |
228 *} |
229 |
229 |
230 ML{*fun inst_spec_tac ctrms = |
230 ML %grayML{*fun inst_spec_tac ctrms = |
231 EVERY' (map (dtac o inst_spec) ctrms)*} |
231 EVERY' (map (dtac o inst_spec) ctrms)*} |
232 |
232 |
233 text {* |
233 text {* |
234 This tactic expects a list of @{ML_type cterm}s. It allows us in the |
234 This tactic expects a list of @{ML_type cterm}s. It allows us in the |
235 proof below to instantiate the three quantifiers in the assumption. |
235 proof below to instantiate the three quantifiers in the assumption. |
476 |
476 |
477 about freshness for lambdas. In order to ease somewhat |
477 about freshness for lambdas. In order to ease somewhat |
478 our work here, we use the following two helper functions. |
478 our work here, we use the following two helper functions. |
479 *} |
479 *} |
480 |
480 |
481 ML{*val all_elims = fold (fn ct => fn th => th RS inst_spec ct) |
481 ML %grayML{*val all_elims = fold (fn ct => fn th => th RS inst_spec ct) |
482 val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp})*} |
482 val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp})*} |
483 |
483 |
484 text {* |
484 text {* |
485 To see what these functions do, let us suppose we have the following three |
485 To see what these functions do, let us suppose we have the following three |
486 theorems. |
486 theorems. |
586 text_raw {* |
586 text_raw {* |
587 \begin{figure}[t] |
587 \begin{figure}[t] |
588 \begin{minipage}{\textwidth} |
588 \begin{minipage}{\textwidth} |
589 \begin{isabelle} |
589 \begin{isabelle} |
590 *} |
590 *} |
591 ML{*fun chop_print params1 params2 prems1 prems2 ctxt = |
591 ML %grayML{*fun chop_print params1 params2 prems1 prems2 ctxt = |
592 let |
592 let |
593 val pps = [Pretty.big_list "Params1 from the rule:" (map (pretty_cterm ctxt) params1), |
593 val pps = [Pretty.big_list "Params1 from the rule:" (map (pretty_cterm ctxt) params1), |
594 Pretty.big_list "Params2 from the predicate:" (map (pretty_cterm ctxt) params2), |
594 Pretty.big_list "Params2 from the predicate:" (map (pretty_cterm ctxt) params2), |
595 Pretty.big_list "Prems1 from the rule:" (map (pretty_thm ctxt) prems1), |
595 Pretty.big_list "Prems1 from the rule:" (map (pretty_thm ctxt) prems1), |
596 Pretty.big_list "Prems2 from the predicate:" (map (pretty_thm ctxt) prems2)] |
596 Pretty.big_list "Prems2 from the predicate:" (map (pretty_thm ctxt) prems2)] |
742 The premise of the complicated case must have at least one @{text "\<forall>"} |
742 The premise of the complicated case must have at least one @{text "\<forall>"} |
743 coming from the quantification over the @{text preds}. So |
743 coming from the quantification over the @{text preds}. So |
744 we can implement the following function |
744 we can implement the following function |
745 *} |
745 *} |
746 |
746 |
747 ML{*fun prepare_prem params2 prems2 prem = |
747 ML %grayML{*fun prepare_prem params2 prems2 prem = |
748 rtac (case prop_of prem of |
748 rtac (case prop_of prem of |
749 _ $ (Const (@{const_name All}, _) $ _) => |
749 _ $ (Const (@{const_name All}, _) $ _) => |
750 prem |> all_elims params2 |
750 prem |> all_elims params2 |
751 |> imp_elims prems2 |
751 |> imp_elims prems2 |
752 | _ => prem) *} |
752 | _ => prem) *} |
756 it has an outermost universial quantification, instantiates it first |
756 it has an outermost universial quantification, instantiates it first |
757 with @{text "params1"} and then @{text "prems1"}. The following |
757 with @{text "params1"} and then @{text "prems1"}. The following |
758 tactic will therefore prove the lemma completely. |
758 tactic will therefore prove the lemma completely. |
759 *} |
759 *} |
760 |
760 |
761 ML{*fun prove_intro_tac i preds rules = |
761 ML %grayML{*fun prove_intro_tac i preds rules = |
762 SUBPROOF (fn {params, prems, ...} => |
762 SUBPROOF (fn {params, prems, ...} => |
763 let |
763 let |
764 val cparams = map snd params |
764 val cparams = map snd params |
765 val (params1, params2) = chop (length cparams - length preds) cparams |
765 val (params1, params2) = chop (length cparams - length preds) cparams |
766 val (prems1, prems2) = chop (length prems - length rules) prems |
766 val (prems1, prems2) = chop (length prems - length rules) prems |
943 |
943 |
944 For convenience, we use the following |
944 For convenience, we use the following |
945 three wrappers this function: |
945 three wrappers this function: |
946 *} |
946 *} |
947 |
947 |
948 ML{*fun note_many qname ((name, attrs), thms) = |
948 ML %grayML{*fun note_many qname ((name, attrs), thms) = |
949 Local_Theory.note ((Binding.qualify false qname name, attrs), thms) |
949 Local_Theory.note ((Binding.qualify false qname name, attrs), thms) |
950 |
950 |
951 fun note_single1 qname ((name, attrs), thm) = |
951 fun note_single1 qname ((name, attrs), thm) = |
952 note_many qname ((name, attrs), [thm]) |
952 note_many qname ((name, attrs), [thm]) |
953 |
953 |