src/ZF/int_arith.ML
changeset 27237 c94eefffc3a5
parent 27154 026f3db3f5c6
child 29269 5c25a2012975
     1.1 --- a/src/ZF/int_arith.ML	Mon Jun 16 17:54:50 2008 +0200
     1.2 +++ b/src/ZF/int_arith.ML	Mon Jun 16 17:54:51 2008 +0200
     1.3 @@ -6,101 +6,15 @@
     1.4  Simprocs for linear arithmetic.
     1.5  *)
     1.6  
     1.7 -
     1.8 -(** To simplify inequalities involving integer negation and literals,
     1.9 -    such as -x = #3
    1.10 -**)
    1.11 -
    1.12 -Addsimps [OldGoals.inst "y" "integ_of(?w)" @{thm zminus_equation},
    1.13 -          OldGoals.inst "x" "integ_of(?w)" @{thm equation_zminus}];
    1.14 -
    1.15 -AddIffs [OldGoals.inst "y" "integ_of(?w)" @{thm zminus_zless},
    1.16 -         OldGoals.inst "x" "integ_of(?w)" @{thm zless_zminus}];
    1.17 -
    1.18 -AddIffs [OldGoals.inst "y" "integ_of(?w)" @{thm zminus_zle},
    1.19 -         OldGoals.inst "x" "integ_of(?w)" @{thm zle_zminus}];
    1.20 -
    1.21 -Addsimps [OldGoals.inst "s" "integ_of(?w)" @{thm Let_def}];
    1.22 -
    1.23 -(*** Simprocs for numeric literals ***)
    1.24 -
    1.25 -(** Combining of literal coefficients in sums of products **)
    1.26 -
    1.27 -Goal "(x $< y) <-> (x$-y $< #0)";
    1.28 -by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
    1.29 -qed "zless_iff_zdiff_zless_0";
    1.30 -
    1.31 -Goal "[| x: int; y: int |] ==> (x = y) <-> (x$-y = #0)";
    1.32 -by (asm_simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
    1.33 -qed "eq_iff_zdiff_eq_0";
    1.34 -
    1.35 -Goal "(x $<= y) <-> (x$-y $<= #0)";
    1.36 -by (asm_simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
    1.37 -qed "zle_iff_zdiff_zle_0";
    1.38 -
    1.39 -
    1.40 -(** For combine_numerals **)
    1.41 -
    1.42 -Goal "i$*u $+ (j$*u $+ k) = (i$+j)$*u $+ k";
    1.43 -by (simp_tac (simpset() addsimps [@{thm zadd_zmult_distrib}]@ @{thms zadd_ac}) 1);
    1.44 -qed "left_zadd_zmult_distrib";
    1.45 -
    1.46 -
    1.47 -(** For cancel_numerals **)
    1.48 -
    1.49 -val rel_iff_rel_0_rls = map (OldGoals.inst "y" "?u$+?v")
    1.50 -                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
    1.51 -                           zle_iff_zdiff_zle_0] @
    1.52 -                        map (OldGoals.inst "y" "n")
    1.53 -                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
    1.54 -                           zle_iff_zdiff_zle_0];
    1.55 -
    1.56 -Goal "(i$*u $+ m = j$*u $+ n) <-> ((i$-j)$*u $+ m = intify(n))";
    1.57 -by (simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]) 1);
    1.58 -by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
    1.59 -by (simp_tac (simpset() addsimps @{thms zadd_ac}) 1);
    1.60 -qed "eq_add_iff1";
    1.61 -
    1.62 -Goal "(i$*u $+ m = j$*u $+ n) <-> (intify(m) = (j$-i)$*u $+ n)";
    1.63 -by (simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]) 1);
    1.64 -by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
    1.65 -by (simp_tac (simpset() addsimps @{thms zadd_ac}) 1);
    1.66 -qed "eq_add_iff2";
    1.67 -
    1.68 -Goal "(i$*u $+ m $< j$*u $+ n) <-> ((i$-j)$*u $+ m $< n)";
    1.69 -by (asm_simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]@
    1.70 -                                     @{thms zadd_ac} @ rel_iff_rel_0_rls) 1);
    1.71 -qed "less_add_iff1";
    1.72 -
    1.73 -Goal "(i$*u $+ m $< j$*u $+ n) <-> (m $< (j$-i)$*u $+ n)";
    1.74 -by (asm_simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]@
    1.75 -                                     @{thms zadd_ac} @ rel_iff_rel_0_rls) 1);
    1.76 -qed "less_add_iff2";
    1.77 -
    1.78 -Goal "(i$*u $+ m $<= j$*u $+ n) <-> ((i$-j)$*u $+ m $<= n)";
    1.79 -by (simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]) 1);
    1.80 -by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
    1.81 -by (simp_tac (simpset() addsimps @{thms zadd_ac}) 1);
    1.82 -qed "le_add_iff1";
    1.83 -
    1.84 -Goal "(i$*u $+ m $<= j$*u $+ n) <-> (m $<= (j$-i)$*u $+ n)";
    1.85 -by (simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]) 1);
    1.86 -by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
    1.87 -by (simp_tac (simpset() addsimps @{thms zadd_ac}) 1);
    1.88 -qed "le_add_iff2";
    1.89 -
    1.90 -
    1.91  structure Int_Numeral_Simprocs =
    1.92  struct
    1.93  
    1.94  (*Utilities*)
    1.95  
    1.96 -val integ_of_const = Const (@{const_name "Bin.integ_of"}, @{typ "i => i"});
    1.97 -
    1.98 -fun mk_numeral n = integ_of_const $ NumeralSyntax.mk_bin n;
    1.99 +fun mk_numeral n = @{const integ_of} $ NumeralSyntax.mk_bin n;
   1.100  
   1.101  (*Decodes a binary INTEGER*)
   1.102 -fun dest_numeral (Const(@{const_name "Bin.integ_of"}, _) $ w) =
   1.103 +fun dest_numeral (Const(@{const_name integ_of}, _) $ w) =
   1.104       (NumeralSyntax.dest_bin w
   1.105        handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
   1.106    | dest_numeral t =  raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
   1.107 @@ -113,8 +27,6 @@
   1.108  val zero = mk_numeral 0;
   1.109  val mk_plus = FOLogic.mk_binop @{const_name "zadd"};
   1.110  
   1.111 -val zminus_const = Const (@{const_name "zminus"}, @{typ "i => i"});
   1.112 -
   1.113  (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
   1.114  fun mk_sum []        = zero
   1.115    | mk_sum [t,u]     = mk_plus (t, u)
   1.116 @@ -132,7 +44,7 @@
   1.117    | dest_summing (pos, Const (@{const_name "zdiff"}, _) $ t $ u, ts) =
   1.118          dest_summing (pos, t, dest_summing (not pos, u, ts))
   1.119    | dest_summing (pos, t, ts) =
   1.120 -        if pos then t::ts else zminus_const$t :: ts;
   1.121 +        if pos then t::ts else @{const zminus} $ t :: ts;
   1.122  
   1.123  fun dest_sum t = dest_summing (true, t, []);
   1.124  
   1.125 @@ -245,8 +157,8 @@
   1.126    val prove_conv = ArithData.prove_conv "inteq_cancel_numerals"
   1.127    val mk_bal   = FOLogic.mk_eq
   1.128    val dest_bal = FOLogic.dest_eq
   1.129 -  val bal_add1 = eq_add_iff1 RS iff_trans
   1.130 -  val bal_add2 = eq_add_iff2 RS iff_trans
   1.131 +  val bal_add1 = @{thm eq_add_iff1} RS iff_trans
   1.132 +  val bal_add2 = @{thm eq_add_iff2} RS iff_trans
   1.133  );
   1.134  
   1.135  structure LessCancelNumerals = CancelNumeralsFun
   1.136 @@ -254,8 +166,8 @@
   1.137    val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
   1.138    val mk_bal   = FOLogic.mk_binrel @{const_name "zless"}
   1.139    val dest_bal = FOLogic.dest_bin @{const_name "zless"} @{typ i}
   1.140 -  val bal_add1 = less_add_iff1 RS iff_trans
   1.141 -  val bal_add2 = less_add_iff2 RS iff_trans
   1.142 +  val bal_add1 = @{thm less_add_iff1} RS iff_trans
   1.143 +  val bal_add2 = @{thm less_add_iff2} RS iff_trans
   1.144  );
   1.145  
   1.146  structure LeCancelNumerals = CancelNumeralsFun
   1.147 @@ -263,8 +175,8 @@
   1.148    val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
   1.149    val mk_bal   = FOLogic.mk_binrel @{const_name "zle"}
   1.150    val dest_bal = FOLogic.dest_bin @{const_name "zle"} @{typ i}
   1.151 -  val bal_add1 = le_add_iff1 RS iff_trans
   1.152 -  val bal_add2 = le_add_iff2 RS iff_trans
   1.153 +  val bal_add1 = @{thm le_add_iff1} RS iff_trans
   1.154 +  val bal_add2 = @{thm le_add_iff2} RS iff_trans
   1.155  );
   1.156  
   1.157  val cancel_numerals =
   1.158 @@ -298,7 +210,7 @@
   1.159    val dest_sum          = dest_sum
   1.160    val mk_coeff          = mk_coeff
   1.161    val dest_coeff        = dest_coeff 1
   1.162 -  val left_distrib      = left_zadd_zmult_distrib RS trans
   1.163 +  val left_distrib      = @{thm left_zadd_zmult_distrib} RS trans
   1.164    val prove_conv        = prove_conv_nohyps "int_combine_numerals"
   1.165    fun trans_tac _       = ArithData.gen_trans_tac trans
   1.166