src/HOL/Isar_examples/BasicLogic.thy
changeset 7982 d534b897ce39
parent 7874 180364256231
child 8902 a705822f4e2a
     1.1 --- a/src/HOL/Isar_examples/BasicLogic.thy	Sat Oct 30 20:13:16 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/BasicLogic.thy	Sat Oct 30 20:20:48 1999 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  Basic propositional and quantifier reasoning.
     1.5  *)
     1.6  
     1.7 -header {* Basic reasoning *};
     1.8 +header {* Basic logical reasoning *};
     1.9  
    1.10  theory BasicLogic = Main:;
    1.11  
    1.12 @@ -70,9 +70,9 @@
    1.13  text {*
    1.14   In fact, concluding any (sub-)proof already involves solving any
    1.15   remaining goals by assumption\footnote{This is not a completely
    1.16 - trivial operation, as proof by assumption involves full higher-order
    1.17 - unification.}.  Thus we may skip the rather vacuous body of the above
    1.18 - proof as well.
    1.19 + trivial operation, as proof by assumption may involve full
    1.20 + higher-order unification.}.  Thus we may skip the rather vacuous body
    1.21 + of the above proof as well.
    1.22  *};
    1.23  
    1.24  lemma "A --> A";
    1.25 @@ -99,7 +99,7 @@
    1.26  text {*
    1.27   Thus we have arrived at an adequate representation of the proof of a
    1.28   tautology that holds by a single standard rule.\footnote{Apparently,
    1.29 - the rule is implication introduction.}
    1.30 + the rule here is implication introduction.}
    1.31  *};
    1.32  
    1.33  text {*
    1.34 @@ -129,7 +129,7 @@
    1.35   Just like $\idt{rule}$, the $\idt{intro}$ and $\idt{elim}$ proof
    1.36   methods pick standard structural rules, in case no explicit arguments
    1.37   are given.  While implicit rules are usually just fine for single
    1.38 - rule application, this may go too far in iteration.  Thus in
    1.39 + rule application, this may go too far with iteration.  Thus in
    1.40   practice, $\idt{intro}$ and $\idt{elim}$ would be typically
    1.41   restricted to certain structures by giving a few rules only, e.g.\
    1.42   \isacommand{proof}~($\idt{intro}$~\name{impI}~\name{allI}) to strip
    1.43 @@ -168,11 +168,12 @@
    1.44  
    1.45  text {*
    1.46   Above, the $\idt{conjunct}_{1/2}$ projection rules had to be named
    1.47 - explicitly, since the goals did not provide any structural clue.
    1.48 - This may be avoided using \isacommand{from} to focus on $\idt{prems}$
    1.49 - (i.e.\ the $A \conj B$ assumption) as the current facts, enabling the
    1.50 - use of double-dot proofs.  Note that \isacommand{from} already
    1.51 - does forward-chaining, involving the \name{conjE} rule.
    1.52 + explicitly, since the goals $B$ and $A$ did not provide any
    1.53 + structural clue.  This may be avoided using \isacommand{from} to
    1.54 + focus on $\idt{prems}$ (i.e.\ the $A \conj B$ assumption) as the
    1.55 + current facts, enabling the use of double-dot proofs.  Note that
    1.56 + \isacommand{from} already does forward-chaining, involving the
    1.57 + \name{conjE} rule here.
    1.58  *};
    1.59  
    1.60  lemma "A & B --> B & A";
    1.61 @@ -222,7 +223,7 @@
    1.62  text {*
    1.63   We can still push forward reasoning a bit further, even at the risk
    1.64   of getting ridiculous.  Note that we force the initial proof step to
    1.65 - do nothing, by referring to the ``-'' proof method.
    1.66 + do nothing here, by referring to the ``-'' proof method.
    1.67  *};
    1.68  
    1.69  lemma "A & B --> B & A";
    1.70 @@ -245,7 +246,7 @@
    1.71  
    1.72   The general lesson learned here is that good proof style would
    1.73   achieve just the \emph{right} balance of top-down backward
    1.74 - decomposition, and bottom-up forward composition.  In practice, there
    1.75 + decomposition, and bottom-up forward composition.  In general, there
    1.76   is no single best way to arrange some pieces of formal reasoning, of
    1.77   course.  Depending on the actual applications, the intended audience
    1.78   etc., rules (and methods) on the one hand vs.\ facts on the other
    1.79 @@ -278,7 +279,7 @@
    1.80  
    1.81  text {*
    1.82   We rephrase some of the basic reasoning examples of
    1.83 - \cite{isabelle-intro} (using HOL rather than FOL).
    1.84 + \cite{isabelle-intro}, using HOL rather than FOL.
    1.85  *};
    1.86  
    1.87  subsubsection {* A propositional proof *};
    1.88 @@ -315,8 +316,8 @@
    1.89   In order to avoid too much explicit parentheses, the Isar system
    1.90   implicitly opens an additional block for any new goal, the
    1.91   \isacommand{next} statement then closes one block level, opening a
    1.92 - new one.  The resulting behavior is what one might expect from
    1.93 - separating cases, only that it is more flexible.  E.g. an induction
    1.94 + new one.  The resulting behavior is what one would expect from
    1.95 + separating cases, only that it is more flexible.  E.g.\ an induction
    1.96   base case (which does not introduce local assumptions) would
    1.97   \emph{not} require \isacommand{next} to separate the subsequent step
    1.98   case.
    1.99 @@ -381,8 +382,8 @@
   1.100  qed;
   1.101  
   1.102  text {*
   1.103 - While explicit rule instantiation may occasionally help to improve
   1.104 - the readability of certain aspects of reasoning, it is usually quite
   1.105 + While explicit rule instantiation may occasionally improve
   1.106 + readability of certain aspects of reasoning, it is usually quite
   1.107   redundant.  Above, the basic proof outline gives already enough
   1.108   structural clues for the system to infer both the rules and their
   1.109   instances (by higher-order unification).  Thus we may as well prune
   1.110 @@ -404,17 +405,18 @@
   1.111  subsubsection {* Deriving rules in Isabelle *};
   1.112  
   1.113  text {*
   1.114 - We derive the conjunction elimination rule from the projections.  The
   1.115 - proof is quite straight-forward, since Isabelle/Isar supports
   1.116 - non-atomic goals and assumptions fully transparently.
   1.117 + We derive the conjunction elimination rule from the corresponding
   1.118 + projections.  The proof is quite straight-forward, since
   1.119 + Isabelle/Isar supports non-atomic goals and assumptions fully
   1.120 + transparently.
   1.121  *};
   1.122  
   1.123  theorem conjE: "A & B ==> (A ==> B ==> C) ==> C";
   1.124  proof -;
   1.125    assume "A & B";
   1.126 -  assume ab_c: "A ==> B ==> C";
   1.127 +  assume r: "A ==> B ==> C";
   1.128    show C;
   1.129 -  proof (rule ab_c);
   1.130 +  proof (rule r);
   1.131      show A; by (rule conjunct1);
   1.132      show B; by (rule conjunct2);
   1.133    qed;
   1.134 @@ -425,7 +427,7 @@
   1.135   different way.  The tactic script as given in \cite{isabelle-intro}
   1.136   for the same example of \name{conjE} depends on the primitive
   1.137   \texttt{goal} command to decompose the rule into premises and
   1.138 - conclusion.  The proper result would then emerge by discharging of
   1.139 + conclusion.  The actual result would then emerge by discharging of
   1.140   the context at \texttt{qed} time.
   1.141  *};
   1.142