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