1566 The third argument of @{ML note in Local_Theory} is the list of theorems we |
1566 The third argument of @{ML note in Local_Theory} is the list of theorems we |
1567 want to store under a name. We can store more than one under a single name. |
1567 want to store under a name. We can store more than one under a single name. |
1568 The first argument of @{ML note in Local_Theory} is the name under |
1568 The first argument of @{ML note in Local_Theory} is the name under |
1569 which we store the theorem or theorems. The second argument can contain a |
1569 which we store the theorem or theorems. The second argument can contain a |
1570 list of theorem attributes, which we will explain in detail in |
1570 list of theorem attributes, which we will explain in detail in |
1571 Section~\ref{sec:attributes}. Below we just use one such attribute for |
1571 Section~\ref{sec:attributes}. Below we just use one such attribute, |
1572 adding the theorem to the simpset: |
1572 @{ML_ind simp_add in Simplifier}, for adding the theorem to the simpset: |
1573 *} |
1573 *} |
1574 |
1574 |
1575 local_setup %gray {* |
1575 local_setup %gray {* |
1576 Local_Theory.note ((@{binding "my_thm_simp"}, |
1576 Local_Theory.note ((@{binding "my_thm_simp"}, |
1577 [Attrib.internal (K Simplifier.simp_add)]), [my_thm]) #> snd *} |
1577 [Attrib.internal (K Simplifier.simp_add)]), [my_thm]) #> snd *} |
1962 @{text "> let \"?case\" = \"?P\""}\\ |
1962 @{text "> let \"?case\" = \"?P\""}\\ |
1963 @{text "> 2:"}\\ |
1963 @{text "> 2:"}\\ |
1964 @{text "> let \"?case\" = \"?P\""} |
1964 @{text "> let \"?case\" = \"?P\""} |
1965 \end{tabular}*} |
1965 \end{tabular}*} |
1966 |
1966 |
1967 |
1967 |
1968 text {* |
1968 text {* |
|
1969 One often wants to know the theorems that are used in the proof |
|
1970 of a theorem. They can be obtained by introspecting the theorem. |
|
1971 To introspect a theorem, let us define the following three functions that |
|
1972 analyse the @{ML_type_ind proof_body} data-structure from the structure |
|
1973 @{ML_struct Proofterm}. |
|
1974 *} |
|
1975 |
|
1976 ML %grayML{*fun pthms_of (PBody {thms, ...}) = map #2 thms |
|
1977 val get_names = map #1 o pthms_of |
|
1978 val get_pbodies = map (Future.join o #3) o pthms_of *} |
|
1979 |
|
1980 text {* |
|
1981 To see what their purpose is, consider the following three short proofs. |
|
1982 *} |
|
1983 |
|
1984 lemma my_conjIa: |
|
1985 shows "A \<and> B \<Longrightarrow> A \<and> B" |
|
1986 apply(rule conjI) |
|
1987 apply(drule conjunct1) |
|
1988 apply(assumption) |
|
1989 apply(drule conjunct2) |
|
1990 apply(assumption) |
|
1991 done |
|
1992 |
|
1993 lemma my_conjIb: |
|
1994 shows "A \<and> B \<Longrightarrow> A \<and> B" |
|
1995 apply(assumption) |
|
1996 done |
|
1997 |
|
1998 lemma my_conjIc: |
|
1999 shows "A \<and> B \<Longrightarrow> A \<and> B" |
|
2000 apply(auto) |
|
2001 done |
|
2002 |
|
2003 text {* |
|
2004 While the information about which theorems are used is obvious in |
|
2005 the first two proofs, it is not obvious in the third, because of the |
|
2006 @{text auto}-step. Fortunately, ``behind'' every proved theorem is |
|
2007 a proof-tree that records all theorems that are employed for |
|
2008 establishing this theorem. We can traverse this proof-tree |
|
2009 extracting this information. Let us first extract the name of the |
|
2010 established theorem. This can be done with |
|
2011 |
|
2012 @{ML_response [display,gray] |
|
2013 "@{thm my_conjIa} |
|
2014 |> Thm.proof_body_of |
|
2015 |> get_names" |
|
2016 "[\"Essential.my_conjIa\"]"} |
|
2017 |
|
2018 whereby @{text "Essential"} refers to the theory name in which |
|
2019 we established the theorem @{thm [source] my_conjIa}. The function @{ML_ind |
|
2020 proof_body_of in Thm} returns a part of the data that is stored in a |
|
2021 theorem. Notice that the first proof above references |
|
2022 three theorems, namely @{thm [source] conjI}, @{thm [source] conjunct1} |
|
2023 and @{thm [source] conjunct2}. We can obtain them by descending into the |
|
2024 first level of the proof-tree, as follows. |
|
2025 |
|
2026 @{ML_response [display,gray] |
|
2027 "@{thm my_conjIa} |
|
2028 |> Thm.proof_body_of |
|
2029 |> get_pbodies |
|
2030 |> map get_names |
|
2031 |> List.concat" |
|
2032 "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\", |
|
2033 \"Pure.protectI\"]"} |
|
2034 |
|
2035 The theorems @{thm [source] protectD} and @{thm [source] |
|
2036 protectI} that are internal theorems are always part of a |
|
2037 proof in Isabelle. Note also that applications of @{text assumption} do not |
|
2038 count as a separate theorem, as you can see in the following code. |
|
2039 |
|
2040 @{ML_response [display,gray] |
|
2041 "@{thm my_conjIb} |
|
2042 |> Thm.proof_body_of |
|
2043 |> get_pbodies |
|
2044 |> map get_names |
|
2045 |> List.concat" |
|
2046 "[\"Pure.protectD\", \"Pure.protectI\"]"} |
|
2047 |
|
2048 Interestingly, but not surprisingly, the proof of @{thm [source] |
|
2049 my_conjIc} procceeds quite differently from @{thm [source] my_conjIa} |
|
2050 and @{thm [source] my_conjIb}, as can be seen by the theorems that |
|
2051 are returned for @{thm [source] my_conjIc}. |
|
2052 |
|
2053 @{ML_response [display,gray] |
|
2054 "@{thm my_conjIc} |
|
2055 |> Thm.proof_body_of |
|
2056 |> get_pbodies |
|
2057 |> map get_names |
|
2058 |> List.concat" |
|
2059 "[\"HOL.Eq_TrueI\", \"HOL.simp_thms_25\", \"HOL.eq_reflection\", |
|
2060 \"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.TrueI\", \"Pure.protectD\", |
|
2061 \"Pure.protectI\"]"} |
|
2062 |
|
2063 Of course we can also descend into the second level of the tree |
|
2064 ``behind'' @{thm [source] my_conjIa} say, which |
|
2065 means we obtain the theorems that are used in order to prove |
|
2066 @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}. |
|
2067 |
|
2068 @{ML_response [display, gray] |
|
2069 "@{thm my_conjIa} |
|
2070 |> Thm.proof_body_of |
|
2071 |> get_pbodies |
|
2072 |> map get_pbodies |
|
2073 |> (map o map) get_names |
|
2074 |> List.concat |
|
2075 |> List.concat |
|
2076 |> duplicates (op=)" |
|
2077 "[\"HOL.spec\", \"HOL.and_def\", \"HOL.mp\", \"HOL.impI\", \"Pure.protectD\", |
|
2078 \"Pure.protectI\"]"} |
|
2079 |
|
2080 \begin{readmore} |
|
2081 The data-structure @{ML_type proof_body} is implemented |
|
2082 in the file @{ML_file "Pure/proofterm.ML"}. The implementation |
|
2083 of theorems and related functions are in @{ML_file "Pure/thm.ML"}. |
|
2084 \end{readmore} |
|
2085 |
1969 One great feature of Isabelle is its document preparation system, where |
2086 One great feature of Isabelle is its document preparation system, where |
1970 proved theorems can be quoted in documents referencing directly their |
2087 proved theorems can be quoted in documents referencing directly their |
1971 formalisation. This helps tremendously to minimise cut-and-paste errors. However, |
2088 formalisation. This helps tremendously to minimise cut-and-paste errors. However, |
1972 sometimes the verbatim quoting is not what is wanted or what can be shown to |
2089 sometimes the verbatim quoting is not what is wanted or what can be shown to |
1973 readers. For such situations Isabelle allows the installation of \emph{\index*{theorem |
2090 readers. For such situations Isabelle allows the installation of \emph{\index*{theorem |