154 let |
154 let |
155 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) |
155 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) |
156 val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt |
156 val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt |
157 in |
157 in |
158 Goal.prove ctxt [] [] goal' (fn _ => eqvt_transform_eq_tac thm 1) |
158 Goal.prove ctxt [] [] goal' (fn _ => eqvt_transform_eq_tac thm 1) |
159 |> singleton (ProofContext.export ctxt' ctxt) |
159 |> singleton (Proof_Context.export ctxt' ctxt) |
160 |> safe_mk_equiv |
160 |> safe_mk_equiv |
161 |> zero_var_indexes |
161 |> zero_var_indexes |
162 end |
162 end |
163 end |
163 end |
164 |
164 |
165 (* transforms equations into the "p o c == c"-form |
165 (* transforms equations into the "p o c == c"-form |
166 from R x1 ...xn ==> R (p o x1) ... (p o xn) *) |
166 from R x1 ...xn ==> R (p o x1) ... (p o xn) *) |
167 |
167 |
168 fun eqvt_transform_imp_tac ctxt p p' thm = |
168 fun eqvt_transform_imp_tac ctxt p p' thm = |
169 let |
169 let |
170 val thy = ProofContext.theory_of ctxt |
170 val thy = Proof_Context.theory_of ctxt |
171 val cp = Thm.cterm_of thy p |
171 val cp = Thm.cterm_of thy p |
172 val cp' = Thm.cterm_of thy (mk_minus p') |
172 val cp' = Thm.cterm_of thy (mk_minus p') |
173 val thm' = Drule.cterm_instantiate [(cp, cp')] thm |
173 val thm' = Drule.cterm_instantiate [(cp, cp')] thm |
174 val simp = HOL_basic_ss addsimps @{thms permute_minus_cancel(2)} |
174 val simp = HOL_basic_ss addsimps @{thms permute_minus_cancel(2)} |
175 in |
175 in |
197 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl)) |
197 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl)) |
198 val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt |
198 val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt |
199 in |
199 in |
200 Goal.prove ctxt' [] [] goal' |
200 Goal.prove ctxt' [] [] goal' |
201 (fn _ => eqvt_transform_imp_tac ctxt' (the p) p' thm 1) |
201 (fn _ => eqvt_transform_imp_tac ctxt' (the p) p' thm 1) |
202 |> singleton (ProofContext.export ctxt' ctxt) |
202 |> singleton (Proof_Context.export ctxt' ctxt) |
203 end |
203 end |
204 end |
204 end |
205 |
205 |
206 fun eqvt_transform ctxt thm = |
206 fun eqvt_transform ctxt thm = |
207 case (prop_of thm) of |
207 case (prop_of thm) of |