773 |
773 |
774 then the function raises an exception. The function @{ML_ind RSN in Drule} |
774 then the function raises an exception. The function @{ML_ind RSN in Drule} |
775 is similar to @{ML RS}, but takes an additional number as argument. This |
775 is similar to @{ML RS}, but takes an additional number as argument. This |
776 number makes explicit which premise should be instantiated. |
776 number makes explicit which premise should be instantiated. |
777 |
777 |
778 To improve readability of the theorems we shall produce below, we will use the |
|
779 function @{ML no_vars} from Section~\ref{sec:printing}, which transforms |
|
780 schematic variables into free ones. Using this function for the first @{ML |
|
781 RS}-expression above produces the more readable result: |
|
782 |
|
783 @{ML_response_fake [display,gray] |
|
784 "no_vars @{context} (@{thm disjI1} RS @{thm conjI})" "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> Q"} |
|
785 |
|
786 If you want to instantiate more than one premise of a theorem, you can use |
778 If you want to instantiate more than one premise of a theorem, you can use |
787 the function @{ML_ind MRS in Drule}: |
779 the function @{ML_ind MRS in Drule}: |
788 |
780 |
789 @{ML_response_fake [display,gray] |
781 @{ML_response_fake [display,gray] |
790 "no_vars @{context} ([@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI})" |
782 "[@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI}" |
791 "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> (Pa \<or> Q)"} |
783 "\<lbrakk>?P2; ?Q1\<rbrakk> \<Longrightarrow> (?P2 \<or> ?Q2) \<and> (?P1 \<or> ?Q1)"} |
792 |
784 |
793 If you need to instantiate lists of theorems, you can use the |
785 If you need to instantiate lists of theorems, you can use the |
794 functions @{ML_ind RL in Drule} and @{ML_ind MRL in Drule}. For |
786 functions @{ML_ind RL in Drule} and @{ML_ind MRL in Drule}. For |
795 example in the code below, every theorem in the second list is |
787 example in the code below, every theorem in the second list is |
796 instantiated with every theorem in the first. |
788 instantiated with every theorem in the first. |
798 @{ML_response_fake [display,gray] |
790 @{ML_response_fake [display,gray] |
799 "let |
791 "let |
800 val list1 = [@{thm impI}, @{thm disjI2}] |
792 val list1 = [@{thm impI}, @{thm disjI2}] |
801 val list2 = [@{thm conjI}, @{thm disjI1}] |
793 val list2 = [@{thm conjI}, @{thm disjI1}] |
802 in |
794 in |
803 map (no_vars @{context}) (list1 RL list2) |
795 list1 RL list2 |
804 end" |
796 end" |
805 "[\<lbrakk>P \<Longrightarrow> Q; Qa\<rbrakk> \<Longrightarrow> (P \<longrightarrow> Q) \<and> Qa, |
797 "[\<lbrakk>?P1 \<Longrightarrow> ?Q1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<longrightarrow> ?Q1) \<and> ?Q, |
806 \<lbrakk>Q; Qa\<rbrakk> \<Longrightarrow> (P \<or> Q) \<and> Qa, |
798 \<lbrakk>?Q1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q, |
807 (P \<Longrightarrow> Q) \<Longrightarrow> (P \<longrightarrow> Q) \<or> Qa, |
799 (?P1 \<Longrightarrow> ?Q1) \<Longrightarrow> (?P1 \<longrightarrow> ?Q1) \<or> ?Q, |
808 Q \<Longrightarrow> (P \<or> Q) \<or> Qa]"} |
800 ?Q1 \<Longrightarrow> (?P1 \<or> ?Q1) \<or> ?Q]"} |
809 |
801 |
810 \begin{readmore} |
802 \begin{readmore} |
811 The combinators for instantiating theorems with other theorems are |
803 The combinators for instantiating theorems with other theorems are |
812 defined in @{ML_file "Pure/drule.ML"}. |
804 defined in @{ML_file "Pure/drule.ML"}. |
813 \end{readmore} |
805 \end{readmore} |