merged.
--- a/src/HOL/Divides.thy Thu Jan 08 17:25:06 2009 +0100
+++ b/src/HOL/Divides.thy Thu Jan 08 21:13:40 2009 -0800
@@ -33,6 +33,10 @@
unfolding mult_commute [of b]
by (rule mod_div_equality)
+lemma mod_div_equality': "a mod b + a div b * b = a"
+ using mod_div_equality [of a b]
+ by (simp only: add_ac)
+
lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
by (simp add: mod_div_equality)
@@ -143,6 +147,173 @@
then show "b mod a = 0" by simp
qed
+lemma mod_div_trivial [simp]: "a mod b div b = 0"
+proof (cases "b = 0")
+ assume "b = 0"
+ thus ?thesis by simp
+next
+ assume "b \<noteq> 0"
+ hence "a div b + a mod b div b = (a mod b + a div b * b) div b"
+ by (rule div_mult_self1 [symmetric])
+ also have "\<dots> = a div b"
+ by (simp only: mod_div_equality')
+ also have "\<dots> = a div b + 0"
+ by simp
+ finally show ?thesis
+ by (rule add_left_imp_eq)
+qed
+
+lemma mod_mod_trivial [simp]: "a mod b mod b = a mod b"
+proof -
+ have "a mod b mod b = (a mod b + a div b * b) mod b"
+ by (simp only: mod_mult_self1)
+ also have "\<dots> = a mod b"
+ by (simp only: mod_div_equality')
+ finally show ?thesis .
+qed
+
+text {* Addition respects modular equivalence. *}
+
+lemma mod_add_left_eq: "(a + b) mod c = (a mod c + b) mod c"
+proof -
+ have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
+ by (simp only: mod_div_equality)
+ also have "\<dots> = (a mod c + b + a div c * c) mod c"
+ by (simp only: add_ac)
+ also have "\<dots> = (a mod c + b) mod c"
+ by (rule mod_mult_self1)
+ finally show ?thesis .
+qed
+
+lemma mod_add_right_eq: "(a + b) mod c = (a + b mod c) mod c"
+proof -
+ have "(a + b) mod c = (a + (b div c * c + b mod c)) mod c"
+ by (simp only: mod_div_equality)
+ also have "\<dots> = (a + b mod c + b div c * c) mod c"
+ by (simp only: add_ac)
+ also have "\<dots> = (a + b mod c) mod c"
+ by (rule mod_mult_self1)
+ finally show ?thesis .
+qed
+
+lemma mod_add_eq: "(a + b) mod c = (a mod c + b mod c) mod c"
+by (rule trans [OF mod_add_left_eq mod_add_right_eq])
+
+lemma mod_add_cong:
+ assumes "a mod c = a' mod c"
+ assumes "b mod c = b' mod c"
+ shows "(a + b) mod c = (a' + b') mod c"
+proof -
+ have "(a mod c + b mod c) mod c = (a' mod c + b' mod c) mod c"
+ unfolding assms ..
+ thus ?thesis
+ by (simp only: mod_add_eq [symmetric])
+qed
+
+text {* Multiplication respects modular equivalence. *}
+
+lemma mod_mult_left_eq: "(a * b) mod c = ((a mod c) * b) mod c"
+proof -
+ have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
+ by (simp only: mod_div_equality)
+ also have "\<dots> = (a mod c * b + a div c * b * c) mod c"
+ by (simp only: left_distrib right_distrib add_ac mult_ac)
+ also have "\<dots> = (a mod c * b) mod c"
+ by (rule mod_mult_self1)
+ finally show ?thesis .
+qed
+
+lemma mod_mult_right_eq: "(a * b) mod c = (a * (b mod c)) mod c"
+proof -
+ have "(a * b) mod c = (a * (b div c * c + b mod c)) mod c"
+ by (simp only: mod_div_equality)
+ also have "\<dots> = (a * (b mod c) + a * (b div c) * c) mod c"
+ by (simp only: left_distrib right_distrib add_ac mult_ac)
+ also have "\<dots> = (a * (b mod c)) mod c"
+ by (rule mod_mult_self1)
+ finally show ?thesis .
+qed
+
+lemma mod_mult_eq: "(a * b) mod c = ((a mod c) * (b mod c)) mod c"
+by (rule trans [OF mod_mult_left_eq mod_mult_right_eq])
+
+lemma mod_mult_cong:
+ assumes "a mod c = a' mod c"
+ assumes "b mod c = b' mod c"
+ shows "(a * b) mod c = (a' * b') mod c"
+proof -
+ have "(a mod c * (b mod c)) mod c = (a' mod c * (b' mod c)) mod c"
+ unfolding assms ..
+ thus ?thesis
+ by (simp only: mod_mult_eq [symmetric])
+qed
+
+lemma mod_mod_cancel:
+ assumes "c dvd b"
+ shows "a mod b mod c = a mod c"
+proof -
+ from `c dvd b` obtain k where "b = c * k"
+ by (rule dvdE)
+ have "a mod b mod c = a mod (c * k) mod c"
+ by (simp only: `b = c * k`)
+ also have "\<dots> = (a mod (c * k) + a div (c * k) * k * c) mod c"
+ by (simp only: mod_mult_self1)
+ also have "\<dots> = (a div (c * k) * (c * k) + a mod (c * k)) mod c"
+ by (simp only: add_ac mult_ac)
+ also have "\<dots> = a mod c"
+ by (simp only: mod_div_equality)
+ finally show ?thesis .
+qed
+
+end
+
+class ring_div = semiring_div + comm_ring_1
+begin
+
+text {* Negation respects modular equivalence. *}
+
+lemma mod_minus_eq: "(- a) mod b = (- (a mod b)) mod b"
+proof -
+ have "(- a) mod b = (- (a div b * b + a mod b)) mod b"
+ by (simp only: mod_div_equality)
+ also have "\<dots> = (- (a mod b) + - (a div b) * b) mod b"
+ by (simp only: minus_add_distrib minus_mult_left add_ac)
+ also have "\<dots> = (- (a mod b)) mod b"
+ by (rule mod_mult_self1)
+ finally show ?thesis .
+qed
+
+lemma mod_minus_cong:
+ assumes "a mod b = a' mod b"
+ shows "(- a) mod b = (- a') mod b"
+proof -
+ have "(- (a mod b)) mod b = (- (a' mod b)) mod b"
+ unfolding assms ..
+ thus ?thesis
+ by (simp only: mod_minus_eq [symmetric])
+qed
+
+text {* Subtraction respects modular equivalence. *}
+
+lemma mod_diff_left_eq: "(a - b) mod c = (a mod c - b) mod c"
+ unfolding diff_minus
+ by (intro mod_add_cong mod_minus_cong) simp_all
+
+lemma mod_diff_right_eq: "(a - b) mod c = (a - b mod c) mod c"
+ unfolding diff_minus
+ by (intro mod_add_cong mod_minus_cong) simp_all
+
+lemma mod_diff_eq: "(a - b) mod c = (a mod c - b mod c) mod c"
+ unfolding diff_minus
+ by (intro mod_add_cong mod_minus_cong) simp_all
+
+lemma mod_diff_cong:
+ assumes "a mod c = a' mod c"
+ assumes "b mod c = b' mod c"
+ shows "(a - b) mod c = (a' - b') mod c"
+ unfolding diff_minus using assms
+ by (intro mod_add_cong mod_minus_cong)
+
end
@@ -467,22 +638,14 @@
done
lemma mod_mult1_eq: "(a*b) mod c = a*(b mod c) mod (c::nat)"
-apply (cases "c = 0", simp)
-apply (blast intro: divmod_rel [THEN divmod_rel_mult1_eq, THEN mod_eq])
-done
+ by (rule mod_mult_right_eq)
lemma mod_mult1_eq': "(a*b) mod (c::nat) = ((a mod c) * b) mod c"
- apply (rule trans)
- apply (rule_tac s = "b*a mod c" in trans)
- apply (rule_tac [2] mod_mult1_eq)
- apply (simp_all add: mult_commute)
- done
+ by (rule mod_mult_left_eq)
lemma mod_mult_distrib_mod:
"(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c"
-apply (rule mod_mult1_eq' [THEN trans])
-apply (rule mod_mult1_eq)
-done
+ by (rule mod_mult_eq)
lemma divmod_rel_add1_eq:
"[| divmod_rel a c aq ar; divmod_rel b c bq br; c > 0 |]
@@ -497,9 +660,7 @@
done
lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"
-apply (cases "c = 0", simp)
-apply (blast intro: divmod_rel_add1_eq [THEN mod_eq] divmod_rel)
-done
+ by (rule mod_add_eq)
lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
apply (cut_tac m = q and n = c in mod_less_divisor)
@@ -618,11 +779,11 @@
apply (auto simp add: Suc_diff_le le_mod_geq)
done
-lemma nat_mod_div_trivial [simp]: "m mod n div n = (0 :: nat)"
- by (cases "n = 0") auto
+lemma nat_mod_div_trivial: "m mod n div n = (0 :: nat)"
+ by simp
-lemma nat_mod_mod_trivial [simp]: "m mod n mod n = (m mod n :: nat)"
- by (cases "n = 0") auto
+lemma nat_mod_mod_trivial: "m mod n mod n = (m mod n :: nat)"
+ by simp
subsubsection {* The Divides Relation *}
@@ -718,18 +879,6 @@
apply (simp add: power_add)
done
-lemma mod_add_left_eq: "((a::nat) + b) mod c = (a mod c + b) mod c"
- apply (rule trans [symmetric])
- apply (rule mod_add1_eq, simp)
- apply (rule mod_add1_eq [symmetric])
- done
-
-lemma mod_add_right_eq: "(a+b) mod (c::nat) = (a + (b mod c)) mod c"
- apply (rule trans [symmetric])
- apply (rule mod_add1_eq, simp)
- apply (rule mod_add1_eq [symmetric])
- done
-
lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
by (induct n) auto
--- a/src/HOL/IntDiv.thy Thu Jan 08 17:25:06 2009 +0100
+++ b/src/HOL/IntDiv.thy Thu Jan 08 21:13:40 2009 -0800
@@ -747,12 +747,12 @@
lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a"
by (simp add: zdiv_zmult1_eq)
-lemma mod_div_trivial [simp]: "(a mod b) div b = (0::int)"
+lemma zmod_zdiv_trivial: "(a mod b) div b = (0::int)"
apply (case_tac "b = 0", simp)
apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
done
-lemma mod_mod_trivial [simp]: "(a mod b) mod b = a mod (b::int)"
+lemma zmod_zmod_trivial: "(a mod b) mod b = a mod (b::int)"
apply (case_tac "b = 0", simp)
apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial)
done
@@ -776,72 +776,50 @@
apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod)
done
-lemma zdiv_zadd_self1[simp]: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
-by (simp add: zdiv_zadd1_eq)
-
-lemma zdiv_zadd_self2[simp]: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
-by (simp add: zdiv_zadd1_eq)
-
-instance int :: semiring_div
+instance int :: ring_div
proof
fix a b c :: int
assume not0: "b \<noteq> 0"
show "(a + c * b) div b = c + a div b"
unfolding zdiv_zadd1_eq [of a "c * b"] using not0
- by (simp add: zmod_zmult1_eq)
+ by (simp add: zmod_zmult1_eq zmod_zdiv_trivial)
qed auto
-lemma zdiv_zmult_self2 [simp]: "b \<noteq> (0::int) ==> (b*a) div b = a"
-by (subst mult_commute, erule zdiv_zmult_self1)
+lemma zdiv_zadd_self1: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
+by (rule div_add_self1) (* already declared [simp] *)
+
+lemma zdiv_zadd_self2: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
+by (rule div_add_self2) (* already declared [simp] *)
-lemma zmod_zmult_self1 [simp]: "(a*b) mod b = (0::int)"
-by (simp add: zmod_zmult1_eq)
+lemma zdiv_zmult_self2: "b \<noteq> (0::int) ==> (b*a) div b = a"
+by (rule div_mult_self1_is_id) (* already declared [simp] *)
-lemma zmod_zmult_self2 [simp]: "(b*a) mod b = (0::int)"
-by (simp add: mult_commute zmod_zmult1_eq)
+lemma zmod_zmult_self1: "(a*b) mod b = (0::int)"
+by (rule mod_mult_self2_is_0) (* already declared [simp] *)
+
+lemma zmod_zmult_self2: "(b*a) mod b = (0::int)"
+by (rule mod_mult_self1_is_0) (* already declared [simp] *)
lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
-proof
- assume "m mod d = 0"
- with zmod_zdiv_equality[of m d] show "EX q::int. m = d*q" by auto
-next
- assume "EX q::int. m = d*q"
- thus "m mod d = 0" by auto
-qed
+by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
+(* REVISIT: should this be generalized to all semiring_div types? *)
lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
lemma zmod_zadd_left_eq: "(a+b) mod (c::int) = ((a mod c) + b) mod c"
-apply (rule trans [symmetric])
-apply (rule zmod_zadd1_eq, simp)
-apply (rule zmod_zadd1_eq [symmetric])
-done
+by (rule mod_add_left_eq)
lemma zmod_zadd_right_eq: "(a+b) mod (c::int) = (a + (b mod c)) mod c"
-apply (rule trans [symmetric])
-apply (rule zmod_zadd1_eq, simp)
-apply (rule zmod_zadd1_eq [symmetric])
-done
+by (rule mod_add_right_eq)
-lemma zmod_zadd_self1[simp]: "(a+b) mod a = b mod (a::int)"
-apply (case_tac "a = 0", simp)
-apply (simp add: zmod_zadd1_eq)
-done
+lemma zmod_zadd_self1: "(a+b) mod a = b mod (a::int)"
+by (rule mod_add_self1) (* already declared [simp] *)
-lemma zmod_zadd_self2[simp]: "(b+a) mod a = b mod (a::int)"
-apply (case_tac "a = 0", simp)
-apply (simp add: zmod_zadd1_eq)
-done
-
+lemma zmod_zadd_self2: "(b+a) mod a = b mod (a::int)"
+by (rule mod_add_self2) (* already declared [simp] *)
-lemma zmod_zdiff1_eq: fixes a::int
- shows "(a - b) mod c = (a mod c - b mod c) mod c" (is "?l = ?r")
-proof -
- have "?l = (c + (a mod c - b mod c)) mod c"
- using zmod_zadd1_eq[of a "-b" c] by(simp add:ring_simps zmod_zminus1_eq_if)
- also have "\<dots> = ?r" by simp
- finally show ?thesis .
-qed
+lemma zmod_zdiff1_eq: "(a - b) mod c = (a mod c - b mod c) mod (c::int)"
+by (rule mod_diff_eq)
subsection{*Proving @{term "a div (b*c) = (a div b) div c"} *}
@@ -954,18 +932,8 @@
apply (auto simp add: mult_commute)
done
-lemma zmod_zmod_cancel:
-assumes "n dvd m" shows "(k::int) mod m mod n = k mod n"
-proof -
- from `n dvd m` obtain r where "m = n*r" by(auto simp:dvd_def)
- have "k mod n = (m * (k div m) + k mod m) mod n"
- using zmod_zdiv_equality[of k m] by simp
- also have "\<dots> = (m * (k div m) mod n + k mod m mod n) mod n"
- by(subst zmod_zadd1_eq, rule refl)
- also have "m * (k div m) mod n = 0" using `m = n*r`
- by(simp add:mult_ac)
- finally show ?thesis by simp
-qed
+lemma zmod_zmod_cancel: "n dvd m \<Longrightarrow> (k::int) mod m mod n = k mod n"
+by (rule mod_mod_cancel)
subsection {*Splitting Rules for div and mod*}
@@ -1169,50 +1137,31 @@
subsection {* The Divides Relation *}
lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
- by (simp add: dvd_def zmod_eq_0_iff)
+ by (rule dvd_eq_mod_eq_0)
lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard]
-lemma zdvd_0_right [iff]: "(m::int) dvd 0"
- by (simp add: dvd_def)
+lemma zdvd_0_right: "(m::int) dvd 0"
+ by (rule dvd_0_right) (* already declared [iff] *)
-lemma zdvd_0_left [iff,noatp]: "(0 dvd (m::int)) = (m = 0)"
- by (simp add: dvd_def)
+lemma zdvd_0_left: "(0 dvd (m::int)) = (m = 0)"
+ by (rule dvd_0_left_iff) (* already declared [noatp,simp] *)
-lemma zdvd_1_left [iff]: "1 dvd (m::int)"
- by (simp add: dvd_def)
+lemma zdvd_1_left: "1 dvd (m::int)"
+ by (rule one_dvd) (* already declared [simp] *)
lemma zdvd_refl [simp]: "m dvd (m::int)"
- by (auto simp add: dvd_def intro: zmult_1_right [symmetric])
+ by (rule dvd_refl) (* TODO: declare generic dvd_refl [simp] *)
lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
- by (auto simp add: dvd_def intro: mult_assoc)
+ by (rule dvd_trans)
lemma zdvd_zminus_iff: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
-proof
- assume "m dvd - n"
- then obtain k where "- n = m * k" ..
- then have "n = m * - k" by simp
- then show "m dvd n" ..
-next
- assume "m dvd n"
- then have "m dvd n * -1" by (rule dvd_mult2)
- then show "m dvd - n" by simp
-qed
+ by (rule dvd_minus_iff)
lemma zdvd_zminus2_iff: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
-proof
- assume "- m dvd n"
- then obtain k where "n = - m * k" ..
- then have "n = m * - k" by simp
- then show "m dvd n" ..
-next
- assume "m dvd n"
- then obtain k where "n = m * k" ..
- then have "n = - m * - k" by simp
- then show "- m dvd n" ..
-qed
+ by (rule minus_dvd_iff)
lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)"
by (cases "i > 0") (simp_all add: zdvd_zminus2_iff)
@@ -1227,9 +1176,7 @@
done
lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)"
- apply (simp add: dvd_def)
- apply (blast intro: right_distrib [symmetric])
- done
+ by (rule dvd_add)
lemma zdvd_dvd_eq: assumes anz:"a \<noteq> 0" and ab: "(a::int) dvd b" and ba:"b dvd a"
shows "\<bar>a\<bar> = \<bar>b\<bar>"
@@ -1244,9 +1191,7 @@
qed
lemma zdvd_zdiff: "k dvd m ==> k dvd n ==> k dvd (m - n :: int)"
- apply (simp add: dvd_def)
- apply (blast intro: right_diff_distrib [symmetric])
- done
+ by (rule Ring_and_Field.dvd_diff)
lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
apply (subgoal_tac "m = n + (m - n)")
@@ -1255,34 +1200,22 @@
done
lemma zdvd_zmult: "k dvd (n::int) ==> k dvd m * n"
- apply (simp add: dvd_def)
- apply (blast intro: mult_left_commute)
- done
+ by (rule dvd_mult)
lemma zdvd_zmult2: "k dvd (m::int) ==> k dvd m * n"
- apply (subst mult_commute)
- apply (erule zdvd_zmult)
- done
+ by (rule dvd_mult2)
-lemma zdvd_triv_right [iff]: "(k::int) dvd m * k"
- apply (rule zdvd_zmult)
- apply (rule zdvd_refl)
- done
+lemma zdvd_triv_right: "(k::int) dvd m * k"
+ by (rule dvd_triv_right) (* already declared [simp] *)
-lemma zdvd_triv_left [iff]: "(k::int) dvd k * m"
- apply (rule zdvd_zmult2)
- apply (rule zdvd_refl)
- done
+lemma zdvd_triv_left: "(k::int) dvd k * m"
+ by (rule dvd_triv_left) (* already declared [simp] *)
lemma zdvd_zmultD2: "j * k dvd n ==> j dvd (n::int)"
- apply (simp add: dvd_def)
- apply (simp add: mult_assoc, blast)
- done
+ by (rule dvd_mult_left)
lemma zdvd_zmultD: "j * k dvd n ==> k dvd (n::int)"
- apply (rule zdvd_zmultD2)
- apply (subst mult_commute, assumption)
- done
+ by (rule dvd_mult_right)
lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n"
by (rule mult_dvd_mono)
@@ -1333,7 +1266,7 @@
{assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
with h have False by (simp add: mult_assoc)}
hence "n = m * h" by blast
- thus ?thesis by blast
+ thus ?thesis by simp
qed
lemma zdvd_zmult_cancel_disj[simp]:
@@ -1371,8 +1304,8 @@
then show ?thesis by (simp only: negative_eq_positive) auto
qed
qed
- then show ?thesis by (auto elim!: dvdE simp only: zmult_int [symmetric])
-qed
+ then show ?thesis by (auto elim!: dvdE simp only: zdvd_triv_left int_mult)
+qed
lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
proof
@@ -1404,10 +1337,10 @@
by (auto simp add: dvd_int_iff)
lemma zminus_dvd_iff [iff]: "(-z dvd w) = (z dvd (w::int))"
- by (simp add: zdvd_zminus2_iff)
+ by (rule minus_dvd_iff)
lemma dvd_zminus_iff [iff]: "(z dvd -w) = (z dvd (w::int))"
- by (simp add: zdvd_zminus_iff)
+ by (rule dvd_minus_iff)
lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
apply (rule_tac z=n in int_cases)
@@ -1449,20 +1382,13 @@
text {* by Brian Huffman *}
lemma zminus_zmod: "- ((x::int) mod m) mod m = - x mod m"
-by (simp only: zmod_zminus1_eq_if mod_mod_trivial)
+by (rule mod_minus_eq [symmetric])
lemma zdiff_zmod_left: "(x mod m - y) mod m = (x - y) mod (m::int)"
-by (simp only: diff_def zmod_zadd_left_eq [symmetric])
+by (rule mod_diff_left_eq [symmetric])
lemma zdiff_zmod_right: "(x - y mod m) mod m = (x - y) mod (m::int)"
-proof -
- have "(x + - (y mod m) mod m) mod m = (x + - y mod m) mod m"
- by (simp only: zminus_zmod)
- hence "(x + - (y mod m)) mod m = (x + - y) mod m"
- by (simp only: zmod_zadd_right_eq [symmetric])
- thus "(x - y mod m) mod m = (x - y) mod m"
- by (simp only: diff_def)
-qed
+by (rule mod_diff_right_eq [symmetric])
lemmas zmod_simps =
IntDiv.zmod_zadd_left_eq [symmetric]
--- a/src/HOL/NatBin.thy Thu Jan 08 17:25:06 2009 +0100
+++ b/src/HOL/NatBin.thy Thu Jan 08 21:13:40 2009 -0800
@@ -29,14 +29,14 @@
unfolding nat_number_of_def ..
abbreviation (xsymbols)
- square :: "'a::power => 'a" ("(_\<twosuperior>)" [1000] 999) where
+ power2 :: "'a::power => 'a" ("(_\<twosuperior>)" [1000] 999) where
"x\<twosuperior> == x^2"
notation (latex output)
- square ("(_\<twosuperior>)" [1000] 999)
+ power2 ("(_\<twosuperior>)" [1000] 999)
notation (HTML output)
- square ("(_\<twosuperior>)" [1000] 999)
+ power2 ("(_\<twosuperior>)" [1000] 999)
subsection {* Predicate for negative binary numbers *}
--- a/src/HOL/Ring_and_Field.thy Thu Jan 08 17:25:06 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy Thu Jan 08 21:13:40 2009 -0800
@@ -235,19 +235,21 @@
lemma minus_mult_right: "- (a * b) = a * - b"
by (rule equals_zero_I) (simp add: right_distrib [symmetric])
+text{*Extract signs from products*}
+lemmas mult_minus_left [simp] = minus_mult_left [symmetric]
+lemmas mult_minus_right [simp] = minus_mult_right [symmetric]
+
lemma minus_mult_minus [simp]: "- a * - b = a * b"
- by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])
+ by simp
lemma minus_mult_commute: "- a * b = a * - b"
- by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])
+ by simp
lemma right_diff_distrib: "a * (b - c) = a * b - a * c"
- by (simp add: right_distrib diff_minus
- minus_mult_left [symmetric] minus_mult_right [symmetric])
+ by (simp add: right_distrib diff_minus)
lemma left_diff_distrib: "(a - b) * c = a * c - b * c"
- by (simp add: left_distrib diff_minus
- minus_mult_left [symmetric] minus_mult_right [symmetric])
+ by (simp add: left_distrib diff_minus)
lemmas ring_distribs =
right_distrib left_distrib left_diff_distrib right_diff_distrib
@@ -293,6 +295,33 @@
subclass ring_1 ..
subclass comm_semiring_1_cancel ..
+lemma dvd_minus_iff: "x dvd - y \<longleftrightarrow> x dvd y"
+proof
+ assume "x dvd - y"
+ then have "x dvd - 1 * - y" by (rule dvd_mult)
+ then show "x dvd y" by simp
+next
+ assume "x dvd y"
+ then have "x dvd - 1 * y" by (rule dvd_mult)
+ then show "x dvd - y" by simp
+qed
+
+lemma minus_dvd_iff: "- x dvd y \<longleftrightarrow> x dvd y"
+proof
+ assume "- x dvd y"
+ then obtain k where "y = - x * k" ..
+ then have "y = x * - k" by simp
+ then show "x dvd y" ..
+next
+ assume "x dvd y"
+ then obtain k where "y = x * k" ..
+ then have "y = - x * - k" by simp
+ then show "- x dvd y" ..
+qed
+
+lemma dvd_diff: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
+ by (simp add: diff_minus dvd_add dvd_minus_iff)
+
end
class ring_no_zero_divisors = ring + no_zero_divisors
@@ -397,67 +426,47 @@
apply auto
done
-lemma nonzero_inverse_minus_eq:
- assumes "a \<noteq> 0"
- shows "inverse (- a) = - inverse a"
-proof -
- have "- a * inverse (- a) = - a * - inverse a"
- using assms by simp
- then show ?thesis unfolding mult_cancel_left using assms by simp
-qed
-
-lemma nonzero_inverse_inverse_eq:
- assumes "a \<noteq> 0"
- shows "inverse (inverse a) = a"
-proof -
- have "(inverse (inverse a) * inverse a) * a = a"
- using assms by (simp add: nonzero_imp_inverse_nonzero)
- then show ?thesis using assms by (simp add: mult_assoc)
-qed
-
-lemma nonzero_inverse_eq_imp_eq:
- assumes inveq: "inverse a = inverse b"
- and anz: "a \<noteq> 0"
- and bnz: "b \<noteq> 0"
- shows "a = b"
-proof -
- have "a * inverse b = a * inverse a"
- by (simp add: inveq)
- hence "(a * inverse b) * b = (a * inverse a) * b"
- by simp
- then show "a = b"
- by (simp add: mult_assoc anz bnz)
-qed
-
-lemma inverse_1 [simp]: "inverse 1 = 1"
-proof -
- have "inverse 1 * 1 = 1"
- by (rule left_inverse) (rule one_neq_zero)
- then show ?thesis by simp
-qed
-
lemma inverse_unique:
assumes ab: "a * b = 1"
shows "inverse a = b"
proof -
have "a \<noteq> 0" using ab by (cases "a = 0") simp_all
- moreover have "inverse a * (a * b) = inverse a" by (simp add: ab)
- ultimately show ?thesis by (simp add: mult_assoc [symmetric])
+ moreover have "inverse a * (a * b) = inverse a" by (simp add: ab)
+ ultimately show ?thesis by (simp add: mult_assoc [symmetric])
qed
+lemma nonzero_inverse_minus_eq:
+ "a \<noteq> 0 \<Longrightarrow> inverse (- a) = - inverse a"
+ by (rule inverse_unique) simp
+
+lemma nonzero_inverse_inverse_eq:
+ "a \<noteq> 0 \<Longrightarrow> inverse (inverse a) = a"
+ by (rule inverse_unique) simp
+
+lemma nonzero_inverse_eq_imp_eq:
+ assumes "inverse a = inverse b" and "a \<noteq> 0" and "b \<noteq> 0"
+ shows "a = b"
+proof -
+ from `inverse a = inverse b`
+ have "inverse (inverse a) = inverse (inverse b)"
+ by (rule arg_cong)
+ with `a \<noteq> 0` and `b \<noteq> 0` show "a = b"
+ by (simp add: nonzero_inverse_inverse_eq)
+qed
+
+lemma inverse_1 [simp]: "inverse 1 = 1"
+ by (rule inverse_unique) simp
+
lemma nonzero_inverse_mult_distrib:
- assumes anz: "a \<noteq> 0"
- and bnz: "b \<noteq> 0"
+ assumes "a \<noteq> 0" and "b \<noteq> 0"
shows "inverse (a * b) = inverse b * inverse a"
proof -
- have "inverse (a * b) * (a * b) * inverse b = inverse b"
- by (simp add: anz bnz)
- hence "inverse (a * b) * a = inverse b"
- by (simp add: mult_assoc bnz)
- hence "inverse (a * b) * a * inverse a = inverse b * inverse a"
- by simp
+ have "a * (b * inverse b) * inverse a = 1"
+ using assms by simp
+ hence "a * b * (inverse b * inverse a) = 1"
+ by (simp only: mult_assoc)
thus ?thesis
- by (simp add: mult_assoc anz)
+ by (rule inverse_unique)
qed
lemma division_ring_inverse_add:
@@ -1266,19 +1275,19 @@
subsection {* Division and Unary Minus *}
lemma nonzero_minus_divide_left: "b \<noteq> 0 ==> - (a/b) = (-a) / (b::'a::field)"
-by (simp add: divide_inverse minus_mult_left)
+by (simp add: divide_inverse)
lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a/b) = a / -(b::'a::field)"
-by (simp add: divide_inverse nonzero_inverse_minus_eq minus_mult_right)
+by (simp add: divide_inverse nonzero_inverse_minus_eq)
lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a)/(-b) = a / (b::'a::field)"
by (simp add: divide_inverse nonzero_inverse_minus_eq)
lemma minus_divide_left: "- (a/b) = (-a) / (b::'a::field)"
-by (simp add: divide_inverse minus_mult_left [symmetric])
+by (simp add: divide_inverse)
lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
-by (simp add: divide_inverse minus_mult_right [symmetric])
+by (simp add: divide_inverse)
text{*The effect is to extract signs from divisions*}
@@ -1286,11 +1295,6 @@
lemmas divide_minus_right = minus_divide_right [symmetric]
declare divide_minus_left [simp] divide_minus_right [simp]
-text{*Also, extract signs from products*}
-lemmas mult_minus_left = minus_mult_left [symmetric]
-lemmas mult_minus_right = minus_mult_right [symmetric]
-declare mult_minus_left [simp] mult_minus_right [simp]
-
lemma minus_divide_divide [simp]:
"(-a)/(-b) = a / (b::'a::{field,division_by_zero})"
apply (cases "b=0", simp)
--- a/src/HOLCF/Tools/domain/domain_theorems.ML Thu Jan 08 17:25:06 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML Thu Jan 08 21:13:40 2009 -0800
@@ -10,6 +10,12 @@
structure Domain_Theorems = struct
+val quiet_mode = ref false;
+val trace_domain = ref false;
+
+fun message s = if !quiet_mode then () else writeln s;
+fun trace s = if !trace_domain then tracing s else ();
+
local
val adm_impl_admw = @{thm adm_impl_admw};
@@ -115,7 +121,7 @@
fun theorems (((dname, _), cons) : eq, eqs : eq list) thy =
let
-val dummy = writeln ("Proving isomorphism properties of domain "^dname^" ...");
+val _ = message ("Proving isomorphism properties of domain "^dname^" ...");
val pg = pg' thy;
(* ----- getting the axioms and definitions --------------------------------- *)
@@ -158,6 +164,8 @@
(* ----- generating beta reduction rules from definitions-------------------- *)
+val _ = trace " Proving beta reduction rules...";
+
local
fun arglist (Const _ $ Abs (s, _, t)) =
let
@@ -179,7 +187,9 @@
in pg (def::betas) appl (K [rtac reflexive_thm 1]) end;
end;
+val _ = trace "Proving when_appl...";
val when_appl = appl_of_def ax_when_def;
+val _ = trace "Proving con_appls...";
val con_appls = map appl_of_def axs_con_def;
local
@@ -229,7 +239,9 @@
rewrite_goals_tac [mk_meta_eq iso_swap],
rtac thm3 1];
in
+ val _ = trace " Proving exhaust...";
val exhaust = pg con_appls (mk_trp exh) (K tacs);
+ val _ = trace " Proving casedist...";
val casedist =
standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
end;
@@ -239,6 +251,7 @@
fun bound_fun i _ = Bound (length cons - i);
val when_app = list_ccomb (%%:(dname^"_when"), mapn bound_fun 1 cons);
in
+ val _ = trace " Proving when_strict...";
val when_strict =
let
val axs = [when_appl, mk_meta_eq rep_strict];
@@ -246,6 +259,7 @@
val tacs = [resolve_tac [sscase1, ssplit1, strictify1] 1];
in pg axs goal (K tacs) end;
+ val _ = trace " Proving when_apps...";
val when_apps =
let
fun one_when n (con,args) =
@@ -276,6 +290,7 @@
val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
in pg axs_dis_def goal (K tacs) end;
+ val _ = trace " Proving dis_apps...";
val dis_apps = maps (fn (c,_) => map (dis_app c) cons) cons;
fun dis_defin (con, args) =
@@ -288,7 +303,9 @@
(asm_simp_tac (HOLCF_ss addsimps dis_apps) 1))];
in pg [] goal (K tacs) end;
+ val _ = trace " Proving dis_stricts...";
val dis_stricts = map dis_strict cons;
+ val _ = trace " Proving dis_defins...";
val dis_defins = map dis_defin cons;
in
val dis_rews = dis_stricts @ dis_defins @ dis_apps;
@@ -301,6 +318,7 @@
val tacs = [rtac when_strict 1];
in pg axs_mat_def goal (K tacs) end;
+ val _ = trace " Proving mat_stricts...";
val mat_stricts = map mat_strict cons;
fun one_mat c (con, args) =
@@ -314,6 +332,7 @@
val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
in pg axs_mat_def goal (K tacs) end;
+ val _ = trace " Proving mat_apps...";
val mat_apps =
maps (fn (c,_) => map (one_mat c) cons) cons;
in
@@ -346,7 +365,9 @@
val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
in pg axs goal (K tacs) end;
+ val _ = trace " Proving pat_stricts...";
val pat_stricts = map pat_strict cons;
+ val _ = trace " Proving pat_apps...";
val pat_apps = maps (fn c => map (pat_app c) cons) cons;
in
val pat_rews = pat_stricts @ pat_apps;
@@ -374,7 +395,9 @@
asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
in pg [] goal tacs end;
in
+ val _ = trace " Proving con_stricts...";
val con_stricts = maps con_strict cons;
+ val _ = trace " Proving pat_defins...";
val con_defins = map con_defin cons;
val con_rews = con_stricts @ con_defins;
end;
@@ -391,6 +414,7 @@
REPEAT (resolve_tac rules 1 ORELSE atac 1)];
in pg con_appls goal (K tacs) end;
in
+ val _ = trace " Proving con_compacts...";
val con_compacts = map con_compact cons;
end;
@@ -402,6 +426,7 @@
fun sel_strict (_, args) =
List.mapPartial (Option.map one_sel o sel_of) args;
in
+ val _ = trace " Proving sel_stricts...";
val sel_stricts = maps sel_strict cons;
end;
@@ -439,6 +464,7 @@
fun one_con (c, args) =
flat (map_filter I (mapn (one_sel' c) 0 args));
in
+ val _ = trace " Proving sel_apps...";
val sel_apps = maps one_con cons;
end;
@@ -453,6 +479,7 @@
(asm_simp_tac (HOLCF_ss addsimps sel_apps) 1))];
in pg [] goal (K tacs) end;
in
+ val _ = trace " Proving sel_defins...";
val sel_defins =
if length cons = 1
then List.mapPartial (fn arg => Option.map sel_defin (sel_of arg))
@@ -463,6 +490,7 @@
val sel_rews = sel_stricts @ sel_defins @ sel_apps;
val rev_contrapos = @{thm rev_contrapos};
+val _ = trace " Proving dist_les...";
val distincts_le =
let
fun dist (con1, args1) (con2, args2) =
@@ -487,6 +515,8 @@
| distincts (c::cs) = (map (distinct c) cs) :: distincts cs;
in distincts cons end;
val dist_les = flat (flat distincts_le);
+
+val _ = trace " Proving dist_eqs...";
val dist_eqs =
let
fun distinct (_,args1) ((_,args2), leqs) =
@@ -517,6 +547,7 @@
in pg con_appls prop end;
val cons' = List.filter (fn (_,args) => args<>[]) cons;
in
+ val _ = trace " Proving inverts...";
val inverts =
let
val abs_less = ax_abs_iso RS (allI RS injection_less);
@@ -524,6 +555,7 @@
[asm_full_simp_tac (HOLCF_ss addsimps [abs_less, spair_less]) 1];
in map (fn (con, args) => pgterm (op <<) con args (K tacs)) cons' end;
+ val _ = trace " Proving injects...";
val injects =
let
val abs_eq = ax_abs_iso RS (allI RS injection_eq);
@@ -551,6 +583,7 @@
val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_apps) 1];
in pg [ax_copy_def] goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
in
+ val _ = trace " Proving copy_apps...";
val copy_apps = map copy_app cons;
end;
@@ -565,6 +598,7 @@
fun has_nonlazy_rec (_, args) = exists is_nonlazy_rec args;
in
+ val _ = trace " Proving copy_stricts...";
val copy_stricts = map one_strict (List.filter has_nonlazy_rec cons);
end;
@@ -603,7 +637,7 @@
val conss = map snd eqs;
val comp_dname = Sign.full_bname thy comp_dnam;
-val d = writeln("Proving induction properties of domain "^comp_dname^" ...");
+val _ = message ("Proving induction properties of domain "^comp_dname^" ...");
val pg = pg' thy;
(* ----- getting the composite axiom and definitions ------------------------ *)
@@ -639,6 +673,7 @@
val copy_con_rews = copy_rews @ con_rews;
val copy_take_defs =
(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
+ val _ = trace " Proving take_stricts...";
val take_stricts =
let
fun one_eq ((dn, args), _) = strict (dc_take dn $ %:"n");
@@ -656,6 +691,7 @@
in pg axs_take_def goal (K [simp_tac iterate_Cprod_ss 1]) end;
val take_0s = mapn take_0 1 dnames;
fun c_UU_tac ctxt = case_UU_tac ctxt (take_stricts'::copy_con_rews) 1;
+ val _ = trace " Proving take_apps...";
val take_apps =
let
fun mk_eqn dn (con, args) =
@@ -737,6 +773,7 @@
val is_finite = forall (not o lazy_rec_to [] false) n__eqs;
end;
in (* local *)
+ val _ = trace " Proving finite_ind...";
val finite_ind =
let
fun concf n dn = %:(P_name n) $ (dc_take dn $ %:"n" `%(x_name n));
@@ -768,6 +805,7 @@
end;
in pg'' thy [] goal tacf end;
+ val _ = trace " Proving take_lemmas...";
val take_lemmas =
let
fun take_lemma n (dn, ax_reach) =
@@ -793,6 +831,7 @@
(* ----- theorems concerning finiteness and induction ----------------------- *)
+ val _ = trace " Proving finites, ind...";
val (finites, ind) =
if is_finite
then (* finite case *)
@@ -914,6 +953,7 @@
fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1);
val take_ss = HOL_ss addsimps take_rews;
val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")"));
+ val _ = trace " Proving coind_lemma...";
val coind_lemma =
let
fun mk_prj n _ = proj (%:"R") eqs n $ bnd_arg n 0 $ bnd_arg n 1;
@@ -940,6 +980,7 @@
flat (mapn (x_tacs ctxt) 0 xs);
in pg [ax_bisim_def] goal tacs end;
in
+ val _ = trace " Proving coind...";
val coind =
let
fun mk_prj n x = mk_trp (proj (%:"R") eqs n $ %:x $ %:(x^"'"));