expand 'split' in direct corecursion as well

--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Thu Feb 06 00:03:12 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Thu Feb 06 00:24:02 2014 +0100
@@ -7,7 +7,7 @@
 
 signature BNF_FP_N2M_SUGAR =
 sig
-  val unfold_let: term -> term
+  val unfold_lets_splits: term -> term
   val dest_map: Proof.context -> string -> term -> term * term list
 
   val mutualize_fp_sugars: BNF_FP_Util.fp_kind -> binding list -> typ list -> (term -> int list) ->
@@ -62,17 +62,18 @@
   Local_Theory.declaration {syntax = false, pervasive = false}
     (fn phi => Data.map (Typtab.default (key, morph_n2m_sugar phi n2m_sugar)));
 
-fun unfold_let (Const (@{const_name Let}, _) $ arg1 $ arg2) = unfold_let (betapply (arg2, arg1))
-  | unfold_let (t as Const (@{const_name prod_case}, _) $ u) =
-    (case unfold_let u of
+fun unfold_lets_splits (Const (@{const_name Let}, _) $ arg1 $ arg2) =
+    unfold_lets_splits (betapply (arg2, arg1))
+  | unfold_lets_splits (t as Const (@{const_name prod_case}, _) $ u) =
+    (case unfold_lets_splits u of
       u' as Abs (s1, T1, Abs (s2, T2, _)) =>
       let val v = Var ((s1 ^ s2, Term.maxidx_of_term u' + 1), HOLogic.mk_prodT (T1, T2)) in
         lambda v (incr_boundvars 1 (betapplys (u', [HOLogic.mk_fst v, HOLogic.mk_snd v])))
       end
     | _ => t)
-  | unfold_let (t $ u) = betapply (unfold_let t, unfold_let u)
-  | unfold_let (Abs (s, T, t)) = Abs (s, T, unfold_let t)
-  | unfold_let t = t;
+  | unfold_lets_splits (t $ u) = betapply (pairself unfold_lets_splits (t, u))
+  | unfold_lets_splits (Abs (s, T, t)) = Abs (s, T, unfold_lets_splits t)
+  | unfold_lets_splits t = t;
 
 fun mk_map_pattern ctxt s =
   let
@@ -255,7 +256,7 @@
     fun indexify_ctr ctr =
       (case AList.lookup Term.aconv_untyped callsss ctr of
         NONE => replicate (num_binder_types (fastype_of ctr)) []
-      | SOME callss => map (map (Envir.beta_eta_contract o unfold_let)) callss);
+      | SOME callss => map (map (Envir.beta_eta_contract o unfold_lets_splits)) callss);
   in
     map indexify_ctr ctrs
   end;

--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Feb 06 00:03:12 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Feb 06 00:24:02 2014 +0100
@@ -149,7 +149,7 @@
 
     fun fld conds t =
       (case Term.strip_comb t of
-        (Const (@{const_name Let}, _), [_, _]) => fld conds (unfold_let t)
+        (Const (@{const_name Let}, _), [_, _]) => fld conds (unfold_lets_splits t)
       | (Const (@{const_name If}, _), [cond, then_branch, else_branch]) =>
         fld (conds @ conjuncts_s cond) then_branch o fld (conds @ s_not_conj [cond]) else_branch
       | (Const (c, _), args as _ :: _ :: _) =>
@@ -190,11 +190,14 @@
     and massage_rec bound_Ts t =
       let val typof = curry fastype_of1 bound_Ts in
         (case Term.strip_comb t of
-          (Const (@{const_name Let}, _), [_, _]) => massage_rec bound_Ts (unfold_let t)
+          (Const (@{const_name Let}, _), [_, _]) => massage_rec bound_Ts (unfold_lets_splits t)
         | (Const (@{const_name If}, _), obj :: (branches as [_, _])) =>
           let val branches' = map (massage_rec bound_Ts) branches in
             Term.list_comb (If_const (typof (hd branches')) $ tap check_no_call obj, branches')
           end
+        | (c as Const (@{const_name prod_case}, _), arg :: args) =>
+          massage_rec bound_Ts
+            (unfold_lets_splits (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args)))
         | (Const (c, _), args as _ :: _ :: _) =>
           (case try strip_fun_type (Sign.the_const_type thy c) of
             SOME (gen_branch_Ts, gen_body_fun_T) =>
@@ -639,7 +642,7 @@
     val (lhs, rhs) = HOLogic.dest_eq concl;
     val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free;
     val SOME basic_ctr_specs = AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name;
-    val (ctr, ctr_args) = strip_comb (unfold_let rhs);
+    val (ctr, ctr_args) = strip_comb (unfold_lets_splits rhs);
     val {disc, sels, ...} = the (find_first (curry (op =) ctr o #ctr) basic_ctr_specs)
       handle Option.Option => primcorec_error_eqn "not a constructor" ctr;
 
@@ -685,7 +688,7 @@
         binder_types (fastype_of ctr)
         |> map_index (fn (n, T) => massage_corec_code_rhs lthy (fn _ => fn ctr' => fn args =>
           if ctr' = ctr then nth args n else Const (@{const_name undefined}, T)) [] rhs')
-        |> curry list_comb ctr
+        |> curry Term.list_comb ctr
         |> curry HOLogic.mk_eq lhs);
 
     val sequentials = replicate (length fun_names) false;
@@ -723,7 +726,7 @@
       ([dissect_coeqn_sel fun_names basic_ctr_specss eqn_pos NONE NONE eqn0 of_spec_opt concl],
        matchedsss)
     else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) then
-      if member (op =) ctrs (head_of (unfold_let (the rhs_opt))) then
+      if member (op =) ctrs (head_of (unfold_lets_splits (the rhs_opt))) then
         dissect_coeqn_ctr fun_names sequentials basic_ctr_specss eqn_pos eqn0
           (if null prems then
              SOME (snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (Logic.strip_assums_concl eqn0))))
@@ -782,9 +785,11 @@
                 if is_Free u andalso has_call u then
                   Inr_const U T $ mk_tuple1 bound_Ts vs
                 else if try (fst o dest_Const) u = SOME @{const_name prod_case} then
-                  map (rewrite bound_Ts) vs |> chop 1 |>> HOLogic.mk_split o the_single |> list_comb
+                  map (rewrite bound_Ts) vs |> chop 1
+                  |>> HOLogic.mk_split o the_single
+                  |> Term.list_comb
                 else
-                  list_comb (rewrite bound_Ts u, map (rewrite bound_Ts) vs)
+                  Term.list_comb (rewrite bound_Ts u, map (rewrite bound_Ts) vs)
               end
             | rewrite _ t =
               if is_Free t andalso has_call t then Inr_const U T $ HOLogic.unit else t;
@@ -854,7 +859,7 @@
             ||> Logic.list_implies
             ||> curry Logic.list_all (map dest_Free fun_args))));
   in
-    map (list_comb o rpair corec_args) corecs
+    map (Term.list_comb o rpair corec_args) corecs
     |> map2 (fn Ts => fn t => if length Ts = 0 then t $ HOLogic.unit else t) arg_Tss
     |> map2 currys arg_Tss
     |> Syntax.check_terms lthy
@@ -905,7 +910,7 @@
   end;
 
 fun applied_fun_of fun_name fun_T fun_args =
-  list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0));
+  Term.list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0));
 
 fun is_trivial_implies thm =
   uncurry (member (op aconv)) (Logic.strip_horn (Thm.prop_of thm));
@@ -1164,7 +1169,7 @@
                   filter (curry (op =) ctr o #ctr) sel_eqns
                   |> fst o finds (op = o apsnd #sel) sels
                   |> map (snd #> (fn [x] => (List.rev (#fun_args x), #rhs_term x)) #-> abstract)
-                  |> curry list_comb ctr)
+                  |> curry Term.list_comb ctr)
                 |> curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args)
                 |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
                 |> curry Logic.list_all (map dest_Free fun_args);
@@ -1219,7 +1224,7 @@
                               |> fst o finds (op = o apsnd #sel) sels
                               |> map (snd #> (fn [x] => (List.rev (#fun_args x), #rhs_term x))
                                 #-> abstract)
-                              |> curry list_comb ctr;
+                              |> curry Term.list_comb ctr;
                           in
                             SOME (prems, t)
                           end;