743 and assm\<^isub>2: "P t" |
743 and assm\<^isub>2: "P t" |
744 shows "Q t" (*<*)oops(*>*) |
744 shows "Q t" (*<*)oops(*>*) |
745 |
745 |
746 text {* |
746 text {* |
747 The corresponding ML-code is as follows: |
747 The corresponding ML-code is as follows: |
748 |
748 *} |
749 @{ML_response_fake [display,gray] |
749 |
750 "let |
750 ML{*val my_thm = let |
751 val assm1 = @{cprop \"\<And>(x::nat). P x \<Longrightarrow> Q x\"} |
751 val assm1 = @{cprop "\<And>(x::nat). P x \<Longrightarrow> Q x"} |
752 val assm2 = @{cprop \"(P::nat\<Rightarrow>bool) t\"} |
752 val assm2 = @{cprop "(P::nat \<Rightarrow> bool) t"} |
753 |
753 |
754 val Pt_implies_Qt = |
754 val Pt_implies_Qt = |
755 assume assm1 |
755 assume assm1 |
756 |> forall_elim @{cterm \"t::nat\"}; |
756 |> forall_elim @{cterm "t::nat"} |
757 |
757 |
758 val Qt = implies_elim Pt_implies_Qt (assume assm2); |
758 val Qt = implies_elim Pt_implies_Qt (assume assm2) |
759 in |
759 in |
760 Qt |
760 Qt |
761 |> implies_intr assm2 |
761 |> implies_intr assm2 |
762 |> implies_intr assm1 |
762 |> implies_intr assm1 |
763 end" "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"} |
763 end*} |
764 |
764 |
765 This code-snippet constructs the following proof: |
765 text {* |
|
766 If we print out the value of @{ML my_thm} then we see only the |
|
767 final statement of the theorem. |
|
768 |
|
769 @{ML_response_fake [display, gray] |
|
770 "string_of_thm @{context} my_thm |
|
771 |> tracing" |
|
772 "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"} |
|
773 |
|
774 However, internally the code-snippet constructs the following |
|
775 proof. |
766 |
776 |
767 \[ |
777 \[ |
768 \infer[(@{text "\<Longrightarrow>"}$-$intro)]{\vdash @{prop "(\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> P t \<Longrightarrow> Q t"}} |
778 \infer[(@{text "\<Longrightarrow>"}$-$intro)]{\vdash @{prop "(\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> P t \<Longrightarrow> Q t"}} |
769 {\infer[(@{text "\<Longrightarrow>"}$-$intro)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}} |
779 {\infer[(@{text "\<Longrightarrow>"}$-$intro)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}} |
770 {\infer[(@{text "\<Longrightarrow>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"}, @{prop "P t"} \vdash @{prop "Q t"}} |
780 {\infer[(@{text "\<Longrightarrow>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"}, @{prop "P t"} \vdash @{prop "Q t"}} |
775 } |
785 } |
776 } |
786 } |
777 } |
787 } |
778 \] |
788 \] |
779 |
789 |
780 However, while we obtained a theorem as result, this theorem is not |
790 While we obtained a theorem as result, this theorem is not |
781 yet stored in Isabelle's theorem database. So it cannot be referenced later |
791 yet stored in Isabelle's theorem database. So it cannot be referenced later |
782 on. How to store theorems will be explained in Section~\ref{sec:storing}. |
792 on. One way to store it is |
|
793 *} |
|
794 |
|
795 local_setup %gray{* |
|
796 LocalTheory.note Thm.theoremK |
|
797 ((@{binding "my_thm"}, []), [my_thm]) #> snd *} |
|
798 |
|
799 text {* |
|
800 Now it can be referenced with the \isacommand{thm}-command on the user-level |
|
801 of Isabelle |
|
802 |
|
803 \begin{isabelle} |
|
804 \isacommand{thm}~@{text "my_thm"}\isanewline |
|
805 @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"} |
|
806 \end{isabelle} |
|
807 |
|
808 or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. Note that the |
|
809 theorem does not have the meta-variables that would be present if we stated |
|
810 this theorem on the user-level. |
|
811 |
783 |
812 |
784 \begin{readmore} |
813 \begin{readmore} |
785 For the functions @{text "assume"}, @{text "forall_elim"} etc |
814 For the functions @{text "assume"}, @{text "forall_elim"} etc |
786 see \isccite{sec:thms}. The basic functions for theorems are defined in |
815 see \isccite{sec:thms}. The basic functions for theorems are defined in |
787 @{ML_file "Pure/thm.ML"}. |
816 @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}. |
788 \end{readmore} |
817 \end{readmore} |
789 |
818 |
790 (FIXME: handy functions working on theorems, like @{ML_ind rulify in ObjectLogic} and so on) |
819 (FIXME: handy functions working on theorems, like @{ML_ind rulify in ObjectLogic} and so on) |
791 |
820 |
792 (FIXME: @{ML_ind prove in Goal}) |
821 (FIXME: @{ML_ind prove in Goal}) |