# HG changeset patch
# User blanchet
# Date 1347463565 -7200
# Node ID 096967bf394055c38b2b3f51f35524b692dd87c7
# Parent  dbc169ddd4047372c7536a108df627c451d47751
added sumEN_tupled_balanced

diff -r dbc169ddd404 -r 096967bf3940 src/HOL/Codatatype/BNF_FP.thy
--- a/src/HOL/Codatatype/BNF_FP.thy	Wed Sep 12 16:54:24 2012 +0200
+++ b/src/HOL/Codatatype/BNF_FP.thy	Wed Sep 12 17:26:05 2012 +0200
@@ -17,10 +17,17 @@
 lemma case_unit: "(case u of () => f) = f"
 by (cases u) (hypsubst, rule unit.cases)
 
-(* FIXME: needed? *)
+lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
+by simp
+
+lemma prod_all_impI: "(\<And>x y. P (x, y) \<Longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
+by clarify
+
+lemma prod_all_impI_step: "(\<And>x. \<forall>y. P (x, y) \<longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
+by auto
+
 lemma all_unit_eq: "(\<And>x. PROP P x) \<equiv> PROP P ()" by simp
 
-(* FIXME: needed? *)
 lemma all_prod_eq: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (a, b))" by clarsimp
 
 (* FIXME: needed? *)
diff -r dbc169ddd404 -r 096967bf3940 src/HOL/Codatatype/Tools/bnf_fp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 12 16:54:24 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 12 17:26:05 2012 +0200
@@ -112,6 +112,7 @@
 
   val mk_sumEN: int -> thm
   val mk_sumEN_balanced: int -> thm
+  val mk_sumEN_tupled_balanced: int list -> thm
   val mk_sum_casesN: int -> int -> thm
   val mk_sum_casesN_balanced: int -> int -> thm
 
@@ -300,11 +301,26 @@
     (fold (fn i => fn thm => @{thm obj_sum_step} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF
       replicate n (impI RS allI);
 
-fun mk_sumEN_balanced 1 = @{thm one_pointE}
+fun mk_obj_sumEN_balanced n =
+  Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f})))
+    (replicate n asm_rl);
+
+fun mk_sumEN_balanced' n all_impIs = mk_obj_sumEN_balanced n OF all_impIs RS @{thm obj_one_pointE};
+
+fun mk_sumEN_balanced 1 = @{thm one_pointE} (*optimization*)
   | mk_sumEN_balanced 2 = @{thm sumE} (*optimization*)
-  | mk_sumEN_balanced n =
-    Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f})))
-      (replicate n asm_rl) OF (replicate n (impI RS allI)) RS @{thm obj_one_pointE};
+  | mk_sumEN_balanced n = mk_sumEN_balanced' n (replicate n (impI RS allI));
+
+fun mk_tupled_allIN 0 = @{thm unit_all_impI}
+  | mk_tupled_allIN 1 = @{thm impI[THEN allI]}
+  | mk_tupled_allIN 2 = @{thm prod_all_impI} (*optimization*)
+  | mk_tupled_allIN n = mk_tupled_allIN (n - 1) RS @{thm prod_all_impI_step};
+
+fun mk_sumEN_tupled_balanced ms =
+  let val n = length ms in
+    if forall (curry (op =) 1) ms then mk_sumEN_balanced n
+    else mk_sumEN_balanced' n (map mk_tupled_allIN ms)
+  end;
 
 fun mk_sum_casesN 1 1 = refl
   | mk_sum_casesN _ 1 = @{thm sum.cases(1)}