src/HOL/Isar_Examples/Peirce.thy

avoid ligatures;

(*  Title:      HOL/Isar_Examples/Peirce.thy
    Author:     Markus Wenzel, TU Muenchen
*)

section \<open>Peirce's Law\<close>

theory Peirce
imports Main
begin

text \<open>We consider Peirce's Law: \<open>((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A\<close>. 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.}\<close>

theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
proof
  assume "(A \<longrightarrow> B) \<longrightarrow> A"
  show A
  proof (rule classical)
    assume "\<not> A"
    have "A \<longrightarrow> B"
    proof
      assume A
      with \<open>\<not> A\<close> show B by contradiction
    qed
    with \<open>(A \<longrightarrow> B) \<longrightarrow> A\<close> show A ..
  qed
qed

text \<open>In the subsequent version the reasoning is rearranged by means of
  ``weak assumptions'' (as introduced by \isacommand{presume}). Before
  assuming the negated goal \<open>\<not> A\<close>, its intended consequence \<open>A \<longrightarrow> B\<close> is put
  into place in order to solve the main problem. Nevertheless, we do not get
  anything for free, but have to establish \<open>A \<longrightarrow> B\<close> later on. The overall
  effect is that of a logical \<^emph>\<open>cut\<close>.

  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.\<close>

theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
proof
  assume "(A \<longrightarrow> B) \<longrightarrow> A"
  show A
  proof (rule classical)
    presume "A \<longrightarrow> B"
    with \<open>(A \<longrightarrow> B) \<longrightarrow> A\<close> show A ..
  next
    assume "\<not> A"
    show "A \<longrightarrow> B"
    proof
      assume A
      with \<open>\<not> A\<close> show B by contradiction
    qed
  qed
qed

text \<open>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>\<open>and\<close> 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.\<close>

end