Theory Pure_I

theory Pure_I imports Pure begin

typedecl bool

judgment Trueprop :: ‹bool ⇒ prop› (‹_›)

axiomatization Imp (infixr ‹⟶› 3)
  where Imp_I [intro]: ‹(p ⟹ q) ⟹ p ⟶ q›
    and Imp_E [elim]: ‹p ⟶ q ⟹ p ⟹ q›

axiomatization Dis (infixr ‹∨› 4)
  where Dis_E [elim]: ‹p ∨ q ⟹ (p ⟹ r) ⟹ (q ⟹ r) ⟹ r›
    and Dis_I1 [intro]: ‹p ⟹ p ∨ q›
    and Dis_I2 [intro]: ‹q ⟹ p ∨ q›

axiomatization Con (infixr ‹∧› 5)
  where Con_I [intro]: ‹p ⟹ q ⟹ p ∧ q›
    and Con_E1 [elim]: ‹p ∧ q ⟹ p›
    and Con_E2 [elim]: ‹p ∧ q ⟹ q›

axiomatization Falsity (‹⊥›)
  where Falsity_E [elim]: ‹⊥ ⟹ p›

definition Truth (‹⊤›) where ‹⊤ ≡ ⊥ ⟶ ⊥›

theorem Truth_I [intro]: ‹⊤›
  unfolding Truth_def ..

definition Neg (‹¬ _› [6] 6) where ‹¬ p ≡ p ⟶ ⊥›

theorem Neg_I [intro]: ‹(p ⟹ ⊥) ⟹ ¬ p›
  unfolding Neg_def ..

theorem Neg_E [elim]: ‹¬ p ⟹ p ⟹ q›
  unfolding Neg_def
proof -
  assume ‹p ⟶ ⊥› and ‹p›
  then have ‹⊥› ..
  then show ‹q› ..
qed

definition Iff (infixr ‹⟷› 3) where ‹p ⟷ q ≡ (p ⟶ q) ∧ (q ⟶ p)›

theorem Iff_I [intro]: ‹(p ⟹ q) ⟹ (q ⟹ p) ⟹ p ⟷ q›
  unfolding Iff_def
proof -
  assume ‹p ⟹ q› and ‹q ⟹ p›
  from ‹p ⟹ q› have ‹p ⟶ q› ..
  from ‹q ⟹ p› have ‹q ⟶ p› ..
  from ‹p ⟶ q› and ‹q ⟶ p› show ‹(p ⟶ q) ∧ (q ⟶ p)› ..
qed

theorem Iff_E1 [elim]: ‹p ⟷ q ⟹ p ⟹ q›
  unfolding Iff_def
proof -
  assume ‹(p ⟶ q) ∧ (q ⟶ p)›
  then have ‹p ⟶ q› ..
  then show ‹p ⟹ q› ..
qed

theorem Iff_E2 [elim]: ‹p ⟷ q ⟹ q ⟹ p›
  unfolding Iff_def
proof -
  assume ‹(p ⟶ q) ∧ (q ⟶ p)›
  then have ‹q ⟶ p› ..
  then show ‹q ⟹ p› ..
qed

proposition ‹p ⟶ ¬ ¬ p›
proof
  assume ‹p›
  show ‹¬ ¬ p›
  proof
    assume ‹¬ p›
    from ‹¬ p› and ‹p› show ‹⊥› ..
  qed
qed

proposition ‹(p ⟶ q) ∧ ¬ q ⟶ ¬ p›
proof
  assume ‹(p ⟶ q) ∧ ¬ q›
  show ‹¬ p›
  proof
    assume ‹p›
    from ‹(p ⟶ q) ∧ ¬ q› have ‹p ⟶ q› ..
    from ‹p ⟶ q› and ‹p› have ‹q› ..
    from ‹(p ⟶ q) ∧ ¬ q› have ‹¬ q› ..
    from ‹¬ q› and ‹q› show ‹⊥› ..
  qed
qed

proposition ‹(p ⟷ q) ⟷ q ⟷ p›
proof
  assume ‹p ⟷ q›
  show ‹q ⟷ p›
  proof
    from ‹p ⟷ q› show ‹q ⟹ p› ..
  next
    from ‹p ⟷ q› show ‹p ⟹ q› ..
  qed
next
  assume ‹q ⟷ p›
  show ‹p ⟷ q›
  proof
    from ‹q ⟷ p› show ‹p ⟹ q› ..
  next
    from ‹q ⟷ p› show ‹q ⟹ p› ..
  qed
qed

end