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_force], and the theorem |
7 list eqvt. In contrast to eqvt-force, the eqvt-lemmas that will be |
7 lists eqvts and eqvts_raw. The first attribute will store the theorem |
8 stored are expected to be of the form |
8 in the eqvts list and also in the eqvts_raw list. For the latter |
|
9 the theorem is expected to be of the form |
9 |
10 |
10 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) ... |
11 |
12 |
12 and are transformed into the form |
13 and is stored in the form |
13 |
14 |
14 p o c == c |
15 p o c == c |
15 |
16 |
16 TODO |
17 The [eqvt_force] attribute just adds the theorem to eqvts. |
17 |
18 |
18 - deal with eqvt-lemmas of the for |
19 TODO: |
|
20 |
|
21 - deal with eqvt-lemmas of the form |
19 |
22 |
20 c x1 x2 ... ==> c (p o x1) (p o x2) .. |
23 c x1 x2 ... ==> c (p o x1) (p o x2) .. |
21 *) |
24 *) |
22 |
25 |
23 signature NOMINAL_THMDECLS = |
26 signature NOMINAL_THMDECLS = |
26 val eqvt_del: attribute |
29 val eqvt_del: attribute |
27 val eqvt_force_add: attribute |
30 val eqvt_force_add: attribute |
28 val eqvt_force_del: attribute |
31 val eqvt_force_del: attribute |
29 val setup: theory -> theory |
32 val setup: theory -> theory |
30 val get_eqvt_thms: Proof.context -> thm list |
33 val get_eqvt_thms: Proof.context -> thm list |
|
34 val get_eqvt_raw_thms: Proof.context -> thm list |
31 |
35 |
32 end; |
36 end; |
33 |
37 |
34 structure Nominal_ThmDecls: NOMINAL_THMDECLS = |
38 structure Nominal_ThmDecls: NOMINAL_THMDECLS = |
35 struct |
39 struct |
36 |
40 |
37 structure EqvtData = Generic_Data |
41 structure EqvtData = Generic_Data |
38 ( |
42 ( |
39 type T = thm Item_Net.T; |
43 type T = (thm * thm option) Item_Net.T; |
40 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) |
41 val extend = I; |
45 val extend = I; |
42 val merge = Item_Net.merge; |
46 val merge = Item_Net.merge; |
43 ); |
47 ); |
44 |
48 |
45 val content = Item_Net.content o EqvtData.get; |
49 val eqvts = (map fst) o Item_Net.content o EqvtData.get; |
46 val get_eqvt_thms = content o Context.Proof; |
50 val eqvts_raw = (map_filter snd) o Item_Net.content o EqvtData.get; |
|
51 |
|
52 val get_eqvt_thms = eqvts o Context.Proof; |
|
53 val get_eqvt_raw_thms = eqvts_raw o Context.Proof; |
47 |
54 |
48 val add_thm = EqvtData.map o Item_Net.update; |
55 val add_thm = EqvtData.map o Item_Net.update; |
49 val del_thm = EqvtData.map o Item_Net.remove; |
56 val del_thm = EqvtData.map o Item_Net.remove; |
50 |
57 |
51 val add_force_thm = EqvtData.map o Item_Net.update; |
58 val add_force_thm = EqvtData.map o Item_Net.update; |
52 val del_force_thm = EqvtData.map o Item_Net.remove; |
59 val del_force_thm = EqvtData.map o Item_Net.remove; |
53 |
|
54 |
60 |
55 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
61 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
56 | dest_perm t = raise TERM("dest_perm", [t]) |
62 | dest_perm t = raise TERM("dest_perm", [t]) |
57 |
63 |
58 fun mk_perm p trm = |
64 fun mk_perm p trm = |
92 let |
98 let |
93 val ctxt = Context.proof_of context |
99 val ctxt = Context.proof_of context |
94 val trm = HOLogic.dest_Trueprop (prop_of thm) |
100 val trm = HOLogic.dest_Trueprop (prop_of thm) |
95 in |
101 in |
96 case trm of |
102 case trm of |
97 Const (@{const_name "op ="}, _) $ lhs $ rhs => |
103 Const (@{const_name "op ="}, _) $ lhs $ rhs => |
98 addel_fn (transform_eq ctxt thm lhs rhs RS @{thm eq_reflection}) context |
104 let |
99 | _ => raise (error "no other cases yet implemented") |
105 val thm2 = transform_eq ctxt thm lhs rhs RS @{thm eq_reflection} |
|
106 in |
|
107 addel_fn (thm, SOME thm2) context |
|
108 end |
|
109 | _ => raise (error "only (op=) case implemented yet") |
100 end |
110 end |
101 |
|
102 |
111 |
103 val eqvt_add = Thm.declaration_attribute (transform add_thm); |
112 val eqvt_add = Thm.declaration_attribute (transform add_thm); |
104 val eqvt_del = Thm.declaration_attribute (transform del_thm); |
113 val eqvt_del = Thm.declaration_attribute (transform del_thm); |
105 |
114 |
106 val eqvt_force_add = Thm.declaration_attribute add_force_thm; |
115 val eqvt_force_add = Thm.declaration_attribute (add_force_thm o rpair NONE); |
107 val eqvt_force_del = Thm.declaration_attribute del_force_thm; |
116 val eqvt_force_del = Thm.declaration_attribute (del_force_thm o rpair NONE); |
108 |
117 |
109 val setup = |
118 val setup = |
110 Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) |
119 Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) |
111 (cat_lines ["declaration of equivariance lemmas - they will automtically be", |
120 (cat_lines ["declaration of equivariance lemmas - they will automtically be", |
112 "brought into the form p o c = c"]) #> |
121 "brought into the form p o c = c"]) #> |
113 Attrib.setup @{binding "eqvt_force"} (Attrib.add_del eqvt_force_add eqvt_force_del) |
122 Attrib.setup @{binding "eqvt_force"} (Attrib.add_del eqvt_force_add eqvt_force_del) |
114 (cat_lines ["declaration of equivariance lemmas - they will will be", |
123 (cat_lines ["declaration of equivariance lemmas - no", |
115 "added/deleted directly to the eqvt thm-list"]) #> |
124 "transformation is performed"]) #> |
116 PureThy.add_thms_dynamic (@{binding "eqvts"}, content); |
125 PureThy.add_thms_dynamic (@{binding "eqvts"}, eqvts) #> |
117 |
126 PureThy.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw); |
118 |
127 |
119 end; |
128 end; |