File SumSort_ProofSystem

From MatchingLogic Require Export ProofMode.MLPM
                                  FOEquality_ProofSystem
                                  Sorts_ProofSystem.
From MatchingLogic.Theories Require Export SumSort_Syntax.

Import MatchingLogic.Logic.Notations.
Import MatchingLogic.Theories.Definedness_Syntax.Notations.
Import MatchingLogic.Theories.Sorts_Syntax.Notations.
Import MatchingLogic.Theories.SumSort_Syntax.Notations.


Section sumsort.
  Context
      {Σ : Signature}
      (s1 s2 : Pattern)
      (wfs1 : well_formed s1 = true)
      (wfs2 : well_formed s2 = true)
      {syntax : SumSort_Syntax.Syntax s1 s2}
    .

  Lemma use_sumsort_axiom ax Γ :
    SumSort_Syntax.theory s1 s2 wfs1 wfs2 ⊆ Γ →
      Γ ⊢ axiom _ _ ax.

  Theorem inject_left_inj : ∀ Γ , theory s1 s2 wfs1 wfs2 ⊆ Γ →
                              Γ ⊢ all s1, all s1, ( (b1).mlInjectL( s1 , s2 ) =ml (b0).mlInjectL( s1 , s2 ) ) --->
                               (b1 =ml b0).

  Theorem inject_right_inj : ∀ Γ , theory s1 s2 wfs1 wfs2 ⊆ Γ →
                              Γ ⊢ all s2, all s2, ( (b1).mlInjectR( s1 , s2 ) =ml (b0).mlInjectR( s1 , s2 ) ) --->
                               (b1 =ml b0).

  Lemma subseteq_implies_membership:
    ∀ (Γ : Theory) (φ φ' : Pattern),
    Definedness_Syntax.theory ⊆ Γ →
    well_formed φ →
    well_formed φ' →
    Γ ⊢i φ ⊆ml φ' --->
        ( all , b0 ∈ml φ ---> b0 ∈ml φ') using AnyReasoning.

  Lemma membership_implies_subseteq:
    ∀ (Γ : Theory) (φ φ' : Pattern),
    Definedness_Syntax.theory ⊆ Γ →
    well_formed φ →
    well_formed φ' →
    Γ ⊢i ( all , b0 ∈ml φ ---> b0 ∈ml φ') ---> φ ⊆ml φ' using AnyReasoning.

  Corollary subseteq_iff_membership:
    ∀ (Γ : Theory) (φ φ' : Pattern),
    Definedness_Syntax.theory ⊆ Γ →
    well_formed φ →
    well_formed φ' →
    Γ ⊢i φ ⊆ml φ' <--->
        ( all , b0 ∈ml φ ---> b0 ∈ml φ') using AnyReasoning.

  Theorem membership_axiom_v1:
    ∀ (Γ : Theory) (φ φ' : Pattern) (x : evar),
    Definedness_Syntax.theory ⊆ Γ →
    well_formed φ →
    well_formed φ' →
    Γ ⊢i patt_free_evar x ∈ml ( φ ⋅ φ' ) =ml ex , ( b0 ∈ml φ and patt_free_evar x ∈ml (b0 ⋅ φ') ) using AnyReasoning.

  Theorem membership_axiom_v2:
    ∀ (Γ : Theory) (φ φ' : Pattern) (x : evar),
    Definedness_Syntax.theory ⊆ Γ →
    well_formed φ →
    well_formed φ' →
    Γ ⊢i patt_free_evar x ∈ml ( φ ⋅ φ' ) =ml ex, (b0 ∈ml φ' and patt_free_evar x ∈ml (φ ⋅ b0) ) using AnyReasoning.

  Theorem sum_inj : ∀ Γ , theory s1 s2 wfs1 wfs2 ⊆ Γ →
                              Γ ⊢ ⟦ mlSum (s1, s2) ⟧ =ml ( (⟦s1⟧).mlInjectL( s1 , s2 ) or (⟦s2⟧).mlInjectR( s1 , s2 ) ) .

End sumsort.

Close Scope ml_scope.
Close Scope string_scope.
Close Scope list_scope.