File Nat_ProofSystem

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

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


Section nat.
  Context
    {Σ : Signature}
    {syntax : Nat_Syntax.Syntax}
  .

(* suppose \phi is_functional 
 *)
  Theorem membership_exists_subst:
    ∀ (Γ : Theory) (φ φ' : Pattern) (i : ProofInfo) ,
      Definedness_Syntax.theory ⊆ Γ →
      well_formed φ →
      well_formed (ex , φ') →
      Γ ⊢i φ ∈ml (ex, φ') --->
      φ'^[evar:0↦φ] using i.

  Lemma use_nat_axiom (ax : Nat_Syntax.AxiomName) Γ :
    Nat_Syntax.theory ⊆ Γ →
      Γ ⊢ Nat_Syntax.axiom ax.

  Lemma nat_subset_imp_in X :
    theory ⊢ (⟦ Nat ⟧ ⊆ml patt_free_svar X) ---> (all Nat, b0 ∈ml patt_free_svar X).
  Theorem peano_induction X :
    theory ⊢
    Zero ∈ml patt_free_svar X --->
    ( all Nat, (b0 ∈ml patt_free_svar X ---> Succ ⋅ b0 ∈ml patt_free_svar X) ) --->
    all Nat, b0 ∈ml patt_free_svar X.

  Theorem peano_induction_1 X :
    theory ⊢ patt_free_svar X ⊆ml ⟦ Nat ⟧ →
    theory ⊢ Zero ∈ml patt_free_svar X →
    theory ⊢ all Nat, ( b0 ∈ml patt_free_svar X ---> Succ ⋅ b0 ∈ml patt_free_svar X ) →
    theory ⊢ all Nat, b0 ∈ml patt_free_svar X.

  Theorem add_zero_r: ∀ Γ , theory ⊆ Γ →
                       Γ ⊢ all Nat, b0 +ml Zero =ml b0.

  Theorem add_zero_l: ∀ Γ , Nat_Syntax.theory ⊆ Γ →
                       Γ ⊢ all Nat, Zero +ml b0 =ml b0.

End nat.