move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used
authorhuffman
Fri Jul 27 19:27:21 2012 +0200 (2012-07-27)
changeset 4856112aa0cb2b447
parent 48560 e0875d956a6b
child 48562 f6d6d58fa318
child 48565 7c497a239007
move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used
src/HOL/Divides.thy
src/HOL/Tools/nat_arith.ML
     1.1 --- a/src/HOL/Divides.thy	Fri Jul 27 17:59:18 2012 +0200
     1.2 +++ b/src/HOL/Divides.thy	Fri Jul 27 19:27:21 2012 +0200
     1.3 @@ -693,8 +693,20 @@
     1.4    val div_name = @{const_name div};
     1.5    val mod_name = @{const_name mod};
     1.6    val mk_binop = HOLogic.mk_binop;
     1.7 -  val mk_sum = Nat_Arith.mk_sum;
     1.8 -  val dest_sum = Nat_Arith.dest_sum;
     1.9 +  val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
    1.10 +  val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
    1.11 +  fun mk_sum [] = HOLogic.zero
    1.12 +    | mk_sum [t] = t
    1.13 +    | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    1.14 +  fun dest_sum tm =
    1.15 +    if HOLogic.is_zero tm then []
    1.16 +    else
    1.17 +      (case try HOLogic.dest_Suc tm of
    1.18 +        SOME t => HOLogic.Suc_zero :: dest_sum t
    1.19 +      | NONE =>
    1.20 +          (case try dest_plus tm of
    1.21 +            SOME (t, u) => dest_sum t @ dest_sum u
    1.22 +          | NONE => [tm]));
    1.23  
    1.24    val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
    1.25  
     2.1 --- a/src/HOL/Tools/nat_arith.ML	Fri Jul 27 17:59:18 2012 +0200
     2.2 +++ b/src/HOL/Tools/nat_arith.ML	Fri Jul 27 19:27:21 2012 +0200
     2.3 @@ -10,40 +10,11 @@
     2.4    val cancel_eq_conv: conv
     2.5    val cancel_le_conv: conv
     2.6    val cancel_less_conv: conv
     2.7 -  (* legacy functions: *)
     2.8 -  val mk_sum: term list -> term
     2.9 -  val mk_norm_sum: term list -> term
    2.10 -  val dest_sum: term -> term list
    2.11  end;
    2.12  
    2.13  structure Nat_Arith: NAT_ARITH =
    2.14  struct
    2.15  
    2.16 -(** abstract syntax of structure nat: 0, Suc, + **)
    2.17 -
    2.18 -val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
    2.19 -val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
    2.20 -
    2.21 -fun mk_sum [] = HOLogic.zero
    2.22 -  | mk_sum [t] = t
    2.23 -  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    2.24 -
    2.25 -(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
    2.26 -fun mk_norm_sum ts =
    2.27 -  let val (ones, sums) = List.partition (equal HOLogic.Suc_zero) ts in
    2.28 -    funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
    2.29 -  end;
    2.30 -
    2.31 -fun dest_sum tm =
    2.32 -  if HOLogic.is_zero tm then []
    2.33 -  else
    2.34 -    (case try HOLogic.dest_Suc tm of
    2.35 -      SOME t => HOLogic.Suc_zero :: dest_sum t
    2.36 -    | NONE =>
    2.37 -        (case try dest_plus tm of
    2.38 -          SOME (t, u) => dest_sum t @ dest_sum u
    2.39 -        | NONE => [tm]));
    2.40 -
    2.41  val add1 = @{lemma "(A::'a::comm_monoid_add) == k + a ==> A + b == k + (a + b)"
    2.42        by (simp only: add_ac)}
    2.43  val add2 = @{lemma "(B::'a::comm_monoid_add) == k + b ==> a + B == k + (a + b)"