31 val eqvt_raw_add: attribute |
31 val eqvt_raw_add: attribute |
32 val eqvt_raw_del: attribute |
32 val eqvt_raw_del: attribute |
33 val setup: theory -> theory |
33 val setup: theory -> theory |
34 val get_eqvts_thms: Proof.context -> thm list |
34 val get_eqvts_thms: Proof.context -> thm list |
35 val get_eqvts_raw_thms: Proof.context -> thm list |
35 val get_eqvts_raw_thms: Proof.context -> thm list |
|
36 val eqvt_transform: Proof.context -> thm -> thm |
36 |
37 |
37 (* TEMPORARY FIX *) |
38 (* TEMPORARY FIX *) |
38 val add_thm: thm -> Context.generic -> Context.generic |
39 val add_thm: thm -> Context.generic -> Context.generic |
39 val add_raw_thm: thm -> Context.generic -> Context.generic |
40 val add_raw_thm: thm -> Context.generic -> Context.generic |
40 end; |
41 end; |
85 val add_thm = EqvtData.map o Item_Net.update; |
86 val add_thm = EqvtData.map o Item_Net.update; |
86 val del_thm = EqvtData.map o Item_Net.remove; |
87 val del_thm = EqvtData.map o Item_Net.remove; |
87 |
88 |
88 fun add_raw_thm thm = |
89 fun add_raw_thm thm = |
89 case prop_of thm of |
90 case prop_of thm of |
90 Const ("==", _) $ _ $ _ => EqvtRawData.map (Item_Net.update (zero_var_indexes thm)) |
91 Const ("==", _) $ _ $ _ => |
|
92 EqvtRawData.map (Item_Net.update (zero_var_indexes thm)) |
91 | _ => raise THM ("Theorem must be a meta-equality", 0, [thm]) |
93 | _ => raise THM ("Theorem must be a meta-equality", 0, [thm]) |
92 |
94 |
93 val del_raw_thm = EqvtRawData.map o Item_Net.remove; |
95 val del_raw_thm = EqvtRawData.map o Item_Net.remove; |
94 |
96 |
95 fun eq_transform_tac thm = |
97 |
|
98 (** transformation of eqvt lemmas **) |
|
99 |
|
100 |
|
101 (* transforms equations into the "p o c = c"-form |
|
102 from p o (c x1 ...xn) = c (p o x1) ... (p o xn) *) |
|
103 |
|
104 fun eqvt_transform_eq_tac thm = |
96 let |
105 let |
97 val ss_thms = @{thms permute_minus_cancel permute_prod.simps split_paired_all} |
106 val ss_thms = @{thms permute_minus_cancel permute_prod.simps split_paired_all} |
98 in |
107 in |
99 REPEAT o FIRST' |
108 REPEAT o FIRST' |
100 [CHANGED o simp_tac (HOL_basic_ss addsimps ss_thms), |
109 [CHANGED o simp_tac (HOL_basic_ss addsimps ss_thms), |
101 rtac (thm RS @{thm trans}), |
110 rtac (thm RS @{thm trans}), |
102 rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}] |
111 rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}] |
103 end |
112 end |
104 |
113 |
105 (* transform equations into the "p o c = c"-form *) |
114 fun eqvt_transform_eq ctxt thm = |
106 fun transform_eq ctxt thm = |
|
107 let |
115 let |
108 val ((p, t), rhs) = apfst dest_perm |
116 val ((p, t), rhs) = apfst dest_perm |
109 (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))) |
117 (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))) |
110 handle TERM _ => error "Eqvt lemma is not of the form p \<bullet> c... = c..." |
118 handle TERM _ => error "Eqvt lemma is not of the form p \<bullet> c... = c..." |
111 val ps = get_ps rhs handle TERM _ => [] |
119 val ps = get_ps rhs handle TERM _ => [] |
116 else if is_bad_list (p::ps) |
124 else if is_bad_list (p::ps) |
117 then error "Eqvt lemma is not of the right form (permutations do not agree)" |
125 then error "Eqvt lemma is not of the right form (permutations do not agree)" |
118 else if not (rhs aconv (put_p p t)) |
126 else if not (rhs aconv (put_p p t)) |
119 then error "Eqvt lemma is not of the right form (arguments do not agree)" |
127 then error "Eqvt lemma is not of the right form (arguments do not agree)" |
120 else if is_Const t |
128 else if is_Const t |
121 then thm |
129 then safe_mk_equiv thm |
122 else |
130 else |
123 let |
131 let |
124 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) |
132 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) |
125 val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt |
133 val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt |
126 in |
134 in |
127 Goal.prove ctxt [] [] goal' (fn _ => eq_transform_tac thm 1) |
135 Goal.prove ctxt [] [] goal' (fn _ => eqvt_transform_eq_tac thm 1) |
128 |> singleton (ProofContext.export ctxt' ctxt) |
136 |> singleton (ProofContext.export ctxt' ctxt) |
|
137 |> safe_mk_equiv |
129 end |
138 end |
130 end |
139 end |
131 |
140 |
132 fun imp_transform_tac thy p p' thm = |
141 (* transforms equations into the "p o c = c"-form |
|
142 from R x1 ...xn ==> R (p o x1) ... (p o xn) *) |
|
143 |
|
144 fun eqvt_transform_imp_tac thy p p' thm = |
133 let |
145 let |
134 val cp = Thm.cterm_of thy p |
146 val cp = Thm.cterm_of thy p |
135 val cp' = Thm.cterm_of thy (mk_minus p') |
147 val cp' = Thm.cterm_of thy (mk_minus p') |
136 val thm' = Drule.cterm_instantiate [(cp, cp')] thm |
148 val thm' = Drule.cterm_instantiate [(cp, cp')] thm |
137 val simp = HOL_basic_ss addsimps @{thms permute_minus_cancel(2)} |
149 val simp = HOL_basic_ss addsimps @{thms permute_minus_cancel(2)} |
138 in |
150 in |
139 EVERY' [rtac @{thm iffI}, dtac @{thm permute_boolE}, rtac thm, atac, |
151 EVERY' [rtac @{thm iffI}, dtac @{thm permute_boolE}, rtac thm, atac, |
140 rtac @{thm permute_boolI}, dtac thm', full_simp_tac simp] |
152 rtac @{thm permute_boolI}, dtac thm', full_simp_tac simp] |
141 end |
153 end |
142 |
154 |
143 fun transform_imp ctxt thm = |
155 fun eqvt_transform_imp ctxt thm = |
144 let |
156 let |
145 val thy = ProofContext.theory_of ctxt |
157 val thy = ProofContext.theory_of ctxt |
146 val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm)) |
158 val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm)) |
147 val (c, c') = (head_of prem, head_of concl) |
159 val (c, c') = (head_of prem, head_of concl) |
148 val ps = get_ps concl handle TERM _ => [] |
160 val ps = get_ps concl handle TERM _ => [] |
159 val prem' = mk_perm (the p) prem |
171 val prem' = mk_perm (the p) prem |
160 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl)) |
172 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl)) |
161 val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt |
173 val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt |
162 in |
174 in |
163 Goal.prove ctxt' [] [] goal' |
175 Goal.prove ctxt' [] [] goal' |
164 (fn _ => imp_transform_tac thy (the p) p' thm 1) |
176 (fn _ => eqvt_transform_imp_tac thy (the p) p' thm 1) |
165 |> singleton (ProofContext.export ctxt' ctxt) |
177 |> singleton (ProofContext.export ctxt' ctxt) |
166 |> transform_eq ctxt |
178 |> eqvt_transform_eq ctxt |
167 end |
179 end |
168 end |
180 end |
169 |
181 |
170 fun transform addel_fun thm context = |
182 fun eqvt_transform ctxt thm = |
171 let |
183 case (prop_of thm) of |
172 val ctxt = Context.proof_of context |
184 @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $ |
173 in |
185 (Const (@{const_name "permute"}, _) $ _ $ _) $ _) => |
174 case (prop_of thm) of |
186 eqvt_transform_eq ctxt thm |
175 @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $ |
187 | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) => |
176 (Const (@{const_name "permute"}, _) $ _ $ _) $ _) => |
188 eqvt_transform_imp ctxt thm |
177 addel_fun (safe_mk_equiv (transform_eq ctxt thm)) context |
189 | _ => raise error "Only _ = _ and _ ==> _ cases are implemented." |
178 | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) => |
190 |
179 addel_fun (safe_mk_equiv (transform_imp ctxt thm)) context |
191 |
180 | _ => raise error "Only _ = _ and _ ==> _ cases are implemented." |
192 (** attributes **) |
181 end |
193 |
182 |
194 val eqvt_add = Thm.declaration_attribute |
183 val eqvt_add = Thm.declaration_attribute (fn thm => (add_thm thm) o (transform add_raw_thm thm)); |
195 (fn thm => fn context => |
184 val eqvt_del = Thm.declaration_attribute (fn thm => (del_thm thm) o (transform del_raw_thm thm)); |
196 let |
|
197 val thm' = eqvt_transform (Context.proof_of context) thm |
|
198 in |
|
199 context |> add_thm thm |> add_raw_thm thm' |
|
200 end) |
|
201 |
|
202 val eqvt_del = Thm.declaration_attribute |
|
203 (fn thm => fn context => |
|
204 let |
|
205 val thm' = eqvt_transform (Context.proof_of context) thm |
|
206 in |
|
207 context |> del_thm thm |> del_raw_thm thm' |
|
208 end) |
185 |
209 |
186 val eqvt_raw_add = Thm.declaration_attribute add_raw_thm; |
210 val eqvt_raw_add = Thm.declaration_attribute add_raw_thm; |
187 val eqvt_raw_del = Thm.declaration_attribute del_raw_thm; |
211 val eqvt_raw_del = Thm.declaration_attribute del_raw_thm; |
|
212 |
|
213 |
|
214 (** setup function **) |
188 |
215 |
189 val setup = |
216 val setup = |
190 Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) |
217 Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) |
191 (cat_lines ["Declaration of equivariance lemmas - they will automtically be", |
218 (cat_lines ["Declaration of equivariance lemmas - they will automtically be", |
192 "brought into the form p o c == c"]) #> |
219 "brought into the form p o c == c"]) #> |