Theory Miniscope
theory Miniscope
imports FOL
begin
lemmas ccontr = FalseE [THEN classical]
subsection ‹Negation Normal Form›
subsubsection ‹de Morgan laws›
lemma demorgans1:
‹¬ (P ∧ Q) ⟷ ¬ P ∨ ¬ Q›
‹¬ (P ∨ Q) ⟷ ¬ P ∧ ¬ Q›
‹¬ ¬ P ⟷ P›
by blast+
lemma demorgans2:
‹⋀P. ¬ (∀x. P(x)) ⟷ (∃x. ¬ P(x))›
‹⋀P. ¬ (∃x. P(x)) ⟷ (∀x. ¬ P(x))›
by blast+
lemmas demorgans = demorgans1 demorgans2
lemma nnf_simps:
‹(P ⟶ Q) ⟷ (¬ P ∨ Q)›
‹¬ (P ⟶ Q) ⟷ (P ∧ ¬ Q)›
‹(P ⟷ Q) ⟷ (¬ P ∨ Q) ∧ (¬ Q ∨ P)›
‹¬ (P ⟷ Q) ⟷ (P ∨ Q) ∧ (¬ P ∨ ¬ Q)›
by blast+
subsubsection ‹Pushing in the existential quantifiers›
lemma ex_simps:
‹(∃x. P) ⟷ P›
‹⋀P Q. (∃x. P(x) ∧ Q) ⟷ (∃x. P(x)) ∧ Q›
‹⋀P Q. (∃x. P ∧ Q(x)) ⟷ P ∧ (∃x. Q(x))›
‹⋀P Q. (∃x. P(x) ∨ Q(x)) ⟷ (∃x. P(x)) ∨ (∃x. Q(x))›
‹⋀P Q. (∃x. P(x) ∨ Q) ⟷ (∃x. P(x)) ∨ Q›
‹⋀P Q. (∃x. P ∨ Q(x)) ⟷ P ∨ (∃x. Q(x))›
by blast+
subsubsection ‹Pushing in the universal quantifiers›
lemma all_simps:
‹(∀x. P) ⟷ P›
‹⋀P Q. (∀x. P(x) ∧ Q(x)) ⟷ (∀x. P(x)) ∧ (∀x. Q(x))›
‹⋀P Q. (∀x. P(x) ∧ Q) ⟷ (∀x. P(x)) ∧ Q›
‹⋀P Q. (∀x. P ∧ Q(x)) ⟷ P ∧ (∀x. Q(x))›
‹⋀P Q. (∀x. P(x) ∨ Q) ⟷ (∀x. P(x)) ∨ Q›
‹⋀P Q. (∀x. P ∨ Q(x)) ⟷ P ∨ (∀x. Q(x))›
by blast+
lemmas mini_simps = demorgans nnf_simps ex_simps all_simps
ML ‹
val mini_ss = simpset_of (\<^context> addsimps @{thms mini_simps});
fun mini_tac ctxt =
resolve_tac ctxt @{thms ccontr} THEN' asm_full_simp_tac (put_simpset mini_ss ctxt);
›
end