src/Doc/Isar_Ref/Synopsis.thy
 author wenzelm Mon Oct 09 21:12:22 2017 +0200 (23 months ago) changeset 66822 4642cf4a7ebb parent 63680 6e1e8b5abbfa child 67369 7360fe6bb423 permissions -rw-r--r--
tuned signature;
     1 (*:maxLineLen=78:*)

     2

     3 theory Synopsis

     4   imports Main Base

     5 begin

     6

     7 chapter \<open>Synopsis\<close>

     8

     9 section \<open>Notepad\<close>

    10

    11 text \<open>

    12   An Isar proof body serves as mathematical notepad to compose logical

    13   content, consisting of types, terms, facts.

    14 \<close>

    15

    16

    17 subsection \<open>Types and terms\<close>

    18

    19 notepad

    20 begin

    21   txt \<open>Locally fixed entities:\<close>

    22   fix x   \<comment> \<open>local constant, without any type information yet\<close>

    23   fix x :: 'a  \<comment> \<open>variant with explicit type-constraint for subsequent use\<close>

    24

    25   fix a b

    26   assume "a = b"  \<comment> \<open>type assignment at first occurrence in concrete term\<close>

    27

    28   txt \<open>Definitions (non-polymorphic):\<close>

    29   define x :: 'a where "x = t"

    30

    31   txt \<open>Abbreviations (polymorphic):\<close>

    32   let ?f = "\<lambda>x. x"

    33   term "?f ?f"

    34

    35   txt \<open>Notation:\<close>

    36   write x  ("***")

    37 end

    38

    39

    40 subsection \<open>Facts\<close>

    41

    42 text \<open>

    43   A fact is a simultaneous list of theorems.

    44 \<close>

    45

    46

    47 subsubsection \<open>Producing facts\<close>

    48

    49 notepad

    50 begin

    51

    52   txt \<open>Via assumption (lambda''):\<close>

    53   assume a: A

    54

    55   txt \<open>Via proof (let''):\<close>

    56   have b: B \<proof>

    57

    58   txt \<open>Via abbreviation (let''):\<close>

    59   note c = a b

    60

    61 end

    62

    63

    64 subsubsection \<open>Referencing facts\<close>

    65

    66 notepad

    67 begin

    68   txt \<open>Via explicit name:\<close>

    69   assume a: A

    70   note a

    71

    72   txt \<open>Via implicit name:\<close>

    73   assume A

    74   note this

    75

    76   txt \<open>Via literal proposition (unification with results from the proof text):\<close>

    77   assume A

    78   note \<open>A\<close>

    79

    80   assume "\<And>x. B x"

    81   note \<open>B a\<close>

    82   note \<open>B b\<close>

    83 end

    84

    85

    86 subsubsection \<open>Manipulating facts\<close>

    87

    88 notepad

    89 begin

    90   txt \<open>Instantiation:\<close>

    91   assume a: "\<And>x. B x"

    92   note a

    93   note a [of b]

    94   note a [where x = b]

    95

    96   txt \<open>Backchaining:\<close>

    97   assume 1: A

    98   assume 2: "A \<Longrightarrow> C"

    99   note 2 [OF 1]

   100   note 1 [THEN 2]

   101

   102   txt \<open>Symmetric results:\<close>

   103   assume "x = y"

   104   note this [symmetric]

   105

   106   assume "x \<noteq> y"

   107   note this [symmetric]

   108

   109   txt \<open>Adhoc-simplification (take care!):\<close>

   110   assume "P ([] @ xs)"

   111   note this [simplified]

   112 end

   113

   114

   115 subsubsection \<open>Projections\<close>

   116

   117 text \<open>

   118   Isar facts consist of multiple theorems.  There is notation to project

   119   interval ranges.

   120 \<close>

   121

   122 notepad

   123 begin

   124   assume stuff: A B C D

   125   note stuff(1)

   126   note stuff(2-3)

   127   note stuff(2-)

   128 end

   129

   130

   131 subsubsection \<open>Naming conventions\<close>

   132

   133 text \<open>

   134   \<^item> Lower-case identifiers are usually preferred.

   135

   136   \<^item> Facts can be named after the main term within the proposition.

   137

   138   \<^item> Facts should \<^emph>\<open>not\<close> be named after the command that

   139   introduced them (@{command "assume"}, @{command "have"}).  This is

   140   misleading and hard to maintain.

   141

   142   \<^item> Natural numbers can be used as meaningless'' names (more

   143   appropriate than \<open>a1\<close>, \<open>a2\<close> etc.)

   144

   145   \<^item> Symbolic identifiers are supported (e.g. \<open>*\<close>, \<open>**\<close>, \<open>***\<close>).

   146 \<close>

   147

   148

   149 subsection \<open>Block structure\<close>

   150

   151 text \<open>

   152   The formal notepad is block structured.  The fact produced by the last

   153   entry of a block is exported into the outer context.

   154 \<close>

   155

   156 notepad

   157 begin

   158   {

   159     have a: A \<proof>

   160     have b: B \<proof>

   161     note a b

   162   }

   163   note this

   164   note \<open>A\<close>

   165   note \<open>B\<close>

   166 end

   167

   168 text \<open>Explicit blocks as well as implicit blocks of nested goal

   169   statements (e.g.\ @{command have}) automatically introduce one extra

   170   pair of parentheses in reserve.  The @{command next} command allows

   171   to jump'' between these sub-blocks.\<close>

   172

   173 notepad

   174 begin

   175

   176   {

   177     have a: A \<proof>

   178   next

   179     have b: B

   180     proof -

   181       show B \<proof>

   182     next

   183       have c: C \<proof>

   184     next

   185       have d: D \<proof>

   186     qed

   187   }

   188

   189   txt \<open>Alternative version with explicit parentheses everywhere:\<close>

   190

   191   {

   192     {

   193       have a: A \<proof>

   194     }

   195     {

   196       have b: B

   197       proof -

   198         {

   199           show B \<proof>

   200         }

   201         {

   202           have c: C \<proof>

   203         }

   204         {

   205           have d: D \<proof>

   206         }

   207       qed

   208     }

   209   }

   210

   211 end

   212

   213

   214 section \<open>Calculational reasoning \label{sec:calculations-synopsis}\<close>

   215

   216 text \<open>

   217   For example, see \<^file>\<open>~~/src/HOL/Isar_Examples/Group.thy\<close>.

   218 \<close>

   219

   220

   221 subsection \<open>Special names in Isar proofs\<close>

   222

   223 text \<open>

   224   \<^item> term \<open>?thesis\<close> --- the main conclusion of the

   225   innermost pending claim

   226

   227   \<^item> term \<open>\<dots>\<close> --- the argument of the last explicitly

   228   stated result (for infix application this is the right-hand side)

   229

   230   \<^item> fact \<open>this\<close> --- the last result produced in the text

   231 \<close>

   232

   233 notepad

   234 begin

   235   have "x = y"

   236   proof -

   237     term ?thesis

   238     show ?thesis \<proof>

   239     term ?thesis  \<comment> \<open>static!\<close>

   240   qed

   241   term "\<dots>"

   242   thm this

   243 end

   244

   245 text \<open>Calculational reasoning maintains the special fact called

   246   \<open>calculation\<close>'' in the background.  Certain language

   247   elements combine primary \<open>this\<close> with secondary \<open>calculation\<close>.\<close>

   248

   249

   250 subsection \<open>Transitive chains\<close>

   251

   252 text \<open>The Idea is to combine \<open>this\<close> and \<open>calculation\<close>

   253   via typical \<open>trans\<close> rules (see also @{command

   254   print_trans_rules}):\<close>

   255

   256 thm trans

   257 thm less_trans

   258 thm less_le_trans

   259

   260 notepad

   261 begin

   262   txt \<open>Plain bottom-up calculation:\<close>

   263   have "a = b" \<proof>

   264   also

   265   have "b = c" \<proof>

   266   also

   267   have "c = d" \<proof>

   268   finally

   269   have "a = d" .

   270

   271   txt \<open>Variant using the \<open>\<dots>\<close> abbreviation:\<close>

   272   have "a = b" \<proof>

   273   also

   274   have "\<dots> = c" \<proof>

   275   also

   276   have "\<dots> = d" \<proof>

   277   finally

   278   have "a = d" .

   279

   280   txt \<open>Top-down version with explicit claim at the head:\<close>

   281   have "a = d"

   282   proof -

   283     have "a = b" \<proof>

   284     also

   285     have "\<dots> = c" \<proof>

   286     also

   287     have "\<dots> = d" \<proof>

   288     finally

   289     show ?thesis .

   290   qed

   291 next

   292   txt \<open>Mixed inequalities (require suitable base type):\<close>

   293   fix a b c d :: nat

   294

   295   have "a < b" \<proof>

   296   also

   297   have "b \<le> c" \<proof>

   298   also

   299   have "c = d" \<proof>

   300   finally

   301   have "a < d" .

   302 end

   303

   304

   305 subsubsection \<open>Notes\<close>

   306

   307 text \<open>

   308   \<^item> The notion of \<open>trans\<close> rule is very general due to the

   309   flexibility of Isabelle/Pure rule composition.

   310

   311   \<^item> User applications may declare their own rules, with some care

   312   about the operational details of higher-order unification.

   313 \<close>

   314

   315

   316 subsection \<open>Degenerate calculations\<close>

   317

   318 text \<open>The Idea is to append \<open>this\<close> to \<open>calculation\<close>, without rule composition.

   319   This is occasionally useful to avoid naming intermediate facts.\<close>

   320

   321 notepad

   322 begin

   323   txt \<open>A vacuous proof:\<close>

   324   have A \<proof>

   325   moreover

   326   have B \<proof>

   327   moreover

   328   have C \<proof>

   329   ultimately

   330   have A and B and C .

   331 next

   332   txt \<open>Slightly more content (trivial bigstep reasoning):\<close>

   333   have A \<proof>

   334   moreover

   335   have B \<proof>

   336   moreover

   337   have C \<proof>

   338   ultimately

   339   have "A \<and> B \<and> C" by blast

   340 end

   341

   342 text \<open>Note that For multi-branch case splitting, it is better to use @{command

   343   consider}.\<close>

   344

   345

   346 section \<open>Induction\<close>

   347

   348 subsection \<open>Induction as Natural Deduction\<close>

   349

   350 text \<open>In principle, induction is just a special case of Natural

   351   Deduction (see also \secref{sec:natural-deduction-synopsis}).  For

   352   example:\<close>

   353

   354 thm nat.induct

   355 print_statement nat.induct

   356

   357 notepad

   358 begin

   359   fix n :: nat

   360   have "P n"

   361   proof (rule nat.induct)  \<comment> \<open>fragile rule application!\<close>

   362     show "P 0" \<proof>

   363   next

   364     fix n :: nat

   365     assume "P n"

   366     show "P (Suc n)" \<proof>

   367   qed

   368 end

   369

   370 text \<open>

   371   In practice, much more proof infrastructure is required.

   372

   373   The proof method @{method induct} provides:

   374

   375   \<^item> implicit rule selection and robust instantiation

   376

   377   \<^item> context elements via symbolic case names

   378

   379   \<^item> support for rule-structured induction statements, with local

   380   parameters, premises, etc.

   381 \<close>

   382

   383 notepad

   384 begin

   385   fix n :: nat

   386   have "P n"

   387   proof (induct n)

   388     case 0

   389     show ?case \<proof>

   390   next

   391     case (Suc n)

   392     from Suc.hyps show ?case \<proof>

   393   qed

   394 end

   395

   396

   397 subsubsection \<open>Example\<close>

   398

   399 text \<open>

   400   The subsequent example combines the following proof patterns:

   401

   402   \<^item> outermost induction (over the datatype structure of natural

   403   numbers), to decompose the proof problem in top-down manner

   404

   405   \<^item> calculational reasoning (\secref{sec:calculations-synopsis})

   406   to compose the result in each case

   407

   408   \<^item> solving local claims within the calculation by simplification

   409 \<close>

   410

   411 lemma

   412   fixes n :: nat

   413   shows "(\<Sum>i=0..n. i) = n * (n + 1) div 2"

   414 proof (induct n)

   415   case 0

   416   have "(\<Sum>i=0..0. i) = (0::nat)" by simp

   417   also have "\<dots> = 0 * (0 + 1) div 2" by simp

   418   finally show ?case .

   419 next

   420   case (Suc n)

   421   have "(\<Sum>i=0..Suc n. i) = (\<Sum>i=0..n. i) + (n + 1)" by simp

   422   also have "\<dots> = n * (n + 1) div 2 + (n + 1)" by (simp add: Suc.hyps)

   423   also have "\<dots> = (n * (n + 1) + 2 * (n + 1)) div 2" by simp

   424   also have "\<dots> = (Suc n * (Suc n + 1)) div 2" by simp

   425   finally show ?case .

   426 qed

   427

   428 text \<open>This demonstrates how induction proofs can be done without

   429   having to consider the raw Natural Deduction structure.\<close>

   430

   431

   432 subsection \<open>Induction with local parameters and premises\<close>

   433

   434 text \<open>Idea: Pure rule statements are passed through the induction

   435   rule.  This achieves convenient proof patterns, thanks to some

   436   internal trickery in the @{method induct} method.

   437

   438   Important: Using compact HOL formulae with \<open>\<forall>/\<longrightarrow>\<close> is a

   439   well-known anti-pattern! It would produce useless formal noise.

   440 \<close>

   441

   442 notepad

   443 begin

   444   fix n :: nat

   445   fix P :: "nat \<Rightarrow> bool"

   446   fix Q :: "'a \<Rightarrow> nat \<Rightarrow> bool"

   447

   448   have "P n"

   449   proof (induct n)

   450     case 0

   451     show "P 0" \<proof>

   452   next

   453     case (Suc n)

   454     from \<open>P n\<close> show "P (Suc n)" \<proof>

   455   qed

   456

   457   have "A n \<Longrightarrow> P n"

   458   proof (induct n)

   459     case 0

   460     from \<open>A 0\<close> show "P 0" \<proof>

   461   next

   462     case (Suc n)

   463     from \<open>A n \<Longrightarrow> P n\<close>

   464       and \<open>A (Suc n)\<close> show "P (Suc n)" \<proof>

   465   qed

   466

   467   have "\<And>x. Q x n"

   468   proof (induct n)

   469     case 0

   470     show "Q x 0" \<proof>

   471   next

   472     case (Suc n)

   473     from \<open>\<And>x. Q x n\<close> show "Q x (Suc n)" \<proof>

   474     txt \<open>Local quantification admits arbitrary instances:\<close>

   475     note \<open>Q a n\<close> and \<open>Q b n\<close>

   476   qed

   477 end

   478

   479

   480 subsection \<open>Implicit induction context\<close>

   481

   482 text \<open>The @{method induct} method can isolate local parameters and

   483   premises directly from the given statement.  This is convenient in

   484   practical applications, but requires some understanding of what is

   485   going on internally (as explained above).\<close>

   486

   487 notepad

   488 begin

   489   fix n :: nat

   490   fix Q :: "'a \<Rightarrow> nat \<Rightarrow> bool"

   491

   492   fix x :: 'a

   493   assume "A x n"

   494   then have "Q x n"

   495   proof (induct n arbitrary: x)

   496     case 0

   497     from \<open>A x 0\<close> show "Q x 0" \<proof>

   498   next

   499     case (Suc n)

   500     from \<open>\<And>x. A x n \<Longrightarrow> Q x n\<close>  \<comment> \<open>arbitrary instances can be produced here\<close>

   501       and \<open>A x (Suc n)\<close> show "Q x (Suc n)" \<proof>

   502   qed

   503 end

   504

   505

   506 subsection \<open>Advanced induction with term definitions\<close>

   507

   508 text \<open>Induction over subexpressions of a certain shape are delicate

   509   to formalize.  The Isar @{method induct} method provides

   510   infrastructure for this.

   511

   512   Idea: sub-expressions of the problem are turned into a defined

   513   induction variable; often accompanied with fixing of auxiliary

   514   parameters in the original expression.\<close>

   515

   516 notepad

   517 begin

   518   fix a :: "'a \<Rightarrow> nat"

   519   fix A :: "nat \<Rightarrow> bool"

   520

   521   assume "A (a x)"

   522   then have "P (a x)"

   523   proof (induct "a x" arbitrary: x)

   524     case 0

   525     note prem = \<open>A (a x)\<close>

   526       and defn = \<open>0 = a x\<close>

   527     show "P (a x)" \<proof>

   528   next

   529     case (Suc n)

   530     note hyp = \<open>\<And>x. n = a x \<Longrightarrow> A (a x) \<Longrightarrow> P (a x)\<close>

   531       and prem = \<open>A (a x)\<close>

   532       and defn = \<open>Suc n = a x\<close>

   533     show "P (a x)" \<proof>

   534   qed

   535 end

   536

   537

   538 section \<open>Natural Deduction \label{sec:natural-deduction-synopsis}\<close>

   539

   540 subsection \<open>Rule statements\<close>

   541

   542 text \<open>

   543   Isabelle/Pure theorems'' are always natural deduction rules,

   544   which sometimes happen to consist of a conclusion only.

   545

   546   The framework connectives \<open>\<And>\<close> and \<open>\<Longrightarrow>\<close> indicate the

   547   rule structure declaratively.  For example:\<close>

   548

   549 thm conjI

   550 thm impI

   551 thm nat.induct

   552

   553 text \<open>

   554   The object-logic is embedded into the Pure framework via an implicit

   555   derivability judgment @{term "Trueprop :: bool \<Rightarrow> prop"}.

   556

   557   Thus any HOL formulae appears atomic to the Pure framework, while

   558   the rule structure outlines the corresponding proof pattern.

   559

   560   This can be made explicit as follows:

   561 \<close>

   562

   563 notepad

   564 begin

   565   write Trueprop  ("Tr")

   566

   567   thm conjI

   568   thm impI

   569   thm nat.induct

   570 end

   571

   572 text \<open>

   573   Isar provides first-class notation for rule statements as follows.

   574 \<close>

   575

   576 print_statement conjI

   577 print_statement impI

   578 print_statement nat.induct

   579

   580

   581 subsubsection \<open>Examples\<close>

   582

   583 text \<open>

   584   Introductions and eliminations of some standard connectives of

   585   the object-logic can be written as rule statements as follows.  (The

   586   proof @{command "by"}~@{method blast}'' serves as sanity check.)

   587 \<close>

   588

   589 lemma "(P \<Longrightarrow> False) \<Longrightarrow> \<not> P" by blast

   590 lemma "\<not> P \<Longrightarrow> P \<Longrightarrow> Q" by blast

   591

   592 lemma "P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q" by blast

   593 lemma "P \<and> Q \<Longrightarrow> (P \<Longrightarrow> Q \<Longrightarrow> R) \<Longrightarrow> R" by blast

   594

   595 lemma "P \<Longrightarrow> P \<or> Q" by blast

   596 lemma "Q \<Longrightarrow> P \<or> Q" by blast

   597 lemma "P \<or> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R" by blast

   598

   599 lemma "(\<And>x. P x) \<Longrightarrow> (\<forall>x. P x)" by blast

   600 lemma "(\<forall>x. P x) \<Longrightarrow> P x" by blast

   601

   602 lemma "P x \<Longrightarrow> (\<exists>x. P x)" by blast

   603 lemma "(\<exists>x. P x) \<Longrightarrow> (\<And>x. P x \<Longrightarrow> R) \<Longrightarrow> R" by blast

   604

   605 lemma "x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A \<inter> B" by blast

   606 lemma "x \<in> A \<inter> B \<Longrightarrow> (x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> R) \<Longrightarrow> R" by blast

   607

   608 lemma "x \<in> A \<Longrightarrow> x \<in> A \<union> B" by blast

   609 lemma "x \<in> B \<Longrightarrow> x \<in> A \<union> B" by blast

   610 lemma "x \<in> A \<union> B \<Longrightarrow> (x \<in> A \<Longrightarrow> R) \<Longrightarrow> (x \<in> B \<Longrightarrow> R) \<Longrightarrow> R" by blast

   611

   612

   613 subsection \<open>Isar context elements\<close>

   614

   615 text \<open>We derive some results out of the blue, using Isar context

   616   elements and some explicit blocks.  This illustrates their meaning

   617   wrt.\ Pure connectives, without goal states getting in the way.\<close>

   618

   619 notepad

   620 begin

   621   {

   622     fix x

   623     have "B x" \<proof>

   624   }

   625   have "\<And>x. B x" by fact

   626

   627 next

   628

   629   {

   630     assume A

   631     have B \<proof>

   632   }

   633   have "A \<Longrightarrow> B" by fact

   634

   635 next

   636

   637   {

   638     define x where "x = t"

   639     have "B x" \<proof>

   640   }

   641   have "B t" by fact

   642

   643 next

   644

   645   {

   646     obtain x :: 'a where "B x" \<proof>

   647     have C \<proof>

   648   }

   649   have C by fact

   650

   651 end

   652

   653

   654 subsection \<open>Pure rule composition\<close>

   655

   656 text \<open>

   657   The Pure framework provides means for:

   658

   659   \<^item> backward-chaining of rules by @{inference resolution}

   660

   661   \<^item> closing of branches by @{inference assumption}

   662

   663

   664   Both principles involve higher-order unification of \<open>\<lambda>\<close>-terms

   665   modulo \<open>\<alpha>\<beta>\<eta>\<close>-equivalence (cf.\ Huet and Miller).

   666 \<close>

   667

   668 notepad

   669 begin

   670   assume a: A and b: B

   671   thm conjI

   672   thm conjI [of A B]  \<comment> "instantiation"

   673   thm conjI [of A B, OF a b]  \<comment> "instantiation and composition"

   674   thm conjI [OF a b]  \<comment> "composition via unification (trivial)"

   675   thm conjI [OF \<open>A\<close> \<open>B\<close>]

   676

   677   thm conjI [OF disjI1]

   678 end

   679

   680 text \<open>Note: Low-level rule composition is tedious and leads to

   681   unreadable~/ unmaintainable expressions in the text.\<close>

   682

   683

   684 subsection \<open>Structured backward reasoning\<close>

   685

   686 text \<open>Idea: Canonical proof decomposition via @{command fix}~/

   687   @{command assume}~/ @{command show}, where the body produces a

   688   natural deduction rule to refine some goal.\<close>

   689

   690 notepad

   691 begin

   692   fix A B :: "'a \<Rightarrow> bool"

   693

   694   have "\<And>x. A x \<Longrightarrow> B x"

   695   proof -

   696     fix x

   697     assume "A x"

   698     show "B x" \<proof>

   699   qed

   700

   701   have "\<And>x. A x \<Longrightarrow> B x"

   702   proof -

   703     {

   704       fix x

   705       assume "A x"

   706       show "B x" \<proof>

   707     } \<comment> "implicit block structure made explicit"

   708     note \<open>\<And>x. A x \<Longrightarrow> B x\<close>

   709       \<comment> "side exit for the resulting rule"

   710   qed

   711 end

   712

   713

   714 subsection \<open>Structured rule application\<close>

   715

   716 text \<open>

   717   Idea: Previous facts and new claims are composed with a rule from

   718   the context (or background library).

   719 \<close>

   720

   721 notepad

   722 begin

   723   assume r\<^sub>1: "A \<Longrightarrow> B \<Longrightarrow> C"  \<comment> \<open>simple rule (Horn clause)\<close>

   724

   725   have A \<proof>  \<comment> "prefix of facts via outer sub-proof"

   726   then have C

   727   proof (rule r\<^sub>1)

   728     show B \<proof>  \<comment> "remaining rule premises via inner sub-proof"

   729   qed

   730

   731   have C

   732   proof (rule r\<^sub>1)

   733     show A \<proof>

   734     show B \<proof>

   735   qed

   736

   737   have A and B \<proof>

   738   then have C

   739   proof (rule r\<^sub>1)

   740   qed

   741

   742   have A and B \<proof>

   743   then have C by (rule r\<^sub>1)

   744

   745 next

   746

   747   assume r\<^sub>2: "A \<Longrightarrow> (\<And>x. B\<^sub>1 x \<Longrightarrow> B\<^sub>2 x) \<Longrightarrow> C"  \<comment> \<open>nested rule\<close>

   748

   749   have A \<proof>

   750   then have C

   751   proof (rule r\<^sub>2)

   752     fix x

   753     assume "B\<^sub>1 x"

   754     show "B\<^sub>2 x" \<proof>

   755   qed

   756

   757   txt \<open>The compound rule premise @{prop "\<And>x. B\<^sub>1 x \<Longrightarrow> B\<^sub>2 x"} is better

   758     addressed via @{command fix}~/ @{command assume}~/ @{command show}

   759     in the nested proof body.\<close>

   760 end

   761

   762

   763 subsection \<open>Example: predicate logic\<close>

   764

   765 text \<open>

   766   Using the above principles, standard introduction and elimination proofs

   767   of predicate logic connectives of HOL work as follows.

   768 \<close>

   769

   770 notepad

   771 begin

   772   have "A \<longrightarrow> B" and A \<proof>

   773   then have B ..

   774

   775   have A \<proof>

   776   then have "A \<or> B" ..

   777

   778   have B \<proof>

   779   then have "A \<or> B" ..

   780

   781   have "A \<or> B" \<proof>

   782   then have C

   783   proof

   784     assume A

   785     then show C \<proof>

   786   next

   787     assume B

   788     then show C \<proof>

   789   qed

   790

   791   have A and B \<proof>

   792   then have "A \<and> B" ..

   793

   794   have "A \<and> B" \<proof>

   795   then have A ..

   796

   797   have "A \<and> B" \<proof>

   798   then have B ..

   799

   800   have False \<proof>

   801   then have A ..

   802

   803   have True ..

   804

   805   have "\<not> A"

   806   proof

   807     assume A

   808     then show False \<proof>

   809   qed

   810

   811   have "\<not> A" and A \<proof>

   812   then have B ..

   813

   814   have "\<forall>x. P x"

   815   proof

   816     fix x

   817     show "P x" \<proof>

   818   qed

   819

   820   have "\<forall>x. P x" \<proof>

   821   then have "P a" ..

   822

   823   have "\<exists>x. P x"

   824   proof

   825     show "P a" \<proof>

   826   qed

   827

   828   have "\<exists>x. P x" \<proof>

   829   then have C

   830   proof

   831     fix a

   832     assume "P a"

   833     show C \<proof>

   834   qed

   835

   836   txt \<open>Less awkward version using @{command obtain}:\<close>

   837   have "\<exists>x. P x" \<proof>

   838   then obtain a where "P a" ..

   839 end

   840

   841 text \<open>Further variations to illustrate Isar sub-proofs involving

   842   @{command show}:\<close>

   843

   844 notepad

   845 begin

   846   have "A \<and> B"

   847   proof  \<comment> \<open>two strictly isolated subproofs\<close>

   848     show A \<proof>

   849   next

   850     show B \<proof>

   851   qed

   852

   853   have "A \<and> B"

   854   proof  \<comment> \<open>one simultaneous sub-proof\<close>

   855     show A and B \<proof>

   856   qed

   857

   858   have "A \<and> B"

   859   proof  \<comment> \<open>two subproofs in the same context\<close>

   860     show A \<proof>

   861     show B \<proof>

   862   qed

   863

   864   have "A \<and> B"

   865   proof  \<comment> \<open>swapped order\<close>

   866     show B \<proof>

   867     show A \<proof>

   868   qed

   869

   870   have "A \<and> B"

   871   proof  \<comment> \<open>sequential subproofs\<close>

   872     show A \<proof>

   873     show B using \<open>A\<close> \<proof>

   874   qed

   875 end

   876

   877

   878 subsubsection \<open>Example: set-theoretic operators\<close>

   879

   880 text \<open>There is nothing special about logical connectives (\<open>\<and>\<close>, \<open>\<or>\<close>, \<open>\<forall>\<close>, \<open>\<exists>\<close> etc.).  Operators from

   881   set-theory or lattice-theory work analogously.  It is only a matter

   882   of rule declarations in the library; rules can be also specified

   883   explicitly.

   884 \<close>

   885

   886 notepad

   887 begin

   888   have "x \<in> A" and "x \<in> B" \<proof>

   889   then have "x \<in> A \<inter> B" ..

   890

   891   have "x \<in> A" \<proof>

   892   then have "x \<in> A \<union> B" ..

   893

   894   have "x \<in> B" \<proof>

   895   then have "x \<in> A \<union> B" ..

   896

   897   have "x \<in> A \<union> B" \<proof>

   898   then have C

   899   proof

   900     assume "x \<in> A"

   901     then show C \<proof>

   902   next

   903     assume "x \<in> B"

   904     then show C \<proof>

   905   qed

   906

   907 next

   908   have "x \<in> \<Inter>A"

   909   proof

   910     fix a

   911     assume "a \<in> A"

   912     show "x \<in> a" \<proof>

   913   qed

   914

   915   have "x \<in> \<Inter>A" \<proof>

   916   then have "x \<in> a"

   917   proof

   918     show "a \<in> A" \<proof>

   919   qed

   920

   921   have "a \<in> A" and "x \<in> a" \<proof>

   922   then have "x \<in> \<Union>A" ..

   923

   924   have "x \<in> \<Union>A" \<proof>

   925   then obtain a where "a \<in> A" and "x \<in> a" ..

   926 end

   927

   928

   929 section \<open>Generalized elimination and cases\<close>

   930

   931 subsection \<open>General elimination rules\<close>

   932

   933 text \<open>

   934   The general format of elimination rules is illustrated by the

   935   following typical representatives:

   936 \<close>

   937

   938 thm exE     \<comment> \<open>local parameter\<close>

   939 thm conjE   \<comment> \<open>local premises\<close>

   940 thm disjE   \<comment> \<open>split into cases\<close>

   941

   942 text \<open>

   943   Combining these characteristics leads to the following general scheme

   944   for elimination rules with cases:

   945

   946   \<^item> prefix of assumptions (or major premises'')

   947

   948   \<^item> one or more cases that enable to establish the main conclusion

   949   in an augmented context

   950 \<close>

   951

   952 notepad

   953 begin

   954   assume r:

   955     "A\<^sub>1 \<Longrightarrow> A\<^sub>2 \<Longrightarrow>  (* assumptions *)

   956       (\<And>x y. B\<^sub>1 x y \<Longrightarrow> C\<^sub>1 x y \<Longrightarrow> R) \<Longrightarrow>  (* case 1 *)

   957       (\<And>x y. B\<^sub>2 x y \<Longrightarrow> C\<^sub>2 x y \<Longrightarrow> R) \<Longrightarrow>  (* case 2 *)

   958       R  (* main conclusion *)"

   959

   960   have A\<^sub>1 and A\<^sub>2 \<proof>

   961   then have R

   962   proof (rule r)

   963     fix x y

   964     assume "B\<^sub>1 x y" and "C\<^sub>1 x y"

   965     show ?thesis \<proof>

   966   next

   967     fix x y

   968     assume "B\<^sub>2 x y" and "C\<^sub>2 x y"

   969     show ?thesis \<proof>

   970   qed

   971 end

   972

   973 text \<open>Here \<open>?thesis\<close> is used to refer to the unchanged goal

   974   statement.\<close>

   975

   976

   977 subsection \<open>Rules with cases\<close>

   978

   979 text \<open>

   980   Applying an elimination rule to some goal, leaves that unchanged

   981   but allows to augment the context in the sub-proof of each case.

   982

   983   Isar provides some infrastructure to support this:

   984

   985   \<^item> native language elements to state eliminations

   986

   987   \<^item> symbolic case names

   988

   989   \<^item> method @{method cases} to recover this structure in a

   990   sub-proof

   991 \<close>

   992

   993 print_statement exE

   994 print_statement conjE

   995 print_statement disjE

   996

   997 lemma

   998   assumes A\<^sub>1 and A\<^sub>2  \<comment> \<open>assumptions\<close>

   999   obtains

  1000     (case\<^sub>1)  x y where "B\<^sub>1 x y" and "C\<^sub>1 x y"

  1001   | (case\<^sub>2)  x y where "B\<^sub>2 x y" and "C\<^sub>2 x y"

  1002   \<proof>

  1003

  1004

  1005 subsubsection \<open>Example\<close>

  1006

  1007 lemma tertium_non_datur:

  1008   obtains

  1009     (T)  A

  1010   | (F)  "\<not> A"

  1011   by blast

  1012

  1013 notepad

  1014 begin

  1015   fix x y :: 'a

  1016   have C

  1017   proof (cases "x = y" rule: tertium_non_datur)

  1018     case T

  1019     from \<open>x = y\<close> show ?thesis \<proof>

  1020   next

  1021     case F

  1022     from \<open>x \<noteq> y\<close> show ?thesis \<proof>

  1023   qed

  1024 end

  1025

  1026

  1027 subsubsection \<open>Example\<close>

  1028

  1029 text \<open>

  1030   Isabelle/HOL specification mechanisms (datatype, inductive, etc.)

  1031   provide suitable derived cases rules.

  1032 \<close>

  1033

  1034 datatype foo = Foo | Bar foo

  1035

  1036 notepad

  1037 begin

  1038   fix x :: foo

  1039   have C

  1040   proof (cases x)

  1041     case Foo

  1042     from \<open>x = Foo\<close> show ?thesis \<proof>

  1043   next

  1044     case (Bar a)

  1045     from \<open>x = Bar a\<close> show ?thesis \<proof>

  1046   qed

  1047 end

  1048

  1049

  1050 subsection \<open>Elimination statements and case-splitting\<close>

  1051

  1052 text \<open>

  1053   The @{command consider} states rules for generalized elimination and case

  1054   splitting. This is like a toplevel statement \<^theory_text>\<open>theorem obtains\<close> used within

  1055   a proof body; or like a multi-branch \<^theory_text>\<open>obtain\<close> without activation of the

  1056   local context elements yet.

  1057

  1058   The proof method @{method cases} is able to use such rules with

  1059   forward-chaining (e.g.\ via \<^theory_text>\<open>then\<close>). This leads to the subsequent pattern

  1060   for case-splitting in a particular situation within a proof.

  1061 \<close>

  1062

  1063 notepad

  1064 begin

  1065   consider (a) A | (b) B | (c) C

  1066     \<proof>  \<comment> \<open>typically \<^theory_text>\<open>by auto\<close>, \<^theory_text>\<open>by blast\<close> etc.\<close>

  1067   then have something

  1068   proof cases

  1069     case a

  1070     then show ?thesis \<proof>

  1071   next

  1072     case b

  1073     then show ?thesis \<proof>

  1074   next

  1075     case c

  1076     then show ?thesis \<proof>

  1077   qed

  1078 end

  1079

  1080 subsection \<open>Obtaining local contexts\<close>

  1081

  1082 text \<open>A single case'' branch may be inlined into Isar proof text

  1083   via @{command obtain}.  This proves @{prop "(\<And>x. B x \<Longrightarrow> thesis) \<Longrightarrow>

  1084   thesis"} on the spot, and augments the context afterwards.\<close>

  1085

  1086 notepad

  1087 begin

  1088   fix B :: "'a \<Rightarrow> bool"

  1089

  1090   obtain x where "B x" \<proof>

  1091   note \<open>B x\<close>

  1092

  1093   txt \<open>Conclusions from this context may not mention @{term x} again!\<close>

  1094   {

  1095     obtain x where "B x" \<proof>

  1096     from \<open>B x\<close> have C \<proof>

  1097   }

  1098   note \<open>C\<close>

  1099 end

  1100

  1101 end