|
1 (* Author: Christian Urban, Xingyuan Zhang, Chunhan Wu *) |
|
2 theory More_Regular_Set |
|
3 imports "Regular_Exp" "Folds" |
|
4 begin |
|
5 |
|
6 text {* Some properties of operator @{text "@@"}. *} |
|
7 |
|
8 notation |
|
9 conc (infixr "\<cdot>" 100) and |
|
10 star ("_\<star>" [101] 102) |
|
11 |
|
12 lemma star_decom: |
|
13 assumes a: "x \<in> A\<star>" "x \<noteq> []" |
|
14 shows "\<exists>a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> A\<star>" |
|
15 using a |
|
16 by (induct rule: star_induct) (blast)+ |
|
17 |
|
18 lemma conc_pow_comm: |
|
19 shows "A \<cdot> (A ^^ n) = (A ^^ n) \<cdot> A" |
|
20 by (induct n) (simp_all add: conc_assoc[symmetric]) |
|
21 |
|
22 lemma conc_star_comm: |
|
23 shows "A \<cdot> A\<star> = A\<star> \<cdot> A" |
|
24 unfolding star_def conc_pow_comm conc_UNION_distrib |
|
25 by simp |
|
26 |
|
27 |
|
28 text {* Two lemmas about the length of strings in @{text "A \<up> n"} *} |
|
29 |
|
30 lemma pow_length: |
|
31 assumes a: "[] \<notin> A" |
|
32 and b: "s \<in> A ^^ Suc n" |
|
33 shows "n < length s" |
|
34 using b |
|
35 proof (induct n arbitrary: s) |
|
36 case 0 |
|
37 have "s \<in> A ^^ Suc 0" by fact |
|
38 with a have "s \<noteq> []" by auto |
|
39 then show "0 < length s" by auto |
|
40 next |
|
41 case (Suc n) |
|
42 have ih: "\<And>s. s \<in> A ^^ Suc n \<Longrightarrow> n < length s" by fact |
|
43 have "s \<in> A ^^ Suc (Suc n)" by fact |
|
44 then obtain s1 s2 where eq: "s = s1 @ s2" and *: "s1 \<in> A" and **: "s2 \<in> A ^^ Suc n" |
|
45 by (auto simp add: conc_def) |
|
46 from ih ** have "n < length s2" by simp |
|
47 moreover have "0 < length s1" using * a by auto |
|
48 ultimately show "Suc n < length s" unfolding eq |
|
49 by (simp only: length_append) |
|
50 qed |
|
51 |
|
52 lemma conc_pow_length: |
|
53 assumes a: "[] \<notin> A" |
|
54 and b: "s \<in> B \<cdot> (A ^^ Suc n)" |
|
55 shows "n < length s" |
|
56 proof - |
|
57 from b obtain s1 s2 where eq: "s = s1 @ s2" and *: "s2 \<in> A ^^ Suc n" |
|
58 by auto |
|
59 from * have " n < length s2" by (rule pow_length[OF a]) |
|
60 then show "n < length s" using eq by simp |
|
61 qed |
|
62 |
|
63 |
|
64 section {* A modified version of Arden's lemma *} |
|
65 |
|
66 text {* A helper lemma for Arden *} |
|
67 |
|
68 lemma arden_helper: |
|
69 assumes eq: "X = X \<cdot> A \<union> B" |
|
70 shows "X = X \<cdot> (A ^^ Suc n) \<union> (\<Union>m\<in>{0..n}. B \<cdot> (A ^^ m))" |
|
71 proof (induct n) |
|
72 case 0 |
|
73 show "X = X \<cdot> (A ^^ Suc 0) \<union> (\<Union>(m::nat)\<in>{0..0}. B \<cdot> (A ^^ m))" |
|
74 using eq by simp |
|
75 next |
|
76 case (Suc n) |
|
77 have ih: "X = X \<cdot> (A ^^ Suc n) \<union> (\<Union>m\<in>{0..n}. B \<cdot> (A ^^ m))" by fact |
|
78 also have "\<dots> = (X \<cdot> A \<union> B) \<cdot> (A ^^ Suc n) \<union> (\<Union>m\<in>{0..n}. B \<cdot> (A ^^ m))" using eq by simp |
|
79 also have "\<dots> = X \<cdot> (A ^^ Suc (Suc n)) \<union> (B \<cdot> (A ^^ Suc n)) \<union> (\<Union>m\<in>{0..n}. B \<cdot> (A ^^ m))" |
|
80 by (simp add: conc_Un_distrib conc_assoc) |
|
81 also have "\<dots> = X \<cdot> (A ^^ Suc (Suc n)) \<union> (\<Union>m\<in>{0..Suc n}. B \<cdot> (A ^^ m))" |
|
82 by (auto simp add: le_Suc_eq) |
|
83 finally show "X = X \<cdot> (A ^^ Suc (Suc n)) \<union> (\<Union>m\<in>{0..Suc n}. B \<cdot> (A ^^ m))" . |
|
84 qed |
|
85 |
|
86 theorem arden: |
|
87 assumes nemp: "[] \<notin> A" |
|
88 shows "X = X \<cdot> A \<union> B \<longleftrightarrow> X = B \<cdot> A\<star>" |
|
89 proof |
|
90 assume eq: "X = B \<cdot> A\<star>" |
|
91 have "A\<star> = {[]} \<union> A\<star> \<cdot> A" |
|
92 unfolding conc_star_comm[symmetric] |
|
93 by(metis Un_commute star_unfold_left) |
|
94 then have "B \<cdot> A\<star> = B \<cdot> ({[]} \<union> A\<star> \<cdot> A)" |
|
95 by metis |
|
96 also have "\<dots> = B \<union> B \<cdot> (A\<star> \<cdot> A)" |
|
97 unfolding conc_Un_distrib by simp |
|
98 also have "\<dots> = B \<union> (B \<cdot> A\<star>) \<cdot> A" |
|
99 by (simp only: conc_assoc) |
|
100 finally show "X = X \<cdot> A \<union> B" |
|
101 using eq by blast |
|
102 next |
|
103 assume eq: "X = X \<cdot> A \<union> B" |
|
104 { fix n::nat |
|
105 have "B \<cdot> (A ^^ n) \<subseteq> X" using arden_helper[OF eq, of "n"] by auto } |
|
106 then have "B \<cdot> A\<star> \<subseteq> X" |
|
107 unfolding conc_def star_def UNION_def by auto |
|
108 moreover |
|
109 { fix s::"'a list" |
|
110 obtain k where "k = length s" by auto |
|
111 then have not_in: "s \<notin> X \<cdot> (A ^^ Suc k)" |
|
112 using conc_pow_length[OF nemp] by blast |
|
113 assume "s \<in> X" |
|
114 then have "s \<in> X \<cdot> (A ^^ Suc k) \<union> (\<Union>m\<in>{0..k}. B \<cdot> (A ^^ m))" |
|
115 using arden_helper[OF eq, of "k"] by auto |
|
116 then have "s \<in> (\<Union>m\<in>{0..k}. B \<cdot> (A ^^ m))" using not_in by auto |
|
117 moreover |
|
118 have "(\<Union>m\<in>{0..k}. B \<cdot> (A ^^ m)) \<subseteq> (\<Union>n. B \<cdot> (A ^^ n))" by auto |
|
119 ultimately |
|
120 have "s \<in> B \<cdot> A\<star>" |
|
121 unfolding conc_Un_distrib star_def by auto } |
|
122 then have "X \<subseteq> B \<cdot> A\<star>" by auto |
|
123 ultimately |
|
124 show "X = B \<cdot> A\<star>" by simp |
|
125 qed |
|
126 |
|
127 |
|
128 text {* Plus-combination for a set of regular expressions *} |
|
129 |
|
130 abbreviation |
|
131 Setalt ("\<Uplus>_" [1000] 999) |
|
132 where |
|
133 "\<Uplus>A \<equiv> folds Plus Zero A" |
|
134 |
|
135 text {* |
|
136 For finite sets, @{term Setalt} is preserved under @{term lang}. |
|
137 *} |
|
138 |
|
139 lemma folds_alt_simp [simp]: |
|
140 fixes rs::"('a rexp) set" |
|
141 assumes a: "finite rs" |
|
142 shows "lang (\<Uplus>rs) = \<Union> (lang ` rs)" |
|
143 unfolding folds_def |
|
144 apply(rule set_eqI) |
|
145 apply(rule someI2_ex) |
|
146 apply(rule_tac finite_imp_fold_graph[OF a]) |
|
147 apply(erule fold_graph.induct) |
|
148 apply(auto) |
|
149 done |
|
150 |
|
151 end |