# HG changeset patch # User wenzelm # Date 1371497029 -7200 # Node ID 4cfa094da3cb827cf636e0ef4f6e755a69c3e772 # Parent f192c4ea5b17bec17c4dedc6918e695122dda787 more on concrete syntax of proof terms; diff -r f192c4ea5b17 -r 4cfa094da3cb src/Doc/IsarImplementation/Logic.thy --- a/src/Doc/IsarImplementation/Logic.thy Mon Jun 17 20:15:34 2013 +0200 +++ b/src/Doc/IsarImplementation/Logic.thy Mon Jun 17 21:23:49 2013 +0200 @@ -1291,6 +1291,46 @@ and can turn it into a theorem by replaying its primitive inferences within the kernel. *} + +subsection {* Concrete syntax of proof terms *} + +text {* The concrete syntax of proof terms is a slight extension of + the regular inner syntax of Isabelle/Pure \cite{isabelle-isar-ref}. + Its main syntactic category @{syntax (inner) proof} is defined as + follows: + + \begin{center} + \begin{supertabular}{rclr} + + @{syntax_def (inner) proof} & = & @{verbatim Lam} @{text params} @{verbatim "."} @{text proof} \\ + & @{text "|"} & @{text "\"} @{text "params"} @{verbatim "."} @{text proof} \\ + & @{text "|"} & @{text proof} @{verbatim "%"} @{text any} \\ + & @{text "|"} & @{text proof} @{text "\"} @{text any} \\ + & @{text "|"} & @{text proof} @{verbatim "%%"} @{text proof} \\ + & @{text "|"} & @{text proof} @{text "\"} @{text proof} \\ + & @{text "|"} & @{text "id | longid"} \\ + \\ + + @{text param} & = & @{text idt} \\ + & @{text "|"} & @{text idt} @{verbatim ":"} @{text prop} \\ + & @{text "|"} & @{verbatim "("} @{text param} @{verbatim ")"} \\ + \\ + + @{text params} & = & @{text param} \\ + & @{text "|"} & @{text param} @{text params} \\ + + \end{supertabular} + \end{center} + + Implicit term arguments in partial proofs are indicated by ``@{text + "_"}''. Type arguments for theorems and axioms may be specified + using @{text "p \ TYPE(type)"} (they must appear before any other + term argument of a theorem or axiom, but may be omitted altogether). + + \medskip There are separate read and print operations for proof + terms, in order to avoid conflicts with the regular term language. +*} + text %mlref {* \begin{mldecls} @{index_ML_type proof} \\ @@ -1300,8 +1340,9 @@ "theory -> term -> proof -> proof"} \\ @{index_ML Reconstruct.expand_proof: "theory -> (string * term option) list -> proof -> proof"} \\ - @{index_ML Proof_Checker.thm_of_proof: - "theory -> proof -> thm"} \\ + @{index_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\ + @{index_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\ + @{index_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\ \end{mldecls} \begin{description} @@ -1354,6 +1395,14 @@ given (full) proof into a theorem, by replaying it using only primitive rules of the inference kernel. + \item @{ML Proof_Syntax.read_proof}~@{text "thy b\<^sub>1 b\<^sub>2 s"} reads in a + proof term. The Boolean flags indicate the use of sort and type + information. Usually, typing information is left implicit and is + inferred during proof reconstruction. %FIXME eliminate flags!? + + \item @{ML Proof_Syntax.pretty_proof}~@{text "ctxt prf"} + pretty-prints the given proof term. + \end{description} *} @@ -1434,12 +1483,11 @@ pretty_item "full proof:" (Proof_Syntax.pretty_proof ctxt full_prf)] |> Pretty.chunks |> Pretty.writeln; - + in (*rechecked theorem*) - val thm' = - Proof_Checker.thm_of_proof thy full_prf - |> singleton (Proof_Context.export ctxt ctxt0); - in thm' end; + Proof_Checker.thm_of_proof thy full_prf + |> singleton (Proof_Context.export ctxt ctxt0) + end; *} text {* As anticipated, the rechecked theorem establishes the same diff -r f192c4ea5b17 -r 4cfa094da3cb src/Doc/IsarImplementation/document/root.tex --- a/src/Doc/IsarImplementation/document/root.tex Mon Jun 17 20:15:34 2013 +0200 +++ b/src/Doc/IsarImplementation/document/root.tex Mon Jun 17 21:23:49 2013 +0200 @@ -7,6 +7,7 @@ \usepackage{isabellesym} \usepackage{railsetup} \usepackage{ttbox} +\usepackage{supertabular} \usepackage{style} \usepackage{pdfsetup} @@ -19,6 +20,7 @@ \\[4ex] The Isabelle/Isar Implementation} \author{\emph{Makarius Wenzel} \\[3ex] With Contributions by + Stefan Berghofer, \\ Florian Haftmann and Larry Paulson } diff -r f192c4ea5b17 -r 4cfa094da3cb src/Doc/ROOT --- a/src/Doc/ROOT Mon Jun 17 20:15:34 2013 +0200 +++ b/src/Doc/ROOT Mon Jun 17 21:23:49 2013 +0200 @@ -258,7 +258,6 @@ "document/build" "document/root.tex" "document/syntax.tex" - "document/thm.tex" session Sledgehammer (doc) in "Sledgehammer" = Pure + options [document_variants = "sledgehammer"] diff -r f192c4ea5b17 -r 4cfa094da3cb src/Doc/Ref/document/root.tex --- a/src/Doc/Ref/document/root.tex Mon Jun 17 20:15:34 2013 +0200 +++ b/src/Doc/Ref/document/root.tex Mon Jun 17 21:23:49 2013 +0200 @@ -41,7 +41,6 @@ \pagenumbering{roman} \tableofcontents \clearfirst -\input{thm} \input{syntax} %%seealso's must be last so that they appear last in the index entries diff -r f192c4ea5b17 -r 4cfa094da3cb src/Doc/Ref/document/thm.tex --- a/src/Doc/Ref/document/thm.tex Mon Jun 17 20:15:34 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,58 +0,0 @@ - -\chapter{Theorems and Forward Proof} - -\section{Proof terms}\label{sec:proofObjects} - - -\subsection{Parsing and printing proof terms} -\index{proof terms!parsing} -\index{proof terms!printing} - -Isabelle offers several functions for parsing and printing -proof terms. The concrete syntax for proof terms is described -in Fig.\ts\ref{fig:proof_gram}. -Implicit term arguments in partial proofs are indicated -by ``{\tt _}''. -Type arguments for theorems and axioms may be specified using -\verb!%! or ``$\cdot$'' with an argument of the form {\tt TYPE($type$)} -(see \S\ref{sec:basic_syntax}). -They must appear before any other term argument of a theorem -or axiom. In contrast to term arguments, type arguments may -be completely omitted. -\begin{ttbox} -ProofSyntax.read_proof : theory -> bool -> string -> Proofterm.proof -ProofSyntax.pretty_proof : Sign.sg -> Proofterm.proof -> Pretty.T -ProofSyntax.pretty_proof_of : bool -> thm -> Pretty.T -ProofSyntax.print_proof_of : bool -> thm -> unit -\end{ttbox} -\begin{figure} -\begin{center} -\begin{tabular}{rcl} -$proof$ & $=$ & {\tt Lam} $params${\tt .} $proof$ ~~$|$~~ - $\Lambda params${\tt .} $proof$ \\ - & $|$ & $proof$ \verb!%! $any$ ~~$|$~~ - $proof$ $\cdot$ $any$ \\ - & $|$ & $proof$ \verb!%%! $proof$ ~~$|$~~ - $proof$ {\boldmath$\cdot$} $proof$ \\ - & $|$ & $id$ ~~$|$~~ $longid$ \\\\ -$param$ & $=$ & $idt$ ~~$|$~~ $idt$ {\tt :} $prop$ ~~$|$~~ - {\tt (} $param$ {\tt )} \\\\ -$params$ & $=$ & $param$ ~~$|$~~ $param$ $params$ -\end{tabular} -\end{center} -\caption{Proof term syntax}\label{fig:proof_gram} -\end{figure} -The function {\tt read_proof} reads in a proof term with -respect to a given theory. The boolean flag indicates whether -the proof term to be parsed contains explicit typing information -to be taken into account. -Usually, typing information is left implicit and -is inferred during proof reconstruction. The pretty printing -functions operating on theorems take a boolean flag as an -argument which indicates whether the proof term should -be reconstructed before printing. - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "ref" -%%% End: