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


begin

:: Preliminaries - Redefinitions
definition
let E be set ;
let a, b be Element of E ^omega ;
:: original:^
redefine funca ^ 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 Function of NAT,(bool E);
let n be Nat;
:: original:.
redefine funcf . n ->  Subset of E;
coherence
 f . n is Subset of E
proofend;
end;

:: Preliminaries - Numbers:
theorem Th1: :: FLANG_1:1
for n1, n, n2 being Nat st ( n1 > n or n2 > n ) holds
n1 + n2 > n
proofend;

theorem Th2: :: FLANG_1:2
for n1, n, n2 being Nat st n1 + n <= n2 + 1 &amp; n > 0 holds
n1 <= n2
proofend;

theorem Th3: :: FLANG_1:3
for n1, n2 being Nat holds
( n1 + n2 = 1 iff ( ( n1 = 1 &amp; n2 = 0 ) or ( n1 = 0 &amp; n2 = 1 ) ) )
proofend;

:: Preliminaries - Sequences:
theorem Th4: :: FLANG_1:4
for x, E being set
for a, b being Element of E ^omega holds
( a ^ b = <%x%> iff ( ( a = <%> E &amp; b = <%x%> ) or ( b = <%> E &amp; a = <%x%> ) ) )
proofend;

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 &amp; q is Element of E ^omega )
proofend;

theorem Th6: :: FLANG_1:6
for x, E being set st <%x%> is Element of E ^omega holds
x in E
proofend;

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 &amp; b = c ^ <%e%> )
proofend;

theorem Th8: :: FLANG_1:8
for p being XFinSequence st p <> {} holds
ex q being XFinSequence ex x being set st p = <%x%> ^ q
proofend;

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 &amp; b = <%e%> ^ c )
proofend;

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 &amp; len q2 = j &amp; 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 &amp; len c2 = m &amp; b = c1 ^ c2 )
proofend;

theorem Th11: :: FLANG_1:11
for E being set
for a being Element of E ^omega st a ^ a = a holds
a = {}
proofend;

begin

:: Concatenation of Languages
:: Definition of ^^
definition
let E be set ;
let A, B be Subset of (E ^omega);
funcA ^^ 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 &amp; b in B &amp; 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 &amp; b in B &amp; x = a ^ b ) )
proofend;
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 &amp; b in B &amp; x = a ^ b ) ) ) &amp; ( for x being set holds
( x in b2 iff ex a, b being Element of E ^omega st
( a in A &amp; b in B &amp; x = a ^ b ) ) ) holds
b1 = b2
proofend;
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 &amp; b in B &amp; 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 = {} ) )
proofend;

theorem Th13: :: FLANG_1:13
for E being set
for A being Subset of (E ^omega) holds
( A ^^ {(<%> E)} = A &amp; {(<%> E)} ^^ A = A )
proofend;

theorem Th14: :: FLANG_1:14
for E being set
for A, B being Subset of (E ^omega) holds
( A ^^ B = {(<%> E)} iff ( A = {(<%> E)} &amp; B = {(<%> E)} ) )
proofend;

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 &amp; <%> E in B ) )
proofend;

theorem Th16: :: FLANG_1:16
for E being set
for B, A being Subset of (E ^omega) st <%> E in B holds
( A c= A ^^ B &amp; A c= B ^^ A )
proofend;

theorem Th17: :: FLANG_1:17
for E being set
for A, C, B, D being Subset of (E ^omega) st A c= C &amp; B c= D holds
A ^^ B c= C ^^ D
proofend;

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)
proofend;

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) &amp; (B /\ C) ^^ A c= (B ^^ A) /\ (C ^^ A) )
proofend;

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) &amp; (B ^^ A) \/ (C ^^ A) = (B \/ C) ^^ A )
proofend;

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) &amp; (B ^^ A) \ (C ^^ A) c= (B \ C) ^^ A )
proofend;

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) &amp; (B ^^ A) \+\ (C ^^ A) c= (B \+\ C) ^^ A )
proofend;

begin

:: Concatenation of a Language with Itself
:: Definition of |^
definition
let E be set ;
let A be Subset of (E ^omega);
let n be Nat;
funcA |^ n ->  Subset of (E ^omega) means :Def2: :: FLANG_1:def 2
 ex concat being Function of NAT,(bool (E ^omega)) st
( it = concat . n &amp; concat . 0 = {(<%> E)} &amp; ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) );
existence
 ex b1 being Subset of (E ^omega) ex concat being Function of NAT,(bool (E ^omega)) st
( b1 = concat . n &amp; concat . 0 = {(<%> E)} &amp; ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) )
proofend;
uniqueness
 for b1, b2 being Subset of (E ^omega) st ex concat being Function of NAT,(bool (E ^omega)) st
( b1 = concat . n &amp; concat . 0 = {(<%> E)} &amp; ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) &amp; ex concat being Function of NAT,(bool (E ^omega)) st
( b2 = concat . n &amp; concat . 0 = {(<%> E)} &amp; ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) holds
b1 = b2
proofend;
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 Function of NAT,(bool (E ^omega)) st
( b4 = concat . n &amp; concat . 0 = {(<%> E)} &amp; ( 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
proofend;

theorem Th24: :: FLANG_1:24
for E being set
for A being Subset of (E ^omega) holds A |^ 0 = {(<%> E)}
proofend;

theorem Th25: :: FLANG_1:25
for E being set
for A being Subset of (E ^omega) holds A |^ 1 = A
proofend;

theorem Th26: :: FLANG_1:26
for E being set
for A being Subset of (E ^omega) holds A |^ 2 = A ^^ A
proofend;

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 &amp; A = {} ) )
proofend;

theorem Th28: :: FLANG_1:28
for E being set
for n being Nat holds {(<%> E)} |^ n = {(<%> E)}
proofend;

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)} ) )
proofend;

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
proofend;

theorem :: FLANG_1:31
for E being set
for A being Subset of (E ^omega)
for n being Nat st <%> E in A |^ n &amp; n > 0 holds
<%> E in A
proofend;

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)
proofend;

theorem Th33: :: FLANG_1:33
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds A |^ (m + n) = (A |^ m) ^^ (A |^ n)
proofend;

theorem :: FLANG_1:34
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ m) |^ n = A |^ (m * n)
proofend;

theorem Th35: :: FLANG_1:35
for E being set
for A being Subset of (E ^omega)
for n being Nat st <%> E in A &amp; n > 0 holds
A c= A |^ n
proofend;

theorem :: FLANG_1:36
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st <%> E in A &amp; m > n holds
A |^ n c= A |^ m
proofend;

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
proofend;

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
proofend;

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)
proofend;

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 m, n being Nat st a in C |^ m &amp; b in C |^ n holds
a ^ b in C |^ (m + n)
proofend;

begin

:: Kleene Closure
:: Definition of *
definition
let E be set ;
let A be Subset of (E ^omega);
funcA *  ->  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)
proofend;
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 )
proofend;

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 *
proofend;

theorem Th43: :: FLANG_1:43
for E being set
for A being Subset of (E ^omega) holds A c= A *
proofend;

theorem :: FLANG_1:44
for E being set
for A being Subset of (E ^omega) holds A ^^ A c= A *
proofend;

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 * &amp; b in C * holds
a ^ b in C *
proofend;

theorem Th46: :: FLANG_1:46
for E being set
for A, C, B being Subset of (E ^omega) st A c= C * &amp; B c= C * holds
A ^^ B c= C *
proofend;

theorem :: FLANG_1:47
for E being set
for A being Subset of (E ^omega) holds
( A * = {(<%> E)} iff ( A = {} or A = {(<%> E)} ) )
proofend;

theorem Th48: :: FLANG_1:48
for E being set
for A being Subset of (E ^omega) holds <%> E in A *
proofend;

theorem :: FLANG_1:49
for x, E being set
for A being Subset of (E ^omega) st A * = {x} holds
x = <%> E
proofend;

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 &amp; x in A ^^ (A *) )
proofend;

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 &amp; A |^ (m + 1) c= A ^^ (A *) )
proofend;

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 *
proofend;

theorem :: FLANG_1:53
for E being set
for A being Subset of (E ^omega) holds
( (A *) ^^ A c= A * &amp; A ^^ (A *) c= A * )
proofend;

theorem Th54: :: FLANG_1:54
for E being set
for A being Subset of (E ^omega) st <%> E in A holds
( A * = (A *) ^^ A &amp; A * = A ^^ (A *) )
proofend;

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) &amp; A * = (A |^ n) ^^ (A *) )
proofend;

theorem Th56: :: FLANG_1:56
for E being set
for A being Subset of (E ^omega) holds
( A * = {(<%> E)} \/ (A ^^ (A *)) &amp; A * = {(<%> E)} \/ ((A *) ^^ A) )
proofend;

theorem Th57: :: FLANG_1:57
for E being set
for A being Subset of (E ^omega) holds A ^^ (A *) = (A *) ^^ A
proofend;

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)
proofend;

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 *
proofend;

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 *
proofend;

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 *
proofend;

theorem Th62: :: FLANG_1:62
for E being set
for A being Subset of (E ^omega) holds (A *) * = A *
proofend;

theorem :: FLANG_1:63
for E being set
for A being Subset of (E ^omega) holds (A *) ^^ (A *) = A *
proofend;

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 *
proofend;

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 *
proofend;

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) *
proofend;

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}) *
proofend;

theorem :: FLANG_1:69
for E being set
for A being Subset of (E ^omega) holds A * = (A \ {(<%> E)}) *
proofend;

theorem :: FLANG_1:70
for E being set
for A, B being Subset of (E ^omega) holds (A *) \/ (B *) c= (A \/ B) *
proofend;

theorem :: FLANG_1:71
for E being set
for A, B being Subset of (E ^omega) holds (A /\ B) * c= (A *) /\ (B *)
proofend;

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 )
proofend;

begin

:: 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 &amp; 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 &amp; x = <%e%> ) )
proofend;
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 &amp; x = <%e%> ) ) ) &amp; ( for x being set holds
( x in b2 iff ex e being Element of E st
( e in E &amp; x = <%e%> ) ) ) holds
b1 = b2
proofend;
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 &amp; 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)
proofend;

theorem :: FLANG_1:74
for E being set holds (Lex E) * = E ^omega
proofend;

theorem :: FLANG_1:75
for E being set
for A being Subset of (E ^omega) st A * = E ^omega holds
Lex E c= A
proofend;