1 (* Authors: Julien Narboux and Christian Urban |
1 (* Title: HOL/Nominal/nominal_thmdecls.ML |
|
2 Author: Julien Narboux, TU Muenchen |
|
3 Author: Christian Urban, TU Muenchen |
2 |
4 |
3 This file introduces the infrastructure for the lemma |
5 Infrastructure for the lemma collection "eqvts". |
4 collection "eqvts". |
|
5 |
6 |
6 By attaching [eqvt] or [eqvt_force] to a lemma, it will get |
7 By attaching [eqvt] or [eqvt_force] to a lemma, it will get stored in |
7 stored in a data-slot in the context. Possible modifiers |
8 a data-slot in the context. Possible modifiers are [... add] and |
8 are [... add] and [... del] for adding and deleting, |
9 [... del] for adding and deleting, respectively, the lemma from the |
9 respectively, the lemma from the data-slot. |
10 data-slot. |
10 *) |
11 *) |
11 |
12 |
12 signature NOMINAL_THMDECLS = |
13 signature NOMINAL_THMDECLS = |
13 sig |
14 sig |
14 val eqvt_add: attribute |
15 val eqvt_add: attribute |
56 val T = fastype_of pi' |
57 val T = fastype_of pi' |
57 val mypifree = Thm.cterm_of ctxt (Const (@{const_name "rev"}, T --> T) $ pi') |
58 val mypifree = Thm.cterm_of ctxt (Const (@{const_name "rev"}, T --> T) $ pi') |
58 val perm_pi_simp = PureThy.get_thms ctxt "perm_pi_simp" |
59 val perm_pi_simp = PureThy.get_thms ctxt "perm_pi_simp" |
59 in |
60 in |
60 EVERY1 [tactic ("iffI applied", rtac @{thm iffI}), |
61 EVERY1 [tactic ("iffI applied", rtac @{thm iffI}), |
61 tactic ("remove pi with perm_boolE", dtac @{thm perm_boolE}), |
62 tactic ("remove pi with perm_boolE", dtac @{thm perm_boolE}), |
62 tactic ("solve with orig_thm", etac orig_thm), |
63 tactic ("solve with orig_thm", etac orig_thm), |
63 tactic ("applies orig_thm instantiated with rev pi", |
64 tactic ("applies orig_thm instantiated with rev pi", |
64 dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm)), |
65 dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm)), |
65 tactic ("getting rid of the pi on the right", rtac @{thm perm_boolI}), |
66 tactic ("getting rid of the pi on the right", rtac @{thm perm_boolI}), |
66 tactic ("getting rid of all remaining perms", |
67 tactic ("getting rid of all remaining perms", |
67 full_simp_tac (HOL_basic_ss addsimps perm_pi_simp))] |
68 full_simp_tac (HOL_basic_ss addsimps perm_pi_simp))] |
68 end; |
69 end; |
69 |
70 |
70 fun get_derived_thm ctxt hyp concl orig_thm pi typi = |
71 fun get_derived_thm ctxt hyp concl orig_thm pi typi = |