author | wenzelm |
Sun, 11 Jan 2009 16:41:48 +0100 | |
changeset 29444 | ff4364596fce |
parent 26928 | ca87aff1ad2d |
child 29585 | c23295521af5 |
permissions | -rw-r--r-- |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
1 |
(* ID: "$Id$" |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
2 |
Authors: Julien Narboux and Christian Urban |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
3 |
|
22846 | 4 |
This file introduces the infrastructure for the lemma |
22562
80b814fe284b
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
narboux
parents:
22541
diff
changeset
|
5 |
declaration "eqvts" "bijs" and "freshs". |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
6 |
|
22846 | 7 |
By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored |
24571 | 8 |
in a data-slot in the context. Possible modifiers |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
9 |
are [attribute add] and [attribute del] for adding and deleting, |
22846 | 10 |
respectively the lemma from the data-slot. |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
11 |
*) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
12 |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
13 |
signature NOMINAL_THMDECLS = |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
14 |
sig |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
15 |
val eqvt_add: attribute |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
16 |
val eqvt_del: attribute |
22715
381e6c45f13b
improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls
urbanc
parents:
22562
diff
changeset
|
17 |
val eqvt_force_add: attribute |
381e6c45f13b
improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls
urbanc
parents:
22562
diff
changeset
|
18 |
val eqvt_force_del: attribute |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
19 |
val setup: theory -> theory |
24571 | 20 |
val get_eqvt_thms: Proof.context -> thm list |
21 |
val get_fresh_thms: Proof.context -> thm list |
|
22 |
val get_bij_thms: Proof.context -> thm list |
|
22846 | 23 |
|
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
24 |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
25 |
val NOMINAL_EQVT_DEBUG : bool ref |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
26 |
end; |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
27 |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
28 |
structure NominalThmDecls: NOMINAL_THMDECLS = |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
29 |
struct |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
30 |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
31 |
structure Data = GenericDataFun |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
32 |
( |
22562
80b814fe284b
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
narboux
parents:
22541
diff
changeset
|
33 |
type T = {eqvts:thm list, freshs:thm list, bijs:thm list}; |
80b814fe284b
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
narboux
parents:
22541
diff
changeset
|
34 |
val empty = ({eqvts=[], freshs=[], bijs=[]}:T); |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
35 |
val extend = I; |
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset
|
36 |
fun merge _ (r1:T,r2:T) = {eqvts = Thm.merge_thms (#eqvts r1, #eqvts r2), |
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset
|
37 |
freshs = Thm.merge_thms (#freshs r1, #freshs r2), |
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset
|
38 |
bijs = Thm.merge_thms (#bijs r1, #bijs r2)} |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
39 |
); |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
40 |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
41 |
(* Exception for when a theorem does not conform with form of an equivariance lemma. *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
42 |
(* There are two forms: one is an implication (for relations) and the other is an *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
43 |
(* equality (for functions). In the implication-case, say P ==> Q, Q must be equal *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
44 |
(* to P except that every free variable of Q, say x, is replaced by pi o x. In the *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
45 |
(* equality case, say lhs = rhs, the lhs must be of the form pi o t and the rhs must *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
46 |
(* be equal to t except that every free variable, say x, is replaced by pi o x. In *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
47 |
(* the implicational case it is also checked that the variables and permutation fit *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
48 |
(* together, i.e. are of the right "pt_class", so that a stronger version of the *) |
24265
4d5917cc60c4
fix the generation of eqvt lemma of equality form from the imp form when the relation is equality
narboux
parents:
24039
diff
changeset
|
49 |
(* equality-lemma can be derived. *) |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset
|
50 |
exception EQVT_FORM of string; |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
51 |
|
24571 | 52 |
val get_eqvt_thms = Context.Proof #> Data.get #> #eqvts; |
53 |
val get_fresh_thms = Context.Proof #> Data.get #> #freshs; |
|
54 |
val get_bij_thms = Context.Proof #> Data.get #> #bijs; |
|
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
55 |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
56 |
(* FIXME: should be a function in a library *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
57 |
fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T)); |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
58 |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
59 |
val NOMINAL_EQVT_DEBUG = ref false; |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
60 |
|
22846 | 61 |
fun tactic (msg,tac) = |
62 |
if !NOMINAL_EQVT_DEBUG |
|
26652 | 63 |
then tac THEN print_tac ("after "^msg) |
22846 | 64 |
else tac |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
65 |
|
22846 | 66 |
fun tactic_eqvt ctx orig_thm pi typi = |
67 |
let |
|
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
68 |
val mypi = Thm.cterm_of ctx (Var (pi,typi)) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
69 |
val mypifree = Thm.cterm_of ctx (Const ("List.rev",typi --> typi) $ Free (fst pi,typi)) |
26343
0dd2eab7b296
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26337
diff
changeset
|
70 |
val perm_pi_simp = PureThy.get_thms ctx "perm_pi_simp" |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
71 |
in |
22846 | 72 |
EVERY [tactic ("iffI applied",rtac iffI 1), |
24571 | 73 |
tactic ("remove pi with perm_boolE", (dtac @{thm perm_boolE} 1)), |
74 |
tactic ("solve with orig_thm", (etac orig_thm 1)), |
|
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
75 |
tactic ("applies orig_thm instantiated with rev pi", |
22846 | 76 |
dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1), |
24265
4d5917cc60c4
fix the generation of eqvt lemma of equality form from the imp form when the relation is equality
narboux
parents:
24039
diff
changeset
|
77 |
tactic ("getting rid of the pi on the right", |
24571 | 78 |
(rtac @{thm perm_boolI} 1)), |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
79 |
tactic ("getting rid of all remaining perms", |
24265
4d5917cc60c4
fix the generation of eqvt lemma of equality form from the imp form when the relation is equality
narboux
parents:
24039
diff
changeset
|
80 |
full_simp_tac (HOL_basic_ss addsimps perm_pi_simp) 1)] |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
81 |
end; |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
82 |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
83 |
fun get_derived_thm thy hyp concl orig_thm pi typi = |
22846 | 84 |
let |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
85 |
val lhs = (Const("Nominal.perm", typi --> HOLogic.boolT --> HOLogic.boolT) $ Var(pi,typi) $ hyp) |
22846 | 86 |
val goal_term = Logic.unvarify (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,concl))) |
87 |
val _ = Display.print_cterm (cterm_of thy goal_term) |
|
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset
|
88 |
in |
22846 | 89 |
Goal.prove_global thy [] [] goal_term (fn _ => (tactic_eqvt thy orig_thm pi typi)) |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
90 |
end |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
91 |
|
22846 | 92 |
(* replaces every variable x in t with pi o x *) |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
93 |
fun apply_pi trm (pi,typi) = |
22846 | 94 |
let |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
95 |
fun only_vars t = |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
96 |
(case t of |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
97 |
Var (n,ty) => (Const ("Nominal.perm",typi --> ty --> ty) $ (Var (pi,typi)) $ (Var (n,ty))) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
98 |
| _ => t) |
22846 | 99 |
in |
100 |
map_aterms only_vars trm |
|
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
101 |
end; |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
102 |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
103 |
(* returns *the* pi which is in front of all variables, provided there *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
104 |
(* exists such a pi; otherwise raises EQVT_FORM *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
105 |
fun get_pi t thy = |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
106 |
let fun get_pi_aux s = |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
107 |
(case s of |
22846 | 108 |
(Const ("Nominal.perm",typrm) $ |
109 |
(Var (pi,typi as Type("List.list",[Type ("*",[Type (tyatm,[]),_])]))) $ |
|
110 |
(Var (n,ty))) => |
|
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
111 |
let |
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset
|
112 |
(* FIXME: this should be an operation the library *) |
22846 | 113 |
val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm) |
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset
|
114 |
in |
24271 | 115 |
if (Sign.of_sort thy (ty,[class_name])) |
22846 | 116 |
then [(pi,typi)] |
117 |
else raise |
|
118 |
EQVT_FORM ("Could not find any permutation or an argument is not an instance of "^class_name) |
|
119 |
end |
|
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
120 |
| Abs (_,_,t1) => get_pi_aux t1 |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
121 |
| (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2 |
22846 | 122 |
| _ => []) |
123 |
in |
|
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
124 |
(* collect first all pi's in front of variables in t and then use distinct *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
125 |
(* to ensure that all pi's must have been the same, i.e. distinct returns *) |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
126 |
(* a singleton-list *) |
22846 | 127 |
(case (distinct (op =) (get_pi_aux t)) of |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
128 |
[(pi,typi)] => (pi,typi) |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset
|
129 |
| _ => raise EQVT_FORM "All permutation should be the same") |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
130 |
end; |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
131 |
|
26652 | 132 |
(* Either adds a theorem (orig_thm) to or deletes one from the equivariance *) |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
133 |
(* lemma list depending on flag. To be added the lemma has to satisfy a *) |
22846 | 134 |
(* certain form. *) |
24265
4d5917cc60c4
fix the generation of eqvt lemma of equality form from the imp form when the relation is equality
narboux
parents:
24039
diff
changeset
|
135 |
|
4d5917cc60c4
fix the generation of eqvt lemma of equality form from the imp form when the relation is equality
narboux
parents:
24039
diff
changeset
|
136 |
fun eqvt_add_del_aux flag orig_thm context = |
22846 | 137 |
let |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
138 |
val thy = Context.theory_of context |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
139 |
val thms_to_be_added = (case (prop_of orig_thm) of |
22846 | 140 |
(* case: eqvt-lemma is of the implicational form *) |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
141 |
(Const("==>", _) $ (Const ("Trueprop",_) $ hyp) $ (Const ("Trueprop",_) $ concl)) => |
22846 | 142 |
let |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
143 |
val (pi,typi) = get_pi concl thy |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
144 |
in |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
145 |
if (apply_pi hyp (pi,typi) = concl) |
22846 | 146 |
then |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
147 |
(warning ("equivariance lemma of the relational form"); |
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
148 |
[orig_thm, get_derived_thm thy hyp concl orig_thm pi typi]) |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset
|
149 |
else raise EQVT_FORM "Type Implication" |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
150 |
end |
22846 | 151 |
(* case: eqvt-lemma is of the equational form *) |
152 |
| (Const ("Trueprop", _) $ (Const ("op =", _) $ |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset
|
153 |
(Const ("Nominal.perm",typrm) $ Var (pi,typi) $ lhs) $ rhs)) => |
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset
|
154 |
(if (apply_pi lhs (pi,typi)) = rhs |
22437
b3526cd2a336
removes some unused code that used to try to derive a simpler version of the eqvt lemmas
narboux
parents:
22418
diff
changeset
|
155 |
then [orig_thm] |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset
|
156 |
else raise EQVT_FORM "Type Equality") |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset
|
157 |
| _ => raise EQVT_FORM "Type unknown") |
22846 | 158 |
in |
26652 | 159 |
fold (fn thm => Data.map (flag thm)) thms_to_be_added context |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
160 |
end |
22846 | 161 |
handle EQVT_FORM s => |
26928 | 162 |
error (Display.string_of_thm orig_thm ^ " does not comply with the form of an equivariance lemma ("^s^").") |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
163 |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
164 |
(* in cases of bij- and freshness, we just add the lemmas to the *) |
22846 | 165 |
(* data-slot *) |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
166 |
|
26652 | 167 |
fun eqvt_map f (r:Data.T) = {eqvts = f (#eqvts r), freshs = #freshs r, bijs = #bijs r}; |
168 |
fun fresh_map f (r:Data.T) = {eqvts = #eqvts r, freshs = f (#freshs r), bijs = #bijs r}; |
|
169 |
fun bij_map f (r:Data.T) = {eqvts = #eqvts r, freshs = #freshs r, bijs = f (#bijs r)}; |
|
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
170 |
|
26652 | 171 |
val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map o Thm.add_thm)); |
172 |
val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map o Thm.del_thm)); |
|
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
173 |
|
26652 | 174 |
val eqvt_force_add = Thm.declaration_attribute (Data.map o eqvt_map o Thm.add_thm); |
175 |
val eqvt_force_del = Thm.declaration_attribute (Data.map o eqvt_map o Thm.del_thm); |
|
176 |
val bij_add = Thm.declaration_attribute (Data.map o bij_map o Thm.add_thm); |
|
177 |
val bij_del = Thm.declaration_attribute (Data.map o bij_map o Thm.del_thm); |
|
178 |
val fresh_add = Thm.declaration_attribute (Data.map o fresh_map o Thm.add_thm); |
|
179 |
val fresh_del = Thm.declaration_attribute (Data.map o fresh_map o Thm.del_thm); |
|
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
180 |
|
22715
381e6c45f13b
improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls
urbanc
parents:
22562
diff
changeset
|
181 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22286
diff
changeset
|
182 |
|
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
183 |
val setup = |
22846 | 184 |
Attrib.add_attributes |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
185 |
[("eqvt", Attrib.add_del_args eqvt_add eqvt_del, "equivariance theorem declaration"), |
22715
381e6c45f13b
improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls
urbanc
parents:
22562
diff
changeset
|
186 |
("eqvt_force", Attrib.add_del_args eqvt_force_add eqvt_force_del, |
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
22846
diff
changeset
|
187 |
"equivariance theorem declaration (without checking the form of the lemma)"), |
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
188 |
("fresh", Attrib.add_del_args fresh_add fresh_del, "freshness theorem declaration"), |
26400 | 189 |
("bij", Attrib.add_del_args bij_add bij_del, "bijection theorem declaration")] #> |
190 |
PureThy.add_thms_dynamic ("eqvts", #eqvts o Data.get) #> |
|
191 |
PureThy.add_thms_dynamic ("freshs", #freshs o Data.get) #> |
|
192 |
PureThy.add_thms_dynamic ("bijs", #bijs o Data.get); |
|
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
193 |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset
|
194 |
end; |