src/ZF/int_arith.ML
changeset 26056 6a0801279f4c
parent 24893 b8ef7afe3a6b
child 26059 b67a225b50fd
     1.1 --- a/src/ZF/int_arith.ML	Mon Feb 11 15:19:17 2008 +0100
     1.2 +++ b/src/ZF/int_arith.ML	Mon Feb 11 15:40:21 2008 +0100
     1.3 @@ -95,12 +95,12 @@
     1.4  
     1.5  (*Utilities*)
     1.6  
     1.7 -val integ_of_const = Const ("Bin.integ_of", iT --> iT);
     1.8 +val integ_of_const = Const (@{const_name "Bin.integ_of"}, iT --> iT);
     1.9  
    1.10  fun mk_numeral n = integ_of_const $ NumeralSyntax.mk_bin n;
    1.11  
    1.12  (*Decodes a binary INTEGER*)
    1.13 -fun dest_numeral (Const("Bin.integ_of", _) $ w) =
    1.14 +fun dest_numeral (Const(@{const_name "Bin.integ_of"}, _) $ w) =
    1.15       (NumeralSyntax.dest_bin w
    1.16        handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
    1.17    | dest_numeral t =  raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
    1.18 @@ -111,11 +111,11 @@
    1.19    | find_first_numeral past [] = raise TERM("find_first_numeral", []);
    1.20  
    1.21  val zero = mk_numeral 0;
    1.22 -val mk_plus = FOLogic.mk_binop "Int.zadd";
    1.23 +val mk_plus = FOLogic.mk_binop @{const_name "Int_ZF.zadd"};
    1.24  
    1.25  val iT = Ind_Syntax.iT;
    1.26  
    1.27 -val zminus_const = Const ("Int.zminus", iT --> iT);
    1.28 +val zminus_const = Const (@{const_name "Int_ZF.zminus"}, iT --> iT);
    1.29  
    1.30  (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
    1.31  fun mk_sum []        = zero
    1.32 @@ -126,30 +126,30 @@
    1.33  fun long_mk_sum []        = zero
    1.34    | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    1.35  
    1.36 -val dest_plus = FOLogic.dest_bin "Int.zadd" iT;
    1.37 +val dest_plus = FOLogic.dest_bin @{const_name "Int_ZF.zadd"} iT;
    1.38  
    1.39  (*decompose additions AND subtractions as a sum*)
    1.40 -fun dest_summing (pos, Const ("Int.zadd", _) $ t $ u, ts) =
    1.41 +fun dest_summing (pos, Const (@{const_name "Int_ZF.zadd"}, _) $ t $ u, ts) =
    1.42          dest_summing (pos, t, dest_summing (pos, u, ts))
    1.43 -  | dest_summing (pos, Const ("Int.zdiff", _) $ t $ u, ts) =
    1.44 +  | dest_summing (pos, Const (@{const_name "Int_ZF.zdiff"}, _) $ t $ u, ts) =
    1.45          dest_summing (pos, t, dest_summing (not pos, u, ts))
    1.46    | dest_summing (pos, t, ts) =
    1.47          if pos then t::ts else zminus_const$t :: ts;
    1.48  
    1.49  fun dest_sum t = dest_summing (true, t, []);
    1.50  
    1.51 -val mk_diff = FOLogic.mk_binop "Int.zdiff";
    1.52 -val dest_diff = FOLogic.dest_bin "Int.zdiff" iT;
    1.53 +val mk_diff = FOLogic.mk_binop @{const_name "Int_ZF.zdiff"};
    1.54 +val dest_diff = FOLogic.dest_bin @{const_name "Int_ZF.zdiff"} iT;
    1.55  
    1.56  val one = mk_numeral 1;
    1.57 -val mk_times = FOLogic.mk_binop "Int.zmult";
    1.58 +val mk_times = FOLogic.mk_binop @{const_name "Int_ZF.zmult"};
    1.59  
    1.60  fun mk_prod [] = one
    1.61    | mk_prod [t] = t
    1.62    | mk_prod (t :: ts) = if t = one then mk_prod ts
    1.63                          else mk_times (t, mk_prod ts);
    1.64  
    1.65 -val dest_times = FOLogic.dest_bin "Int.zmult" iT;
    1.66 +val dest_times = FOLogic.dest_bin @{const_name "Int_ZF.zmult"} iT;
    1.67  
    1.68  fun dest_prod t =
    1.69        let val (t,u) = dest_times t
    1.70 @@ -160,7 +160,7 @@
    1.71  fun mk_coeff (k, t) = mk_times (mk_numeral k, t);
    1.72  
    1.73  (*Express t as a product of (possibly) a numeral with other sorted terms*)
    1.74 -fun dest_coeff sign (Const ("Int.zminus", _) $ t) = dest_coeff (~sign) t
    1.75 +fun dest_coeff sign (Const (@{const_name "Int_ZF.zminus"}, _) $ t) = dest_coeff (~sign) t
    1.76    | dest_coeff sign t =
    1.77      let val ts = sort Term.term_ord (dest_prod t)
    1.78          val (n, ts') = find_first_numeral [] ts
    1.79 @@ -254,8 +254,8 @@
    1.80  structure LessCancelNumerals = CancelNumeralsFun
    1.81   (open CancelNumeralsCommon
    1.82    val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
    1.83 -  val mk_bal   = FOLogic.mk_binrel "Int.zless"
    1.84 -  val dest_bal = FOLogic.dest_bin "Int.zless" iT
    1.85 +  val mk_bal   = FOLogic.mk_binrel @{const_name "Int_ZF.zless"}
    1.86 +  val dest_bal = FOLogic.dest_bin @{const_name "Int_ZF.zless"} iT
    1.87    val bal_add1 = less_add_iff1 RS iff_trans
    1.88    val bal_add2 = less_add_iff2 RS iff_trans
    1.89  );
    1.90 @@ -263,8 +263,8 @@
    1.91  structure LeCancelNumerals = CancelNumeralsFun
    1.92   (open CancelNumeralsCommon
    1.93    val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
    1.94 -  val mk_bal   = FOLogic.mk_binrel "Int.zle"
    1.95 -  val dest_bal = FOLogic.dest_bin "Int.zle" iT
    1.96 +  val mk_bal   = FOLogic.mk_binrel @{const_name "Int_ZF.zle"}
    1.97 +  val dest_bal = FOLogic.dest_bin @{const_name "Int_ZF.zle"} iT
    1.98    val bal_add1 = le_add_iff1 RS iff_trans
    1.99    val bal_add2 = le_add_iff2 RS iff_trans
   1.100  );