|
444
|
1 |
theory GeneralRegexBound imports
|
|
|
2 |
"BasicIdentities"
|
|
|
3 |
begin
|
|
|
4 |
|
|
|
5 |
|
|
|
6 |
lemma non_zero_size:
|
|
|
7 |
shows "rsize r \<ge> Suc 0"
|
|
|
8 |
apply(induct r)
|
|
|
9 |
apply auto done
|
|
|
10 |
|
|
|
11 |
corollary size_geq1:
|
|
|
12 |
shows "rsize r \<ge> 1"
|
|
|
13 |
by (simp add: non_zero_size)
|
|
|
14 |
|
|
|
15 |
|
|
|
16 |
definition SEQ_set where
|
|
|
17 |
"SEQ_set A n \<equiv> {RSEQ r1 r2 | r1 r2. r1 \<in> A \<and> r2 \<in> A \<and> rsize r1 + rsize r2 \<le> n}"
|
|
|
18 |
|
|
|
19 |
definition SEQ_set_cartesian where
|
|
|
20 |
"SEQ_set_cartesian A n = {RSEQ r1 r2 | r1 r2. r1 \<in> A \<and> r2 \<in> A}"
|
|
|
21 |
|
|
|
22 |
definition ALT_set where
|
|
|
23 |
"ALT_set A n \<equiv> {RALTS rs | rs. set rs \<subseteq> A \<and> sum_list (map rsize rs) \<le> n}"
|
|
|
24 |
|
|
|
25 |
|
|
|
26 |
definition
|
|
|
27 |
"sizeNregex N \<equiv> {r. rsize r \<le> N}"
|
|
|
28 |
|
|
|
29 |
lemma sizenregex_induct:
|
|
|
30 |
shows "sizeNregex (Suc n) = sizeNregex n \<union> {RZERO, RONE, RALTS []} \<union> {RCHAR c| c. True} \<union>
|
|
|
31 |
SEQ_set ( sizeNregex n) n \<union> ALT_set (sizeNregex n) n \<union> (RSTAR ` (sizeNregex n))"
|
|
|
32 |
sorry
|
|
|
33 |
|
|
|
34 |
|
|
|
35 |
lemma chars_finite:
|
|
|
36 |
shows "finite (RCHAR ` (UNIV::(char set)))"
|
|
|
37 |
apply(simp)
|
|
|
38 |
done
|
|
|
39 |
|
|
|
40 |
thm full_SetCompr_eq
|
|
|
41 |
|
|
|
42 |
lemma size1finite:
|
|
|
43 |
shows "finite (sizeNregex (Suc 0))"
|
|
|
44 |
apply(subst sizenregex_induct)
|
|
|
45 |
apply(subst finite_Un)+
|
|
|
46 |
apply(subgoal_tac "sizeNregex 0 = {}")
|
|
|
47 |
apply(rule conjI)+
|
|
|
48 |
apply (metis Collect_empty_eq finite.emptyI non_zero_size not_less_eq_eq sizeNregex_def)
|
|
|
49 |
apply simp
|
|
|
50 |
apply (simp add: full_SetCompr_eq)
|
|
|
51 |
apply (simp add: SEQ_set_def)
|
|
|
52 |
apply (simp add: ALT_set_def)
|
|
|
53 |
apply(simp add: full_SetCompr_eq)
|
|
|
54 |
using non_zero_size not_less_eq_eq sizeNregex_def by fastforce
|
|
|
55 |
|
|
|
56 |
lemma seq_included_in_cart:
|
|
|
57 |
shows "SEQ_set A n \<subseteq> SEQ_set_cartesian A n"
|
|
|
58 |
using SEQ_set_cartesian_def SEQ_set_def by fastforce
|
|
|
59 |
|
|
|
60 |
lemma finite_seq:
|
|
|
61 |
shows " finite (sizeNregex n) \<Longrightarrow> finite (SEQ_set (sizeNregex n) n)"
|
|
|
62 |
apply(rule finite_subset)
|
|
|
63 |
sorry
|
|
|
64 |
|
|
|
65 |
|
|
|
66 |
lemma finite_size_n:
|
|
|
67 |
shows "finite (sizeNregex n)"
|
|
|
68 |
apply(induct n)
|
|
|
69 |
apply (metis Collect_empty_eq finite.emptyI non_zero_size not_less_eq_eq sizeNregex_def)
|
|
|
70 |
apply(subst sizenregex_induct)
|
|
|
71 |
apply(subst finite_Un)+
|
|
|
72 |
apply(rule conjI)+
|
|
|
73 |
apply simp
|
|
|
74 |
apply simp
|
|
|
75 |
apply (simp add: full_SetCompr_eq)
|
|
|
76 |
|
|
|
77 |
sorry
|
|
|
78 |
|
|
|
79 |
lemma three_easy_cases0: shows
|
|
|
80 |
"rsize (rders_simp RZERO s) \<le> Suc 0"
|
|
|
81 |
sorry
|
|
|
82 |
|
|
|
83 |
|
|
|
84 |
lemma three_easy_cases1: shows
|
|
|
85 |
"rsize (rders_simp RONE s) \<le> Suc 0"
|
|
|
86 |
sorry
|
|
|
87 |
|
|
|
88 |
lemma three_easy_casesC: shows
|
|
|
89 |
"rsize (rders_simp (RCHAR c) s) \<le> Suc 0"
|
|
|
90 |
|
|
|
91 |
sorry
|
|
|
92 |
|
|
|
93 |
|
|
|
94 |
|
|
|
95 |
|
|
|
96 |
end
|
|
|
97 |
|