equal
deleted
inserted
replaced
171 (** transformation of equivariance lemmas **) |
171 (** transformation of equivariance lemmas **) |
172 |
172 |
173 (* Transforms a theorem of the form (1) into the form (4). *) |
173 (* Transforms a theorem of the form (1) into the form (4). *) |
174 local |
174 local |
175 |
175 |
176 fun tac thm = |
176 fun tac ctxt thm = |
177 let |
177 let |
178 val ss_thms = @{thms "permute_minus_cancel" "permute_prod.simps" "split_paired_all"} |
178 val ss_thms = @{thms "permute_minus_cancel" "permute_prod.simps" "split_paired_all"} |
179 in |
179 in |
180 REPEAT o FIRST' |
180 REPEAT o FIRST' |
181 [CHANGED o simp_tac (HOL_basic_ss addsimps ss_thms), |
181 [CHANGED o simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss_thms), |
182 rtac (thm RS @{thm "trans"}), |
182 rtac (thm RS @{thm "trans"}), |
183 rtac @{thm "trans"[OF "permute_fun_def"]} THEN' rtac @{thm "ext"}] |
183 rtac @{thm "trans"[OF "permute_fun_def"]} THEN' rtac @{thm "ext"}] |
184 end |
184 end |
185 |
185 |
186 in |
186 in |
190 val (p, c) = thm |> prop_of |> HOLogic.dest_Trueprop |
190 val (p, c) = thm |> prop_of |> HOLogic.dest_Trueprop |
191 |> HOLogic.dest_eq |> fst |> dest_perm ||> fst o (fixed_nonfixed_args ctxt) |
191 |> 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)) |
192 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 |
193 val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt |
194 in |
194 in |
195 Goal.prove ctxt [] [] goal' (fn _ => tac thm 1) |
195 Goal.prove ctxt [] [] goal' (fn {context, ...} => tac context thm 1) |
196 |> singleton (Proof_Context.export ctxt' ctxt) |
196 |> singleton (Proof_Context.export ctxt' ctxt) |
197 |> (fn th => th RS @{thm "eq_reflection"}) |
197 |> (fn th => th RS @{thm "eq_reflection"}) |
198 |> zero_var_indexes |
198 |> zero_var_indexes |
199 end |
199 end |
200 handle TERM _ => |
200 handle TERM _ => |
203 end (* local *) |
203 end (* local *) |
204 |
204 |
205 (* Transforms a theorem of the form (2) into the form (1). *) |
205 (* Transforms a theorem of the form (2) into the form (1). *) |
206 local |
206 local |
207 |
207 |
208 fun tac thm thm' = |
208 fun tac ctxt thm thm' = |
209 let |
209 let |
210 val ss_thms = @{thms "permute_minus_cancel"(2)} |
210 val ss_thms = @{thms "permute_minus_cancel"(2)} |
211 in |
211 in |
212 EVERY' [rtac @{thm "iffI"}, dtac @{thm "permute_boolE"}, rtac thm, atac, |
212 EVERY' [rtac @{thm "iffI"}, dtac @{thm "permute_boolE"}, rtac thm, atac, |
213 rtac @{thm "permute_boolI"}, dtac thm', full_simp_tac (HOL_basic_ss addsimps ss_thms)] |
213 rtac @{thm "permute_boolI"}, dtac thm', |
|
214 full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss_thms)] |
214 end |
215 end |
215 |
216 |
216 in |
217 in |
217 |
218 |
218 fun thm_1_of_2 ctxt thm = |
219 fun thm_1_of_2 ctxt thm = |
228 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p prem, concl)) |
229 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p prem, concl)) |
229 val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt |
230 val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt |
230 val certify = cterm_of (theory_of_thm thm) |
231 val certify = cterm_of (theory_of_thm thm) |
231 val thm' = Drule.cterm_instantiate [(certify p, certify (mk_minus p'))] thm |
232 val thm' = Drule.cterm_instantiate [(certify p, certify (mk_minus p'))] thm |
232 in |
233 in |
233 Goal.prove ctxt' [] [] goal' (fn _ => tac thm thm' 1) |
234 Goal.prove ctxt' [] [] goal' (fn {context, ...} => tac context thm thm' 1) |
234 |> singleton (Proof_Context.export ctxt' ctxt) |
235 |> singleton (Proof_Context.export ctxt' ctxt) |
235 end |
236 end |
236 handle TERM _ => |
237 handle TERM _ => |
237 raise THM ("thm_1_of_2", 0, [thm]) |
238 raise THM ("thm_1_of_2", 0, [thm]) |
238 |
239 |