1(*****************************************************************************) 2(* Formal Language Theory *) 3(* *) 4(* A formal language is a set of strings over an alphabet. The notion of *) 5(* 'a list exactly captures such strings. We define the following language *) 6(* operations: concatenation, iterated concatenation, and Kleene Star. We *) 7(* prove a collection of lemmas about these operations, including Arden's *) 8(* lemma. *) 9(*****************************************************************************) 10 11 12(*===========================================================================*) 13(* Load and open context theories and proof support (lists and sets). *) 14(*===========================================================================*) 15 16open HolKernel boolLib bossLib Parse; 17open pred_setLib pred_setTheory arithmeticTheory listTheory; 18 19val _ = new_theory "FormalLang"; 20 21(*---------------------------------------------------------------------------*) 22(* Basic simplification support *) 23(*---------------------------------------------------------------------------*) 24 25val APPEND_EQNS = LIST_CONJ [APPEND,APPEND_NIL,APPEND_eq_NIL]; 26 27val basic_ss = list_ss ++ PRED_SET_ss ++ rewrites [APPEND_EQNS]; 28 29 30(*---------------------------------------------------------------------------*) 31(* A language is a set of strings over an alphabet. A string is represented *) 32(* by an 'a list. *) 33(*---------------------------------------------------------------------------*) 34 35val _ = type_abbrev ("lang", ``:'a list set``); 36 37(*---------------------------------------------------------------------------*) 38(* Binary language concatenation. Right infix *) 39(*---------------------------------------------------------------------------*) 40 41val dot_def = 42 Define 43 `$dot A B = {x ++ y | x IN A /\ y IN B}`; 44 45val _ = set_fixity "dot" (Infixr 675); 46 47(*---------------------------------------------------------------------------*) 48(* Some lemmas about language concatenation. *) 49(*---------------------------------------------------------------------------*) 50 51val IN_dot = Q.store_thm 52("IN_dot", 53`!w A B. w IN (A dot B) <=> ?u v. (w = u ++ v) /\ u IN A /\ v IN B`, 54 RW_TAC basic_ss [dot_def]); 55 56val DOT_EMPTYSET = Q.store_thm 57("DOT_EMPTYSET", 58`!A. (A dot {} = {}) /\ ({} dot A = {})`, 59 RW_TAC basic_ss [dot_def,EXTENSION]); 60 61val DOT_EMPTYSTRING = Q.store_thm 62("DOT_EMPTYSTRING", 63`!A. (A dot {[]} = A) /\ ({[]} dot A = A)`, 64 RW_TAC basic_ss [dot_def,EXTENSION]); 65 66val STRCAT_IN_dot = Q.store_thm 67("STRCAT_IN_dot", 68`!a b A B. a IN A /\ b IN B ==> (a ++ b) IN (A dot B)`, 69 METIS_TAC[IN_dot]); 70 71val EMPTY_IN_DOT = Q.store_thm 72("EMPTY_IN_DOT", 73`!A B. [] IN (A dot B) <=> [] IN A /\ [] IN B`, 74 METIS_TAC [IN_dot,APPEND_EQNS]); 75 76val DOT_ASSOC = Q.store_thm 77("DOT_ASSOC", 78`!A B C. A dot (B dot C) = (A dot B) dot C`, 79 RW_TAC basic_ss [EXTENSION,IN_dot] THEN METIS_TAC [APPEND_ASSOC]); 80 81val DOT_UNION_LDISTRIB = Q.store_thm 82("DOT_UNION_LDISTRIB", 83`!A B C. A dot (B UNION C) = (A dot B) UNION (A dot C)`, 84 RW_TAC basic_ss [EXTENSION,IN_dot] THEN METIS_TAC []); 85 86val DOT_UNION_RDISTRIB = Q.store_thm 87("DOT_UNION_RDISTRIB", 88`!A B C. (A UNION B) dot C = (A dot C) UNION (B dot C)`, 89 RW_TAC basic_ss [EXTENSION,IN_dot] THEN METIS_TAC []); 90 91val DOT_MONO = Q.store_thm 92("DOT_MONO", 93`!A B C D. A SUBSET C /\ B SUBSET D ==> (A dot B) SUBSET (C dot D)`, 94 RW_TAC basic_ss [SUBSET_DEF,IN_dot] THEN METIS_TAC []); 95 96(*---------------------------------------------------------------------------*) 97(* Iterated language concatenation. *) 98(*---------------------------------------------------------------------------*) 99 100val DOTn_def = 101 Define 102 `(DOTn A 0 = {[]}) /\ 103 (DOTn A (SUC n) = A dot (DOTn A n))`; 104 105val DOTn_RIGHT = Q.store_thm 106("DOTn_RIGHT", 107`!n A. A dot DOTn A n = DOTn A n dot A`, 108 Induct THEN RW_TAC basic_ss [DOTn_def] THENL 109 [RW_TAC basic_ss [EXTENSION,IN_dot], 110 METIS_TAC [DOT_ASSOC]]); 111 112val SUBSET_DOTn = Q.store_thm 113("SUBSET_DOTn", 114`!A. A SUBSET DOTn A (SUC 0)`, 115 RW_TAC basic_ss [SUBSET_DEF,DOTn_def,IN_dot]); 116 117val EMPTY_IN_DOTn_ZERO = Q.store_thm 118("EMPTY_IN_DOTn_ZERO", 119`!x A. x IN DOTn A 0 <=> (x = [])`, 120 RW_TAC basic_ss [DOTn_def]); 121 122val STRCAT_IN_DOTn_SUC = Q.store_thm 123("STRCAT_IN_DOTn_SUC", 124 `!a b A n. (a IN A /\ b IN DOTn A n) \/ (a IN DOTn A n /\ b IN A) 125 ==> (a ++ b) IN DOTn A (SUC n)`, 126 RW_TAC basic_ss [DOTn_def] THEN METIS_TAC [STRCAT_IN_dot,DOTn_RIGHT]); 127 128val STRCAT_IN_DOTn_ADD = Q.store_thm 129("STRCAT_IN_DOTn_ADD", 130`!m n a b A. 131 a IN DOTn A m /\ b IN DOTn A n ==> (a ++ b) IN DOTn A (m + n)`, 132 Induct THEN RW_TAC basic_ss [DOTn_def] THEN 133 FULL_SIMP_TAC basic_ss [IN_dot] THEN 134 `(v ++ b) IN DOTn A (m + n)` by METIS_TAC [] THEN 135 METIS_TAC [STRCAT_IN_DOTn_SUC,APPEND_ASSOC,DECIDE``SUC(m+n) = n + SUC m``]); 136 137val DOTn_EMPTYSET = Q.store_thm 138("DOTn_EMPTYSET", 139`!n. DOTn {} n = if n=0 then {[]} else {}`, 140 Induct THEN RW_TAC basic_ss [DOTn_def,DOT_EMPTYSET]); 141 142val DOTn_EMPTYSTRING = Q.store_thm 143("DOTn_EMPTYSTRING", 144`!n. DOTn {[]} n = {[]}`, 145 Induct THEN RW_TAC basic_ss [DOTn_def,dot_def,EXTENSION] THEN 146 METIS_TAC[APPEND_EQNS]); 147 148val EMPTY_IN_DOTn = Q.store_thm 149("EMPTY_IN_DOTn", 150`!n. ([] IN DOTn A n) <=> (n=0) \/ ([] IN A)`, 151 Induct THEN RW_TAC basic_ss [DOTn_def,EMPTY_IN_DOT] THEN METIS_TAC[]); 152 153val DOTn_UNION = Q.store_thm 154("DOTn_UNION", 155`!n x A B. x IN DOTn A n ==> x IN DOTn (A UNION B) n`, 156 Induct THEN RW_TAC basic_ss [DOTn_def,IN_dot] THEN METIS_TAC[]); 157 158val DOTn_DIFF = Q.store_thm 159("DOTn_DIFF", 160`!n x A B. x IN DOTn (A DIFF B) n ==> x IN DOTn A n`, 161 Induct THEN RW_TAC basic_ss [DOTn_def,IN_dot] THEN METIS_TAC[]); 162 163(*---------------------------------------------------------------------------*) 164(* This lemma can be extended so that k is as large or small as possible. It *) 165(* says that a word in A^n is either empty or can be split into k non-empty *) 166(* pieces. *) 167(*---------------------------------------------------------------------------*) 168 169val DOTn_EMPTYSTRING_FREE = Q.store_thm 170("DOTn_EMPTYSTRING_FREE", 171`!n A w. w IN DOTn A n ==> 172 (w = []) \/ 173 ?k. w IN DOTn (A DELETE []) k`, 174 Induct THEN RW_TAC basic_ss [DOTn_def,IN_dot] THEN 175 RES_TAC THEN Cases_on `u` THEN RW_TAC basic_ss [] THEN 176 `h::t IN (A DELETE [])` by RW_TAC basic_ss [] THENL 177 [METIS_TAC [SUBSET_DOTn,SUBSET_DEF], 178 METIS_TAC [STRCAT_IN_DOTn_SUC,APPEND_EQNS]]); 179 180(*---------------------------------------------------------------------------*) 181(* Kleene star *) 182(*---------------------------------------------------------------------------*) 183 184val KSTAR_def = 185 Define 186 `KSTAR(L:'a lang) = BIGUNION {DOTn L n | n IN UNIV}`; 187 188Theorem IN_KSTAR: 189 x IN KSTAR(L) <=> ?n. x IN DOTn L n 190Proof 191 RW_TAC basic_ss [KSTAR_def,BIGUNION] THEN 192 RW_TAC basic_ss [SPECIFICATION] THEN 193 METIS_TAC[] 194QED 195 196val KSTAR_EMPTYSET = Q.store_thm 197("KSTAR_EMPTYSET", 198`KSTAR {} = {[]}`, 199 RW_TAC basic_ss [EXTENSION,IN_KSTAR,DOTn_EMPTYSET] THEN 200 EQ_TAC THEN RW_TAC basic_ss [] THENL 201 [Cases_on `n` THEN FULL_SIMP_TAC basic_ss [], 202 METIS_TAC [IN_INSERT]]); 203 204val EMPTY_IN_KSTAR = Q.store_thm 205("EMPTY_IN_KSTAR", 206`!A. [] IN (KSTAR A)`, 207 RW_TAC basic_ss [IN_KSTAR] THEN METIS_TAC [DOTn_def,IN_INSERT]); 208 209val KSTAR_SING = Q.store_thm 210("KSTAR_SING", 211`!x. x IN (KSTAR {x})`, 212 RW_TAC basic_ss [IN_KSTAR] THEN 213 Q.EXISTS_TAC `SUC 0` THEN 214 RW_TAC basic_ss [DOTn_def,IN_dot]); 215 216val SUBSET_KSTAR = Q.store_thm 217("SUBSET_KSTAR", 218`!A. A SUBSET KSTAR(A)`, 219 RW_TAC basic_ss [SUBSET_DEF,IN_KSTAR] THEN 220 Q.EXISTS_TAC `SUC 0` THEN 221 RW_TAC basic_ss [DOTn_def,IN_dot]); 222 223val SUBSET_KSTAR_DOT = Q.store_thm 224("SUBSET_KSTAR_DOT", 225`!A B. B SUBSET (KSTAR A) dot B`, 226 RW_TAC basic_ss [SUBSET_DEF,IN_KSTAR,IN_dot] THEN 227 MAP_EVERY Q.EXISTS_TAC [`[]`,`x`] THEN 228 RW_TAC basic_ss [] THEN METIS_TAC [DOTn_def,IN_INSERT]); 229 230val STRCAT_IN_KSTAR = Q.store_thm 231("STRCAT_IN_KSTAR", 232`!u v A B. 233 u IN A /\ v IN KSTAR(A) dot B ==> (u ++ v) IN KSTAR(A) dot B`, 234 RW_TAC list_ss [IN_KSTAR,IN_dot] THEN 235 MAP_EVERY Q.EXISTS_TAC [`u++u'`,`v'`] THEN 236 RW_TAC list_ss [APPEND_ASSOC] THEN 237 Q.EXISTS_TAC `SUC n` THEN RW_TAC std_ss [DOTn_def] THEN 238 METIS_TAC [STRCAT_IN_dot]); 239 240val KSTAR_EQ_INTRO = Q.store_thm 241("KSTAR_EQ_INTRO", 242`!A B. (!n. DOTn A n = DOTn B n) ==> (KSTAR A = KSTAR B)`, 243 RW_TAC basic_ss [EXTENSION,IN_KSTAR]); 244 245val IN_KSTAR_LIST = Q.store_thm 246("IN_KSTAR_LIST", 247 `!s A. s IN KSTAR A <=> ?wlist. EVERY (\w. w IN A) wlist /\ (s = FLAT wlist)`, 248 RW_TAC list_ss [IN_KSTAR,EQ_IMP_THM] THENL 249 [POP_ASSUM MP_TAC THEN Q.ID_SPEC_TAC `s` 250 THEN Induct_on `n` THEN RW_TAC list_ss [] 251 THENL 252 [FULL_SIMP_TAC list_ss [EMPTY_IN_DOTn_ZERO] THEN RW_TAC list_ss [] 253 THEN Q.EXISTS_TAC `[]` THEN RW_TAC list_ss [], 254 FULL_SIMP_TAC list_ss [DOTn_def,IN_dot] 255 THEN RW_TAC list_ss [] THEN RES_TAC 256 THEN Q.EXISTS_TAC `u::wlist` THEN RW_TAC list_ss []], 257 Induct_on `wlist` THEN FULL_SIMP_TAC list_ss [] 258 THENL [METIS_TAC [EMPTY_IN_DOTn], 259 RW_TAC list_ss [] THEN RES_TAC 260 THEN Q.EXISTS_TAC `SUC n` 261 THEN RW_TAC list_ss [DOTn_def] THEN METIS_TAC[IN_dot]]]); 262 263(*---------------------------------------------------------------------------*) 264(* Some more complex equalities *) 265(*---------------------------------------------------------------------------*) 266 267val lang_ss = basic_ss ++ 268 rewrites [IN_KSTAR, IN_dot, DOTn_def, 269 DOT_EMPTYSET,DOT_EMPTYSTRING, DOTn_EMPTYSTRING, 270 KSTAR_SING,KSTAR_EMPTYSET,EMPTY_IN_KSTAR]; 271 272val KSTAR_EQ_EPSILON_UNION_DOT = Q.store_thm 273("KSTAR_EQ_EPSILON_UNION_DOT", 274`!A. KSTAR A = {[]} UNION (A dot KSTAR A)`, 275 RW_TAC lang_ss [EXTENSION,EQ_IMP_THM] THENL 276 [Cases_on `n` 277 THENL [METIS_TAC[EMPTY_IN_DOTn_ZERO], 278 FULL_SIMP_TAC lang_ss [] THEN METIS_TAC[]], 279 METIS_TAC [EMPTY_IN_DOTn_ZERO], 280 METIS_TAC [STRCAT_IN_DOTn_SUC]]); 281 282Theorem IN_KSTAR_THM: 283 !w L. w IN KSTAR L <=> (w = []) \/ 284 ?w1 w2. (w = w1++w2) /\ w1 IN L /\ w2 IN KSTAR L 285Proof RW_TAC list_ss [Once KSTAR_EQ_EPSILON_UNION_DOT,IN_UNION, IN_SING,IN_dot] 286QED 287 288val KSTAR_EQ_KSTAR_UNION = Q.store_thm 289("KSTAR_EQ_KSTAR_UNION", 290`!A. KSTAR A = KSTAR ({[]} UNION A)`, 291 RW_TAC lang_ss [EXTENSION,EQ_IMP_THM] THENL 292 [METIS_TAC [DOTn_UNION,UNION_COMM], 293 POP_ASSUM MP_TAC THEN Q.ID_SPEC_TAC `x` THEN 294 Induct_on `n` THEN RW_TAC lang_ss [] THENL 295 [METIS_TAC [EMPTY_IN_DOTn_ZERO], 296 METIS_TAC [APPEND_EQNS], 297 METIS_TAC [STRCAT_IN_DOTn_SUC,APPEND_EQNS]]]); 298 299val KSTAR_DOT_KSTAR = Q.store_thm 300("KSTAR_DOT_KSTAR", 301`!A. (KSTAR A dot KSTAR A) = KSTAR A`, 302 RW_TAC lang_ss [EXTENSION,EQ_IMP_THM] THENL 303 [METIS_TAC [STRCAT_IN_DOTn_ADD], 304 Cases_on `n` THEN FULL_SIMP_TAC lang_ss[] THENL 305 [METIS_TAC [APPEND_eq_NIL,EMPTY_IN_DOTn_ZERO], 306 METIS_TAC [SUBSET_DOTn,SUBSET_DEF]]]); 307 308val KSTAR_KSTAR_EQ_KSTAR = Q.store_thm 309("KSTAR_KSTAR_EQ_KSTAR", 310`!A. KSTAR(KSTAR A) = KSTAR A`, 311 RW_TAC lang_ss [EXTENSION,EQ_IMP_THM] THENL 312 [POP_ASSUM MP_TAC THEN Q.ID_SPEC_TAC `x` THEN 313 Induct_on `n` THEN RW_TAC lang_ss [] THEN 314 METIS_TAC [EMPTY_IN_DOTn_ZERO,STRCAT_IN_DOTn_ADD], 315 METIS_TAC [SUBSET_KSTAR,IN_KSTAR,SUBSET_DEF]]); 316 317val DOT_KSTAR_EQ_KSTAR_DOT = Q.store_thm 318("DOT_KSTAR_EQ_KSTAR_DOT", 319`!A. (A dot KSTAR A) = (KSTAR A dot A)`, 320 RW_TAC lang_ss [EXTENSION,EQ_IMP_THM] THENL 321 [`(u++v) IN (DOTn A n dot A)` by METIS_TAC [DOTn_RIGHT,EXTENSION,IN_dot], 322 `(u++v) IN (A dot DOTn A n)` by METIS_TAC [DOTn_RIGHT,EXTENSION,IN_dot]] 323 THEN METIS_TAC [IN_dot]); 324 325val lemma = Q.prove 326(`(!n. DOTn (A dot B) n dot A = A dot DOTn (B dot A) n) 327 ==> (KSTAR (A dot B) dot A = A dot KSTAR(B dot A))`, 328 RW_TAC lang_ss [EXTENSION] THEN METIS_TAC[]); 329 330val KSTAR_DOT_SHIFT = Q.store_thm 331("KSTAR_DOT_SHIFT", 332`!A. KSTAR (A dot B) dot A = A dot KSTAR(B dot A)`, 333 GEN_TAC THEN MATCH_MP_TAC lemma THEN 334 Induct THEN RW_TAC lang_ss [] THEN METIS_TAC [DOT_ASSOC]); 335 336val DOT_SQUARED_SUBSET = Q.store_thm 337("DOT_SQUARED_SUBSET", 338`!L. (L dot L) SUBSET L ==> (L dot KSTAR L) SUBSET L`, 339 RW_TAC lang_ss [SUBSET_DEF,GSYM LEFT_FORALL_IMP_THM] THEN 340 NTAC 2 (POP_ASSUM MP_TAC) THEN MAP_EVERY Q.ID_SPEC_TAC [`v`, `u`] THEN 341 Induct_on `n` THEN RW_TAC lang_ss [] THEN 342 METIS_TAC [DOT_ASSOC]); 343 344val KSTAR_UNION = Q.store_thm 345("KSTAR_UNION", 346`!A B. KSTAR (A UNION B) = KSTAR(KSTAR A dot B) dot KSTAR A`, 347 RW_TAC lang_ss [EXTENSION,EQ_IMP_THM] THENL 348 [POP_ASSUM MP_TAC THEN Q.ID_SPEC_TAC `x` THEN Induct_on `n` THENL 349 [METIS_TAC [EMPTY_IN_DOTn_ZERO,APPEND_EQNS], 350 SIMP_TAC basic_ss [DOTn_def,DOTn_RIGHT] THEN RW_TAC lang_ss [] THENL 351 [`?u1 u2. (u = u1 ++ u2) /\ (?m. u1 IN DOTn (KSTAR A dot B) m) /\ 352 ?k. u2 IN DOTn A k` by METIS_TAC[] THEN 353 METIS_TAC [APPEND_ASSOC,STRCAT_IN_DOTn_SUC], 354 `?u1 u2. (u = u1 ++ u2) /\ (?m. u1 IN DOTn (KSTAR A dot B) m) /\ 355 ?k. u2 IN DOTn A k` by METIS_TAC[] THEN 356 Q.EXISTS_TAC `u1 ++ (u2 ++ v)` THEN Q.EXISTS_TAC `[]` THEN 357 RW_TAC lang_ss [APPEND_ASSOC] THENL 358 [`u2 ++ v IN (KSTAR A dot B)` by (RW_TAC lang_ss [] THEN METIS_TAC[]) 359 THEN METIS_TAC [APPEND_ASSOC,STRCAT_IN_DOTn_SUC], 360 METIS_TAC [EMPTY_IN_DOTn_ZERO]]]] 361 , 362 REPEAT (POP_ASSUM MP_TAC) THEN MAP_EVERY Q.ID_SPEC_TAC [`v`, `u`, `n`] 363 THEN Induct_on `n'` THEN RW_TAC lang_ss [] THENL 364 [POP_ASSUM MP_TAC THEN Q.ID_SPEC_TAC `u` THEN 365 Induct_on`n` THEN RW_TAC lang_ss [] THENL 366 [METIS_TAC [EMPTY_IN_DOTn_ZERO], 367 METIS_TAC [IN_UNION,APPEND_ASSOC,STRCAT_IN_DOTn_ADD, 368 STRCAT_IN_DOTn_SUC,DOTn_UNION]], 369 `u' ++ v' IN DOTn A n' dot A` by METIS_TAC [IN_dot,DOTn_RIGHT] THEN 370 FULL_SIMP_TAC lang_ss [] THEN 371 METIS_TAC [IN_UNION,APPEND_ASSOC,STRCAT_IN_DOTn_ADD, 372 STRCAT_IN_DOTn_SUC,DOTn_UNION]]]); 373 374(*===========================================================================*) 375(* Arden's Lemma. *) 376(*===========================================================================*) 377 378val LENGTH_LESS = Q.store_thm 379("LENGTH_LESS", 380`!u x v. (x = u++v) /\ ~(u = []) ==> LENGTH v < LENGTH x`, 381 Cases_on `u` THEN RW_TAC list_ss []); 382 383val lemma = Q.prove 384(`!A B X. (!n. (DOTn A n dot B) SUBSET X) ==> KSTAR(A) dot B SUBSET X`, 385 RW_TAC basic_ss [SUBSET_DEF,IN_KSTAR,IN_dot] THEN METIS_TAC []); 386 387(*---------------------------------------------------------------------------*) 388(* Although Arden's Lemma doesn't directly mention machines, it can be used *) 389(* to map DFAs to equivalent regular languages. *) 390(*---------------------------------------------------------------------------*) 391 392val ARDENS_LEMMA = Q.store_thm 393("ARDENS_LEMMA", 394 `!A B X:'a lang. 395 ~([] IN A) /\ (X = (A dot X) UNION B) ==> (X = KSTAR(A) dot B)`, 396 REPEAT STRIP_TAC THEN RW_TAC basic_ss [SET_EQ_SUBSET] THENL 397 [REWRITE_TAC [SUBSET_DEF] THEN GEN_TAC THEN 398 measureInduct_on `LENGTH x` THEN 399 Cases_on `LENGTH x` THENL 400 [FULL_SIMP_TAC basic_ss [LENGTH_NIL,EMPTY_IN_DOT] THEN RW_TAC std_ss [] 401 THENL [METIS_TAC [EMPTY_IN_KSTAR],METIS_TAC [EMPTY_IN_DOT,IN_UNION]], 402 STRIP_TAC THEN 403 `x IN A dot X \/ x IN B` by METIS_TAC [IN_UNION] THENL 404 [`?u v. (x = u ++ v) /\ u IN A /\ v IN X` by METIS_TAC [IN_dot] THEN 405 `~(u = [])` by METIS_TAC [] THEN 406 `LENGTH v < LENGTH x` by METIS_TAC [LENGTH_LESS] THEN 407 `v IN KSTAR A dot B` by METIS_TAC [] THEN METIS_TAC [STRCAT_IN_KSTAR] 408 , 409 METIS_TAC [SUBSET_DEF,SUBSET_KSTAR_DOT]]] 410 , 411 MATCH_MP_TAC lemma THEN Induct THENL 412 [RW_TAC basic_ss [DOTn_def,SUBSET_DEF,dot_def] THEN METIS_TAC [IN_UNION], 413 `A dot (DOTn A n dot B) SUBSET (A dot X)` 414 by METIS_TAC [DOT_MONO,SUBSET_REFL] THEN 415 SIMP_TAC std_ss [DOTn_def,GSYM DOT_ASSOC] THEN 416 METIS_TAC [IN_UNION,SUBSET_DEF]]]); 417 418val _ = export_theory(); 419