src/HOL/Isar_examples/BasicLogic.thy
 author paulson Tue Jun 28 15:27:45 2005 +0200 (2005-06-28) changeset 16587 b34c8aa657a5 parent 16417 9bc16273c2d4 child 18193 54419506df9e permissions -rw-r--r--
Constant "If" is now local
 wenzelm@6444  1 (* Title: HOL/Isar_examples/BasicLogic.thy  wenzelm@6444  2  ID: $Id$  wenzelm@6444  3  Author: Markus Wenzel, TU Muenchen  wenzelm@6444  4 wenzelm@6444  5 Basic propositional and quantifier reasoning.  wenzelm@6444  6 *)  wenzelm@6444  7 wenzelm@10007  8 header {* Basic logical reasoning *}  wenzelm@7748  9 haftmann@16417  10 theory BasicLogic imports Main begin  wenzelm@6444  11 wenzelm@7761  12 wenzelm@10007  13 subsection {* Pure backward reasoning *}  wenzelm@7740  14 wenzelm@7820  15 text {*  wenzelm@7820  16  In order to get a first idea of how Isabelle/Isar proof documents may  wenzelm@7820  17  look like, we consider the propositions $I$, $K$, and $S$. The  wenzelm@7820  18  following (rather explicit) proofs should require little extra  wenzelm@7820  19  explanations.  wenzelm@10007  20 *}  wenzelm@7001  21 wenzelm@10007  22 lemma I: "A --> A"  wenzelm@10007  23 proof  wenzelm@10007  24  assume A  wenzelm@10007  25  show A by assumption  wenzelm@10007  26 qed  wenzelm@6444  27 wenzelm@10007  28 lemma K: "A --> B --> A"  wenzelm@10007  29 proof  wenzelm@10007  30  assume A  wenzelm@10007  31  show "B --> A"  wenzelm@10007  32  proof  wenzelm@10007  33  show A by assumption  wenzelm@10007  34  qed  wenzelm@10007  35 qed  wenzelm@6444  36 wenzelm@10007  37 lemma S: "(A --> B --> C) --> (A --> B) --> A --> C"  wenzelm@10007  38 proof  wenzelm@10007  39  assume "A --> B --> C"  wenzelm@10007  40  show "(A --> B) --> A --> C"  wenzelm@10007  41  proof  wenzelm@10007  42  assume "A --> B"  wenzelm@10007  43  show "A --> C"  wenzelm@10007  44  proof  wenzelm@10007  45  assume A  wenzelm@10007  46  show C  wenzelm@10007  47  proof (rule mp)  wenzelm@10007  48  show "B --> C" by (rule mp)  wenzelm@10007  49  show B by (rule mp)  wenzelm@10007  50  qed  wenzelm@10007  51  qed  wenzelm@10007  52  qed  wenzelm@10007  53 qed  wenzelm@6444  54 wenzelm@7820  55 text {*  wenzelm@7820  56  Isar provides several ways to fine-tune the reasoning, avoiding  wenzelm@7874  57  excessive detail. Several abbreviated language elements are  wenzelm@7820  58  available, enabling the writer to express proofs in a more concise  wenzelm@7820  59  way, even without referring to any automated proof tools yet.  wenzelm@7761  60 wenzelm@7820  61  First of all, proof by assumption may be abbreviated as a single dot.  wenzelm@10007  62 *}  wenzelm@7820  63 wenzelm@10007  64 lemma "A --> A"  wenzelm@10007  65 proof  wenzelm@10007  66  assume A  wenzelm@10007  67  show A .  wenzelm@10007  68 qed  wenzelm@7820  69 wenzelm@7820  70 text {*  wenzelm@7820  71  In fact, concluding any (sub-)proof already involves solving any  wenzelm@7860  72  remaining goals by assumption\footnote{This is not a completely  wenzelm@7982  73  trivial operation, as proof by assumption may involve full  wenzelm@7982  74  higher-order unification.}. Thus we may skip the rather vacuous body  wenzelm@7982  75  of the above proof as well.  wenzelm@10007  76 *}  wenzelm@7820  77 wenzelm@10007  78 lemma "A --> A"  wenzelm@10007  79 proof  wenzelm@10007  80 qed  wenzelm@7820  81 wenzelm@7820  82 text {*  wenzelm@7820  83  Note that the \isacommand{proof} command refers to the $\idt{rule}$  wenzelm@7820  84  method (without arguments) by default. Thus it implicitly applies a  wenzelm@7820  85  single rule, as determined from the syntactic form of the statements  wenzelm@7820  86  involved. The \isacommand{by} command abbreviates any proof with  wenzelm@7820  87  empty body, so the proof may be further pruned.  wenzelm@10007  88 *}  wenzelm@7820  89 wenzelm@10007  90 lemma "A --> A"  wenzelm@10007  91  by rule  wenzelm@7820  92 wenzelm@7820  93 text {*  wenzelm@7874  94  Proof by a single rule may be abbreviated as double-dot.  wenzelm@10007  95 *}  wenzelm@7820  96 wenzelm@10007  97 lemma "A --> A" ..  wenzelm@7820  98 wenzelm@7820  99 text {*  wenzelm@7820  100  Thus we have arrived at an adequate representation of the proof of a  wenzelm@7860  101  tautology that holds by a single standard rule.\footnote{Apparently,  wenzelm@7982  102  the rule here is implication introduction.}  wenzelm@10007  103 *}  wenzelm@7820  104 wenzelm@7820  105 text {*  wenzelm@7874  106  Let us also reconsider $K$. Its statement is composed of iterated  wenzelm@7820  107  connectives. Basic decomposition is by a single rule at a time,  wenzelm@7820  108  which is why our first version above was by nesting two proofs.  wenzelm@7820  109 wenzelm@7820  110  The $\idt{intro}$ proof method repeatedly decomposes a goal's  wenzelm@7820  111  conclusion.\footnote{The dual method is $\idt{elim}$, acting on a  wenzelm@7820  112  goal's premises.}  wenzelm@10007  113 *}  wenzelm@7820  114 wenzelm@10007  115 lemma "A --> B --> A"  wenzelm@12387  116 proof (intro impI)  wenzelm@10007  117  assume A  wenzelm@10007  118  show A .  wenzelm@10007  119 qed  wenzelm@7820  120 wenzelm@7820  121 text {*  wenzelm@7820  122  Again, the body may be collapsed.  wenzelm@10007  123 *}  wenzelm@7820  124 wenzelm@10007  125 lemma "A --> B --> A"  wenzelm@12387  126  by (intro impI)  wenzelm@7820  127 wenzelm@7820  128 text {*  wenzelm@7820  129  Just like $\idt{rule}$, the $\idt{intro}$ and $\idt{elim}$ proof  wenzelm@7820  130  methods pick standard structural rules, in case no explicit arguments  wenzelm@7820  131  are given. While implicit rules are usually just fine for single  wenzelm@7982  132  rule application, this may go too far with iteration. Thus in  wenzelm@7820  133  practice, $\idt{intro}$ and $\idt{elim}$ would be typically  wenzelm@7820  134  restricted to certain structures by giving a few rules only, e.g.\  wenzelm@7860  135  \isacommand{proof}~($\idt{intro}$~\name{impI}~\name{allI}) to strip  wenzelm@7860  136  implications and universal quantifiers.  wenzelm@7820  137 wenzelm@7874  138  Such well-tuned iterated decomposition of certain structures is the  wenzelm@7874  139  prime application of $\idt{intro}$ and $\idt{elim}$. In contrast,  wenzelm@7874  140  terminal steps that solve a goal completely are usually performed by  wenzelm@7874  141  actual automated proof methods (such as  wenzelm@7820  142  \isacommand{by}~$\idt{blast}$).  wenzelm@10007  143 *}  wenzelm@7820  144 wenzelm@7820  145 wenzelm@10007  146 subsection {* Variations of backward vs.\ forward reasoning *}  wenzelm@7820  147 wenzelm@7820  148 text {*  wenzelm@7820  149  Certainly, any proof may be performed in backward-style only. On the  wenzelm@7820  150  other hand, small steps of reasoning are often more naturally  wenzelm@7820  151  expressed in forward-style. Isar supports both backward and forward  wenzelm@7820  152  reasoning as a first-class concept. In order to demonstrate the  wenzelm@7820  153  difference, we consider several proofs of $A \conj B \impl B \conj  wenzelm@7820  154  A$.  wenzelm@7820  155 wenzelm@7820  156  The first version is purely backward.  wenzelm@10007  157 *}  wenzelm@7001  158 wenzelm@10007  159 lemma "A & B --> B & A"  wenzelm@10007  160 proof  wenzelm@10007  161  assume "A & B"  wenzelm@10007  162  show "B & A"  wenzelm@10007  163  proof  wenzelm@10007  164  show B by (rule conjunct2)  wenzelm@10007  165  show A by (rule conjunct1)  wenzelm@10007  166  qed  wenzelm@10007  167 qed  wenzelm@6444  168 wenzelm@7820  169 text {*  wenzelm@7820  170  Above, the $\idt{conjunct}_{1/2}$ projection rules had to be named  wenzelm@7982  171  explicitly, since the goals $B$ and $A$ did not provide any  wenzelm@7982  172  structural clue. This may be avoided using \isacommand{from} to  wenzelm@7982  173  focus on $\idt{prems}$ (i.e.\ the $A \conj B$ assumption) as the  wenzelm@7982  174  current facts, enabling the use of double-dot proofs. Note that  wenzelm@7982  175  \isacommand{from} already does forward-chaining, involving the  wenzelm@7982  176  \name{conjE} rule here.  wenzelm@10007  177 *}  wenzelm@6444  178 wenzelm@10007  179 lemma "A & B --> B & A"  wenzelm@10007  180 proof  wenzelm@10007  181  assume "A & B"  wenzelm@10007  182  show "B & A"  wenzelm@10007  183  proof  wenzelm@10007  184  from prems show B ..  wenzelm@10007  185  from prems show A ..  wenzelm@10007  186  qed  wenzelm@10007  187 qed  wenzelm@7604  188 wenzelm@7820  189 text {*  wenzelm@7820  190  In the next version, we move the forward step one level upwards.  wenzelm@7820  191  Forward-chaining from the most recent facts is indicated by the  wenzelm@7820  192  \isacommand{then} command. Thus the proof of $B \conj A$ from $A  wenzelm@7820  193  \conj B$ actually becomes an elimination, rather than an  wenzelm@7820  194  introduction. The resulting proof structure directly corresponds to  wenzelm@7820  195  that of the $\name{conjE}$ rule, including the repeated goal  wenzelm@7820  196  proposition that is abbreviated as $\var{thesis}$ below.  wenzelm@10007  197 *}  wenzelm@7820  198 wenzelm@10007  199 lemma "A & B --> B & A"  wenzelm@10007  200 proof  wenzelm@10007  201  assume "A & B"  wenzelm@10007  202  then show "B & A"  wenzelm@10007  203  proof -- {* rule \name{conjE} of $A \conj B$ *}  wenzelm@10007  204  assume A B  wenzelm@10007  205  show ?thesis .. -- {* rule \name{conjI} of $B \conj A$ *}  wenzelm@10007  206  qed  wenzelm@10007  207 qed  wenzelm@7820  208 wenzelm@7820  209 text {*  wenzelm@7874  210  In the subsequent version we flatten the structure of the main body  wenzelm@7874  211  by doing forward reasoning all the time. Only the outermost  wenzelm@7874  212  decomposition step is left as backward.  wenzelm@10007  213 *}  wenzelm@7820  214 wenzelm@10007  215 lemma "A & B --> B & A"  wenzelm@10007  216 proof  wenzelm@10007  217  assume ab: "A & B"  wenzelm@10007  218  from ab have a: A ..  wenzelm@10007  219  from ab have b: B ..  wenzelm@10007  220  from b a show "B & A" ..  wenzelm@10007  221 qed  wenzelm@6444  222 wenzelm@7820  223 text {*  wenzelm@9659  224  We can still push forward-reasoning a bit further, even at the risk  wenzelm@7820  225  of getting ridiculous. Note that we force the initial proof step to  wenzelm@7982  226  do nothing here, by referring to the -'' proof method.  wenzelm@10007  227 *}  wenzelm@7820  228 wenzelm@10007  229 lemma "A & B --> B & A"  wenzelm@10007  230 proof -  wenzelm@10007  231  {  wenzelm@10007  232  assume ab: "A & B"  wenzelm@10007  233  from ab have a: A ..  wenzelm@10007  234  from ab have b: B ..  wenzelm@10007  235  from b a have "B & A" ..  wenzelm@10007  236  }  wenzelm@10007  237  thus ?thesis .. -- {* rule \name{impI} *}  wenzelm@10007  238 qed  wenzelm@7820  239 wenzelm@7820  240 text {*  wenzelm@7820  241  \medskip With these examples we have shifted through a whole range  wenzelm@7820  242  from purely backward to purely forward reasoning. Apparently, in the  wenzelm@7820  243  extreme ends we get slightly ill-structured proofs, which also  wenzelm@7820  244  require much explicit naming of either rules (backward) or local  wenzelm@7820  245  facts (forward).  wenzelm@7820  246 wenzelm@7820  247  The general lesson learned here is that good proof style would  wenzelm@7820  248  achieve just the \emph{right} balance of top-down backward  wenzelm@7982  249  decomposition, and bottom-up forward composition. In general, there  wenzelm@7820  250  is no single best way to arrange some pieces of formal reasoning, of  wenzelm@7820  251  course. Depending on the actual applications, the intended audience  wenzelm@7874  252  etc., rules (and methods) on the one hand vs.\ facts on the other  wenzelm@7874  253  hand have to be emphasized in an appropriate way. This requires the  wenzelm@7874  254  proof writer to develop good taste, and some practice, of course.  wenzelm@10007  255 *}  wenzelm@7820  256 wenzelm@7820  257 text {*  wenzelm@7820  258  For our example the most appropriate way of reasoning is probably the  wenzelm@7820  259  middle one, with conjunction introduction done after elimination.  wenzelm@7820  260  This reads even more concisely using \isacommand{thus}, which  wenzelm@7820  261  abbreviates \isacommand{then}~\isacommand{show}.\footnote{In the same  wenzelm@7820  262  vein, \isacommand{hence} abbreviates  wenzelm@7820  263  \isacommand{then}~\isacommand{have}.}  wenzelm@10007  264 *}  wenzelm@7820  265 wenzelm@10007  266 lemma "A & B --> B & A"  wenzelm@10007  267 proof  wenzelm@10007  268  assume "A & B"  wenzelm@10007  269  thus "B & A"  wenzelm@10007  270  proof  wenzelm@10007  271  assume A B  wenzelm@10007  272  show ?thesis ..  wenzelm@10007  273  qed  wenzelm@10007  274 qed  wenzelm@7820  275 wenzelm@7820  276 wenzelm@6444  277 wenzelm@10007  278 subsection {* A few examples from Introduction to Isabelle'' *}  wenzelm@7001  279 wenzelm@7820  280 text {*  wenzelm@7820  281  We rephrase some of the basic reasoning examples of  wenzelm@7982  282  \cite{isabelle-intro}, using HOL rather than FOL.  wenzelm@10007  283 *}  wenzelm@7820  284 wenzelm@10007  285 subsubsection {* A propositional proof *}  wenzelm@7833  286 wenzelm@7833  287 text {*  wenzelm@7833  288  We consider the proposition $P \disj P \impl P$. The proof below  wenzelm@7833  289  involves forward-chaining from $P \disj P$, followed by an explicit  wenzelm@7833  290  case-analysis on the two \emph{identical} cases.  wenzelm@10007  291 *}  wenzelm@6444  292 wenzelm@10007  293 lemma "P | P --> P"  wenzelm@10007  294 proof  wenzelm@10007  295  assume "P | P"  wenzelm@10007  296  thus P  wenzelm@7833  297  proof -- {*  wenzelm@7833  298  rule \name{disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}  wenzelm@10007  299  *}  wenzelm@10007  300  assume P show P .  wenzelm@10007  301  next  wenzelm@10007  302  assume P show P .  wenzelm@10007  303  qed  wenzelm@10007  304 qed  wenzelm@7833  305 wenzelm@7833  306 text {*  wenzelm@7833  307  Case splits are \emph{not} hardwired into the Isar language as a  wenzelm@7833  308  special feature. The \isacommand{next} command used to separate the  wenzelm@7833  309  cases above is just a short form of managing block structure.  wenzelm@7833  310 wenzelm@7833  311  \medskip In general, applying proof methods may split up a goal into  wenzelm@7833  312  separate cases'', i.e.\ new subgoals with individual local  wenzelm@7833  313  assumptions. The corresponding proof text typically mimics this by  wenzelm@7833  314  establishing results in appropriate contexts, separated by blocks.  wenzelm@7833  315 wenzelm@7860  316  In order to avoid too much explicit parentheses, the Isar system  wenzelm@7833  317  implicitly opens an additional block for any new goal, the  wenzelm@7833  318  \isacommand{next} statement then closes one block level, opening a  wenzelm@7982  319  new one. The resulting behavior is what one would expect from  wenzelm@7982  320  separating cases, only that it is more flexible. E.g.\ an induction  wenzelm@7833  321  base case (which does not introduce local assumptions) would  wenzelm@7833  322  \emph{not} require \isacommand{next} to separate the subsequent step  wenzelm@7833  323  case.  wenzelm@7833  324 wenzelm@7833  325  \medskip In our example the situation is even simpler, since the two  wenzelm@7874  326  cases actually coincide. Consequently the proof may be rephrased as  wenzelm@7874  327  follows.  wenzelm@10007  328 *}  wenzelm@7833  329 wenzelm@10007  330 lemma "P | P --> P"  wenzelm@10007  331 proof  wenzelm@10007  332  assume "P | P"  wenzelm@10007  333  thus P  wenzelm@10007  334  proof  wenzelm@10007  335  assume P  wenzelm@10007  336  show P .  wenzelm@10007  337  show P .  wenzelm@10007  338  qed  wenzelm@10007  339 qed  wenzelm@6444  340 wenzelm@7833  341 text {*  wenzelm@7833  342  Again, the rather vacuous body of the proof may be collapsed. Thus  wenzelm@7860  343  the case analysis degenerates into two assumption steps, which are  wenzelm@7860  344  implicitly performed when concluding the single rule step of the  wenzelm@7860  345  double-dot proof as follows.  wenzelm@10007  346 *}  wenzelm@7833  347 wenzelm@10007  348 lemma "P | P --> P"  wenzelm@10007  349 proof  wenzelm@10007  350  assume "P | P"  wenzelm@10007  351  thus P ..  wenzelm@10007  352 qed  wenzelm@6444  353 wenzelm@6444  354 wenzelm@10007  355 subsubsection {* A quantifier proof *}  wenzelm@7833  356 wenzelm@7833  357 text {*  wenzelm@7833  358  To illustrate quantifier reasoning, let us prove $(\ex x P \ap (f \ap  wenzelm@7833  359  x)) \impl (\ex x P \ap x)$. Informally, this holds because any $a$  wenzelm@7833  360  with $P \ap (f \ap a)$ may be taken as a witness for the second  wenzelm@7833  361  existential statement.  wenzelm@6444  362 wenzelm@7833  363  The first proof is rather verbose, exhibiting quite a lot of  wenzelm@7833  364  (redundant) detail. It gives explicit rules, even with some  wenzelm@7833  365  instantiation. Furthermore, we encounter two new language elements:  wenzelm@7833  366  the \isacommand{fix} command augments the context by some new  wenzelm@7833  367  arbitrary, but fixed'' element; the \isacommand{is} annotation  wenzelm@7833  368  binds term abbreviations by higher-order pattern matching.  wenzelm@10007  369 *}  wenzelm@7833  370 wenzelm@10636  371 lemma "(EX x. P (f x)) --> (EX y. P y)"  wenzelm@10007  372 proof  wenzelm@10007  373  assume "EX x. P (f x)"  wenzelm@10636  374  thus "EX y. P y"  wenzelm@7833  375  proof (rule exE) -- {*  wenzelm@7833  376  rule \name{exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}  wenzelm@10007  377  *}  wenzelm@10007  378  fix a  wenzelm@10007  379  assume "P (f a)" (is "P ?witness")  wenzelm@10007  380  show ?thesis by (rule exI [of P ?witness])  wenzelm@10007  381  qed  wenzelm@10007  382 qed  wenzelm@6444  383 wenzelm@7833  384 text {*  wenzelm@7982  385  While explicit rule instantiation may occasionally improve  wenzelm@7982  386  readability of certain aspects of reasoning, it is usually quite  wenzelm@7833  387  redundant. Above, the basic proof outline gives already enough  wenzelm@7833  388  structural clues for the system to infer both the rules and their  wenzelm@7833  389  instances (by higher-order unification). Thus we may as well prune  wenzelm@7833  390  the text as follows.  wenzelm@10007  391 *}  wenzelm@7833  392 wenzelm@10636  393 lemma "(EX x. P (f x)) --> (EX y. P y)"  wenzelm@10007  394 proof  wenzelm@10007  395  assume "EX x. P (f x)"  wenzelm@10636  396  thus "EX y. P y"  wenzelm@10007  397  proof  wenzelm@10007  398  fix a  wenzelm@10007  399  assume "P (f a)"  wenzelm@10007  400  show ?thesis ..  wenzelm@10007  401  qed  wenzelm@10007  402 qed  wenzelm@6444  403 wenzelm@9477  404 text {*  wenzelm@9477  405  Explicit $\exists$-elimination as seen above can become quite  wenzelm@9477  406  cumbersome in practice. The derived Isar language element  wenzelm@9477  407  \isakeyword{obtain}'' provides a more handsome way to do  wenzelm@9477  408  generalized existence reasoning.  wenzelm@10007  409 *}  wenzelm@9477  410 wenzelm@10636  411 lemma "(EX x. P (f x)) --> (EX y. P y)"  wenzelm@10007  412 proof  wenzelm@10007  413  assume "EX x. P (f x)"  wenzelm@10636  414  then obtain a where "P (f a)" ..  wenzelm@10636  415  thus "EX y. P y" ..  wenzelm@10007  416 qed  wenzelm@9477  417 wenzelm@9477  418 text {*  wenzelm@9477  419  Technically, \isakeyword{obtain} is similar to \isakeyword{fix} and  wenzelm@9477  420  \isakeyword{assume} together with a soundness proof of the  wenzelm@9477  421  elimination involved. Thus it behaves similar to any other forward  wenzelm@9477  422  proof element. Also note that due to the nature of general existence  wenzelm@9477  423  reasoning involved here, any result exported from the context of an  wenzelm@9477  424  \isakeyword{obtain} statement may \emph{not} refer to the parameters  wenzelm@9477  425  introduced there.  wenzelm@10007  426 *}  wenzelm@9477  427 wenzelm@9477  428 wenzelm@6444  429 wenzelm@10007  430 subsubsection {* Deriving rules in Isabelle *}  wenzelm@7001  431 wenzelm@7833  432 text {*  wenzelm@7982  433  We derive the conjunction elimination rule from the corresponding  wenzelm@7982  434  projections. The proof is quite straight-forward, since  wenzelm@7982  435  Isabelle/Isar supports non-atomic goals and assumptions fully  wenzelm@7982  436  transparently.  wenzelm@10007  437 *}  wenzelm@7001  438 wenzelm@10007  439 theorem conjE: "A & B ==> (A ==> B ==> C) ==> C"  wenzelm@10007  440 proof -  wenzelm@10007  441  assume "A & B"  wenzelm@10007  442  assume r: "A ==> B ==> C"  wenzelm@10007  443  show C  wenzelm@10007  444  proof (rule r)  wenzelm@10007  445  show A by (rule conjunct1)  wenzelm@10007  446  show B by (rule conjunct2)  wenzelm@10007  447  qed  wenzelm@10007  448 qed  wenzelm@7001  449 wenzelm@7860  450 text {*  wenzelm@7860  451  Note that classic Isabelle handles higher rules in a slightly  wenzelm@7860  452  different way. The tactic script as given in \cite{isabelle-intro}  wenzelm@7860  453  for the same example of \name{conjE} depends on the primitive  wenzelm@7860  454  \texttt{goal} command to decompose the rule into premises and  wenzelm@7982  455  conclusion. The actual result would then emerge by discharging of  wenzelm@7860  456  the context at \texttt{qed} time.  wenzelm@10007  457 *}  wenzelm@7860  458 wenzelm@10007  459 end