:: 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 b1 being Subset of (E ^omega) st
for x being set holds
( x in b1 iff ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) )
proof end;
uniqueness
for b1, b2 being Subset of (E ^omega) st ( for x being set holds
( x in b1 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 b2 iff ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines ^^ FLANG_1:def 1 :
for E being set
for A, B, b4 being Subset of (E ^omega) holds
( b4 = A ^^ B iff for x being set holds
( x in b4 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 b1 being Subset of (E ^omega) ex concat being sequence of (bool (E ^omega)) st
( b1 = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) )
proof end;
uniqueness
for b1, b2 being Subset of (E ^omega) st ex concat being sequence of (bool (E ^omega)) st
( b1 = 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
( b2 = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) holds
b1 = b2
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 b4 being Subset of (E ^omega) holds
( b4 = A |^ n iff ex concat being sequence of (bool (E ^omega)) st
( b4 = 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 b1 being Subset of (E ^omega) st
for x being set holds
( x in b1 iff ex e being Element of E st
( e in E & x = <%e%> ) )
proof end;
uniqueness
for b1, b2 being Subset of (E ^omega) st ( for x being set holds
( x in b1 iff ex e being Element of E st
( e in E & x = <%e%> ) ) ) & ( for x being set holds
( x in b2 iff ex e being Element of E st
( e in E & x = <%e%> ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines Lex FLANG_1:def 4 :
for E being set
for b2 being Subset of (E ^omega) holds
( b2 = Lex E iff for x being set holds
( x in b2 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;