824 apply(simp add: L_flat_Prf) |
824 apply(simp add: L_flat_Prf) |
825 apply(auto) |
825 apply(auto) |
826 apply (metis v3_proj v4_proj2) |
826 apply (metis v3_proj v4_proj2) |
827 done |
827 done |
828 |
828 |
|
829 lemma |
|
830 "lex2 (ALT (CHAR a) (ALT (CHAR b) (SEQ (CHAR a) (CHAR b)))) [a,b] = Right (Right (Seq (Char a) (Char b)))" |
|
831 apply(simp) |
|
832 done |
|
833 |
|
834 |
829 section {* Sulzmann's Ordering of values *} |
835 section {* Sulzmann's Ordering of values *} |
830 |
836 |
831 thm PMatch.intros |
837 thm PMatch.intros |
832 |
838 |
833 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100) |
839 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100) |
868 "\<lbrakk>v1 2\<succ> v2; \<turnstile> v1 : r\<rbrakk> \<Longrightarrow> v1 \<succ>r v2" |
874 "\<lbrakk>v1 2\<succ> v2; \<turnstile> v1 : r\<rbrakk> \<Longrightarrow> v1 \<succ>r v2" |
869 apply(induct v1 v2 arbitrary: r rule: ValOrd2.induct) |
875 apply(induct v1 v2 arbitrary: r rule: ValOrd2.induct) |
870 apply(auto intro: ValOrd.intros elim: Prf.cases) |
876 apply(auto intro: ValOrd.intros elim: Prf.cases) |
871 done |
877 done |
872 |
878 |
|
879 section {* Posix definition *} |
|
880 |
|
881 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" |
|
882 where |
|
883 "POSIX v r \<equiv> (\<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> flat v' \<sqsubseteq> flat v) \<longrightarrow> v \<succ>r v'))" |
|
884 |
873 lemma ValOrd_refl: |
885 lemma ValOrd_refl: |
874 assumes "\<turnstile> v : r" |
886 assumes "\<turnstile> v : r" |
875 shows "v \<succ>r v" |
887 shows "v \<succ>r v" |
876 using assms |
888 using assms |
877 apply(induct) |
889 apply(induct) |
973 apply(simp_all)[8] |
985 apply(simp_all)[8] |
974 apply(erule ValOrd.cases) |
986 apply(erule ValOrd.cases) |
975 apply(simp_all)[8] |
987 apply(simp_all)[8] |
976 done |
988 done |
977 |
989 |
|
990 lemma POSIX_ALT_I1: |
|
991 assumes "POSIX v1 r1" |
|
992 shows "POSIX (Left v1) (ALT r1 r2)" |
|
993 using assms |
|
994 unfolding POSIX_def |
|
995 apply(auto) |
|
996 apply (metis Prf.intros(2)) |
|
997 apply(rotate_tac 2) |
|
998 apply(erule Prf.cases) |
|
999 apply(simp_all)[5] |
|
1000 apply(auto) |
|
1001 apply(rule ValOrd.intros) |
|
1002 apply(auto) |
|
1003 apply(rule ValOrd.intros) |
|
1004 by (metis le_eq_less_or_eq length_sprefix sprefix_def) |
|
1005 |
|
1006 lemma POSIX_ALT_I2: |
|
1007 assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')" |
|
1008 shows "POSIX (Right v2) (ALT r1 r2)" |
|
1009 using assms |
|
1010 unfolding POSIX_def |
|
1011 apply(auto) |
|
1012 apply (metis Prf.intros) |
|
1013 apply(rotate_tac 3) |
|
1014 apply(erule Prf.cases) |
|
1015 apply(simp_all)[5] |
|
1016 apply(auto) |
|
1017 apply(rule ValOrd.intros) |
|
1018 apply metis |
|
1019 apply(rule ValOrd.intros) |
|
1020 apply metis |
|
1021 done |
|
1022 |
|
1023 thm PMatch.intros[no_vars] |
|
1024 |
|
1025 lemma POSIX_PMatch: |
|
1026 assumes "s \<in> r \<rightarrow> v" "\<turnstile> v' : r" |
|
1027 shows "length (flat v') \<le> length (flat v)" |
|
1028 using assms |
|
1029 apply(induct arbitrary: s v v' rule: rexp.induct) |
|
1030 apply(erule Prf.cases) |
|
1031 apply(simp_all)[5] |
|
1032 apply(erule Prf.cases) |
|
1033 apply(simp_all)[5] |
|
1034 apply(erule Prf.cases) |
|
1035 apply(simp_all)[5] |
|
1036 apply(erule PMatch.cases) |
|
1037 apply(simp_all)[5] |
|
1038 defer |
|
1039 apply(erule Prf.cases) |
|
1040 apply(simp_all)[5] |
|
1041 apply(erule PMatch.cases) |
|
1042 apply(simp_all)[5] |
|
1043 apply(clarify) |
|
1044 apply(simp add: L_flat_Prf) |
|
1045 |
|
1046 apply(clarify) |
|
1047 apply (metis ValOrd.intros(8)) |
|
1048 apply (metis POSIX_ALT_I1) |
|
1049 apply(rule POSIX_ALT_I2) |
|
1050 apply(simp) |
|
1051 apply(auto)[1] |
|
1052 apply(simp add: POSIX_def) |
|
1053 apply(frule PMatch1(1)) |
|
1054 apply(frule PMatch1(2)) |
|
1055 apply(simp) |
|
1056 |
|
1057 |
|
1058 lemma POSIX_PMatch: |
|
1059 assumes "s \<in> r \<rightarrow> v" |
|
1060 shows "POSIX v r" |
|
1061 using assms |
|
1062 apply(induct arbitrary: rule: PMatch.induct) |
|
1063 apply(auto) |
|
1064 apply(simp add: POSIX_def) |
|
1065 apply(auto)[1] |
|
1066 apply (metis Prf.intros(4)) |
|
1067 apply(erule Prf.cases) |
|
1068 apply(simp_all)[5] |
|
1069 apply (metis ValOrd.intros(7)) |
|
1070 apply(simp add: POSIX_def) |
|
1071 apply(auto)[1] |
|
1072 apply (metis Prf.intros(5)) |
|
1073 apply(erule Prf.cases) |
|
1074 apply(simp_all)[5] |
|
1075 apply (metis ValOrd.intros(8)) |
|
1076 apply (metis POSIX_ALT_I1) |
|
1077 apply(rule POSIX_ALT_I2) |
|
1078 apply(simp) |
|
1079 apply(auto)[1] |
|
1080 apply(simp add: POSIX_def) |
|
1081 apply(frule PMatch1(1)) |
|
1082 apply(frule PMatch1(2)) |
|
1083 apply(simp) |
|
1084 |
|
1085 |
978 |
1086 |
979 lemma ValOrd_PMatch: |
1087 lemma ValOrd_PMatch: |
980 assumes "s \<in> r \<rightarrow> v1" "\<turnstile> v2 : r" "flat v2 = s" |
1088 assumes "s \<in> r \<rightarrow> v1" "\<turnstile> v2 : r" "flat v2 = s" |
981 shows "v1 \<succ>r v2" |
1089 shows "v1 \<succ>r v2" |
982 using assms |
1090 using assms |
996 apply(erule Prf.cases) |
1104 apply(erule Prf.cases) |
997 apply(simp_all)[5] |
1105 apply(simp_all)[5] |
998 apply(clarify) |
1106 apply(clarify) |
999 apply (metis Prf_flat_L) |
1107 apply (metis Prf_flat_L) |
1000 apply (metis ValOrd.intros(5)) |
1108 apply (metis ValOrd.intros(5)) |
|
1109 (* Seq case *) |
1001 apply(erule Prf.cases) |
1110 apply(erule Prf.cases) |
1002 apply(simp_all)[5] |
1111 apply(simp_all)[5] |
1003 apply(auto) |
1112 apply(auto) |
1004 apply(case_tac "v1 = v1a") |
1113 apply(case_tac "v1 = v1a") |
1005 apply(auto) |
1114 apply(auto) |
1006 apply (metis PMatch1(2) ValOrd.intros(1) same_append_eq) |
1115 apply (metis PMatch1(2) ValOrd.intros(1) same_append_eq) |
1007 apply(rule ValOrd.intros(2)) |
1116 apply(rule ValOrd.intros(2)) |
1008 apply(auto) |
1117 apply(auto) |
|
1118 apply(drule_tac x="v1a" in meta_spec) |
|
1119 apply(drule_tac meta_mp) |
|
1120 apply(simp) |
|
1121 apply(drule_tac meta_mp) |
|
1122 prefer 2 |
|
1123 apply(simp) |
|
1124 apply(simp add: append_eq_append_conv2) |
|
1125 apply(auto) |
|
1126 apply (metis Prf_flat_L) |
|
1127 apply(case_tac "us = []") |
|
1128 apply(simp) |
|
1129 apply(drule_tac x="us" in spec) |
|
1130 apply(drule mp) |
|
1131 |
1009 thm L_flat_Prf |
1132 thm L_flat_Prf |
1010 apply(simp add: L_flat_Prf) |
1133 apply(simp add: L_flat_Prf) |
1011 thm append_eq_append_conv2 |
1134 thm append_eq_append_conv2 |
1012 apply(simp add: append_eq_append_conv2) |
1135 apply(simp add: append_eq_append_conv2) |
1013 apply(auto) |
1136 apply(auto) |
1015 apply(drule mp) |
1138 apply(drule mp) |
1016 apply metis |
1139 apply metis |
1017 apply (metis append_Nil2) |
1140 apply (metis append_Nil2) |
1018 apply(case_tac "us = []") |
1141 apply(case_tac "us = []") |
1019 apply(auto) |
1142 apply(auto) |
|
1143 apply(drule_tac x="s2" in spec) |
|
1144 apply(drule mp) |
|
1145 |
|
1146 apply(auto)[1] |
1020 apply(drule_tac x="v1a" in meta_spec) |
1147 apply(drule_tac x="v1a" in meta_spec) |
1021 apply(simp) |
1148 apply(simp) |
1022 |
1149 |
1023 lemma refl_on_ValOrd: |
1150 lemma refl_on_ValOrd: |
1024 "refl_on (Values r s) {(v1, v2). v1 \<succ>r v2 \<and> v1 \<in> Values r s \<and> v2 \<in> Values r s}" |
1151 "refl_on (Values r s) {(v1, v2). v1 \<succ>r v2 \<and> v1 \<in> Values r s \<and> v2 \<in> Values r s}" |