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 |
45 fun |
46 fun |
46 nullable :: "rexp \<Rightarrow> bool" |
47 nullable :: "rexp \<Rightarrow> bool" |
47 where |
48 where |
48 "nullable (NULL) = False" |
49 "nullable (NULL) = False" |
49 | "nullable (EMPTY) = True" |
50 | "nullable (EMPTY) = True" |
50 | "nullable (CHAR c) = False" |
51 | "nullable (CHAR c) = False" |
51 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)" |
52 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)" |
52 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)" |
53 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)" |
53 |
54 ======= |
|
55 value "L(CHAR c)" |
|
56 value "L(SEQ(CHAR c)(CHAR b))" |
|
57 >>>>>>> other |
|
58 |
|
59 <<<<<<< local |
54 lemma nullable_correctness: |
60 lemma nullable_correctness: |
55 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
61 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
56 apply (induct r) |
62 apply (induct r) |
57 apply(auto simp add: Sequ_def) |
63 apply(auto simp add: Sequ_def) |
58 done |
64 done |
|
65 ======= |
|
66 >>>>>>> other |
59 |
67 |
60 section {* Values *} |
68 section {* Values *} |
61 |
69 |
62 datatype val = |
70 datatype val = |
63 Void |
71 Void |
114 using assms |
122 using assms |
115 apply(induct rule: nullable.induct) |
123 apply(induct rule: nullable.induct) |
116 apply(auto intro: Prf.intros) |
124 apply(auto intro: Prf.intros) |
117 done |
125 done |
118 |
126 |
119 |
127 <<<<<<< local |
|
128 ======= |
|
129 value "flat(Seq(Char c)(Char b))" |
|
130 value "flat(Right(Void))" |
|
131 >>>>>>> other |
|
132 |
|
133 <<<<<<< local |
120 |
134 |
121 lemma mkeps_flat: |
135 lemma mkeps_flat: |
122 assumes "nullable(r)" shows "flat (mkeps r) = []" |
136 assumes "nullable(r)" shows "flat (mkeps r) = []" |
123 using assms |
137 using assms |
124 apply(induct rule: nullable.induct) |
138 apply(induct rule: nullable.induct) |
127 |
141 |
128 text {* |
142 text {* |
129 The value mkeps returns is always the correct POSIX |
143 The value mkeps returns is always the correct POSIX |
130 value. |
144 value. |
131 *} |
145 *} |
|
146 ======= |
|
147 fun flats :: "val \<Rightarrow> string list" |
|
148 where |
|
149 "flats(Void) = [[]]" |
|
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))" |
132 |
157 |
133 lemma Prf_flat_L: |
158 lemma Prf_flat_L: |
134 assumes "\<turnstile> v : r" shows "flat v \<in> L r" |
159 assumes "\<turnstile> v : r" shows "flat v \<in> L r" |
135 using assms |
160 using assms |
136 apply(induct) |
161 apply(induct) |
148 apply (metis Prf.intros(3) flat.simps(4)) |
173 apply (metis Prf.intros(3) flat.simps(4)) |
149 apply(erule Prf.cases) |
174 apply(erule Prf.cases) |
150 apply(auto) |
175 apply(auto) |
151 done |
176 done |
152 |
177 |
153 definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100) |
178 definition definition prefix :: :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubset> _" [100, 100] 100) |
154 where |
179 where |
155 "s1 \<sqsubset> s2 \<equiv> \<exists>s3. s1 @ s3 = s2" |
180 "s1 \<sqsubset> s2 \<equiv> \<exists>s3. s1 @ s3 = s2" |
156 |
181 |
157 section {* Ordering of values *} |
182 section {* Ordering of values *} |
158 |
183 |