summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | clasohm |

Thu, 19 Jan 1995 16:05:21 +0100 | |

changeset 866 | 2d3d020eef11 |

parent 865 | b38c67991122 |

child 867 | e1a654c29b05 |

added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
and theory_of_thm

--- a/doc-src/Ref/defining.tex Wed Jan 18 11:36:04 1995 +0100 +++ b/doc-src/Ref/defining.tex Thu Jan 19 16:05:21 1995 +0100 @@ -688,26 +688,10 @@ {\out ...} \end{ttbox} -On the other hand it's also possible that none of the parse trees can be -typed correctly although the user did not make a mistake. - -%% FIXME remove? -%By default Isabelle -%assumes that the type of a syntax translation rule is {\tt logic} but does -%not look at the type unless parsing the rule produces more than one parse -%tree. In that case this message is output if the rule's type is different -%from {\tt logic}: -% -%\begin{ttbox} -%{\out Warning: Ambiguous input "..."} -%{\out produces the following parse trees:} -%{\out ...} -%{\out This occured in syntax translation rule: "..." -> "..."} -%{\out Type checking error: Term does not have expected type} -%{\out ...} -%\end{ttbox} -% -%To circumvent this the rule's type has to be stated. +Ambiguities occuring in syntax translation rules cannot be resolved by +type inference because it is not necessary for these rules to be type +correct. Therefore Isabelle always generates an error message and the +ambiguity should be eliminated by changing the grammar or the rule. \section{Example: some minimal logics} \label{sec:min_logics}

--- a/doc-src/Ref/goals.tex Wed Jan 18 11:36:04 1995 +0100 +++ b/doc-src/Ref/goals.tex Thu Jan 19 16:05:21 1995 +0100 @@ -117,34 +117,47 @@ the goal in intuitionistic logic and proving it using classical logic. \end{itemize} -\subsection{Extracting the proved theorem} +\subsection{Extracting and storing the proved theorem} +\label{ExtractingAndStoringTheProvedTheorem} \index{theorems!from subgoal module} \begin{ttbox} -result : unit -> thm -uresult : unit -> thm +result : unit -> thm +uresult : unit -> thm +bind_thm : string * thm -> unit +qed : string -> unit \end{ttbox} \begin{ttdescription} \item[\ttindexbold{result}()]\index{assumptions!of main goal} -returns the final theorem, after converting the free variables to -schematics. It discharges the assumptions supplied to the matching -{\tt goal} command. + returns the final theorem, after converting the free variables to + schematics. It discharges the assumptions supplied to the matching + {\tt goal} command. -It raises an exception unless the proof state passes certain checks. There -must be no assumptions other than those supplied to {\tt goal}. There -must be no subgoals. The theorem proved must be a (first-order) instance -of the original goal, as stated in the {\tt goal} command. This allows -{\bf answer extraction} --- instantiation of variables --- but no other -changes to the main goal. The theorem proved must have the same signature -as the initial proof state. + It raises an exception unless the proof state passes certain checks. There + must be no assumptions other than those supplied to {\tt goal}. There + must be no subgoals. The theorem proved must be a (first-order) instance + of the original goal, as stated in the {\tt goal} command. This allows + {\bf answer extraction} --- instantiation of variables --- but no other + changes to the main goal. The theorem proved must have the same signature + as the initial proof state. -These checks are needed because an Isabelle tactic can return any proof -state at all. + These checks are needed because an Isabelle tactic can return any proof + state at all. \item[\ttindexbold{uresult}()] is like {\tt result()} but omits the checks. It is needed when the initial goal contains function unknowns, when definitions are unfolded in the main goal (by calling \ttindex{rewrite_tac}),\index{definitions!unfolding} or when \ttindex{assume_ax} has been used. + +\item[\ttindexbold{bind_thm}($name$, $thm$)]\index{theorems!storing of} + stores {\tt standard($thm$)} (see \S\ref{MiscellaneousForwardRules}) + in Isabelle's theorem database and in the ML variable $name$. The + theorem can be retrieved from Isabelle's database by {\tt get_thm} + (see \S\ref{BasicOperationsOnTheories}). + +\item[\ttindexbold{qed} $name$] + combines {\tt result} and {\tt bind_thm} in that it first uses {\tt + result()} to get the theorem and then stores it like {\tt bind_thm}. \end{ttdescription} @@ -332,8 +345,10 @@ \section{Executing batch proofs} \index{batch execution} \begin{ttbox} -prove_goal : theory-> string->(thm list->tactic list)->thm -prove_goalw : theory->thm list->string->(thm list->tactic list)->thm +prove_goal : theory-> string->(thm list->tactic list)->thm +qed_goal : string->theory-> string->(thm list->tactic list)->unit +prove_goalw: theory->thm list->string->(thm list->tactic list)->thm +qed_goalw : string->theory->thm list->string->(thm list->tactic list)->unit prove_goalw_cterm: thm list->Sign.cterm->(thm list->tactic list)->thm \end{ttbox} These batch functions create an initial proof state, then apply a tactic to @@ -366,11 +381,19 @@ executes a proof of the {\it formula\/} in the given {\it theory}, using the given tactic function. +\item[\ttindexbold{qed_goal} $name$ $theory$ $formula$ $tacsf$;] +acts like {\tt prove_goal} but also stores the resulting theorem in +Isabelle's theorem database and in the ML variable $name$ (see +\S\ref{ExtractingAndStoringTheProvedTheorem}). + \item[\ttindexbold{prove_goalw} {\it theory} {\it defs} {\it formula} {\it tacsf};]\index{meta-rewriting} is like {\tt prove_goal} but also applies the list of {\it defs\/} as meta-rewrite rules to the first subgoal and the premises. +\item[\ttindexbold{qed_goalw} $name$ $theory$ $defs$ $formula$ $tacsf$;] +is analogous to {\tt qed_goal}. + \item[\ttindexbold{prove_goalw_cterm} {\it theory} {\it defs} {\it ct} {\it tacsf};] is a version of {\tt prove_goalw} for programming applications. The main

--- a/doc-src/Ref/theories.tex Wed Jan 18 11:36:04 1995 +0100 +++ b/doc-src/Ref/theories.tex Thu Jan 19 16:05:21 1995 +0100 @@ -308,7 +308,7 @@ -\section{Basic operations on theories} +\section{Basic operations on theories}\label{BasicOperationsOnTheories} \subsection{Extracting an axiom or theorem from a theory} \index{theories!axioms of}\index{axioms!extracting} \index{theories!theorems of}\index{theorems!extracting} @@ -319,12 +319,14 @@ \end{ttbox} \begin{ttdescription} \item[\ttindexbold{get_axiom} $thy$ $name$] -returns an axiom with the given $name$ from $thy$, raising exception -\xdx{THEORY} if none exists. Merging theories can cause several axioms -to have the same name; {\tt get_axiom} returns an arbitrary one. + returns an axiom with the given $name$ from $thy$, raising exception + \xdx{THEORY} if none exists. Merging theories can cause several axioms + to have the same name; {\tt get_axiom} returns an arbitrary one. \item[\ttindexbold{get_thm} $thy$ $name$] - is analogous to {\tt get_axiom}, but looks for a stored theorem. + is analogous to {\tt get_axiom}, but looks for a stored theorem. Like + {\tt get_axiom} it searches all parents of a theory if the theorem + is not associated with $thy$. \item[\ttindexbold{assume_ax} $thy$ $formula$] reads the {\it formula} using the syntax of $thy$, following the same @@ -427,7 +429,7 @@ returns the additional axioms of the most recent extend node of~$thy$. \item[\ttindexbold{thms_of} $thy$] -similar to {\tt axioms_of}, but returns the stored theorems. +returns all theorems that are associated with $thy$. \item[\ttindexbold{parents_of} $thy$] returns the direct ancestors of~$thy$.

--- a/doc-src/Ref/thm.tex Wed Jan 18 11:36:04 1995 +0100 +++ b/doc-src/Ref/thm.tex Thu Jan 19 16:05:21 1995 +0100 @@ -166,7 +166,7 @@ \end{ttdescription} -\subsection{Miscellaneous forward rules} +\subsection{Miscellaneous forward rules}\label{MiscellaneousForwardRules} \index{theorems!standardizing} \begin{ttbox} standard : thm -> thm @@ -209,6 +209,7 @@ nprems_of : thm -> int tpairs_of : thm -> (term*term)list stamps_of_thy : thm -> string ref list +theory_of_thm : thm -> theory dest_state : thm*int -> (term*term)list*term list*term*term rep_thm : thm -> \{prop:term, hyps:term list, maxidx:int, sign:Sign.sg\} @@ -230,6 +231,9 @@ \item[\ttindexbold{stamps_of_thm} $thm$] returns the \rmindex{stamps} of the signature associated with~$thm$. +\item[\ttindexbold{theory_of_thm} $thm$] +returns the theory associated with $thm$. + \item[\ttindexbold{dest_state} $(thm,i)$] decomposes $thm$ as a tuple containing a list of flex-flex constraints, a list of the subgoals~1 to~$i-1$, subgoal~$i$, and the rest of the theorem