221 |
221 |
222 lemma fresh_unit: |
222 lemma fresh_unit: |
223 shows "a \<sharp> ()" |
223 shows "a \<sharp> ()" |
224 by (simp add: fresh_def supp_unit) |
224 by (simp add: fresh_def supp_unit) |
225 |
225 |
|
226 lemma permute_eqvt_raw: |
|
227 shows "p \<bullet> permute = permute" |
|
228 apply(simp add: expand_fun_eq permute_fun_def) |
|
229 apply(subst permute_eqvt) |
|
230 apply(simp) |
|
231 done |
|
232 |
226 section {* Equivariance automation *} |
233 section {* Equivariance automation *} |
227 |
234 |
228 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_force} *} |
235 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_force} *} |
229 |
236 |
230 use "nominal_thmdecls.ML" |
237 use "nominal_thmdecls.ML" |
235 eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt |
242 eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt |
236 True_eqvt False_eqvt ex_eqvt all_eqvt ex1_eqvt |
243 True_eqvt False_eqvt ex_eqvt all_eqvt ex1_eqvt |
237 imp_eqvt [folded induct_implies_def] |
244 imp_eqvt [folded induct_implies_def] |
238 |
245 |
239 (* nominal *) |
246 (* nominal *) |
240 (*permute_eqvt commented out since it loops *) |
|
241 supp_eqvt fresh_eqvt |
247 supp_eqvt fresh_eqvt |
242 permute_pure |
|
243 |
248 |
244 (* datatypes *) |
249 (* datatypes *) |
245 permute_prod.simps append_eqvt rev_eqvt set_eqvt |
250 permute_prod.simps append_eqvt rev_eqvt set_eqvt |
246 fst_eqvt snd_eqvt Pair_eqvt |
251 fst_eqvt snd_eqvt Pair_eqvt |
247 |
252 |
248 (* sets *) |
253 (* sets *) |
249 empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt |
254 empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt |
250 Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt image_eqvt |
255 Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt image_eqvt |
251 |
256 |
252 atom_eqvt add_perm_eqvt |
257 atom_eqvt add_perm_eqvt |
|
258 |
|
259 lemmas [eqvt_raw] = |
|
260 permute_eqvt_raw[THEN eq_reflection] (* the normal version of this lemma loops *) |
253 |
261 |
254 thm eqvts |
262 thm eqvts |
255 thm eqvts_raw |
263 thm eqvts_raw |
256 |
264 |
257 text {* helper lemmas for the eqvt_tac *} |
265 text {* helper lemmas for the eqvt_tac *} |
272 |
280 |
273 lemma eqvt_bound: |
281 lemma eqvt_bound: |
274 shows "p \<bullet> unpermute p x \<equiv> x" |
282 shows "p \<bullet> unpermute p x \<equiv> x" |
275 unfolding unpermute_def by simp |
283 unfolding unpermute_def by simp |
276 |
284 |
|
285 ML {* @{const Trueprop} *} |
|
286 |
277 use "nominal_permeq.ML" |
287 use "nominal_permeq.ML" |
278 |
288 setup Nominal_Permeq.setup |
279 |
289 |
280 lemma "p \<bullet> (A \<longrightarrow> B = C)" |
290 method_setup perm_simp = |
281 apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *}) |
291 {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt thms))) *} |
282 oops |
292 {* pushes permutations inside *} |
283 |
293 |
284 lemma "p \<bullet> (\<lambda>(x::'a::pt). A \<longrightarrow> (B::'a \<Rightarrow> bool) x = C) = foo" |
294 declare [[trace_eqvt = true]] |
285 apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *}) |
295 |
286 oops |
296 lemma |
287 |
297 fixes B::"'a::pt" |
288 lemma "p \<bullet> (\<lambda>x y. \<exists>z. x = z \<and> x = y \<longrightarrow> z \<noteq> x) = foo" |
298 shows "p \<bullet> (B = C)" |
289 apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *}) |
299 apply(perm_simp) |
290 oops |
300 oops |
291 |
301 |
292 lemma "p \<bullet> (\<lambda>f x. f (g (f x))) = foo" |
302 lemma |
293 apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *}) |
303 fixes B::"bool" |
294 oops |
304 shows "p \<bullet> (B = C)" |
295 |
305 apply(perm_simp) |
296 lemma "p \<bullet> (\<lambda>q. q \<bullet> (r \<bullet> x)) = foo" |
306 oops |
297 apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *}) |
307 |
298 oops |
308 lemma |
299 |
309 fixes B::"bool" |
300 lemma "p \<bullet> (q \<bullet> r \<bullet> x) = foo" |
310 shows "p \<bullet> (A \<longrightarrow> B = C)" |
301 apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *}) |
311 apply (perm_simp) |
|
312 oops |
|
313 |
|
314 lemma |
|
315 shows "p \<bullet> (\<lambda>(x::'a::pt). A \<longrightarrow> (B::'a \<Rightarrow> bool) x = C) = foo" |
|
316 apply(perm_simp) |
|
317 oops |
|
318 |
|
319 lemma |
|
320 shows "p \<bullet> (\<lambda>B::bool. A \<longrightarrow> (B = C)) = foo" |
|
321 apply (perm_simp) |
|
322 oops |
|
323 |
|
324 lemma |
|
325 shows "p \<bullet> (\<lambda>x y. \<exists>z. x = z \<and> x = y \<longrightarrow> z \<noteq> x) = foo" |
|
326 apply (perm_simp) |
|
327 oops |
|
328 |
|
329 lemma |
|
330 shows "p \<bullet> (\<lambda>f x. f (g (f x))) = foo" |
|
331 apply (perm_simp) |
|
332 oops |
|
333 |
|
334 lemma |
|
335 fixes p q::"perm" |
|
336 and x::"'a::pt" |
|
337 shows "p \<bullet> (q \<bullet> x) = foo" |
|
338 apply(perm_simp) |
|
339 oops |
|
340 |
|
341 lemma |
|
342 fixes p q r::"perm" |
|
343 and x::"'a::pt" |
|
344 shows "p \<bullet> (q \<bullet> r \<bullet> x) = foo" |
|
345 apply(perm_simp) |
|
346 oops |
|
347 |
|
348 lemma |
|
349 fixes p r::"perm" |
|
350 shows "p \<bullet> (\<lambda>q::perm. q \<bullet> (r \<bullet> x)) = foo" |
|
351 apply (perm_simp) |
|
352 oops |
|
353 |
|
354 lemma |
|
355 fixes p q r::"perm" |
|
356 and x::"'a::pt" |
|
357 shows "p \<bullet> (q \<bullet> r \<bullet> x) = foo" |
|
358 apply(perm_simp) |
|
359 oops |
|
360 |
|
361 lemma |
|
362 fixes C D::"bool" |
|
363 shows "B (p \<bullet> (C = D))" |
|
364 apply(perm_simp) |
|
365 oops |
|
366 |
|
367 declare [[trace_eqvt = false]] |
|
368 |
|
369 text {* Problem: there is no raw eqvt-rule for The *} |
|
370 lemma "p \<bullet> (THE x. P x) = foo" |
|
371 apply(perm_simp) |
302 oops |
372 oops |
303 |
373 |
304 |
374 |
305 end |
375 end |