import "10-theory-definedness.mm0";

--| The Countable sort allows us to define recursively enumarable theories.
sort Countable;
term zero :             Countable;
term succ : Countable > Countable;

def emptyset : Pattern = $bot$;

term epsilon_symbol : Symbol;
def epsilon : Pattern = $sym epsilon_symbol$;
axiom functional_epsilon {x : EVar} : $exists x (eVar x == epsilon)$;

term letter_symbol : Countable > Symbol;
def letter(N: Countable) : Pattern = $sym (letter_symbol N)$;
def a : Pattern = $letter zero$;
axiom functional_letter {x : EVar} (N: Countable) : $exists x (eVar x == (letter N))$;

term alphabet_symbol: Countable > Symbol;
def alphabet(N: Countable): Pattern = $sym (alphabet_symbol N)$;
axiom domain_letter_zero : $(alphabet zero) == a$;
axiom domain_letter_succ (N: Countable): $(alphabet (succ N)) == (letter (succ N)) \/ (alphabet N)$;
axiom no_confusion_letters (N: Countable): $~(letter (succ N) C_ (alphabet N))$;
axiom no_confusion_epsilon_letter (N: Countable): $~(epsilon C_ (alphabet N))$;

term concat_symbol : Symbol;
def concat (phi psi: Pattern) : Pattern = $(app (app (sym concat_symbol) phi) psi)$;
infixl concat: $.$ prec 39;
axiom functional_concat  {w v x: EVar} : $exists x (eVar x == (eVar w . eVar v))$;
axiom no_confusion_ec_e  {u v: EVar} : $(epsilon == eVar u . eVar v) -> (epsilon == eVar u) /\ (epsilon == eVar v)$;
axiom no_confusion_cc_e  {u v x y: EVar} (N: Countable) : $(x in (alphabet N)) -> (y in (alphabet N))
                            -> (eVar x . eVar u == eVar y . eVar v) -> (eVar x == eVar y) /\ (eVar u == eVar v)$;
axiom assoc_concat_e     {u v w: EVar} : $(eVar u . eVar v) . eVar w == eVar u . (eVar v . eVar w)$;
axiom identity_left_e    {u : EVar} : $epsilon . (eVar u) == (eVar u)$;
axiom identity_right_e   {u : EVar} : $(eVar u) . epsilon == (eVar u)$;

def kleene_l {X: SVar} (alpha: Pattern X) : Pattern = $mu X (epsilon \/ sVar X . alpha)$;
def kleene_r {X: SVar} (alpha: Pattern X) : Pattern = $mu X (epsilon \/ alpha . sVar X)$;
def kleene   {X: SVar} (alpha: Pattern X) : Pattern = $(kleene_r X alpha)$;

def top_word_l {X: SVar} (N: Countable) : Pattern = $(kleene_l X (alphabet N) )$ ;
def top_word_r {X: SVar} (N: Countable) : Pattern = $(kleene_r X (alphabet N) )$ ;
def top_word   {X: SVar} (N: Countable) : Pattern = $(kleene   X (alphabet N) )$ ;

--- We can no longer define the domain axiom.
--- In any case, it is probably best to move towards sorts, and sorted negation.
def neg (N: Countable) (phi: Pattern) = $(top_word N) /\ ~ phi$

def derivative (l: Pattern) (phi: Pattern) {.box : SVar}: Pattern
= $ctximp_app box (l . sVar box) phi $;