22
+ − 1
theory My
24
+ − 2
imports Main Infinite_Set
22
+ − 3
begin
+ − 4
+ − 5
+ − 6
definition
24
+ − 7
Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
22
+ − 8
where
24
+ − 9
"L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"
22
+ − 10
+ − 11
inductive_set
+ − 12
Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
+ − 13
for L :: "string set"
+ − 14
where
+ − 15
start[intro]: "[] \<in> L\<star>"
+ − 16
| step[intro]: "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1@s2 \<in> L\<star>"
+ − 17
24
+ − 18
lemma lang_star_cases:
+ − 19
shows "L\<star> = {[]} \<union> L ;; L\<star>"
+ − 20
unfolding Seq_def
+ − 21
by (auto) (metis Star.simps)
+ − 22
+ − 23
lemma lang_star_cases2:
+ − 24
shows "L ;; L\<star> = L\<star> ;; L"
+ − 25
sorry
+ − 26
+ − 27
+ − 28
theorem ardens_revised:
+ − 29
assumes nemp: "[] \<notin> A"
+ − 30
shows "(X = X ;; A \<union> B) \<longleftrightarrow> (X = B ;; A\<star>)"
+ − 31
proof
+ − 32
assume eq: "X = B ;; A\<star>"
+ − 33
have "A\<star> = {[]} \<union> A\<star> ;; A" sorry
+ − 34
then have "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)" unfolding Seq_def by simp
+ − 35
also have "\<dots> = B \<union> B ;; (A\<star> ;; A)" unfolding Seq_def by auto
+ − 36
also have "\<dots> = B \<union> (B ;; A\<star>) ;; A" unfolding Seq_def
+ − 37
by (auto) (metis append_assoc)+
+ − 38
finally show "X = X ;; A \<union> B" using eq by auto
+ − 39
next
+ − 40
assume "X = X ;; A \<union> B"
+ − 41
then have "B \<subseteq> X" "X ;; A \<subseteq> X" by auto
+ − 42
show "X = B ;; A\<star>" sorry
+ − 43
qed
22
+ − 44
+ − 45
datatype rexp =
+ − 46
NULL
+ − 47
| EMPTY
+ − 48
| CHAR char
+ − 49
| SEQ rexp rexp
+ − 50
| ALT rexp rexp
+ − 51
| STAR rexp
+ − 52
+ − 53
fun
24
+ − 54
Sem :: "rexp \<Rightarrow> string set" ("\<lparr>_\<rparr>" [0] 1000)
22
+ − 55
where
24
+ − 56
"\<lparr>NULL\<rparr> = {}"
+ − 57
| "\<lparr>EMPTY\<rparr> = {[]}"
+ − 58
| "\<lparr>CHAR c\<rparr> = {[c]}"
+ − 59
| "\<lparr>SEQ r1 r2\<rparr> = \<lparr>r1\<rparr> ;; \<lparr>r2\<rparr>"
+ − 60
| "\<lparr>ALT r1 r2\<rparr> = \<lparr>r1\<rparr> \<union> \<lparr>r2\<rparr>"
+ − 61
| "\<lparr>STAR r\<rparr> = \<lparr>r\<rparr>\<star>"
22
+ − 62
+ − 63
definition
+ − 64
folds :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"
+ − 65
where
+ − 66
"folds f z S \<equiv> SOME x. fold_graph f z S x"
+ − 67
+ − 68
lemma folds_simp_null [simp]:
24
+ − 69
"finite rs \<Longrightarrow> x \<in> \<lparr>folds ALT NULL rs\<rparr> \<longleftrightarrow> (\<exists>r \<in> rs. x \<in> \<lparr>r\<rparr>)"
22
+ − 70
apply (simp add: folds_def)
+ − 71
apply (rule someI2_ex)
+ − 72
apply (erule finite_imp_fold_graph)
+ − 73
apply (erule fold_graph.induct)
+ − 74
apply (auto)
+ − 75
done
+ − 76
+ − 77
lemma folds_simp_empty [simp]:
24
+ − 78
"finite rs \<Longrightarrow> x \<in> \<lparr>folds ALT EMPTY rs\<rparr> \<longleftrightarrow> (\<exists>r \<in> rs. x \<in> \<lparr>r\<rparr>) \<or> x = []"
22
+ − 79
apply (simp add: folds_def)
+ − 80
apply (rule someI2_ex)
+ − 81
apply (erule finite_imp_fold_graph)
+ − 82
apply (erule fold_graph.induct)
+ − 83
apply (auto)
+ − 84
done
+ − 85
+ − 86
lemma [simp]:
24
+ − 87
shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
22
+ − 88
by simp
+ − 89
+ − 90
definition
+ − 91
str_eq ("_ \<approx>_ _")
+ − 92
where
+ − 93
"x \<approx>Lang y \<equiv> (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)"
+ − 94
+ − 95
definition
+ − 96
str_eq_rel ("\<approx>_")
+ − 97
where
+ − 98
"\<approx>Lang \<equiv> {(x, y). x \<approx>Lang y}"
+ − 99
+ − 100
definition
+ − 101
final :: "string set \<Rightarrow> string set \<Rightarrow> bool"
+ − 102
where
+ − 103
"final X Lang \<equiv> (X \<in> UNIV // \<approx>Lang) \<and> (\<forall>s \<in> X. s \<in> Lang)"
+ − 104
+ − 105
lemma lang_is_union_of_finals:
+ − 106
"Lang = \<Union> {X. final X Lang}"
+ − 107
proof -
+ − 108
have "Lang \<subseteq> \<Union> {X. final X Lang}"
+ − 109
unfolding final_def
+ − 110
unfolding quotient_def Image_def
+ − 111
unfolding str_eq_rel_def
+ − 112
apply(simp)
+ − 113
apply(auto)
+ − 114
apply(rule_tac x="(\<approx>Lang) `` {x}" in exI)
+ − 115
unfolding Image_def
+ − 116
unfolding str_eq_rel_def
+ − 117
apply(auto)
+ − 118
unfolding str_eq_def
+ − 119
apply(auto)
+ − 120
apply(drule_tac x="[]" in spec)
+ − 121
apply(simp)
+ − 122
done
+ − 123
moreover
+ − 124
have "\<Union>{X. final X Lang} \<subseteq> Lang"
+ − 125
unfolding final_def by auto
+ − 126
ultimately
+ − 127
show "Lang = \<Union> {X. final X Lang}"
+ − 128
by blast
+ − 129
qed
+ − 130
+ − 131
lemma all_rexp:
24
+ − 132
"\<lbrakk>finite (UNIV // \<approx>Lang); X \<in> (UNIV // \<approx>Lang)\<rbrakk> \<Longrightarrow> \<exists>r. X = \<lparr>r\<rparr>"
22
+ − 133
sorry
+ − 134
+ − 135
lemma final_rexp:
24
+ − 136
"\<lbrakk>finite (UNIV // (\<approx>Lang)); final X Lang\<rbrakk> \<Longrightarrow> \<exists>r. X = \<lparr>r\<rparr>"
22
+ − 137
unfolding final_def
+ − 138
using all_rexp by blast
+ − 139
+ − 140
lemma finite_f_one_to_one:
+ − 141
assumes "finite B"
+ − 142
and "\<forall>x \<in> B. \<exists>y. f y = x"
+ − 143
shows "\<exists>rs. finite rs \<and> (B = {f y | y . y \<in> rs})"
+ − 144
using assms
+ − 145
by (induct) (auto)
+ − 146
+ − 147
lemma finite_final:
+ − 148
assumes "finite (UNIV // (\<approx>Lang))"
+ − 149
shows "finite {X. final X Lang}"
+ − 150
using assms
+ − 151
proof -
+ − 152
have "{X. final X Lang} \<subseteq> (UNIV // (\<approx>Lang))"
+ − 153
unfolding final_def by auto
+ − 154
with assms show "finite {X. final X Lang}"
+ − 155
using finite_subset by auto
+ − 156
qed
+ − 157
+ − 158
lemma finite_regular_aux:
+ − 159
fixes Lang :: "string set"
+ − 160
assumes "finite (UNIV // (\<approx>Lang))"
24
+ − 161
shows "\<exists>rs. Lang = \<lparr>folds ALT NULL rs\<rparr>"
22
+ − 162
apply(subst lang_is_union_of_finals)
+ − 163
using assms
+ − 164
apply -
+ − 165
apply(drule finite_final)
24
+ − 166
apply(drule_tac f="Sem" in finite_f_one_to_one)
22
+ − 167
apply(clarify)
+ − 168
apply(drule final_rexp[OF assms])
+ − 169
apply(auto)[1]
+ − 170
apply(clarify)
+ − 171
apply(rule_tac x="rs" in exI)
+ − 172
apply(simp)
+ − 173
apply(rule set_eqI)
+ − 174
apply(auto)
+ − 175
done
+ − 176
+ − 177
lemma finite_regular:
+ − 178
fixes Lang :: "string set"
+ − 179
assumes "finite (UNIV // (\<approx>Lang))"
24
+ − 180
shows "\<exists>r. Lang = \<lparr>r\<rparr>"
22
+ − 181
using assms finite_regular_aux
+ − 182
by auto
+ − 183
+ − 184
+ − 185
+ − 186
section {* other direction *}
+ − 187
+ − 188
+ − 189
lemma inj_image_lang:
+ − 190
fixes f::"string \<Rightarrow> 'a"
+ − 191
assumes str_inj: "\<And>x y. f x = f y \<Longrightarrow> x \<approx>Lang y"
+ − 192
shows "inj_on (image f) (UNIV // (\<approx>Lang))"
+ − 193
proof -
+ − 194
{ fix x y::string
+ − 195
assume eq_tag: "f ` {z. x \<approx>Lang z} = f ` {z. y \<approx>Lang z}"
+ − 196
moreover
+ − 197
have "{z. x \<approx>Lang z} \<noteq> {}" unfolding str_eq_def by auto
+ − 198
ultimately obtain a b where "x \<approx>Lang a" "y \<approx>Lang b" "f a = f b" by blast
+ − 199
then have "x \<approx>Lang a" "y \<approx>Lang b" "a \<approx>Lang b" using str_inj by auto
+ − 200
then have "x \<approx>Lang y" unfolding str_eq_def by simp
+ − 201
then have "{z. x \<approx>Lang z} = {z. y \<approx>Lang z}" unfolding str_eq_def by simp
+ − 202
}
+ − 203
then have "\<forall>x\<in>UNIV // \<approx>Lang. \<forall>y\<in>UNIV // \<approx>Lang. f ` x = f ` y \<longrightarrow> x = y"
+ − 204
unfolding quotient_def Image_def str_eq_rel_def by simp
+ − 205
then show "inj_on (image f) (UNIV // (\<approx>Lang))"
+ − 206
unfolding inj_on_def by simp
+ − 207
qed
+ − 208
+ − 209
+ − 210
lemma finite_range_image:
+ − 211
assumes fin: "finite (range f)"
+ − 212
shows "finite ((image f) ` X)"
+ − 213
proof -
+ − 214
from fin have "finite (Pow (f ` UNIV))" by auto
+ − 215
moreover
+ − 216
have "(image f) ` X \<subseteq> Pow (f ` UNIV)" by auto
+ − 217
ultimately show "finite ((image f) ` X)" using finite_subset by auto
+ − 218
qed
+ − 219
+ − 220
definition
+ − 221
tag1 :: "string set \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> (string set \<times> string set)"
+ − 222
where
+ − 223
"tag1 L\<^isub>1 L\<^isub>2 \<equiv> \<lambda>x. ((\<approx>L\<^isub>1) `` {x}, (\<approx>L\<^isub>2) `` {x})"
+ − 224
+ − 225
lemma tag1_range_finite:
+ − 226
assumes finite1: "finite (UNIV // \<approx>L\<^isub>1)"
+ − 227
and finite2: "finite (UNIV // \<approx>L\<^isub>2)"
+ − 228
shows "finite (range (tag1 L\<^isub>1 L\<^isub>2))"
+ − 229
proof -
+ − 230
have "finite (UNIV // \<approx>L\<^isub>1 \<times> UNIV // \<approx>L\<^isub>2)" using finite1 finite2 by auto
+ − 231
moreover
+ − 232
have "range (tag1 L\<^isub>1 L\<^isub>2) \<subseteq> (UNIV // \<approx>L\<^isub>1) \<times> (UNIV // \<approx>L\<^isub>2)"
+ − 233
unfolding tag1_def quotient_def by auto
+ − 234
ultimately show "finite (range (tag1 L\<^isub>1 L\<^isub>2))"
+ − 235
using finite_subset by blast
+ − 236
qed
+ − 237
+ − 238
lemma tag1_inj:
+ − 239
"tag1 L\<^isub>1 L\<^isub>2 x = tag1 L\<^isub>1 L\<^isub>2 y \<Longrightarrow> x \<approx>(L\<^isub>1 \<union> L\<^isub>2) y"
+ − 240
unfolding tag1_def Image_def str_eq_rel_def str_eq_def
+ − 241
by auto
+ − 242
+ − 243
lemma quot_alt_cu:
+ − 244
fixes L\<^isub>1 L\<^isub>2::"string set"
+ − 245
assumes fin1: "finite (UNIV // \<approx>L\<^isub>1)"
+ − 246
and fin2: "finite (UNIV // \<approx>L\<^isub>2)"
+ − 247
shows "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))"
+ − 248
proof -
+ − 249
have "finite (range (tag1 L\<^isub>1 L\<^isub>2))"
+ − 250
using fin1 fin2 tag1_range_finite by simp
+ − 251
then have "finite (image (tag1 L\<^isub>1 L\<^isub>2) ` (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2)))"
+ − 252
using finite_range_image by blast
+ − 253
moreover
+ − 254
have "\<And>x y. tag1 L\<^isub>1 L\<^isub>2 x = tag1 L\<^isub>1 L\<^isub>2 y \<Longrightarrow> x \<approx>(L\<^isub>1 \<union> L\<^isub>2) y"
+ − 255
using tag1_inj by simp
+ − 256
then have "inj_on (image (tag1 L\<^isub>1 L\<^isub>2)) (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))"
+ − 257
using inj_image_lang by blast
+ − 258
ultimately
+ − 259
show "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))" by (rule finite_imageD)
+ − 260
qed
+ − 261
+ − 262
+ − 263
section {* finite \<Rightarrow> regular *}
+ − 264
+ − 265
definition
+ − 266
transitions :: "string set \<Rightarrow> string set \<Rightarrow> rexp set" ("_\<Turnstile>\<Rightarrow>_")
+ − 267
where
24
+ − 268
"Y \<Turnstile>\<Rightarrow> X \<equiv> {CHAR c | c. Y ;; {[c]} \<subseteq> X}"
22
+ − 269
+ − 270
definition
+ − 271
transitions_rexp ("_ \<turnstile>\<rightarrow> _")
+ − 272
where
+ − 273
"Y \<turnstile>\<rightarrow> X \<equiv> if [] \<in> X then folds ALT EMPTY (Y \<Turnstile>\<Rightarrow>X) else folds ALT NULL (Y \<Turnstile>\<Rightarrow>X)"
+ − 274
+ − 275
definition
+ − 276
"rhs CS X \<equiv> if X = {[]} then {({[]}, EMPTY)} else {(Y, Y \<turnstile>\<rightarrow>X) | Y. Y \<in> CS}"
+ − 277
+ − 278
definition
24
+ − 279
"rhs_sem CS X \<equiv> \<Union> {(Y;; \<lparr>r\<rparr>) | Y r . (Y, r) \<in> rhs CS X}"
22
+ − 280
+ − 281
definition
+ − 282
"eqs CS \<equiv> (\<Union>X \<in> CS. {(X, rhs CS X)})"
+ − 283
+ − 284
definition
+ − 285
"eqs_sem CS \<equiv> (\<Union>X \<in> CS. {(X, rhs_sem CS X)})"
+ − 286
+ − 287
lemma [simp]:
+ − 288
shows "finite (Y \<Turnstile>\<Rightarrow> X)"
+ − 289
unfolding transitions_def
+ − 290
by auto
+ − 291
+ − 292
+ − 293
lemma defined_by_str:
+ − 294
assumes "s \<in> X"
+ − 295
and "X \<in> UNIV // (\<approx>Lang)"
+ − 296
shows "X = (\<approx>Lang) `` {s}"
+ − 297
using assms
+ − 298
unfolding quotient_def Image_def
+ − 299
unfolding str_eq_rel_def str_eq_def
+ − 300
by auto
+ − 301
+ − 302
lemma every_eqclass_has_transition:
+ − 303
assumes has_str: "s @ [c] \<in> X"
+ − 304
and in_CS: "X \<in> UNIV // (\<approx>Lang)"
24
+ − 305
obtains Y where "Y \<in> UNIV // (\<approx>Lang)" and "Y ;; {[c]} \<subseteq> X" and "s \<in> Y"
22
+ − 306
proof -
+ − 307
def Y \<equiv> "(\<approx>Lang) `` {s}"
+ − 308
have "Y \<in> UNIV // (\<approx>Lang)"
+ − 309
unfolding Y_def quotient_def by auto
+ − 310
moreover
+ − 311
have "X = (\<approx>Lang) `` {s @ [c]}"
+ − 312
using has_str in_CS defined_by_str by blast
24
+ − 313
then have "Y ;; {[c]} \<subseteq> X"
+ − 314
unfolding Y_def Image_def Seq_def
22
+ − 315
unfolding str_eq_rel_def
+ − 316
by (auto) (simp add: str_eq_def)
+ − 317
moreover
+ − 318
have "s \<in> Y" unfolding Y_def
+ − 319
unfolding Image_def str_eq_rel_def str_eq_def by simp
24
+ − 320
(*moreover
+ − 321
have "True" by simp FIXME *)
+ − 322
ultimately show thesis by (blast intro: that)
22
+ − 323
qed
+ − 324
+ − 325
lemma test:
+ − 326
assumes "[] \<in> X"
24
+ − 327
shows "[] \<in> \<lparr>Y \<turnstile>\<rightarrow> X\<rparr>"
22
+ − 328
using assms
+ − 329
by (simp add: transitions_rexp_def)
+ − 330
+ − 331
lemma rhs_sem:
+ − 332
assumes "X \<in> (UNIV // (\<approx>Lang))"
+ − 333
shows "X \<subseteq> rhs_sem (UNIV // (\<approx>Lang)) X"
+ − 334
apply(case_tac "X = {[]}")
+ − 335
apply(simp)
24
+ − 336
apply(simp add: rhs_sem_def rhs_def Seq_def)
22
+ − 337
apply(rule subsetI)
+ − 338
apply(case_tac "x = []")
+ − 339
apply(simp add: rhs_sem_def rhs_def)
+ − 340
apply(rule_tac x = "X" in exI)
+ − 341
apply(simp)
+ − 342
apply(rule_tac x = "X" in exI)
+ − 343
apply(simp add: assms)
+ − 344
apply(simp add: transitions_rexp_def)
24
+ − 345
oops
+ − 346
+ − 347
+ − 348
(*
+ − 349
fun
+ − 350
power :: "string \<Rightarrow> nat \<Rightarrow> string" (infixr "\<Up>" 100)
+ − 351
where
+ − 352
"s \<Up> 0 = s"
+ − 353
| "s \<Up> (Suc n) = s @ (s \<Up> n)"
+ − 354
+ − 355
definition
+ − 356
"Lone = {(''0'' \<Up> n) @ (''1'' \<Up> n) | n. True }"
+ − 357
+ − 358
lemma
+ − 359
"infinite (UNIV // (\<approx>Lone))"
+ − 360
unfolding infinite_iff_countable_subset
+ − 361
apply(rule_tac x="\<lambda>n. {(''0'' \<Up> n) @ (''1'' \<Up> i) | i. i \<in> {..n} }" in exI)
+ − 362
apply(auto)
+ − 363
prefer 2
+ − 364
unfolding Lone_def
+ − 365
unfolding quotient_def
+ − 366
unfolding Image_def
+ − 367
apply(simp)
+ − 368
unfolding str_eq_rel_def
+ − 369
unfolding str_eq_def
+ − 370
apply(auto)
+ − 371
apply(rule_tac x="''0'' \<Up> n" in exI)
+ − 372
apply(auto)
+ − 373
unfolding infinite_nat_iff_unbounded
+ − 374
unfolding Lone_def
+ − 375
*)
+ − 376
+ − 377
+ − 378
+ − 379
text {* Derivatives *}
+ − 380
+ − 381
definition
+ − 382
DERS :: "string \<Rightarrow> string set \<Rightarrow> string set"
+ − 383
where
+ − 384
"DERS s L \<equiv> {s'. s @ s' \<in> L}"
+ − 385
+ − 386
lemma
+ − 387
shows "x \<approx>L y \<longleftrightarrow> DERS x L = DERS y L"
+ − 388
unfolding DERS_def str_eq_def
+ − 389
by auto