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