11 where |
11 where |
12 "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}" |
12 "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}" |
13 |
13 |
14 text {* Two Simple Properties about Sequential Composition *} |
14 text {* Two Simple Properties about Sequential Composition *} |
15 |
15 |
16 lemma seq_empty [simp]: |
16 lemma Sequ_empty_string [simp]: |
17 shows "A ;; {[]} = A" |
17 shows "A ;; {[]} = A" |
18 and "{[]} ;; A = A" |
18 and "{[]} ;; A = A" |
19 by (simp_all add: Sequ_def) |
19 by (simp_all add: Sequ_def) |
20 |
20 |
21 lemma seq_null [simp]: |
21 lemma Sequ_empty [simp]: |
22 shows "A ;; {} = {}" |
22 shows "A ;; {} = {}" |
23 and "{} ;; A = {}" |
23 and "{} ;; A = {}" |
24 by (simp_all add: Sequ_def) |
24 by (simp_all add: Sequ_def) |
25 |
25 |
26 |
26 |
69 for A :: "string set" |
69 for A :: "string set" |
70 where |
70 where |
71 start[intro]: "[] \<in> A\<star>" |
71 start[intro]: "[] \<in> A\<star>" |
72 | step[intro]: "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>" |
72 | step[intro]: "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>" |
73 |
73 |
74 lemma star_cases: |
74 (* Arden's lemma *) |
|
75 |
|
76 lemma Star_cases: |
75 shows "A\<star> = {[]} \<union> A ;; A\<star>" |
77 shows "A\<star> = {[]} \<union> A ;; A\<star>" |
76 unfolding Sequ_def |
78 unfolding Sequ_def |
77 by (auto) (metis Star.simps) |
79 by (auto) (metis Star.simps) |
78 |
80 |
79 lemma star_decomp: |
81 lemma Star_decomp: |
80 assumes a: "c # x \<in> A\<star>" |
82 assumes a: "c # x \<in> A\<star>" |
81 shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>" |
83 shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>" |
82 using a |
84 using a |
83 by (induct x\<equiv>"c # x" rule: Star.induct) |
85 by (induct x\<equiv>"c # x" rule: Star.induct) |
84 (auto simp add: append_eq_Cons_conv) |
86 (auto simp add: append_eq_Cons_conv) |
85 |
87 |
86 lemma Der_star [simp]: |
88 lemma Der_star [simp]: |
87 shows "Der c (A\<star>) = (Der c A) ;; A\<star>" |
89 shows "Der c (A\<star>) = (Der c A) ;; A\<star>" |
88 proof - |
90 proof - |
89 have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)" |
91 have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)" |
90 by (simp only: star_cases[symmetric]) |
92 by (simp only: Star_cases[symmetric]) |
91 also have "... = Der c (A ;; A\<star>)" |
93 also have "... = Der c (A ;; A\<star>)" |
92 by (simp only: Der_union Der_empty) (simp) |
94 by (simp only: Der_union Der_empty) (simp) |
93 also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})" |
95 also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})" |
94 by simp |
96 by simp |
95 also have "... = (Der c A) ;; A\<star>" |
97 also have "... = (Der c A) ;; A\<star>" |
96 unfolding Sequ_def Der_def |
98 unfolding Sequ_def Der_def |
97 by (auto dest: star_decomp) |
99 by (auto dest: Star_decomp) |
98 finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" . |
100 finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" . |
99 qed |
101 qed |
100 |
102 |
101 |
103 |
102 section {* Regular Expressions *} |
104 section {* Regular Expressions *} |
289 apply (metis empty_iff list.set(1)) |
291 apply (metis empty_iff list.set(1)) |
290 by (metis concat.simps(2) list.simps(9) set_ConsD) |
292 by (metis concat.simps(2) list.simps(9) set_ConsD) |
291 |
293 |
292 |
294 |
293 lemma L_flat_Prf1: |
295 lemma L_flat_Prf1: |
294 assumes "\<turnstile> v : r" shows "flat v \<in> L r" |
296 assumes "\<turnstile> v : r" |
|
297 shows "flat v \<in> L r" |
295 using assms |
298 using assms |
296 by (induct)(auto simp add: Sequ_def) |
299 by (induct)(auto simp add: Sequ_def) |
297 |
300 |
298 lemma L_flat_Prf2: |
301 lemma L_flat_Prf2: |
299 assumes "s \<in> L r" shows "\<exists>v. \<turnstile> v : r \<and> flat v = s" |
302 assumes "s \<in> L r" |
|
303 shows "\<exists>v. \<turnstile> v : r \<and> flat v = s" |
300 using assms |
304 using assms |
301 apply(induct r arbitrary: s) |
305 apply(induct r arbitrary: s) |
302 apply(auto simp add: Sequ_def intro: Prf.intros) |
306 apply(auto simp add: Sequ_def intro: Prf.intros) |
303 using Prf.intros(1) flat.simps(5) apply blast |
307 using Prf.intros(1) flat.simps(5) apply blast |
304 using Prf.intros(2) flat.simps(3) apply blast |
308 using Prf.intros(2) flat.simps(3) apply blast |
322 assumes "s \<in> (L r)\<star>" |
326 assumes "s \<in> (L r)\<star>" |
323 shows "\<exists>vs. concat (map flat vs) = s \<and> \<turnstile> Stars vs : STAR r" |
327 shows "\<exists>vs. concat (map flat vs) = s \<and> \<turnstile> Stars vs : STAR r" |
324 using assms |
328 using assms |
325 apply(drule_tac Star_string) |
329 apply(drule_tac Star_string) |
326 apply(auto) |
330 apply(auto) |
327 |
|
328 by (metis L_flat_Prf2 Prf_Stars Star_val) |
331 by (metis L_flat_Prf2 Prf_Stars Star_val) |
329 |
332 |
330 |
333 |
331 |
334 |
332 section {* Sulzmann and Lu functions *} |
335 section {* Sulzmann and Lu functions *} |