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