namespace http://cds.omdoc.org/examples

// like fol.mmt but for sorted first-order logic ❚

theory TypedTerms : ur:?LF =
  tp: type
  tm: tp ⟶ type# tm 1 prec -5


theory SFOL : http://cds.omdoc.org/urtheories?LF =
  include ?PL
  include ?TypedTerms
  forall : {S} (tm S ⟶ prop) ⟶ prop#  2                           
  exists : {S} (tm S ⟶ prop) ⟶ prop#  2


theory SFOLEQ : http://cds.omdoc.org/urtheories?LF =
  include ?SFOL
  equal  : {S} tm S ⟶ tm S ⟶ prop# 2  3 prec 30


theory SFOLNatDed : http://cds.omdoc.org/urtheories?LF =
  include ?SFOL
  include ?PLNatDed  
  forallI  : {S,A} ({x: tm S} ⊦ (A x)) ⟶ ⊦ ∀ A 
  forallE  : {S,A} ⊦ (∀ A) ⟶ {x: tm S} ⊦ (A x) role ForwardRule

  existsI  : {S,A} {c} ⊦ (A c) ⟶ ⊦ ∃ [x: tm S] (A x) # existsI 2 3
  existsE  : {S,A,C} ⊦ (∃ [x: tm S] A x) ⟶ ({x} ⊦ (A x) ⟶ ⊦ C) ⟶ ⊦ C


theory Declarative_SFOL =
  include ?SFOLNatDed
  include ?DeclarativeProofs
  
  decl_forallI = forallI # ASSUME 3
  decl_existsI = existsI # TAKE 3 4


theory SFOLEQNatDed : http://cds.omdoc.org/urtheories?LF =
  include ?SFOLEQ
  include ?SFOLNatDed  
  refl     : {S,x: tm S} ⊦ x ≐ x
  congT    : {S, T, x,y} ⊦ x ≐ y ⟶ {F: tm S ⟶ tm T} ⊦ (F x) ≐ (F y) # congT 3 4
  congF    : {S, x,y: tm S} ⊦ x ≐ y ⟶ {F: tm S ⟶ prop} ⊦ (F x) ⟶ ⊦ (F y)# congF 3 4 5
  sym      : {S, x,y: tm S} ⊦ x ≐ y ⟶ ⊦ y ≐ x
  trans    : {S, x,y,z: tm S} ⊦ x ≐ y ⟶ ⊦ y ≐ z ⟶ ⊦ x ≐ z
  
  trans3   : {S, w,x,y,z: tm S} ⊦ w ≐ x ⟶ ⊦ x ≐ y ⟶ ⊦ y ≐ z ⟶ ⊦ w ≐ z
           = [S, w,x,y,z,p,q,r] trans (trans p q) r
  trans4   : {S, v,w,x,y,z: tm S} ⊦ v ≐ w ⟶⊦ w ≐ x ⟶ ⊦ x ≐ y ⟶ ⊦ y ≐ z ⟶ ⊦ v ≐ z
           = [S, v,w,x,y,z,p,q,r,s] trans3 (trans p q) r s