# HG changeset patch # User wenzelm # Date 1371490241 -7200 # Node ID fb1fb867c1461ab4539a8bf24ff82ecb75159449 # Parent 47c62377be787a5e5505e487d223ff69b5666dea more examples on proof terms; diff -r 47c62377be78 -r fb1fb867c146 src/Doc/IsarImplementation/Logic.thy --- a/src/Doc/IsarImplementation/Logic.thy Sat Jun 15 21:07:32 2013 +0200 +++ b/src/Doc/IsarImplementation/Logic.thy Mon Jun 17 19:30:41 2013 +0200 @@ -1314,4 +1314,107 @@ \end{description} *} +text %mlex {* Detailed proof information of a theorem may be retrieved + as follows: *} + +lemma ex: "A \ B \ B \ A" +proof + assume "A \ B" + then obtain B and A .. + then show "B \ A" .. +qed + +ML_val {* + (*proof body with digest*) + val body = Proofterm.strip_thm (Thm.proof_body_of @{thm ex}); + + (*proof term only*) + val prf = Proofterm.proof_of body; + Pretty.writeln (Proof_Syntax.pretty_proof @{context} prf); + + (*all theorems used in the graph of nested proofs*) + val all_thms = + Proofterm.fold_body_thms + (fn (name, _, _) => insert (op =) name) [body] []; +*} + +text {* The result refers to various basic facts of Isabelle/HOL: + @{thm [source] HOL.impI}, @{thm [source] HOL.conjE}, @{thm [source] + HOL.conjI} etc. The combinator @{ML Proofterm.fold_body_thms} + recursively explores the graph of the proofs of all theorems being + used here. + + \medskip Alternatively, we may produce a proof term manually, and + turn it into a theorem as follows: *} + +ML_val {* + val thy = @{theory}; + val prf = + Proof_Syntax.read_proof thy true false + "impI \ _ \ _ \ \ + \ (Lam H: _. \ + \ conjE \ _ \ _ \ _ \ H \ \ + \ (Lam (H: _) Ha: _. conjI \ _ \ _ \ Ha \ H))"; + val thm = + prf + |> Reconstruct.reconstruct_proof thy @{prop "A \ B \ B \ A"} + |> Proof_Checker.thm_of_proof thy + |> Drule.export_without_context; +*} + +text {* \medskip The subsequent example illustrates the use of various + key operations on proof terms: the proof term of an existing theorem + is reconstructed and turned again into a theorem using the proof + checker; some informative output is printed as well. *} + +ML {* + fun recheck ctxt0 thm0 = + let + (*formal transfer and import -- avoid schematic variables*) + val thy = Proof_Context.theory_of ctxt0; + val ((_, [thm]), ctxt) = + Variable.import true [Thm.transfer thy thm0] ctxt0; + + (*main proof information*) + val prop = Thm.prop_of thm; + val prf = + Proofterm.proof_of + (Proofterm.strip_thm (Thm.proof_body_of thm)); + val full_prf = Reconstruct.reconstruct_proof thy prop prf; + + (*informative output*) + fun pretty_item name prt = + Pretty.block [Pretty.str name, Pretty.brk 1, prt]; + val _ = + [pretty_item "proposition:" (Syntax.pretty_term ctxt prop), + pretty_item "proof:" (Proof_Syntax.pretty_proof ctxt prf), + pretty_item "full proof:" + (Proof_Syntax.pretty_proof ctxt full_prf)] + |> Pretty.chunks |> Pretty.writeln; + + (*rechecked theorem*) + val thm' = + Proof_Checker.thm_of_proof thy full_prf + |> singleton (Proof_Context.export ctxt ctxt0); + in thm' end; +*} + +text {* As anticipated, the rechecked theorem establishes the same + proposition: *} + +ML_val {* + val thm = @{thm ex}; + val thm' = recheck @{context} thm; + @{assert} (Thm.eq_thm_prop (thm, thm')); +*} + +text {* More precise theorem equality is achieved by adjusting a few + accidental details of the theorems involved here: *} + +ML_val {* + val thm = Thm.map_tags (K []) @{thm ex}; + val thm' = Thm.strip_shyps (recheck @{context} thm); + @{assert} (Thm.eq_thm (thm, thm')); +*} + end diff -r 47c62377be78 -r fb1fb867c146 src/Doc/ROOT --- a/src/Doc/ROOT Sat Jun 15 21:07:32 2013 +0200 +++ b/src/Doc/ROOT Mon Jun 17 19:30:41 2013 +0200 @@ -69,19 +69,20 @@ "document/build" "document/root.tex" -session IsarImplementation (doc) in "IsarImplementation" = HOL + +session IsarImplementation (doc) in "IsarImplementation" = "HOL-Proofs" + options [document_variants = "implementation"] theories Eq Integration Isar Local_Theory - Logic ML Prelim Proof Syntax Tactic + theories [proofs = 2, parallel_proofs = 0] + Logic files "../prepare_document" "../pdfsetup.sty" diff -r 47c62377be78 -r fb1fb867c146 src/Doc/Ref/document/thm.tex --- a/src/Doc/Ref/document/thm.tex Sat Jun 15 21:07:32 2013 +0200 +++ b/src/Doc/Ref/document/thm.tex Mon Jun 17 19:30:41 2013 +0200 @@ -3,26 +3,6 @@ \section{Proof terms}\label{sec:proofObjects} -Each theorem's derivation is stored as the {\tt der} field of its internal -record: -\begin{ttbox} -#2 (#der (rep_thm conjI)); -{\out PThm (("HOL.conjI", []),} -{\out AbsP ("H", None, AbsP ("H", None, \dots)), \dots, None) %} -{\out None % None : Proofterm.proof} -\end{ttbox} -This proof term identifies a labelled theorem, {\tt conjI} of theory -\texttt{HOL}, whose underlying proof is -{\tt AbsP ("H", None, AbsP ("H", None, $\dots$))}. -The theorem is applied to two (implicit) term arguments, which correspond -to the two variables occurring in its proposition. - -Reconstruction and checking of proofs as described in \S\ref{sec:reconstruct_proofs} -will not work for proofs constructed with {\tt proofs} set to -{\tt 0} or {\tt 1}. -Theorems involving oracles will be printed with a -suffixed \verb|[!]| to point out the different quality of confidence achieved. - \subsection{Reconstructing and checking proof terms}\label{sec:reconstruct_proofs} \index{proof terms!reconstructing} \index{proof terms!checking} @@ -115,45 +95,6 @@ argument which indicates whether the proof term should be reconstructed before printing. -The following example (based on Isabelle/HOL) illustrates how -to parse and check proof terms. We start by parsing a partial -proof term -\begin{ttbox} -val prf = ProofSyntax.read_proof Main.thy false - "impI % _ % _ %% (Lam H : _. conjE % _ % _ % _ %% H %% - (Lam (H1 : _) H2 : _. conjI % _ % _ %% H2 %% H1))"; -{\out val prf = PThm (("HOL.impI", []), \dots, \dots, None) % None % None %%} -{\out AbsP ("H", None, PThm (("HOL.conjE", []), \dots, \dots, None) %} -{\out None % None % None %% PBound 0 %%} -{\out AbsP ("H1", None, AbsP ("H2", None, \dots))) : Proofterm.proof} -\end{ttbox} -The statement to be established by this proof is -\begin{ttbox} -val t = term_of - (read_cterm (sign_of Main.thy) ("A & B --> B & A", propT)); -{\out val t = Const ("Trueprop", "bool => prop") $} -{\out (Const ("op -->", "[bool, bool] => bool") $} -{\out \dots $ \dots : Term.term} -\end{ttbox} -Using {\tt t} we can reconstruct the full proof -\begin{ttbox} -val prf' = Reconstruct.reconstruct_proof (sign_of Main.thy) t prf; -{\out val prf' = PThm (("HOL.impI", []), \dots, \dots, Some []) %} -{\out Some (Const ("op &", \dots) $ Free ("A", \dots) $ Free ("B", \dots)) %} -{\out Some (Const ("op &", \dots) $ Free ("B", \dots) $ Free ("A", \dots)) %%} -{\out AbsP ("H", Some (Const ("Trueprop", \dots) $ \dots), \dots)} -{\out : Proofterm.proof} -\end{ttbox} -This proof can finally be turned into a theorem -\begin{ttbox} -val thm = ProofChecker.thm_of_proof Main.thy prf'; -{\out val thm = "A & B --> B & A" : Thm.thm} -\end{ttbox} - -\index{proof terms|)} -\index{theorems|)} - - %%% Local Variables: %%% mode: latex %%% TeX-master: "ref"