:: Formal Languages -- Concatenation and Closure
:: by Micha{\l} Trybulec
::
:: Received March 9, 2007
:: Copyright (c) 2007-2021 Association of Mizar Users

:: Preliminaries - Redefinitions

definition

let E be set ;
let a, b be Element of E ^omega ;
:: original: ^
redefine func a ^ b -> Element of E ^omega ;
coherence
a ^ b is Element of E ^omega by AFINSQ_1:def 7;

end;

definition

let E be set ;
:: original: <%>
redefine func <%> E -> Element of E ^omega ;
coherence
<%> E is Element of E ^omega by AFINSQ_1:def 7;

end;

definition

let E be non empty set ;
let e be Element of E;
:: original: <%
redefine func <%e%> -> Element of E ^omega ;
coherence
<%e%> is Element of E ^omega by AFINSQ_1:def 7;

end;

definition

let E be set ;
let a be Element of E ^omega ;
:: original: {
redefine func {a} -> Subset of (E ^omega);
coherence
{a} is Subset of (E ^omega) by SUBSET_1:33;

end;

definition

let E be set ;
let f be sequence of (bool E);
let n be Nat;
:: original: .
redefine func f . n -> Subset of E;
coherence
f . n is Subset of E

proof end;

end;

:: Preliminaries - Numbers:

theorem Th1: :: FLANG_1:1

for n, n1, n2 being Nat st ( n1 > n or n2 > n ) holds
n1 + n2 > n

proof end;

theorem Th2: :: FLANG_1:2

for n, n1, n2 being Nat st n1 + n <= n2 + 1 & n > 0 holds
n1 <= n2

proof end;

theorem Th3: :: FLANG_1:3

for n1, n2 being Nat holds
( n1 + n2 = 1 iff ( ( n1 = 1 & n2 = 0 ) or ( n1 = 0 & n2 = 1 ) ) )

proof end;

:: Preliminaries - Sequences:

theorem Th4: :: FLANG_1:4

for E, x being set
for a, b being Element of E ^omega holds
( a ^ b = <%x%> iff ( ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) ) )

proof end;

theorem Th5: :: FLANG_1:5

for E being set
for a being Element of E ^omega
for p, q being XFinSequence st a = p ^ q holds
( p is Element of E ^omega & q is Element of E ^omega )

proof end;

theorem Th6: :: FLANG_1:6

for E being set
for x being object st <%x%> is Element of E ^omega holds
x in E

proof end;

theorem Th7: :: FLANG_1:7

for E being set
for b being Element of E ^omega
for n being Nat st len b = n + 1 holds
ex c being Element of E ^omega ex e being Element of E st
( len c = n & b = c ^ <%e%> )

proof end;

theorem Th8: :: FLANG_1:8

for p being XFinSequence st p <> {} holds
ex q being XFinSequence ex x being object st p = <%x%> ^ q

proof end;

theorem :: FLANG_1:9

for E being set
for b being Element of E ^omega
for n being Nat st len b = n + 1 holds
ex c being Element of E ^omega ex e being Element of E st
( len c = n & b = <%e%> ^ c )

proof end;

Lm1: for i, j being Nat
for p being XFinSequence st len p = i + j holds
ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 )
by AFINSQ_1:61;

theorem :: FLANG_1:10

for E being set
for b being Element of E ^omega
for n, m being Nat st len b = n + m holds
ex c1, c2 being Element of E ^omega st
( len c1 = n & len c2 = m & b = c1 ^ c2 )

proof end;

theorem Th11: :: FLANG_1:11

for E being set
for a being Element of E ^omega st a ^ a = a holds
a = {}

proof end;

:: Concatenation of Languages
:: Definition of ^^

definition

let E be set ;
let A, B be Subset of (E ^omega);

func A ^^ B -> Subset of (E ^omega) means :Def1: :: FLANG_1:def 1
for x being set holds
( x in it iff ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) );

existence
ex b₁ being Subset of (E ^omega) st
for x being set holds
( x in b₁ iff ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) )

proof end;

uniqueness
for b₁, b₂ being Subset of (E ^omega) st ( for x being set holds
( x in b₁ iff ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) ) ) & ( for x being set holds
( x in b₂ iff ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines ^^ FLANG_1:def 1 :
for E being set
for A, B, b₄ being Subset of (E ^omega) holds
( b₄ = A ^^ B iff for x being set holds
( x in b₄ iff ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) ) );

:: Concatenation of Languages
:: Properties of ^^

theorem Th12: :: FLANG_1:12

for E being set
for A, B being Subset of (E ^omega) holds
( A ^^ B = {} iff ( A = {} or B = {} ) )

proof end;

theorem Th13: :: FLANG_1:13

for E being set
for A being Subset of (E ^omega) holds
( A ^^ {(<%> E)} = A & {(<%> E)} ^^ A = A )

proof end;

theorem Th14: :: FLANG_1:14

for E being set
for A, B being Subset of (E ^omega) holds
( A ^^ B = {(<%> E)} iff ( A = {(<%> E)} & B = {(<%> E)} ) )

proof end;

theorem Th15: :: FLANG_1:15

for E being set
for A, B being Subset of (E ^omega) holds
( <%> E in A ^^ B iff ( <%> E in A & <%> E in B ) )

proof end;

theorem Th16: :: FLANG_1:16

for E being set
for A, B being Subset of (E ^omega) st <%> E in B holds
( A c= A ^^ B & A c= B ^^ A )

proof end;

theorem Th17: :: FLANG_1:17

for E being set
for A, B, C, D being Subset of (E ^omega) st A c= C & B c= D holds
A ^^ B c= C ^^ D

proof end;

theorem Th18: :: FLANG_1:18

for E being set
for A, B, C being Subset of (E ^omega) holds (A ^^ B) ^^ C = A ^^ (B ^^ C)

proof end;

theorem Th19: :: FLANG_1:19

for E being set
for A, B, C being Subset of (E ^omega) holds
( A ^^ (B /\ C) c= (A ^^ B) /\ (A ^^ C) & (B /\ C) ^^ A c= (B ^^ A) /\ (C ^^ A) )

proof end;

theorem Th20: :: FLANG_1:20

for E being set
for A, B, C being Subset of (E ^omega) holds
( (A ^^ B) \/ (A ^^ C) = A ^^ (B \/ C) & (B ^^ A) \/ (C ^^ A) = (B \/ C) ^^ A )

proof end;

theorem Th21: :: FLANG_1:21

for E being set
for A, B, C being Subset of (E ^omega) holds
( (A ^^ B) \ (A ^^ C) c= A ^^ (B \ C) & (B ^^ A) \ (C ^^ A) c= (B \ C) ^^ A )

proof end;

theorem :: FLANG_1:22

for E being set
for A, B, C being Subset of (E ^omega) holds
( (A ^^ B) \+\ (A ^^ C) c= A ^^ (B \+\ C) & (B ^^ A) \+\ (C ^^ A) c= (B \+\ C) ^^ A )

proof end;

:: Concatenation of a Language with Itself
:: Definition of |^

definition

let E be set ;
let A be Subset of (E ^omega);
let n be Nat;

func A |^ n -> Subset of (E ^omega) means :Def2: :: FLANG_1:def 2
ex concat being sequence of (bool (E ^omega)) st
( it = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) );

existence
ex b₁ being Subset of (E ^omega) ex concat being sequence of (bool (E ^omega)) st
( b₁ = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) )

proof end;

uniqueness
for b₁, b₂ being Subset of (E ^omega) st ex concat being sequence of (bool (E ^omega)) st
( b₁ = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) & ex concat being sequence of (bool (E ^omega)) st
( b₂ = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines |^ FLANG_1:def 2 :
for E being set
for A being Subset of (E ^omega)
for n being Nat
for b₄ being Subset of (E ^omega) holds
( b₄ = A |^ n iff ex concat being sequence of (bool (E ^omega)) st
( b₄ = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) );

:: Concatenation of a Language with Itself
:: Properties of |^

theorem Th23: :: FLANG_1:23

for E being set
for A being Subset of (E ^omega)
for n being Nat holds A |^ (n + 1) = (A |^ n) ^^ A

proof end;

theorem Th24: :: FLANG_1:24

for E being set
for A being Subset of (E ^omega) holds A |^ 0 = {(<%> E)}

proof end;

theorem Th25: :: FLANG_1:25

for E being set
for A being Subset of (E ^omega) holds A |^ 1 = A

proof end;

theorem Th26: :: FLANG_1:26

for E being set
for A being Subset of (E ^omega) holds A |^ 2 = A ^^ A

proof end;

theorem Th27: :: FLANG_1:27

for E being set
for A being Subset of (E ^omega)
for n being Nat holds
( A |^ n = {} iff ( n > 0 & A = {} ) )

proof end;

theorem Th28: :: FLANG_1:28

for E being set
for n being Nat holds {(<%> E)} |^ n = {(<%> E)}

proof end;

theorem :: FLANG_1:29

for E being set
for A being Subset of (E ^omega)
for n being Nat holds
( A |^ n = {(<%> E)} iff ( n = 0 or A = {(<%> E)} ) )

proof end;

theorem Th30: :: FLANG_1:30

for E being set
for A being Subset of (E ^omega)
for n being Nat st <%> E in A holds
<%> E in A |^ n

proof end;

theorem :: FLANG_1:31

for E being set
for A being Subset of (E ^omega)
for n being Nat st <%> E in A |^ n & n > 0 holds
<%> E in A

proof end;

theorem Th32: :: FLANG_1:32

for E being set
for A being Subset of (E ^omega)
for n being Nat holds (A |^ n) ^^ A = A ^^ (A |^ n)

proof end;

theorem Th33: :: FLANG_1:33

for E being set
for A being Subset of (E ^omega)
for n, m being Nat holds A |^ (m + n) = (A |^ m) ^^ (A |^ n)

proof end;

theorem :: FLANG_1:34

for E being set
for A being Subset of (E ^omega)
for n, m being Nat holds (A |^ m) |^ n = A |^ (m * n)

proof end;

theorem Th35: :: FLANG_1:35

for E being set
for A being Subset of (E ^omega)
for n being Nat st <%> E in A & n > 0 holds
A c= A |^ n

proof end;

theorem :: FLANG_1:36

for E being set
for A being Subset of (E ^omega)
for n, m being Nat st <%> E in A & m > n holds
A |^ n c= A |^ m

proof end;

theorem Th37: :: FLANG_1:37

for E being set
for A, B being Subset of (E ^omega)
for n being Nat st A c= B holds
A |^ n c= B |^ n

proof end;

theorem :: FLANG_1:38

for E being set
for A, B being Subset of (E ^omega)
for n being Nat holds (A |^ n) \/ (B |^ n) c= (A \/ B) |^ n

proof end;

theorem :: FLANG_1:39

for E being set
for A, B being Subset of (E ^omega)
for n being Nat holds (A /\ B) |^ n c= (A |^ n) /\ (B |^ n)

proof end;

theorem Th40: :: FLANG_1:40

for E being set
for C being Subset of (E ^omega)
for a, b being Element of E ^omega
for n, m being Nat st a in C |^ m & b in C |^ n holds
a ^ b in C |^ (m + n)

proof end;

:: Kleene Closure
:: Definition of *

definition

let E be set ;
let A be Subset of (E ^omega);

func A * -> Subset of (E ^omega) equals :: FLANG_1:def 3
union { B where B is Subset of (E ^omega) : ex n being Nat st B = A |^ n } ;

coherence
union { B where B is Subset of (E ^omega) : ex n being Nat st B = A |^ n } is Subset of (E ^omega)

proof end;

end;

:: deftheorem defines * FLANG_1:def 3 :
for E being set
for A being Subset of (E ^omega) holds A * = union { B where B is Subset of (E ^omega) : ex n being Nat st B = A |^ n } ;

:: Kleene Closure
:: Properties of *

theorem Th41: :: FLANG_1:41

for E, x being set
for A being Subset of (E ^omega) holds
( x in A * iff ex n being Nat st x in A |^ n )

proof end;

theorem Th42: :: FLANG_1:42

for E being set
for A being Subset of (E ^omega)
for n being Nat holds A |^ n c= A *

proof end;

theorem Th43: :: FLANG_1:43

for E being set
for A being Subset of (E ^omega) holds A c= A *

proof end;

theorem :: FLANG_1:44

for E being set
for A being Subset of (E ^omega) holds A ^^ A c= A *

proof end;

theorem Th45: :: FLANG_1:45

for E being set
for C being Subset of (E ^omega)
for a, b being Element of E ^omega st a in C * & b in C * holds
a ^ b in C *

proof end;

theorem Th46: :: FLANG_1:46

for E being set
for A, B, C being Subset of (E ^omega) st A c= C * & B c= C * holds
A ^^ B c= C *

proof end;

theorem :: FLANG_1:47

for E being set
for A being Subset of (E ^omega) holds
( A * = {(<%> E)} iff ( A = {} or A = {(<%> E)} ) )

proof end;

theorem Th48: :: FLANG_1:48

for E being set
for A being Subset of (E ^omega) holds <%> E in A *

proof end;

theorem :: FLANG_1:49

for E, x being set
for A being Subset of (E ^omega) st A * = {x} holds
x = <%> E

proof end;

theorem Th50: :: FLANG_1:50

for E, x being set
for A being Subset of (E ^omega)
for m being Nat st x in A |^ (m + 1) holds
( x in (A *) ^^ A & x in A ^^ (A *) )

proof end;

theorem :: FLANG_1:51

for E being set
for A being Subset of (E ^omega)
for m being Nat holds
( A |^ (m + 1) c= (A *) ^^ A & A |^ (m + 1) c= A ^^ (A *) ) by Th50;

theorem Th52: :: FLANG_1:52

for E, x being set
for A being Subset of (E ^omega) st ( x in (A *) ^^ A or x in A ^^ (A *) ) holds
x in A *

proof end;

theorem :: FLANG_1:53

for E being set
for A being Subset of (E ^omega) holds
( (A *) ^^ A c= A * & A ^^ (A *) c= A * ) by Th52;

theorem Th54: :: FLANG_1:54

for E being set
for A being Subset of (E ^omega) st <%> E in A holds
( A * = (A *) ^^ A & A * = A ^^ (A *) )

proof end;

theorem :: FLANG_1:55

for E being set
for A being Subset of (E ^omega)
for n being Nat st <%> E in A holds
( A * = (A *) ^^ (A |^ n) & A * = (A |^ n) ^^ (A *) )

proof end;

theorem Th56: :: FLANG_1:56

for E being set
for A being Subset of (E ^omega) holds
( A * = {(<%> E)} \/ (A ^^ (A *)) & A * = {(<%> E)} \/ ((A *) ^^ A) )

proof end;

theorem Th57: :: FLANG_1:57

for E being set
for A being Subset of (E ^omega) holds A ^^ (A *) = (A *) ^^ A

proof end;

theorem :: FLANG_1:58

for E being set
for A being Subset of (E ^omega)
for n being Nat holds (A |^ n) ^^ (A *) = (A *) ^^ (A |^ n)

proof end;

theorem Th59: :: FLANG_1:59

for E being set
for A, B being Subset of (E ^omega)
for n being Nat st A c= B * holds
A |^ n c= B *

proof end;

theorem Th60: :: FLANG_1:60

for E being set
for A, B being Subset of (E ^omega) st A c= B * holds
A * c= B *

proof end;

theorem Th61: :: FLANG_1:61

for E being set
for A, B being Subset of (E ^omega) st A c= B holds
A * c= B *

proof end;

theorem Th62: :: FLANG_1:62

for E being set
for A being Subset of (E ^omega) holds (A *) * = A *

proof end;

theorem :: FLANG_1:63

for E being set
for A being Subset of (E ^omega) holds (A *) ^^ (A *) = A *

proof end;

theorem :: FLANG_1:64

for E being set
for A being Subset of (E ^omega)
for n being Nat holds (A |^ n) * c= A * by Th42, Th60;

theorem Th65: :: FLANG_1:65

for E being set
for A being Subset of (E ^omega)
for n being Nat holds (A *) |^ n c= A *

proof end;

theorem :: FLANG_1:66

for E being set
for A being Subset of (E ^omega)
for n being Nat st n > 0 holds
(A *) |^ n = A *

proof end;

theorem Th67: :: FLANG_1:67

for E being set
for A, B being Subset of (E ^omega) st A c= B * holds
B * = (B \/ A) *

proof end;

theorem Th68: :: FLANG_1:68

for E being set
for A being Subset of (E ^omega)
for a being Element of E ^omega st a in A * holds
A * = (A \/ {a}) * by ZFMISC_1:31, Th67;

theorem :: FLANG_1:69

for E being set
for A being Subset of (E ^omega) holds A * = (A \ {(<%> E)}) *

proof end;

theorem :: FLANG_1:70

for E being set
for A, B being Subset of (E ^omega) holds (A *) \/ (B *) c= (A \/ B) *

proof end;

theorem :: FLANG_1:71

for E being set
for A, B being Subset of (E ^omega) holds (A /\ B) * c= (A *) /\ (B *)

proof end;

theorem Th72: :: FLANG_1:72

for E, x being set
for A being Subset of (E ^omega) holds
( <%x%> in A * iff <%x%> in A )

proof end;

:: Lexemes as a Subset of E^omega
:: Definition of Lex

definition

let E be set ;

func Lex E -> Subset of (E ^omega) means :Def4: :: FLANG_1:def 4
for x being set holds
( x in it iff ex e being Element of E st
( e in E & x = <%e%> ) );

existence
ex b₁ being Subset of (E ^omega) st
for x being set holds
( x in b₁ iff ex e being Element of E st
( e in E & x = <%e%> ) )

proof end;

uniqueness
for b₁, b₂ being Subset of (E ^omega) st ( for x being set holds
( x in b₁ iff ex e being Element of E st
( e in E & x = <%e%> ) ) ) & ( for x being set holds
( x in b₂ iff ex e being Element of E st
( e in E & x = <%e%> ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines Lex FLANG_1:def 4 :
for E being set
for b₂ being Subset of (E ^omega) holds
( b₂ = Lex E iff for x being set holds
( x in b₂ iff ex e being Element of E st
( e in E & x = <%e%> ) ) );

:: Lexemes as a Subset of E^omega
:: Properties of Lex

theorem Th73: :: FLANG_1:73

for E being set
for a being Element of E ^omega holds a in (Lex E) |^ (len a)

proof end;

theorem :: FLANG_1:74

for E being set holds (Lex E) * = E ^omega

proof end;

theorem :: FLANG_1:75

for E being set
for A being Subset of (E ^omega) st A * = E ^omega holds
Lex E c= A

proof end;