# HG changeset patch
# User blanchet
# Date 1347292321 -7200
# Node ID 669a820ef21393ebb6202eaa2c5f3025a9440501
# Parent  831d4c259f5fed645fdf913b5121684dafe4deda
fixed general case of "mk_sumEN_balanced"

diff -r 831d4c259f5f -r 669a820ef213 src/HOL/Codatatype/BNF_Library.thy
--- a/src/HOL/Codatatype/BNF_Library.thy	Mon Sep 10 17:36:02 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Library.thy	Mon Sep 10 17:52:01 2012 +0200
@@ -829,6 +829,9 @@
 lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
 by simp
 
+lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
+by blast
+
 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)
diff -r 831d4c259f5f -r 669a820ef213 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Mon Sep 10 17:36:02 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Mon Sep 10 17:52:01 2012 +0200
@@ -72,15 +72,8 @@
 fun mk_sumEN_balanced 1 = @{thm one_pointE}
   | mk_sumEN_balanced 2 = @{thm sumE} (*optimization*)
   | 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;
+    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};
 
 fun tick v f = Term.lambda v (HOLogic.mk_prod (v, f $ v));
 
diff -r 831d4c259f5f -r 669a820ef213 src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Mon Sep 10 17:36:02 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Mon Sep 10 17:52:01 2012 +0200
@@ -30,11 +30,7 @@
    rtac refl) 1;
 
 fun mk_exhaust_tac ctxt n ctr_defs fld_iff_unf sumEN' =
-print_tac "A1" THEN(*###*)
-  Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN
-print_tac ("A2: " ^ Display.string_of_thm ctxt sumEN') THEN(*###*)
-  rtac sumEN' 1 THEN
-print_tac "A3" THEN(*###*)
+  Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN rtac sumEN' 1 THEN
   Local_Defs.unfold_tac ctxt @{thms all_prod_eq} THEN
   EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k, REPEAT_DETERM o dtac @{thm meta_spec},
     etac @{thm meta_mp}, atac]) (1 upto n)) 1;