--- a/src/HOL/arith_data.ML Wed Nov 26 17:52:53 1997 +0100
+++ b/src/HOL/arith_data.ML Thu Nov 27 13:38:06 1997 +0100
@@ -18,19 +18,25 @@
(** abstract syntax of structure nat: 0, Suc, + **)
-(* mk_sum *)
+(* mk_sum, mk_norm_sum *)
+val one = HOLogic.mk_nat 1;
val mk_plus = HOLogic.mk_binop "op +";
fun mk_sum [] = HOLogic.zero
| mk_sum [t] = t
| mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
+(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
+fun mk_norm_sum ts =
+ let val (ones, sums) = partition (equal one) ts in
+ funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
+ end;
+
(* dest_sum *)
val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
-val one = HOLogic.mk_nat 1;
fun dest_sum tm =
if HOLogic.is_zero tm then []
@@ -72,7 +78,7 @@
structure Sum =
struct
- val mk_sum = mk_sum;
+ val mk_sum = mk_norm_sum;
val dest_sum = dest_sum;
val prove_conv = prove_conv;
val norm_tac = simp_all add_rules THEN simp_all add_ac;
@@ -125,7 +131,7 @@
structure Factor =
struct
- val mk_sum = mk_sum;
+ val mk_sum = mk_norm_sum;
val dest_sum = dest_sum;
val prove_conv = prove_conv;
val norm_tac = simp_all (add_rules @ mult_rules) THEN simp_all add_ac;