Structure ConseqConvTheory

signature ConseqConvTheory =
sig
  type thm = Thm.thm

  (*  Definitions  *)
    val ASM_MARKER_DEF : thm

  (*  Theorems  *)
    val AND_CLAUSES_FX : thm
    val AND_CLAUSES_TX : thm
    val AND_CLAUSES_XF : thm
    val AND_CLAUSES_XT : thm
    val AND_CLAUSES_XX : thm
    val ASM_MARKER_THM : thm
    val COND_CLAUSES_CF : thm
    val COND_CLAUSES_CT : thm
    val COND_CLAUSES_FF : thm
    val COND_CLAUSES_FT : thm
    val COND_CLAUSES_ID : thm
    val COND_CLAUSES_TF : thm
    val COND_CLAUSES_TT : thm
    val IMP_CLAUSES_FX : thm
    val IMP_CLAUSES_TX : thm
    val IMP_CLAUSES_XF : thm
    val IMP_CLAUSES_XT : thm
    val IMP_CLAUSES_XX : thm
    val IMP_CONG_cond : thm
    val IMP_CONG_cond_simple : thm
    val IMP_CONG_conj_strengthen : thm
    val IMP_CONG_conj_weaken : thm
    val IMP_CONG_disj_strengthen : thm
    val IMP_CONG_disj_weaken : thm
    val IMP_CONG_imp_strengthen : thm
    val IMP_CONG_imp_weaken : thm
    val IMP_CONG_simple_imp_strengthen : thm
    val IMP_CONG_simple_imp_weaken : thm
    val NOT_CLAUSES_F : thm
    val NOT_CLAUSES_T : thm
    val NOT_CLAUSES_X : thm
    val OR_CLAUSES_FX : thm
    val OR_CLAUSES_TX : thm
    val OR_CLAUSES_XF : thm
    val OR_CLAUSES_XT : thm
    val OR_CLAUSES_XX : thm
    val exists_eq_thm : thm
    val false_imp : thm
    val forall_eq_thm : thm
    val true_imp : thm

  val ConseqConv_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [bool] Parent theory of "ConseqConv"

   [ASM_MARKER_DEF]  Definition

      |- ASM_MARKER = (λy x. x)

   [AND_CLAUSES_FX]  Theorem

      |- ∀t. F ∧ t ⇔ F

   [AND_CLAUSES_TX]  Theorem

      |- ∀t. T ∧ t ⇔ t

   [AND_CLAUSES_XF]  Theorem

      |- ∀t. t ∧ F ⇔ F

   [AND_CLAUSES_XT]  Theorem

      |- ∀t. t ∧ T ⇔ t

   [AND_CLAUSES_XX]  Theorem

      |- ∀t. t ∧ t ⇔ t

   [ASM_MARKER_THM]  Theorem

      |- ∀y x. ASM_MARKER y x ⇔ x

   [COND_CLAUSES_CF]  Theorem

      |- ∀t1 t2. (if F then t1 else t2) = t2

   [COND_CLAUSES_CT]  Theorem

      |- ∀t1 t2. (if T then t1 else t2) = t1

   [COND_CLAUSES_FF]  Theorem

      |- ∀c x. (if c then x else F) ⇔ c ∧ x

   [COND_CLAUSES_FT]  Theorem

      |- ∀c x. (if c then x else T) ⇔ c ⇒ x

   [COND_CLAUSES_ID]  Theorem

      |- ∀b t. (if b then t else t) = t

   [COND_CLAUSES_TF]  Theorem

      |- ∀c x. (if c then F else x) ⇔ ¬c ∧ x

   [COND_CLAUSES_TT]  Theorem

      |- ∀c x. (if c then T else x) ⇔ ¬c ⇒ x

   [IMP_CLAUSES_FX]  Theorem

      |- ∀t. F ⇒ t ⇔ T

   [IMP_CLAUSES_TX]  Theorem

      |- ∀t. T ⇒ t ⇔ t

   [IMP_CLAUSES_XF]  Theorem

      |- ∀t. t ⇒ F ⇔ ¬t

   [IMP_CLAUSES_XT]  Theorem

      |- ∀t. t ⇒ T ⇔ T

   [IMP_CLAUSES_XX]  Theorem

      |- ∀t. t ⇒ t ⇔ T

   [IMP_CONG_cond]  Theorem

      |- ∀c x x' y y'.
           (c ⇒ x' ⇒ x) ∧ (¬c ⇒ y' ⇒ y) ⇒
           (if c then x' else y') ⇒
           if c then x else y

   [IMP_CONG_cond_simple]  Theorem

      |- ∀c x x' y y'.
           (x' ⇒ x) ∧ (y' ⇒ y) ⇒
           (if c then x' else y') ⇒
           if c then x else y

   [IMP_CONG_conj_strengthen]  Theorem

      |- ∀x x' y y'. (y ⇒ x' ⇒ x) ∧ (x' ⇒ y' ⇒ y) ⇒ x' ∧ y' ⇒ x ∧ y

   [IMP_CONG_conj_weaken]  Theorem

      |- ∀x x' y y'. (y ⇒ x ⇒ x') ∧ (x' ⇒ y ⇒ y') ⇒ x ∧ y ⇒ x' ∧ y'

   [IMP_CONG_disj_strengthen]  Theorem

      |- ∀x x' y y'. (¬y ⇒ x' ⇒ x) ∧ (¬x' ⇒ y' ⇒ y) ⇒ x' ∨ y' ⇒ x ∨ y

   [IMP_CONG_disj_weaken]  Theorem

      |- ∀x x' y y'. (¬y ⇒ x ⇒ x') ∧ (¬x' ⇒ y ⇒ y') ⇒ x ∨ y ⇒ x' ∨ y'

   [IMP_CONG_imp_strengthen]  Theorem

      |- ∀x x' y y'. (x ⇒ y' ⇒ y) ∧ (¬y' ⇒ x ⇒ x') ⇒ (x' ⇒ y') ⇒ x ⇒ y

   [IMP_CONG_imp_weaken]  Theorem

      |- ∀x x' y y'. (x ⇒ y ⇒ y') ∧ (¬y' ⇒ x' ⇒ x) ⇒ (x ⇒ y) ⇒ x' ⇒ y'

   [IMP_CONG_simple_imp_strengthen]  Theorem

      |- ∀x x' y y'. (x ⇒ x') ∧ (x' ⇒ y' ⇒ y) ⇒ (x' ⇒ y') ⇒ x ⇒ y

   [IMP_CONG_simple_imp_weaken]  Theorem

      |- ∀x x' y y'. (x' ⇒ x) ∧ (x' ⇒ y ⇒ y') ⇒ (x ⇒ y) ⇒ x' ⇒ y'

   [NOT_CLAUSES_F]  Theorem

      |- ¬F ⇔ T

   [NOT_CLAUSES_T]  Theorem

      |- ¬T ⇔ F

   [NOT_CLAUSES_X]  Theorem

      |- ∀t. ¬ ¬t ⇔ t

   [OR_CLAUSES_FX]  Theorem

      |- ∀t. F ∨ t ⇔ t

   [OR_CLAUSES_TX]  Theorem

      |- ∀t. T ∨ t ⇔ T

   [OR_CLAUSES_XF]  Theorem

      |- ∀t. t ∨ F ⇔ t

   [OR_CLAUSES_XT]  Theorem

      |- ∀t. t ∨ T ⇔ T

   [OR_CLAUSES_XX]  Theorem

      |- ∀t. t ∨ t ⇔ t

   [exists_eq_thm]  Theorem

      |- (∀s. P s ⇔ Q s) ⇒ ((∃s. P s) ⇔ ∃s. Q s)

   [false_imp]  Theorem

      |- ∀t. F ⇒ t

   [forall_eq_thm]  Theorem

      |- (∀s. P s ⇔ Q s) ⇒ ((∀s. P s) ⇔ ∀s. Q s)

   [true_imp]  Theorem

      |- ∀t. t ⇒ T


*)
end

HOL 4, Kananaskis-11