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