# 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 () \ Q ()) \ \x. P x \ Q x" +by simp + +lemma prod_all_impI: "(\x y. P (x, y) \ Q (x, y)) \ \x. P x \ Q x" +by clarify + +lemma prod_all_impI_step: "(\x. \y. P (x, y) \ Q (x, y)) \ \x. P x \ Q x" +by auto + lemma all_unit_eq: "(\x. PROP P x) \ PROP P ()" by simp -(* FIXME: needed? *) lemma all_prod_eq: "(\x. PROP P x) \ (\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)}