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