# HG changeset patch
# User wenzelm
# Date 1213631691 -7200
# Node ID c94eefffc3a56fdfeb081dab33bb4432411e652a
# Parent  80356567e7ad598e4cb0e6db791826d096c9edf0
converted ML proofs;

diff -r 80356567e7ad -r c94eefffc3a5 src/ZF/IntArith.thy
--- a/src/ZF/IntArith.thy	Mon Jun 16 17:54:50 2008 +0200
+++ b/src/ZF/IntArith.thy	Mon Jun 16 17:54:51 2008 +0200
@@ -1,5 +1,91 @@
 
 theory IntArith imports Bin
-uses "int_arith.ML" begin
+uses ("int_arith.ML")
+begin
+
+
+(** To simplify inequalities involving integer negation and literals,
+    such as -x = #3
+**)
+
+lemmas [simp] =
+  zminus_equation [where y = "integ_of(w)", standard]
+  equation_zminus [where x = "integ_of(w)", standard]
+
+lemmas [iff] =
+  zminus_zless [where y = "integ_of(w)", standard]
+  zless_zminus [where x = "integ_of(w)", standard]
+
+lemmas [iff] =
+  zminus_zle [where y = "integ_of(w)", standard]
+  zle_zminus [where x = "integ_of(w)", standard]
+
+lemmas [simp] =
+  Let_def [where s = "integ_of(w)", standard]
+
+
+(*** Simprocs for numeric literals ***)
+
+(** Combining of literal coefficients in sums of products **)
+
+lemma zless_iff_zdiff_zless_0: "(x $< y) <-> (x$-y $< #0)"
+  by (simp add: zcompare_rls)
+
+lemma eq_iff_zdiff_eq_0: "[| x: int; y: int |] ==> (x = y) <-> (x$-y = #0)"
+  by (simp add: zcompare_rls)
+
+lemma zle_iff_zdiff_zle_0: "(x $<= y) <-> (x$-y $<= #0)"
+  by (simp add: zcompare_rls)
+
+
+(** For combine_numerals **)
+
+lemma left_zadd_zmult_distrib: "i$*u $+ (j$*u $+ k) = (i$+j)$*u $+ k"
+  by (simp add: zadd_zmult_distrib zadd_ac)
+
+
+(** For cancel_numerals **)
+
+lemmas rel_iff_rel_0_rls =
+  zless_iff_zdiff_zless_0 [where y = "u $+ v", standard]
+  eq_iff_zdiff_eq_0 [where y = "u $+ v", standard]
+  zle_iff_zdiff_zle_0 [where y = "u $+ v", standard]
+  zless_iff_zdiff_zless_0 [where y = n]
+  eq_iff_zdiff_eq_0 [where y = n]
+  zle_iff_zdiff_zle_0 [where y = n]
+
+lemma eq_add_iff1: "(i$*u $+ m = j$*u $+ n) <-> ((i$-j)$*u $+ m = intify(n))"
+  apply (simp add: zdiff_def zadd_zmult_distrib)
+  apply (simp add: zcompare_rls)
+  apply (simp add: zadd_ac)
+  done
+
+lemma eq_add_iff2: "(i$*u $+ m = j$*u $+ n) <-> (intify(m) = (j$-i)$*u $+ n)"
+  apply (simp add: zdiff_def zadd_zmult_distrib)
+  apply (simp add: zcompare_rls)
+  apply (simp add: zadd_ac)
+  done
+
+lemma less_add_iff1: "(i$*u $+ m $< j$*u $+ n) <-> ((i$-j)$*u $+ m $< n)"
+  apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
+  done
+
+lemma less_add_iff2: "(i$*u $+ m $< j$*u $+ n) <-> (m $< (j$-i)$*u $+ n)"
+  apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
+  done
+
+lemma le_add_iff1: "(i$*u $+ m $<= j$*u $+ n) <-> ((i$-j)$*u $+ m $<= n)"
+  apply (simp add: zdiff_def zadd_zmult_distrib)
+  apply (simp add: zcompare_rls)
+  apply (simp add: zadd_ac)
+  done
+
+lemma le_add_iff2: "(i$*u $+ m $<= j$*u $+ n) <-> (m $<= (j$-i)$*u $+ n)"
+  apply (simp add: zdiff_def zadd_zmult_distrib)
+  apply (simp add: zcompare_rls)
+  apply (simp add: zadd_ac)
+  done
+
+use "int_arith.ML"
 
 end
diff -r 80356567e7ad -r c94eefffc3a5 src/ZF/int_arith.ML
--- a/src/ZF/int_arith.ML	Mon Jun 16 17:54:50 2008 +0200
+++ b/src/ZF/int_arith.ML	Mon Jun 16 17:54:51 2008 +0200
@@ -6,101 +6,15 @@
 Simprocs for linear arithmetic.
 *)
 
-
-(** To simplify inequalities involving integer negation and literals,
-    such as -x = #3
-**)
-
-Addsimps [OldGoals.inst "y" "integ_of(?w)" @{thm zminus_equation},
-          OldGoals.inst "x" "integ_of(?w)" @{thm equation_zminus}];
-
-AddIffs [OldGoals.inst "y" "integ_of(?w)" @{thm zminus_zless},
-         OldGoals.inst "x" "integ_of(?w)" @{thm zless_zminus}];
-
-AddIffs [OldGoals.inst "y" "integ_of(?w)" @{thm zminus_zle},
-         OldGoals.inst "x" "integ_of(?w)" @{thm zle_zminus}];
-
-Addsimps [OldGoals.inst "s" "integ_of(?w)" @{thm Let_def}];
-
-(*** Simprocs for numeric literals ***)
-
-(** Combining of literal coefficients in sums of products **)
-
-Goal "(x $< y) <-> (x$-y $< #0)";
-by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
-qed "zless_iff_zdiff_zless_0";
-
-Goal "[| x: int; y: int |] ==> (x = y) <-> (x$-y = #0)";
-by (asm_simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
-qed "eq_iff_zdiff_eq_0";
-
-Goal "(x $<= y) <-> (x$-y $<= #0)";
-by (asm_simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
-qed "zle_iff_zdiff_zle_0";
-
-
-(** For combine_numerals **)
-
-Goal "i$*u $+ (j$*u $+ k) = (i$+j)$*u $+ k";
-by (simp_tac (simpset() addsimps [@{thm zadd_zmult_distrib}]@ @{thms zadd_ac}) 1);
-qed "left_zadd_zmult_distrib";
-
-
-(** For cancel_numerals **)
-
-val rel_iff_rel_0_rls = map (OldGoals.inst "y" "?u$+?v")
-                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
-                           zle_iff_zdiff_zle_0] @
-                        map (OldGoals.inst "y" "n")
-                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
-                           zle_iff_zdiff_zle_0];
-
-Goal "(i$*u $+ m = j$*u $+ n) <-> ((i$-j)$*u $+ m = intify(n))";
-by (simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]) 1);
-by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
-by (simp_tac (simpset() addsimps @{thms zadd_ac}) 1);
-qed "eq_add_iff1";
-
-Goal "(i$*u $+ m = j$*u $+ n) <-> (intify(m) = (j$-i)$*u $+ n)";
-by (simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]) 1);
-by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
-by (simp_tac (simpset() addsimps @{thms zadd_ac}) 1);
-qed "eq_add_iff2";
-
-Goal "(i$*u $+ m $< j$*u $+ n) <-> ((i$-j)$*u $+ m $< n)";
-by (asm_simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]@
-                                     @{thms zadd_ac} @ rel_iff_rel_0_rls) 1);
-qed "less_add_iff1";
-
-Goal "(i$*u $+ m $< j$*u $+ n) <-> (m $< (j$-i)$*u $+ n)";
-by (asm_simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]@
-                                     @{thms zadd_ac} @ rel_iff_rel_0_rls) 1);
-qed "less_add_iff2";
-
-Goal "(i$*u $+ m $<= j$*u $+ n) <-> ((i$-j)$*u $+ m $<= n)";
-by (simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]) 1);
-by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
-by (simp_tac (simpset() addsimps @{thms zadd_ac}) 1);
-qed "le_add_iff1";
-
-Goal "(i$*u $+ m $<= j$*u $+ n) <-> (m $<= (j$-i)$*u $+ n)";
-by (simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]) 1);
-by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
-by (simp_tac (simpset() addsimps @{thms zadd_ac}) 1);
-qed "le_add_iff2";
-
-
 structure Int_Numeral_Simprocs =
 struct
 
 (*Utilities*)
 
-val integ_of_const = Const (@{const_name "Bin.integ_of"}, @{typ "i => i"});
-
-fun mk_numeral n = integ_of_const $ NumeralSyntax.mk_bin n;
+fun mk_numeral n = @{const integ_of} $ NumeralSyntax.mk_bin n;
 
 (*Decodes a binary INTEGER*)
-fun dest_numeral (Const(@{const_name "Bin.integ_of"}, _) $ w) =
+fun dest_numeral (Const(@{const_name integ_of}, _) $ w) =
      (NumeralSyntax.dest_bin w
       handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
   | dest_numeral t =  raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
@@ -113,8 +27,6 @@
 val zero = mk_numeral 0;
 val mk_plus = FOLogic.mk_binop @{const_name "zadd"};
 
-val zminus_const = Const (@{const_name "zminus"}, @{typ "i => i"});
-
 (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
 fun mk_sum []        = zero
   | mk_sum [t,u]     = mk_plus (t, u)
@@ -132,7 +44,7 @@
   | dest_summing (pos, Const (@{const_name "zdiff"}, _) $ t $ u, ts) =
         dest_summing (pos, t, dest_summing (not pos, u, ts))
   | dest_summing (pos, t, ts) =
-        if pos then t::ts else zminus_const$t :: ts;
+        if pos then t::ts else @{const zminus} $ t :: ts;
 
 fun dest_sum t = dest_summing (true, t, []);
 
@@ -245,8 +157,8 @@
   val prove_conv = ArithData.prove_conv "inteq_cancel_numerals"
   val mk_bal   = FOLogic.mk_eq
   val dest_bal = FOLogic.dest_eq
-  val bal_add1 = eq_add_iff1 RS iff_trans
-  val bal_add2 = eq_add_iff2 RS iff_trans
+  val bal_add1 = @{thm eq_add_iff1} RS iff_trans
+  val bal_add2 = @{thm eq_add_iff2} RS iff_trans
 );
 
 structure LessCancelNumerals = CancelNumeralsFun
@@ -254,8 +166,8 @@
   val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
   val mk_bal   = FOLogic.mk_binrel @{const_name "zless"}
   val dest_bal = FOLogic.dest_bin @{const_name "zless"} @{typ i}
-  val bal_add1 = less_add_iff1 RS iff_trans
-  val bal_add2 = less_add_iff2 RS iff_trans
+  val bal_add1 = @{thm less_add_iff1} RS iff_trans
+  val bal_add2 = @{thm less_add_iff2} RS iff_trans
 );
 
 structure LeCancelNumerals = CancelNumeralsFun
@@ -263,8 +175,8 @@
   val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
   val mk_bal   = FOLogic.mk_binrel @{const_name "zle"}
   val dest_bal = FOLogic.dest_bin @{const_name "zle"} @{typ i}
-  val bal_add1 = le_add_iff1 RS iff_trans
-  val bal_add2 = le_add_iff2 RS iff_trans
+  val bal_add1 = @{thm le_add_iff1} RS iff_trans
+  val bal_add2 = @{thm le_add_iff2} RS iff_trans
 );
 
 val cancel_numerals =
@@ -298,7 +210,7 @@
   val dest_sum          = dest_sum
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff 1
-  val left_distrib      = left_zadd_zmult_distrib RS trans
+  val left_distrib      = @{thm left_zadd_zmult_distrib} RS trans
   val prove_conv        = prove_conv_nohyps "int_combine_numerals"
   fun trans_tac _       = ArithData.gen_trans_tac trans