--- a/src/HOL/Tools/Function/partial_function.ML Tue Dec 03 02:51:20 2013 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML Thu Dec 05 09:20:32 2013 +0100
@@ -168,6 +168,9 @@
simpset_of (put_simpset HOL_basic_ss @{context}
addsimps [@{thm Product_Type.split_conv}]);
+val curry_K_ss =
+ simpset_of (put_simpset HOL_basic_ss @{context}
+ addsimps [@{thm Product_Type.curry_K}]);
(* instantiate generic fixpoint induction and eliminate the canonical assumptions;
curry induction predicate *)
@@ -181,7 +184,8 @@
|> cterm_instantiate' [SOME (cert uncurry), NONE, SOME (cert curry), NONE, SOME (cert P_inst)]
|> Tactic.rule_by_tactic ctxt
(Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 3 (* discharge U (C f) = f *)
- THEN Simplifier.full_simp_tac (put_simpset curry_uncurry_ss ctxt) 4) (* simplify induction step *)
+ THEN Simplifier.simp_tac (put_simpset curry_K_ss ctxt) 4 (* simplify bot case *)
+ THEN Simplifier.full_simp_tac (put_simpset curry_uncurry_ss ctxt) 5) (* simplify induction step *)
|> (fn thm => thm OF [mono_thm, f_def])
|> Conv.fconv_rule (Conv.concl_conv ~1 (* simplify conclusion *)
(Raw_Simplifier.rewrite false [mk_meta_eq @{thm Product_Type.curry_split}]))