--- a/ProgTutorial/Essential.thy Tue Jun 19 17:58:12 2012 +0100
+++ b/ProgTutorial/Essential.thy Wed Jun 20 08:29:12 2012 +0100
@@ -1513,8 +1513,8 @@
val assm2 = @{cprop "(P::nat \<Rightarrow> bool) t"}
val Pt_implies_Qt =
- Thm.assume assm1
- |> Thm.forall_elim @{cterm "t::nat"}
+ Thm.assume assm1
+ |> Thm.forall_elim @{cterm "t::nat"}
val Qt = Thm.implies_elim Pt_implies_Qt (Thm.assume assm2)
in
@@ -1568,8 +1568,8 @@
The first argument of @{ML note in Local_Theory} is the name under
which we store the theorem or theorems. The second argument can contain a
list of theorem attributes, which we will explain in detail in
- Section~\ref{sec:attributes}. Below we just use one such attribute for
- adding the theorem to the simpset:
+ Section~\ref{sec:attributes}. Below we just use one such attribute,
+ @{ML_ind simp_add in Simplifier}, for adding the theorem to the simpset:
*}
local_setup %gray {*
@@ -1928,7 +1928,7 @@
*}
lemma
- shows "Q \<Longrightarrow> Q \<Longrightarrow> Q"
+shows "Q \<Longrightarrow> Q \<Longrightarrow> Q"
proof (cases rule: foo_data')
(*<*)oops(*>*)
@@ -1950,7 +1950,7 @@
*}
lemma
- shows "Q \<Longrightarrow> Q \<Longrightarrow> Q"
+shows "Q \<Longrightarrow> Q \<Longrightarrow> Q"
proof (cases rule: foo_data)
(*<*)oops(*>*)
@@ -1964,8 +1964,125 @@
@{text "> let \"?case\" = \"?P\""}
\end{tabular}*}
+
+text {*
+ One often wants to know the theorems that are used in the proof
+ of a theorem. They can be obtained by introspecting the theorem.
+ To introspect a theorem, let us define the following three functions that
+ analyse the @{ML_type_ind proof_body} data-structure from the structure
+ @{ML_struct Proofterm}.
+*}
+
+ML %grayML{*fun pthms_of (PBody {thms, ...}) = map #2 thms
+val get_names = map #1 o pthms_of
+val get_pbodies = map (Future.join o #3) o pthms_of *}
+
+text {*
+ To see what their purpose is, consider the following three short proofs.
+*}
+
+lemma my_conjIa:
+shows "A \<and> B \<Longrightarrow> A \<and> B"
+apply(rule conjI)
+apply(drule conjunct1)
+apply(assumption)
+apply(drule conjunct2)
+apply(assumption)
+done
+
+lemma my_conjIb:
+shows "A \<and> B \<Longrightarrow> A \<and> B"
+apply(assumption)
+done
+
+lemma my_conjIc:
+shows "A \<and> B \<Longrightarrow> A \<and> B"
+apply(auto)
+done
text {*
+ While the information about which theorems are used is obvious in
+ the first two proofs, it is not obvious in the third, because of the
+ @{text auto}-step. Fortunately, ``behind'' every proved theorem is
+ a proof-tree that records all theorems that are employed for
+ establishing this theorem. We can traverse this proof-tree
+ extracting this information. Let us first extract the name of the
+ established theorem. This can be done with
+
+ @{ML_response [display,gray]
+ "@{thm my_conjIa}
+ |> Thm.proof_body_of
+ |> get_names"
+ "[\"Essential.my_conjIa\"]"}
+
+ whereby @{text "Essential"} refers to the theory name in which
+ we established the theorem @{thm [source] my_conjIa}. The function @{ML_ind
+ proof_body_of in Thm} returns a part of the data that is stored in a
+ theorem. Notice that the first proof above references
+ three theorems, namely @{thm [source] conjI}, @{thm [source] conjunct1}
+ and @{thm [source] conjunct2}. We can obtain them by descending into the
+ first level of the proof-tree, as follows.
+
+ @{ML_response [display,gray]
+ "@{thm my_conjIa}
+ |> Thm.proof_body_of
+ |> get_pbodies
+ |> map get_names
+ |> List.concat"
+ "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\",
+ \"Pure.protectI\"]"}
+
+ The theorems @{thm [source] protectD} and @{thm [source]
+ protectI} that are internal theorems are always part of a
+ proof in Isabelle. Note also that applications of @{text assumption} do not
+ count as a separate theorem, as you can see in the following code.
+
+ @{ML_response [display,gray]
+ "@{thm my_conjIb}
+ |> Thm.proof_body_of
+ |> get_pbodies
+ |> map get_names
+ |> List.concat"
+ "[\"Pure.protectD\", \"Pure.protectI\"]"}
+
+ Interestingly, but not surprisingly, the proof of @{thm [source]
+ my_conjIc} procceeds quite differently from @{thm [source] my_conjIa}
+ and @{thm [source] my_conjIb}, as can be seen by the theorems that
+ are returned for @{thm [source] my_conjIc}.
+
+ @{ML_response [display,gray]
+ "@{thm my_conjIc}
+ |> Thm.proof_body_of
+ |> get_pbodies
+ |> map get_names
+ |> List.concat"
+ "[\"HOL.Eq_TrueI\", \"HOL.simp_thms_25\", \"HOL.eq_reflection\",
+ \"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.TrueI\", \"Pure.protectD\",
+ \"Pure.protectI\"]"}
+
+ Of course we can also descend into the second level of the tree
+ ``behind'' @{thm [source] my_conjIa} say, which
+ means we obtain the theorems that are used in order to prove
+ @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}.
+
+ @{ML_response [display, gray]
+ "@{thm my_conjIa}
+ |> Thm.proof_body_of
+ |> get_pbodies
+ |> map get_pbodies
+ |> (map o map) get_names
+ |> List.concat
+ |> List.concat
+ |> duplicates (op=)"
+ "[\"HOL.spec\", \"HOL.and_def\", \"HOL.mp\", \"HOL.impI\", \"Pure.protectD\",
+ \"Pure.protectI\"]"}
+
+ \begin{readmore}
+ The data-structure @{ML_type proof_body} is implemented
+ in the file @{ML_file "Pure/proofterm.ML"}. The implementation
+ of theorems and related functions are in @{ML_file "Pure/thm.ML"}.
+ \end{readmore}
+
One great feature of Isabelle is its document preparation system, where
proved theorems can be quoted in documents referencing directly their
formalisation. This helps tremendously to minimise cut-and-paste errors. However,
@@ -2002,7 +2119,7 @@
*}
theorem style_test:
- shows "\<forall>x y z. (x, x) = (y, z)" sorry
+shows "\<forall>x y z. (x, x) = (y, z)" sorry
text {*
Now printing out in a document the theorem @{thm [source] style_test} normally