# HG changeset patch
# User blanchet
# Date 1347291353 -7200
# Node ID 2ecc533d6697496459874e914c17c5486407d157
# Parent  edc322ac527932d818c0132b0219443d91da3996
use balanced sums for constructors (to gracefully handle 100 constructors or more)

diff -r edc322ac5279 -r 2ecc533d6697 src/HOL/Codatatype/BNF_Library.thy
--- a/src/HOL/Codatatype/BNF_Library.thy	Mon Sep 10 17:32:39 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Library.thy	Mon Sep 10 17:35:53 2012 +0200
@@ -19,7 +19,7 @@
 
 lemma all_unit_eq: "(\<And>x. PROP P x) \<equiv> PROP P ()" by simp
 
-lemma all_prod_eq: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (a, b))" by auto
+lemma all_prod_eq: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (a, b))" by clarsimp
 
 lemma False_imp_eq: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
 by presburger
@@ -89,23 +89,23 @@
 by (rule ext) (auto simp add: collect_def)
 
 lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})"
-by auto
+by blast
 
 lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
-by auto
+by blast
 
 lemma rev_bspec: "a \<in> A \<Longrightarrow> \<forall>z \<in> A. P z \<Longrightarrow> P a"
 by simp
 
 lemma Un_cong: "\<lbrakk>A = B; C = D\<rbrakk> \<Longrightarrow> A \<union> C = B \<union> D"
-by auto
+by simp
 
 lemma UN_image_subset: "\<Union>f ` g x \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
-by auto
+by blast
 
 lemma image_Collect_subsetI:
   "(\<And>x. P x \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` {x. P x} \<subseteq> B"
-by auto
+by blast
 
 lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>(\<lambda>f. f x) ` X| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
 by (unfold o_apply collect_def SUP_def)
@@ -826,17 +826,21 @@
   "sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p"
 by auto
 
+lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+by simp
+
+lemma obj_sumE_f:
+"\<lbrakk>\<forall>x. s = f (Inl x) \<longrightarrow> P; \<forall>x. s = f (Inr x) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f x \<longrightarrow> P"
+by (metis sum.exhaust)
+
 lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
 by (cases s) auto
 
-lemma obj_sum_base: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
-by auto
-
 lemma obj_sum_step:
   "\<lbrakk>\<forall>x. s = f (Inr (Inl x)) \<longrightarrow> P; \<forall>x. s = f (Inr (Inr x)) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f (Inr x) \<longrightarrow> P"
 by (metis obj_sumE)
 
 lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
-by auto
+by simp
 
 end
diff -r edc322ac5279 -r 2ecc533d6697 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Mon Sep 10 17:32:39 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Mon Sep 10 17:35:53 2012 +0200
@@ -50,11 +50,33 @@
 fun mk_uncurried2_fun f xss =
   mk_tupled_fun (HOLogic.mk_tuple (map HOLogic.mk_tuple xss)) f (flat xss);
 
+val mk_sumTN_balanced = Balanced_Tree.make mk_sumT;
+val dest_sumTN_balanced = Balanced_Tree.dest dest_sumT;
+
+fun mk_InN_balanced ctxt sum_T Ts t k =
+  let
+    val u =
+      Balanced_Tree.access {left = mk_Inl dummyT, right = mk_Inr dummyT, init = t} (length Ts) k;
+  in singleton (Type_Infer_Context.infer_types ctxt) (Type.constraint sum_T u) end;
+
+val mk_sum_caseN_balanced = Balanced_Tree.make mk_sum_case;
+
+fun mk_sumEN_balanced n =
+  let
+    val thm =
+      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));
+    val f as (_, f_T) =
+      Term.add_vars (prop_of thm) []
+      |> filter (fn ((s, _), _) => s = "f") |> the_single;
+    val inst = [pairself (cterm_of @{theory}) (Var f, Abs (Name.uu, domain_type f_T, Bound 0))];
+  in cterm_instantiate inst thm end;
+
 fun tick v f = Term.lambda v (HOLogic.mk_prod (v, f $ v));
 
 fun tack z_name (c, v) f =
   let val z = Free (z_name, mk_sumT (fastype_of v, fastype_of c)) in
-    Term.lambda z (mk_sum_case (Term.lambda v v) (Term.lambda c (f $ c)) $ z)
+    Term.lambda z (mk_sum_case (Term.lambda v v, Term.lambda c (f $ c)) $ z)
   end;
 
 fun cannot_merge_types () = error "Mutually recursive types must have the same type parameters";
@@ -148,9 +170,9 @@
       | freeze_fp T = T;
 
     val ctr_TsssXs = map (map (map freeze_fp)) fake_ctr_Tsss;
-    val sum_prod_TsXs = map (mk_sumTN o map HOLogic.mk_tupleT) ctr_TsssXs;
+    val ctr_sum_prod_TsXs = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctr_TsssXs;
 
-    val eqs = map dest_TFree Xs ~~ sum_prod_TsXs;
+    val eqs = map dest_TFree Xs ~~ ctr_sum_prod_TsXs;
 
     val (pre_bnfs, ((unfs0, flds0, fp_iters0, fp_recs0, unf_flds, fld_unfs, fld_injects,
         fp_iter_thms, fp_rec_thms), lthy)) =
@@ -215,7 +237,7 @@
       if lfp then
         let
           val y_Tsss =
-            map3 (fn n => fn ms => map2 dest_tupleT ms o dest_sumTN n o domain_type)
+            map3 (fn n => fn ms => map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type)
               ns mss fp_iter_fun_Ts;
           val g_Tss = map2 (map2 (curry (op --->))) y_Tsss Css;
 
@@ -225,8 +247,8 @@
             ||>> mk_Freesss "x" y_Tsss;
 
           val z_Tssss =
-            map3 (fn n => fn ms => map2 (map dest_rec_pair oo dest_tupleT) ms o dest_sumTN n
-              o domain_type) ns mss fp_rec_fun_Ts;
+            map3 (fn n => fn ms => map2 (map dest_rec_pair oo dest_tupleT) ms o
+              dest_sumTN_balanced n o domain_type) ns mss fp_rec_fun_Ts;
           val h_Tss = map2 (map2 (fold_rev (curry (op --->)))) z_Tssss Css;
 
           val hss = map2 (map2 retype_free) gss h_Tss;
@@ -251,7 +273,7 @@
           fun mk_types fun_Ts =
             let
               val f_sum_prod_Ts = map range_type fun_Ts;
-              val f_prod_Tss = map2 dest_sumTN ns f_sum_prod_Ts;
+              val f_prod_Tss = map2 dest_sumTN_balanced ns f_sum_prod_Ts;
               val f_Tsss =
                 map3 (fn C => map2 (map (curry (op -->) C) oo dest_tupleT)) Cs mss' f_prod_Tss;
               val pf_Tss = map2 zip_preds_getters p_Tss f_Tsss
@@ -288,6 +310,7 @@
       let
         val unfT = domain_type (fastype_of fld);
         val ctr_prod_Ts = map HOLogic.mk_tupleT ctr_Tss;
+        val ctr_sum_prod_T = mk_sumTN_balanced ctr_prod_Ts;
         val case_Ts = map (fn Ts => Ts ---> C) ctr_Tss;
 
         val ((((u, v), fs), xss), _) =
@@ -299,12 +322,15 @@
 
         val ctr_rhss =
           map2 (fn k => fn xs =>
-            fold_rev Term.lambda xs (fld $ mk_InN ctr_prod_Ts (HOLogic.mk_tuple xs) k)) ks xss;
+              fold_rev Term.lambda xs (fld $ mk_InN_balanced no_defs_lthy ctr_sum_prod_T ctr_prod_Ts
+                (HOLogic.mk_tuple xs) k))
+            ks xss;
 
         val case_binder = Binding.suffix_name ("_" ^ caseN) b;
 
         val case_rhs =
-          fold_rev Term.lambda (fs @ [v]) (mk_sum_caseN (map2 mk_uncurried_fun fs xss) $ (unf $ v));
+          fold_rev Term.lambda (fs @ [v])
+            (mk_sum_caseN_balanced (map2 mk_uncurried_fun fs xss) $ (unf $ v));
 
         val ((raw_case :: raw_ctrs, raw_case_def :: raw_ctr_defs), (lthy', lthy)) = no_defs_lthy
           |> apfst split_list o fold_map3 (fn b => fn mx => fn rhs =>
@@ -340,7 +366,8 @@
 
             val sumEN_thm' =
               Local_Defs.unfold lthy @{thms all_unit_eq}
-                (Drule.instantiate' (map (SOME o certifyT lthy) ctr_prod_Ts) [] (mk_sumEN n))
+                (Drule.instantiate' (map (SOME o certifyT lthy) ctr_prod_Ts) []
+                   (mk_sumEN_balanced n))
               |> Morphism.thm phi;
           in
             mk_exhaust_tac ctxt n ctr_defs fld_iff_unf_thm sumEN_thm'
@@ -373,7 +400,7 @@
                 val spec =
                   mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binder, res_T)),
                     Term.list_comb (fp_iter_like,
-                      map2 (mk_sum_caseN oo map2 mk_uncurried2_fun) fss xssss));
+                      map2 (mk_sum_caseN_balanced oo map2 mk_uncurried2_fun) fss xssss));
               in (binder, spec) end;
 
             val iter_likes =
@@ -411,7 +438,8 @@
 
                 fun mk_preds_getters_join c n cps sum_prod_T prod_Ts cfss =
                   Term.lambda c (mk_IfN sum_prod_T cps
-                    (map2 (mk_InN prod_Ts) (map HOLogic.mk_tuple cfss) (1 upto n)));
+                    (map2 (mk_InN_balanced no_defs_lthy sum_prod_T prod_Ts)
+                      (map HOLogic.mk_tuple cfss) (1 upto n)));
 
                 val spec =
                   mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binder, res_T)),
diff -r edc322ac5279 -r 2ecc533d6697 src/HOL/Codatatype/Tools/bnf_fp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Mon Sep 10 17:32:39 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Mon Sep 10 17:35:53 2012 +0200
@@ -81,15 +81,18 @@
   val split_conj_thm: thm -> thm list
   val split_conj_prems: int -> thm -> thm
 
+  val mk_sumTN: typ list -> typ
+
   val Inl_const: typ -> typ -> term
   val Inr_const: typ -> typ -> term
 
-  val mk_Inl: term -> typ -> term
-  val mk_Inr: term -> typ -> term
+  val mk_Inl: typ -> term -> term
+  val mk_Inr: typ -> term -> term
   val mk_InN: typ list -> term -> int -> term
-  val mk_sum_case: term -> term -> term
+  val mk_sum_case: term * term -> term
   val mk_sum_caseN: term list -> term
 
+  val dest_sumT: typ -> typ * typ
   val dest_sumTN: int -> typ -> typ list
   val dest_tupleT: int -> typ -> typ list
 
@@ -197,18 +200,20 @@
 val set_inclN = "set_incl"
 val set_set_inclN = "set_set_incl"
 
+fun mk_sumTN Ts = Library.foldr1 mk_sumT Ts;
+
 fun Inl_const LT RT = Const (@{const_name Inl}, LT --> mk_sumT (LT, RT));
-fun mk_Inl t RT = Inl_const (fastype_of t) RT $ t;
+fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t;
 
 fun Inr_const LT RT = Const (@{const_name Inr}, RT --> mk_sumT (LT, RT));
-fun mk_Inr t LT = Inr_const LT (fastype_of t) $ t;
+fun mk_Inr LT t = Inr_const LT (fastype_of t) $ t;
 
 fun mk_InN [_] t 1 = t
-  | mk_InN (_ :: Ts) t 1 = mk_Inl t (mk_sumTN Ts)
-  | mk_InN (LT :: Ts) t m = mk_Inr (mk_InN Ts t (m - 1)) LT
+  | mk_InN (_ :: Ts) t 1 = mk_Inl (mk_sumTN Ts) t
+  | mk_InN (LT :: Ts) t m = mk_Inr LT (mk_InN Ts t (m - 1))
   | mk_InN Ts t _ = raise (TYPE ("mk_InN", Ts, [t]));
 
-fun mk_sum_case f g =
+fun mk_sum_case (f, g) =
   let
     val fT = fastype_of f;
     val gT = fastype_of g;
@@ -218,7 +223,9 @@
   end;
 
 fun mk_sum_caseN [f] = f
-  | mk_sum_caseN (f :: fs) = mk_sum_case f (mk_sum_caseN fs);
+  | mk_sum_caseN (f :: fs) = mk_sum_case (f, mk_sum_caseN fs);
+
+fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T');
 
 fun dest_sumTN 1 T = [T]
   | dest_sumTN n (Type (@{type_name sum}, [T, T'])) = T :: dest_sumTN (n - 1) T';
@@ -247,7 +254,7 @@
       if i = n then th else split n (i + 1) (conjI RSN (i, th)) handle THM _ => th;
   in split limit 1 th end;
 
-fun mk_sumEN 1 = @{thm obj_sum_base}
+fun mk_sumEN 1 = @{thm one_pointE}
   | mk_sumEN 2 = @{thm sumE}
   | mk_sumEN n =
     (fold (fn i => fn thm => @{thm obj_sum_step} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF
diff -r edc322ac5279 -r 2ecc533d6697 src/HOL/Codatatype/Tools/bnf_gfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Mon Sep 10 17:32:39 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Mon Sep 10 17:35:53 2012 +0200
@@ -506,7 +506,7 @@
     val mor_sum_case_thm =
       let
         val maps = map3 (fn s => fn sum_s => fn map =>
-          mk_sum_case (HOLogic.mk_comp (Term.list_comb (map, passive_ids @ Inls), s)) sum_s)
+          mk_sum_case (HOLogic.mk_comp (Term.list_comb (map, passive_ids @ Inls), s), sum_s))
           s's sum_ss map_Inls;
       in
         Skip_Proof.prove lthy [] []
@@ -2144,7 +2144,7 @@
       let
         val corecT = Library.foldr (op -->) (corec_sTs, AT --> T);
         val maps = map3 (fn unf => fn sum_s => fn map => mk_sum_case
-            (HOLogic.mk_comp (Term.list_comb (map, passive_ids @ corec_Inls), unf)) sum_s)
+            (HOLogic.mk_comp (Term.list_comb (map, passive_ids @ corec_Inls), unf), sum_s))
           unfs corec_ss corec_maps;
 
         val lhs = Term.list_comb (Free (corec_name i, corecT), corec_ss);
@@ -2171,7 +2171,7 @@
     val corec_defs = map (Morphism.thm phi) corec_def_frees;
 
     val sum_cases =
-      map2 (fn T => fn i => mk_sum_case (HOLogic.id_const T) (mk_corec corec_ss i)) Ts ks;
+      map2 (fn T => fn i => mk_sum_case (HOLogic.id_const T, mk_corec corec_ss i)) Ts ks;
     val corec_thms =
       let
         fun mk_goal i corec_s corec_map unf z =
diff -r edc322ac5279 -r 2ecc533d6697 src/HOL/Codatatype/Tools/bnf_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_util.ML	Mon Sep 10 17:32:39 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Mon Sep 10 17:35:53 2012 +0200
@@ -62,7 +62,6 @@
   val mk_relT: typ * typ -> typ
   val dest_relT: typ -> typ * typ
   val mk_sumT: typ * typ -> typ
-  val mk_sumTN: typ list -> typ
 
   val ctwo: term
   val fst_const: typ -> term
@@ -304,7 +303,6 @@
 val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT;
 val dest_relT = HOLogic.dest_prodT o HOLogic.dest_setT;
 fun mk_sumT (LT, RT) = Type (@{type_name Sum_Type.sum}, [LT, RT]);
-fun mk_sumTN Ts = Library.foldr1 mk_sumT Ts;
 fun mk_partial_funT (ranT, domT) = domT --> mk_optionT ranT;