Theory Propositional_Int
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›
lemma ‹P ⟶ (Q ⟶ 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) ∨ (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