Theory IFOL

(*  Title:      FOL/IFOL.thy
    Author:     Lawrence C Paulson and Markus Wenzel
*)

section ‹Intuitionistic first-order logic›

theory IFOL
  imports Pure
  abbrevs "?<" = "∃1"
begin

ML_file ‹~~/src/Tools/misc_legacy.ML›
ML_file ‹~~/src/Provers/splitter.ML›
ML_file ‹~~/src/Provers/hypsubst.ML›
ML_file ‹~~/src/Tools/IsaPlanner/zipper.ML›
ML_file ‹~~/src/Tools/IsaPlanner/isand.ML›
ML_file ‹~~/src/Tools/IsaPlanner/rw_inst.ML›
ML_file ‹~~/src/Provers/quantifier1.ML›
ML_file ‹~~/src/Tools/intuitionistic.ML›
ML_file ‹~~/src/Tools/project_rule.ML›
ML_file ‹~~/src/Tools/atomize_elim.ML›


subsection ‹Syntax and axiomatic basis›

setup Pure_Thy.old_appl_syntax_setup
setup Proofterm.set_preproc (Proof_Rewrite_Rules.standard_preproc [])

class "term"
default_sort term

typedecl o

judgment
  Trueprop :: o  prop  ((_) 5)


subsubsection ‹Equality›

axiomatization
  eq :: ['a, 'a]  o  (infixl = 50)
where
  refl: a = a and
  subst: a = b  P(a)  P(b)


subsubsection ‹Propositional logic›

axiomatization
  False :: o and
  conj :: [o, o] => o  (infixr  35) and
  disj :: [o, o] => o  (infixr  30) and
  imp :: [o, o] => o  (infixr  25)
where
  conjI: P;  Q  P  Q and
  conjunct1: P  Q  P and
  conjunct2: P  Q  Q and

  disjI1: P  P  Q and
  disjI2: Q  P  Q and
  disjE: P  Q; P  R; Q  R  R and

  impI: (P  Q)  P  Q and
  mp: P  Q; P  Q and

  FalseE: False  P


subsubsection ‹Quantifiers›

axiomatization
  All :: ('a  o)  o  (binder  10) and
  Ex :: ('a  o)  o  (binder  10)
where
  allI: (x. P(x))  (x. P(x)) and
  spec: (x. P(x))  P(x) and
  exI: P(x)  (x. P(x)) and
  exE: x. P(x); x. P(x)  R  R


subsubsection ‹Definitions›

definition True  False  False

definition Not (¬ _› [40] 40)
  where not_def: ¬ P  P  False

definition iff  (infixr  25)
  where P  Q  (P  Q)  (Q  P)

definition Uniq :: "('a  o)  o"
  where Uniq(P)  (x y. P(x)  P(y)  y = x)

definition Ex1 :: ('a  o)  o  (binder ∃! 10)
  where ex1_def: ∃!x. P(x)  x. P(x)  (y. P(y)  y = x)

axiomatization where  ― ‹Reflection, admissible›
  eq_reflection: (x = y)  (x  y) and
  iff_reflection: (P  Q)  (P  Q)

abbreviation not_equal :: ['a, 'a]  o  (infixl  50)
  where x  y  ¬ (x = y)

syntax "_Uniq" :: "pttrn  o  o"  ("(21 _./ _)" [0, 10] 10)
translations "1x. P"  "CONST Uniq (λx. P)"

print_translation [Syntax_Trans.preserve_binder_abs_tr' const_syntaxUniq syntax_const‹_Uniq›] ― ‹to avoid eta-contraction of body›


subsubsection ‹Old-style ASCII syntax›

notation (ASCII)
  not_equal  (infixl ~= 50) and
  Not  (~ _› [40] 40) and
  conj  (infixr & 35) and
  disj  (infixr | 30) and
  All  (binder ALL 10) and
  Ex  (binder EX 10) and
  Ex1  (binder EX! 10) and
  imp  (infixr --> 25) and
  iff  (infixr <-> 25)


subsection ‹Lemmas and proof tools›

lemmas strip = impI allI

lemma TrueI: True
  unfolding True_def by (rule impI)


subsubsection ‹Sequent-style elimination rules for ∧› ⟶› and ∀›

lemma conjE:
  assumes major: P  Q
    and r: P; Q  R
  shows R
proof (rule r)
  show "P"
    by (rule major [THEN conjunct1])
  show "Q"
    by (rule major [THEN conjunct2])
qed

lemma impE:
  assumes major: P  Q
    and P
  and r: Q  R
  shows R
proof (rule r)
  show "Q"
    by (rule mp [OF major P])
qed

lemma allE:
  assumes major: x. P(x)
    and r: P(x)  R
  shows R
proof (rule r)
  show "P(x)"
    by (rule major [THEN spec])
qed

text ‹Duplicates the quantifier; for use with MLeresolve_tac.›
lemma all_dupE:
  assumes major: x. P(x)
    and r: P(x); x. P(x)  R
  shows R
proof (rule r)
  show "P(x)"
    by (rule major [THEN spec])
qed (rule major)



subsubsection ‹Negation rules, which translate between ¬ P› and P ⟶ False›

lemma notI: (P  False)  ¬ P
  unfolding not_def by (erule impI)

lemma notE: ¬ P; P  R
  unfolding not_def by (erule mp [THEN FalseE])

lemma rev_notE: P; ¬ P  R
  by (erule notE)

text ‹This is useful with the special implication rules for each kind of P›.›
lemma not_to_imp:
  assumes ¬ P
    and r: P  False  Q
  shows Q
  apply (rule r)
  apply (rule impI)
  apply (erule notE [OF ¬ P])
  done

text ‹
  For substitution into an assumption P›, reduce Q› to P ⟶ Q›, substitute into this implication, then apply impI› to
  move P› back into the assumptions.
›
lemma rev_mp: P; P  Q  Q
  by (erule mp)

text ‹Contrapositive of an inference rule.›
lemma contrapos:
  assumes major: ¬ Q
    and minor: P  Q
  shows ¬ P
  apply (rule major [THEN notE, THEN notI])
  apply (erule minor)
  done


subsubsection ‹Modus Ponens Tactics›

text ‹
  Finds P ⟶ Q› and P in the assumptions, replaces implication by
  Q›.
›
ML fun mp_tac ctxt i =
    eresolve_tac ctxt @{thms notE impE} i THEN assume_tac ctxt i;
  fun eq_mp_tac ctxt i =
    eresolve_tac ctxt @{thms notE impE} i THEN eq_assume_tac i;


subsection ‹If-and-only-if›

lemma iffI: P  Q; Q  P  P  Q
  unfolding iff_def
  by (rule conjI; erule impI)

lemma iffE:
  assumes major: P  Q
    and r: P  Q; Q  P  R
  shows R
  using major
  unfolding iff_def
  apply (rule conjE)
  apply (erule r)
  apply assumption
  done


subsubsection ‹Destruct rules for ⟷› similar to Modus Ponens›

lemma iffD1: P  Q; P  Q
  unfolding iff_def
  apply (erule conjunct1 [THEN mp])
  apply assumption
  done

lemma iffD2: P  Q; Q  P
  unfolding iff_def
  apply (erule conjunct2 [THEN mp])
  apply assumption
  done

lemma rev_iffD1: P; P  Q  Q
  apply (erule iffD1)
  apply assumption
  done

lemma rev_iffD2: Q; P  Q  P
  apply (erule iffD2)
  apply assumption
  done

lemma iff_refl: P  P
  by (rule iffI)

lemma iff_sym: Q  P  P  Q
  apply (erule iffE)
  apply (rule iffI)
  apply (assumption | erule mp)+
  done

lemma iff_trans: P  Q; Q  R  P  R
  apply (rule iffI)
  apply (assumption | erule iffE | erule (1) notE impE)+
  done


subsection ‹Unique existence›

text ‹
  NOTE THAT the following 2 quantifications:

     ∃!x› such that [∃!y› such that P(x,y)]   (sequential)
     ∃!x,y› such that P(x,y)                   (simultaneous)

  do NOT mean the same thing. The parser treats ∃!x y.P(x,y)› as sequential.
›

lemma ex1I: P(a)  (x. P(x)  x = a)  ∃!x. P(x)
  unfolding ex1_def
  apply (assumption | rule exI conjI allI impI)+
  done

text ‹Sometimes easier to use: the premises have no shared variables. Safe!›
lemma ex_ex1I: x. P(x)  (x y. P(x); P(y)  x = y)  ∃!x. P(x)
  apply (erule exE)
  apply (rule ex1I)
   apply assumption
  apply assumption
  done

lemma ex1E: ∃! x. P(x)  (x. P(x); y. P(y)  y = x  R)  R
  unfolding ex1_def
  apply (assumption | erule exE conjE)+
  done


subsubsection ⟷› congruence rules for simplification›

text ‹Use iffE› on a premise. For conj_cong›, imp_cong›, all_cong›, ex_cong›.›
ML fun iff_tac ctxt prems i =
    resolve_tac ctxt (prems RL @{thms iffE}) i THEN
    REPEAT1 (eresolve_tac ctxt @{thms asm_rl mp} i);

method_setup iff =
  Attrib.thms >>
    (fn prems => fn ctxt => SIMPLE_METHOD' (iff_tac ctxt prems))

lemma conj_cong:
  assumes P  P'
    and P'  Q  Q'
  shows (P  Q)  (P'  Q')
  apply (insert assms)
  apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+
  done

text ‹Reversed congruence rule!  Used in ZF/Order.›
lemma conj_cong2:
  assumes P  P'
    and P'  Q  Q'
  shows (Q  P)  (Q'  P')
  apply (insert assms)
  apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+
  done

lemma disj_cong:
  assumes P  P' and Q  Q'
  shows (P  Q)  (P'  Q')
  apply (insert assms)
  apply (erule iffE disjE disjI1 disjI2 |
    assumption | rule iffI | erule (1) notE impE)+
  done

lemma imp_cong:
  assumes P  P'
    and P'  Q  Q'
  shows (P  Q)  (P'  Q')
  apply (insert assms)
  apply (assumption | rule iffI impI | erule iffE | erule (1) notE impE | iff assms)+
  done

lemma iff_cong: P  P'; Q  Q'  (P  Q)  (P'  Q')
  apply (erule iffE | assumption | rule iffI | erule (1) notE impE)+
  done

lemma not_cong: P  P'  ¬ P  ¬ P'
  apply (assumption | rule iffI notI | erule (1) notE impE | erule iffE notE)+
  done

lemma all_cong:
  assumes x. P(x)  Q(x)
  shows (x. P(x))  (x. Q(x))
  apply (assumption | rule iffI allI | erule (1) notE impE | erule allE | iff assms)+
  done

lemma ex_cong:
  assumes x. P(x)  Q(x)
  shows (x. P(x))  (x. Q(x))
  apply (erule exE | assumption | rule iffI exI | erule (1) notE impE | iff assms)+
  done

lemma ex1_cong:
  assumes x. P(x)  Q(x)
  shows (∃!x. P(x))  (∃!x. Q(x))
  apply (erule ex1E spec [THEN mp] | assumption | rule iffI ex1I | erule (1) notE impE | iff assms)+
  done


subsection ‹Equality rules›

lemma sym: a = b  b = a
  apply (erule subst)
  apply (rule refl)
  done

lemma trans: a = b; b = c  a = c
  apply (erule subst, assumption)
  done

lemma not_sym: b  a  a  b
  apply (erule contrapos)
  apply (erule sym)
  done

text ‹
  Two theorems for rewriting only one instance of a definition:
  the first for definitions of formulae and the second for terms.
›

lemma def_imp_iff: (A  B)  A  B
  apply unfold
  apply (rule iff_refl)
  done

lemma meta_eq_to_obj_eq: (A  B)  A = B
  apply unfold
  apply (rule refl)
  done

lemma meta_eq_to_iff: x  y  x  y
  by unfold (rule iff_refl)

text ‹Substitution.›
lemma ssubst: b = a; P(a)  P(b)
  apply (drule sym)
  apply (erule (1) subst)
  done

text ‹A special case of ex1E› that would otherwise need quantifier
  expansion.›
lemma ex1_equalsE: ∃!x. P(x); P(a); P(b)  a = b
  apply (erule ex1E)
  apply (rule trans)
   apply (rule_tac [2] sym)
   apply (assumption | erule spec [THEN mp])+
  done


subsection ‹Simplifications of assumed implications›

text ‹
  Roy Dyckhoff has proved that conj_impE›, disj_impE›, and
  imp_impE› used with MLmp_tac (restricted to atomic formulae) is
  COMPLETE for intuitionistic propositional logic.

  See R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
  (preprint, University of St Andrews, 1991).
›

lemma conj_impE:
  assumes major: (P  Q)  S
    and r: P  (Q  S)  R
  shows R
  by (assumption | rule conjI impI major [THEN mp] r)+

lemma disj_impE:
  assumes major: (P  Q)  S
    and r: P  S; Q  S  R
  shows R
  by (assumption | rule disjI1 disjI2 impI major [THEN mp] r)+

text ‹Simplifies the implication.  Classical version is stronger.
  Still UNSAFE since Q must be provable -- backtracking needed.›
lemma imp_impE:
  assumes major: (P  Q)  S
    and r1: P; Q  S  Q
    and r2: S  R
  shows R
  by (assumption | rule impI major [THEN mp] r1 r2)+

text ‹Simplifies the implication.  Classical version is stronger.
  Still UNSAFE since ~P must be provable -- backtracking needed.›
lemma not_impE: ¬ P  S  (P  False)  (S  R)  R
  apply (drule mp)
   apply (rule notI | assumption)+
  done

text ‹Simplifies the implication. UNSAFE.›
lemma iff_impE:
  assumes major: (P  Q)  S
    and r1: P; Q  S  Q
    and r2: Q; P  S  P
    and r3: S  R
  shows R
  by (assumption | rule iffI impI major [THEN mp] r1 r2 r3)+

text ‹What if (∀x. ¬ ¬ P(x)) ⟶ ¬ ¬ (∀x. P(x))› is an assumption?
  UNSAFE.›
lemma all_impE:
  assumes major: (x. P(x))  S
    and r1: x. P(x)
    and r2: S  R
  shows R
  by (rule allI impI major [THEN mp] r1 r2)+

text ‹
  Unsafe: ∃x. P(x)) ⟶ S› is equivalent
  to ∀x. P(x) ⟶ S›.›
lemma ex_impE:
  assumes major: (x. P(x))  S
    and r: P(x)  S  R
  shows R
  by (assumption | rule exI impI major [THEN mp] r)+

text ‹Courtesy of Krzysztof Grabczewski.›
lemma disj_imp_disj: P  Q  (P  R)  (Q  S)  R  S
  apply (erule disjE)
  apply (rule disjI1) apply assumption
  apply (rule disjI2) apply assumption
  done

ML structure Project_Rule = Project_Rule
(
  val conjunct1 = @{thm conjunct1}
  val conjunct2 = @{thm conjunct2}
  val mp = @{thm mp}
)

ML_file ‹fologic.ML›

lemma thin_refl: x = x; PROP W  PROP W .

ML structure Hypsubst = Hypsubst
(
  val dest_eq = FOLogic.dest_eq
  val dest_Trueprop = dest_judgment
  val dest_imp = FOLogic.dest_imp
  val eq_reflection = @{thm eq_reflection}
  val rev_eq_reflection = @{thm meta_eq_to_obj_eq}
  val imp_intr = @{thm impI}
  val rev_mp = @{thm rev_mp}
  val subst = @{thm subst}
  val sym = @{thm sym}
  val thin_refl = @{thm thin_refl}
);
open Hypsubst;

ML_file ‹intprover.ML›


subsection ‹Intuitionistic Reasoning›

setup Intuitionistic.method_setup bindingiprover

lemma impE':
  assumes 1: P  Q
    and 2: Q  R
    and 3: P  Q  P
  shows R
proof -
  from 3 and 1 have P .
  with 1 have Q by (rule impE)
  with 2 show R .
qed

lemma allE':
  assumes 1: x. P(x)
    and 2: P(x)  x. P(x)  Q
  shows Q
proof -
  from 1 have P(x) by (rule spec)
  from this and 1 show Q by (rule 2)
qed

lemma notE':
  assumes 1: ¬ P
    and 2: ¬ P  P
  shows R
proof -
  from 2 and 1 have P .
  with 1 show R by (rule notE)
qed

lemmas [Pure.elim!] = disjE iffE FalseE conjE exE
  and [Pure.intro!] = iffI conjI impI TrueI notI allI refl
  and [Pure.elim 2] = allE notE' impE'
  and [Pure.intro] = exI disjI2 disjI1

setup Context_Rules.addSWrapper
    (fn ctxt => fn tac => hyp_subst_tac ctxt ORELSE' tac)


lemma iff_not_sym: ¬ (Q  P)  ¬ (P  Q)
  by iprover

lemmas [sym] = sym iff_sym not_sym iff_not_sym
  and [Pure.elim?] = iffD1 iffD2 impE


lemma eq_commute: a = b  b = a
  by iprover


subsection ‹Polymorphic congruence rules›

lemma subst_context: a = b  t(a) = t(b)
  by iprover

lemma subst_context2: a = b; c = d  t(a,c) = t(b,d)
  by iprover

lemma subst_context3: a = b; c = d; e = f  t(a,c,e) = t(b,d,f)
  by iprover

text ‹
  Useful with MLeresolve_tac for proving equalities from known
  equalities.

        a = b
        |   |
        c = d
›
lemma box_equals: a = b; a = c; b = d  c = d
  by iprover

text ‹Dual of box_equals›: for proving equalities backwards.›
lemma simp_equals: a = c; b = d; c = d  a = b
  by iprover


subsubsection ‹Congruence rules for predicate letters›

lemma pred1_cong: a = a'  P(a)  P(a')
  by iprover

lemma pred2_cong: a = a'; b = b'  P(a,b)  P(a',b')
  by iprover

lemma pred3_cong: a = a'; b = b'; c = c'  P(a,b,c)  P(a',b',c')
  by iprover

text ‹Special case for the equality predicate!›
lemma eq_cong: a = a'; b = b'  a = b  a' = b'
  by iprover


subsection ‹Atomizing meta-level rules›

lemma atomize_all [atomize]: (x. P(x))  Trueprop (x. P(x))
proof
  assume x. P(x)
  then show x. P(x) ..
next
  assume x. P(x)
  then show x. P(x) ..
qed

lemma atomize_imp [atomize]: (A  B)  Trueprop (A  B)
proof
  assume A  B
  then show A  B ..
next
  assume A  B and A
  then show B by (rule mp)
qed

lemma atomize_eq [atomize]: (x  y)  Trueprop (x = y)
proof
  assume x  y
  show x = y unfolding x  y by (rule refl)
next
  assume x = y
  then show x  y by (rule eq_reflection)
qed

lemma atomize_iff [atomize]: (A  B)  Trueprop (A  B)
proof
  assume A  B
  show A  B unfolding A  B by (rule iff_refl)
next
  assume A  B
  then show A  B by (rule iff_reflection)
qed

lemma atomize_conj [atomize]: (A &&& B)  Trueprop (A  B)
proof
  assume conj: A &&& B
  show A  B
  proof (rule conjI)
    from conj show A by (rule conjunctionD1)
    from conj show B by (rule conjunctionD2)
  qed
next
  assume conj: A  B
  show A &&& B
  proof -
    from conj show A ..
    from conj show B ..
  qed
qed

lemmas [symmetric, rulify] = atomize_all atomize_imp
  and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff


subsection ‹Atomizing elimination rules›

lemma atomize_exL[atomize_elim]: (x. P(x)  Q)  ((x. P(x))  Q)
  by rule iprover+

lemma atomize_conjL[atomize_elim]: (A  B  C)  (A  B  C)
  by rule iprover+

lemma atomize_disjL[atomize_elim]: ((A  C)  (B  C)  C)  ((A  B  C)  C)
  by rule iprover+

lemma atomize_elimL[atomize_elim]: (B. (A  B)  B)  Trueprop(A) ..


subsection ‹Calculational rules›

lemma forw_subst: a = b  P(b)  P(a)
  by (rule ssubst)

lemma back_subst: P(a)  a = b  P(b)
  by (rule subst)

text ‹
  Note that this list of rules is in reverse order of priorities.
›

lemmas basic_trans_rules [trans] =
  forw_subst
  back_subst
  rev_mp
  mp
  trans


subsection ‹``Let'' declarations›

nonterminal letbinds and letbind

definition Let :: ['a::{}, 'a => 'b]  ('b::{})
  where Let(s, f)  f(s)

syntax
  "_bind"       :: [pttrn, 'a] => letbind           ((2_ =/ _) 10)
  ""            :: letbind => letbinds              (‹_›)
  "_binds"      :: [letbind, letbinds] => letbinds  (‹_;/ _›)
  "_Let"        :: [letbinds, 'a] => 'a             ((let (_)/ in (_)) 10)

translations
  "_Let(_binds(b, bs), e)"  == "_Let(b, _Let(bs, e))"
  "let x = a in e"          == "CONST Let(a, λx. e)"

lemma LetI:
  assumes x. x = t  P(u(x))
  shows P(let x = t in u(x))
  unfolding Let_def
  apply (rule refl [THEN assms])
  done


subsection ‹Intuitionistic simplification rules›

lemma conj_simps:
  P  True  P
  True  P  P
  P  False  False
  False  P  False
  P  P  P
  P  P  Q  P  Q
  P  ¬ P  False
  ¬ P  P  False
  (P  Q)  R  P  (Q  R)
  by iprover+

lemma disj_simps:
  P  True  True
  True  P  True
  P  False  P
  False  P  P
  P  P  P
  P  P  Q  P  Q
  (P  Q)  R  P  (Q  R)
  by iprover+

lemma not_simps:
  ¬ (P  Q)  ¬ P  ¬ Q
  ¬ False  True
  ¬ True  False
  by iprover+

lemma imp_simps:
  (P  False)  ¬ P
  (P  True)  True
  (False  P)  True
  (True  P)  P
  (P  P)  True
  (P  ¬ P)  ¬ P
  by iprover+

lemma iff_simps:
  (True  P)  P
  (P  True)  P
  (P  P)  True
  (False  P)  ¬ P
  (P  False)  ¬ P
  by iprover+

text ‹The x = t› versions are needed for the simplification
  procedures.›
lemma quant_simps:
  P. (x. P)  P
  (x. x = t  P(x))  P(t)
  (x. t = x  P(x))  P(t)
  P. (x. P)  P
  x. x = t
  x. t = x
  (x. x = t  P(x))  P(t)
  (x. t = x  P(x))  P(t)
  by iprover+

text ‹These are NOT supplied by default!›
lemma distrib_simps:
  P  (Q  R)  P  Q  P  R
  (Q  R)  P  Q  P  R  P
  (P  Q  R)  (P  R)  (Q  R)
  by iprover+

lemma subst_all:
  (x. x = a  PROP P(x))  PROP P(a)
  (x. a = x  PROP P(x))  PROP P(a)
proof -
  show (x. x = a  PROP P(x))  PROP P(a)
  proof (rule equal_intr_rule)
    assume *: x. x = a  PROP P(x)
    show PROP P(a)
      by (rule *) (rule refl)
  next
    fix x
    assume PROP P(a) and x = a
    from x = a have x  a
      by (rule eq_reflection)
    with PROP P(a) show PROP P(x)
      by simp
  qed
  show (x. a = x  PROP P(x))  PROP P(a)
  proof (rule equal_intr_rule)
    assume *: x. a = x  PROP P(x)
    show PROP P(a)
      by (rule *) (rule refl)
  next
    fix x
    assume PROP P(a) and a = x
    from a = x have a  x
      by (rule eq_reflection)
    with PROP P(a) show PROP P(x)
      by simp
  qed
qed


subsubsection ‹Conversion into rewrite rules›

lemma P_iff_F: ¬ P  (P  False)
  by iprover
lemma iff_reflection_F: ¬ P  (P  False)
  by (rule P_iff_F [THEN iff_reflection])

lemma P_iff_T: P  (P  True)
  by iprover
lemma iff_reflection_T: P  (P  True)
  by (rule P_iff_T [THEN iff_reflection])


subsubsection ‹More rewrite rules›

lemma conj_commute: P  Q  Q  P by iprover
lemma conj_left_commute: P  (Q  R)  Q  (P  R) by iprover
lemmas conj_comms = conj_commute conj_left_commute

lemma disj_commute: P  Q  Q  P by iprover
lemma disj_left_commute: P  (Q  R)  Q  (P  R) by iprover
lemmas disj_comms = disj_commute disj_left_commute

lemma conj_disj_distribL: P  (Q  R)  (P  Q  P  R) by iprover
lemma conj_disj_distribR: (P  Q)  R  (P  R  Q  R) by iprover

lemma disj_conj_distribL: P  (Q  R)  (P  Q)  (P  R) by iprover
lemma disj_conj_distribR: (P  Q)  R  (P  R)  (Q  R) by iprover

lemma imp_conj_distrib: (P  (Q  R))  (P  Q)  (P  R) by iprover
lemma imp_conj: ((P  Q)  R)  (P  (Q  R)) by iprover
lemma imp_disj: (P  Q  R)  (P  R)  (Q  R) by iprover

lemma de_Morgan_disj: (¬ (P  Q))  (¬ P  ¬ Q) by iprover

lemma not_ex: (¬ (x. P(x)))  (x. ¬ P(x)) by iprover
lemma imp_ex: ((x. P(x))  Q)  (x. P(x)  Q) by iprover

lemma ex_disj_distrib: (x. P(x)  Q(x))  ((x. P(x))  (x. Q(x)))
  by iprover

lemma all_conj_distrib: (x. P(x)  Q(x))  ((x. P(x))  (x. Q(x)))
  by iprover

end