src/Doc/Isar_Ref/Synopsis.thy
author wenzelm
Mon Oct 09 21:12:22 2017 +0200 (23 months ago)
changeset 66822 4642cf4a7ebb
parent 63680 6e1e8b5abbfa
child 67369 7360fe6bb423
permissions -rw-r--r--
tuned signature;
     1 (*:maxLineLen=78:*)
     2 
     3 theory Synopsis
     4   imports Main Base
     5 begin
     6 
     7 chapter \<open>Synopsis\<close>
     8 
     9 section \<open>Notepad\<close>
    10 
    11 text \<open>
    12   An Isar proof body serves as mathematical notepad to compose logical
    13   content, consisting of types, terms, facts.
    14 \<close>
    15 
    16 
    17 subsection \<open>Types and terms\<close>
    18 
    19 notepad
    20 begin
    21   txt \<open>Locally fixed entities:\<close>
    22   fix x   \<comment> \<open>local constant, without any type information yet\<close>
    23   fix x :: 'a  \<comment> \<open>variant with explicit type-constraint for subsequent use\<close>
    24 
    25   fix a b
    26   assume "a = b"  \<comment> \<open>type assignment at first occurrence in concrete term\<close>
    27 
    28   txt \<open>Definitions (non-polymorphic):\<close>
    29   define x :: 'a where "x = t"
    30 
    31   txt \<open>Abbreviations (polymorphic):\<close>
    32   let ?f = "\<lambda>x. x"
    33   term "?f ?f"
    34 
    35   txt \<open>Notation:\<close>
    36   write x  ("***")
    37 end
    38 
    39 
    40 subsection \<open>Facts\<close>
    41 
    42 text \<open>
    43   A fact is a simultaneous list of theorems.
    44 \<close>
    45 
    46 
    47 subsubsection \<open>Producing facts\<close>
    48 
    49 notepad
    50 begin
    51 
    52   txt \<open>Via assumption (``lambda''):\<close>
    53   assume a: A
    54 
    55   txt \<open>Via proof (``let''):\<close>
    56   have b: B \<proof>
    57 
    58   txt \<open>Via abbreviation (``let''):\<close>
    59   note c = a b
    60 
    61 end
    62 
    63 
    64 subsubsection \<open>Referencing facts\<close>
    65 
    66 notepad
    67 begin
    68   txt \<open>Via explicit name:\<close>
    69   assume a: A
    70   note a
    71 
    72   txt \<open>Via implicit name:\<close>
    73   assume A
    74   note this
    75 
    76   txt \<open>Via literal proposition (unification with results from the proof text):\<close>
    77   assume A
    78   note \<open>A\<close>
    79 
    80   assume "\<And>x. B x"
    81   note \<open>B a\<close>
    82   note \<open>B b\<close>
    83 end
    84 
    85 
    86 subsubsection \<open>Manipulating facts\<close>
    87 
    88 notepad
    89 begin
    90   txt \<open>Instantiation:\<close>
    91   assume a: "\<And>x. B x"
    92   note a
    93   note a [of b]
    94   note a [where x = b]
    95 
    96   txt \<open>Backchaining:\<close>
    97   assume 1: A
    98   assume 2: "A \<Longrightarrow> C"
    99   note 2 [OF 1]
   100   note 1 [THEN 2]
   101 
   102   txt \<open>Symmetric results:\<close>
   103   assume "x = y"
   104   note this [symmetric]
   105 
   106   assume "x \<noteq> y"
   107   note this [symmetric]
   108 
   109   txt \<open>Adhoc-simplification (take care!):\<close>
   110   assume "P ([] @ xs)"
   111   note this [simplified]
   112 end
   113 
   114 
   115 subsubsection \<open>Projections\<close>
   116 
   117 text \<open>
   118   Isar facts consist of multiple theorems.  There is notation to project
   119   interval ranges.
   120 \<close>
   121 
   122 notepad
   123 begin
   124   assume stuff: A B C D
   125   note stuff(1)
   126   note stuff(2-3)
   127   note stuff(2-)
   128 end
   129 
   130 
   131 subsubsection \<open>Naming conventions\<close>
   132 
   133 text \<open>
   134   \<^item> Lower-case identifiers are usually preferred.
   135 
   136   \<^item> Facts can be named after the main term within the proposition.
   137 
   138   \<^item> Facts should \<^emph>\<open>not\<close> be named after the command that
   139   introduced them (@{command "assume"}, @{command "have"}).  This is
   140   misleading and hard to maintain.
   141 
   142   \<^item> Natural numbers can be used as ``meaningless'' names (more
   143   appropriate than \<open>a1\<close>, \<open>a2\<close> etc.)
   144 
   145   \<^item> Symbolic identifiers are supported (e.g. \<open>*\<close>, \<open>**\<close>, \<open>***\<close>).
   146 \<close>
   147 
   148 
   149 subsection \<open>Block structure\<close>
   150 
   151 text \<open>
   152   The formal notepad is block structured.  The fact produced by the last
   153   entry of a block is exported into the outer context.
   154 \<close>
   155 
   156 notepad
   157 begin
   158   {
   159     have a: A \<proof>
   160     have b: B \<proof>
   161     note a b
   162   }
   163   note this
   164   note \<open>A\<close>
   165   note \<open>B\<close>
   166 end
   167 
   168 text \<open>Explicit blocks as well as implicit blocks of nested goal
   169   statements (e.g.\ @{command have}) automatically introduce one extra
   170   pair of parentheses in reserve.  The @{command next} command allows
   171   to ``jump'' between these sub-blocks.\<close>
   172 
   173 notepad
   174 begin
   175 
   176   {
   177     have a: A \<proof>
   178   next
   179     have b: B
   180     proof -
   181       show B \<proof>
   182     next
   183       have c: C \<proof>
   184     next
   185       have d: D \<proof>
   186     qed
   187   }
   188 
   189   txt \<open>Alternative version with explicit parentheses everywhere:\<close>
   190 
   191   {
   192     {
   193       have a: A \<proof>
   194     }
   195     {
   196       have b: B
   197       proof -
   198         {
   199           show B \<proof>
   200         }
   201         {
   202           have c: C \<proof>
   203         }
   204         {
   205           have d: D \<proof>
   206         }
   207       qed
   208     }
   209   }
   210 
   211 end
   212 
   213 
   214 section \<open>Calculational reasoning \label{sec:calculations-synopsis}\<close>
   215 
   216 text \<open>
   217   For example, see \<^file>\<open>~~/src/HOL/Isar_Examples/Group.thy\<close>.
   218 \<close>
   219 
   220 
   221 subsection \<open>Special names in Isar proofs\<close>
   222 
   223 text \<open>
   224   \<^item> term \<open>?thesis\<close> --- the main conclusion of the
   225   innermost pending claim
   226 
   227   \<^item> term \<open>\<dots>\<close> --- the argument of the last explicitly
   228   stated result (for infix application this is the right-hand side)
   229 
   230   \<^item> fact \<open>this\<close> --- the last result produced in the text
   231 \<close>
   232 
   233 notepad
   234 begin
   235   have "x = y"
   236   proof -
   237     term ?thesis
   238     show ?thesis \<proof>
   239     term ?thesis  \<comment> \<open>static!\<close>
   240   qed
   241   term "\<dots>"
   242   thm this
   243 end
   244 
   245 text \<open>Calculational reasoning maintains the special fact called
   246   ``\<open>calculation\<close>'' in the background.  Certain language
   247   elements combine primary \<open>this\<close> with secondary \<open>calculation\<close>.\<close>
   248 
   249 
   250 subsection \<open>Transitive chains\<close>
   251 
   252 text \<open>The Idea is to combine \<open>this\<close> and \<open>calculation\<close>
   253   via typical \<open>trans\<close> rules (see also @{command
   254   print_trans_rules}):\<close>
   255 
   256 thm trans
   257 thm less_trans
   258 thm less_le_trans
   259 
   260 notepad
   261 begin
   262   txt \<open>Plain bottom-up calculation:\<close>
   263   have "a = b" \<proof>
   264   also
   265   have "b = c" \<proof>
   266   also
   267   have "c = d" \<proof>
   268   finally
   269   have "a = d" .
   270 
   271   txt \<open>Variant using the \<open>\<dots>\<close> abbreviation:\<close>
   272   have "a = b" \<proof>
   273   also
   274   have "\<dots> = c" \<proof>
   275   also
   276   have "\<dots> = d" \<proof>
   277   finally
   278   have "a = d" .
   279 
   280   txt \<open>Top-down version with explicit claim at the head:\<close>
   281   have "a = d"
   282   proof -
   283     have "a = b" \<proof>
   284     also
   285     have "\<dots> = c" \<proof>
   286     also
   287     have "\<dots> = d" \<proof>
   288     finally
   289     show ?thesis .
   290   qed
   291 next
   292   txt \<open>Mixed inequalities (require suitable base type):\<close>
   293   fix a b c d :: nat
   294 
   295   have "a < b" \<proof>
   296   also
   297   have "b \<le> c" \<proof>
   298   also
   299   have "c = d" \<proof>
   300   finally
   301   have "a < d" .
   302 end
   303 
   304 
   305 subsubsection \<open>Notes\<close>
   306 
   307 text \<open>
   308   \<^item> The notion of \<open>trans\<close> rule is very general due to the
   309   flexibility of Isabelle/Pure rule composition.
   310 
   311   \<^item> User applications may declare their own rules, with some care
   312   about the operational details of higher-order unification.
   313 \<close>
   314 
   315 
   316 subsection \<open>Degenerate calculations\<close>
   317 
   318 text \<open>The Idea is to append \<open>this\<close> to \<open>calculation\<close>, without rule composition.
   319   This is occasionally useful to avoid naming intermediate facts.\<close>
   320 
   321 notepad
   322 begin
   323   txt \<open>A vacuous proof:\<close>
   324   have A \<proof>
   325   moreover
   326   have B \<proof>
   327   moreover
   328   have C \<proof>
   329   ultimately
   330   have A and B and C .
   331 next
   332   txt \<open>Slightly more content (trivial bigstep reasoning):\<close>
   333   have A \<proof>
   334   moreover
   335   have B \<proof>
   336   moreover
   337   have C \<proof>
   338   ultimately
   339   have "A \<and> B \<and> C" by blast
   340 end
   341 
   342 text \<open>Note that For multi-branch case splitting, it is better to use @{command
   343   consider}.\<close>
   344 
   345 
   346 section \<open>Induction\<close>
   347 
   348 subsection \<open>Induction as Natural Deduction\<close>
   349 
   350 text \<open>In principle, induction is just a special case of Natural
   351   Deduction (see also \secref{sec:natural-deduction-synopsis}).  For
   352   example:\<close>
   353 
   354 thm nat.induct
   355 print_statement nat.induct
   356 
   357 notepad
   358 begin
   359   fix n :: nat
   360   have "P n"
   361   proof (rule nat.induct)  \<comment> \<open>fragile rule application!\<close>
   362     show "P 0" \<proof>
   363   next
   364     fix n :: nat
   365     assume "P n"
   366     show "P (Suc n)" \<proof>
   367   qed
   368 end
   369 
   370 text \<open>
   371   In practice, much more proof infrastructure is required.
   372 
   373   The proof method @{method induct} provides:
   374 
   375   \<^item> implicit rule selection and robust instantiation
   376 
   377   \<^item> context elements via symbolic case names
   378 
   379   \<^item> support for rule-structured induction statements, with local
   380   parameters, premises, etc.
   381 \<close>
   382 
   383 notepad
   384 begin
   385   fix n :: nat
   386   have "P n"
   387   proof (induct n)
   388     case 0
   389     show ?case \<proof>
   390   next
   391     case (Suc n)
   392     from Suc.hyps show ?case \<proof>
   393   qed
   394 end
   395 
   396 
   397 subsubsection \<open>Example\<close>
   398 
   399 text \<open>
   400   The subsequent example combines the following proof patterns:
   401 
   402   \<^item> outermost induction (over the datatype structure of natural
   403   numbers), to decompose the proof problem in top-down manner
   404 
   405   \<^item> calculational reasoning (\secref{sec:calculations-synopsis})
   406   to compose the result in each case
   407 
   408   \<^item> solving local claims within the calculation by simplification
   409 \<close>
   410 
   411 lemma
   412   fixes n :: nat
   413   shows "(\<Sum>i=0..n. i) = n * (n + 1) div 2"
   414 proof (induct n)
   415   case 0
   416   have "(\<Sum>i=0..0. i) = (0::nat)" by simp
   417   also have "\<dots> = 0 * (0 + 1) div 2" by simp
   418   finally show ?case .
   419 next
   420   case (Suc n)
   421   have "(\<Sum>i=0..Suc n. i) = (\<Sum>i=0..n. i) + (n + 1)" by simp
   422   also have "\<dots> = n * (n + 1) div 2 + (n + 1)" by (simp add: Suc.hyps)
   423   also have "\<dots> = (n * (n + 1) + 2 * (n + 1)) div 2" by simp
   424   also have "\<dots> = (Suc n * (Suc n + 1)) div 2" by simp
   425   finally show ?case .
   426 qed
   427 
   428 text \<open>This demonstrates how induction proofs can be done without
   429   having to consider the raw Natural Deduction structure.\<close>
   430 
   431 
   432 subsection \<open>Induction with local parameters and premises\<close>
   433 
   434 text \<open>Idea: Pure rule statements are passed through the induction
   435   rule.  This achieves convenient proof patterns, thanks to some
   436   internal trickery in the @{method induct} method.
   437 
   438   Important: Using compact HOL formulae with \<open>\<forall>/\<longrightarrow>\<close> is a
   439   well-known anti-pattern! It would produce useless formal noise.
   440 \<close>
   441 
   442 notepad
   443 begin
   444   fix n :: nat
   445   fix P :: "nat \<Rightarrow> bool"
   446   fix Q :: "'a \<Rightarrow> nat \<Rightarrow> bool"
   447 
   448   have "P n"
   449   proof (induct n)
   450     case 0
   451     show "P 0" \<proof>
   452   next
   453     case (Suc n)
   454     from \<open>P n\<close> show "P (Suc n)" \<proof>
   455   qed
   456 
   457   have "A n \<Longrightarrow> P n"
   458   proof (induct n)
   459     case 0
   460     from \<open>A 0\<close> show "P 0" \<proof>
   461   next
   462     case (Suc n)
   463     from \<open>A n \<Longrightarrow> P n\<close>
   464       and \<open>A (Suc n)\<close> show "P (Suc n)" \<proof>
   465   qed
   466 
   467   have "\<And>x. Q x n"
   468   proof (induct n)
   469     case 0
   470     show "Q x 0" \<proof>
   471   next
   472     case (Suc n)
   473     from \<open>\<And>x. Q x n\<close> show "Q x (Suc n)" \<proof>
   474     txt \<open>Local quantification admits arbitrary instances:\<close>
   475     note \<open>Q a n\<close> and \<open>Q b n\<close>
   476   qed
   477 end
   478 
   479 
   480 subsection \<open>Implicit induction context\<close>
   481 
   482 text \<open>The @{method induct} method can isolate local parameters and
   483   premises directly from the given statement.  This is convenient in
   484   practical applications, but requires some understanding of what is
   485   going on internally (as explained above).\<close>
   486 
   487 notepad
   488 begin
   489   fix n :: nat
   490   fix Q :: "'a \<Rightarrow> nat \<Rightarrow> bool"
   491 
   492   fix x :: 'a
   493   assume "A x n"
   494   then have "Q x n"
   495   proof (induct n arbitrary: x)
   496     case 0
   497     from \<open>A x 0\<close> show "Q x 0" \<proof>
   498   next
   499     case (Suc n)
   500     from \<open>\<And>x. A x n \<Longrightarrow> Q x n\<close>  \<comment> \<open>arbitrary instances can be produced here\<close>
   501       and \<open>A x (Suc n)\<close> show "Q x (Suc n)" \<proof>
   502   qed
   503 end
   504 
   505 
   506 subsection \<open>Advanced induction with term definitions\<close>
   507 
   508 text \<open>Induction over subexpressions of a certain shape are delicate
   509   to formalize.  The Isar @{method induct} method provides
   510   infrastructure for this.
   511 
   512   Idea: sub-expressions of the problem are turned into a defined
   513   induction variable; often accompanied with fixing of auxiliary
   514   parameters in the original expression.\<close>
   515 
   516 notepad
   517 begin
   518   fix a :: "'a \<Rightarrow> nat"
   519   fix A :: "nat \<Rightarrow> bool"
   520 
   521   assume "A (a x)"
   522   then have "P (a x)"
   523   proof (induct "a x" arbitrary: x)
   524     case 0
   525     note prem = \<open>A (a x)\<close>
   526       and defn = \<open>0 = a x\<close>
   527     show "P (a x)" \<proof>
   528   next
   529     case (Suc n)
   530     note hyp = \<open>\<And>x. n = a x \<Longrightarrow> A (a x) \<Longrightarrow> P (a x)\<close>
   531       and prem = \<open>A (a x)\<close>
   532       and defn = \<open>Suc n = a x\<close>
   533     show "P (a x)" \<proof>
   534   qed
   535 end
   536 
   537 
   538 section \<open>Natural Deduction \label{sec:natural-deduction-synopsis}\<close>
   539 
   540 subsection \<open>Rule statements\<close>
   541 
   542 text \<open>
   543   Isabelle/Pure ``theorems'' are always natural deduction rules,
   544   which sometimes happen to consist of a conclusion only.
   545 
   546   The framework connectives \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> indicate the
   547   rule structure declaratively.  For example:\<close>
   548 
   549 thm conjI
   550 thm impI
   551 thm nat.induct
   552 
   553 text \<open>
   554   The object-logic is embedded into the Pure framework via an implicit
   555   derivability judgment @{term "Trueprop :: bool \<Rightarrow> prop"}.
   556 
   557   Thus any HOL formulae appears atomic to the Pure framework, while
   558   the rule structure outlines the corresponding proof pattern.
   559 
   560   This can be made explicit as follows:
   561 \<close>
   562 
   563 notepad
   564 begin
   565   write Trueprop  ("Tr")
   566 
   567   thm conjI
   568   thm impI
   569   thm nat.induct
   570 end
   571 
   572 text \<open>
   573   Isar provides first-class notation for rule statements as follows.
   574 \<close>
   575 
   576 print_statement conjI
   577 print_statement impI
   578 print_statement nat.induct
   579 
   580 
   581 subsubsection \<open>Examples\<close>
   582 
   583 text \<open>
   584   Introductions and eliminations of some standard connectives of
   585   the object-logic can be written as rule statements as follows.  (The
   586   proof ``@{command "by"}~@{method blast}'' serves as sanity check.)
   587 \<close>
   588 
   589 lemma "(P \<Longrightarrow> False) \<Longrightarrow> \<not> P" by blast
   590 lemma "\<not> P \<Longrightarrow> P \<Longrightarrow> Q" by blast
   591 
   592 lemma "P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q" by blast
   593 lemma "P \<and> Q \<Longrightarrow> (P \<Longrightarrow> Q \<Longrightarrow> R) \<Longrightarrow> R" by blast
   594 
   595 lemma "P \<Longrightarrow> P \<or> Q" by blast
   596 lemma "Q \<Longrightarrow> P \<or> Q" by blast
   597 lemma "P \<or> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R" by blast
   598 
   599 lemma "(\<And>x. P x) \<Longrightarrow> (\<forall>x. P x)" by blast
   600 lemma "(\<forall>x. P x) \<Longrightarrow> P x" by blast
   601 
   602 lemma "P x \<Longrightarrow> (\<exists>x. P x)" by blast
   603 lemma "(\<exists>x. P x) \<Longrightarrow> (\<And>x. P x \<Longrightarrow> R) \<Longrightarrow> R" by blast
   604 
   605 lemma "x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A \<inter> B" by blast
   606 lemma "x \<in> A \<inter> B \<Longrightarrow> (x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> R) \<Longrightarrow> R" by blast
   607 
   608 lemma "x \<in> A \<Longrightarrow> x \<in> A \<union> B" by blast
   609 lemma "x \<in> B \<Longrightarrow> x \<in> A \<union> B" by blast
   610 lemma "x \<in> A \<union> B \<Longrightarrow> (x \<in> A \<Longrightarrow> R) \<Longrightarrow> (x \<in> B \<Longrightarrow> R) \<Longrightarrow> R" by blast
   611 
   612 
   613 subsection \<open>Isar context elements\<close>
   614 
   615 text \<open>We derive some results out of the blue, using Isar context
   616   elements and some explicit blocks.  This illustrates their meaning
   617   wrt.\ Pure connectives, without goal states getting in the way.\<close>
   618 
   619 notepad
   620 begin
   621   {
   622     fix x
   623     have "B x" \<proof>
   624   }
   625   have "\<And>x. B x" by fact
   626 
   627 next
   628 
   629   {
   630     assume A
   631     have B \<proof>
   632   }
   633   have "A \<Longrightarrow> B" by fact
   634 
   635 next
   636 
   637   {
   638     define x where "x = t"
   639     have "B x" \<proof>
   640   }
   641   have "B t" by fact
   642 
   643 next
   644 
   645   {
   646     obtain x :: 'a where "B x" \<proof>
   647     have C \<proof>
   648   }
   649   have C by fact
   650 
   651 end
   652 
   653 
   654 subsection \<open>Pure rule composition\<close>
   655 
   656 text \<open>
   657   The Pure framework provides means for:
   658 
   659   \<^item> backward-chaining of rules by @{inference resolution}
   660 
   661   \<^item> closing of branches by @{inference assumption}
   662 
   663 
   664   Both principles involve higher-order unification of \<open>\<lambda>\<close>-terms
   665   modulo \<open>\<alpha>\<beta>\<eta>\<close>-equivalence (cf.\ Huet and Miller).
   666 \<close>
   667 
   668 notepad
   669 begin
   670   assume a: A and b: B
   671   thm conjI
   672   thm conjI [of A B]  \<comment> "instantiation"
   673   thm conjI [of A B, OF a b]  \<comment> "instantiation and composition"
   674   thm conjI [OF a b]  \<comment> "composition via unification (trivial)"
   675   thm conjI [OF \<open>A\<close> \<open>B\<close>]
   676 
   677   thm conjI [OF disjI1]
   678 end
   679 
   680 text \<open>Note: Low-level rule composition is tedious and leads to
   681   unreadable~/ unmaintainable expressions in the text.\<close>
   682 
   683 
   684 subsection \<open>Structured backward reasoning\<close>
   685 
   686 text \<open>Idea: Canonical proof decomposition via @{command fix}~/
   687   @{command assume}~/ @{command show}, where the body produces a
   688   natural deduction rule to refine some goal.\<close>
   689 
   690 notepad
   691 begin
   692   fix A B :: "'a \<Rightarrow> bool"
   693 
   694   have "\<And>x. A x \<Longrightarrow> B x"
   695   proof -
   696     fix x
   697     assume "A x"
   698     show "B x" \<proof>
   699   qed
   700 
   701   have "\<And>x. A x \<Longrightarrow> B x"
   702   proof -
   703     {
   704       fix x
   705       assume "A x"
   706       show "B x" \<proof>
   707     } \<comment> "implicit block structure made explicit"
   708     note \<open>\<And>x. A x \<Longrightarrow> B x\<close>
   709       \<comment> "side exit for the resulting rule"
   710   qed
   711 end
   712 
   713 
   714 subsection \<open>Structured rule application\<close>
   715 
   716 text \<open>
   717   Idea: Previous facts and new claims are composed with a rule from
   718   the context (or background library).
   719 \<close>
   720 
   721 notepad
   722 begin
   723   assume r\<^sub>1: "A \<Longrightarrow> B \<Longrightarrow> C"  \<comment> \<open>simple rule (Horn clause)\<close>
   724 
   725   have A \<proof>  \<comment> "prefix of facts via outer sub-proof"
   726   then have C
   727   proof (rule r\<^sub>1)
   728     show B \<proof>  \<comment> "remaining rule premises via inner sub-proof"
   729   qed
   730 
   731   have C
   732   proof (rule r\<^sub>1)
   733     show A \<proof>
   734     show B \<proof>
   735   qed
   736 
   737   have A and B \<proof>
   738   then have C
   739   proof (rule r\<^sub>1)
   740   qed
   741 
   742   have A and B \<proof>
   743   then have C by (rule r\<^sub>1)
   744 
   745 next
   746 
   747   assume r\<^sub>2: "A \<Longrightarrow> (\<And>x. B\<^sub>1 x \<Longrightarrow> B\<^sub>2 x) \<Longrightarrow> C"  \<comment> \<open>nested rule\<close>
   748 
   749   have A \<proof>
   750   then have C
   751   proof (rule r\<^sub>2)
   752     fix x
   753     assume "B\<^sub>1 x"
   754     show "B\<^sub>2 x" \<proof>
   755   qed
   756 
   757   txt \<open>The compound rule premise @{prop "\<And>x. B\<^sub>1 x \<Longrightarrow> B\<^sub>2 x"} is better
   758     addressed via @{command fix}~/ @{command assume}~/ @{command show}
   759     in the nested proof body.\<close>
   760 end
   761 
   762 
   763 subsection \<open>Example: predicate logic\<close>
   764 
   765 text \<open>
   766   Using the above principles, standard introduction and elimination proofs
   767   of predicate logic connectives of HOL work as follows.
   768 \<close>
   769 
   770 notepad
   771 begin
   772   have "A \<longrightarrow> B" and A \<proof>
   773   then have B ..
   774 
   775   have A \<proof>
   776   then have "A \<or> B" ..
   777 
   778   have B \<proof>
   779   then have "A \<or> B" ..
   780 
   781   have "A \<or> B" \<proof>
   782   then have C
   783   proof
   784     assume A
   785     then show C \<proof>
   786   next
   787     assume B
   788     then show C \<proof>
   789   qed
   790 
   791   have A and B \<proof>
   792   then have "A \<and> B" ..
   793 
   794   have "A \<and> B" \<proof>
   795   then have A ..
   796 
   797   have "A \<and> B" \<proof>
   798   then have B ..
   799 
   800   have False \<proof>
   801   then have A ..
   802 
   803   have True ..
   804 
   805   have "\<not> A"
   806   proof
   807     assume A
   808     then show False \<proof>
   809   qed
   810 
   811   have "\<not> A" and A \<proof>
   812   then have B ..
   813 
   814   have "\<forall>x. P x"
   815   proof
   816     fix x
   817     show "P x" \<proof>
   818   qed
   819 
   820   have "\<forall>x. P x" \<proof>
   821   then have "P a" ..
   822 
   823   have "\<exists>x. P x"
   824   proof
   825     show "P a" \<proof>
   826   qed
   827 
   828   have "\<exists>x. P x" \<proof>
   829   then have C
   830   proof
   831     fix a
   832     assume "P a"
   833     show C \<proof>
   834   qed
   835 
   836   txt \<open>Less awkward version using @{command obtain}:\<close>
   837   have "\<exists>x. P x" \<proof>
   838   then obtain a where "P a" ..
   839 end
   840 
   841 text \<open>Further variations to illustrate Isar sub-proofs involving
   842   @{command show}:\<close>
   843 
   844 notepad
   845 begin
   846   have "A \<and> B"
   847   proof  \<comment> \<open>two strictly isolated subproofs\<close>
   848     show A \<proof>
   849   next
   850     show B \<proof>
   851   qed
   852 
   853   have "A \<and> B"
   854   proof  \<comment> \<open>one simultaneous sub-proof\<close>
   855     show A and B \<proof>
   856   qed
   857 
   858   have "A \<and> B"
   859   proof  \<comment> \<open>two subproofs in the same context\<close>
   860     show A \<proof>
   861     show B \<proof>
   862   qed
   863 
   864   have "A \<and> B"
   865   proof  \<comment> \<open>swapped order\<close>
   866     show B \<proof>
   867     show A \<proof>
   868   qed
   869 
   870   have "A \<and> B"
   871   proof  \<comment> \<open>sequential subproofs\<close>
   872     show A \<proof>
   873     show B using \<open>A\<close> \<proof>
   874   qed
   875 end
   876 
   877 
   878 subsubsection \<open>Example: set-theoretic operators\<close>
   879 
   880 text \<open>There is nothing special about logical connectives (\<open>\<and>\<close>, \<open>\<or>\<close>, \<open>\<forall>\<close>, \<open>\<exists>\<close> etc.).  Operators from
   881   set-theory or lattice-theory work analogously.  It is only a matter
   882   of rule declarations in the library; rules can be also specified
   883   explicitly.
   884 \<close>
   885 
   886 notepad
   887 begin
   888   have "x \<in> A" and "x \<in> B" \<proof>
   889   then have "x \<in> A \<inter> B" ..
   890 
   891   have "x \<in> A" \<proof>
   892   then have "x \<in> A \<union> B" ..
   893 
   894   have "x \<in> B" \<proof>
   895   then have "x \<in> A \<union> B" ..
   896 
   897   have "x \<in> A \<union> B" \<proof>
   898   then have C
   899   proof
   900     assume "x \<in> A"
   901     then show C \<proof>
   902   next
   903     assume "x \<in> B"
   904     then show C \<proof>
   905   qed
   906 
   907 next
   908   have "x \<in> \<Inter>A"
   909   proof
   910     fix a
   911     assume "a \<in> A"
   912     show "x \<in> a" \<proof>
   913   qed
   914 
   915   have "x \<in> \<Inter>A" \<proof>
   916   then have "x \<in> a"
   917   proof
   918     show "a \<in> A" \<proof>
   919   qed
   920 
   921   have "a \<in> A" and "x \<in> a" \<proof>
   922   then have "x \<in> \<Union>A" ..
   923 
   924   have "x \<in> \<Union>A" \<proof>
   925   then obtain a where "a \<in> A" and "x \<in> a" ..
   926 end
   927 
   928 
   929 section \<open>Generalized elimination and cases\<close>
   930 
   931 subsection \<open>General elimination rules\<close>
   932 
   933 text \<open>
   934   The general format of elimination rules is illustrated by the
   935   following typical representatives:
   936 \<close>
   937 
   938 thm exE     \<comment> \<open>local parameter\<close>
   939 thm conjE   \<comment> \<open>local premises\<close>
   940 thm disjE   \<comment> \<open>split into cases\<close>
   941 
   942 text \<open>
   943   Combining these characteristics leads to the following general scheme
   944   for elimination rules with cases:
   945 
   946   \<^item> prefix of assumptions (or ``major premises'')
   947 
   948   \<^item> one or more cases that enable to establish the main conclusion
   949   in an augmented context
   950 \<close>
   951 
   952 notepad
   953 begin
   954   assume r:
   955     "A\<^sub>1 \<Longrightarrow> A\<^sub>2 \<Longrightarrow>  (* assumptions *)
   956       (\<And>x y. B\<^sub>1 x y \<Longrightarrow> C\<^sub>1 x y \<Longrightarrow> R) \<Longrightarrow>  (* case 1 *)
   957       (\<And>x y. B\<^sub>2 x y \<Longrightarrow> C\<^sub>2 x y \<Longrightarrow> R) \<Longrightarrow>  (* case 2 *)
   958       R  (* main conclusion *)"
   959 
   960   have A\<^sub>1 and A\<^sub>2 \<proof>
   961   then have R
   962   proof (rule r)
   963     fix x y
   964     assume "B\<^sub>1 x y" and "C\<^sub>1 x y"
   965     show ?thesis \<proof>
   966   next
   967     fix x y
   968     assume "B\<^sub>2 x y" and "C\<^sub>2 x y"
   969     show ?thesis \<proof>
   970   qed
   971 end
   972 
   973 text \<open>Here \<open>?thesis\<close> is used to refer to the unchanged goal
   974   statement.\<close>
   975 
   976 
   977 subsection \<open>Rules with cases\<close>
   978 
   979 text \<open>
   980   Applying an elimination rule to some goal, leaves that unchanged
   981   but allows to augment the context in the sub-proof of each case.
   982 
   983   Isar provides some infrastructure to support this:
   984 
   985   \<^item> native language elements to state eliminations
   986 
   987   \<^item> symbolic case names
   988 
   989   \<^item> method @{method cases} to recover this structure in a
   990   sub-proof
   991 \<close>
   992 
   993 print_statement exE
   994 print_statement conjE
   995 print_statement disjE
   996 
   997 lemma
   998   assumes A\<^sub>1 and A\<^sub>2  \<comment> \<open>assumptions\<close>
   999   obtains
  1000     (case\<^sub>1)  x y where "B\<^sub>1 x y" and "C\<^sub>1 x y"
  1001   | (case\<^sub>2)  x y where "B\<^sub>2 x y" and "C\<^sub>2 x y"
  1002   \<proof>
  1003 
  1004 
  1005 subsubsection \<open>Example\<close>
  1006 
  1007 lemma tertium_non_datur:
  1008   obtains
  1009     (T)  A
  1010   | (F)  "\<not> A"
  1011   by blast
  1012 
  1013 notepad
  1014 begin
  1015   fix x y :: 'a
  1016   have C
  1017   proof (cases "x = y" rule: tertium_non_datur)
  1018     case T
  1019     from \<open>x = y\<close> show ?thesis \<proof>
  1020   next
  1021     case F
  1022     from \<open>x \<noteq> y\<close> show ?thesis \<proof>
  1023   qed
  1024 end
  1025 
  1026 
  1027 subsubsection \<open>Example\<close>
  1028 
  1029 text \<open>
  1030   Isabelle/HOL specification mechanisms (datatype, inductive, etc.)
  1031   provide suitable derived cases rules.
  1032 \<close>
  1033 
  1034 datatype foo = Foo | Bar foo
  1035 
  1036 notepad
  1037 begin
  1038   fix x :: foo
  1039   have C
  1040   proof (cases x)
  1041     case Foo
  1042     from \<open>x = Foo\<close> show ?thesis \<proof>
  1043   next
  1044     case (Bar a)
  1045     from \<open>x = Bar a\<close> show ?thesis \<proof>
  1046   qed
  1047 end
  1048 
  1049 
  1050 subsection \<open>Elimination statements and case-splitting\<close>
  1051 
  1052 text \<open>
  1053   The @{command consider} states rules for generalized elimination and case
  1054   splitting. This is like a toplevel statement \<^theory_text>\<open>theorem obtains\<close> used within
  1055   a proof body; or like a multi-branch \<^theory_text>\<open>obtain\<close> without activation of the
  1056   local context elements yet.
  1057 
  1058   The proof method @{method cases} is able to use such rules with
  1059   forward-chaining (e.g.\ via \<^theory_text>\<open>then\<close>). This leads to the subsequent pattern
  1060   for case-splitting in a particular situation within a proof.
  1061 \<close>
  1062 
  1063 notepad
  1064 begin
  1065   consider (a) A | (b) B | (c) C
  1066     \<proof>  \<comment> \<open>typically \<^theory_text>\<open>by auto\<close>, \<^theory_text>\<open>by blast\<close> etc.\<close>
  1067   then have something
  1068   proof cases
  1069     case a
  1070     then show ?thesis \<proof>
  1071   next
  1072     case b
  1073     then show ?thesis \<proof>
  1074   next
  1075     case c
  1076     then show ?thesis \<proof>
  1077   qed
  1078 end
  1079 
  1080 subsection \<open>Obtaining local contexts\<close>
  1081 
  1082 text \<open>A single ``case'' branch may be inlined into Isar proof text
  1083   via @{command obtain}.  This proves @{prop "(\<And>x. B x \<Longrightarrow> thesis) \<Longrightarrow>
  1084   thesis"} on the spot, and augments the context afterwards.\<close>
  1085 
  1086 notepad
  1087 begin
  1088   fix B :: "'a \<Rightarrow> bool"
  1089 
  1090   obtain x where "B x" \<proof>
  1091   note \<open>B x\<close>
  1092 
  1093   txt \<open>Conclusions from this context may not mention @{term x} again!\<close>
  1094   {
  1095     obtain x where "B x" \<proof>
  1096     from \<open>B x\<close> have C \<proof>
  1097   }
  1098   note \<open>C\<close>
  1099 end
  1100 
  1101 end