--- a/src/ZF/Bin.thy Thu Aug 21 14:41:05 2014 +0200
+++ b/src/ZF/Bin.thy Thu Aug 21 14:41:08 2014 +0200
@@ -594,4 +594,92 @@
"(integ_of(w) = x $* y) \<longleftrightarrow> (x $* y = integ_of(w))"
by auto
+(** To simplify inequalities involving integer negation and literals,
+ such as -x = #3
+**)
+
+lemmas [simp] =
+ zminus_equation [where y = "integ_of(w)"]
+ equation_zminus [where x = "integ_of(w)"]
+ for w
+
+lemmas [iff] =
+ zminus_zless [where y = "integ_of(w)"]
+ zless_zminus [where x = "integ_of(w)"]
+ for w
+
+lemmas [iff] =
+ zminus_zle [where y = "integ_of(w)"]
+ zle_zminus [where x = "integ_of(w)"]
+ for w
+
+lemmas [simp] =
+ Let_def [where s = "integ_of(w)"] for w
+
+
+(*** Simprocs for numeric literals ***)
+
+(** Combining of literal coefficients in sums of products **)
+
+lemma zless_iff_zdiff_zless_0: "(x $< y) \<longleftrightarrow> (x$-y $< #0)"
+ by (simp add: zcompare_rls)
+
+lemma eq_iff_zdiff_eq_0: "[| x \<in> int; y \<in> int |] ==> (x = y) \<longleftrightarrow> (x$-y = #0)"
+ by (simp add: zcompare_rls)
+
+lemma zle_iff_zdiff_zle_0: "(x $<= y) \<longleftrightarrow> (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"]
+ eq_iff_zdiff_eq_0 [where y = "u $+ v"]
+ zle_iff_zdiff_zle_0 [where y = "u $+ v"]
+ zless_iff_zdiff_zless_0 [where y = n]
+ eq_iff_zdiff_eq_0 [where y = n]
+ zle_iff_zdiff_zle_0 [where y = n]
+ for u v (* FIXME n (!?) *)
+
+lemma eq_add_iff1: "(i$*u $+ m = j$*u $+ n) \<longleftrightarrow> ((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) \<longleftrightarrow> (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) \<longleftrightarrow> ((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) \<longleftrightarrow> (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) \<longleftrightarrow> ((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) \<longleftrightarrow> (m $<= (j$-i)$*u $+ n)"
+ apply (simp add: zdiff_def zadd_zmult_distrib)
+ apply (simp add: zcompare_rls)
+ apply (simp add: zadd_ac)
+ done
+
+ML_file "int_arith.ML"
+
end
--- a/src/ZF/IntArith.thy Thu Aug 21 14:41:05 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,94 +0,0 @@
-
-theory IntArith imports Bin
-begin
-
-
-(** To simplify inequalities involving integer negation and literals,
- such as -x = #3
-**)
-
-lemmas [simp] =
- zminus_equation [where y = "integ_of(w)"]
- equation_zminus [where x = "integ_of(w)"]
- for w
-
-lemmas [iff] =
- zminus_zless [where y = "integ_of(w)"]
- zless_zminus [where x = "integ_of(w)"]
- for w
-
-lemmas [iff] =
- zminus_zle [where y = "integ_of(w)"]
- zle_zminus [where x = "integ_of(w)"]
- for w
-
-lemmas [simp] =
- Let_def [where s = "integ_of(w)"] for w
-
-
-(*** Simprocs for numeric literals ***)
-
-(** Combining of literal coefficients in sums of products **)
-
-lemma zless_iff_zdiff_zless_0: "(x $< y) \<longleftrightarrow> (x$-y $< #0)"
- by (simp add: zcompare_rls)
-
-lemma eq_iff_zdiff_eq_0: "[| x \<in> int; y \<in> int |] ==> (x = y) \<longleftrightarrow> (x$-y = #0)"
- by (simp add: zcompare_rls)
-
-lemma zle_iff_zdiff_zle_0: "(x $<= y) \<longleftrightarrow> (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"]
- eq_iff_zdiff_eq_0 [where y = "u $+ v"]
- zle_iff_zdiff_zle_0 [where y = "u $+ v"]
- zless_iff_zdiff_zless_0 [where y = n]
- eq_iff_zdiff_eq_0 [where y = n]
- zle_iff_zdiff_zle_0 [where y = n]
- for u v (* FIXME n (!?) *)
-
-lemma eq_add_iff1: "(i$*u $+ m = j$*u $+ n) \<longleftrightarrow> ((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) \<longleftrightarrow> (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) \<longleftrightarrow> ((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) \<longleftrightarrow> (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) \<longleftrightarrow> ((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) \<longleftrightarrow> (m $<= (j$-i)$*u $+ n)"
- apply (simp add: zdiff_def zadd_zmult_distrib)
- apply (simp add: zcompare_rls)
- apply (simp add: zadd_ac)
- done
-
-ML_file "int_arith.ML"
-
-end
--- a/src/ZF/IntDiv_ZF.thy Thu Aug 21 14:41:05 2014 +0200
+++ b/src/ZF/IntDiv_ZF.thy Thu Aug 21 14:41:08 2014 +0200
@@ -29,7 +29,9 @@
header{*The Division Operators Div and Mod*}
-theory IntDiv_ZF imports IntArith OrderArith begin
+theory IntDiv_ZF
+imports Bin OrderArith
+begin
definition
quorem :: "[i,i] => o" where
--- a/src/ZF/int_arith.ML Thu Aug 21 14:41:05 2014 +0200
+++ b/src/ZF/int_arith.ML Thu Aug 21 14:41:08 2014 +0200
@@ -151,7 +151,7 @@
structure CancelNumeralsCommon =
struct
- val mk_sum = (fn T:typ => mk_sum)
+ val mk_sum = (fn _ : typ => mk_sum)
val dest_sum = dest_sum
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
@@ -236,7 +236,7 @@
type coeff = int
val iszero = (fn x => x = 0)
val add = op +
- val mk_sum = (fn T:typ => long_mk_sum) (*to work for #2*x $+ #3*x *)
+ val mk_sum = (fn _ : typ => long_mk_sum) (*to work for #2*x $+ #3*x *)
val dest_sum = dest_sum
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
@@ -284,7 +284,7 @@
type coeff = int
val iszero = (fn x => x = 0)
val add = op *
- val mk_sum = (fn T:typ => mk_prod)
+ val mk_sum = (fn _ : typ => mk_prod)
val dest_sum = dest_prod
fun mk_coeff(k,t) = if t=one then mk_numeral k
else raise TERM("mk_coeff", [])