(*  Title:      HOL/Isar_examples/Peirce.thy

     ID:         $Id$

     Author:     Markus Wenzel, TU Muenchen

 *)

 header {* Peirce's Law *};

 theory Peirce = Main:;

 text {*

  We consider Peirce's Law: $((A \impl B) \impl A) \impl A$.  This is

  an inherently non-intuitionistic statement, so its proof will

  certainly involve some form of classical contradiction.

  The first proof is again a well-balanced combination of plain

  backward and forward reasoning.  The actual classical step is where

  the negated goal may be introduced as additional assumption.  This

  eventually leads to a contradiction.\footnote{The rule involved there

  is negation elimination; it holds in intuitionistic logic as well.}

 *};

 theorem "((A --> B) --> A) --> A";

 proof;

   assume aba: "(A --> B) --> A";

   show A;

   proof (rule classical);

     assume "~ A";

     have "A --> B";

     proof;

       assume A;

       thus B; by contradiction;

     qed;

     with aba; show A; ..;

   qed;

 qed;

 text {*

  In the subsequent version the reasoning is rearranged by means of

  ``weak assumptions'' (as introduced by \isacommand{presume}).  Before

  assuming the negated goal $\neg A$, its intended consequence $A \impl

  B$ is put into place in order to solve the main problem.

  Nevertheless, we do not get anything for free, but have to establish

  $A \impl B$ later on.  The overall effect is that of a logical

  \emph{cut}.

  Technically speaking, whenever some goal is solved by

  \isacommand{show} in the context of weak assumptions then the latter

  give rise to new subgoals, which may be established separately.  In

  contrast, strong assumptions (as introduced by \isacommand{assume})

  are solved immediately.

 *};

 theorem "((A --> B) --> A) --> A";

 proof;

   assume aba: "(A --> B) --> A";

   show A;

   proof (rule classical);

     presume "A --> B";

     with aba; show A; ..;

   next;

     assume "~ A";

     show "A --> B";

     proof;

       assume A;

       thus B; by contradiction;

     qed;

   qed;

 qed;

 text {*

  Note that the goals stemming from weak assumptions may be even left

  until qed time, where they get eventually solved ``by assumption'' as

  well.  In that case there is really no fundamental difference between

  the two kinds of assumptions, apart from the order of reducing the

  individual parts of the proof configuration.

  Nevertheless, the ``strong'' mode of plain assumptions is quite

  important in practice to achieve robustness of proof text

  interpretation.  By forcing both the conclusion \emph{and} the

  assumptions to unify with the pending goal to be solved, goal

  selection becomes quite deterministic.  For example, decomposition

  with rules of the ``case-analysis'' type usually gives rise to

  several goals that only differ in there local contexts.  With strong

  assumptions these may be still solved in any order in a predictable

  way, while weak ones would quickly lead to great confusion,

  eventually demanding even some backtracking.

 *};

 end;