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