src/HOL/Isar_examples/BasicLogic.thy
changeset 10007 64bf7da1994a
parent 9659 b9cf6801f3da
child 10636 d1efa59ea259
     1.1 --- a/src/HOL/Isar_examples/BasicLogic.thy	Sun Sep 17 22:15:08 2000 +0200
     1.2 +++ b/src/HOL/Isar_examples/BasicLogic.thy	Sun Sep 17 22:19:02 2000 +0200
     1.3 @@ -5,52 +5,52 @@
     1.4  Basic propositional and quantifier reasoning.
     1.5  *)
     1.6  
     1.7 -header {* Basic logical reasoning *};
     1.8 +header {* Basic logical reasoning *}
     1.9  
    1.10 -theory BasicLogic = Main:;
    1.11 +theory BasicLogic = Main:
    1.12  
    1.13  
    1.14 -subsection {* Pure backward reasoning *};
    1.15 +subsection {* Pure backward reasoning *}
    1.16  
    1.17  text {*
    1.18   In order to get a first idea of how Isabelle/Isar proof documents may
    1.19   look like, we consider the propositions $I$, $K$, and $S$.  The
    1.20   following (rather explicit) proofs should require little extra
    1.21   explanations.
    1.22 -*};
    1.23 +*}
    1.24  
    1.25 -lemma I: "A --> A";
    1.26 -proof;
    1.27 -  assume A;
    1.28 -  show A; by assumption;
    1.29 -qed;
    1.30 +lemma I: "A --> A"
    1.31 +proof
    1.32 +  assume A
    1.33 +  show A by assumption
    1.34 +qed
    1.35  
    1.36 -lemma K: "A --> B --> A";
    1.37 -proof;
    1.38 -  assume A;
    1.39 -  show "B --> A";
    1.40 -  proof;
    1.41 -    show A; by assumption;
    1.42 -  qed;
    1.43 -qed;
    1.44 +lemma K: "A --> B --> A"
    1.45 +proof
    1.46 +  assume A
    1.47 +  show "B --> A"
    1.48 +  proof
    1.49 +    show A by assumption
    1.50 +  qed
    1.51 +qed
    1.52  
    1.53 -lemma S: "(A --> B --> C) --> (A --> B) --> A --> C";
    1.54 -proof;
    1.55 -  assume "A --> B --> C";
    1.56 -  show "(A --> B) --> A --> C";
    1.57 -  proof;
    1.58 -    assume "A --> B";
    1.59 -    show "A --> C";
    1.60 -    proof;
    1.61 -      assume A;
    1.62 -      show C;
    1.63 -      proof (rule mp);
    1.64 -	show "B --> C"; by (rule mp);
    1.65 -        show B; by (rule mp);
    1.66 -      qed;
    1.67 -    qed;
    1.68 -  qed;
    1.69 -qed;
    1.70 +lemma S: "(A --> B --> C) --> (A --> B) --> A --> C"
    1.71 +proof
    1.72 +  assume "A --> B --> C"
    1.73 +  show "(A --> B) --> A --> C"
    1.74 +  proof
    1.75 +    assume "A --> B"
    1.76 +    show "A --> C"
    1.77 +    proof
    1.78 +      assume A
    1.79 +      show C
    1.80 +      proof (rule mp)
    1.81 +	show "B --> C" by (rule mp)
    1.82 +        show B by (rule mp)
    1.83 +      qed
    1.84 +    qed
    1.85 +  qed
    1.86 +qed
    1.87  
    1.88  text {*
    1.89   Isar provides several ways to fine-tune the reasoning, avoiding
    1.90 @@ -59,13 +59,13 @@
    1.91   way, even without referring to any automated proof tools yet.
    1.92  
    1.93   First of all, proof by assumption may be abbreviated as a single dot.
    1.94 -*};
    1.95 +*}
    1.96  
    1.97 -lemma "A --> A";
    1.98 -proof;
    1.99 -  assume A;
   1.100 -  show A; .;
   1.101 -qed;
   1.102 +lemma "A --> A"
   1.103 +proof
   1.104 +  assume A
   1.105 +  show A .
   1.106 +qed
   1.107  
   1.108  text {*
   1.109   In fact, concluding any (sub-)proof already involves solving any
   1.110 @@ -73,11 +73,11 @@
   1.111   trivial operation, as proof by assumption may involve full
   1.112   higher-order unification.}.  Thus we may skip the rather vacuous body
   1.113   of the above proof as well.
   1.114 -*};
   1.115 +*}
   1.116  
   1.117 -lemma "A --> A";
   1.118 -proof;
   1.119 -qed;
   1.120 +lemma "A --> A"
   1.121 +proof
   1.122 +qed
   1.123  
   1.124  text {*
   1.125   Note that the \isacommand{proof} command refers to the $\idt{rule}$
   1.126 @@ -85,22 +85,22 @@
   1.127   single rule, as determined from the syntactic form of the statements
   1.128   involved.  The \isacommand{by} command abbreviates any proof with
   1.129   empty body, so the proof may be further pruned.
   1.130 -*};
   1.131 +*}
   1.132  
   1.133 -lemma "A --> A";
   1.134 -  by rule;
   1.135 +lemma "A --> A"
   1.136 +  by rule
   1.137  
   1.138  text {*
   1.139   Proof by a single rule may be abbreviated as double-dot.
   1.140 -*};
   1.141 +*}
   1.142  
   1.143 -lemma "A --> A"; ..;
   1.144 +lemma "A --> A" ..
   1.145  
   1.146  text {*
   1.147   Thus we have arrived at an adequate representation of the proof of a
   1.148   tautology that holds by a single standard rule.\footnote{Apparently,
   1.149   the rule here is implication introduction.}
   1.150 -*};
   1.151 +*}
   1.152  
   1.153  text {*
   1.154   Let us also reconsider $K$.  Its statement is composed of iterated
   1.155 @@ -110,20 +110,20 @@
   1.156   The $\idt{intro}$ proof method repeatedly decomposes a goal's
   1.157   conclusion.\footnote{The dual method is $\idt{elim}$, acting on a
   1.158   goal's premises.}
   1.159 -*};
   1.160 +*}
   1.161  
   1.162 -lemma "A --> B --> A";
   1.163 -proof intro;
   1.164 -  assume A;
   1.165 -  show A; .;
   1.166 -qed;
   1.167 +lemma "A --> B --> A"
   1.168 +proof intro
   1.169 +  assume A
   1.170 +  show A .
   1.171 +qed
   1.172  
   1.173  text {*
   1.174   Again, the body may be collapsed.
   1.175 -*};
   1.176 +*}
   1.177  
   1.178 -lemma "A --> B --> A";
   1.179 -  by intro;
   1.180 +lemma "A --> B --> A"
   1.181 +  by intro
   1.182  
   1.183  text {*
   1.184   Just like $\idt{rule}$, the $\idt{intro}$ and $\idt{elim}$ proof
   1.185 @@ -140,10 +140,10 @@
   1.186   terminal steps that solve a goal completely are usually performed by
   1.187   actual automated proof methods (such as
   1.188   \isacommand{by}~$\idt{blast}$).
   1.189 -*};
   1.190 +*}
   1.191  
   1.192  
   1.193 -subsection {* Variations of backward vs.\ forward reasoning *};
   1.194 +subsection {* Variations of backward vs.\ forward reasoning *}
   1.195  
   1.196  text {*
   1.197   Certainly, any proof may be performed in backward-style only.  On the
   1.198 @@ -154,17 +154,17 @@
   1.199   A$.
   1.200  
   1.201   The first version is purely backward.
   1.202 -*};
   1.203 +*}
   1.204  
   1.205 -lemma "A & B --> B & A";
   1.206 -proof;
   1.207 -  assume "A & B";
   1.208 -  show "B & A";
   1.209 -  proof;
   1.210 -    show B; by (rule conjunct2);
   1.211 -    show A; by (rule conjunct1);
   1.212 -  qed;
   1.213 -qed;
   1.214 +lemma "A & B --> B & A"
   1.215 +proof
   1.216 +  assume "A & B"
   1.217 +  show "B & A"
   1.218 +  proof
   1.219 +    show B by (rule conjunct2)
   1.220 +    show A by (rule conjunct1)
   1.221 +  qed
   1.222 +qed
   1.223  
   1.224  text {*
   1.225   Above, the $\idt{conjunct}_{1/2}$ projection rules had to be named
   1.226 @@ -174,17 +174,17 @@
   1.227   current facts, enabling the use of double-dot proofs.  Note that
   1.228   \isacommand{from} already does forward-chaining, involving the
   1.229   \name{conjE} rule here.
   1.230 -*};
   1.231 +*}
   1.232  
   1.233 -lemma "A & B --> B & A";
   1.234 -proof;
   1.235 -  assume "A & B";
   1.236 -  show "B & A";
   1.237 -  proof;
   1.238 -    from prems; show B; ..;
   1.239 -    from prems; show A; ..;
   1.240 -  qed;
   1.241 -qed;
   1.242 +lemma "A & B --> B & A"
   1.243 +proof
   1.244 +  assume "A & B"
   1.245 +  show "B & A"
   1.246 +  proof
   1.247 +    from prems show B ..
   1.248 +    from prems show A ..
   1.249 +  qed
   1.250 +qed
   1.251  
   1.252  text {*
   1.253   In the next version, we move the forward step one level upwards.
   1.254 @@ -194,48 +194,48 @@
   1.255   introduction.  The resulting proof structure directly corresponds to
   1.256   that of the $\name{conjE}$ rule, including the repeated goal
   1.257   proposition that is abbreviated as $\var{thesis}$ below.
   1.258 -*};
   1.259 +*}
   1.260  
   1.261 -lemma "A & B --> B & A";
   1.262 -proof;
   1.263 -  assume "A & B";
   1.264 -  then; show "B & A";
   1.265 -  proof                    -- {* rule \name{conjE} of $A \conj B$ *};
   1.266 -    assume A B;
   1.267 -    show ?thesis; ..       -- {* rule \name{conjI} of $B \conj A$ *};
   1.268 -  qed;
   1.269 -qed;
   1.270 +lemma "A & B --> B & A"
   1.271 +proof
   1.272 +  assume "A & B"
   1.273 +  then show "B & A"
   1.274 +  proof                    -- {* rule \name{conjE} of $A \conj B$ *}
   1.275 +    assume A B
   1.276 +    show ?thesis ..       -- {* rule \name{conjI} of $B \conj A$ *}
   1.277 +  qed
   1.278 +qed
   1.279  
   1.280  text {*
   1.281   In the subsequent version we flatten the structure of the main body
   1.282   by doing forward reasoning all the time.  Only the outermost
   1.283   decomposition step is left as backward.
   1.284 -*};
   1.285 +*}
   1.286  
   1.287 -lemma "A & B --> B & A";
   1.288 -proof;
   1.289 -  assume ab: "A & B";
   1.290 -  from ab; have a: A; ..;
   1.291 -  from ab; have b: B; ..;
   1.292 -  from b a; show "B & A"; ..;
   1.293 -qed;
   1.294 +lemma "A & B --> B & A"
   1.295 +proof
   1.296 +  assume ab: "A & B"
   1.297 +  from ab have a: A ..
   1.298 +  from ab have b: B ..
   1.299 +  from b a show "B & A" ..
   1.300 +qed
   1.301  
   1.302  text {*
   1.303   We can still push forward-reasoning a bit further, even at the risk
   1.304   of getting ridiculous.  Note that we force the initial proof step to
   1.305   do nothing here, by referring to the ``-'' proof method.
   1.306 -*};
   1.307 +*}
   1.308  
   1.309 -lemma "A & B --> B & A";
   1.310 -proof -;
   1.311 -  {;
   1.312 -    assume ab: "A & B";
   1.313 -    from ab; have a: A; ..;
   1.314 -    from ab; have b: B; ..;
   1.315 -    from b a; have "B & A"; ..;
   1.316 -  };
   1.317 -  thus ?thesis; ..         -- {* rule \name{impI} *};
   1.318 -qed;
   1.319 +lemma "A & B --> B & A"
   1.320 +proof -
   1.321 +  {
   1.322 +    assume ab: "A & B"
   1.323 +    from ab have a: A ..
   1.324 +    from ab have b: B ..
   1.325 +    from b a have "B & A" ..
   1.326 +  }
   1.327 +  thus ?thesis ..         -- {* rule \name{impI} *}
   1.328 +qed
   1.329  
   1.330  text {*
   1.331   \medskip With these examples we have shifted through a whole range
   1.332 @@ -252,7 +252,7 @@
   1.333   etc., rules (and methods) on the one hand vs.\ facts on the other
   1.334   hand have to be emphasized in an appropriate way.  This requires the
   1.335   proof writer to develop good taste, and some practice, of course.
   1.336 -*};
   1.337 +*}
   1.338  
   1.339  text {*
   1.340   For our example the most appropriate way of reasoning is probably the
   1.341 @@ -261,47 +261,47 @@
   1.342   abbreviates \isacommand{then}~\isacommand{show}.\footnote{In the same
   1.343   vein, \isacommand{hence} abbreviates
   1.344   \isacommand{then}~\isacommand{have}.}
   1.345 -*};
   1.346 +*}
   1.347  
   1.348 -lemma "A & B --> B & A";
   1.349 -proof;
   1.350 -  assume "A & B";
   1.351 -  thus "B & A";
   1.352 -  proof;
   1.353 -    assume A B;
   1.354 -    show ?thesis; ..;
   1.355 -  qed;
   1.356 -qed;
   1.357 +lemma "A & B --> B & A"
   1.358 +proof
   1.359 +  assume "A & B"
   1.360 +  thus "B & A"
   1.361 +  proof
   1.362 +    assume A B
   1.363 +    show ?thesis ..
   1.364 +  qed
   1.365 +qed
   1.366  
   1.367  
   1.368  
   1.369 -subsection {* A few examples from ``Introduction to Isabelle'' *};
   1.370 +subsection {* A few examples from ``Introduction to Isabelle'' *}
   1.371  
   1.372  text {*
   1.373   We rephrase some of the basic reasoning examples of
   1.374   \cite{isabelle-intro}, using HOL rather than FOL.
   1.375 -*};
   1.376 +*}
   1.377  
   1.378 -subsubsection {* A propositional proof *};
   1.379 +subsubsection {* A propositional proof *}
   1.380  
   1.381  text {*
   1.382   We consider the proposition $P \disj P \impl P$.  The proof below
   1.383   involves forward-chaining from $P \disj P$, followed by an explicit
   1.384   case-analysis on the two \emph{identical} cases.
   1.385 -*};
   1.386 +*}
   1.387  
   1.388 -lemma "P | P --> P";
   1.389 -proof;
   1.390 -  assume "P | P";
   1.391 -  thus P;
   1.392 +lemma "P | P --> P"
   1.393 +proof
   1.394 +  assume "P | P"
   1.395 +  thus P
   1.396    proof                    -- {*
   1.397      rule \name{disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
   1.398 -  *};
   1.399 -    assume P; show P; .;
   1.400 -  next;
   1.401 -    assume P; show P; .;
   1.402 -  qed;
   1.403 -qed;
   1.404 +  *}
   1.405 +    assume P show P .
   1.406 +  next
   1.407 +    assume P show P .
   1.408 +  qed
   1.409 +qed
   1.410  
   1.411  text {*
   1.412   Case splits are \emph{not} hardwired into the Isar language as a
   1.413 @@ -325,34 +325,34 @@
   1.414   \medskip In our example the situation is even simpler, since the two
   1.415   cases actually coincide.  Consequently the proof may be rephrased as
   1.416   follows.
   1.417 -*};
   1.418 +*}
   1.419  
   1.420 -lemma "P | P --> P";
   1.421 -proof;
   1.422 -  assume "P | P";
   1.423 -  thus P;
   1.424 -  proof;
   1.425 -    assume P;
   1.426 -    show P; .;
   1.427 -    show P; .;
   1.428 -  qed;
   1.429 -qed;
   1.430 +lemma "P | P --> P"
   1.431 +proof
   1.432 +  assume "P | P"
   1.433 +  thus P
   1.434 +  proof
   1.435 +    assume P
   1.436 +    show P .
   1.437 +    show P .
   1.438 +  qed
   1.439 +qed
   1.440  
   1.441  text {*
   1.442   Again, the rather vacuous body of the proof may be collapsed.  Thus
   1.443   the case analysis degenerates into two assumption steps, which are
   1.444   implicitly performed when concluding the single rule step of the
   1.445   double-dot proof as follows.
   1.446 -*};
   1.447 +*}
   1.448  
   1.449 -lemma "P | P --> P";
   1.450 -proof;
   1.451 -  assume "P | P";
   1.452 -  thus P; ..;
   1.453 -qed;
   1.454 +lemma "P | P --> P"
   1.455 +proof
   1.456 +  assume "P | P"
   1.457 +  thus P ..
   1.458 +qed
   1.459  
   1.460  
   1.461 -subsubsection {* A quantifier proof *};
   1.462 +subsubsection {* A quantifier proof *}
   1.463  
   1.464  text {*
   1.465   To illustrate quantifier reasoning, let us prove $(\ex x P \ap (f \ap
   1.466 @@ -366,20 +366,20 @@
   1.467   the \isacommand{fix} command augments the context by some new
   1.468   ``arbitrary, but fixed'' element; the \isacommand{is} annotation
   1.469   binds term abbreviations by higher-order pattern matching.
   1.470 -*};
   1.471 +*}
   1.472  
   1.473 -lemma "(EX x. P (f x)) --> (EX x. P x)";
   1.474 -proof;
   1.475 -  assume "EX x. P (f x)";
   1.476 -  thus "EX x. P x";
   1.477 +lemma "(EX x. P (f x)) --> (EX x. P x)"
   1.478 +proof
   1.479 +  assume "EX x. P (f x)"
   1.480 +  thus "EX x. P x"
   1.481    proof (rule exE)             -- {*
   1.482      rule \name{exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}
   1.483 -  *};
   1.484 -    fix a;
   1.485 -    assume "P (f a)" (is "P ?witness");
   1.486 -    show ?thesis; by (rule exI [of P ?witness]);
   1.487 -  qed;
   1.488 -qed;
   1.489 +  *}
   1.490 +    fix a
   1.491 +    assume "P (f a)" (is "P ?witness")
   1.492 +    show ?thesis by (rule exI [of P ?witness])
   1.493 +  qed
   1.494 +qed
   1.495  
   1.496  text {*
   1.497   While explicit rule instantiation may occasionally improve
   1.498 @@ -388,32 +388,32 @@
   1.499   structural clues for the system to infer both the rules and their
   1.500   instances (by higher-order unification).  Thus we may as well prune
   1.501   the text as follows.
   1.502 -*};
   1.503 +*}
   1.504  
   1.505 -lemma "(EX x. P (f x)) --> (EX x. P x)";
   1.506 -proof;
   1.507 -  assume "EX x. P (f x)";
   1.508 -  thus "EX x. P x";
   1.509 -  proof;
   1.510 -    fix a;
   1.511 -    assume "P (f a)";
   1.512 -    show ?thesis; ..;
   1.513 -  qed;
   1.514 -qed;
   1.515 +lemma "(EX x. P (f x)) --> (EX x. P x)"
   1.516 +proof
   1.517 +  assume "EX x. P (f x)"
   1.518 +  thus "EX x. P x"
   1.519 +  proof
   1.520 +    fix a
   1.521 +    assume "P (f a)"
   1.522 +    show ?thesis ..
   1.523 +  qed
   1.524 +qed
   1.525  
   1.526  text {*
   1.527   Explicit $\exists$-elimination as seen above can become quite
   1.528   cumbersome in practice.  The derived Isar language element
   1.529   ``\isakeyword{obtain}'' provides a more handsome way to do
   1.530   generalized existence reasoning.
   1.531 -*};
   1.532 +*}
   1.533  
   1.534 -lemma "(EX x. P (f x)) --> (EX x. P x)";
   1.535 -proof;
   1.536 -  assume "EX x. P (f x)";
   1.537 -  then; obtain a where "P (f a)"; by blast;
   1.538 -  thus "EX x. P x"; ..;
   1.539 -qed;
   1.540 +lemma "(EX x. P (f x)) --> (EX x. P x)"
   1.541 +proof
   1.542 +  assume "EX x. P (f x)"
   1.543 +  then obtain a where "P (f a)" by blast
   1.544 +  thus "EX x. P x" ..
   1.545 +qed
   1.546  
   1.547  text {*
   1.548   Technically, \isakeyword{obtain} is similar to \isakeyword{fix} and
   1.549 @@ -423,29 +423,29 @@
   1.550   reasoning involved here, any result exported from the context of an
   1.551   \isakeyword{obtain} statement may \emph{not} refer to the parameters
   1.552   introduced there.
   1.553 -*};
   1.554 +*}
   1.555  
   1.556  
   1.557  
   1.558 -subsubsection {* Deriving rules in Isabelle *};
   1.559 +subsubsection {* Deriving rules in Isabelle *}
   1.560  
   1.561  text {*
   1.562   We derive the conjunction elimination rule from the corresponding
   1.563   projections.  The proof is quite straight-forward, since
   1.564   Isabelle/Isar supports non-atomic goals and assumptions fully
   1.565   transparently.
   1.566 -*};
   1.567 +*}
   1.568  
   1.569 -theorem conjE: "A & B ==> (A ==> B ==> C) ==> C";
   1.570 -proof -;
   1.571 -  assume "A & B";
   1.572 -  assume r: "A ==> B ==> C";
   1.573 -  show C;
   1.574 -  proof (rule r);
   1.575 -    show A; by (rule conjunct1);
   1.576 -    show B; by (rule conjunct2);
   1.577 -  qed;
   1.578 -qed;
   1.579 +theorem conjE: "A & B ==> (A ==> B ==> C) ==> C"
   1.580 +proof -
   1.581 +  assume "A & B"
   1.582 +  assume r: "A ==> B ==> C"
   1.583 +  show C
   1.584 +  proof (rule r)
   1.585 +    show A by (rule conjunct1)
   1.586 +    show B by (rule conjunct2)
   1.587 +  qed
   1.588 +qed
   1.589  
   1.590  text {*
   1.591   Note that classic Isabelle handles higher rules in a slightly
   1.592 @@ -454,6 +454,6 @@
   1.593   \texttt{goal} command to decompose the rule into premises and
   1.594   conclusion.  The actual result would then emerge by discharging of
   1.595   the context at \texttt{qed} time.
   1.596 -*};
   1.597 +*}
   1.598  
   1.599 -end;
   1.600 +end