# Theory LK

Up to index of Isabelle/Sequents

theory LK
imports LK0
uses (simpdata.ML)
begin

    (*  Title:      LK/LK.ML
        ID:         $Id: LK.thy,v 1.6 2005/09/18 13:20:08 wenzelm Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1993  University of Cambridge

    Axiom to express monotonicity (a variant of the deduction theorem).  Makes the
    link between |- and ==>, needed for instance to prove imp_cong.

    Axiom left_cong allows the simplifier to use left-side formulas.  Ideally it
    should be derived from lower-level axioms.

    CANNOT be added to LK0.thy because modal logic is built upon it, and
    various modal rules would become inconsistent.
    *)

    theory LK
    imports LK0
    uses ("simpdata.ML")
    begin

    axioms

      monotonic:  "($H |- P ==> $H |- Q) ==> $H, P |- Q"

      left_cong:  "[| P == P';  |- P' ==> ($H |- $F) == ($H' |- $F') |]
                   ==> (P, $H |- $F) == (P', $H' |- $F')"

    ML {* use_legacy_bindings (the_context ()) *}

    use "simpdata.ML"

    end

theorem P_iff_F:

       |- ¬ P ==>  |- P <-> False

theorem P_iff_T:

       |- P ==>  |- P <-> True

theorem conj_commute:

       |- P ∧ Q <-> Q ∧ P

theorem conj_left_commute:

       |- P ∧ Q ∧ R <-> Q ∧ P ∧ R

theorem disj_commute:

       |- P ∨ Q <-> Q ∨ P

theorem disj_left_commute:

       |- P ∨ Q ∨ R <-> Q ∨ P ∨ R

theorem conj_disj_distribL:

       |- P ∧ (Q ∨ R) <-> P ∧ Q ∨ P ∧ R

theorem conj_disj_distribR:

       |- (P ∨ Q) ∧ R <-> P ∧ R ∨ Q ∧ R

theorem disj_conj_distribL:

       |- P ∨ Q ∧ R <-> (P ∨ Q) ∧ (P ∨ R)

theorem disj_conj_distribR:

       |- P ∧ Q ∨ R <-> (P ∨ R) ∧ (Q ∨ R)

theorem imp_conj_distrib:

       |- (P --> Q ∧ R) <-> (P --> Q) ∧ (P --> R)

theorem imp_conj:

       |- (P ∧ Q --> R) <-> P --> Q --> R

theorem imp_disj:

       |- (P ∨ Q --> R) <-> (P --> R) ∧ (Q --> R)

theorem imp_disj1:

       |- (P --> Q) ∨ R <-> P --> Q ∨ R

theorem imp_disj2:

       |- Q ∨ (P --> R) <-> P --> Q ∨ R

theorem de_Morgan_disj:

       |- ¬ (P ∨ Q) <-> ¬ P ∧ ¬ Q

theorem de_Morgan_conj:

       |- ¬ (P ∧ Q) <-> ¬ P ∨ ¬ Q

theorem not_iff:

       |- ¬ (P <-> Q) <-> P <-> ¬ Q

theorem imp_cong:

      [|  |- P <-> P';  |- P' ==>  |- Q <-> Q' |] ==>  |- (P --> Q) <-> P' --> Q'

theorem conj_cong:

      [|  |- P <-> P';  |- P' ==>  |- Q <-> Q' |] ==>  |- P ∧ Q <-> P' ∧ Q'

theorem eq_sym_conv:

       |- x = y <-> y = x

theorem if_True:

       |- (if True then x else y) = x

theorem if_False:

       |- (if False then x else y) = y

theorem if_P:

       |- P ==>  |- (if P then x else y) = x

theorem if_not_P:

       |- ¬ P ==>  |- (if P then x else y) = y

theorem eq_imp_subst:

       |- a = b ==> $H, A(a), $G |- $E, A(b), $F

theorem split_if:

       |- P(if Q then x else y) <-> (Q --> P(x)) ∧ (¬ Q --> P(y))

theorem if_cancel:

       |- (if P then x else x) = x

theorem if_eq_cancel:

       |- (if x = y then y else x) = x