# HG changeset patch # User blanchet # Date 1347291362 -7200 # Node ID 4bf74375b4f737d842e6c8ce2b98cc2568286684 # Parent 0dc6cf758ed1b348b81f780487307e79d1e19e63 fixed base case of "mk_sumEN_balanced" diff -r 0dc6cf758ed1 -r 4bf74375b4f7 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:36:02 2012 +0200 @@ -69,16 +69,18 @@ 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 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; fun tick v f = Term.lambda v (HOLogic.mk_prod (v, f $ v));