more examples on proof terms;
authorwenzelm
Mon Jun 17 19:30:41 2013 +0200 (2013-06-17)
changeset 52410fb1fb867c146
parent 52409 47c62377be78
child 52411 f192c4ea5b17
more examples on proof terms;
src/Doc/IsarImplementation/Logic.thy
src/Doc/ROOT
src/Doc/Ref/document/thm.tex
src/HOL/Tools/reflection.ML
     1.1 --- a/src/Doc/IsarImplementation/Logic.thy	Sat Jun 15 21:07:32 2013 +0200
     1.2 +++ b/src/Doc/IsarImplementation/Logic.thy	Mon Jun 17 19:30:41 2013 +0200
     1.3 @@ -1314,4 +1314,107 @@
     1.4    \end{description}
     1.5  *}
     1.6  
     1.7 +text %mlex {* Detailed proof information of a theorem may be retrieved
     1.8 +  as follows: *}
     1.9 +
    1.10 +lemma ex: "A \<and> B \<longrightarrow> B \<and> A"
    1.11 +proof
    1.12 +  assume "A \<and> B"
    1.13 +  then obtain B and A ..
    1.14 +  then show "B \<and> A" ..
    1.15 +qed
    1.16 +
    1.17 +ML_val {*
    1.18 +  (*proof body with digest*)
    1.19 +  val body = Proofterm.strip_thm (Thm.proof_body_of @{thm ex});
    1.20 +
    1.21 +  (*proof term only*)
    1.22 +  val prf = Proofterm.proof_of body;
    1.23 +  Pretty.writeln (Proof_Syntax.pretty_proof @{context} prf);
    1.24 +
    1.25 +  (*all theorems used in the graph of nested proofs*)
    1.26 +  val all_thms =
    1.27 +    Proofterm.fold_body_thms
    1.28 +      (fn (name, _, _) => insert (op =) name) [body] [];
    1.29 +*}
    1.30 +
    1.31 +text {* The result refers to various basic facts of Isabelle/HOL:
    1.32 +  @{thm [source] HOL.impI}, @{thm [source] HOL.conjE}, @{thm [source]
    1.33 +  HOL.conjI} etc.  The combinator @{ML Proofterm.fold_body_thms}
    1.34 +  recursively explores the graph of the proofs of all theorems being
    1.35 +  used here.
    1.36 +
    1.37 +  \medskip Alternatively, we may produce a proof term manually, and
    1.38 +  turn it into a theorem as follows: *}
    1.39 +
    1.40 +ML_val {*
    1.41 +  val thy = @{theory};
    1.42 +  val prf =
    1.43 +    Proof_Syntax.read_proof thy true false
    1.44 +      "impI \<cdot> _ \<cdot> _ \<bullet> \
    1.45 +      \   (Lam H: _. \
    1.46 +      \     conjE \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> H \<bullet> \
    1.47 +      \       (Lam (H: _) Ha: _. conjI \<cdot> _ \<cdot> _ \<bullet> Ha \<bullet> H))";
    1.48 +  val thm =
    1.49 +    prf
    1.50 +    |> Reconstruct.reconstruct_proof thy @{prop "A \<and> B \<longrightarrow> B \<and> A"}
    1.51 +    |> Proof_Checker.thm_of_proof thy
    1.52 +    |> Drule.export_without_context;
    1.53 +*}
    1.54 +
    1.55 +text {* \medskip The subsequent example illustrates the use of various
    1.56 +  key operations on proof terms: the proof term of an existing theorem
    1.57 +  is reconstructed and turned again into a theorem using the proof
    1.58 +  checker; some informative output is printed as well.  *}
    1.59 +
    1.60 +ML {*
    1.61 +  fun recheck ctxt0 thm0 =
    1.62 +    let
    1.63 +      (*formal transfer and import -- avoid schematic variables*)
    1.64 +      val thy = Proof_Context.theory_of ctxt0;
    1.65 +      val ((_, [thm]), ctxt) =
    1.66 +        Variable.import true [Thm.transfer thy thm0] ctxt0;
    1.67 +
    1.68 +      (*main proof information*)
    1.69 +      val prop = Thm.prop_of thm;
    1.70 +      val prf =
    1.71 +        Proofterm.proof_of
    1.72 +          (Proofterm.strip_thm (Thm.proof_body_of thm));
    1.73 +      val full_prf = Reconstruct.reconstruct_proof thy prop prf;
    1.74 +
    1.75 +      (*informative output*)
    1.76 +      fun pretty_item name prt =
    1.77 +        Pretty.block [Pretty.str name, Pretty.brk 1, prt];
    1.78 +      val _ =
    1.79 +        [pretty_item "proposition:" (Syntax.pretty_term ctxt prop),
    1.80 +         pretty_item "proof:" (Proof_Syntax.pretty_proof ctxt prf),
    1.81 +         pretty_item "full proof:"
    1.82 +          (Proof_Syntax.pretty_proof ctxt full_prf)]
    1.83 +        |> Pretty.chunks |> Pretty.writeln;
    1.84 +
    1.85 +      (*rechecked theorem*)
    1.86 +      val thm' =
    1.87 +        Proof_Checker.thm_of_proof thy full_prf
    1.88 +        |> singleton (Proof_Context.export ctxt ctxt0);
    1.89 +    in thm' end;
    1.90 +*}
    1.91 +
    1.92 +text {* As anticipated, the rechecked theorem establishes the same
    1.93 +  proposition: *}
    1.94 +
    1.95 +ML_val {*
    1.96 +  val thm = @{thm ex};
    1.97 +  val thm' = recheck @{context} thm;
    1.98 +  @{assert} (Thm.eq_thm_prop (thm, thm'));
    1.99 +*}
   1.100 +
   1.101 +text {* More precise theorem equality is achieved by adjusting a few
   1.102 +  accidental details of the theorems involved here: *}
   1.103 +
   1.104 +ML_val {*
   1.105 +  val thm = Thm.map_tags (K []) @{thm ex};
   1.106 +  val thm' = Thm.strip_shyps (recheck @{context} thm);
   1.107 +  @{assert} (Thm.eq_thm (thm, thm'));
   1.108 +*}
   1.109 +
   1.110  end
     2.1 --- a/src/Doc/ROOT	Sat Jun 15 21:07:32 2013 +0200
     2.2 +++ b/src/Doc/ROOT	Mon Jun 17 19:30:41 2013 +0200
     2.3 @@ -69,19 +69,20 @@
     2.4      "document/build"
     2.5      "document/root.tex"
     2.6  
     2.7 -session IsarImplementation (doc) in "IsarImplementation" = HOL +
     2.8 +session IsarImplementation (doc) in "IsarImplementation" = "HOL-Proofs" +
     2.9    options [document_variants = "implementation"]
    2.10    theories
    2.11      Eq
    2.12      Integration
    2.13      Isar
    2.14      Local_Theory
    2.15 -    Logic
    2.16      ML
    2.17      Prelim
    2.18      Proof
    2.19      Syntax
    2.20      Tactic
    2.21 +  theories [proofs = 2, parallel_proofs = 0]
    2.22 +    Logic
    2.23    files
    2.24      "../prepare_document"
    2.25      "../pdfsetup.sty"
     3.1 --- a/src/Doc/Ref/document/thm.tex	Sat Jun 15 21:07:32 2013 +0200
     3.2 +++ b/src/Doc/Ref/document/thm.tex	Mon Jun 17 19:30:41 2013 +0200
     3.3 @@ -3,26 +3,6 @@
     3.4  
     3.5  \section{Proof terms}\label{sec:proofObjects}
     3.6  
     3.7 -Each theorem's derivation is stored as the {\tt der} field of its internal
     3.8 -record: 
     3.9 -\begin{ttbox} 
    3.10 -#2 (#der (rep_thm conjI));
    3.11 -{\out PThm (("HOL.conjI", []),}
    3.12 -{\out   AbsP ("H", None, AbsP ("H", None, \dots)), \dots, None) %}
    3.13 -{\out     None % None : Proofterm.proof}
    3.14 -\end{ttbox}
    3.15 -This proof term identifies a labelled theorem, {\tt conjI} of theory
    3.16 -\texttt{HOL}, whose underlying proof is
    3.17 -{\tt AbsP ("H", None, AbsP ("H", None, $\dots$))}. 
    3.18 -The theorem is applied to two (implicit) term arguments, which correspond
    3.19 -to the two variables occurring in its proposition.
    3.20 -
    3.21 -Reconstruction and checking of proofs as described in \S\ref{sec:reconstruct_proofs}
    3.22 -will not work for proofs constructed with {\tt proofs} set to
    3.23 -{\tt 0} or {\tt 1}.
    3.24 -Theorems involving oracles will be printed with a
    3.25 -suffixed \verb|[!]| to point out the different quality of confidence achieved.
    3.26 -
    3.27  \subsection{Reconstructing and checking proof terms}\label{sec:reconstruct_proofs}
    3.28  \index{proof terms!reconstructing}
    3.29  \index{proof terms!checking}
    3.30 @@ -115,45 +95,6 @@
    3.31  argument which indicates whether the proof term should
    3.32  be reconstructed before printing.
    3.33  
    3.34 -The following example (based on Isabelle/HOL) illustrates how
    3.35 -to parse and check proof terms. We start by parsing a partial
    3.36 -proof term
    3.37 -\begin{ttbox}
    3.38 -val prf = ProofSyntax.read_proof Main.thy false
    3.39 -  "impI % _ % _ %% (Lam H : _. conjE % _ % _ % _ %% H %%
    3.40 -     (Lam (H1 : _) H2 : _. conjI % _ % _ %% H2 %% H1))";
    3.41 -{\out val prf = PThm (("HOL.impI", []), \dots, \dots, None) % None % None %%}
    3.42 -{\out   AbsP ("H", None, PThm (("HOL.conjE", []), \dots, \dots, None) %}
    3.43 -{\out     None % None % None %% PBound 0 %%}
    3.44 -{\out     AbsP ("H1", None, AbsP ("H2", None, \dots))) : Proofterm.proof}
    3.45 -\end{ttbox}
    3.46 -The statement to be established by this proof is
    3.47 -\begin{ttbox}
    3.48 -val t = term_of
    3.49 -  (read_cterm (sign_of Main.thy) ("A & B --> B & A", propT));
    3.50 -{\out val t = Const ("Trueprop", "bool => prop") $}
    3.51 -{\out   (Const ("op -->", "[bool, bool] => bool") $}
    3.52 -{\out     \dots $ \dots : Term.term}
    3.53 -\end{ttbox}
    3.54 -Using {\tt t} we can reconstruct the full proof
    3.55 -\begin{ttbox}
    3.56 -val prf' = Reconstruct.reconstruct_proof (sign_of Main.thy) t prf;
    3.57 -{\out val prf' = PThm (("HOL.impI", []), \dots, \dots, Some []) %}
    3.58 -{\out   Some (Const ("op &", \dots) $ Free ("A", \dots) $ Free ("B", \dots)) %}
    3.59 -{\out   Some (Const ("op &", \dots) $ Free ("B", \dots) $ Free ("A", \dots)) %%}
    3.60 -{\out   AbsP ("H", Some (Const ("Trueprop", \dots) $ \dots), \dots)}
    3.61 -{\out     : Proofterm.proof}
    3.62 -\end{ttbox}
    3.63 -This proof can finally be turned into a theorem
    3.64 -\begin{ttbox}
    3.65 -val thm = ProofChecker.thm_of_proof Main.thy prf';
    3.66 -{\out val thm = "A & B --> B & A" : Thm.thm}
    3.67 -\end{ttbox}
    3.68 -
    3.69 -\index{proof terms|)}
    3.70 -\index{theorems|)}
    3.71 -
    3.72 -
    3.73  %%% Local Variables: 
    3.74  %%% mode: latex
    3.75  %%% TeX-master: "ref"