:: Formal Languages -- Concatenation and Closure :: by Micha{\l} Trybulec :: :: Received March 9, 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, SUBSET_1, AFINSQ_1, NAT_1, ORDINAL4, XBOOLE_0, TARSKI, RELAT_1, FUNCT_1, ZFMISC_1, XXREAL_0, ARYTM_3, CARD_1, FINSEQ_1, PRE_POLY, NEWTON, SETFAM_1, FLANG_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, FUNCT_1, RELSET_1, FUNCT_2, SETFAM_1, XXREAL_0, NAT_1, AFINSQ_1, CATALAN2; constructors XREAL_0, NAT_1, CATALAN2, RELSET_1; registrations XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, XXREAL_0, XREAL_0, NAT_1, AFINSQ_1, CATALAN2, FUNCT_1, FINSET_1; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin reserve E, x, y, X for set; reserve A, B, C, D for Subset of E^omega; reserve a, a1, a2, b, c, c1, c2, d, ab, bc for Element of E^omega; reserve e for Element of E; reserve i, j, k, l, n, n1, n2, m for Nat; :: Preliminaries - Redefinitions definition let E, a, b; redefine func a ^ b -> Element of E^omega; end; definition let E; redefine func <%>E -> Element of E^omega; end; definition let E be non empty set; let e be Element of E; redefine func <%e%> -> Element of E^omega; end; definition let E, a; redefine func {a} -> Subset of E^omega; end; definition let E; let f be sequence of bool E; let n; redefine func f.n -> Subset of E; end; :: Preliminaries - Numbers: theorem :: FLANG_1:1 n1 > n or n2 > n implies n1 + n2 > n; theorem :: FLANG_1:2 n1 + n <= n2 + 1 & n > 0 implies n1 <= n2; theorem :: FLANG_1:3 n1 + n2 = 1 iff n1 = 1 & n2 = 0 or n1 = 0 & n2 = 1; :: Preliminaries - Sequences: theorem :: FLANG_1:4 a ^ b = <%x%> iff a = <%>E & b = <%x%> or b = <%>E & a = <%x%>; theorem :: FLANG_1:5 for p, q being XFinSequence holds a = p ^ q implies p is Element of E^omega & q is Element of E^omega; theorem :: FLANG_1:6 for x being object holds <%x%> is Element of E^omega implies x in E; theorem :: FLANG_1:7 len b = n + 1 implies ex c, e st len c = n & b = c ^ <%e%>; theorem :: FLANG_1:8 for p being XFinSequence st p <> {} ex q being XFinSequence, x being object st p = <%x%> ^ q; theorem :: FLANG_1:9 len b = n + 1 implies ex c, e st len c = n & b = <%e%> ^ c; theorem :: FLANG_1:10 len b = n + m implies ex c1, c2 st len c1 = n & len c2 = m & b = c1 ^ c2; theorem :: FLANG_1:11 a ^ a = a implies a = {}; begin :: Concatenation of Languages :: Definition of ^^ definition let E, A, B; func A ^^ B -> Subset of E^omega means :: FLANG_1:def 1 x in it iff ex a, b st a in A & b in B & x = a ^ b; end; :: Concatenation of Languages :: Properties of ^^ theorem :: FLANG_1:12 A ^^ B = {} iff A = {} or B = {}; theorem :: FLANG_1:13 A ^^ {<%>E} = A & {<%>E} ^^ A = A; theorem :: FLANG_1:14 A ^^ B = {<%>E} iff A = {<%>E} & B = {<%>E}; theorem :: FLANG_1:15 <%>E in A ^^ B iff <%>E in A & <%>E in B; theorem :: FLANG_1:16 <%>E in B implies A c= A ^^ B & A c= B ^^ A; theorem :: FLANG_1:17 A c= C & B c= D implies A ^^ B c= C ^^ D; theorem :: FLANG_1:18 (A ^^ B) ^^ C = A ^^ (B ^^ C); theorem :: FLANG_1:19 A ^^ (B /\ C) c= (A ^^ B) /\ (A ^^ C) & (B /\ C) ^^ A c= (B ^^ A ) /\ (C ^^ A); theorem :: FLANG_1:20 A ^^ B \/ A ^^ C = A ^^ (B \/ C) & B ^^ A \/ C ^^ A = (B \/ C) ^^ A; theorem :: FLANG_1:21 (A ^^ B) \ (A ^^ C) c= A ^^ (B \ C) & (B ^^ A) \ (C ^^ A) c= (B \ C) ^^ A; theorem :: FLANG_1:22 (A ^^ B) \+\ (A ^^ C) c= A ^^ (B \+\ C) & (B ^^ A) \+\ (C ^^ A) c= (B \+\ C) ^^ A; begin :: Concatenation of a Language with Itself :: Definition of |^ definition let E, A, n; func A |^ n -> Subset of E^omega means :: FLANG_1:def 2 ex concat being sequence of bool (E^omega) st it = concat.n & concat.0 = {<%>E} & for i holds concat.( i + 1) = concat.i ^^ A; end; :: Concatenation of a Language with Itself :: Properties of |^ theorem :: FLANG_1:23 A |^ (n + 1) = (A |^ n) ^^ A; theorem :: FLANG_1:24 A |^ 0 = {<%>E}; theorem :: FLANG_1:25 A |^ 1 = A; theorem :: FLANG_1:26 A |^ 2 = A ^^ A; theorem :: FLANG_1:27 A |^ n = {} iff n > 0 & A = {}; theorem :: FLANG_1:28 {<%>E} |^ n = {<%>E}; theorem :: FLANG_1:29 A |^ n = {<%>E} iff n = 0 or A = {<%>E}; theorem :: FLANG_1:30 <%>E in A implies <%>E in A |^ n; theorem :: FLANG_1:31 <%>E in A |^ n & n > 0 implies <%>E in A; theorem :: FLANG_1:32 (A |^ n) ^^ A = A ^^ (A |^ n); theorem :: FLANG_1:33 A |^ (m + n) = (A |^ m) ^^ (A |^ n); theorem :: FLANG_1:34 (A |^ m) |^ n = A |^ (m * n); theorem :: FLANG_1:35 <%>E in A & n > 0 implies A c= A |^ n; theorem :: FLANG_1:36 <%>E in A & m > n implies A |^ n c= A |^ m; theorem :: FLANG_1:37 A c= B implies A |^ n c= B |^ n; theorem :: FLANG_1:38 (A |^ n) \/ (B |^ n) c= (A \/ B) |^ n; theorem :: FLANG_1:39 (A /\ B) |^ n c= (A |^ n) /\ (B |^ n); theorem :: FLANG_1:40 a in C |^ m & b in C |^ n implies a ^ b in C |^ (m + n); begin :: Kleene Closure :: Definition of * definition let E, A; func A* -> Subset of E^omega equals :: FLANG_1:def 3 union { B : ex n st B = A |^ n }; end; :: Kleene Closure :: Properties of * theorem :: FLANG_1:41 x in A* iff ex n st x in A |^ n; theorem :: FLANG_1:42 A |^ n c= A*; theorem :: FLANG_1:43 A c= A*; theorem :: FLANG_1:44 A ^^ A c= A*; theorem :: FLANG_1:45 a in C* & b in C* implies a ^ b in C*; theorem :: FLANG_1:46 A c= C* & B c= C* implies A ^^ B c= C*; theorem :: FLANG_1:47 A* = {<%>E} iff A = {} or A = {<%>E}; theorem :: FLANG_1:48 <%>E in A*; theorem :: FLANG_1:49 A* = {x} implies x = <%>E; theorem :: FLANG_1:50 x in A |^ (m + 1) implies x in (A*) ^^ A & x in A ^^ (A*); theorem :: FLANG_1:51 A |^ (m + 1) c= (A*) ^^ A & A |^ (m + 1) c= A ^^ (A*); theorem :: FLANG_1:52 x in (A*) ^^ A or x in A ^^ (A*) implies x in A*; theorem :: FLANG_1:53 (A*) ^^ A c= A* & A ^^ (A*) c= A*; theorem :: FLANG_1:54 <%>E in A implies A* = (A*) ^^ A & A* = A ^^ (A*); theorem :: FLANG_1:55 <%>E in A implies A* = (A*) ^^ (A |^ n) & A* = (A |^ n) ^^ (A*); theorem :: FLANG_1:56 A* = {<%>E} \/ A ^^ (A*) & A* = {<%>E} \/ (A*) ^^ A; theorem :: FLANG_1:57 A ^^ (A*) = (A*) ^^ A; theorem :: FLANG_1:58 (A |^ n) ^^ (A*) = (A*) ^^ (A |^ n); theorem :: FLANG_1:59 A c= B* implies A |^ n c= B*; theorem :: FLANG_1:60 A c= B* implies A* c= B*; theorem :: FLANG_1:61 A c= B implies A* c= B*; theorem :: FLANG_1:62 (A*)* = A*; theorem :: FLANG_1:63 (A*) ^^ (A*) = A*; theorem :: FLANG_1:64 (A |^ n)* c= A*; theorem :: FLANG_1:65 (A*) |^ n c= A*; theorem :: FLANG_1:66 n > 0 implies (A*) |^ n = A*; theorem :: FLANG_1:67 A c= B* implies B* = (B \/ A)*; theorem :: FLANG_1:68 a in A* implies A* = (A \/ {a})*; theorem :: FLANG_1:69 A* = (A \ {<%>E})*; theorem :: FLANG_1:70 (A*) \/ (B*) c= (A \/ B)*; theorem :: FLANG_1:71 (A /\ B)* c= (A*) /\ (B*); theorem :: FLANG_1:72 <%x%> in A* iff <%x%> in A; begin :: Lexemes as a Subset of E^omega :: Definition of Lex definition let E; func Lex(E) -> Subset of E^omega means :: FLANG_1:def 4 x in it iff ex e st e in E & x = <%e%>; end; :: Lexemes as a Subset of E^omega :: Properties of Lex theorem :: FLANG_1:73 a in Lex(E) |^ len a; theorem :: FLANG_1:74 Lex(E)* = E^omega; theorem :: FLANG_1:75 A* = E^omega implies Lex(E) c= A;