137 | "flats(Left v) = flats(v)" |
137 | "flats(Left v) = flats(v)" |
138 | "flats(Right v) = flats(v)" |
138 | "flats(Right v) = flats(v)" |
139 | "flats(Seq v1 v2) = (flats v1) @ (flats v2)" |
139 | "flats(Seq v1 v2) = (flats v1) @ (flats v2)" |
140 |
140 |
141 value "flats(Seq(Char c)(Char b))" |
141 value "flats(Seq(Char c)(Char b))" |
|
142 |
|
143 inductive StrOrd :: "string list \<Rightarrow> string list \<Rightarrow> bool" ("_ \<sqsupset> _" [100, 100] 100) |
|
144 where |
|
145 "[] \<sqsupset> []" |
|
146 | "xs \<sqsupset> ys \<Longrightarrow> (x#xs) \<sqsupset> (x#ys)" |
|
147 | "length x \<ge> length y \<Longrightarrow> (x#xs) \<sqsupset> (y#xs)" |
|
148 |
|
149 lemma StrOrd_append: |
|
150 "xs \<sqsupset> ys \<Longrightarrow> (zs @ xs) \<sqsupset> (zs @ ys)" |
|
151 apply(induct zs) |
|
152 apply(auto intro: StrOrd.intros) |
|
153 done |
142 |
154 |
143 section {* Relation between values and regular expressions *} |
155 section {* Relation between values and regular expressions *} |
144 |
156 |
145 inductive Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100) |
157 inductive Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100) |
146 where |
158 where |
231 | "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')" |
243 | "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')" |
232 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')" |
244 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')" |
233 | "Void \<succ>EMPTY Void" |
245 | "Void \<succ>EMPTY Void" |
234 | "(Char c) \<succ>(CHAR c) (Char c)" |
246 | "(Char c) \<succ>(CHAR c) (Char c)" |
235 |
247 |
236 inductive ValOrd2 :: "val \<Rightarrow> rexp \<Rightarrow> nat \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsupset>_,_ _" [100, 100, 100, 100] 100) |
248 inductive ValOrd2 :: "val \<Rightarrow> val \<Rightarrow> bool" ("_ 2\<succ> _" [100, 100] 100) |
237 where |
249 where |
238 "v2 \<sqsupset>r2,n v2' \<Longrightarrow> (Seq v1 v2) \<sqsupset>(SEQ r1 r2),(length (flat v1) + n) (Seq v1 v2')" |
250 "v2 2\<succ> v2' \<Longrightarrow> (Seq v1 v2) 2\<succ> (Seq v1 v2')" |
239 | "\<lbrakk>v1 \<sqsupset>r1,n v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<sqsupset>(SEQ r1 r2),(n + length (flat v2)) (Seq v1' v2')" |
251 | "\<lbrakk>v1 2\<succ> v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) 2\<succ> (Seq v1' v2')" |
240 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<sqsupset>(ALT r1 r2),(length (flat v1)) (Right v2)" |
252 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) 2\<succ> (Right v2)" |
241 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<sqsupset>(ALT r1 r2),(length (flat v2)) (Left v1)" |
253 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) 2\<succ> (Left v1)" |
242 | "v2 \<sqsupset>r2,n v2' \<Longrightarrow> (Right v2) \<sqsupset>(ALT r1 r2),n (Right v2')" |
254 | "v2 2\<succ> v2' \<Longrightarrow> (Right v2) 2\<succ> (Right v2')" |
243 | "v1 \<sqsupset>r1,n v1' \<Longrightarrow> (Left v1) \<sqsupset>(ALT r1 r2),n (Left v1')" |
255 | "v1 2\<succ> v1' \<Longrightarrow> (Left v1) 2\<succ> (Left v1')" |
244 | "Void \<sqsupset>EMPTY,0 Void" |
256 | "Void 2\<succ> Void" |
245 | "(Char c) \<sqsupset>(CHAR c),1 (Char c)" |
257 | "(Char c) 2\<succ> (Char c)" |
246 |
258 |
247 lemma |
259 lemma Ord1: |
248 assumes "v1 \<sqsupset>r,n v2" |
260 "v1 \<succ>r v2 \<Longrightarrow> v1 2\<succ> v2" |
249 shows "length(flat v1) = n" |
261 apply(induct rule: ValOrd.induct) |
250 using assms |
262 apply(auto intro: ValOrd2.intros) |
251 apply(induct) |
263 done |
252 apply(auto) |
264 |
253 done |
265 lemma Ord2: |
254 |
266 "v1 2\<succ> v2 \<Longrightarrow> \<exists>r. v1 \<succ>r v2" |
255 lemma |
267 apply(induct v1 v2 rule: ValOrd2.induct) |
256 assumes "v1 \<sqsupset>r,n v2" |
268 apply(auto intro: ValOrd.intros) |
257 shows "length(flat v2) <= n" |
269 done |
258 using assms |
270 |
259 apply(induct) |
271 lemma Ord3: |
260 apply(auto) |
272 "\<lbrakk>v1 2\<succ> v2; \<turnstile> v1 : r\<rbrakk> \<Longrightarrow> v1 \<succ>r v2" |
261 oops |
273 apply(induct v1 v2 arbitrary: r rule: ValOrd2.induct) |
262 |
274 apply(auto intro: ValOrd.intros elim: Prf.cases) |
263 |
275 done |
264 section {* The ordering is reflexive *} |
276 |
265 |
277 |
266 lemma ValOrd_refl: |
278 lemma ValOrd_refl: |
267 assumes "\<turnstile> v : r" |
279 assumes "\<turnstile> v : r" |
268 shows "v \<succ>r v" |
280 shows "v \<succ>r v" |
269 using assms |
281 using assms |
274 section {* Posix definition *} |
286 section {* Posix definition *} |
275 |
287 |
276 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" |
288 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" |
277 where |
289 where |
278 "POSIX v r \<equiv> (\<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v \<succ>r v'))" |
290 "POSIX v r \<equiv> (\<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v \<succ>r v'))" |
|
291 |
|
292 definition POSIX2 :: "val \<Rightarrow> rexp \<Rightarrow> bool" |
|
293 where |
|
294 "POSIX2 v r \<equiv> (\<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v 2\<succ> v'))" |
|
295 |
|
296 lemma "POSIX v r = POSIX2 v r" |
|
297 unfolding POSIX_def POSIX2_def |
|
298 apply(auto) |
|
299 apply(rule Ord1) |
|
300 apply(auto) |
|
301 apply(rule Ord3) |
|
302 apply(auto) |
|
303 done |
279 |
304 |
280 (* |
305 (* |
281 an alternative definition: might cause problems |
306 an alternative definition: might cause problems |
282 with theorem mkeps_POSIX |
307 with theorem mkeps_POSIX |
283 *) |
308 *) |
882 apply(simp) |
907 apply(simp) |
883 apply(rule ValOrd.intros(2)) |
908 apply(rule ValOrd.intros(2)) |
884 prefer 2 |
909 prefer 2 |
885 apply (metis list.distinct(1) mkeps_flat v4) |
910 apply (metis list.distinct(1) mkeps_flat v4) |
886 by (metis h) |
911 by (metis h) |
|
912 |
|
913 lemma POSIX_der: |
|
914 assumes "POSIX2 v (der c r)" "\<turnstile> v : der c r" |
|
915 shows "POSIX2 (injval r c v) r" |
|
916 using assms |
|
917 unfolding POSIX2_def |
|
918 apply(auto) |
|
919 thm v3 |
|
920 apply (erule v3) |
|
921 thm v4 |
|
922 apply(subst (asm) v4) |
|
923 apply(assumption) |
|
924 apply(drule_tac x="projval r c v'" in spec) |
|
925 apply(drule mp) |
|
926 apply(rule conjI) |
|
927 thm v3_proj |
|
928 apply(rule v3_proj) |
|
929 apply(simp) |
|
930 apply(rule_tac x="flat v" in exI) |
|
931 apply(simp) |
|
932 thm t |
|
933 apply(rule_tac c="c" in t) |
|
934 apply(simp) |
|
935 thm v4_proj |
|
936 apply(subst v4_proj) |
|
937 apply(simp) |
|
938 apply(rule_tac x="flat v" in exI) |
|
939 apply(simp) |
|
940 apply(simp) |
|
941 oops |
|
942 |
887 |
943 |
888 lemma Prf_inj_test: |
944 lemma Prf_inj_test: |
889 assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" "\<Turnstile> vs : rs" "flat v1 = flat v2" |
945 assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r" "\<Turnstile> vs : rs" "flat v1 = flat v2" |
890 shows "Seqs (injval r c v1) vs \<succ>(SEQS r rs) Seqs (injval r c v2) vs" |
946 shows "Seqs (injval r c v1) vs \<succ>(SEQS r rs) Seqs (injval r c v2) vs" |
891 using assms |
947 using assms |