1 (* Title: Nominal2_Eqvt |
1 (* Title: Nominal2_Eqvt |
2 Author: Brian Huffman, |
2 Author: Brian Huffman, |
3 Author: Christian Urban |
3 Author: Christian Urban |
4 |
4 |
5 Equivariance, Supp and Fresh Lemmas for Operators. |
5 Equivariance, supp and freshness lemmas for various operators |
6 (Contains many, but not all such lemmas.) |
6 (contains many, but not all such lemmas). |
7 *) |
7 *) |
8 theory Nominal2_Eqvt |
8 theory Nominal2_Eqvt |
9 imports Nominal2_Base Nominal2_Atoms |
9 imports Nominal2_Base Nominal2_Atoms |
10 uses ("nominal_thmdecls.ML") |
10 uses ("nominal_thmdecls.ML") |
11 ("nominal_permeq.ML") |
11 ("nominal_permeq.ML") |
12 ("nominal_eqvt.ML") |
12 ("nominal_eqvt.ML") |
13 begin |
13 begin |
14 |
|
15 |
14 |
16 section {* Logical Operators *} |
15 section {* Logical Operators *} |
17 |
16 |
18 lemma eq_eqvt: |
17 lemma eq_eqvt: |
19 shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)" |
18 shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)" |
287 |
286 |
288 (* provides perm_simp methods *) |
287 (* provides perm_simp methods *) |
289 use "nominal_permeq.ML" |
288 use "nominal_permeq.ML" |
290 setup Nominal_Permeq.setup |
289 setup Nominal_Permeq.setup |
291 |
290 |
|
291 ML {* |
|
292 val test1 = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) []; |
|
293 val test2 = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- |
|
294 (Scan.repeat (Args.const true))) [] |
|
295 *} |
|
296 |
292 method_setup perm_simp = |
297 method_setup perm_simp = |
293 {* Attrib.thms >> |
298 {* test1 -- test2 >> |
294 (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt thms ["The"]))) *} |
299 (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt [] consts))) *} |
295 {* pushes permutations inside *} |
300 {* pushes permutations inside *} |
296 |
301 |
297 method_setup perm_strict_simp = |
302 method_setup perm_strict_simp = |
298 {* Attrib.thms >> |
303 {* test1 -- test2 >> |
299 (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_strict_tac ctxt thms ["The"]))) *} |
304 (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL |
|
305 (Nominal_Permeq.eqvt_strict_tac ctxt thms consts))) *} |
300 {* pushes permutations inside, raises an error if it cannot solve all permutations *} |
306 {* pushes permutations inside, raises an error if it cannot solve all permutations *} |
301 |
307 |
302 declare [[trace_eqvt = true]] |
308 declare [[trace_eqvt = true]] |
303 |
309 |
304 lemma |
310 lemma |
367 |
373 |
368 declare [[trace_eqvt = false]] |
374 declare [[trace_eqvt = false]] |
369 |
375 |
370 text {* Problem: there is no raw eqvt-rule for The *} |
376 text {* Problem: there is no raw eqvt-rule for The *} |
371 lemma "p \<bullet> (THE x. P x) = foo" |
377 lemma "p \<bullet> (THE x. P x) = foo" |
372 apply(tactic {* Nominal_Permeq.eqvt_tac @{context} [] [@{const_name "The"}] 1*}) |
378 apply(perm_strict_simp exclude: The) |
373 apply(perm_simp) |
379 apply(perm_simp exclude: The) |
374 (* apply(perm_strict_simp) *) |
|
375 oops |
380 oops |
376 |
381 |
377 (* automatic equivariance procedure for |
382 (* automatic equivariance procedure for |
378 inductive definitions *) |
383 inductive definitions *) |
379 use "nominal_eqvt.ML" |
384 use "nominal_eqvt.ML" |