817 apply(rule ValOrd.intros(2)) |
817 apply(rule ValOrd.intros(2)) |
818 prefer 2 |
818 prefer 2 |
819 apply (metis list.distinct(1) mkeps_flat v4) |
819 apply (metis list.distinct(1) mkeps_flat v4) |
820 by (metis h) |
820 by (metis h) |
821 |
821 |
|
822 lemma Prf_inj_test: |
|
823 assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" "flat v1 = flat v2" |
|
824 shows "(injval r c v1) \<succ>r (injval r c v2)" |
|
825 sorry |
|
826 |
822 lemma Prf_inj: |
827 lemma Prf_inj: |
823 assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" (*"flat v1 = flat v2"*) |
828 assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" (*"flat v1 = flat v2"*) |
824 shows "(injval r c v1) \<succ>r (injval r c v2)" |
829 shows "(injval r c v1) \<succ>r (injval r c v2)" |
825 using assms |
830 using assms |
826 apply(induct arbitrary: v1 v2 rule: der.induct) |
831 apply(induct arbitrary: v1 v2 rule: der.induct) |
941 apply(clarify) |
946 apply(clarify) |
942 apply(simp) |
947 apply(simp) |
943 apply(rule ValOrd.intros(2)) |
948 apply(rule ValOrd.intros(2)) |
944 apply (metis h) |
949 apply (metis h) |
945 apply (metis list.distinct(1) mkeps_flat v4) |
950 apply (metis list.distinct(1) mkeps_flat v4) |
|
951 (* last case *) |
946 apply(clarify) |
952 apply(clarify) |
947 apply(erule Prf.cases) |
953 apply(erule Prf.cases) |
948 apply(simp_all)[5] |
954 apply(simp_all)[5] |
949 apply(clarify) |
955 apply(clarify) |
950 apply(rotate_tac 6) |
956 apply(rotate_tac 6) |
951 apply(erule Prf.cases) |
957 apply(erule Prf.cases) |
952 apply(simp_all)[5] |
958 apply(simp_all)[5] |
953 apply(clarify) |
959 apply(clarify) |
954 apply(erule ValOrd.cases) |
|
955 apply(simp_all)[8] |
|
956 apply(clarify) |
|
957 apply(simp) |
|
958 prefer 2 |
960 prefer 2 |
959 apply(clarify) |
961 apply(clarify) |
960 apply(erule ValOrd.cases) |
962 apply(erule ValOrd.cases) |
961 apply(simp_all)[8] |
963 apply(simp_all)[8] |
962 apply(clarify) |
964 apply(clarify) |
963 apply(rule ValOrd.intros(1)) |
965 apply(rule ValOrd.intros(1)) |
964 apply(metis) |
966 apply(metis) |
|
967 apply(rule ValOrd.intros(2)) |
|
968 prefer 2 |
965 thm mkeps_flat v4 |
969 thm mkeps_flat v4 |
966 apply (metis list.distinct(1) mkeps_flat v4) |
970 apply (metis list.distinct(1) mkeps_flat v4) |
967 defer |
971 oops |
968 apply(clarify) |
972 |
969 apply(erule ValOrd.cases) |
973 lemma POSIX_der: |
970 apply(simp_all)[8] |
974 assumes "POSIX v (der c r)" "\<turnstile> v : der c r" |
971 apply(clarify) |
975 shows "POSIX (injval r c v) r" |
972 apply(rule ValOrd.intros(1)) |
976 using assms |
973 apply(metis) |
977 unfolding POSIX_def |
974 apply(drule_tac x="v1" in meta_spec) |
978 apply(auto) |
975 apply(rotate_tac 7) |
979 thm v3 |
976 apply(drule_tac x="projval r1 c (mkeps r1)" in meta_spec) |
980 apply (metis v3) |
977 apply(drule meta_mp) |
981 thm v4 |
978 |
982 apply(subst (asm) v4) |
979 defer |
983 apply(assumption) |
980 apply(erule ValOrd.cases) |
984 apply(drule_tac x="projval r c v'" in spec) |
981 apply(simp_all del: injval.simps)[8] |
985 apply(drule mp) |
982 apply(simp) |
986 apply(rule conjI) |
983 apply(clarify) |
987 thm v3_proj |
984 apply(simp) |
988 apply(rule v3_proj) |
985 apply(erule Prf.cases) |
989 apply(simp) |
986 apply(simp_all)[5] |
990 apply(rule_tac x="flat v" in exI) |
987 apply(erule Prf.cases) |
991 apply(simp) |
988 apply(simp_all)[5] |
992 thm t |
989 apply(clarify) |
993 apply(rule_tac c="c" in t) |
990 apply(erule Prf.cases) |
994 apply(simp) |
991 apply(simp_all)[5] |
995 thm v4_proj |
992 apply(clarify) |
996 apply(subst v4_proj) |
993 apply(rule ValOrd.intros(2)) |
997 apply(simp) |
|
998 apply(rule_tac x="flat v" in exI) |
|
999 apply(simp) |
|
1000 apply(simp) |
|
1001 thm Prf_inj_test |
|
1002 apply(drule Prf_inj_test) |
|
1003 apply(simp) |
|
1004 apply (metis v3_proj) |
|
1005 apply(rule_tac c="c" in t) |
|
1006 apply(simp) |
|
1007 thm v4_proj |
|
1008 apply(subst v4_proj) |
|
1009 apply(simp) |
|
1010 apply(rule_tac x="flat v" in exI) |
|
1011 apply(simp) |
|
1012 apply(simp) |
|
1013 |
|
1014 apply(simp add: Cons_eq_append_conv) |
|
1015 apply(auto)[1] |
|
1016 |
994 |
1017 |
995 |
1018 |
996 lemma POSIX_ex: "\<turnstile> v : r \<Longrightarrow> \<exists>v. POSIX v r" |
1019 lemma POSIX_ex: "\<turnstile> v : r \<Longrightarrow> \<exists>v. POSIX v r" |
997 apply(induct r arbitrary: v) |
1020 apply(induct r arbitrary: v) |
998 apply(erule Prf.cases) |
1021 apply(erule Prf.cases) |
1605 apply(rule ValOrd.intros(2)) |
1628 apply(rule ValOrd.intros(2)) |
1606 oops |
1629 oops |
1607 *} |
1630 *} |
1608 oops |
1631 oops |
1609 |
1632 |
1610 lemma POSIX_der: |
1633 |
1611 assumes "POSIX v (der c r)" "\<turnstile> v : der c r" |
|
1612 shows "POSIX (injval r c v) r" |
|
1613 using assms |
|
1614 unfolding POSIX_def |
|
1615 apply(auto) |
|
1616 thm v4 |
|
1617 apply(subst (asm) v4) |
|
1618 apply(assumption) |
|
1619 apply(drule_tac x="projval r c v'" in spec) |
|
1620 apply(auto) |
|
1621 apply(rule v3_proj) |
|
1622 apply(simp) |
|
1623 apply(rule_tac x="flat v" in exI) |
|
1624 apply(simp) |
|
1625 apply(rule_tac c="c" in t) |
|
1626 apply(simp) |
|
1627 apply(subst v4_proj) |
|
1628 apply(simp) |
|
1629 apply(rule_tac x="flat v" in exI) |
|
1630 apply(simp) |
|
1631 apply(simp) |
|
1632 apply(simp add: Cons_eq_append_conv) |
|
1633 apply(auto)[1] |
|
1634 |
1634 |
1635 text {* |
1635 text {* |
1636 Injection followed by projection is the identity. |
1636 Injection followed by projection is the identity. |
1637 *} |
1637 *} |
1638 |
1638 |