50 and "{} ;; A = {}" |
50 and "{} ;; A = {}" |
51 by (simp_all add: Seq_def) |
51 by (simp_all add: Seq_def) |
52 |
52 |
53 lemma seq_union: |
53 lemma seq_union: |
54 shows "A ;; (B \<union> C) = A ;; B \<union> A ;; C" |
54 shows "A ;; (B \<union> C) = A ;; B \<union> A ;; C" |
|
55 and "(B \<union> C) ;; A = B ;; A \<union> C ;; A" |
55 by (auto simp add: Seq_def) |
56 by (auto simp add: Seq_def) |
56 |
57 |
57 lemma seq_Union: |
58 lemma seq_Union: |
58 shows "A ;; (\<Union>x\<in>B. C x) = (\<Union>x\<in>B. A ;; C x)" |
59 shows "A ;; (\<Union>x\<in>B. C x) = (\<Union>x\<in>B. A ;; C x)" |
59 by (auto simp add: Seq_def) |
60 by (auto simp add: Seq_def) |
60 |
61 |
61 lemma seq_empty_in [simp]: |
62 lemma seq_empty_in [simp]: |
62 "[] \<in> A ;; B \<longleftrightarrow> ([] \<in> A \<and> [] \<in> B)" |
63 "[] \<in> A ;; B \<longleftrightarrow> ([] \<in> A \<and> [] \<in> B)" |
63 by (simp add: Seq_def) |
64 by (simp add: Seq_def) |
64 |
65 |
|
66 lemma seq_assoc: |
|
67 shows "A ;; (B ;; C) = (A ;; B) ;; C" |
|
68 apply(auto simp add: Seq_def) |
|
69 apply(metis append_assoc) |
|
70 apply(metis) |
|
71 done |
|
72 |
|
73 |
|
74 section {* Power for Sets *} |
|
75 |
|
76 fun |
|
77 pow :: "string set \<Rightarrow> nat \<Rightarrow> string set" ("_ \<up> _" [101, 102] 101) |
|
78 where |
|
79 "A \<up> 0 = {[]}" |
|
80 | "A \<up> (Suc n) = A ;; (A \<up> n)" |
|
81 |
|
82 lemma pow_empty [simp]: |
|
83 shows "[] \<in> A \<up> n \<longleftrightarrow> (n = 0 \<or> [] \<in> A)" |
|
84 by (induct n) (auto) |
|
85 |
|
86 lemma pow_plus: |
|
87 "A \<up> (n + m) = A \<up> n ;; A \<up> m" |
|
88 by (induct n) (simp_all add: seq_assoc) |
|
89 |
65 section {* Kleene Star for Sets *} |
90 section {* Kleene Star for Sets *} |
66 |
91 |
67 inductive_set |
92 inductive_set |
68 Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102) |
93 Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102) |
69 for A :: "string set" |
94 for A :: "string set" |
70 where |
95 where |
71 start[intro]: "[] \<in> A\<star>" |
96 start[intro]: "[] \<in> A\<star>" |
72 | step[intro]: "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>" |
97 | step[intro]: "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>" |
73 |
98 |
74 |
|
75 text {* A Standard Property of Star *} |
99 text {* A Standard Property of Star *} |
76 |
|
77 lemma star_cases: |
|
78 shows "A\<star> = {[]} \<union> A ;; A\<star>" |
|
79 unfolding Seq_def |
|
80 by (auto) (metis Star.simps) |
|
81 |
100 |
82 lemma star_decomp: |
101 lemma star_decomp: |
83 assumes a: "c # x \<in> A\<star>" |
102 assumes a: "c # x \<in> A\<star>" |
84 shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>" |
103 shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>" |
|
104 using a |
85 using a |
105 using a |
86 by (induct x\<equiv>"c # x" rule: Star.induct) |
106 by (induct x\<equiv>"c # x" rule: Star.induct) |
87 (auto simp add: append_eq_Cons_conv) |
107 (auto simp add: append_eq_Cons_conv) |
88 |
108 |
89 section {* Power for Sets *} |
109 lemma star_cases: |
90 |
110 shows "A\<star> = {[]} \<union> A ;; A\<star>" |
91 fun |
111 unfolding Seq_def |
92 pow :: "string set \<Rightarrow> nat \<Rightarrow> string set" ("_ \<up> _" [101, 102] 101) |
112 by (auto) (metis Star.simps) |
93 where |
113 |
94 "A \<up> 0 = {[]}" |
114 lemma Star_in_Pow: |
95 | "A \<up> (Suc n) = A ;; (A \<up> n)" |
115 assumes a: "s \<in> A\<star>" |
96 |
116 shows "\<exists>n. s \<in> A \<up> n" |
97 |
117 using a |
98 lemma pow_empty [simp]: |
118 apply(induct) |
99 shows "[] \<in> A \<up> n \<longleftrightarrow> (n = 0 \<or> [] \<in> A)" |
119 apply(auto) |
100 by (induct n) (auto) |
120 apply(rule_tac x="Suc n" in exI) |
|
121 apply(auto simp add: Seq_def) |
|
122 done |
|
123 |
|
124 lemma Pow_in_Star: |
|
125 assumes a: "s \<in> A \<up> n" |
|
126 shows "s \<in> A\<star>" |
|
127 using a |
|
128 by (induct n arbitrary: s) (auto simp add: Seq_def) |
|
129 |
|
130 |
|
131 lemma Star_def2: |
|
132 shows "A\<star> = (\<Union>n. A \<up> n)" |
|
133 using Star_in_Pow Pow_in_Star |
|
134 by (auto) |
|
135 |
101 |
136 |
102 |
137 |
103 section {* Semantics of Regular Expressions *} |
138 section {* Semantics of Regular Expressions *} |
104 |
139 |
105 fun |
140 fun |
263 shows "matcher r s \<longleftrightarrow> s \<in> L r" |
298 shows "matcher r s \<longleftrightarrow> s \<in> L r" |
264 by (induct s arbitrary: r) |
299 by (induct s arbitrary: r) |
265 (simp_all add: nullable_correctness der_correctness Der_def) |
300 (simp_all add: nullable_correctness der_correctness Der_def) |
266 |
301 |
267 |
302 |
|
303 |
|
304 |
|
305 lemma bb: "A \<up> n ;; A\<star> \<subseteq> A\<star>" |
|
306 apply(induct n) |
|
307 apply(simp) |
|
308 apply(simp) |
|
309 apply(subst aa[symmetric]) |
|
310 apply(subst Seq_def) |
|
311 apply(auto) |
|
312 done |
|
313 |
|
314 lemma cc: "(\<Union>i\<in>{..n}. A \<up> i) ;; A\<star> \<subseteq> A\<star>" |
|
315 apply(induct n) |
|
316 apply(simp) |
|
317 apply(simp add: Suc_Union del: pow.simps) |
|
318 apply(simp only: seq_union) |
|
319 apply(rule Un_least) |
|
320 defer |
|
321 apply(simp) |
|
322 apply(rule bb) |
|
323 done |
|
324 |
|
325 lemma "A\<star> ;; A\<star> = A\<star>" |
|
326 apply(simp add: Seq_def) |
|
327 apply(rule subset_antisym) |
|
328 defer |
|
329 apply(auto)[1] |
|
330 apply(auto simp add: Star_def2) |
|
331 |
|
332 apply(subst (asm) Star_def2) |
|
333 apply(subst (asm) Star_def2) |
|
334 apply(auto) |
|
335 |
|
336 |
|
337 |
268 end |
338 end |