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

author | nipkow |

Tue, 03 Sep 2002 13:41:29 +0200 | |

changeset 13555 | fc529625b494 |

parent 13554 | 4679359bb218 |

child 13556 | d17f6474eed0 |

*** empty log message ***

--- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy Mon Sep 02 12:25:19 2002 +0200 +++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy Tue Sep 03 13:41:29 2002 +0200 @@ -220,13 +220,33 @@ application of introduction and elimination rules but applies to explicit application of rules as well. Thus you could replace the final ``..'' above with \isakeyword{by}@{text"(rule conjI)"}. - -Note that Isar's predefined introduction and elimination rules include all the -usual natural deduction rules. We conclude this -section with an extended example --- which rules are used implicitly where? -Rule @{thm[source]ccontr} is @{thm ccontr[no_vars]}. *} +subsection{*More constructs*} + +text{* In the previous proof of @{prop"A \<and> B \<longrightarrow> B \<and> A"} we needed to feed +more than one fact into a proof step, a frequent situation. Then the +UNIX-pipe model appears to break down and we need to name the different +facts to refer to them. But this can be avoided: +*} +lemma "A \<and> B \<longrightarrow> B \<and> A" +proof + assume ab: "A \<and> B" + from ab have B .. + moreover + from ab have A .. + ultimately show "B \<and> A" .. +qed +text{*\noindent You can combine any number of facts @{term A1} \dots\ @{term +An} into a sequence by separating their proofs with +\isakeyword{moreover}. After the final fact, \isakeyword{ultimately} stands +for \isakeyword{from}~@{term A1}~\dots~@{term An}. This avoids having to +introduce names for all of the sequence elements. *} + +text{* Although we have only seen a few introduction and elemination rules so +far, Isar's predefined rules include all the usual natural deduction +rules. We conclude our exposition of propositional logic with an extended +example --- which rules are used implicitly where? *} lemma "\<not> (A \<and> B) \<longrightarrow> \<not> A \<or> \<not> B" proof assume n: "\<not> (A \<and> B)" @@ -249,7 +269,10 @@ with nn show False .. qed qed -text{*\noindent Apart from demonstrating the strangeness of classical +text{*\noindent +Rule @{thm[source]ccontr} (``classical contradiction'') is +@{thm ccontr[no_vars]}. +Apart from demonstrating the strangeness of classical arguments by contradiction, this example also introduces two new abbreviations: \begin{center}