1319   about the type variable.

  1319   about the type variable.

  1320 *}

  1320 *}

  1321 

  1321 

  1322 

  1322 

  1323 ML {* Sign.classes_of @{theory} *}

  1323 ML {* Sign.classes_of @{theory} *}

  1324 

  1326 

  1325 text {*

  1327 text {*

  1326   \begin{readmore}

  1328   \begin{readmore}

  1327   Classes, sorts and arities are defined in @{ML_file "Pure/term.ML"}.

  1329   Classes, sorts and arities are defined in @{ML_file "Pure/term.ML"}.

  1328   

  1330   

  2012 lemma my_conjIc:

  2014 lemma my_conjIc:

  2013 shows "A \<and> B \<Longrightarrow> A \<and> B"

  2015 shows "A \<and> B \<Longrightarrow> A \<and> B"

  2014 apply(auto)

  2016 apply(auto)

  2015 done

  2017 done

  2016 

  2018 

  2017 text {*

  2020 text {*

  2018   While the information about which theorems are used is obvious in

  2021   While the information about which theorems are used is obvious in

  2019   the first two proofs, it is not obvious in the third, because of the

  2022   the first two proofs, it is not obvious in the third, because of the

  2020   @{text auto}-step.  Fortunately, ``behind'' every proved theorem is

  2023   @{text auto}-step.  Fortunately, ``behind'' every proved theorem is

  2021   a proof-tree that records all theorems that are employed for

  2024   a proof-tree that records all theorems that are employed for

  2022   establishing this theorem.  We can traverse this proof-tree

  2025   establishing this theorem.  We can traverse this proof-tree

  2023   extracting this information.  Let us first extract the name of the

  2026   extracting this information.  Let us first extract the name of the

  2024   established theorem. This can be done with

  2027   established theorem. This can be done with

  2025 

  2028 

  2027   "@{thm my_conjIa}

  2030   "@{thm my_conjIa}

  2028   |> Thm.proof_body_of

  2031   |> Thm.proof_body_of

  2029   |> get_names"

  2032   |> get_names"

  2030   "[\"Essential.my_conjIa\"]"}

  2033   "[\"Essential.my_conjIa\"]"}

  2031 

  2034 

  2035   theorem.  Notice that the first proof above references

  2038   theorem.  Notice that the first proof above references

  2036   three theorems, namely @{thm [source] conjI}, @{thm [source] conjunct1} 

  2039   three theorems, namely @{thm [source] conjI}, @{thm [source] conjunct1} 

  2037   and @{thm [source] conjunct2}. We can obtain them by descending into the

  2040   and @{thm [source] conjunct2}. We can obtain them by descending into the

  2038   first level of the proof-tree, as follows.

  2041   first level of the proof-tree, as follows.

  2039 

  2042 

  2041   "@{thm my_conjIa}

  2044   "@{thm my_conjIa}

  2042   |> Thm.proof_body_of

  2045   |> Thm.proof_body_of

  2043   |> get_pbodies

  2046   |> get_pbodies

  2044   |> map get_names

  2047   |> map get_names

  2045   |> List.concat"

  2048   |> List.concat"

  2049   The theorems @{thm [source] Pure.protectD} and @{thm [source]

  2052   The theorems @{thm [source] Pure.protectD} and @{thm [source]

  2050   Pure.protectI} that are internal theorems are always part of a

  2053   Pure.protectI} that are internal theorems are always part of a

  2051   proof in Isabelle. Note also that applications of @{text assumption} do not

  2054   proof in Isabelle. Note also that applications of @{text assumption} do not

  2052   count as a separate theorem, as you can see in the following code.

  2055   count as a separate theorem, as you can see in the following code.

  2053 

  2056 

  2055   "@{thm my_conjIb}

  2058   "@{thm my_conjIb}

  2056   |> Thm.proof_body_of

  2059   |> Thm.proof_body_of

  2057   |> get_pbodies

  2060   |> get_pbodies

  2058   |> map get_names

  2061   |> map get_names

  2059   |> List.concat"

  2062   |> List.concat"

  2062   Interestingly, but not surprisingly, the proof of @{thm [source]

  2065   Interestingly, but not surprisingly, the proof of @{thm [source]

  2063   my_conjIc} procceeds quite differently from @{thm [source] my_conjIa}

  2066   my_conjIc} procceeds quite differently from @{thm [source] my_conjIa}

  2064   and @{thm [source] my_conjIb}, as can be seen by the theorems that

  2067   and @{thm [source] my_conjIb}, as can be seen by the theorems that

  2065   are returned for @{thm [source] my_conjIc}.

  2068   are returned for @{thm [source] my_conjIc}.

  2066 

  2069 

  2068   "@{thm my_conjIc}

  2071   "@{thm my_conjIc}

  2069   |> Thm.proof_body_of

  2072   |> Thm.proof_body_of

  2070   |> get_pbodies

  2073   |> get_pbodies

  2071   |> map get_names

  2074   |> map get_names

  2072   |> List.concat"

  2075   |> List.concat"

  2077   Of course we can also descend into the second level of the tree 

  2080   Of course we can also descend into the second level of the tree 

  2078   ``behind'' @{thm [source] my_conjIa} say, which

  2081   ``behind'' @{thm [source] my_conjIa} say, which

  2079   means we obtain the theorems that are used in order to prove

  2082   means we obtain the theorems that are used in order to prove

  2080   @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}.

  2083   @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}.

  2081 

  2084 

  2083   "@{thm my_conjIa}

  2086   "@{thm my_conjIa}

  2084   |> Thm.proof_body_of

  2087   |> Thm.proof_body_of

  2085   |> get_pbodies

  2088   |> get_pbodies

  2086   |> map get_pbodies

  2089   |> map get_pbodies

  2087   |> (map o map) get_names

  2090   |> (map o map) get_names