60 sig |
60 sig |
61 val eqvt_add: attribute |
61 val eqvt_add: attribute |
62 val eqvt_del: attribute |
62 val eqvt_del: attribute |
63 val eqvt_raw_add: attribute |
63 val eqvt_raw_add: attribute |
64 val eqvt_raw_del: attribute |
64 val eqvt_raw_del: attribute |
65 val setup: theory -> theory |
|
66 val get_eqvts_thms: Proof.context -> thm list |
65 val get_eqvts_thms: Proof.context -> thm list |
67 val get_eqvts_raw_thms: Proof.context -> thm list |
66 val get_eqvts_raw_thms: Proof.context -> thm list |
68 val eqvt_transform: Proof.context -> thm -> thm |
67 val eqvt_transform: Proof.context -> thm -> thm |
69 val is_eqvt: Proof.context -> term -> bool |
68 val is_eqvt: Proof.context -> term -> bool |
70 end; |
69 end; |
89 val merge = Termtab.merge (K true)); |
88 val merge = Termtab.merge (K true)); |
90 |
89 |
91 val eqvts = Item_Net.content o EqvtData.get |
90 val eqvts = Item_Net.content o EqvtData.get |
92 val eqvts_raw = map snd o Termtab.dest o EqvtRawData.get |
91 val eqvts_raw = map snd o Termtab.dest o EqvtRawData.get |
93 |
92 |
|
93 val _ = |
|
94 Theory.setup |
|
95 (Global_Theory.add_thms_dynamic (@{binding "eqvts"}, eqvts) #> |
|
96 Global_Theory.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw)) |
|
97 |
94 val get_eqvts_thms = eqvts o Context.Proof |
98 val get_eqvts_thms = eqvts o Context.Proof |
95 val get_eqvts_raw_thms = eqvts_raw o Context.Proof |
99 val get_eqvts_raw_thms = eqvts_raw o Context.Proof |
96 |
100 |
97 |
101 |
98 (** raw equivariance lemmas **) |
102 (** raw equivariance lemmas **) |
107 fun key_of_raw_thm context thm = |
111 fun key_of_raw_thm context thm = |
108 let |
112 let |
109 fun error_msg () = |
113 fun error_msg () = |
110 error |
114 error |
111 ("Theorem must be of the form \"?p \<bullet> c \<equiv> c\", with c a constant or fixed parameter:\n" ^ |
115 ("Theorem must be of the form \"?p \<bullet> c \<equiv> c\", with c a constant or fixed parameter:\n" ^ |
112 Syntax.string_of_term (Context.proof_of context) (prop_of thm)) |
116 Syntax.string_of_term (Context.proof_of context) (Thm.prop_of thm)) |
113 in |
117 in |
114 case prop_of thm of |
118 case Thm.prop_of thm of |
115 Const (@{const_name Pure.eq}, _) $ (Const (@{const_name "permute"}, _) $ p $ c) $ c' => |
119 Const (@{const_name Pure.eq}, _) $ (Const (@{const_name "permute"}, _) $ p $ c) $ c' => |
116 if is_Var p andalso is_fixed (Context.proof_of context) c andalso c aconv c' then |
120 if is_Var p andalso is_fixed (Context.proof_of context) c andalso c aconv c' then |
117 c |
121 c |
118 else |
122 else |
119 error_msg () |
123 error_msg () |
149 |
153 |
150 fun add_thm thm context = |
154 fun add_thm thm context = |
151 ( |
155 ( |
152 if Item_Net.member (EqvtData.get context) thm then |
156 if Item_Net.member (EqvtData.get context) thm then |
153 warning ("Theorem already declared as equivariant:\n" ^ |
157 warning ("Theorem already declared as equivariant:\n" ^ |
154 Syntax.string_of_term (Context.proof_of context) (prop_of thm)) |
158 Syntax.string_of_term (Context.proof_of context) (Thm.prop_of thm)) |
155 else (); |
159 else (); |
156 EqvtData.map (Item_Net.update thm) context |
160 EqvtData.map (Item_Net.update thm) context |
157 ) |
161 ) |
158 |
162 |
159 fun del_thm thm context = |
163 fun del_thm thm context = |
160 ( |
164 ( |
161 if Item_Net.member (EqvtData.get context) thm then |
165 if Item_Net.member (EqvtData.get context) thm then |
162 EqvtData.map (Item_Net.remove thm) context |
166 EqvtData.map (Item_Net.remove thm) context |
163 else ( |
167 else ( |
164 warning ("Cannot delete non-existing equivariance theorem:\n" ^ |
168 warning ("Cannot delete non-existing equivariance theorem:\n" ^ |
165 Syntax.string_of_term (Context.proof_of context) (prop_of thm)); |
169 Syntax.string_of_term (Context.proof_of context) (Thm.prop_of thm)); |
166 context |
170 context |
167 ) |
171 ) |
168 ) |
172 ) |
169 |
173 |
170 |
174 |
185 |
189 |
186 in |
190 in |
187 |
191 |
188 fun thm_4_of_1 ctxt thm = |
192 fun thm_4_of_1 ctxt thm = |
189 let |
193 let |
190 val (p, c) = thm |> prop_of |> HOLogic.dest_Trueprop |
194 val (p, c) = thm |> Thm.prop_of |> HOLogic.dest_Trueprop |
191 |> HOLogic.dest_eq |> fst |> dest_perm ||> fst o (fixed_nonfixed_args ctxt) |
195 |> HOLogic.dest_eq |> fst |> dest_perm ||> fst o (fixed_nonfixed_args ctxt) |
192 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) |
196 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) |
193 val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt |
197 val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt |
194 in |
198 in |
195 Goal.prove ctxt [] [] goal' (fn {context, ...} => tac context thm 1) |
199 Goal.prove ctxt [] [] goal' (fn {context, ...} => tac context thm 1) |
207 |
211 |
208 fun tac ctxt thm thm' = |
212 fun tac ctxt thm thm' = |
209 let |
213 let |
210 val ss_thms = @{thms "permute_minus_cancel"(2)} |
214 val ss_thms = @{thms "permute_minus_cancel"(2)} |
211 in |
215 in |
212 EVERY' [rtac @{thm "iffI"}, dtac @{thm "permute_boolE"}, rtac thm, atac, |
216 EVERY' [rtac @{thm "iffI"}, dtac @{thm "permute_boolE"}, rtac thm, assume_tac ctxt, |
213 rtac @{thm "permute_boolI"}, dtac thm', |
217 rtac @{thm "permute_boolI"}, dtac thm', |
214 full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss_thms)] |
218 full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss_thms)] |
215 end |
219 end |
216 |
220 |
217 in |
221 in |
218 |
222 |
219 fun thm_1_of_2 ctxt thm = |
223 fun thm_1_of_2 ctxt thm = |
220 let |
224 let |
221 val (prem, concl) = thm |> prop_of |> Logic.dest_implies |> pairself HOLogic.dest_Trueprop |
225 val (prem, concl) = thm |> Thm.prop_of |> Logic.dest_implies |> apply2 HOLogic.dest_Trueprop |
222 (* since argument terms "?p \<bullet> ?x1" may actually be eta-expanded |
226 (* since argument terms "?p \<bullet> ?x1" may actually be eta-expanded |
223 or tuples, we need the following function to find ?p *) |
227 or tuples, we need the following function to find ?p *) |
224 fun find_perm (Const (@{const_name "permute"}, _) $ (p as Var _) $ _) = p |
228 fun find_perm (Const (@{const_name "permute"}, _) $ (p as Var _) $ _) = p |
225 | find_perm (Const (@{const_name "Pair"}, _) $ x $ _) = find_perm x |
229 | find_perm (Const (@{const_name "Pair"}, _) $ x $ _) = find_perm x |
226 | find_perm (Abs (_, _, body)) = find_perm body |
230 | find_perm (Abs (_, _, body)) = find_perm body |
227 | find_perm _ = raise THM ("thm_3_of_2", 0, [thm]) |
231 | find_perm _ = raise THM ("thm_3_of_2", 0, [thm]) |
228 val p = concl |> dest_comb |> snd |> find_perm |
232 val p = concl |> dest_comb |> snd |> find_perm |
229 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p prem, concl)) |
233 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p prem, concl)) |
230 val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt |
234 val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt |
231 val certify = cterm_of (theory_of_thm thm) |
235 val thm' = Drule.cterm_instantiate [apply2 (Thm.cterm_of ctxt') (p, mk_minus p')] thm |
232 val thm' = Drule.cterm_instantiate [(certify p, certify (mk_minus p'))] thm |
236 in |
233 in |
237 Goal.prove ctxt' [] [] goal' (fn {context = ctxt'', ...} => tac ctxt'' thm thm' 1) |
234 Goal.prove ctxt' [] [] goal' (fn {context, ...} => tac context thm thm' 1) |
|
235 |> singleton (Proof_Context.export ctxt' ctxt) |
238 |> singleton (Proof_Context.export ctxt' ctxt) |
236 end |
239 end |
237 handle TERM _ => |
240 handle TERM _ => |
238 raise THM ("thm_1_of_2", 0, [thm]) |
241 raise THM ("thm_1_of_2", 0, [thm]) |
239 |
242 |
266 (* Transforms a theorem of the form (1) into theorems of the |
269 (* Transforms a theorem of the form (1) into theorems of the |
267 form (1) (or, if c is a relation with arity >= 1, of the form |
270 form (1) (or, if c is a relation with arity >= 1, of the form |
268 (3)) and (4); transforms a theorem of the form (2) into |
271 (3)) and (4); transforms a theorem of the form (2) into |
269 theorems of the form (3) and (4). *) |
272 theorems of the form (3) and (4). *) |
270 fun eqvt_and_raw_transform ctxt thm = |
273 fun eqvt_and_raw_transform ctxt thm = |
271 (case prop_of thm of @{const "Trueprop"} $ (Const (@{const_name "HOL.eq"}, _) $ _ $ c_args) => |
274 (case Thm.prop_of thm of @{const "Trueprop"} $ (Const (@{const_name "HOL.eq"}, _) $ _ $ c_args) => |
272 let |
275 let |
273 val th' = |
276 val th' = |
274 if fastype_of c_args = @{typ "bool"} |
277 if fastype_of c_args = @{typ "bool"} |
275 andalso (not o null) (snd (fixed_nonfixed_args ctxt c_args)) then |
278 andalso (not o null) (snd (fixed_nonfixed_args ctxt c_args)) then |
276 thm_3_of_1 ctxt thm |
279 thm_3_of_1 ctxt thm |
308 end) |
311 end) |
309 |
312 |
310 val eqvt_add = eqvt_add_or_del add_thm add_raw_thm |
313 val eqvt_add = eqvt_add_or_del add_thm add_raw_thm |
311 val eqvt_del = eqvt_add_or_del del_thm del_raw_thm |
314 val eqvt_del = eqvt_add_or_del del_thm del_raw_thm |
312 |
315 |
313 |
316 val _ = |
314 (** setup function **) |
317 Theory.setup |
315 |
318 (Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) |
316 val setup = |
319 "Declaration of equivariance lemmas - they will automatically be brought into the form ?p \<bullet> c \<equiv> c" #> |
317 Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) |
320 Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del) |
318 "Declaration of equivariance lemmas - they will automatically be brought into the form ?p \<bullet> c \<equiv> c" #> |
321 "Declaration of raw equivariance lemmas - no transformation is performed") |
319 Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del) |
|
320 "Declaration of raw equivariance lemmas - no transformation is performed" #> |
|
321 Global_Theory.add_thms_dynamic (@{binding "eqvts"}, eqvts) #> |
|
322 Global_Theory.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw) |
|
323 |
322 |
324 end; |
323 end; |