1 |
|
2 theory RegLangs |
1 theory RegLangs |
3 imports Main "~~/src/HOL/Library/Sublist" |
2 imports Main "~~/src/HOL/Library/Sublist" |
4 begin |
3 begin |
5 |
4 |
6 section {* Sequential Composition of Languages *} |
5 section \<open>Sequential Composition of Languages\<close> |
7 |
6 |
8 definition |
7 definition |
9 Sequ :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100) |
8 Sequ :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100) |
10 where |
9 where |
11 "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}" |
10 "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}" |
12 |
11 |
13 text {* Two Simple Properties about Sequential Composition *} |
12 text \<open>Two Simple Properties about Sequential Composition\<close> |
14 |
13 |
15 lemma Sequ_empty_string [simp]: |
14 lemma Sequ_empty_string [simp]: |
16 shows "A ;; {[]} = A" |
15 shows "A ;; {[]} = A" |
17 and "{[]} ;; A = A" |
16 and "{[]} ;; A = A" |
18 by (simp_all add: Sequ_def) |
17 by (simp_all add: Sequ_def) |
20 lemma Sequ_empty [simp]: |
19 lemma Sequ_empty [simp]: |
21 shows "A ;; {} = {}" |
20 shows "A ;; {} = {}" |
22 and "{} ;; A = {}" |
21 and "{} ;; A = {}" |
23 by (simp_all add: Sequ_def) |
22 by (simp_all add: Sequ_def) |
24 |
23 |
25 lemma |
|
26 shows "(A \<union> B) ;; C = (A ;; C) \<union> (B ;; C)" |
|
27 apply(auto simp add: Sequ_def) |
|
28 done |
|
29 |
24 |
30 lemma |
25 section \<open>Semantic Derivative (Left Quotient) of Languages\<close> |
31 shows "(A \<inter> B) ;; C \<subseteq> (A ;; C) \<inter> (B ;; C)" |
|
32 apply(auto simp add: Sequ_def) |
|
33 done |
|
34 |
|
35 lemma |
|
36 shows "(A ;; C) \<inter> (B ;; C) \<subseteq> (A \<inter> B) ;; C" |
|
37 apply(auto simp add: Sequ_def) |
|
38 oops |
|
39 |
|
40 section {* Semantic Derivative (Left Quotient) of Languages *} |
|
41 |
26 |
42 definition |
27 definition |
43 Der :: "char \<Rightarrow> string set \<Rightarrow> string set" |
28 Der :: "char \<Rightarrow> string set \<Rightarrow> string set" |
44 where |
29 where |
45 "Der c A \<equiv> {s. c # s \<in> A}" |
30 "Der c A \<equiv> {s. c # s \<in> A}" |
73 shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})" |
58 shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})" |
74 unfolding Der_def Sequ_def |
59 unfolding Der_def Sequ_def |
75 by (auto simp add: Cons_eq_append_conv) |
60 by (auto simp add: Cons_eq_append_conv) |
76 |
61 |
77 |
62 |
78 section {* Kleene Star for Languages *} |
63 section \<open>Kleene Star for Languages\<close> |
79 |
64 |
80 inductive_set |
65 inductive_set |
81 Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102) |
66 Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102) |
82 for A :: "string set" |
67 for A :: "string set" |
83 where |
68 where |
102 shows "Der c (A\<star>) \<subseteq> (Der c A) ;; A\<star>" |
87 shows "Der c (A\<star>) \<subseteq> (Der c A) ;; A\<star>" |
103 unfolding Der_def Sequ_def |
88 unfolding Der_def Sequ_def |
104 by(auto simp add: Star_decomp) |
89 by(auto simp add: Star_decomp) |
105 |
90 |
106 |
91 |
107 lemma Der_star [simp]: |
92 lemma Der_star[simp]: |
108 shows "Der c (A\<star>) = (Der c A) ;; A\<star>" |
93 shows "Der c (A\<star>) = (Der c A) ;; A\<star>" |
109 proof - |
94 proof - |
110 have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)" |
95 have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)" |
111 by (simp only: Star_cases[symmetric]) |
96 by (simp only: Star_cases[symmetric]) |
112 also have "... = Der c (A ;; A\<star>)" |
97 also have "... = Der c (A ;; A\<star>)" |
132 apply(clarify) |
117 apply(clarify) |
133 by (metis append_Nil concat.simps(2) set_ConsD) |
118 by (metis append_Nil concat.simps(2) set_ConsD) |
134 |
119 |
135 |
120 |
136 |
121 |
137 section {* Regular Expressions *} |
122 section \<open>Regular Expressions\<close> |
138 |
123 |
139 datatype rexp = |
124 datatype rexp = |
140 ZERO |
125 ZERO |
141 | ONE |
126 | ONE |
142 | CHAR char |
127 | CH char |
143 | SEQ rexp rexp |
128 | SEQ rexp rexp |
144 | ALT rexp rexp |
129 | ALT rexp rexp |
145 | STAR rexp |
130 | STAR rexp |
146 |
131 |
147 section {* Semantics of Regular Expressions *} |
132 section \<open>Semantics of Regular Expressions\<close> |
148 |
133 |
149 fun |
134 fun |
150 L :: "rexp \<Rightarrow> string set" |
135 L :: "rexp \<Rightarrow> string set" |
151 where |
136 where |
152 "L (ZERO) = {}" |
137 "L (ZERO) = {}" |
153 | "L (ONE) = {[]}" |
138 | "L (ONE) = {[]}" |
154 | "L (CHAR c) = {[c]}" |
139 | "L (CH c) = {[c]}" |
155 | "L (SEQ r1 r2) = (L r1) ;; (L r2)" |
140 | "L (SEQ r1 r2) = (L r1) ;; (L r2)" |
156 | "L (ALT r1 r2) = (L r1) \<union> (L r2)" |
141 | "L (ALT r1 r2) = (L r1) \<union> (L r2)" |
157 | "L (STAR r) = (L r)\<star>" |
142 | "L (STAR r) = (L r)\<star>" |
158 |
143 |
159 |
144 |
160 section {* Nullable, Derivatives *} |
145 section \<open>Nullable, Derivatives\<close> |
161 |
146 |
162 fun |
147 fun |
163 nullable :: "rexp \<Rightarrow> bool" |
148 nullable :: "rexp \<Rightarrow> bool" |
164 where |
149 where |
165 "nullable (ZERO) = False" |
150 "nullable (ZERO) = False" |
166 | "nullable (ONE) = True" |
151 | "nullable (ONE) = True" |
167 | "nullable (CHAR c) = False" |
152 | "nullable (CH c) = False" |
168 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)" |
153 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)" |
169 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)" |
154 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)" |
170 | "nullable (STAR r) = True" |
155 | "nullable (STAR r) = True" |
171 |
156 |
172 |
157 |
173 fun |
158 fun |
174 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
159 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
175 where |
160 where |
176 "der c (ZERO) = ZERO" |
161 "der c (ZERO) = ZERO" |
177 | "der c (ONE) = ZERO" |
162 | "der c (ONE) = ZERO" |
178 | "der c (CHAR d) = (if c = d then ONE else ZERO)" |
163 | "der c (CH d) = (if c = d then ONE else ZERO)" |
179 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)" |
164 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)" |
180 | "der c (SEQ r1 r2) = |
165 | "der c (SEQ r1 r2) = |
181 (if nullable r1 |
166 (if nullable r1 |
182 then ALT (SEQ (der c r1) r2) (der c r2) |
167 then ALT (SEQ (der c r1) r2) (der c r2) |
183 else SEQ (der c r1) r2)" |
168 else SEQ (der c r1) r2)" |