:: String Rewriting Systems
::  by Micha{\l} Trybulec
::
:: Received July 17, 2007
:: Copyright (c) 2007-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, NAT_1, FINSEQ_1, RELAT_1, ARYTM_3, CARD_1, XXREAL_0,
      ORDINAL4, REWRITE1, TARSKI, SUBSET_1, FUNCT_1, AFINSQ_1, XBOOLE_0,
      ORDINAL2, RELAT_2, PRELAMB, FINSEQ_5, LANG1, CIRCTRM1, REWRITE2,
      ORDINAL1, FINSET_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, FINSET_1, RELAT_1,
      DOMAIN_1, XCMPLX_0, NAT_1, FINSEQ_5, FUNCT_1, RELSET_1, XXREAL_0,
      AFINSQ_1, RELAT_2, FINSEQ_1, REWRITE1, FLANG_1, LANG1, PARTIT_2;
 constructors NAT_1, FINSEQ_5, REWRITE1, FLANG_1, LANG1, XREAL_0, RELSET_1,
      PARTIT_2;
 registrations NAT_1, AFINSQ_1, REWRITE1, FINSEQ_1, XXREAL_0, XBOOLE_0,
      RELAT_1, FUNCT_1, XREAL_0, ORDINAL1;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin :: Preliminaries: finite sequences.

reserve x for set;
reserve k, l for Nat;
reserve p, q for FinSequence;

theorem :: REWRITE2:1
  not k in dom p & k + 1 in dom p implies k = 0;

theorem :: REWRITE2:2
  k > len p & k <= len (p^q) implies ex l st k = len p + l & l >= 1
  & l <= len q;

:: Preliminaries: reduction sequences.

reserve R for Relation;
reserve p, q for RedSequence of R;

theorem :: REWRITE2:3
  k >= 1 implies p | k is RedSequence of R;

theorem :: REWRITE2:4
  k in dom p implies ex q st len q = k & q.1 = p.1 & q.len q = p.k;

begin

:: XFinSequence yielding functions and finite sequences.
:: These definitions will be later used for introduction of
:: reduction sequences between words from E^omega (XFinSequences).

definition
  let f be Function;
  attr f is XFinSequence-yielding means
:: REWRITE2:def 1

  x in dom f implies f.x is XFinSequence;
end;

registration
  cluster empty -> XFinSequence-yielding for Function;
end;

registration
  let f be XFinSequence;
  cluster <*f*> -> XFinSequence-yielding;
end;

registration
  let p be XFinSequence-yielding Function;
  let x be object;
  cluster p.x -> finite Function-like Relation-like;
end;

registration
  let p be XFinSequence-yielding Function;
  let x be object;
  cluster p.x -> Sequence-like;
end;

registration
  cluster XFinSequence-yielding for FinSequence;
end;

registration
  let E be set;
  cluster -> XFinSequence-yielding for FinSequence of E^omega;
end;

registration
  let p, q be XFinSequence-yielding FinSequence;
  cluster p^q -> XFinSequence-yielding;
end;

begin

:: Concatenation (left-sided and right-sided ) of an XFinSequence
:: with all elements of a XFinSequence-yielding Function.

definition
  let s be XFinSequence;
  let p be XFinSequence-yielding Function;
  func s ^+ p -> XFinSequence-yielding Function means
:: REWRITE2:def 2

  dom it = dom p & for x st x in dom p holds it.x = s^(p.x);
  func p +^ s -> XFinSequence-yielding Function means
:: REWRITE2:def 3

  dom it = dom p & for x st x in dom p holds it.x = (p.x)^s;
end;

registration
  let s be XFinSequence;
  let p be XFinSequence-yielding FinSequence;
  cluster s ^+ p -> FinSequence-like;
  cluster p +^ s -> FinSequence-like;
end;

:: Properties of the left-sided and right-sided concatenation.

reserve E for set;
reserve s, t for XFinSequence;
reserve p, q for XFinSequence-yielding FinSequence;

theorem :: REWRITE2:5
  len (s ^+ p) = len p & len(p +^ s) = len p;

theorem :: REWRITE2:6
  <%>E ^+ p = p & p +^ <%>E = p;

theorem :: REWRITE2:7
  s ^+ (t ^+ p) = (s^t) ^+ p & (p +^ t) +^ s = p +^ (t^s);

theorem :: REWRITE2:8
  s ^+ (p +^ t) = (s ^+ p) +^ t;

theorem :: REWRITE2:9
  s ^+ (p^q) = (s ^+ p)^(s ^+ q) & (p^q) +^ s = (p +^ s)^(q +^ s);

begin

:: Redefinitions for E^omega:

definition
  let E be set;
  let p be FinSequence of E^omega;
  let k be Nat;
  redefine func p.k -> Element of E^omega;
end;

definition
  let E be set;
  let s be Element of E^omega;
  let p be FinSequence of E^omega;
  redefine func s ^+ p -> FinSequence of E^omega;
  redefine func p +^ s -> FinSequence of E^omega;
end;

:: Definitions of semi-Thue systems and Thue systems.

definition
  let E be set;
  mode semi-Thue-system of E is Relation of E^omega;
end;

reserve E for set;
reserve S, T, U for semi-Thue-system of E;

registration
  let S be Relation;
  cluster S \/ S~-> symmetric;
end;

registration
  let E;
  cluster symmetric for semi-Thue-system of E;
end;

definition
  let E be set;
  mode Thue-system of E is symmetric semi-Thue-system of E;
end;

begin

:: Direct derivations.

reserve s, t, s1, t1, u, v, u1, v1, w for Element of E^omega;
reserve p for FinSequence of E^omega;

definition
  let E, S, s, t;
  pred s -->. t, S means
:: REWRITE2:def 4

  [s, t] in S;
end;

definition
  let E, S, s, t;
  pred s ==>. t, S means
:: REWRITE2:def 5

  ex v, w, s1, t1 st s = v^s1^w & t = v^t1^w & s1 -->. t1, S;
end;

theorem :: REWRITE2:10
  s -->. t, S implies s ==>. t, S;

theorem :: REWRITE2:11
  s ==>. s, S implies ex v, w, s1 st s = v^s1^w & s1 -->. s1, S;

theorem :: REWRITE2:12
  s ==>. t, S implies u^s ==>. u^t, S & s^u ==>. t^u, S;

theorem :: REWRITE2:13
  s ==>. t, S implies u^s^v ==>. u^t^v, S;

theorem :: REWRITE2:14
  s -->. t, S implies u^s ==>. u^t, S & s^u ==>. t^u, S;

theorem :: REWRITE2:15
  s -->. t, S implies u^s^v ==>. u^t^v, S;

theorem :: REWRITE2:16
  S is Thue-system of E & s -->. t, S implies t -->. s, S;

theorem :: REWRITE2:17
  S is Thue-system of E & s ==>. t, S implies t ==>. s, S;

theorem :: REWRITE2:18
  S c= T & s -->. t, S implies s -->.t, T;

theorem :: REWRITE2:19
  S c= T & s ==>. t, S implies s ==>.t, T;

theorem :: REWRITE2:20
  not s ==>. t, {}(E^omega, E^omega);

theorem :: REWRITE2:21
  s ==>. t, S \/ T implies s ==>. t, S or s ==>. t, T;

begin

:: ==>.-relation is introduced to define derivations
:: using concepts from REWRITE1.

definition
  let E;
  redefine func id E -> Relation of E;
end;

definition
  let E, S;
  func ==>.-relation(S) -> Relation of E^omega means
:: REWRITE2:def 6

  [s, t] in it iff s ==>. t, S;
end;

theorem :: REWRITE2:22
  S c= ==>.-relation(S);

theorem :: REWRITE2:23
  p is RedSequence of ==>.-relation(S) implies p +^ u is
  RedSequence of ==>.-relation(S) & u ^+ p is RedSequence of ==>.-relation(S);

theorem :: REWRITE2:24
  p is RedSequence of ==>.-relation(S) implies t ^+ p +^ u is
  RedSequence of ==>.-relation(S);

theorem :: REWRITE2:25
  S is Thue-system of E implies ==>.-relation(S) = (==>.-relation( S))~;

theorem :: REWRITE2:26
  S c= T implies ==>.-relation(S) c= ==>.-relation(T);

theorem :: REWRITE2:27
  ==>.-relation(id (E^omega)) = id (E^omega);

theorem :: REWRITE2:28
  ==>.-relation(S \/ id (E^omega)) = ==>.-relation(S) \/ id (E ^omega);

theorem :: REWRITE2:29
  ==>.-relation({}(E^omega, E^omega)) = {}(E^omega, E^omega);

theorem :: REWRITE2:30
  s ==>. t, ==>.-relation(S) implies s ==>. t, S;

theorem :: REWRITE2:31
  ==>.-relation(==>.-relation(S)) = ==>.-relation(S);

begin :: Derivations.

definition
  let E, S, s, t;
  pred s ==>* t, S means
:: REWRITE2:def 7

  ==>.-relation(S) reduces s, t;
end;

theorem :: REWRITE2:32
  s ==>* s, S;

theorem :: REWRITE2:33
  s ==>. t, S implies s ==>* t, S;

theorem :: REWRITE2:34
  s -->. t, S implies s ==>* t, S;

theorem :: REWRITE2:35
  s ==>* t, S & t ==>* u, S implies s ==>* u, S;

theorem :: REWRITE2:36
  s ==>* t, S implies s^u ==>* t^u, S & u^s ==>* u^t, S;

theorem :: REWRITE2:37
  s ==>* t, S implies u^s^v ==>* u^t^v, S;

theorem :: REWRITE2:38
  s ==>* t, S & u ==>* v, S implies s^u ==>* t^v, S & u^s ==>* v^t, S;

theorem :: REWRITE2:39
  S is Thue-system of E & s ==>* t, S implies t ==>* s, S;

theorem :: REWRITE2:40
  S c= T & s ==>* t, S implies s ==>* t, T;

theorem :: REWRITE2:41
  s ==>* t, S iff s ==>* t, S \/ id (E^omega);

theorem :: REWRITE2:42
  s ==>* t, {}(E^omega, E^omega) implies s = t;

theorem :: REWRITE2:43
  s ==>* t, ==>.-relation(S) implies s ==>* t, S;

theorem :: REWRITE2:44
  s ==>* t, S & u ==>. v, {[s, t]} implies u ==>* v, S;

theorem :: REWRITE2:45
  s ==>* t, S & u ==>* v, S \/ {[s, t]} implies u ==>* v, S;

begin :: Languages generated by semi-Thue systems.

definition
  let E, S, w;
  func Lang(w, S) -> Subset of E^omega equals
:: REWRITE2:def 8
  { s : w ==>* s, S };
end;

theorem :: REWRITE2:46
  s in Lang(w, S) iff w ==>* s, S;

theorem :: REWRITE2:47
  w in Lang(w, S);

registration
  let E be non empty set;
  let S be semi-Thue-system of E;
  let w be Element of E^omega;
  cluster Lang(w, S) -> non empty;
end;

theorem :: REWRITE2:48
  S c= T implies Lang(w, S) c= Lang(w, T);

theorem :: REWRITE2:49
  Lang(w, S) = Lang(w, S \/ id (E^omega));

theorem :: REWRITE2:50
  Lang(w, {}(E^omega, E^omega)) = {w};

theorem :: REWRITE2:51
  Lang(w, id (E^omega)) = {w};

begin :: Equivalence of semi-Thue systems.

definition
  let E, S, T, w;
  pred S, T are_equivalent_wrt w means
:: REWRITE2:def 9

  Lang(w, S) = Lang(w, T);
end;

theorem :: REWRITE2:52
  S, S are_equivalent_wrt w;

theorem :: REWRITE2:53
  S, T are_equivalent_wrt w implies T, S are_equivalent_wrt w;

theorem :: REWRITE2:54
  S, T are_equivalent_wrt w & T, U are_equivalent_wrt w implies S, U
  are_equivalent_wrt w;

theorem :: REWRITE2:55
  S, S \/ id (E^omega) are_equivalent_wrt w;

theorem :: REWRITE2:56
  S, T are_equivalent_wrt w & S c= U & U c= T implies S, U
  are_equivalent_wrt w & U, T are_equivalent_wrt w;

theorem :: REWRITE2:57
  S, ==>.-relation(S) are_equivalent_wrt w;

theorem :: REWRITE2:58
  S, T are_equivalent_wrt w & ==>.-relation(S \/ T) reduces w, s
  implies ==>.-relation(S) reduces w, s;

theorem :: REWRITE2:59
  S, T are_equivalent_wrt w & w ==>* s, S \/ T implies w ==>* s, S;

theorem :: REWRITE2:60
  S, T are_equivalent_wrt w implies S, S \/ T are_equivalent_wrt w;

theorem :: REWRITE2:61
  s ==>. t, S implies S, (S \/ {[s, t]}) are_equivalent_wrt w;

theorem :: REWRITE2:62
  s ==>* t, S implies S, (S \/ {[s, t]}) are_equivalent_wrt w;