more on concrete syntax of proof terms;
authorwenzelm
Mon Jun 17 21:23:49 2013 +0200 (2013-06-17)
changeset 524124cfa094da3cb
parent 52411 f192c4ea5b17
child 52413 a59ba6de9687
more on concrete syntax of proof terms;
src/Doc/IsarImplementation/Logic.thy
src/Doc/IsarImplementation/document/root.tex
src/Doc/ROOT
src/Doc/Ref/document/root.tex
src/Doc/Ref/document/thm.tex
src/HOL/Tools/reflection.ML
     1.1 --- a/src/Doc/IsarImplementation/Logic.thy	Mon Jun 17 20:15:34 2013 +0200
     1.2 +++ b/src/Doc/IsarImplementation/Logic.thy	Mon Jun 17 21:23:49 2013 +0200
     1.3 @@ -1291,6 +1291,46 @@
     1.4    and can turn it into a theorem by replaying its primitive inferences
     1.5    within the kernel.  *}
     1.6  
     1.7 +
     1.8 +subsection {* Concrete syntax of proof terms *}
     1.9 +
    1.10 +text {* The concrete syntax of proof terms is a slight extension of
    1.11 +  the regular inner syntax of Isabelle/Pure \cite{isabelle-isar-ref}.
    1.12 +  Its main syntactic category @{syntax (inner) proof} is defined as
    1.13 +  follows:
    1.14 +
    1.15 +  \begin{center}
    1.16 +  \begin{supertabular}{rclr}
    1.17 +
    1.18 +  @{syntax_def (inner) proof} & = & @{verbatim Lam} @{text params} @{verbatim "."} @{text proof} \\
    1.19 +    & @{text "|"} & @{text "\<Lambda>"} @{text "params"} @{verbatim "."} @{text proof} \\
    1.20 +    & @{text "|"} & @{text proof} @{verbatim "%"} @{text any} \\
    1.21 +    & @{text "|"} & @{text proof} @{text "\<cdot>"} @{text any} \\
    1.22 +    & @{text "|"} & @{text proof} @{verbatim "%%"} @{text proof} \\
    1.23 +    & @{text "|"} & @{text proof} @{text "\<bullet>"} @{text proof} \\
    1.24 +    & @{text "|"} & @{text "id  |  longid"} \\
    1.25 +  \\
    1.26 +
    1.27 +  @{text param} & = & @{text idt} \\
    1.28 +    & @{text "|"} & @{text idt} @{verbatim ":"} @{text prop} \\
    1.29 +    & @{text "|"} & @{verbatim "("} @{text param} @{verbatim ")"} \\
    1.30 +  \\
    1.31 +
    1.32 +  @{text params} & = & @{text param} \\
    1.33 +    & @{text "|"} & @{text param} @{text params} \\
    1.34 +
    1.35 +  \end{supertabular}
    1.36 +  \end{center}
    1.37 +
    1.38 +  Implicit term arguments in partial proofs are indicated by ``@{text
    1.39 +  "_"}''.  Type arguments for theorems and axioms may be specified
    1.40 +  using @{text "p \<cdot> TYPE(type)"} (they must appear before any other
    1.41 +  term argument of a theorem or axiom, but may be omitted altogether).
    1.42 +
    1.43 +  \medskip There are separate read and print operations for proof
    1.44 +  terms, in order to avoid conflicts with the regular term language.
    1.45 +*}
    1.46 +
    1.47  text %mlref {*
    1.48    \begin{mldecls}
    1.49    @{index_ML_type proof} \\
    1.50 @@ -1300,8 +1340,9 @@
    1.51    "theory -> term -> proof -> proof"} \\
    1.52    @{index_ML Reconstruct.expand_proof: "theory ->
    1.53    (string * term option) list -> proof -> proof"} \\
    1.54 -  @{index_ML Proof_Checker.thm_of_proof:
    1.55 -  "theory -> proof -> thm"} \\
    1.56 +  @{index_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\
    1.57 +  @{index_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\
    1.58 +  @{index_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\
    1.59    \end{mldecls}
    1.60  
    1.61    \begin{description}
    1.62 @@ -1354,6 +1395,14 @@
    1.63    given (full) proof into a theorem, by replaying it using only
    1.64    primitive rules of the inference kernel.
    1.65  
    1.66 +  \item @{ML Proof_Syntax.read_proof}~@{text "thy b\<^sub>1 b\<^sub>2 s"} reads in a
    1.67 +  proof term. The Boolean flags indicate the use of sort and type
    1.68 +  information.  Usually, typing information is left implicit and is
    1.69 +  inferred during proof reconstruction.  %FIXME eliminate flags!?
    1.70 +
    1.71 +  \item @{ML Proof_Syntax.pretty_proof}~@{text "ctxt prf"}
    1.72 +  pretty-prints the given proof term.
    1.73 +
    1.74    \end{description}
    1.75  *}
    1.76  
    1.77 @@ -1434,12 +1483,11 @@
    1.78           pretty_item "full proof:"
    1.79            (Proof_Syntax.pretty_proof ctxt full_prf)]
    1.80          |> Pretty.chunks |> Pretty.writeln;
    1.81 -
    1.82 +    in
    1.83        (*rechecked theorem*)
    1.84 -      val thm' =
    1.85 -        Proof_Checker.thm_of_proof thy full_prf
    1.86 -        |> singleton (Proof_Context.export ctxt ctxt0);
    1.87 -    in thm' end;
    1.88 +      Proof_Checker.thm_of_proof thy full_prf
    1.89 +      |> singleton (Proof_Context.export ctxt ctxt0)
    1.90 +    end;
    1.91  *}
    1.92  
    1.93  text {* As anticipated, the rechecked theorem establishes the same
     2.1 --- a/src/Doc/IsarImplementation/document/root.tex	Mon Jun 17 20:15:34 2013 +0200
     2.2 +++ b/src/Doc/IsarImplementation/document/root.tex	Mon Jun 17 21:23:49 2013 +0200
     2.3 @@ -7,6 +7,7 @@
     2.4  \usepackage{isabellesym}
     2.5  \usepackage{railsetup}
     2.6  \usepackage{ttbox}
     2.7 +\usepackage{supertabular}
     2.8  \usepackage{style}
     2.9  \usepackage{pdfsetup}
    2.10  
    2.11 @@ -19,6 +20,7 @@
    2.12    \\[4ex] The Isabelle/Isar Implementation}
    2.13  \author{\emph{Makarius Wenzel}  \\[3ex]
    2.14    With Contributions by
    2.15 +  Stefan Berghofer, \\
    2.16    Florian Haftmann
    2.17    and Larry Paulson
    2.18  }
     3.1 --- a/src/Doc/ROOT	Mon Jun 17 20:15:34 2013 +0200
     3.2 +++ b/src/Doc/ROOT	Mon Jun 17 21:23:49 2013 +0200
     3.3 @@ -258,7 +258,6 @@
     3.4      "document/build"
     3.5      "document/root.tex"
     3.6      "document/syntax.tex"
     3.7 -    "document/thm.tex"
     3.8  
     3.9  session Sledgehammer (doc) in "Sledgehammer" = Pure +
    3.10    options [document_variants = "sledgehammer"]
     4.1 --- a/src/Doc/Ref/document/root.tex	Mon Jun 17 20:15:34 2013 +0200
     4.2 +++ b/src/Doc/Ref/document/root.tex	Mon Jun 17 21:23:49 2013 +0200
     4.3 @@ -41,7 +41,6 @@
     4.4  
     4.5  \pagenumbering{roman} \tableofcontents \clearfirst
     4.6  
     4.7 -\input{thm}
     4.8  \input{syntax}
     4.9  
    4.10  %%seealso's must be last so that they appear last in the index entries
     5.1 --- a/src/Doc/Ref/document/thm.tex	Mon Jun 17 20:15:34 2013 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,58 +0,0 @@
     5.4 -
     5.5 -\chapter{Theorems and Forward Proof}
     5.6 -
     5.7 -\section{Proof terms}\label{sec:proofObjects}
     5.8 -
     5.9 -
    5.10 -\subsection{Parsing and printing proof terms}
    5.11 -\index{proof terms!parsing}
    5.12 -\index{proof terms!printing}
    5.13 -
    5.14 -Isabelle offers several functions for parsing and printing
    5.15 -proof terms. The concrete syntax for proof terms is described
    5.16 -in Fig.\ts\ref{fig:proof_gram}.
    5.17 -Implicit term arguments in partial proofs are indicated
    5.18 -by ``{\tt _}''.
    5.19 -Type arguments for theorems and axioms may be specified using
    5.20 -\verb!%! or ``$\cdot$'' with an argument of the form {\tt TYPE($type$)}
    5.21 -(see \S\ref{sec:basic_syntax}).
    5.22 -They must appear before any other term argument of a theorem
    5.23 -or axiom. In contrast to term arguments, type arguments may
    5.24 -be completely omitted.
    5.25 -\begin{ttbox}
    5.26 -ProofSyntax.read_proof : theory -> bool -> string -> Proofterm.proof
    5.27 -ProofSyntax.pretty_proof : Sign.sg -> Proofterm.proof -> Pretty.T
    5.28 -ProofSyntax.pretty_proof_of : bool -> thm -> Pretty.T
    5.29 -ProofSyntax.print_proof_of : bool -> thm -> unit
    5.30 -\end{ttbox}
    5.31 -\begin{figure}
    5.32 -\begin{center}
    5.33 -\begin{tabular}{rcl}
    5.34 -$proof$  & $=$ & {\tt Lam} $params${\tt .} $proof$ ~~$|$~~
    5.35 -                 $\Lambda params${\tt .} $proof$ \\
    5.36 -         & $|$ & $proof$ \verb!%! $any$ ~~$|$~~
    5.37 -                 $proof$ $\cdot$ $any$ \\
    5.38 -         & $|$ & $proof$ \verb!%%! $proof$ ~~$|$~~
    5.39 -                 $proof$ {\boldmath$\cdot$} $proof$ \\
    5.40 -         & $|$ & $id$ ~~$|$~~ $longid$ \\\\
    5.41 -$param$  & $=$ & $idt$ ~~$|$~~ $idt$ {\tt :} $prop$ ~~$|$~~
    5.42 -                 {\tt (} $param$ {\tt )} \\\\
    5.43 -$params$ & $=$ & $param$ ~~$|$~~ $param$ $params$
    5.44 -\end{tabular}
    5.45 -\end{center}
    5.46 -\caption{Proof term syntax}\label{fig:proof_gram}
    5.47 -\end{figure}
    5.48 -The function {\tt read_proof} reads in a proof term with
    5.49 -respect to a given theory. The boolean flag indicates whether
    5.50 -the proof term to be parsed contains explicit typing information
    5.51 -to be taken into account.
    5.52 -Usually, typing information is left implicit and
    5.53 -is inferred during proof reconstruction. The pretty printing
    5.54 -functions operating on theorems take a boolean flag as an
    5.55 -argument which indicates whether the proof term should
    5.56 -be reconstructed before printing.
    5.57 -
    5.58 -%%% Local Variables: 
    5.59 -%%% mode: latex
    5.60 -%%% TeX-master: "ref"
    5.61 -%%% End: