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