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