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

author | nipkow |

Fri, 23 Aug 2002 17:10:47 +0200 | |

changeset 13519 | 36ee816b5ee3 |

parent 13518 | a0749ce05100 |

child 13520 | a3d5d8b03d63 |

*** empty log message ***

doc-src/TutorialI/IsarOverview/Isar/Logic.thy | file | annotate | diff | comparison | revisions | |

doc-src/TutorialI/IsarOverview/Isar/document/root.tex | file | annotate | diff | comparison | revisions |

--- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy Fri Aug 23 11:08:01 2002 +0200 +++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy Fri Aug 23 17:10:47 2002 +0200 @@ -133,15 +133,18 @@ This is too much proof text. Elimination rules should be selected automatically based on their major premise, the formula or rather connective to be eliminated. In Isar they are triggered by propositions being fed -\emph{into} a proof block. Syntax: +\emph{into} a proof. Syntax: \begin{center} -\isakeyword{from} \emph{fact} \isakeyword{show} \emph{proposition} +\isakeyword{from} \emph{fact} \isakeyword{show} \emph{proposition} \emph{proof} \end{center} where \emph{fact} stands for the name of a previously proved proposition, e.g.\ an assumption, an intermediate result or some global -theorem. The fact may also be modified with @{text of}, @{text OF} etc. -This command applies an elimination rule (from a predefined list) -whose first premise is solved by the fact. Thus: *} +theorem, which may also be modified with @{text of}, @{text OF} etc. +The \emph{fact} is ``piped'' into the \emph{proof}, which can deal with it +how it choses. If the \emph{proof} starts with a plain \isakeyword{proof}, +an elimination rule (from a predefined list) is applied +whose first premise is solved by the \emph{fact}. Thus the proof above +is equivalent to the following one: *} lemma "A \<and> B \<longrightarrow> B \<and> A" proof @@ -210,7 +213,7 @@ again using the facts to prove the premises. \end{itemize} In this case, the proof succeeds with @{thm[source]conjI}. Note that the proof -would fail if we had written \isakeyword{from}~@{text"a b"} +would fail had we written \isakeyword{from}~@{text"a b"} instead of \isakeyword{from}~@{text"b a"}. This treatment of facts fed into a proof is not restricted to implicit @@ -477,8 +480,9 @@ text{*\noindent Of course this only works in the context of HOL's carefully constructed introduction and elimination rules for set theory. -Finally, whole scripts may appear in the leaves of the proof tree, although -this is best avoided. Here is a contrived example: *} +Finally, whole ``scripts'' (unstructured proofs in the style of +\cite{LNCS2283}) may appear in the leaves of the proof tree, although this is +best avoided. Here is a contrived example: *} lemma "A \<longrightarrow> (A \<longrightarrow> B) \<longrightarrow> B" proof

--- a/doc-src/TutorialI/IsarOverview/Isar/document/root.tex Fri Aug 23 11:08:01 2002 +0200 +++ b/doc-src/TutorialI/IsarOverview/Isar/document/root.tex Fri Aug 23 17:10:47 2002 +0200 @@ -37,7 +37,8 @@ {\small \paragraph{Acknowledgment} -I am deeply indebted to Markus Wenzel for conceiving Isar. Stefan Berghofer, +I am deeply indebted to Markus Wenzel for conceiving Isar. Clemens Ballarin, +Stefan Berghofer, Gerwin Klein, Norbert Schirmer and Markus Wenzel commented on this document. }