diff -r e2c0138b5cea -r 13d7ea419c5f ProgTutorial/Essential.thy --- 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 \ 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 \ Q \ Q" +shows "Q \ Q \ Q" proof (cases rule: foo_data') (*<*)oops(*>*) @@ -1950,7 +1950,7 @@ *} lemma - shows "Q \ Q \ Q" +shows "Q \ Q \ 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 \ B \ A \ B" +apply(rule conjI) +apply(drule conjunct1) +apply(assumption) +apply(drule conjunct2) +apply(assumption) +done + +lemma my_conjIb: +shows "A \ B \ A \ B" +apply(assumption) +done + +lemma my_conjIc: +shows "A \ B \ A \ 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 "\x y z. (x, x) = (y, z)" sorry +shows "\x y z. (x, x) = (y, z)" sorry text {* Now printing out in a document the theorem @{thm [source] style_test} normally