equal
deleted
inserted
replaced
212 fun resolve f_def = |
212 fun resolve f_def = |
213 let |
213 let |
214 val ctrm2 = f_def |
214 val ctrm2 = f_def |
215 |> cprop_of |
215 |> cprop_of |
216 |> Thm.dest_equals_lhs |
216 |> Thm.dest_equals_lhs |
|
217 val _ = tracing ("ctrm1:\n" ^ @{make_string} ctrm1) |
|
218 val _ = tracing ("ctrm2:\n" ^ @{make_string} ctrm2) |
217 in |
219 in |
218 eqvt_thm |
220 eqvt_thm |
219 |> Thm.instantiate (Thm.match (ctrm1, ctrm2)) |
221 |> Thm.instantiate (Thm.match (ctrm1, ctrm2)) |
220 |> simplify (HOL_basic_ss addsimps (@{thm Pair_eqvt} :: @{thms permute_sum.simps})) |
222 |> simplify (HOL_basic_ss addsimps (@{thm Pair_eqvt} :: @{thms permute_sum.simps})) |
221 |> Local_Defs.unfold ctxt [f_def] |
223 |> Local_Defs.unfold ctxt [f_def] |