File NamedAxioms

From MatchingLogic Require Export Pattern.

(* TODO: set? *)
(* TODO: well-formedness *)
Record NamedAxioms {Σ : Signature} :=
{
  NAName : Type;
  NAAxiom : NAName → Pattern ;
  NAwf : ∀ (name : NAName), well_formed (NAAxiom name) ;
}.

Definition theory_of_NamedAxioms {Σ : Signature} (NAs : NamedAxioms) : Theory :=
  PropSet (fun p ⇒ ∃ (n : NAName NAs), p = NAAxiom _ n).


(* TODO: do we want to make this a type class? *)
Record NamedAxiomsIncluded {Σ : Signature} (NA₁ NA₂ : NamedAxioms) :=
  { NAIinj : NAName NA₁ → NAName NA₂;
    NAIax : ∀ (n : NAName NA₁), NAAxiom _ n = NAAxiom _ (NAIinj n);
  }.

Lemma NamedAxiomsIncluded_impl_TheoryIncluded {Σ : Signature} NA₁ NA₂:
  NamedAxiomsIncluded NA₁ NA₂ →
  (theory_of_NamedAxioms NA₁) ⊆ (theory_of_NamedAxioms NA₂).

Program Definition NamedAxiomsIncluded_refl {Σ : Signature} NA : NamedAxiomsIncluded NA NA :=
  {| NAIinj := λ n, n; |}.
(* TODO make it a stdpp preorder  *)

Program Definition NamedAxiomsIncluded_compose {Σ : Signature} NA₁ NA₂ NA₃ :
  NamedAxiomsIncluded NA₁ NA₂ →
  NamedAxiomsIncluded NA₂ NA₃ →
  NamedAxiomsIncluded NA₁ NA₃ :=
  λ HI₁ HI₂, {| NAIinj := λ n, NAIinj _ _ HI₂ (NAIinj _ _ HI₁ n); |}.