# HG changeset patch
# User blanchet
# Date 1407851339 -7200
# Node ID a85e0ab840c1922193ca0a3a427e42d62b97264b
# Parent  6c992a4bcfbd9c839dc74d934244b27c3ef2df6b
less aggressive unfolding; removed debugging;

diff -r 6c992a4bcfbd -r a85e0ab840c1 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Aug 12 12:32:05 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Aug 12 15:48:59 2014 +0200
@@ -8,6 +8,7 @@
 signature BNF_FP_N2M_SUGAR =
 sig
   val unfold_lets_splits: term -> term
+  val unfold_splits_lets: term -> term
   val dest_map: Proof.context -> string -> term -> term * term list
 
   val mutualize_fp_sugars: BNF_Util.fp_kind -> int list -> binding list -> typ list -> term list ->
@@ -60,18 +61,21 @@
   Local_Theory.declaration {syntax = false, pervasive = false}
     (fn phi => Data.map (Typtab.update (key, morph_n2m_sugar phi n2m_sugar)));
 
-fun unfold_lets_splits (Const (@{const_name Let}, _) $ arg1 $ arg2) =
-    unfold_lets_splits (betapply (arg2, arg1))
-  | unfold_lets_splits (t as Const (@{const_name case_prod}, _) $ u) =
-    (case unfold_lets_splits u of
+fun unfold_lets_splits (Const (@{const_name Let}, _) $ t $ u) =
+    unfold_lets_splits (betapply (u, unfold_splits_lets t))
+  | unfold_lets_splits (t $ u) = betapply (unfold_lets_splits t, unfold_lets_splits u)
+  | unfold_lets_splits (Abs (s, T, t)) = Abs (s, T, unfold_lets_splits t)
+  | unfold_lets_splits t = t
+and unfold_splits_lets (t as Const (@{const_name case_prod}, _) $ u) =
+    (case unfold_splits_lets 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_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;
+  | unfold_splits_lets (t $ u) = betapply (unfold_lets_splits t, u)
+  | unfold_splits_lets (Abs (s, T, t)) = Abs (s, T, unfold_splits_lets t)
+  | unfold_splits_lets t = unfold_lets_splits t;
 
 fun mk_map_pattern ctxt s =
   let
diff -r 6c992a4bcfbd -r a85e0ab840c1 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Aug 12 12:32:05 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Aug 12 15:48:59 2014 +0200
@@ -198,7 +198,7 @@
           end
         | (c as Const (@{const_name case_prod}, _), arg :: args) =>
           massage_rec bound_Ts
-            (unfold_lets_splits (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args)))
+            (unfold_splits_lets (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) =>
@@ -694,14 +694,6 @@
         handle ListPair.UnequalLengths =>
           primcorec_error_eqn "partially applied constructor in right-hand side" rhs;
 
-(*
-val _ = tracing ("reduced\n    " ^ Syntax.string_of_term @{context} concl ^ "\nto\n    \<cdot> " ^
- (is_some eqn_data_disc_opt ? K (Syntax.string_of_term @{context} disc_concl ^ "\n    \<cdot> ")) "" ^
- space_implode "\n    \<cdot> " (map (Syntax.string_of_term @{context}) sel_concls) ^
- "\nfor premise(s)\n    \<cdot> " ^
- space_implode "\n    \<cdot> " (map (Syntax.string_of_term @{context}) prems));
-*)
-
     val eqns_data_sel =
       map (dissect_coeqn_sel lthy fun_names basic_ctr_specss eqn_pos
         (SOME (abstract (List.rev fun_args) rhs)) code_rhs_opt eqn0 (SOME ctr)) sel_concls;
@@ -890,11 +882,6 @@
       | currys Ts t = t $ mk_tuple1_balanced (List.rev Ts) (map Bound (length Ts - 1 downto 0))
           |> fold_rev (Term.abs o pair Name.uu) Ts;
 
-(*
-val _ = tracing ("corecursor arguments:\n    \<cdot> " ^
- space_implode "\n    \<cdot> " (map (Syntax.string_of_term lthy) corec_args));
-*)
-
     val excludess' =
       disc_eqnss
       |> map (map (fn x => (#fun_args x, #ctr_no x, #prems x, #auto_gen x))
@@ -1006,10 +993,6 @@
       |> map2 (curry (op |>)) (map (map (fn {ctr, sels, ...} =>
         (ctr, map (K []) sels))) basic_ctr_specss);
 
-(*
-val _ = tracing ("callssss = " ^ @{make_string} callssss);
-*)
-
     val ((n2m, corec_specs', _, coinduct_thm, strong_coinduct_thm, coinduct_thms,
           strong_coinduct_thms), lthy') =
       corec_specs_of bs arg_Ts res_Ts frees callssss lthy;
@@ -1051,11 +1034,6 @@
       else
         tac_opt;
 
-(*
-val _ = tracing ("exclusiveness properties:\n    \<cdot> " ^
- space_implode "\n    \<cdot> " (maps (map (Syntax.string_of_term lthy o snd)) excludess'));
-*)
-
     val excludess'' = map3 (fn tac_opt => fn sequential => map (fn (j, goal) =>
         (j, (Option.map (Goal.prove_sorry lthy [] [] goal #> Thm.close_derivation)
            (exclude_tac tac_opt sequential j), goal))))