1310 qed |
1310 qed |
1311 |
1311 |
1312 |
1312 |
1313 text {* tests by Christian *} |
1313 text {* tests by Christian *} |
1314 |
1314 |
|
1315 (* compatibility with stable Isabelle *) |
1315 lemma temp_set_ext[no_atp]: "(\<And>x. (x:A) = (x:B)) \<Longrightarrow> (A = B)" |
1316 lemma temp_set_ext[no_atp]: "(\<And>x. (x:A) = (x:B)) \<Longrightarrow> (A = B)" |
1316 by(auto intro:set_eqI) |
1317 by(auto intro:set_eqI) |
1317 |
1318 |
1318 fun |
1319 abbreviation |
1319 MNRel |
1320 str_eq ("_ \<approx>_ _") |
1320 where |
1321 where |
1321 "MNRel Lang (x, y) = (x \<equiv>Lang\<equiv> y)" |
1322 "x \<approx>Lang y \<equiv> (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)" |
1322 |
1323 |
1323 lemma |
1324 abbreviation |
1324 "equiv UNIV (MNRel Lang)" |
1325 lang_eq ("\<approx>_") |
|
1326 where |
|
1327 "\<approx>Lang \<equiv> (\<lambda>(x, y). x \<approx>Lang y)" |
|
1328 |
|
1329 lemma lang_eq_is_equiv: |
|
1330 "equiv UNIV (\<approx>Lang)" |
1325 unfolding equiv_def |
1331 unfolding equiv_def |
1326 unfolding refl_on_def sym_def trans_def |
1332 unfolding refl_on_def sym_def trans_def |
1327 apply(auto simp add: mem_def equiv_str_def) |
1333 by (simp add: mem_def equiv_str_def) |
|
1334 |
|
1335 text {* |
|
1336 equivalence classes of x can be written |
|
1337 |
|
1338 (\<approx>Lang)``{x} |
|
1339 |
|
1340 the language quotient can be written |
|
1341 |
|
1342 UNIV // (\<approx>Lang) |
|
1343 *} |
|
1344 |
|
1345 lemma |
|
1346 "(\<approx>Lang)``{x} = \<lbrakk>x\<rbrakk>Lang" |
|
1347 unfolding equiv_class_def equiv_str_def Image_def mem_def |
|
1348 by (simp) |
|
1349 |
|
1350 lemma |
|
1351 "UNIV // (\<approx>Lang) = UNIV Quo Lang" |
|
1352 unfolding quotient_def quot_def |
|
1353 unfolding equiv_class_def equiv_str_def |
|
1354 unfolding Image_def mem_def |
|
1355 by auto |
|
1356 |
|
1357 lemma |
|
1358 "{} \<notin> UNIV // (\<approx>Lang)" |
|
1359 unfolding quotient_def |
|
1360 unfolding Image_def |
|
1361 apply(auto) |
|
1362 apply(rule_tac x="x" in exI) |
|
1363 unfolding mem_def |
|
1364 apply(simp) |
1328 done |
1365 done |
1329 |
1366 |
|
1367 definition |
|
1368 transitions :: "string set \<Rightarrow> string set \<Rightarrow> rexp set" ("_\<Turnstile>\<Rightarrow>_") |
|
1369 where |
|
1370 "X \<Turnstile>\<Rightarrow> Y \<equiv> {CHAR c | c. X ; {[c]} \<subseteq> Y}" |
|
1371 |
|
1372 definition |
|
1373 "rhs CS X \<equiv> { (Y, X \<Turnstile>\<Rightarrow>Y) | Y. Y \<in> CS }" |
|
1374 |
|
1375 definition |
|
1376 "rhs_sem CS X \<equiv> { (Y; L (folds ALT NULL (X \<Turnstile>\<Rightarrow>Y))) | Y. Y \<in> CS }" |
|
1377 |
|
1378 definition |
|
1379 "eqs CS \<equiv> (\<Union>X \<in> CS. {(X, rhs CS X)})" |
|
1380 |
|
1381 lemma finite_rhs: |
|
1382 assumes fin: "finite CS" |
|
1383 shows "finite (rhs CS X)" |
|
1384 using fin unfolding rhs_def by (auto) |
|
1385 |
|
1386 lemma finite_eqs: |
|
1387 assumes fin: "finite CS" |
|
1388 shows "finite (eqs CS)" |
|
1389 unfolding eqs_def |
|
1390 apply(rule finite_UN_I) |
|
1391 apply(rule fin) |
|
1392 apply(simp add: eq_def) |
|
1393 done |
|
1394 |
1330 lemma |
1395 lemma |
1331 "(MNRel Lang)``{x} = \<lbrakk>x\<rbrakk>Lang" |
1396 shows "X ; L (folds ALT NULL X \<Turnstile>\<Rightarrow> Y) \<subseteq> Y" |
1332 unfolding equiv_class_def Image_def mem_def |
1397 by (auto simp add: transitions_def lang_seq_def fold_alt_null_eqs) |
1333 by (simp) |
1398 |
|
1399 lemma |
|
1400 assumes a: "X \<in> (UNIV // (\<approx>Lang))" |
|
1401 shows "X \<subseteq> \<Union> (rhs_sem (UNIV // (\<approx>Lang)) X)" |
|
1402 unfolding rhs_sem_def |
|
1403 apply (auto simp add: transitions_def lang_seq_def fold_alt_null_eqs) |
|
1404 apply(rule_tac x="X" in exI) |
|
1405 apply(simp) |
|
1406 apply(simp add: quotient_def Image_def) |
|
1407 apply(subst (4) mem_def) |
|
1408 apply(simp) |
|
1409 using a |
|
1410 apply(simp add: quotient_def Image_def) |
|
1411 apply(subst (asm) (2) mem_def) |
|
1412 apply(simp) |
|
1413 apply(rule_tac x="X" in exI) |
|
1414 apply(simp) |
|
1415 apply(erule exE) |
|
1416 apply(simp) |
|
1417 apply(rule temp_set_ext) |
|
1418 apply(simp) |
|
1419 apply(rule iffI) |
|
1420 apply(rule_tac x="x" in exI) |
|
1421 apply(simp) |
|
1422 oops |
1334 |
1423 |
1335 lemma tt: "\<lbrakk>A = B; C \<subseteq> B\<rbrakk> \<Longrightarrow> C \<subseteq> A" by simp |
1424 lemma tt: "\<lbrakk>A = B; C \<subseteq> B\<rbrakk> \<Longrightarrow> C \<subseteq> A" by simp |
1336 |
1425 |
1337 lemma |
1426 lemma |
1338 "UNIV//(MNRel (L1 \<union> L2)) \<subseteq> (UNIV//(MNRel L1)) \<union> (UNIV//(MNRel L2))" |
1427 "UNIV//(\<approx>(L1 \<union> L2)) \<subseteq> (UNIV//(\<approx>L1)) \<union> (UNIV//(\<approx>L2))" |
1339 unfolding quotient_def |
1428 unfolding quotient_def Image_def |
1340 unfolding UNION_eq_Union_image |
|
1341 apply(rule tt) |
|
1342 apply(rule Un_Union_image[symmetric]) |
|
1343 apply(simp) |
|
1344 apply(rule UN_mono) |
|
1345 apply(simp) |
|
1346 apply(simp) |
|
1347 unfolding Image_def |
|
1348 unfolding mem_def |
|
1349 unfolding MNRel.simps |
|
1350 apply(simp) |
|
1351 oops |
1429 oops |
1352 |
1430 |
1353 |
1431 |
1354 |
1432 |
1355 text {* Alternative definition for Quo *} |
1433 text {* Alternative definition for Quo *} |
1356 definition |
1434 definition |
1357 QUOT :: "string set \<Rightarrow> (string set) set" |
1435 QUOT :: "string set \<Rightarrow> (string set) set" |
1358 where |
1436 where |
1359 "QUOT Lang \<equiv> (\<Union>x. {\<lbrakk>x\<rbrakk>Lang})" |
1437 "QUOT Lang \<equiv> (\<Union>x. {\<lbrakk>x\<rbrakk>Lang})" |
|
1438 |
1360 |
1439 |
1361 lemma test_01: |
1440 lemma test_01: |
1362 "Lang \<subseteq> (\<Union> QUOT Lang)" |
1441 "Lang \<subseteq> (\<Union> QUOT Lang)" |
1363 unfolding QUOT_def equiv_class_def equiv_str_def |
1442 unfolding QUOT_def equiv_class_def equiv_str_def |
1364 by (blast) |
1443 by (blast) |
1365 |
1444 |
1366 |
1445 text{* by chunhan *} |
1367 (* by chunhan *) |
|
1368 lemma quot_lambda: "QUOT {[]} = {{[]}, UNIV - {[]}}" |
1446 lemma quot_lambda: "QUOT {[]} = {{[]}, UNIV - {[]}}" |
1369 proof |
1447 proof |
1370 show "QUOT {[]} \<subseteq> {{[]}, UNIV - {[]}}" |
1448 show "QUOT {[]} \<subseteq> {{[]}, UNIV - {[]}}" |
1371 proof |
1449 proof |
1372 fix x |
1450 fix x |