152 |
152 |
153 lemma strong_exhaust1: |
153 lemma strong_exhaust1: |
154 fixes c::"'a::fs" |
154 fixes c::"'a::fs" |
155 assumes "\<exists>name. y = Var name \<Longrightarrow> P" |
155 assumes "\<exists>name. y = Var name \<Longrightarrow> P" |
156 and "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
156 and "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
157 and "\<exists>name trm. {atom name} \<sharp>* c \<and> y = Lam name trm \<Longrightarrow> P" |
157 and "\<exists>name trm. {atom name} \<sharp>* c \<and> y = Lam name trm \<Longrightarrow> P" |
158 and "\<exists>assn trm. set (bn1 assn) \<sharp>* c \<and> y = Let1 assn trm \<Longrightarrow> P" |
158 and "\<exists>(c::'a::fs) assn trm. set (bn1 assn) \<sharp>* c \<and> y = Let1 assn trm \<Longrightarrow> P" |
159 and "\<exists>assn trm. set (bn2 assn) \<sharp>* c \<and> y = Let2 assn trm \<Longrightarrow> P" |
159 and "\<exists>(c::'a::fs) assn trm. set (bn2 assn) \<sharp>* c \<and> y = Let2 assn trm \<Longrightarrow> P" |
160 and "\<exists>assn trm. set (bn3 assn) \<sharp>* c \<and> y = Let3 assn trm \<Longrightarrow> P" |
160 and "\<exists>(c::'a::fs) assn trm. set (bn3 assn) \<sharp>* c \<and> y = Let3 assn trm \<Longrightarrow> P" |
161 and "\<exists>assn' trm. (bn4 assn') \<sharp>* c \<and> y = Let4 assn' trm \<Longrightarrow> P" |
161 and "\<exists>(c::'a::fs) assn' trm. (bn4 assn') \<sharp>* c \<and> y = Let4 assn' trm \<Longrightarrow> P" |
162 shows "P" |
162 shows "P" |
163 apply(rule_tac y="y" in foo.exhaust(1)) |
163 apply(rule_tac y="y" in foo.exhaust(1)) |
164 apply(rule assms(1)) |
164 apply(rule assms(1)) |
165 apply(rule exI) |
165 apply(rule exI) |
166 apply(assumption) |
166 apply(assumption) |
167 apply(rule assms(2)) |
167 apply(rule assms(2)) |
168 apply(rule exI)+ |
168 apply(rule exI)+ |
169 apply(assumption) |
169 apply(assumption) |
170 apply(rule assms(3)) |
170 apply(rule assms(3)) |
|
171 apply(subgoal_tac "\<exists>p::perm. (p \<bullet> {atom name}) \<sharp>* (c, name, trm)") |
|
172 apply(erule exE) |
|
173 apply(perm_simp) |
|
174 apply(rule_tac exI)+ |
|
175 apply(rule conjI) |
|
176 apply(simp add: fresh_star_prod) |
|
177 apply(erule conjE)+ |
|
178 apply(assumption) |
|
179 apply(simp) |
|
180 apply(simp add: foo.eq_iff) |
|
181 (* HERE *) |
|
182 defer |
|
183 defer |
|
184 apply(rule assms(4)) |
|
185 apply(subgoal_tac "\<exists>p::perm. (p \<bullet> (set (bn1 assg))) \<sharp>* (c, assg, trm)") |
|
186 apply(erule exE) |
|
187 apply(perm_simp add: tt1) |
|
188 apply(simp only: fresh_star_prod) |
|
189 apply(erule conjE)+ |
|
190 apply(rule_tac exI)+ |
|
191 apply(rule conjI) |
|
192 apply(assumption) |
|
193 apply(simp add: foo.eq_iff) |
|
194 apply(rule conjI) |
|
195 apply(simp only: tt1[symmetric]) |
|
196 defer |
|
197 apply(rule uu1) |
|
198 defer |
|
199 apply(rule assms(5)) |
|
200 apply(subgoal_tac "\<exists>p::perm. (p \<bullet> (set (bn2 assg))) \<sharp>* (c, assg, trm)") |
|
201 apply(erule exE) |
|
202 apply(perm_simp add: tt2) |
|
203 apply(simp only: fresh_star_prod) |
|
204 apply(erule conjE)+ |
|
205 apply(rule_tac exI)+ |
|
206 apply(rule conjI) |
|
207 apply(assumption) |
|
208 apply(simp add: foo.eq_iff) |
|
209 apply(rule conjI) |
|
210 apply(simp only: tt2[symmetric]) |
|
211 defer |
|
212 apply(rule uu2) |
|
213 defer |
|
214 apply(rule refl) |
|
215 apply(subst (asm) fresh_star_supp_conv) |
|
216 apply(simp) |
|
217 |
|
218 |
|
219 lemma strong_exhaust2: |
|
220 fixes c::"'a::fs" |
|
221 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
|
222 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
|
223 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
|
224 and "\<And>assn trm. \<lbrakk>set (bn1 assn) \<sharp>* c; y = Let1 assn trm\<rbrakk> \<Longrightarrow> P" |
|
225 and "\<And>assn trm. \<lbrakk>set (bn2 assn) \<sharp>* c; y = Let2 assn trm\<rbrakk> \<Longrightarrow> P" |
|
226 and "\<And>assn trm. \<lbrakk>set (bn3 assn) \<sharp>* c; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P" |
|
227 and "\<And>assn' trm. \<lbrakk>(bn4 assn') \<sharp>* c; y = Let4 assn' trm\<rbrakk> \<Longrightarrow> P" |
|
228 shows "P" |
|
229 apply(rule strong_exhaust1[where y="y"]) |
|
230 apply(erule exE)+ |
|
231 apply(rule assms(1)) |
|
232 apply(assumption) |
|
233 apply(erule exE)+ |
|
234 apply(rule assms(2)) |
|
235 apply(assumption) |
|
236 apply(erule exE | erule conjE)? |
|
237 apply(rule assms(3)) |
|
238 apply(drule_tac x="c" in spec) |
|
239 apply(erule exE | erule conjE)+ |
|
240 apply(assumption)+ |
|
241 apply(drule_tac x="c" in spec) |
|
242 apply(erule exE | erule conjE)+ |
|
243 apply(assumption)+ |
|
244 apply(erule exE | erule conjE)+ |
|
245 apply(rule assms(4)) |
|
246 apply(assumption)+ |
|
247 apply(erule exE | erule conjE)+ |
|
248 apply(rule assms(5)) |
|
249 apply(assumption)+ |
|
250 apply(erule exE | erule conjE)+ |
|
251 apply(rule assms(6)) |
|
252 apply(assumption)+ |
|
253 apply(erule exE | erule conjE)+ |
|
254 apply(rule assms(7)) |
|
255 apply(assumption)+ |
|
256 done |
|
257 |
|
258 |
|
259 |
|
260 |
|
261 |
|
262 |
|
263 |
|
264 |
|
265 |
|
266 |
|
267 |
|
268 |
|
269 apply(rule_tac y="y" in foo.exhaust(1)) |
|
270 apply(rule assms(1)) |
|
271 apply(rule exI) |
|
272 apply(assumption) |
|
273 apply(rule assms(2)) |
|
274 apply(rule exI)+ |
|
275 apply(assumption) |
|
276 apply(rule assms(3)) |
|
277 apply(rule_tac p="p" in permute_boolE) |
|
278 apply(perm_simp) |
|
279 apply(simp) |
171 apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q") |
280 apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q") |
172 apply(erule exE) |
281 apply(erule exE) |
173 apply(erule conjE) |
282 apply(erule conjE) |
174 apply(rule assms(3)) |
283 apply(rule assms(3)) |
175 apply(perm_simp) |
284 apply(perm_simp) |