equal
deleted
inserted
replaced
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 involved in proving |
1969 Sometimes one wants to know the theorems that are involved in |
1970 a theorem. They can be obtained by introspecting the theorem. |
1970 proving a theorem, especially when the proof is by @{text |
1971 To introspect a theorem, let us define the following three functions that |
1971 auto}. These theorems can be obtained by introspecting the proved theorem. |
1972 analyse the @{ML_type_ind proof_body} data-structure from the structure |
1972 To introspect a theorem, let us define the following three functions |
1973 @{ML_struct Proofterm}. |
1973 that analyse the @{ML_type_ind proof_body} data-structure from the |
|
1974 structure @{ML_struct Proofterm}. |
1974 *} |
1975 *} |
1975 |
1976 |
1976 ML %grayML{*fun pthms_of (PBody {thms, ...}) = map #2 thms |
1977 ML %grayML{*fun pthms_of (PBody {thms, ...}) = map #2 thms |
1977 val get_names = map #1 o pthms_of |
1978 val get_names = map #1 o pthms_of |
1978 val get_pbodies = map (Future.join o #3) o pthms_of *} |
1979 val get_pbodies = map (Future.join o #3) o pthms_of *} |
2030 |> map get_names |
2031 |> map get_names |
2031 |> List.concat" |
2032 |> List.concat" |
2032 "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\", |
2033 "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\", |
2033 \"Pure.protectI\"]"} |
2034 \"Pure.protectI\"]"} |
2034 |
2035 |
2035 The theorems @{thm [source] protectD} and @{thm [source] |
2036 The theorems @{thm [source] Pure.protectD} and @{thm [source] |
2036 protectI} that are internal theorems are always part of a |
2037 Pure.protectI} that are internal theorems are always part of a |
2037 proof in Isabelle. Note also that applications of @{text assumption} do not |
2038 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 count as a separate theorem, as you can see in the following code. |
2039 |
2040 |
2040 @{ML_response [display,gray] |
2041 @{ML_response [display,gray] |
2041 "@{thm my_conjIb} |
2042 "@{thm my_conjIb} |
2074 |> List.concat |
2075 |> List.concat |
2075 |> List.concat |
2076 |> List.concat |
2076 |> duplicates (op=)" |
2077 |> duplicates (op=)" |
2077 "[\"HOL.spec\", \"HOL.and_def\", \"HOL.mp\", \"HOL.impI\", \"Pure.protectD\", |
2078 "[\"HOL.spec\", \"HOL.and_def\", \"HOL.mp\", \"HOL.impI\", \"Pure.protectD\", |
2078 \"Pure.protectI\"]"} |
2079 \"Pure.protectI\"]"} |
|
2080 |
|
2081 \begin{exercise} |
|
2082 Have a look at the theorems that are used when a lemma is ``proved'' |
|
2083 by \isacommand{sorry}? |
|
2084 \end{exercise} |
2079 |
2085 |
2080 \begin{readmore} |
2086 \begin{readmore} |
2081 The data-structure @{ML_type proof_body} is implemented |
2087 The data-structure @{ML_type proof_body} is implemented |
2082 in the file @{ML_file "Pure/proofterm.ML"}. The implementation |
2088 in the file @{ML_file "Pure/proofterm.ML"}. The implementation |
2083 of theorems and related functions are in @{ML_file "Pure/thm.ML"}. |
2089 of theorems and related functions are in @{ML_file "Pure/thm.ML"}. |