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
```