|
1 theory "RegSet" |
|
2 imports "Main" |
|
3 begin |
|
4 |
|
5 |
|
6 text {* Sequential composition of sets *} |
|
7 |
|
8 definition |
|
9 lang_seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ; _" [100,100] 100) |
|
10 where |
|
11 "L1 ; L2 = {s1@s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}" |
|
12 |
|
13 |
|
14 section {* Kleene star for sets *} |
|
15 |
|
16 inductive_set |
|
17 Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102) |
|
18 for L :: "string set" |
|
19 where |
|
20 start[intro]: "[] \<in> L\<star>" |
|
21 | step[intro]: "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> L\<star>" |
|
22 |
|
23 |
|
24 text {* A standard property of star *} |
|
25 |
|
26 lemma lang_star_cases: |
|
27 shows "L\<star> = {[]} \<union> L ; L\<star>" |
|
28 proof |
|
29 { fix x |
|
30 have "x \<in> L\<star> \<Longrightarrow> x \<in> {[]} \<union> L ; L\<star>" |
|
31 unfolding lang_seq_def |
|
32 by (induct rule: Star.induct) (auto) |
|
33 } |
|
34 then show "L\<star> \<subseteq> {[]} \<union> L ; L\<star>" by auto |
|
35 next |
|
36 show "{[]} \<union> L ; L\<star> \<subseteq> L\<star>" |
|
37 unfolding lang_seq_def by auto |
|
38 qed |
|
39 |
|
40 |
|
41 lemma lang_star_cases2: |
|
42 shows "[] \<notin> L \<Longrightarrow> L\<star> - {[]} = L ; L\<star>" |
|
43 by (subst lang_star_cases) |
|
44 (simp add: lang_seq_def) |
|
45 |
|
46 |
|
47 section {* Regular Expressions *} |
|
48 |
|
49 datatype rexp = |
|
50 NULL |
|
51 | EMPTY |
|
52 | CHAR char |
|
53 | SEQ rexp rexp |
|
54 | ALT rexp rexp |
|
55 | STAR rexp |
|
56 |
|
57 |
|
58 section {* Semantics of Regular Expressions *} |
|
59 |
|
60 fun |
|
61 L :: "rexp \<Rightarrow> string set" |
|
62 where |
|
63 "L (NULL) = {}" |
|
64 | "L (EMPTY) = {[]}" |
|
65 | "L (CHAR c) = {[c]}" |
|
66 | "L (SEQ r1 r2) = (L r1) ; (L r2)" |
|
67 | "L (ALT r1 r2) = (L r1) \<union> (L r2)" |
|
68 | "L (STAR r) = (L r)\<star>" |
|
69 |
|
70 abbreviation |
|
71 CUNIV :: "string set" |
|
72 where |
|
73 "CUNIV \<equiv> (\<lambda>x. [x]) ` (UNIV::char set)" |
|
74 |
|
75 lemma CUNIV_star_minus: |
|
76 "(CUNIV\<star> - {[c]}) = {[]} \<union> (CUNIV - {[c]}; (CUNIV\<star>))" |
|
77 apply(subst lang_star_cases) |
|
78 apply(simp add: lang_seq_def) |
|
79 oops |
|
80 |
|
81 |
|
82 lemma string_in_CUNIV: |
|
83 shows "s \<in> CUNIV\<star>" |
|
84 proof (induct s) |
|
85 case Nil |
|
86 show "[] \<in> CUNIV\<star>" by (rule start) |
|
87 next |
|
88 case (Cons c s) |
|
89 have "[c] \<in> CUNIV" by simp |
|
90 moreover |
|
91 have "s \<in> CUNIV\<star>" by fact |
|
92 ultimately have "[c] @ s \<in> CUNIV\<star>" by (rule step) |
|
93 then show "c # s \<in> CUNIV\<star>" by simp |
|
94 qed |
|
95 |
|
96 lemma UNIV_CUNIV_star: |
|
97 shows "UNIV = CUNIV\<star>" |
|
98 using string_in_CUNIV |
|
99 by (auto) |
|
100 |
|
101 abbreviation |
|
102 reg :: "string set => bool" |
|
103 where |
|
104 "reg L1 \<equiv> (\<exists>r. L r = L1)" |
|
105 |
|
106 lemma reg_null [intro]: |
|
107 shows "reg {}" |
|
108 by (metis L.simps(1)) |
|
109 |
|
110 lemma reg_empty [intro]: |
|
111 shows "reg {[]}" |
|
112 by (metis L.simps(2)) |
|
113 |
|
114 lemma reg_star [intro]: |
|
115 shows "reg L1 \<Longrightarrow> reg (L1\<star>)" |
|
116 by (metis L.simps(6)) |
|
117 |
|
118 lemma reg_seq [intro]: |
|
119 assumes a: "reg L1" "reg L2" |
|
120 shows "reg (L1 ; L2)" |
|
121 using a |
|
122 by (metis L.simps(4)) |
|
123 |
|
124 lemma reg_union [intro]: |
|
125 assumes a: "reg L1" "reg L2" |
|
126 shows "reg (L1 \<union> L2)" |
|
127 using a |
|
128 by (metis L.simps(5)) |
|
129 |
|
130 lemma reg_string [intro]: |
|
131 fixes s::string |
|
132 shows "reg {s}" |
|
133 proof (induct s) |
|
134 case Nil |
|
135 show "reg {[]}" by (rule reg_empty) |
|
136 next |
|
137 case (Cons c s) |
|
138 have "reg {s}" by fact |
|
139 then obtain r where "L r = {s}" by auto |
|
140 then have "L (SEQ (CHAR c) r) = {[c]} ; {s}" by simp |
|
141 also have "\<dots> = {c # s}" by (simp add: lang_seq_def) |
|
142 finally show "reg {c # s}" by blast |
|
143 qed |
|
144 |
|
145 lemma reg_finite [intro]: |
|
146 assumes a: "finite L1" |
|
147 shows "reg L1" |
|
148 using a |
|
149 proof(induct) |
|
150 case empty |
|
151 show "reg {}" by (rule reg_null) |
|
152 next |
|
153 case (insert s S) |
|
154 have "reg {s}" by (rule reg_string) |
|
155 moreover |
|
156 have "reg S" by fact |
|
157 ultimately have "reg ({s} \<union> S)" by (rule reg_union) |
|
158 then show "reg (insert s S)" by simp |
|
159 qed |
|
160 |
|
161 lemma reg_cuniv [intro]: |
|
162 shows "reg (CUNIV)" |
|
163 by (rule reg_finite) (auto) |
|
164 |
|
165 lemma reg_univ: |
|
166 shows "reg (UNIV::string set)" |
|
167 proof - |
|
168 have "reg CUNIV" by (rule reg_cuniv) |
|
169 then have "reg (CUNIV\<star>)" by (rule reg_star) |
|
170 then show "reg UNIV" by (simp add: UNIV_CUNIV_star) |
|
171 qed |
|
172 |
|
173 lemma reg_finite_subset: |
|
174 assumes a: "finite L1" |
|
175 and b: "reg L1" "L2 \<subseteq> L1" |
|
176 shows "reg L2" |
|
177 using a b |
|
178 apply(induct arbitrary: L2) |
|
179 apply(simp add: reg_empty) |
|
180 oops |
|
181 |
|
182 |
|
183 lemma reg_not: |
|
184 shows "reg (UNIV - L r)" |
|
185 proof (induct r) |
|
186 case NULL |
|
187 have "reg UNIV" by (rule reg_univ) |
|
188 then show "reg (UNIV - L NULL)" by simp |
|
189 next |
|
190 case EMPTY |
|
191 have "[] \<notin> CUNIV" by auto |
|
192 moreover |
|
193 have "reg (CUNIV; CUNIV\<star>)" by auto |
|
194 ultimately have "reg (CUNIV\<star> - {[]})" |
|
195 using lang_star_cases2 by simp |
|
196 then show "reg (UNIV - L EMPTY)" by (simp add: UNIV_CUNIV_star) |
|
197 next |
|
198 case (CHAR c) |
|
199 then show "?case" |
|
200 apply(simp) |
|
201 |
|
202 using reg_UNIV |
|
203 apply(simp) |
|
204 apply(simp add: char_star2[symmetric]) |
|
205 apply(rule reg_seq) |
|
206 apply(rule reg_cuniv) |
|
207 apply(rule reg_star) |
|
208 apply(rule reg_cuniv) |
|
209 oops |
|
210 |
|
211 |
|
212 |
|
213 end |
|
214 |
|
215 |
|
216 |
|
217 |
|
218 |
|
219 |
|
220 |
|
221 |
|
222 |
|
223 |