14 chapter {* Isabelle in More Detail *} |
14 chapter {* Isabelle in More Detail *} |
15 |
15 |
16 text {* |
16 text {* |
17 Isabelle is build around a few central ideas. One central idea is the |
17 Isabelle is build around a few central ideas. One central idea is the |
18 LCF-approach to theorem proving where there is a small trusted core and |
18 LCF-approach to theorem proving where there is a small trusted core and |
19 everything else is build on top of this trusted core. The fundamental data |
19 everything else is build on top of this trusted core |
|
20 \cite{GordonMilnerWadsworth79}. The fundamental data |
20 structures involved in this core are certified terms and certified types, |
21 structures involved in this core are certified terms and certified types, |
21 as well as theorems. |
22 as well as theorems. |
22 *} |
23 *} |
23 |
24 |
24 |
25 |
718 |
719 |
719 @{ML_response_fake [display,gray] |
720 @{ML_response_fake [display,gray] |
720 "Thm.capply @{cterm \"P::nat \<Rightarrow> bool\"} @{cterm \"3::nat\"}" |
721 "Thm.capply @{cterm \"P::nat \<Rightarrow> bool\"} @{cterm \"3::nat\"}" |
721 "P 3"} |
722 "P 3"} |
722 |
723 |
723 Similarly @{ML_ind list_comb in Drule} applies a list of @{ML_type cterm}s. |
724 Similarly the function @{ML_ind list_comb in Drule} from the structure @{ML_struct Drule} |
|
725 applies a list of @{ML_type cterm}s. |
724 |
726 |
725 @{ML_response_fake [display,gray] |
727 @{ML_response_fake [display,gray] |
726 "let |
728 "let |
727 val chead = @{cterm \"P::unit \<Rightarrow> nat \<Rightarrow> bool\"} |
729 val chead = @{cterm \"P::unit \<Rightarrow> nat \<Rightarrow> bool\"} |
728 val cargs = [@{cterm \"()\"}, @{cterm \"3::nat\"}] |
730 val cargs = [@{cterm \"()\"}, @{cterm \"3::nat\"}] |
741 section {* Theorems *} |
743 section {* Theorems *} |
742 |
744 |
743 text {* |
745 text {* |
744 Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm} |
746 Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm} |
745 that can only be built by going through interfaces. As a consequence, every proof |
747 that can only be built by going through interfaces. As a consequence, every proof |
746 in Isabelle is correct by construction. This follows the tradition of the LCF approach |
748 in Isabelle is correct by construction. This follows the tradition of the LCF approach. |
747 \cite{GordonMilnerWadsworth79}. |
|
748 |
749 |
749 |
750 |
750 To see theorems in ``action'', let us give a proof on the ML-level for the following |
751 To see theorems in ``action'', let us give a proof on the ML-level for the following |
751 statement: |
752 statement: |
752 *} |
753 *} |
753 |
754 |
754 lemma |
755 lemma |
755 assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x" |
756 assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x" |
756 and assm\<^isub>2: "P t" |
757 and assm\<^isub>2: "P t" |
757 shows "Q t" (*<*)oops(*>*) |
758 shows "Q t"(*<*)oops(*>*) |
758 |
759 |
759 text {* |
760 text {* |
760 The corresponding ML-code is as follows: |
761 The corresponding ML-code is as follows: |
761 *} |
762 *} |
762 |
763 |
801 \] |
802 \] |
802 |
803 |
803 While we obtained a theorem as result, this theorem is not |
804 While we obtained a theorem as result, this theorem is not |
804 yet stored in Isabelle's theorem database. Consequently, it cannot be |
805 yet stored in Isabelle's theorem database. Consequently, it cannot be |
805 referenced on the user level. One way to store it in the theorem database is |
806 referenced on the user level. One way to store it in the theorem database is |
806 by using the function @{ML_ind note in LocalTheory}. |
807 by using the function @{ML_ind note in LocalTheory}.\footnote{\bf FIXME: make sure a pointer |
|
808 to the section about local-setup is given eralier.} |
807 *} |
809 *} |
808 |
810 |
809 local_setup %gray {* |
811 local_setup %gray {* |
810 LocalTheory.note Thm.theoremK |
812 LocalTheory.note Thm.theoremK |
811 ((@{binding "my_thm"}, []), [my_thm]) #> snd *} |
813 ((@{binding "my_thm"}, []), [my_thm]) #> snd *} |
812 |
814 |
813 text {* |
815 text {* |
814 The first argument @{ML_ind theoremK in Thm} is a kind indicator, which |
816 The first argument @{ML_ind theoremK in Thm} is a kind indicator, which |
815 classifies the theorem. There are several such kind indicators: for a |
817 classifies the theorem. There are several such kind indicators: for a |
816 theorem arising from a definition we should use @{ML_ind definitionK in |
818 theorem arising from a definition we should use @{ML_ind definitionK in |
817 Thm}, for an axiom @{ML_ind axiomK in Thm}, for ``normal'' theorems the |
819 Thm}, for an axiom @{ML_ind axiomK in Thm}, and for ``normal'' theorems the |
818 kinds @{ML_ind theoremK in Thm} or @{ML_ind lemmaK in Thm}. The second |
820 kinds @{ML_ind theoremK in Thm} or @{ML_ind lemmaK in Thm}. The second |
819 argument of @{ML note in LocalTheory} is the name under which we store the |
821 argument of @{ML note in LocalTheory} is the name under which we store the |
820 theorem or theorems. The third argument can contain a list of (theorem) |
822 theorem or theorems. The third argument can contain a list of theorem |
821 attributes. We will explain them in detail in |
823 attributes, which we will explain in detail in Section~\ref{sec:attributes}. |
822 Section~\ref{sec:attributes}. Below we just use one such attribute in order add |
824 Below we just use one such attribute in order add |
823 the theorem to the simpset: |
825 the theorem to the simpset: |
824 *} |
826 *} |
825 |
827 |
826 local_setup %gray {* |
828 local_setup %gray {* |
827 LocalTheory.note Thm.theoremK |
829 LocalTheory.note Thm.theoremK |
828 ((@{binding "my_thm_simp"}, |
830 ((@{binding "my_thm_simp"}, |
829 [Attrib.internal (K Simplifier.simp_add)]), [my_thm]) #> snd *} |
831 [Attrib.internal (K Simplifier.simp_add)]), [my_thm]) #> snd *} |
830 |
832 |
831 text {* |
833 text {* |
832 Note that we have to use another name under which the theorem is stored, |
834 Note that we have to use another name under which the theorem is stored, |
833 since Isabelle does not allow us to store another theorem under the same |
835 since Isabelle does not allow us to store two theorems under the same |
834 name. The attribute needs to be wrapped inside the function @{ML_ind |
836 name. The attribute needs to be wrapped inside the function @{ML_ind |
835 internal in Attrib}. If we use the function @{ML get_thm_names_from_ss} from |
837 internal in Attrib}. If we use the function @{ML get_thm_names_from_ss} from |
836 the previous chapter, we can check whether the theorem has actually been |
838 the previous chapter, we can check whether the theorem has actually been |
837 added. |
839 added. |
838 |
840 |
853 \begin{isabelle} |
855 \begin{isabelle} |
854 \isacommand{thm}~@{text "my_thm"}\isanewline |
856 \isacommand{thm}~@{text "my_thm"}\isanewline |
855 @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"} |
857 @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"} |
856 \end{isabelle} |
858 \end{isabelle} |
857 |
859 |
858 or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. As can be seen |
860 or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. As can be seen, |
859 the theorem does not have any meta-variables that would be present if we proved |
861 the theorem does not have any meta-variables that would be present if we proved |
860 this theorem on the user-level. We will see later on that usually we have to |
862 this theorem on the user-level. We will see later on that we have to |
861 construct meta-variables in theorems explicitly. |
863 construct meta-variables in theorems explicitly. |
862 |
864 |
863 \footnote{\bf FIXME say something about @{ML_ind add_thms_dynamic in PureThy}} |
865 \footnote{\bf FIXME say something about @{ML_ind add_thms_dynamic in PureThy}} |
864 *} |
866 *} |
865 |
867 |
866 text {* |
868 text {* |
867 There is a multitude of functions that manage or manipulate theorems. For example |
869 There is a multitude of functions that manage or manipulate theorems in the |
|
870 structures @{ML_struct Thm} and @{ML_struct Drule}. For example |
868 we can test theorems for alpha equality. Suppose you proved the following three |
871 we can test theorems for alpha equality. Suppose you proved the following three |
869 theorems. |
872 theorems. |
870 *} |
873 *} |
871 |
874 |
872 lemma |
875 lemma |