1315 (* by chunhan *)

  1316 lemma quot_lambda: "QUOT {[]} = {{[]}, UNIV - {[]}}"

  1317 proof 

  1318   show "QUOT {[]} \<subseteq> {{[]}, UNIV - {[]}}"

  1319   proof 

  1320     fix x 

  1321     assume in_quot: "x \<in> QUOT {[]}"

  1322     show "x \<in> {{[]}, UNIV - {[]}}"

  1323     proof -

  1324       from in_quot 

  1325       have "x = {[]} \<or> x = UNIV - {[]}"

  1326         unfolding QUOT_def equiv_class_def

  1327       proof 

  1328         fix xa

  1329         assume in_univ: "xa \<in> UNIV"

  1330            and in_eqiv: "x \<in> {{y. xa \<equiv>{[]}\<equiv> y}}"

  1331         show "x = {[]} \<or> x = UNIV - {[]}"

  1332         proof(cases "xa = []")

  1333           case True

  1334           hence "{y. xa \<equiv>{[]}\<equiv> y} = {[]}" using in_eqiv

  1335             by (auto simp add:equiv_str_def)

  1336           thus ?thesis using in_eqiv by (rule_tac disjI1, simp)

  1337         next

  1338           case False

  1339           hence "{y. xa \<equiv>{[]}\<equiv> y} = UNIV - {[]}" using in_eqiv

  1340             by (auto simp:equiv_str_def)

  1341           thus ?thesis using in_eqiv by (rule_tac disjI2, simp)

  1342         qed

  1343       qed

  1344       thus ?thesis by simp

  1345     qed

  1346   qed

  1347 next

  1348   show "{{[]}, UNIV - {[]}} \<subseteq> QUOT {[]}"

  1349   proof

  1350     fix x

  1351     assume in_res: "x \<in> {{[]}, (UNIV::string set) - {[]}}"

  1352     show "x \<in> (QUOT {[]})"

  1353     proof -

  1354       have "x = {[]} \<Longrightarrow> x \<in> QUOT {[]}"

  1355         apply (simp add:QUOT_def equiv_class_def equiv_str_def)

  1356         by (rule_tac x = "[]" in exI, auto)

  1357       moreover have "x = UNIV - {[]} \<Longrightarrow> x \<in> QUOT {[]}"

  1358         apply (simp add:QUOT_def equiv_class_def equiv_str_def)

  1359         by (rule_tac x = "''a''" in exI, auto)

  1360       ultimately show ?thesis using in_res by blast

  1361     qed

  1362   qed

  1363 qed

  1364 

  1365 lemma quot_single_aux: "\<lbrakk>x \<noteq> []; x \<noteq> [c]\<rbrakk> \<Longrightarrow> x @ z \<noteq> [c]"

  1366 by (induct x, auto)

  1367 

  1368 lemma quot_single: "\<And> (c::char). QUOT {[c]} = {{[]}, {[c]}, UNIV - {[], [c]}}"

  1369 proof - 

  1370   fix c::"char" 

  1371   have exist_another: "\<exists> a. a \<noteq> c" 

  1372     apply (case_tac "c = CHR ''a''")

  1373     apply (rule_tac x = "CHR ''b''" in exI, simp)

  1374     by (rule_tac x = "CHR ''a''" in exI, simp)  

  1375   show "QUOT {[c]} = {{[]}, {[c]}, UNIV - {[], [c]}}"

  1376   proof

  1377     show "QUOT {[c]} \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}"

  1378     proof 

  1379       fix x 

  1380       assume in_quot: "x \<in> QUOT {[c]}"

  1381       show "x \<in> {{[]}, {[c]}, UNIV - {[],[c]}}"

  1382       proof -

  1383         from in_quot 

  1384         have "x = {[]} \<or> x = {[c]} \<or> x = UNIV - {[],[c]}"

  1385           unfolding QUOT_def equiv_class_def

  1386         proof 

  1387           fix xa

  1388           assume in_eqiv: "x \<in> {{y. xa \<equiv>{[c]}\<equiv> y}}"

  1389           show "x = {[]} \<or> x = {[c]} \<or> x = UNIV - {[], [c]}"

  1390           proof-

  1391             have "xa = [] \<Longrightarrow> x = {[]}" using in_eqiv 

  1392               by (auto simp add:equiv_str_def)

  1393             moreover have "xa = [c] \<Longrightarrow> x = {[c]}"

  1394             proof -

  1395               have "xa = [c] \<Longrightarrow> {y. xa \<equiv>{[c]}\<equiv> y} = {[c]}" using in_eqiv

  1396                 apply (simp add:equiv_str_def)

  1397                 apply (rule set_ext, rule iffI, simp)

  1398                 apply (drule_tac x = "[]" in spec, auto)

  1399                 done   

  1400               thus "xa = [c] \<Longrightarrow> x = {[c]}" using in_eqiv by simp 

  1401             qed

  1402             moreover have "\<lbrakk>xa \<noteq> []; xa \<noteq> [c]\<rbrakk> \<Longrightarrow> x = UNIV - {[],[c]}"

  1403             proof -

  1404               have "\<lbrakk>xa \<noteq> []; xa \<noteq> [c]\<rbrakk> \<Longrightarrow> {y. xa \<equiv>{[c]}\<equiv> y} = UNIV - {[],[c]}" 

  1405                 apply (clarsimp simp add:equiv_str_def)

  1406                 apply (rule set_ext, rule iffI, simp)

  1407                 apply (rule conjI)

  1408                 apply (drule_tac x = "[c]" in spec, simp)

  1409                 apply (drule_tac x = "[]" in spec, simp)

  1410                 by (auto dest:quot_single_aux)

  1411               thus "\<lbrakk>xa \<noteq> []; xa \<noteq> [c]\<rbrakk> \<Longrightarrow> x = UNIV - {[],[c]}" using in_eqiv by simp

  1412             qed

  1413             ultimately show ?thesis by blast

  1414           qed

  1415         qed

  1416         thus ?thesis by simp

  1417       qed

  1418     qed

  1419   next

  1420     show "{{[]}, {[c]}, UNIV - {[],[c]}} \<subseteq> QUOT {[c]}"

  1421     proof

  1422       fix x

  1423       assume in_res: "x \<in> {{[]},{[c]}, (UNIV::string set) - {[],[c]}}"

  1424       show "x \<in> (QUOT {[c]})"

  1425       proof -

  1426         have "x = {[]} \<Longrightarrow> x \<in> QUOT {[c]}"

  1427           apply (simp add:QUOT_def equiv_class_def equiv_str_def)

  1428           by (rule_tac x = "[]" in exI, auto)

  1429         moreover have "x = {[c]} \<Longrightarrow> x \<in> QUOT {[c]}"

  1430           apply (simp add:QUOT_def equiv_class_def equiv_str_def)

  1431           apply (rule_tac x = "[c]" in exI, simp)

  1432           apply (rule set_ext, rule iffI, simp+)

  1433           by (drule_tac x = "[]" in spec, simp)

  1434         moreover have "x = UNIV - {[],[c]} \<Longrightarrow> x \<in> QUOT {[c]}"

  1435           using exist_another

  1436           apply (clarsimp simp add:QUOT_def equiv_class_def equiv_str_def)        

  1437           apply (rule_tac x = "[a]" in exI, simp)

  1438           apply (rule set_ext, rule iffI, simp)

  1439           apply (clarsimp simp:quot_single_aux, simp)

  1440           apply (rule conjI)

  1441           apply (drule_tac x = "[c]" in spec, simp)

  1442           by (drule_tac x = "[]" in spec, simp)     

  1443         ultimately show ?thesis using in_res by blast

  1444       qed

  1445     qed

  1446   qed

  1447 qed

  1448 

  1449 lemma quot_seq: 

  1450   assumes finite1: "finite (QUOT L\<^isub>1)"

  1451   and finite2: "finite (QUOT L\<^isub>2)"

  1452   shows "finite (QUOT (L\<^isub>1;L\<^isub>2))"

  1453 apply (simp add:QUOT_def equiv_class_def equiv_str_def)

  1454 sorry

  1455  

  1456 lemma quot_alt:

  1457   assumes finite1: "finite (QUOT L\<^isub>1)"

  1458   and finite2: "finite (QUOT L\<^isub>2)"

  1459   shows "finite (QUOT (L\<^isub>1 \<union> L\<^isub>2))"

  1460 sorry

  1461 

  1462 lemma quot_star:  

  1463   assumes finite1: "finite (QUOT L\<^isub>1)"

  1464   shows "finite (QUOT (L\<^isub>1\<star>))"

  1465 sorry

  1466 

  1467 lemma other_direction:

  1468   "Lang = L (r::rexp) \<Longrightarrow> finite (QUOT Lang)"

  1469 apply (induct arbitrary:Lang rule:rexp.induct)

  1470 apply (simp add:QUOT_def equiv_class_def equiv_str_def)

  1471 by (simp_all add:quot_lambda quot_single quot_seq quot_alt quot_star)  

  1472 

  1473 

  1474 

  1475 

  1476 

  1477