321 definition Values :: "rexp \<Rightarrow> string \<Rightarrow> val set" where |
321 definition Values :: "rexp \<Rightarrow> string \<Rightarrow> val set" where |
322 "Values r s \<equiv> {v. \<turnstile> v : r \<and> flat v \<sqsubseteq> s}" |
322 "Values r s \<equiv> {v. \<turnstile> v : r \<and> flat v \<sqsubseteq> s}" |
323 |
323 |
324 definition rest :: "val \<Rightarrow> string \<Rightarrow> string" where |
324 definition rest :: "val \<Rightarrow> string \<Rightarrow> string" where |
325 "rest v s \<equiv> drop (length (flat v)) s" |
325 "rest v s \<equiv> drop (length (flat v)) s" |
|
326 |
|
327 lemma rest_flat: |
|
328 assumes "flat v1 \<sqsubseteq> s" |
|
329 shows "flat v1 @ rest v1 s = s" |
|
330 using assms |
|
331 apply(auto simp add: rest_def prefix_def) |
|
332 done |
|
333 |
326 |
334 |
327 lemma rest_Suffixes: |
335 lemma rest_Suffixes: |
328 "rest v s \<in> Suffixes s" |
336 "rest v s \<in> Suffixes s" |
329 unfolding rest_def |
337 unfolding rest_def |
330 by (metis Suffixes_in append_take_drop_id) |
338 by (metis Suffixes_in append_take_drop_id) |
834 |
842 |
835 section {* Sulzmann's Ordering of values *} |
843 section {* Sulzmann's Ordering of values *} |
836 |
844 |
837 thm PMatch.intros |
845 thm PMatch.intros |
838 |
846 |
|
847 inductive ValOrds :: "string \<Rightarrow> val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<turnstile> _ \<succ>_ _" [100, 100, 100] 100) |
|
848 where |
|
849 "\<lbrakk>s2 \<turnstile> v2 \<succ>r2 v2'; flat v1 = s1\<rbrakk> \<Longrightarrow> (s1 @ s2) \<turnstile> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" |
|
850 | "\<lbrakk>s1 \<turnstile> v1 \<succ>r1 v1'; v1 \<noteq> v1'; flat v2 = s2; (flat v1' @ flat v2') \<sqsubseteq> (s1 @ s2)\<rbrakk> |
|
851 \<Longrightarrow> s1 @ s2 \<turnstile> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" |
|
852 | "\<lbrakk>(flat v2) \<sqsubseteq> (flat v1); flat v1 = s\<rbrakk> \<Longrightarrow> s \<turnstile> (Left v1) \<succ>(ALT r1 r2) (Right v2)" |
|
853 | "\<lbrakk>(flat v1) \<sqsubset> (flat v2); flat v2 = s\<rbrakk> \<Longrightarrow> s \<turnstile> (Right v2) \<succ>(ALT r1 r2) (Left v1)" |
|
854 | "s \<turnstile> v2 \<succ>r2 v2' \<Longrightarrow> s \<turnstile> (Right v2) \<succ>(ALT r1 r2) (Right v2')" |
|
855 | "s \<turnstile> v1 \<succ>r1 v1' \<Longrightarrow> s \<turnstile> (Left v1) \<succ>(ALT r1 r2) (Left v1')" |
|
856 | "[] \<turnstile> Void \<succ>EMPTY Void" |
|
857 | "[c] \<turnstile> (Char c) \<succ>(CHAR c) (Char c)" |
|
858 |
|
859 lemma valord_prefix: |
|
860 assumes "s \<turnstile> v1 \<succ>r v2" |
|
861 shows "flat v1 \<sqsubseteq> s" and "flat v2 \<sqsubseteq> s" |
|
862 using assms |
|
863 apply(induct) |
|
864 apply(auto) |
|
865 apply(simp add: prefix_def rest_def) |
|
866 apply(auto)[1] |
|
867 apply(simp add: prefix_def rest_def) |
|
868 apply(auto)[1] |
|
869 apply(auto simp add: prefix_def rest_def) |
|
870 done |
|
871 |
|
872 lemma valord_prefix2: |
|
873 assumes "s \<turnstile> v1 \<succ>r v2" |
|
874 shows "flat v2 \<sqsubseteq> flat v1" |
|
875 using assms |
|
876 apply(induct) |
|
877 apply(auto) |
|
878 apply(simp add: prefix_def rest_def) |
|
879 apply(simp add: prefix_def rest_def) |
|
880 apply(auto)[1] |
|
881 defer |
|
882 apply(simp add: prefix_def rest_def) |
|
883 apply(auto)[1] |
|
884 apply (metis append_eq_append_conv_if append_eq_conv_conj) |
|
885 apply(simp add: prefix_def rest_def) |
|
886 apply(auto)[1] |
|
887 apply (metis append_eq_append_conv_if append_take_drop_id le_eq_less_or_eq) |
|
888 apply(simp add: prefix_def rest_def) |
|
889 apply(simp add: prefix_def rest_def) |
|
890 |
|
891 |
839 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100) |
892 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100) |
840 where |
893 where |
841 "v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" |
894 "v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" |
842 | "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" |
895 | "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" |
843 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)" |
896 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)" |
1021 done |
1074 done |
1022 |
1075 |
1023 thm PMatch.intros[no_vars] |
1076 thm PMatch.intros[no_vars] |
1024 |
1077 |
1025 lemma POSIX_PMatch: |
1078 lemma POSIX_PMatch: |
1026 assumes "s \<in> r \<rightarrow> v" "\<turnstile> v' : r" |
1079 assumes "s \<in> r \<rightarrow> v" "v' \<in> Values r s" |
1027 shows "length (flat v') \<le> length (flat v)" |
1080 shows "v \<succ>r v' \<or> length (flat v') < length (flat v)" |
1028 using assms |
1081 using assms |
1029 apply(induct arbitrary: s v v' rule: rexp.induct) |
1082 apply(induct r arbitrary: s v v' rule: rexp.induct) |
|
1083 apply(simp_all add: Values_recs) |
|
1084 apply(erule PMatch.cases) |
|
1085 apply(simp_all)[5] |
|
1086 apply (metis ValOrd.intros(7)) |
|
1087 apply(erule PMatch.cases) |
|
1088 apply(simp_all)[5] |
|
1089 apply(simp add: prefix_def) |
|
1090 apply (metis ValOrd.intros(8)) |
|
1091 apply(auto)[1] |
|
1092 defer |
|
1093 apply(auto)[1] |
|
1094 apply(erule PMatch.cases) |
|
1095 apply(simp_all)[5] |
|
1096 apply (metis ValOrd.intros(6)) |
|
1097 apply (metis (no_types, lifting) PMatch1(2) Prf_flat_L Values_def length_sprefix mem_Collect_eq sprefix_def) |
|
1098 apply(erule PMatch.cases) |
|
1099 apply(simp_all)[5] |
|
1100 apply (metis (no_types, lifting) PMatch1(2) ValOrd.intros(3) Values_def length_sprefix mem_Collect_eq order_refl sprefix_def) |
|
1101 apply (metis ValOrd.intros(5)) |
|
1102 apply(erule PMatch.cases) |
|
1103 apply(simp_all)[5] |
|
1104 apply(auto) |
|
1105 apply(case_tac "v1a = v1") |
|
1106 apply(simp) |
|
1107 apply(rule ValOrd.intros(1)) |
|
1108 apply (metis PMatch1(2) append_Nil comm_monoid_diff_class.diff_cancel drop_0 drop_all drop_append order_refl rest_def) |
|
1109 apply(rule ValOrd.intros(2)) |
|
1110 apply(auto) |
|
1111 apply(drule_tac x="s1" in meta_spec) |
|
1112 apply(drule_tac x="v1a" in meta_spec) |
|
1113 apply(drule_tac x="v1" in meta_spec) |
|
1114 apply(auto) |
|
1115 apply(drule meta_mp) |
|
1116 defer |
|
1117 apply(auto)[1] |
|
1118 apply(frule PMatch1) |
|
1119 apply(drule PMatch1(2)) |
|
1120 apply(frule PMatch1) |
|
1121 apply(drule PMatch1(2)) |
|
1122 apply(auto)[1] |
|
1123 apply(simp add: Values_def) |
|
1124 apply(simp add: prefix_def) |
|
1125 apply(auto)[1] |
|
1126 apply(simp add: append_eq_append_conv2) |
|
1127 apply(auto)[1] |
|
1128 apply(rotate_tac 10) |
|
1129 apply(drule sym) |
|
1130 apply(simp) |
|
1131 apply(simp add: rest_def) |
|
1132 apply(case_tac "s3a = []") |
|
1133 apply(auto)[1] |
|
1134 |
|
1135 |
|
1136 apply (metis ValOrd.intros(6)) |
|
1137 apply (metis (no_types, lifting) PMatch1(2) ValOrd.intros(3) Values_def length_sprefix mem_Collect_eq order_refl sprefix_def) |
|
1138 apply(auto)[1] |
|
1139 apply (metis (no_types, lifting) PMatch1(2) Prf_flat_L Values_def length_sprefix mem_Collect_eq sprefix_def) |
|
1140 apply (metis ValOrd.intros(5)) |
|
1141 apply(auto)[1] |
1030 apply(erule Prf.cases) |
1142 apply(erule Prf.cases) |
1031 apply(simp_all)[5] |
1143 apply(simp_all)[5] |
1032 apply(erule Prf.cases) |
1144 apply(erule Prf.cases) |
1033 apply(simp_all)[5] |
1145 apply(simp_all)[5] |
1034 apply(erule Prf.cases) |
1146 apply(erule Prf.cases) |