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

section ‹First-Order Logic: propositional examples (intuitionistic version)›

theory Propositional_Int
imports IFOL
begin

text ‹commutative laws of ‹∧› and ‹∨››

lemma ‹P ∧ Q ⟶ Q ∧ P›
  by (tactic "IntPr.fast_tac context 1")

lemma ‹P ∨ Q ⟶ Q ∨ P›
  by (tactic "IntPr.fast_tac context 1")


text ‹associative laws of ‹∧› and ‹∨››
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 ‹distributive laws of ‹∧› and ‹∨››
lemma ‹(P ∧ Q) ∨ R ⟶ (P ∨ R) ∧ (Q ∨ R)›
  by (tactic "IntPr.fast_tac context 1")

lemma ‹(P ∨ R) ∧ (Q ∨ R) ⟶ (P ∧ Q) ∨ R›
  by (tactic "IntPr.fast_tac context 1")

lemma ‹(P ∨ Q) ∧ R ⟶ (P ∧ R) ∨ (Q ∧ R)›
  by (tactic "IntPr.fast_tac context 1")

lemma ‹(P ∧ R) ∨ (Q ∧ R) ⟶ (P ∨ Q) ∧ R›
  by (tactic "IntPr.fast_tac context 1")


text ‹Laws involving implication›

lemma ‹(P ⟶ R) ∧ (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")

lemma ‹((P ⟶ R) ⟶ R) ⟶ ((Q ⟶ R) ⟶ R) ⟶ (P ∧ Q ⟶ R) ⟶ R›
  by (tactic "IntPr.fast_tac context 1")

lemma ‹¬ (P ⟶ R) ⟶ ¬ (Q ⟶ R) ⟶ ¬ (P ∧ Q ⟶ R)›
  by (tactic "IntPr.fast_tac context 1")

lemma ‹(P ⟶ Q ∧ R) ⟷ (P ⟶ Q) ∧ (P ⟶ R)›
  by (tactic "IntPr.fast_tac context 1")


text ‹Propositions-as-types›

― ‹The combinator K›
lemma ‹P ⟶ (Q ⟶ P)›
  by (tactic "IntPr.fast_tac context 1")

― ‹The combinator S›
lemma ‹(P ⟶ Q ⟶ R) ⟶ (P ⟶ Q) ⟶ (P ⟶ R)›
  by (tactic "IntPr.fast_tac context 1")


― ‹Converse is classical›
lemma ‹(P ⟶ Q) ∨ (P ⟶ R) ⟶ (P ⟶ Q ∨ R)›
  by (tactic "IntPr.fast_tac context 1")

lemma ‹(P ⟶ Q) ⟶ (¬ Q ⟶ ¬ P)›
  by (tactic "IntPr.fast_tac context 1")


text ‹Schwichtenberg's examples (via T. Nipkow)›

lemma stab_imp: ‹(((Q ⟶ R) ⟶ R) ⟶ Q) ⟶ (((P ⟶ Q) ⟶ R) ⟶ R) ⟶ P ⟶ Q›
  by (tactic "IntPr.fast_tac context 1")

lemma stab_to_peirce:
  ‹(((P ⟶ R) ⟶ R) ⟶ P) ⟶ (((Q ⟶ R) ⟶ R) ⟶ Q)
 ⟶ ((P ⟶ Q) ⟶ P) ⟶ P›
  by (tactic "IntPr.fast_tac context 1")

lemma peirce_imp1:
  ‹(((Q ⟶ R) ⟶ Q) ⟶ Q)
 ⟶ (((P ⟶ Q) ⟶ R) ⟶ P ⟶ Q) ⟶ P ⟶ Q›
  by (tactic "IntPr.fast_tac context 1")

lemma peirce_imp2: ‹(((P ⟶ R) ⟶ P) ⟶ P) ⟶ ((P ⟶ Q ⟶ R) ⟶ P) ⟶ P›
  by (tactic "IntPr.fast_tac context 1")

lemma mints: ‹((((P ⟶ Q) ⟶ P) ⟶ P) ⟶ Q) ⟶ Q›
  by (tactic "IntPr.fast_tac context 1")

lemma mints_solovev: ‹(P ⟶ (Q ⟶ R) ⟶ Q) ⟶ ((P ⟶ Q) ⟶ R) ⟶ R›
  by (tactic "IntPr.fast_tac context 1")

lemma tatsuta:
  ‹(((P7 ⟶ P1) ⟶ P10) ⟶ P4 ⟶ P5)
 ⟶ (((P8 ⟶ P2) ⟶ P9) ⟶ P3 ⟶ P10)
 ⟶ (P1 ⟶ P8) ⟶ P6 ⟶ P7
 ⟶ (((P3 ⟶ P2) ⟶ P9) ⟶ P4)
 ⟶ (P1 ⟶ P3) ⟶ (((P6 ⟶ P1) ⟶ P2) ⟶ P9) ⟶ P5›
  by (tactic "IntPr.fast_tac context 1")

lemma tatsuta1:
  ‹(((P8 ⟶ P2) ⟶ P9) ⟶ P3 ⟶ P10)
 ⟶ (((P3 ⟶ P2) ⟶ P9) ⟶ P4)
 ⟶ (((P6 ⟶ P1) ⟶ P2) ⟶ P9)
 ⟶ (((P7 ⟶ P1) ⟶ P10) ⟶ P4 ⟶ P5)
 ⟶ (P1 ⟶ P3) ⟶ (P1 ⟶ P8) ⟶ P6 ⟶ P7 ⟶ P5›
  by (tactic "IntPr.fast_tac context 1")

end