Theory Intuitionistic

(*  Title:      FOL/ex/Intuitionistic.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1991  University of Cambridge
*)

section ‹Intuitionistic First-Order Logic›

theory Intuitionistic
imports IFOL
begin

(*
Single-step ML commands:
by (IntPr.step_tac 1)
by (biresolve_tac safe_brls 1);
by (biresolve_tac haz_brls 1);
by (assume_tac 1);
by (IntPr.safe_tac 1);
by (IntPr.mp_tac 1);
by (IntPr.fast_tac @{context} 1);
*)


text‹Metatheorem (for \emph{propositional} formulae):
  $P$ is classically provable iff $\neg\neg P$ is intuitionistically provable.
  Therefore $\neg P$ is classically provable iff it is intuitionistically
  provable.

Proof: Let $Q$ be the conjunction of the propositions $A\vee\neg A$, one for
each atom $A$ in $P$.  Now $\neg\neg Q$ is intuitionistically provable because
$\neg\neg(A\vee\neg A)$ is and because double-negation distributes over
conjunction.  If $P$ is provable classically, then clearly $Q\rightarrow P$ is
provable intuitionistically, so $\neg\neg(Q\rightarrow P)$ is also provable
intuitionistically.  The latter is intuitionistically equivalent to $\neg\neg
Q\rightarrow\neg\neg P$, hence to $\neg\neg P$, since $\neg\neg Q$ is
intuitionistically provable.  Finally, if $P$ is a negation then $\neg\neg P$
is intuitionstically equivalent to $P$.  [Andy Pitts]›

lemma ‹¬ ¬ (P ∧ Q) ⟷ ¬ ¬ P ∧ ¬ ¬ Q›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

lemma ‹¬ ¬ ((¬ P ⟶ Q) ⟶ (¬ P ⟶ ¬ Q) ⟶ P)›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text ‹Double-negation does NOT distribute over disjunction.›

lemma ‹¬ ¬ (P ⟶ Q) ⟷ (¬ ¬ P ⟶ ¬ ¬ Q)›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

lemma ‹¬ ¬ ¬ P ⟷ ¬ P›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

lemma ‹¬ ¬ ((P ⟶ Q ∨ R) ⟶ (P ⟶ Q) ∨ (P ⟶ R))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

lemma ‹(P ⟷ Q) ⟷ (Q ⟷ P)›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

lemma ‹((P ⟶ (Q ∨ (Q ⟶ R))) ⟶ R) ⟶ R›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

lemma
  ‹(((G ⟶ A) ⟶ J) ⟶ D ⟶ E) ⟶ (((H ⟶ B) ⟶ I) ⟶ C ⟶ J)
    ⟶ (A ⟶ H) ⟶ F ⟶ G ⟶ (((C ⟶ B) ⟶ I) ⟶ D) ⟶ (A ⟶ C)
    ⟶ (((F ⟶ A) ⟶ B) ⟶ I) ⟶ E›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)


subsection ‹Lemmas for the propositional double-negation translation›

lemma ‹P ⟶ ¬ ¬ P›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

lemma ‹¬ ¬ (¬ ¬ P ⟶ P)›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

lemma ‹¬ ¬ P ∧ ¬ ¬ (P ⟶ Q) ⟶ ¬ ¬ Q›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)


text ‹The following are classically but not constructively valid.
  The attempt to prove them terminates quickly!›
lemma ‹((P ⟶ Q) ⟶ P) ⟶ P›
apply (tactic ‹IntPr.fast_tac \<^context> 1›)?
apply (rule asm_rl) ― ‹Checks that subgoals remain: proof failed.›
oops

lemma ‹(P ∧ Q ⟶ R) ⟶ (P ⟶ R) ∨ (Q ⟶ R)›
apply (tactic ‹IntPr.fast_tac \<^context> 1›)?
apply (rule asm_rl) ― ‹Checks that subgoals remain: proof failed.›
oops


subsection ‹de Bruijn formulae›

text ‹de Bruijn formula with three predicates›
lemma
  ‹((P ⟷ Q) ⟶ P ∧ Q ∧ R) ∧
    ((Q ⟷ R) ⟶ P ∧ Q ∧ R) ∧
    ((R ⟷ P) ⟶ P ∧ Q ∧ R) ⟶ P ∧ Q ∧ R›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)


text ‹de Bruijn formula with five predicates›
lemma
  ‹((P ⟷ Q) ⟶ P ∧ Q ∧ R ∧ S ∧ T) ∧
    ((Q ⟷ R) ⟶ P ∧ Q ∧ R ∧ S ∧ T) ∧
    ((R ⟷ S) ⟶ P ∧ Q ∧ R ∧ S ∧ T) ∧
    ((S ⟷ T) ⟶ P ∧ Q ∧ R ∧ S ∧ T) ∧
    ((T ⟷ P) ⟶ P ∧ Q ∧ R ∧ S ∧ T) ⟶ P ∧ Q ∧ R ∧ S ∧ T›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)


text ‹
  Problems from of Sahlin, Franzen and Haridi,
  An Intuitionistic Predicate Logic Theorem Prover.
  J. Logic and Comp. 2 (5), October 1992, 619-656.
›

text‹Problem 1.1›
lemma
  ‹(∀x. ∃y. ∀z. p(x) ∧ q(y) ∧ r(z)) ⟷
    (∀z. ∃y. ∀x. p(x) ∧ q(y) ∧ r(z))›
  by (tactic ‹IntPr.best_dup_tac \<^context> 1›)  ― ‹SLOW›

text‹Problem 3.1›
lemma ‹¬ (∃x. ∀y. mem(y,x) ⟷ ¬ mem(x,x))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹Problem 4.1: hopeless!›
lemma
  ‹(∀x. p(x) ⟶ p(h(x)) ∨ p(g(x))) ∧ (∃x. p(x)) ∧ (∀x. ¬ p(h(x)))
    ⟶ (∃x. p(g(g(g(g(g(x)))))))›
  oops


subsection ‹Intuitionistic FOL: propositional problems based on Pelletier.›

text‹‹¬¬›1›
lemma ‹¬ ¬ ((P ⟶ Q) ⟷ (¬ Q ⟶ ¬ P))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹‹¬¬›2›
lemma ‹¬ ¬ (¬ ¬ P ⟷ P)›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹3›
lemma ‹¬ (P ⟶ Q) ⟶ (Q ⟶ P)›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹‹¬¬›4›
lemma ‹¬ ¬ ((¬ P ⟶ Q) ⟷ (¬ Q ⟶ P))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹‹¬¬›5›
lemma ‹¬ ¬ ((P ∨ Q ⟶ P ∨ R) ⟶ P ∨ (Q ⟶ R))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹‹¬¬›6›
lemma ‹¬ ¬ (P ∨ ¬ P)›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹‹¬¬›7›
lemma ‹¬ ¬ (P ∨ ¬ ¬ ¬ P)›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹‹¬¬›8. Peirce's law›
lemma ‹¬ ¬ (((P ⟶ Q) ⟶ P) ⟶ P)›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹9›
lemma ‹((P ∨ Q) ∧ (¬ P ∨ Q) ∧ (P ∨ ¬ Q)) ⟶ ¬ (¬ P ∨ ¬ Q)›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹10›
lemma ‹(Q ⟶ R) ⟶ (R ⟶ P ∧ Q) ⟶ (P ⟶ (Q ∨ R)) ⟶ (P ⟷ Q)›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)


subsection‹11. Proved in each direction (incorrectly, says Pelletier!!)›

lemma ‹P ⟷ P›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹‹¬¬›12. Dijkstra's law›
lemma ‹¬ ¬ (((P ⟷ Q) ⟷ R) ⟷ (P ⟷ (Q ⟷ R)))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

lemma ‹((P ⟷ Q) ⟷ R) ⟶ ¬ ¬ (P ⟷ (Q ⟷ R))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹13. Distributive law›
lemma ‹P ∨ (Q ∧ R) ⟷ (P ∨ Q) ∧ (P ∨ R)›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹‹¬¬›14›
lemma ‹¬ ¬ ((P ⟷ Q) ⟷ ((Q ∨ ¬ P) ∧ (¬ Q ∨ P)))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹‹¬¬›15›
lemma ‹¬ ¬ ((P ⟶ Q) ⟷ (¬ P ∨ Q))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹‹¬¬›16›
lemma ‹¬ ¬ ((P ⟶ Q) ∨ (Q ⟶ P))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹‹¬¬›17›
lemma ‹¬ ¬ (((P ∧ (Q ⟶ R)) ⟶ S) ⟷ ((¬ P ∨ Q ∨ S) ∧ (¬ P ∨ ¬ R ∨ S)))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text ‹Dijkstra's ``Golden Rule''›
lemma ‹(P ∧ Q) ⟷ P ⟷ Q ⟷ (P ∨ Q)›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)


section ‹Examples with quantifiers›

subsection ‹The converse is classical in the following implications \dots›

lemma ‹(∃x. P(x) ⟶ Q) ⟶ (∀x. P(x)) ⟶ Q›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

lemma ‹((∀x. P(x)) ⟶ Q) ⟶ ¬ (∀x. P(x) ∧ ¬ Q)›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

lemma ‹((∀x. ¬ P(x)) ⟶ Q) ⟶ ¬ (∀x. ¬ (P(x) ∨ Q))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

lemma ‹(∀x. P(x)) ∨ Q ⟶ (∀x. P(x) ∨ Q)›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

lemma ‹(∃x. P ⟶ Q(x)) ⟶ (P ⟶ (∃x. Q(x)))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)


subsection ‹The following are not constructively valid!›
text ‹The attempt to prove them terminates quickly!›

lemma ‹((∀x. P(x)) ⟶ Q) ⟶ (∃x. P(x) ⟶ Q)›
  apply (tactic ‹IntPr.fast_tac \<^context> 1›)?
  apply (rule asm_rl) ― ‹Checks that subgoals remain: proof failed.›
  oops

lemma ‹(P ⟶ (∃x. Q(x))) ⟶ (∃x. P ⟶ Q(x))›
  apply (tactic ‹IntPr.fast_tac \<^context> 1›)?
  apply (rule asm_rl) ― ‹Checks that subgoals remain: proof failed.›
  oops

lemma ‹(∀x. P(x) ∨ Q) ⟶ ((∀x. P(x)) ∨ Q)›
  apply (tactic ‹IntPr.fast_tac \<^context> 1›)?
  apply (rule asm_rl) ― ‹Checks that subgoals remain: proof failed.›
  oops

lemma ‹(∀x. ¬ ¬ P(x)) ⟶ ¬ ¬ (∀x. P(x))›
  apply (tactic ‹IntPr.fast_tac \<^context> 1›)?
  apply (rule asm_rl) ― ‹Checks that subgoals remain: proof failed.›
  oops

text ‹Classically but not intuitionistically valid.  Proved by a bug in 1986!›
lemma ‹∃x. Q(x) ⟶ (∀x. Q(x))›
  apply (tactic ‹IntPr.fast_tac \<^context> 1›)?
  apply (rule asm_rl) ― ‹Checks that subgoals remain: proof failed.›
  oops


subsection ‹Hard examples with quantifiers›

text ‹
  The ones that have not been proved are not known to be valid! Some will
  require quantifier duplication -- not currently available.
›

text‹‹¬¬›18›
lemma ‹¬ ¬ (∃y. ∀x. P(y) ⟶ P(x))›
  oops  ― ‹NOT PROVED›

text‹‹¬¬›19›
lemma ‹¬ ¬ (∃x. ∀y z. (P(y) ⟶ Q(z)) ⟶ (P(x) ⟶ Q(x)))›
  oops  ― ‹NOT PROVED›

text‹20›
lemma
  ‹(∀x y. ∃z. ∀w. (P(x) ∧ Q(y) ⟶ R(z) ∧ S(w)))
    ⟶ (∃x y. P(x) ∧ Q(y)) ⟶ (∃z. R(z))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹21›
lemma ‹(∃x. P ⟶ Q(x)) ∧ (∃x. Q(x) ⟶ P) ⟶ ¬ ¬ (∃x. P ⟷ Q(x))›
  oops ― ‹NOT PROVED; needs quantifier duplication›

text‹22›
lemma ‹(∀x. P ⟷ Q(x)) ⟶ (P ⟷ (∀x. Q(x)))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹‹¬¬›23›
lemma ‹¬ ¬ ((∀x. P ∨ Q(x)) ⟷ (P ∨ (∀x. Q(x))))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹24›
lemma
  ‹¬ (∃x. S(x) ∧ Q(x)) ∧ (∀x. P(x) ⟶ Q(x) ∨ R(x)) ∧
    (¬ (∃x. P(x)) ⟶ (∃x. Q(x))) ∧ (∀x. Q(x) ∨ R(x) ⟶ S(x))
    ⟶ ¬ ¬ (∃x. P(x) ∧ R(x))›
text ‹
  Not clear why ‹fast_tac›, ‹best_tac›, ‹ASTAR› and
  ‹ITER_DEEPEN› all take forever.
›
  apply (tactic ‹IntPr.safe_tac \<^context>›)
  apply (erule impE)
  apply (tactic ‹IntPr.fast_tac \<^context> 1›)
  apply (tactic ‹IntPr.fast_tac \<^context> 1›)
  done

text‹25›
lemma
  ‹(∃x. P(x)) ∧
      (∀x. L(x) ⟶ ¬ (M(x) ∧ R(x))) ∧
      (∀x. P(x) ⟶ (M(x) ∧ L(x))) ∧
      ((∀x. P(x) ⟶ Q(x)) ∨ (∃x. P(x) ∧ R(x)))
    ⟶ (∃x. Q(x) ∧ P(x))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹‹¬¬›26›
lemma
  ‹(¬ ¬ (∃x. p(x)) ⟷ ¬ ¬ (∃x. q(x))) ∧
    (∀x. ∀y. p(x) ∧ q(y) ⟶ (r(x) ⟷ s(y)))
  ⟶ ((∀x. p(x) ⟶ r(x)) ⟷ (∀x. q(x) ⟶ s(x)))›
  oops  ― ‹NOT PROVED›

text‹27›
lemma
  ‹(∃x. P(x) ∧ ¬ Q(x)) ∧
    (∀x. P(x) ⟶ R(x)) ∧
    (∀x. M(x) ∧ L(x) ⟶ P(x)) ∧
    ((∃x. R(x) ∧ ¬ Q(x)) ⟶ (∀x. L(x) ⟶ ¬ R(x)))
  ⟶ (∀x. M(x) ⟶ ¬ L(x))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹‹¬¬›28. AMENDED›
lemma
  ‹(∀x. P(x) ⟶ (∀x. Q(x))) ∧
      (¬ ¬ (∀x. Q(x) ∨ R(x)) ⟶ (∃x. Q(x) ∧ S(x))) ∧
      (¬ ¬ (∃x. S(x)) ⟶ (∀x. L(x) ⟶ M(x)))
    ⟶ (∀x. P(x) ∧ L(x) ⟶ M(x))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹29. Essentially the same as Principia Mathematica *11.71›
lemma
  ‹(∃x. P(x)) ∧ (∃y. Q(y))
    ⟶ ((∀x. P(x) ⟶ R(x)) ∧ (∀y. Q(y) ⟶ S(y)) ⟷
      (∀x y. P(x) ∧ Q(y) ⟶ R(x) ∧ S(y)))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹‹¬¬›30›
lemma
  ‹(∀x. (P(x) ∨ Q(x)) ⟶ ¬ R(x)) ∧
      (∀x. (Q(x) ⟶ ¬ S(x)) ⟶ P(x) ∧ R(x))
    ⟶ (∀x. ¬ ¬ S(x))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹31›
lemma
  ‹¬ (∃x. P(x) ∧ (Q(x) ∨ R(x))) ∧
      (∃x. L(x) ∧ P(x)) ∧
      (∀x. ¬ R(x) ⟶ M(x))
  ⟶ (∃x. L(x) ∧ M(x))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹32›
lemma
  ‹(∀x. P(x) ∧ (Q(x) ∨ R(x)) ⟶ S(x)) ∧
    (∀x. S(x) ∧ R(x) ⟶ L(x)) ∧
    (∀x. M(x) ⟶ R(x))
  ⟶ (∀x. P(x) ∧ M(x) ⟶ L(x))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹‹¬¬›33›
lemma
  ‹(∀x. ¬ ¬ (P(a) ∧ (P(x) ⟶ P(b)) ⟶ P(c))) ⟷
    (∀x. ¬ ¬ ((¬ P(a) ∨ P(x) ∨ P(c)) ∧ (¬ P(a) ∨ ¬ P(b) ∨ P(c))))›
  apply (tactic ‹IntPr.best_tac \<^context> 1›)
  done


text‹36›
lemma
  ‹(∀x. ∃y. J(x,y)) ∧
    (∀x. ∃y. G(x,y)) ∧
    (∀x y. J(x,y) ∨ G(x,y) ⟶ (∀z. J(y,z) ∨ G(y,z) ⟶ H(x,z)))
  ⟶ (∀x. ∃y. H(x,y))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹37›
lemma
  ‹(∀z. ∃w. ∀x. ∃y.
      ¬ ¬ (P(x,z) ⟶ P(y,w)) ∧ P(y,z) ∧ (P(y,w) ⟶ (∃u. Q(u,w)))) ∧
        (∀x z. ¬ P(x,z) ⟶ (∃y. Q(y,z))) ∧
        (¬ ¬ (∃x y. Q(x,y)) ⟶ (∀x. R(x,x)))
    ⟶ ¬ ¬ (∀x. ∃y. R(x,y))›
  oops  ― ‹NOT PROVED›

text‹39›
lemma ‹¬ (∃x. ∀y. F(y,x) ⟷ ¬ F(y,y))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹40. AMENDED›
lemma
  ‹(∃y. ∀x. F(x,y) ⟷ F(x,x)) ⟶
    ¬ (∀x. ∃y. ∀z. F(z,y) ⟷ ¬ F(z,x))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹44›
lemma
  ‹(∀x. f(x) ⟶
    (∃y. g(y) ∧ h(x,y) ∧ (∃y. g(y) ∧ ¬ h(x,y)))) ∧
    (∃x. j(x) ∧ (∀y. g(y) ⟶ h(x,y)))
    ⟶ (∃x. j(x) ∧ ¬ f(x))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹48›
lemma ‹(a = b ∨ c = d) ∧ (a = c ∨ b = d) ⟶ a = d ∨ b = c›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹51›
lemma
  ‹(∃z w. ∀x y. P(x,y) ⟷ (x = z ∧ y = w)) ⟶
    (∃z. ∀x. ∃w. (∀y. P(x,y) ⟷ y = w) ⟷ x = z)›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹52›
text ‹Almost the same as 51.›
lemma
  ‹(∃z w. ∀x y. P(x,y) ⟷ (x = z ∧ y = w)) ⟶
    (∃w. ∀y. ∃z. (∀x. P(x,y) ⟷ x = z) ⟷ y = w)›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹56›
lemma ‹(∀x. (∃y. P(y) ∧ x = f(y)) ⟶ P(x)) ⟷ (∀x. P(x) ⟶ P(f(x)))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹57›
lemma
  ‹P(f(a,b), f(b,c)) ∧ P(f(b,c), f(a,c)) ∧
    (∀x y z. P(x,y) ∧ P(y,z) ⟶ P(x,z)) ⟶ P(f(a,b), f(a,c))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

text‹60›
lemma ‹∀x. P(x,f(x)) ⟷ (∃y. (∀z. P(z,y) ⟶ P(z,f(x))) ∧ P(x,y))›
  by (tactic ‹IntPr.fast_tac \<^context> 1›)

end