80 |
80 |
81 lemma Posix_simp: |
81 lemma Posix_simp: |
82 assumes "s \<in> (fst (simp r)) \<rightarrow> v" |
82 assumes "s \<in> (fst (simp r)) \<rightarrow> v" |
83 shows "s \<in> r \<rightarrow> ((snd (simp r)) v)" |
83 shows "s \<in> r \<rightarrow> ((snd (simp r)) v)" |
84 using assms |
84 using assms |
85 apply(induct r arbitrary: s v rule: simp.induct) |
85 proof(induct r arbitrary: s v rule: rexp.induct) |
86 apply(simp_all) |
86 case (ALT r1 r2 s v) |
87 apply(auto)[1] |
87 have IH1: "\<And>s v. s \<in> fst (simp r1) \<rightarrow> v \<Longrightarrow> s \<in> r1 \<rightarrow> snd (simp r1) v" by fact |
88 using Posix_elims(1) apply blast |
88 have IH2: "\<And>s v. s \<in> fst (simp r2) \<rightarrow> v \<Longrightarrow> s \<in> r2 \<rightarrow> snd (simp r2) v" by fact |
89 apply (simp add: Posix_ALT1) |
89 have as: "s \<in> fst (simp (ALT r1 r2)) \<rightarrow> v" by fact |
90 apply (metis L.simps(1) L_fst_simp Posix_ALT2 empty_iff) |
90 consider (ZERO_ZERO) "fst (simp r1) = ZERO" "fst (simp r2) = ZERO" |
91 apply (smt F_ALT.simps(1) F_ALT.simps(2) L_fst_simp Posix_ALT1 Posix_ALT2 Posix_elims(4)) |
91 | (ZERO_NZERO) "fst (simp r1) = ZERO" "fst (simp r2) \<noteq> ZERO" |
92 apply(auto)[1] |
92 | (NZERO_ZERO) "fst (simp r1) \<noteq> ZERO" "fst (simp r2) = ZERO" |
93 apply (metis (no_types, lifting) Nil_is_append_conv Posix_SEQ Posix_elims(2)) |
93 | (NZERO_NZERO) "fst (simp r1) \<noteq> ZERO" "fst (simp r2) \<noteq> ZERO" by auto |
94 apply(subst append_Nil2[symmetric]) |
94 then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" |
95 apply(rule Posix_SEQ) |
95 proof(cases) |
96 apply(simp) |
96 case (ZERO_ZERO) |
97 using Posix_ONE apply blast |
97 with as have "s \<in> ZERO \<rightarrow> v" by simp |
98 apply blast |
98 then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" by (rule Posix_elims(1)) |
99 apply(subst append_Nil[symmetric]) |
99 next |
100 apply(rule Posix_SEQ) |
100 case (ZERO_NZERO) |
101 using Posix_ONE apply blast |
101 with as have "s \<in> fst (simp r2) \<rightarrow> v" by simp |
102 apply blast |
102 with IH2 have "s \<in> r2 \<rightarrow> snd (simp r2) v" by simp |
103 apply(auto)[1] |
103 moreover |
104 apply (metis L.simps(2) L_fst_simp ex_in_conv insert_iff) |
104 from ZERO_NZERO have "fst (simp r1) = ZERO" by simp |
105 apply(erule Posix_elims) |
105 then have "L (fst (simp r1)) = {}" by simp |
106 apply(auto) |
106 then have "L r1 = {}" using L_fst_simp by simp |
107 using L_fst_simp Posix_SEQ by auto |
107 then have "s \<notin> L r1" by simp |
|
108 ultimately have "s \<in> ALT r1 r2 \<rightarrow> Right (snd (simp r2) v)" by (rule Posix_ALT2) |
|
109 then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" |
|
110 using ZERO_NZERO by simp |
|
111 next |
|
112 case (NZERO_ZERO) |
|
113 with as have "s \<in> fst (simp r1) \<rightarrow> v" by simp |
|
114 with IH1 have "s \<in> r1 \<rightarrow> snd (simp r1) v" by simp |
|
115 then have "s \<in> ALT r1 r2 \<rightarrow> Left (snd (simp r1) v)" by (rule Posix_ALT1) |
|
116 then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" using NZERO_ZERO by simp |
|
117 next |
|
118 case (NZERO_NZERO) |
|
119 with as have "s \<in> ALT (fst (simp r1)) (fst (simp r2)) \<rightarrow> v" by simp |
|
120 then consider (Left) v1 where "v = Left v1" "s \<in> (fst (simp r1)) \<rightarrow> v1" |
|
121 | (Right) v2 where "v = Right v2" "s \<in> (fst (simp r2)) \<rightarrow> v2" "s \<notin> L (fst (simp r1))" |
|
122 by (erule_tac Posix_elims(4)) |
|
123 then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" |
|
124 proof(cases) |
|
125 case (Left) |
|
126 then have "v = Left v1" "s \<in> r1 \<rightarrow> (snd (simp r1) v1)" using IH1 by simp_all |
|
127 then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" using NZERO_NZERO |
|
128 by (simp_all add: Posix_ALT1) |
|
129 next |
|
130 case (Right) |
|
131 then have "v = Right v2" "s \<in> r2 \<rightarrow> (snd (simp r2) v2)" "s \<notin> L r1" using IH2 L_fst_simp by simp_all |
|
132 then show "s \<in> ALT r1 r2 \<rightarrow> snd (simp (ALT r1 r2)) v" using NZERO_NZERO |
|
133 by (simp_all add: Posix_ALT2) |
|
134 qed |
|
135 qed |
|
136 next |
|
137 case (SEQ r1 r2 s v) |
|
138 have IH1: "\<And>s v. s \<in> fst (simp r1) \<rightarrow> v \<Longrightarrow> s \<in> r1 \<rightarrow> snd (simp r1) v" by fact |
|
139 have IH2: "\<And>s v. s \<in> fst (simp r2) \<rightarrow> v \<Longrightarrow> s \<in> r2 \<rightarrow> snd (simp r2) v" by fact |
|
140 have as: "s \<in> fst (simp (SEQ r1 r2)) \<rightarrow> v" by fact |
|
141 consider (ONE_ONE) "fst (simp r1) = ONE" "fst (simp r2) = ONE" |
|
142 | (ONE_NONE) "fst (simp r1) = ONE" "fst (simp r2) \<noteq> ONE" |
|
143 | (NONE_ONE) "fst (simp r1) \<noteq> ONE" "fst (simp r2) = ONE" |
|
144 | (NONE_NONE) "fst (simp r1) \<noteq> ONE" "fst (simp r2) \<noteq> ONE" by auto |
|
145 then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" |
|
146 proof(cases) |
|
147 case (ONE_ONE) |
|
148 with as have b: "s \<in> ONE \<rightarrow> v" by simp |
|
149 from b have "s \<in> r1 \<rightarrow> snd (simp r1) v" using IH1 ONE_ONE by simp |
|
150 moreover |
|
151 from b have c: "s = []" "v = Void" using Posix_elims(2) by auto |
|
152 moreover |
|
153 have "[] \<in> ONE \<rightarrow> Void" by (simp add: Posix_ONE) |
|
154 then have "[] \<in> fst (simp r2) \<rightarrow> Void" using ONE_ONE by simp |
|
155 then have "[] \<in> r2 \<rightarrow> snd (simp r2) Void" using IH2 by simp |
|
156 ultimately have "([] @ []) \<in> SEQ r1 r2 \<rightarrow> Seq (snd (simp r1) Void) (snd (simp r2) Void)" |
|
157 using Posix_SEQ by blast |
|
158 then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" using c ONE_ONE by simp |
|
159 next |
|
160 case (ONE_NONE) |
|
161 with as have b: "s \<in> fst (simp r2) \<rightarrow> v" by simp |
|
162 from b have "s \<in> r2 \<rightarrow> snd (simp r2) v" using IH2 ONE_NONE by simp |
|
163 moreover |
|
164 have "[] \<in> ONE \<rightarrow> Void" by (simp add: Posix_ONE) |
|
165 then have "[] \<in> fst (simp r1) \<rightarrow> Void" using ONE_NONE by simp |
|
166 then have "[] \<in> r1 \<rightarrow> snd (simp r1) Void" using IH1 by simp |
|
167 moreover |
|
168 from ONE_NONE(1) have "L (fst (simp r1)) = {[]}" by simp |
|
169 then have "L r1 = {[]}" by (simp add: L_fst_simp[symmetric]) |
|
170 ultimately have "([] @ s) \<in> SEQ r1 r2 \<rightarrow> Seq (snd (simp r1) Void) (snd (simp r2) v)" |
|
171 by(rule_tac Posix_SEQ) auto |
|
172 then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" using ONE_NONE by simp |
|
173 next |
|
174 case (NONE_ONE) |
|
175 with as have "s \<in> fst (simp r1) \<rightarrow> v" by simp |
|
176 with IH1 have "s \<in> r1 \<rightarrow> snd (simp r1) v" by simp |
|
177 moreover |
|
178 have "[] \<in> ONE \<rightarrow> Void" by (simp add: Posix_ONE) |
|
179 then have "[] \<in> fst (simp r2) \<rightarrow> Void" using NONE_ONE by simp |
|
180 then have "[] \<in> r2 \<rightarrow> snd (simp r2) Void" using IH2 by simp |
|
181 ultimately have "(s @ []) \<in> SEQ r1 r2 \<rightarrow> Seq (snd (simp r1) v) (snd (simp r2) Void)" |
|
182 by(rule_tac Posix_SEQ) auto |
|
183 then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" using NONE_ONE by simp |
|
184 next |
|
185 case (NONE_NONE) |
|
186 with as have "s \<in> SEQ (fst (simp r1)) (fst (simp r2)) \<rightarrow> v" by simp |
|
187 then obtain s1 s2 v1 v2 where eqs: "s = s1 @ s2" "v = Seq v1 v2" |
|
188 "s1 \<in> (fst (simp r1)) \<rightarrow> v1" "s2 \<in> (fst (simp r2)) \<rightarrow> v2" |
|
189 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" |
|
190 by (erule_tac Posix_elims(5)) (auto simp add: L_fst_simp[symmetric]) |
|
191 then have "s1 \<in> r1 \<rightarrow> (snd (simp r1) v1)" "s2 \<in> r2 \<rightarrow> (snd (simp r2) v2)" |
|
192 using IH1 IH2 by auto |
|
193 then show "s \<in> SEQ r1 r2 \<rightarrow> snd (simp (SEQ r1 r2)) v" using eqs NONE_NONE |
|
194 by(auto intro: Posix_SEQ) |
|
195 qed |
|
196 qed (simp_all) |
108 |
197 |
109 |
198 |
110 lemma slexer_correctness: |
199 lemma slexer_correctness: |
111 shows "slexer r s = lexer r s" |
200 shows "slexer r s = lexer r s" |
112 proof(induct s arbitrary: r) |
201 proof(induct s arbitrary: r) |