src/HOL/Codatatype/Tools/bnf_fp_util.ML
changeset 49335 096967bf3940
parent 49330 276ff43ee0b1
child 49337 538687a77075
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 12 16:54:24 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 12 17:26:05 2012 +0200
     1.3 @@ -112,6 +112,7 @@
     1.4  
     1.5    val mk_sumEN: int -> thm
     1.6    val mk_sumEN_balanced: int -> thm
     1.7 +  val mk_sumEN_tupled_balanced: int list -> thm
     1.8    val mk_sum_casesN: int -> int -> thm
     1.9    val mk_sum_casesN_balanced: int -> int -> thm
    1.10  
    1.11 @@ -300,11 +301,26 @@
    1.12      (fold (fn i => fn thm => @{thm obj_sum_step} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF
    1.13        replicate n (impI RS allI);
    1.14  
    1.15 -fun mk_sumEN_balanced 1 = @{thm one_pointE}
    1.16 +fun mk_obj_sumEN_balanced n =
    1.17 +  Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f})))
    1.18 +    (replicate n asm_rl);
    1.19 +
    1.20 +fun mk_sumEN_balanced' n all_impIs = mk_obj_sumEN_balanced n OF all_impIs RS @{thm obj_one_pointE};
    1.21 +
    1.22 +fun mk_sumEN_balanced 1 = @{thm one_pointE} (*optimization*)
    1.23    | mk_sumEN_balanced 2 = @{thm sumE} (*optimization*)
    1.24 -  | mk_sumEN_balanced n =
    1.25 -    Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f})))
    1.26 -      (replicate n asm_rl) OF (replicate n (impI RS allI)) RS @{thm obj_one_pointE};
    1.27 +  | mk_sumEN_balanced n = mk_sumEN_balanced' n (replicate n (impI RS allI));
    1.28 +
    1.29 +fun mk_tupled_allIN 0 = @{thm unit_all_impI}
    1.30 +  | mk_tupled_allIN 1 = @{thm impI[THEN allI]}
    1.31 +  | mk_tupled_allIN 2 = @{thm prod_all_impI} (*optimization*)
    1.32 +  | mk_tupled_allIN n = mk_tupled_allIN (n - 1) RS @{thm prod_all_impI_step};
    1.33 +
    1.34 +fun mk_sumEN_tupled_balanced ms =
    1.35 +  let val n = length ms in
    1.36 +    if forall (curry (op =) 1) ms then mk_sumEN_balanced n
    1.37 +    else mk_sumEN_balanced' n (map mk_tupled_allIN ms)
    1.38 +  end;
    1.39  
    1.40  fun mk_sum_casesN 1 1 = refl
    1.41    | mk_sum_casesN _ 1 = @{thm sum.cases(1)}