1057 shows "t1 \<sqsubseteq>pre s1" |
1080 shows "t1 \<sqsubseteq>pre s1" |
1058 using assms |
1081 using assms |
1059 apply(auto simp add: Sequ_def prefix_list_def append_eq_append_conv2) |
1082 apply(auto simp add: Sequ_def prefix_list_def append_eq_append_conv2) |
1060 done |
1083 done |
1061 |
1084 |
1062 |
|
1063 |
|
1064 lemma CPTpre_test: |
|
1065 assumes "s \<in> r \<rightarrow> v" |
|
1066 shows "\<not>(\<exists>v' \<in> CPT r s. v :\<sqsubset>val v')" |
|
1067 using assms |
|
1068 apply(induct r arbitrary: s v rule: rexp.induct) |
|
1069 apply(erule Posix.cases) |
|
1070 apply(simp_all) |
|
1071 apply(erule Posix.cases) |
|
1072 apply(simp_all) |
|
1073 apply(simp add: CPT_simps) |
|
1074 apply(simp add: val_ord_def val_ord_ex_def) |
|
1075 apply(erule Posix.cases) |
|
1076 apply(simp_all) |
|
1077 apply(simp add: CPT_simps) |
|
1078 apply (simp add: val_ord_def val_ord_ex_def) |
|
1079 (* SEQ *) |
|
1080 apply(rule ballI) |
|
1081 apply(erule Posix.cases) |
|
1082 apply(simp_all) |
|
1083 apply(clarify) |
|
1084 apply(subst (asm) CPT_simps) |
|
1085 apply(simp) |
|
1086 apply(clarify) |
|
1087 thm val_ord_SEQ |
|
1088 apply(drule_tac ?r="r1" in val_ord_SEQ) |
|
1089 apply(simp) |
|
1090 apply (simp add: CPT_def Posix1(2)) |
|
1091 apply (simp add: Posix1a) |
|
1092 apply (simp add: CPT_def Posix1a) |
|
1093 using Prf_CPrf apply auto[1] |
|
1094 apply(erule disjE) |
|
1095 apply(drule_tac x="s1" in meta_spec) |
|
1096 apply(drule_tac x="v1" in meta_spec) |
|
1097 apply(simp) |
|
1098 apply(drule_tac x="v1a" in bspec) |
|
1099 apply(subgoal_tac "s1 = s1a") |
|
1100 apply(simp) |
|
1101 apply(auto simp add: append_eq_append_conv2)[1] |
|
1102 apply (metis (mono_tags, lifting) CPT_def L_flat_Prf1 Prf_CPrf append_Nil append_Nil2 mem_Collect_eq) |
|
1103 apply(simp add: CPT_def) |
|
1104 apply(auto)[1] |
|
1105 oops |
|
1106 |
1085 |
1107 |
1086 |
1108 lemma test: |
1087 lemma test: |
1109 assumes "finite A" |
1088 assumes "finite A" |
1110 shows "finite {vs. Stars vs \<in> A}" |
1089 shows "finite {vs. Stars vs \<in> A}" |
1411 using assms |
1390 using assms |
1412 apply(rule_tac Posix_val_ord) |
1391 apply(rule_tac Posix_val_ord) |
1413 apply(assumption) |
1392 apply(assumption) |
1414 apply(simp add: CPTpre_def CPT_def) |
1393 apply(simp add: CPTpre_def CPT_def) |
1415 done |
1394 done |
|
1395 |
|
1396 |
|
1397 lemma STAR_val_ord: |
|
1398 assumes "Stars (v1 # vs1) \<sqsubset>val (Suc p # ps) Stars (v2 # vs2)" "flat v1 = flat v2" |
|
1399 shows "(Stars vs1) \<sqsubset>val (p # ps) (Stars vs2)" |
|
1400 using assms(1,2) |
|
1401 apply - |
|
1402 apply(simp(no_asm) add: val_ord_def) |
|
1403 apply(rule conjI) |
|
1404 apply(simp add: val_ord_def) |
|
1405 apply(rule conjI) |
|
1406 apply(simp add: val_ord_def) |
|
1407 apply(auto simp add: pflat_len_simps pflat_len_Stars_simps2)[1] |
|
1408 apply(rule ballI) |
|
1409 apply(rule impI) |
|
1410 apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append) |
|
1411 apply(clarify) |
|
1412 apply(case_tac q) |
|
1413 apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append) |
|
1414 apply(clarify) |
|
1415 apply(erule disjE) |
|
1416 prefer 2 |
|
1417 apply(drule_tac x="Suc a # list" in bspec) |
|
1418 apply(simp) |
|
1419 apply(drule mp) |
|
1420 apply(simp) |
|
1421 apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append) |
|
1422 apply(drule_tac x="Suc a # list" in bspec) |
|
1423 apply(simp) |
|
1424 apply(drule mp) |
|
1425 apply(simp) |
|
1426 apply(simp add: val_ord_def pflat_len_simps pflat_len_Stars_simps2 intlen_append) |
|
1427 done |
|
1428 |
|
1429 |
|
1430 lemma Posix_val_ord_reverse: |
|
1431 assumes "s \<in> r \<rightarrow> v1" |
|
1432 shows "\<not>(\<exists>v2 \<in> CPT r s. v2 :\<sqsubset>val v1)" |
|
1433 using assms |
|
1434 apply(induct) |
|
1435 apply(auto)[1] |
|
1436 apply(simp add: CPT_def) |
|
1437 apply(simp add: val_ord_ex_def) |
|
1438 apply(erule exE) |
|
1439 apply(simp add: val_ord_def) |
|
1440 apply(auto simp add: pflat_len_simps)[1] |
|
1441 using Prf_CPrf Prf_elims(4) apply blast |
|
1442 (* CHAR *) |
|
1443 apply(auto)[1] |
|
1444 apply(simp add: CPT_def) |
|
1445 apply(simp add: val_ord_ex_def) |
|
1446 apply(clarify) |
|
1447 apply(erule CPrf.cases) |
|
1448 apply(simp_all) |
|
1449 apply(simp add: val_ord_def) |
|
1450 (* ALT *) |
|
1451 apply(auto)[1] |
|
1452 apply(simp add: CPT_def) |
|
1453 apply(clarify) |
|
1454 apply(erule CPrf.cases) |
|
1455 apply(simp_all) |
|
1456 apply(simp add: val_ord_ex_def) |
|
1457 apply(clarify) |
|
1458 apply(case_tac p) |
|
1459 apply(simp) |
|
1460 apply(simp add: val_ord_def) |
|
1461 apply(auto)[1] |
|
1462 apply(auto simp add: pflat_len_simps)[1] |
|
1463 using Posix1(2) apply auto[1] |
|
1464 apply(clarify) |
|
1465 using val_ord_ALTE apply blast |
|
1466 apply(simp add: val_ord_ex_def) |
|
1467 apply(clarify) |
|
1468 apply(simp add: val_ord_def) |
|
1469 apply(auto simp add: pflat_len_simps)[1] |
|
1470 using Posix1(2) apply auto[1] |
|
1471 apply (metis (mono_tags, lifting) One_nat_def Pos_empty Sulzmann.lexordp_simps(3) Un_iff inlen_bigger less_minus_one_simps(1) mem_Collect_eq not_less pflat_len_simps(3) pflat_len_simps(6) pflat_len_simps(7) zero_less_one) |
|
1472 (* ALT RIGHT case *) |
|
1473 apply(auto)[1] |
|
1474 apply(simp add: CPT_def) |
|
1475 apply(clarify) |
|
1476 apply(erule CPrf.cases) |
|
1477 apply(simp_all) |
|
1478 apply(simp add: val_ord_ex_def) |
|
1479 apply(clarify) |
|
1480 apply (simp add: L_flat_Prf1 Prf_CPrf) |
|
1481 apply(simp add: val_ord_ex_def) |
|
1482 apply(clarify) |
|
1483 apply(case_tac p) |
|
1484 apply (simp add: Posix1(2) pflat_len_simps(7) val_ord_def) |
|
1485 using val_ord_ALTE2 apply blast |
|
1486 (* SEQ case *) |
|
1487 apply(clarify) |
|
1488 apply(simp add: CPT_def) |
|
1489 apply(clarify) |
|
1490 apply(erule CPrf.cases) |
|
1491 apply(simp_all) |
|
1492 apply(drule_tac r="r1a" in val_ord_SEQ) |
|
1493 apply(simp) |
|
1494 using Posix1(2) apply auto[1] |
|
1495 apply (simp add: Prf_CPrf) |
|
1496 apply (simp add: Posix1a) |
|
1497 apply(auto)[1] |
|
1498 apply(subgoal_tac "length (flat v1a) \<le> length s1") |
|
1499 prefer 2 |
|
1500 apply (metis L_flat_Prf1 Prf_CPrf append_eq_append_conv_if append_eq_conv_conj drop_eq_Nil) |
|
1501 apply(subst (asm) append_eq_append_conv_if) |
|
1502 apply(simp) |
|
1503 apply (metis (mono_tags, lifting) CPT_def Posix_CPT le_less_linear mem_Collect_eq take_all val_ord_ex_trans val_ord_shorterI) |
|
1504 using Posix1(2) apply auto[1] |
|
1505 (* STAR case *) |
|
1506 apply(clarify) |
|
1507 apply(simp add: CPT_def) |
|
1508 apply(clarify) |
|
1509 apply(erule CPrf.cases) |
|
1510 apply(simp_all) |
|
1511 apply (simp add: Posix1(2)) |
|
1512 apply(subgoal_tac "length (flat va) \<le> length s1") |
|
1513 prefer 2 |
|
1514 apply (metis L.simps(6) L_flat_Prf1 Prf_CPrf append_eq_append_conv_if append_eq_conv_conj drop_eq_Nil flat_Stars) |
|
1515 apply(subst (asm) append_eq_append_conv_if) |
|
1516 apply(simp) |
|
1517 (* HERE *) |
|
1518 apply(case_tac "flat va = s1") |
|
1519 prefer 2 |
|
1520 apply(subgoal_tac "v :\<sqsubset>val va") |
|
1521 prefer 2 |
|
1522 apply (metis Posix1(2) le_less_linear take_all val_ord_shorterI) |
|
1523 apply(rotate_tac 3) |
|
1524 apply(simp add: val_ord_ex_def) |
|
1525 apply(clarify) |
|
1526 apply(case_tac p) |
|
1527 apply(simp add: val_ord_def pflat_len_simps) |
|
1528 apply (smt Posix1(2) append_take_drop_id flat_Stars intlen_append) |
|
1529 apply(simp) |
|
1530 prefer 2 |
|
1531 apply(simp) |
|
1532 apply(drule_tac x="va" in spec) |
|
1533 apply(simp) |
|
1534 apply(subst (asm) (2) val_ord_ex_def) |
|
1535 apply(subst (asm) (2) val_ord_ex_def) |
|
1536 apply(clarify) |
|
1537 apply(simp) |
|
1538 apply(drule_tac x="Stars vsa" in spec) |
|
1539 apply(simp) |
|
1540 apply(case_tac p) |
|
1541 apply(simp) |
|
1542 apply (metis Posix1(2) flat.simps(7) flat_Stars less_irrefl pflat_len_simps(7) val_ord_def) |
|
1543 apply(clarify) |
|
1544 apply(case_tac a) |
|
1545 apply(simp) |
|
1546 apply(subst (asm) val_ord_ex_def) |
|
1547 apply(simp) |
|
1548 apply(subst (asm) (2) val_ord_def) |
|
1549 apply(clarify) |
|
1550 apply(simp add: pflat_len_Stars_simps) |
|
1551 apply(simp add: pflat_len_simps) |
|
1552 prefer 3 |
|
1553 proof - |
|
1554 fix s1 :: "char list" and v :: val and s2 :: "char list" and vs :: "val list" and va :: val and ra :: rexp and vsa :: "val list" and p :: "nat list" and pa :: "nat list" and a :: nat and list :: "nat list" |
|
1555 assume a1: "length (flat va) \<le> length s1" |
|
1556 assume a2: "s1 \<in> ra \<rightarrow> v" |
|
1557 assume a3: "s2 \<in> STAR ra \<rightarrow> Stars vs" |
|
1558 assume a4: "Stars (va # vsa) \<sqsubset>val a # list Stars (v # vs)" |
|
1559 assume a5: "v \<sqsubset>val pa va" |
|
1560 assume a6: "flat va = take (length (flat va)) s1" |
|
1561 assume a7: "concat (map flat vsa) = drop (length (flat va)) s1 @ s2" |
|
1562 assume "p = a # list" |
|
1563 obtain nns :: "val \<Rightarrow> val \<Rightarrow> nat list" where |
|
1564 f8: "(\<forall>v va. \<not> v :\<sqsubset>val va \<or> v \<sqsubset>val nns v va va) \<and> (\<forall>v va. (\<forall>ns. \<not> v \<sqsubset>val ns va) \<or> v :\<sqsubset>val va)" |
|
1565 using val_ord_ex_def by moura |
|
1566 then have "Stars (v # vs) :\<sqsubset>val Stars (va # vsa)" |
|
1567 using a7 a6 a5 a3 a2 a1 by (metis Posix1(2) append_eq_append_conv_if flat.simps(7) flat_Stars val_ord_STARI) |
|
1568 then show False |
|
1569 using f8 a4 by (meson less_irrefl val_ord_def val_ord_ex_trans) |
|
1570 next |
|
1571 fix v :: val and vs :: "val list" and va :: val and ra :: rexp and vsa :: "val list" and list :: "nat list" |
|
1572 assume a1: "intlen (flat va @ concat (map flat vsa)) = intlen (flat v @ concat (map flat vs)) \<and> (\<forall>q\<in>{0 # ps |ps. ps \<in> Pos va} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vsa)} \<union> ({0 # ps |ps. ps \<in> Pos v} \<union> {Suc n # ps |n ps. n # ps \<in> Pos (Stars vs)}). q \<sqsubset>lex 0 # list \<longrightarrow> pflat_len (Stars (va # vsa)) q = pflat_len (Stars (v # vs)) q)" |
|
1573 assume a2: "pflat_len v list < pflat_len va list" |
|
1574 assume a3: "list \<in> Pos va" |
|
1575 assume a4: "\<forall>p. \<not> va \<sqsubset>val p v" |
|
1576 have f5: "\<And>ns. pflat_len (Stars (v # vs)) ns = pflat_len (Stars (va # vsa)) ns \<or> \<not> ns \<sqsubset>lex 0 # list \<or> (\<forall>nsa. ns \<noteq> 0 # nsa \<or> nsa \<notin> Pos v)" |
|
1577 using a1 by fastforce |
|
1578 have "\<And>ns. pflat_len (Stars (v # vs)) ns = pflat_len (Stars (va # vsa)) ns \<or> \<not> ns \<sqsubset>lex 0 # list \<or> (\<forall>nsa. ns \<noteq> 0 # nsa \<or> nsa \<notin> Pos va)" |
|
1579 using a1 by fastforce |
|
1580 then show False |
|
1581 using f5 a4 a3 a2 by (metis (no_types) Sulzmann.lexordp_simps(3) Un_iff pflat_len_Stars_simps2(2) val_ord_def) |
|
1582 next |
|
1583 fix v abd vs and va and ra and vsa and p a and list and nat |
|
1584 assume "flat va \<in> ra \<rightarrow> v" |
|
1585 "concat (map flat vsa) \<in> STAR ra \<rightarrow> Stars vs" "flat v \<noteq> []" |
|
1586 "\<forall>s\<^sub>3. flat va @ s\<^sub>3 \<in> L ra \<longrightarrow> s\<^sub>3 = [] \<or> (\<forall>s\<^sub>4. s\<^sub>3 @ s\<^sub>4 = concat (map flat vsa) \<longrightarrow> s\<^sub>4 \<notin> L ra\<star>)" |
|
1587 "\<Turnstile> va : ra" "flat va \<noteq> []" |
|
1588 "\<Turnstile> Stars vsa : STAR ra" |
|
1589 "\<forall>p. \<not> va \<sqsubset>val p v" "Stars (va # vsa) \<sqsubset>val a # list Stars (v # vs)" |
|
1590 "\<not> Stars vsa :\<sqsubset>val Stars vs" "a = Suc nat" |
|
1591 then show "False" |
|
1592 apply - |
|
1593 apply(subst (asm) val_ord_ex_def) |
|
1594 apply(simp) |
|
1595 apply(drule STAR_val_ord) |
|
1596 using Posix1(2) apply auto[1] |
|
1597 apply blast |
|
1598 done |
|
1599 next |
|
1600 fix r |
|
1601 show " \<forall>v2\<in>CPT (STAR r) []. \<not> v2 :\<sqsubset>val Stars []" |
|
1602 apply - |
|
1603 apply(rule ballI) |
|
1604 apply(simp add: CPT_def) |
|
1605 apply(auto) |
|
1606 apply(erule CPrf.cases) |
|
1607 apply(simp_all) |
|
1608 apply(simp add: val_ord_ex_def) |
|
1609 apply(clarify) |
|
1610 apply(simp add: val_ord_def) |
|
1611 done |
|
1612 qed |
|
1613 |
1416 |
1614 |
1417 definition Minval :: "rexp \<Rightarrow> string \<Rightarrow> val \<Rightarrow> bool" |
1615 definition Minval :: "rexp \<Rightarrow> string \<Rightarrow> val \<Rightarrow> bool" |
1418 where |
1616 where |
1419 "Minval r s v \<equiv> \<Turnstile> v : r \<and> flat v = s \<and> (\<forall>v' \<in> CPT r s. v :\<sqsubset>val v' \<or> v = v')" |
1617 "Minval r s v \<equiv> \<Turnstile> v : r \<and> flat v = s \<and> (\<forall>v' \<in> CPT r s. v :\<sqsubset>val v' \<or> v = v')" |
1420 |
1618 |