178 Conv.implies_conv split_paired_all_conv Conv.all_conv) |
178 Conv.implies_conv split_paired_all_conv Conv.all_conv) |
179 |
179 |
180 val inst_rule = |
180 val inst_rule = |
181 cterm_instantiate' [SOME cuncurry, NONE, SOME ccurry] rule |
181 cterm_instantiate' [SOME cuncurry, NONE, SOME ccurry] rule |
182 |
182 |
183 val P_rangeT = |
183 val (P_var, x_var) = |
184 Thm.prop_of inst_rule |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |
184 Thm.prop_of inst_rule |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |
185 |> Term.head_of |> Term.dest_Var |> snd |> range_type |
185 |> strip_comb |> apsnd hd |
|
186 val P_rangeT = range_type (snd (Term.dest_Var P_var)) |
186 val PT = map (snd o dest_Free) args ---> P_rangeT |
187 val PT = map (snd o dest_Free) args ---> P_rangeT |
187 val x_inst = cert (foldl1 HOLogic.mk_prod args) |
188 val x_inst = cert (foldl1 HOLogic.mk_prod args) |
188 val P_inst = cert (uncurry_n (length args) (Free (P, PT))) |
189 val P_inst = cert (uncurry_n (length args) (Free (P, PT))) |
189 |
190 |
190 val inst_rule' = inst_rule |
191 val inst_rule' = inst_rule |
191 |> Tactic.rule_by_tactic ctxt |
192 |> Tactic.rule_by_tactic ctxt |
192 (Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 4 |
193 (Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 4 |
193 THEN Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 3 |
194 THEN Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 3 |
194 THEN CONVERSION (split_params_conv ctxt |
195 THEN CONVERSION (split_params_conv ctxt |
195 then_conv (Conv.forall_conv (K split_paired_all_conv) ctxt)) 3) |
196 then_conv (Conv.forall_conv (K split_paired_all_conv) ctxt)) 3) |
196 |> Drule.instantiate' [] [NONE, NONE, SOME P_inst, SOME x_inst] |
197 |> Thm.instantiate ([], [(cert P_var, P_inst), (cert x_var, x_inst)]) |
197 |> Simplifier.full_simplify (put_simpset split_conv_ss ctxt) |
198 |> Simplifier.full_simplify (put_simpset split_conv_ss ctxt) |
198 |> singleton (Variable.export ctxt' ctxt) |
199 |> singleton (Variable.export ctxt' ctxt) |
199 in |
200 in |
200 inst_rule' |
201 inst_rule' |
201 end; |
202 end; |