src/HOL/arith_data.ML
changeset 4310 cad4f24be60b
parent 4309 c98f44948d86
child 4332 d4a15e32c024
     1.1 --- a/src/HOL/arith_data.ML	Wed Nov 26 17:52:53 1997 +0100
     1.2 +++ b/src/HOL/arith_data.ML	Thu Nov 27 13:38:06 1997 +0100
     1.3 @@ -18,19 +18,25 @@
     1.4  
     1.5  (** abstract syntax of structure nat: 0, Suc, + **)
     1.6  
     1.7 -(* mk_sum *)
     1.8 +(* mk_sum, mk_norm_sum *)
     1.9  
    1.10 +val one = HOLogic.mk_nat 1;
    1.11  val mk_plus = HOLogic.mk_binop "op +";
    1.12  
    1.13  fun mk_sum [] = HOLogic.zero
    1.14    | mk_sum [t] = t
    1.15    | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    1.16  
    1.17 +(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
    1.18 +fun mk_norm_sum ts =
    1.19 +  let val (ones, sums) = partition (equal one) ts in
    1.20 +    funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
    1.21 +  end;
    1.22 +
    1.23  
    1.24  (* dest_sum *)
    1.25  
    1.26  val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
    1.27 -val one = HOLogic.mk_nat 1;
    1.28  
    1.29  fun dest_sum tm =
    1.30    if HOLogic.is_zero tm then []
    1.31 @@ -72,7 +78,7 @@
    1.32  
    1.33  structure Sum =
    1.34  struct
    1.35 -  val mk_sum = mk_sum;
    1.36 +  val mk_sum = mk_norm_sum;
    1.37    val dest_sum = dest_sum;
    1.38    val prove_conv = prove_conv;
    1.39    val norm_tac = simp_all add_rules THEN simp_all add_ac;
    1.40 @@ -125,7 +131,7 @@
    1.41  
    1.42  structure Factor =
    1.43  struct
    1.44 -  val mk_sum = mk_sum;
    1.45 +  val mk_sum = mk_norm_sum;
    1.46    val dest_sum = dest_sum;
    1.47    val prove_conv = prove_conv;
    1.48    val norm_tac = simp_all (add_rules @ mult_rules) THEN simp_all add_ac;