src/ZF/int_arith.ML
changeset 26190 cf51a23c0cd0
parent 26059 b67a225b50fd
child 27154 026f3db3f5c6
     1.1 --- a/src/ZF/int_arith.ML	Sat Mar 01 14:10:15 2008 +0100
     1.2 +++ b/src/ZF/int_arith.ML	Sat Mar 01 15:01:03 2008 +0100
     1.3 @@ -95,7 +95,7 @@
     1.4  
     1.5  (*Utilities*)
     1.6  
     1.7 -val integ_of_const = Const (@{const_name "Bin.integ_of"}, iT --> iT);
     1.8 +val integ_of_const = Const (@{const_name "Bin.integ_of"}, @{typ "i => i"});
     1.9  
    1.10  fun mk_numeral n = integ_of_const $ NumeralSyntax.mk_bin n;
    1.11  
    1.12 @@ -113,9 +113,7 @@
    1.13  val zero = mk_numeral 0;
    1.14  val mk_plus = FOLogic.mk_binop @{const_name "zadd"};
    1.15  
    1.16 -val iT = Ind_Syntax.iT;
    1.17 -
    1.18 -val zminus_const = Const (@{const_name "zminus"}, iT --> iT);
    1.19 +val zminus_const = Const (@{const_name "zminus"}, @{typ "i => i"});
    1.20  
    1.21  (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
    1.22  fun mk_sum []        = zero
    1.23 @@ -126,7 +124,7 @@
    1.24  fun long_mk_sum []        = zero
    1.25    | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    1.26  
    1.27 -val dest_plus = FOLogic.dest_bin @{const_name "zadd"} iT;
    1.28 +val dest_plus = FOLogic.dest_bin @{const_name "zadd"} @{typ i};
    1.29  
    1.30  (*decompose additions AND subtractions as a sum*)
    1.31  fun dest_summing (pos, Const (@{const_name "zadd"}, _) $ t $ u, ts) =
    1.32 @@ -139,7 +137,7 @@
    1.33  fun dest_sum t = dest_summing (true, t, []);
    1.34  
    1.35  val mk_diff = FOLogic.mk_binop @{const_name "zdiff"};
    1.36 -val dest_diff = FOLogic.dest_bin @{const_name "zdiff"} iT;
    1.37 +val dest_diff = FOLogic.dest_bin @{const_name "zdiff"} @{typ i};
    1.38  
    1.39  val one = mk_numeral 1;
    1.40  val mk_times = FOLogic.mk_binop @{const_name "zmult"};
    1.41 @@ -149,7 +147,7 @@
    1.42    | mk_prod (t :: ts) = if t = one then mk_prod ts
    1.43                          else mk_times (t, mk_prod ts);
    1.44  
    1.45 -val dest_times = FOLogic.dest_bin @{const_name "zmult"} iT;
    1.46 +val dest_times = FOLogic.dest_bin @{const_name "zmult"} @{typ i};
    1.47  
    1.48  fun dest_prod t =
    1.49        let val (t,u) = dest_times t
    1.50 @@ -255,7 +253,7 @@
    1.51   (open CancelNumeralsCommon
    1.52    val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
    1.53    val mk_bal   = FOLogic.mk_binrel @{const_name "zless"}
    1.54 -  val dest_bal = FOLogic.dest_bin @{const_name "zless"} iT
    1.55 +  val dest_bal = FOLogic.dest_bin @{const_name "zless"} @{typ i}
    1.56    val bal_add1 = less_add_iff1 RS iff_trans
    1.57    val bal_add2 = less_add_iff2 RS iff_trans
    1.58  );
    1.59 @@ -264,7 +262,7 @@
    1.60   (open CancelNumeralsCommon
    1.61    val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
    1.62    val mk_bal   = FOLogic.mk_binrel @{const_name "zle"}
    1.63 -  val dest_bal = FOLogic.dest_bin @{const_name "zle"} iT
    1.64 +  val dest_bal = FOLogic.dest_bin @{const_name "zle"} @{typ i}
    1.65    val bal_add1 = le_add_iff1 RS iff_trans
    1.66    val bal_add2 = le_add_iff2 RS iff_trans
    1.67  );