--- a/src/HOL/Int.thy Mon Jan 09 18:53:06 2017 +0100
+++ b/src/HOL/Int.thy Mon Jan 09 18:53:20 2017 +0100
@@ -357,7 +357,6 @@
then show ?thesis ..
qed
-
end
text \<open>Comparisons involving @{term of_int}.\<close>
@@ -848,6 +847,13 @@
by simp
qed (auto elim!: Nats_cases)
+lemma (in idom_divide) of_int_divide_in_Ints:
+ "of_int a div of_int b \<in> \<int>" if "b dvd a"
+proof -
+ from that obtain c where "a = b * c" ..
+ then show ?thesis
+ by (cases "of_int b = 0") simp_all
+qed
text \<open>The premise involving @{term Ints} prevents @{term "a = 1/2"}.\<close>
--- a/src/HOL/Library/Polynomial.thy Mon Jan 09 18:53:06 2017 +0100
+++ b/src/HOL/Library/Polynomial.thy Mon Jan 09 18:53:20 2017 +0100
@@ -12,20 +12,6 @@
"~~/src/HOL/Library/Infinite_Set"
begin
-subsection \<open>Misc\<close>
-
-lemma quotient_of_denom_pos': "snd (quotient_of x) > 0"
- using quotient_of_denom_pos [OF surjective_pairing] .
-
-lemma (in idom_divide) of_int_divide_in_Ints:
- "of_int a div of_int b \<in> \<int>" if "b dvd a"
-proof -
- from that obtain c where "a = b * c" ..
- then show ?thesis
- by (cases "of_int b = 0") simp_all
-qed
-
-
subsection \<open>Auxiliary: operations for lists (later) representing coefficients\<close>
definition cCons :: "'a::zero \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "##" 65)
--- a/src/HOL/Nat.thy Mon Jan 09 18:53:06 2017 +0100
+++ b/src/HOL/Nat.thy Mon Jan 09 18:53:20 2017 +0100
@@ -170,6 +170,28 @@
text \<open>Injectiveness and distinctness lemmas\<close>
+lemma (in semidom_divide) inj_times:
+ "inj (times a)" if "a \<noteq> 0"
+proof (rule injI)
+ fix b c
+ assume "a * b = a * c"
+ then have "a * b div a = a * c div a"
+ by (simp only:)
+ with that show "b = c"
+ by simp
+qed
+
+lemma (in cancel_ab_semigroup_add) inj_plus:
+ "inj (plus a)"
+proof (rule injI)
+ fix b c
+ assume "a + b = a + c"
+ then have "a + b - a = a + c - a"
+ by (simp only:)
+ then show "b = c"
+ by simp
+qed
+
lemma inj_Suc[simp]: "inj_on Suc N"
by (simp add: inj_on_def)
--- a/src/HOL/Rat.thy Mon Jan 09 18:53:06 2017 +0100
+++ b/src/HOL/Rat.thy Mon Jan 09 18:53:20 2017 +0100
@@ -401,6 +401,9 @@
lemma quotient_of_denom_pos: "quotient_of r = (p, q) \<Longrightarrow> q > 0"
by (cases r) (simp add: quotient_of_Fract normalize_denom_pos)
+lemma quotient_of_denom_pos': "snd (quotient_of r) > 0"
+ using quotient_of_denom_pos [of r] by (simp add: prod_eq_iff)
+
lemma quotient_of_coprime: "quotient_of r = (p, q) \<Longrightarrow> coprime p q"
by (cases r) (simp add: quotient_of_Fract normalize_coprime)