# HG changeset patch
# User haftmann
# Date 1483984400 -3600
# Node ID 766db3539859a6af6eddbad952999c9b95d84c9d
# Parent  c50db21280482517eeb10a00d5e60051cfd3a7f9
moved some lemmas to appropriate places

diff -r c50db2128048 -r 766db3539859 src/HOL/Int.thy
--- 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>
 
diff -r c50db2128048 -r 766db3539859 src/HOL/Library/Polynomial.thy
--- 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)
diff -r c50db2128048 -r 766db3539859 src/HOL/Nat.thy
--- 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)
 
diff -r c50db2128048 -r 766db3539859 src/HOL/Rat.thy
--- 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)