add(FirstOrder/Concat): Language of Theory of Concatenation

Foundation/FirstOrder/Concatenation/Basic/Axioms.lean

@@ -0,0 +1,27 @@
+module
+
+public import Foundation.FirstOrder.SetTheory.Basic.Misc
+public import Foundation.FirstOrder.Concatenation.Basic.Misc
+
+@[expose] public section
+
+namespace LO.FirstOrder.ConcatTheory
+
+namespace Axiom
+
+def concat_zero    : Sentence ℒ⌢ := “∀ x, x ⌢ 0 = x”
+def zero_concat    : Sentence ℒ⌢ := “∀ x, 0 ⌢ x = 0”
+
+def concat_assoc   : Sentence ℒ⌢ := “∀ x y z, (x ⌢ y) ⌢ z = x ⌢ (y ⌢ z)”
+
+def concat_ne_zero : Sentence ℒ⌢ := “∀ x y, x ⌢ y ≠ 0”
+
+def concat_ne_one  : Sentence ℒ⌢ := “∀ x y, x ⌢ y ≠ 1”
+
+def editor_axiom   : Sentence ℒ⌢ := “∀ x y u v, x ⌢ y = u ⌢ v → ∃ w, (u = x ⌢ w ∧ y = w ⌢ v) ∨ (x = u ⌢ w ∧ v = w ⌢ y)”
+
+def nontrivial     : Sentence ℒ⌢ := “0 ≠ 1”
+
+end Axiom
+
+end LO.FirstOrder.ConcatTheory

Foundation/FirstOrder/Concatenation/Basic/Misc.lean

@@ -0,0 +1,95 @@
+module
+
+public import Foundation.FirstOrder.Completeness.Corollaries
+public import Foundation.FirstOrder.Completeness.Corollaries
+public import Mathlib.SetTheory.Cardinal.Basic
+
+/-! # Preperations for theory of concatenation -/
+
+@[expose] public section
+
+namespace LO.FirstOrder
+
+namespace Language
+
+namespace concat
+
+inductive Func : ℕ → Type
+  | zero   : Func 0
+  | one    : Func 0
+  | concat : Func 2
+
+inductive Rel : ℕ → Type
+  | eq : Rel 2
+
+end concat
+
+/-- Language of concat theory -/
+@[reducible]
+def concat : Language where
+  Func := concat.Func
+  Rel := concat.Rel
+
+notation "ℒ⌢" => Language.concat
+
+namespace concat
+
+instance (k) : DecidableEq (concat.Func k) := λ a b => by
+  rcases a <;> rcases b <;>
+  simp only [reduceCtorEq] <;> try {exact instDecidableTrue} <;> try {exact instDecidableFalse}
+
+instance (k) : DecidableEq (concat.Rel k) := λ a b => by
+  rcases a <;> rcases b <;>
+  simp only [reduceCtorEq] <;> try {exact instDecidableTrue} <;> try {exact instDecidableFalse}
+
+instance (k) : Encodable (concat.Func k) where
+  encode := fun x =>
+    match x with
+    | .zero => 0
+    | .one  => 1
+    | .concat => 0
+  decode := fun e =>
+    match k, e with
+    | 0, 0 => some .zero
+    | 0, 1 => some .one
+    | 2, 0 => some .concat
+    | _, _ => none
+  encodek := fun x => by rcases x <;> simp
+
+instance (k) : Encodable (concat.Rel k) where
+  encode := fun x =>
+    match x with
+    | .eq => 0
+  decode := fun e =>
+    match k, e with
+    | 2, 0 => some .eq
+    | _, _ => none
+  encodek := fun x => by rcases x <;> simp
+
+instance : (ℒ⌢).DecidableEq := ⟨fun _ ↦ inferInstance, fun _ ↦ inferInstance⟩
+
+instance : (ℒ⌢).Encodable := ⟨fun _ ↦ inferInstance, fun _ ↦ inferInstance⟩
+
+instance : (ℒ⌢).Zero := ⟨Func.zero⟩
+
+instance : (ℒ⌢).One := ⟨Func.one⟩
+
+instance : (ℒ⌢).Concat := ⟨Func.concat⟩
+
+instance : (ℒ⌢).Eq := ⟨Rel.eq⟩
+
+end concat
+
+end Language
+
+abbrev ConcatTheory := Theory ℒ⌢
+
+abbrev ConcatTheorySemiterm := Semiterm ℒ⌢
+
+variable [ToString ξ]
+
+def ConcatTheorySemiterm.toString' : Semiterm ℒ⌢ ξ n→ String
+  | #x => "x_{" ++ toString (n - 1 - (x : ℕ)) ++ "}"
+  | &x => "a_{" ++ toString x ++ "}"
+
+end LO.FirstOrder

Foundation/Syntax/Predicate/Language.lean

@@ -287,7 +287,20 @@ class Pairing (L : Language) where
 class Star (L : Language) where
   star : L.Func 0
 
-attribute [match_pattern] Zero.zero One.one Add.add Mul.mul Exp.exp Eq.eq LT.lt Mem.mem Star.star
+class Concat (L : Language) where
+  concat : L.Func 2
+
+attribute [match_pattern]
+  Zero.zero
+  One.one
+  Add.add
+  Mul.mul
+  Exp.exp
+  Eq.eq
+  LT.lt
+  Mem.mem
+  Star.star
+  Concat.concat
 
 class ORing (L : Language) extends L.Eq, L.LT, L.Zero, L.One, L.Add, L.Mul