# HG changeset patch
# User blanchet
# Date 1394198475 -3600
# Node ID 8820ddb8f9f422cf8efb6e3c084f0c74561141df
# Parent  94242fa87638c2afc8e29d466d98e302fa256264
use balanced tuples in 'primcorec'

diff -r 94242fa87638 -r 8820ddb8f9f4 src/HOL/String.thy
--- a/src/HOL/String.thy	Fri Mar 07 14:21:15 2014 +0100
+++ b/src/HOL/String.thy	Fri Mar 07 14:21:15 2014 +0100
@@ -3,7 +3,7 @@
 header {* Character and string types *}
 
 theory String
-imports List Enum
+imports Enum
 begin
 
 subsection {* Characters and strings *}
@@ -443,4 +443,3 @@
 hide_type (open) literal
 
 end
-
diff -r 94242fa87638 -r 8820ddb8f9f4 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Mar 07 14:21:15 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Mar 07 14:21:15 2014 +0100
@@ -128,6 +128,7 @@
   val split_conj_prems: int -> thm -> thm
 
   val mk_sumTN: typ list -> typ
+  val mk_tupleT_balanced: typ list -> typ
   val mk_sumprodT_balanced: typ list list -> typ
 
   val mk_proj: typ -> int -> int -> term
@@ -136,6 +137,8 @@
 
   val Inl_const: typ -> typ -> term
   val Inr_const: typ -> typ -> term
+  val mk_tuple_balanced: term list -> term
+  val mk_tuple1_balanced: typ list -> term list -> term
 
   val mk_case_sum: term * term -> term
   val mk_case_sumN: term list -> term
@@ -373,8 +376,13 @@
 fun Inr_const LT RT = Const (@{const_name Inr}, RT --> mk_sumT (LT, RT));
 fun mk_Inr LT t = Inr_const LT (fastype_of t) $ t;
 
-fun mk_tuple_balanced [] = HOLogic.unit
-  | mk_tuple_balanced ts = Balanced_Tree.make HOLogic.mk_prod ts;
+fun mk_prod1 bound_Ts (t, u) =
+  HOLogic.pair_const (fastype_of1 (bound_Ts, t)) (fastype_of1 (bound_Ts, u)) $ t $ u;
+
+fun mk_tuple1_balanced _ [] = HOLogic.unit
+  | mk_tuple1_balanced bound_Ts ts = Balanced_Tree.make (mk_prod1 bound_Ts) ts;
+
+val mk_tuple_balanced = mk_tuple1_balanced [];
 
 fun mk_absumprod absT abs0 n k ts =
   let val abs = mk_abs absT abs0;
diff -r 94242fa87638 -r 8820ddb8f9f4 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Mar 07 14:21:15 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Mar 07 14:21:15 2014 +0100
@@ -477,7 +477,7 @@
 
 val undef_const = Const (@{const_name undefined}, dummyT);
 
-val abs_tuple = HOLogic.tupled_lambda o HOLogic.mk_tuple;
+val abs_tuple_balanced = HOLogic.tupled_lambda o mk_tuple_balanced;
 
 fun abstract vs =
   let
@@ -489,10 +489,6 @@
         end;
   in abs 0 end;
 
-fun mk_prod1 bound_Ts (t, u) =
-  HOLogic.pair_const (fastype_of1 (bound_Ts, t)) (fastype_of1 (bound_Ts, u)) $ t $ u;
-fun mk_tuple1 bound_Ts = the_default HOLogic.unit o try (foldr1 (mk_prod1 bound_Ts));
-
 type coeqn_data_disc = {
   fun_name: string,
   fun_T: typ,
@@ -734,12 +730,12 @@
   if is_none (#pred (nth ctr_specs ctr_no)) then I else
     s_conjs prems
     |> curry subst_bounds (List.rev fun_args)
-    |> HOLogic.tupled_lambda (HOLogic.mk_tuple fun_args)
+    |> abs_tuple_balanced fun_args
     |> K |> nth_map (the (#pred (nth ctr_specs ctr_no)));
 
 fun build_corec_arg_no_call (sel_eqns : coeqn_data_sel list) sel =
   find_first (curry (op =) sel o #sel) sel_eqns
-  |> try (fn SOME {fun_args, rhs_term, ...} => abs_tuple fun_args rhs_term)
+  |> try (fn SOME {fun_args, rhs_term, ...} => abs_tuple_balanced fun_args rhs_term)
   |> the_default undef_const
   |> K;
 
@@ -752,9 +748,9 @@
       fun rewrite_stop _ t = if has_call t then @{term False} else @{term True};
       fun rewrite_end _ t = if has_call t then undef_const else t;
       fun rewrite_cont bound_Ts t =
-        if has_call t then mk_tuple1 bound_Ts (snd (strip_comb t)) else undef_const;
+        if has_call t then mk_tuple1_balanced bound_Ts (snd (strip_comb t)) else undef_const;
       fun massage f _ = massage_let_if_case lthy has_call f bound_Ts rhs_term
-        |> abs_tuple fun_args;
+        |> abs_tuple_balanced fun_args;
     in
       (massage rewrite_stop, massage rewrite_end, massage rewrite_cont)
     end);
@@ -770,7 +766,7 @@
             | rewrite bound_Ts (t as _ $ _) =
               let val (u, vs) = strip_comb t in
                 if is_Free u andalso has_call u then
-                  Inr_const U T $ mk_tuple1 bound_Ts vs
+                  Inr_const U T $ mk_tuple1_balanced bound_Ts vs
                 else if try (fst o dest_Const) u = SOME @{const_name case_prod} then
                   map (rewrite bound_Ts) vs |> chop 1
                   |>> HOLogic.mk_split o the_single
@@ -789,7 +785,7 @@
       fun build t =
         rhs_term
         |> massage_nested_corec_call lthy has_call massage bound_Ts (range_type (fastype_of t))
-        |> abs_tuple fun_args;
+        |> abs_tuple_balanced fun_args;
     in
       build
     end);
@@ -827,7 +823,7 @@
       |> fold2 (fold o build_corec_arg_disc) ctr_specss disc_eqnss
       |> fold2 (fold o build_corec_args_sel lthy has_call) sel_eqnss ctr_specss;
     fun currys [] t = t
-      | currys Ts t = t $ mk_tuple1 (List.rev Ts) (map Bound (length Ts - 1 downto 0))
+      | 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;
 
 (*
@@ -907,7 +903,7 @@
     val thy = Proof_Context.theory_of lthy;
 
     val (bs, mxs) = map_split (apfst fst) fixes;
-    val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> HOLogic.mk_tupleT) fixes |> split_list;
+    val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> mk_tupleT_balanced) fixes |> split_list;
 
     val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, HOLogic.typeS)) (bs ~~ arg_Ts) of
         [] => ()