1 (* Title: nominal_thmdecls.ML |
1 (* Title: nominal_thmdecls.ML |
2 Author: Christian Urban |
2 Author: Christian Urban |
3 |
3 |
4 Infrastructure for the lemma collection "eqvts". |
4 Infrastructure for the lemma collection "eqvts". |
5 |
5 |
6 Provides the attributes [eqvt] and [eqvt_force], and the theorem |
6 Provides the attributes [eqvt] and [eqvt_raw], and the theorem |
7 lists eqvts and eqvts_raw. The first attribute will store the theorem |
7 lists eqvts and eqvts_raw. The first attribute will store the |
8 in the eqvts list and also in the eqvts_raw list. For the latter |
8 theorem in the eqvts list and also in the eqvts_raw list. For |
9 the theorem is expected to be of the form |
9 the latter the theorem is expected to be of the form |
10 |
10 |
11 p o (c x1 x2 ...) = c (p o x1) (p o x2) ... |
11 p o (c x1 x2 ...) = c (p o x1) (p o x2) ... |
12 |
12 |
13 and is stored in the form |
13 and it is stored in the form |
14 |
14 |
15 p o c == c |
15 p o c == c |
16 |
16 |
17 The [eqvt_force] attribute just adds the theorem to eqvts. |
17 The [eqvt_raw] attribute just adds the theorem to eqvts_raw. |
18 |
18 |
19 TODO: |
19 TODO: |
20 |
20 |
21 - deal with eqvt-lemmas of the form |
21 - deal with eqvt-lemmas of the form |
22 |
22 |
25 |
25 |
26 signature NOMINAL_THMDECLS = |
26 signature NOMINAL_THMDECLS = |
27 sig |
27 sig |
28 val eqvt_add: attribute |
28 val eqvt_add: attribute |
29 val eqvt_del: attribute |
29 val eqvt_del: attribute |
30 val eqvt_force_add: attribute |
30 val eqvt_raw_add: attribute |
31 val eqvt_force_del: attribute |
31 val eqvt_raw_del: attribute |
32 val setup: theory -> theory |
32 val setup: theory -> theory |
33 val get_eqvt_thms: Proof.context -> thm list |
33 val get_eqvts_thms: Proof.context -> thm list |
34 val get_eqvt_raw_thms: Proof.context -> thm list |
34 val get_eqvts_raw_thms: Proof.context -> thm list |
35 |
35 |
36 end; |
36 end; |
37 |
37 |
38 structure Nominal_ThmDecls: NOMINAL_THMDECLS = |
38 structure Nominal_ThmDecls: NOMINAL_THMDECLS = |
39 struct |
39 struct |
40 |
40 |
|
41 |
41 structure EqvtData = Generic_Data |
42 structure EqvtData = Generic_Data |
42 ( |
43 ( type T = thm Item_Net.T; |
43 type T = (thm * thm option) Item_Net.T; |
44 val empty = Thm.full_rules; |
44 val empty = Item_Net.init (eq_fst Thm.eq_thm_prop) (single o Thm.full_prop_of o fst) |
|
45 val extend = I; |
45 val extend = I; |
46 val merge = Item_Net.merge; |
46 val merge = Item_Net.merge ); |
47 ); |
|
48 |
47 |
49 val eqvts = (map fst) o Item_Net.content o EqvtData.get; |
48 structure EqvtRawData = Generic_Data |
50 val eqvts_raw = (map_filter snd) o Item_Net.content o EqvtData.get; |
49 ( type T = thm Item_Net.T; |
|
50 val empty = Thm.full_rules; |
|
51 val extend = I; |
|
52 val merge = Item_Net.merge ); |
51 |
53 |
52 val get_eqvt_thms = eqvts o Context.Proof; |
54 val eqvts = Item_Net.content o EqvtData.get; |
53 val get_eqvt_raw_thms = eqvts_raw o Context.Proof; |
55 val eqvts_raw = Item_Net.content o EqvtRawData.get; |
|
56 |
|
57 val get_eqvts_thms = eqvts o Context.Proof; |
|
58 val get_eqvts_raw_thms = eqvts_raw o Context.Proof; |
54 |
59 |
55 val add_thm = EqvtData.map o Item_Net.update; |
60 val add_thm = EqvtData.map o Item_Net.update; |
56 val del_thm = EqvtData.map o Item_Net.remove; |
61 val del_thm = EqvtData.map o Item_Net.remove; |
57 |
62 |
58 val add_force_thm = EqvtData.map o Item_Net.update; |
63 val add_raw_thm = EqvtRawData.map o Item_Net.update; |
59 val del_force_thm = EqvtData.map o Item_Net.remove; |
64 val del_raw_thm = EqvtRawData.map o Item_Net.remove; |
60 |
65 |
61 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
66 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
62 | dest_perm t = raise TERM("dest_perm", [t]) |
67 | dest_perm t = raise TERM("dest_perm", [t]) |
63 |
68 |
64 fun mk_perm p trm = |
69 fun mk_perm p trm = |
92 then thm |
97 then thm |
93 else Goal.prove ctxt [p_str] [] goal |
98 else Goal.prove ctxt [p_str] [] goal |
94 (fn _ => eqvt_transform_tac thm 1) |
99 (fn _ => eqvt_transform_tac thm 1) |
95 end |
100 end |
96 |
101 |
97 fun transform addel_fn thm context = |
102 fun transform addel_fun thm context = |
98 let |
103 let |
99 val ctxt = Context.proof_of context |
104 val ctxt = Context.proof_of context |
100 val trm = HOLogic.dest_Trueprop (prop_of thm) |
105 val trm = HOLogic.dest_Trueprop (prop_of thm) |
101 in |
106 in |
102 case trm of |
107 case trm of |
103 Const (@{const_name "op ="}, _) $ lhs $ rhs => |
108 Const (@{const_name "op ="}, _) $ lhs $ rhs => |
104 let |
109 let |
105 val thm2 = transform_eq ctxt thm lhs rhs RS @{thm eq_reflection} |
110 val thm' = transform_eq ctxt thm lhs rhs RS @{thm eq_reflection} |
106 in |
111 in |
107 addel_fn (thm, SOME thm2) context |
112 addel_fun thm' context |
108 end |
113 end |
109 | _ => raise (error "only (op=) case implemented yet") |
114 | _ => raise (error "only (op=) case implemented yet") |
110 end |
115 end |
111 |
116 |
112 val eqvt_add = Thm.declaration_attribute (transform add_thm); |
117 val eqvt_add = Thm.declaration_attribute (fn thm => (add_thm thm) o (transform add_raw_thm thm)); |
113 val eqvt_del = Thm.declaration_attribute (transform del_thm); |
118 val eqvt_del = Thm.declaration_attribute (fn thm => (del_thm thm) o (transform del_raw_thm thm)); |
114 |
119 |
115 val eqvt_force_add = Thm.declaration_attribute (add_force_thm o rpair NONE); |
120 val eqvt_raw_add = Thm.declaration_attribute add_raw_thm; |
116 val eqvt_force_del = Thm.declaration_attribute (del_force_thm o rpair NONE); |
121 val eqvt_raw_del = Thm.declaration_attribute del_raw_thm; |
117 |
122 |
118 val setup = |
123 val setup = |
119 Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) |
124 Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) |
120 (cat_lines ["declaration of equivariance lemmas - they will automtically be", |
125 (cat_lines ["declaration of equivariance lemmas - they will automtically be", |
121 "brought into the form p o c = c"]) #> |
126 "brought into the form p o c = c"]) #> |
122 Attrib.setup @{binding "eqvt_force"} (Attrib.add_del eqvt_force_add eqvt_force_del) |
127 Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del) |
123 (cat_lines ["declaration of equivariance lemmas - no", |
128 (cat_lines ["declaration of equivariance lemmas - no", |
124 "transformation is performed"]) #> |
129 "transformation is performed"]) #> |
125 PureThy.add_thms_dynamic (@{binding "eqvts"}, eqvts) #> |
130 PureThy.add_thms_dynamic (@{binding "eqvts"}, eqvts) #> |
126 PureThy.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw); |
131 PureThy.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw); |
127 |
132 |
|
133 |
128 end; |
134 end; |