equal
deleted
inserted
replaced
40 | "L (EMPTY) = {[]}" |
40 | "L (EMPTY) = {[]}" |
41 | "L (CHAR c) = {[c]}" |
41 | "L (CHAR c) = {[c]}" |
42 | "L (SEQ r1 r2) = (L r1) ;; (L r2)" |
42 | "L (SEQ r1 r2) = (L r1) ;; (L r2)" |
43 | "L (ALT r1 r2) = (L r1) \<union> (L r2)" |
43 | "L (ALT r1 r2) = (L r1) \<union> (L r2)" |
44 |
44 |
45 <<<<<<< local |
|
46 fun |
45 fun |
47 nullable :: "rexp \<Rightarrow> bool" |
46 nullable :: "rexp \<Rightarrow> bool" |
48 where |
47 where |
49 "nullable (NULL) = False" |
48 "nullable (NULL) = False" |
50 | "nullable (EMPTY) = True" |
49 | "nullable (EMPTY) = True" |
51 | "nullable (CHAR c) = False" |
50 | "nullable (CHAR c) = False" |
52 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)" |
51 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)" |
53 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)" |
52 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)" |
54 ======= |
53 |
55 value "L(CHAR c)" |
54 value "L(CHAR c)" |
56 value "L(SEQ(CHAR c)(CHAR b))" |
55 value "L(SEQ(CHAR c)(CHAR b))" |
57 >>>>>>> other |
56 |
58 |
|
59 <<<<<<< local |
|
60 lemma nullable_correctness: |
57 lemma nullable_correctness: |
61 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
58 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
62 apply (induct r) |
59 apply (induct r) |
63 apply(auto simp add: Sequ_def) |
60 apply(auto simp add: Sequ_def) |
64 done |
61 done |
65 ======= |
|
66 >>>>>>> other |
|
67 |
62 |
68 section {* Values *} |
63 section {* Values *} |
69 |
64 |
70 datatype val = |
65 datatype val = |
71 Void |
66 Void |
98 | "flats(Char c) = [[c]]" |
93 | "flats(Char c) = [[c]]" |
99 | "flats(Left v) = flats(v)" |
94 | "flats(Left v) = flats(v)" |
100 | "flats(Right v) = flats(v)" |
95 | "flats(Right v) = flats(v)" |
101 | "flats(Seq v1 v2) = (flats v1) @ (flats v2)" |
96 | "flats(Seq v1 v2) = (flats v1) @ (flats v2)" |
102 |
97 |
|
98 value "flats(Seq(Char c)(Char b))" |
103 |
99 |
104 section {* Relation between values and regular expressions *} |
100 section {* Relation between values and regular expressions *} |
105 |
101 |
106 inductive Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100) |
102 inductive Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100) |
107 where |
103 where |
122 using assms |
118 using assms |
123 apply(induct rule: nullable.induct) |
119 apply(induct rule: nullable.induct) |
124 apply(auto intro: Prf.intros) |
120 apply(auto intro: Prf.intros) |
125 done |
121 done |
126 |
122 |
127 <<<<<<< local |
|
128 ======= |
|
129 value "flat(Seq(Char c)(Char b))" |
123 value "flat(Seq(Char c)(Char b))" |
130 value "flat(Right(Void))" |
124 value "flat(Right(Void))" |
131 >>>>>>> other |
|
132 |
|
133 <<<<<<< local |
|
134 |
125 |
135 lemma mkeps_flat: |
126 lemma mkeps_flat: |
136 assumes "nullable(r)" shows "flat (mkeps r) = []" |
127 assumes "nullable(r)" shows "flat (mkeps r) = []" |
137 using assms |
128 using assms |
138 apply(induct rule: nullable.induct) |
129 apply(induct rule: nullable.induct) |
141 |
132 |
142 text {* |
133 text {* |
143 The value mkeps returns is always the correct POSIX |
134 The value mkeps returns is always the correct POSIX |
144 value. |
135 value. |
145 *} |
136 *} |
146 ======= |
137 |
147 fun flats :: "val \<Rightarrow> string list" |
138 |
148 where |
139 |
149 "flats(Void) = [[]]" |
140 |
150 | "flats(Char c) = [[c]]" |
|
151 | "flats(Left v) = flats(v)" |
|
152 | "flats(Right v) = flats(v)" |
|
153 | "flats(Seq v1 v2) = (flats v1) @ (flats v2)" |
|
154 >>>>>>> other |
|
155 |
|
156 value "flats(Seq(Char c)(Char b))" |
|
157 |
141 |
158 lemma Prf_flat_L: |
142 lemma Prf_flat_L: |
159 assumes "\<turnstile> v : r" shows "flat v \<in> L r" |
143 assumes "\<turnstile> v : r" shows "flat v \<in> L r" |
160 using assms |
144 using assms |
161 apply(induct) |
145 apply(induct) |
173 apply (metis Prf.intros(3) flat.simps(4)) |
157 apply (metis Prf.intros(3) flat.simps(4)) |
174 apply(erule Prf.cases) |
158 apply(erule Prf.cases) |
175 apply(auto) |
159 apply(auto) |
176 done |
160 done |
177 |
161 |
178 definition definition prefix :: :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100) |
162 definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100) |
179 where |
163 where |
180 "s1 \<sqsubset> s2 \<equiv> \<exists>s3. s1 @ s3 = s2" |
164 "s1 \<sqsubset> s2 \<equiv> \<exists>s3. s1 @ s3 = s2" |
181 |
165 |
182 section {* Ordering of values *} |
166 section {* Ordering of values *} |
183 |
167 |