File Bool_ProofSystem

From MatchingLogic Require Export Sorts_ProofSystem
                                  Bool_Syntax.
Import MatchingLogic.Logic.Notations
       MatchingLogic.Theories.Definedness_Syntax.Notations
       MatchingLogic.Theories.Sorts_Syntax.Notations
       MatchingLogic.Theories.Bool_Syntax.Notations.


Open Scope list_scope.

Section bools.
Context
  { Σ : Signature}
  { syntax : Syntax}.

  Lemma use_bool_axiom ax Γ :
    Bool_Syntax.theory ⊆ Γ →
      Γ ⊢ axiom ax.

  Lemma functional_pattern_defined :
    ∀ Γ φ, Definedness_Syntax.theory ⊆ Γ → well_formed φ →
       Γ ⊢ (ex , (φ =ml b0)) ---> ⌈ φ ⌉.

  Lemma membership_equal_equal :
    ∀ Γ φ φ',
      Definedness_Syntax.theory ⊆ Γ → mu_free φ' →
      well_formed φ → well_formed φ' →
      Γ ⊢ (ex , (φ =ml b0)) →
      Γ ⊢ (ex , (φ' =ml b0)) →
      Γ ⊢ (φ ∈ml φ') =ml (φ =ml φ') .

  Theorem double_neg : ∀ Γ , theory ⊆ Γ →
                        Γ ⊢ all mlBool, (!b !b b0) =ml b0.

  Theorem true_andBool : ∀ Γ , theory ⊆ Γ →
                          Γ ⊢ all mlBool, b0 &&ml mlTrue =ml b0.


  Theorem false_andBool : ∀ Γ , theory ⊆ Γ →
                           Γ ⊢ all mlBool, b0 &&ml mlFalse =ml mlFalse.


  Theorem comm_andBool : ∀ Γ , theory ⊆ Γ →
                          Γ ⊢ all mlBool, all mlBool, b0 &&ml b1 =ml b1 &&ml b0.
  Theorem true_andThenBool : ∀ Γ , theory ⊆ Γ →
                              Γ ⊢ all mlBool, b0 andThen mlTrue =ml b0.

  Theorem false_andThenBool : ∀ Γ , theory ⊆ Γ →
                               Γ ⊢ all, b0 andThen mlFalse =ml mlFalse.

End bools.
Close Scope ml_scope.
Close Scope string_scope.
Close Scope list_scope.