# HG changeset patch
# User blanchet
# Date 1412273040 -7200
# Node ID 07901e99565c56dc6eb07f49018bf8ece4d9f448
# Parent  64f6b4bd52a7ccfd2683c73a3a15a0e7fcbaafd3# Parent  0bf0cf1d3547c5662b57646de0e004f310005521
merge

diff -r 64f6b4bd52a7 -r 07901e99565c NEWS
--- a/NEWS	Thu Oct 02 18:10:09 2014 +0200
+++ b/NEWS	Thu Oct 02 20:04:00 2014 +0200
@@ -32,6 +32,9 @@
 
 *** HOL ***
 
+* Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1
+Minor INCOMPATIBILITY.
+
 * Bootstrap of listsum as special case of abstract product over lists.
 Fact rename:
     listsum_def ~> listsum.eq_foldr
diff -r 64f6b4bd52a7 -r 07901e99565c src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Oct 02 18:10:09 2014 +0200
+++ b/src/HOL/Divides.thy	Thu Oct 02 20:04:00 2014 +0200
@@ -2425,16 +2425,6 @@
 
 subsubsection {* The Divides Relation *}
 
-lemma dvd_neg_numeral_left [simp]:
-  fixes y :: "'a::comm_ring_1"
-  shows "(- numeral k) dvd y \<longleftrightarrow> (numeral k) dvd y"
-  by (fact minus_dvd_iff)
-
-lemma dvd_neg_numeral_right [simp]:
-  fixes x :: "'a::comm_ring_1"
-  shows "x dvd (- numeral k) \<longleftrightarrow> x dvd (numeral k)"
-  by (fact dvd_minus_iff)
-
 lemmas dvd_eq_mod_eq_0_numeral [simp] =
   dvd_eq_mod_eq_0 [of "numeral x" "numeral y"] for x y
 
diff -r 64f6b4bd52a7 -r 07901e99565c src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Thu Oct 02 18:10:09 2014 +0200
+++ b/src/HOL/Fields.thy	Thu Oct 02 20:04:00 2014 +0200
@@ -375,6 +375,9 @@
   "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (x / y = w / z) = (x * z = w * y)"
   by (simp add: field_simps)
 
+lemma divide_minus1 [simp]: "x / - 1 = - x"
+  using nonzero_minus_divide_right [of "1" x] by simp
+  
 end
 
 class field_inverse_zero = field +
diff -r 64f6b4bd52a7 -r 07901e99565c src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Thu Oct 02 18:10:09 2014 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Thu Oct 02 20:04:00 2014 +0200
@@ -255,8 +255,7 @@
 lemma effect_nthE [effect_elims]:
   assumes "effect (nth a i) h h' r"
   obtains "i < length h a" "r = get h a ! i" "h' = h"
-  using assms by (rule effectE)
-    (erule successE, cases "i < length h a", simp_all add: execute_simps)
+  using assms by (rule effectE) (cases "i < length h a", auto simp: execute_simps elim: successE)
 
 lemma execute_upd [execute_simps]:
   "i < length h a \<Longrightarrow>
@@ -276,8 +275,7 @@
 lemma effect_updE [effect_elims]:
   assumes "effect (upd i v a) h h' r"
   obtains "r = a" "h' = update a i v h" "i < length h a"
-  using assms by (rule effectE)
-    (erule successE, cases "i < length h a", simp_all add: execute_simps)
+  using assms by (rule effectE) (cases "i < length h a", auto simp: execute_simps elim: successE)
 
 lemma execute_map_entry [execute_simps]:
   "i < length h a \<Longrightarrow>
@@ -298,8 +296,7 @@
 lemma effect_map_entryE [effect_elims]:
   assumes "effect (map_entry i f a) h h' r"
   obtains "r = a" "h' = update a i (f (get h a ! i)) h" "i < length h a"
-  using assms by (rule effectE)
-    (erule successE, cases "i < length h a", simp_all add: execute_simps)
+  using assms by (rule effectE) (cases "i < length h a", auto simp: execute_simps elim: successE)
 
 lemma execute_swap [execute_simps]:
   "i < length h a \<Longrightarrow>
@@ -320,8 +317,7 @@
 lemma effect_swapE [effect_elims]:
   assumes "effect (swap i x a) h h' r"
   obtains "r = get h a ! i" "h' = update a i x h" "i < length h a"
-  using assms by (rule effectE)
-    (erule successE, cases "i < length h a", simp_all add: execute_simps)
+  using assms by (rule effectE) (cases "i < length h a", auto simp: execute_simps elim: successE)
 
 lemma execute_freeze [execute_simps]:
   "execute (freeze a) h = Some (get h a, h)"
diff -r 64f6b4bd52a7 -r 07901e99565c src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Oct 02 18:10:09 2014 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Oct 02 20:04:00 2014 +0200
@@ -82,10 +82,8 @@
 
 lemma successE:
   assumes "success f h"
-  obtains r h' where "r = fst (the (execute c h))"
-    and "h' = snd (the (execute c h))"
-    and "execute f h \<noteq> None"
-  using assms by (simp add: success_def)
+  obtains r h' where "execute f h = Some (r, h')"
+  using assms by (auto simp: success_def)
 
 named_theorems success_intros "introduction rules for success"
 
@@ -266,11 +264,11 @@
 
 lemma execute_bind_success:
   "success f h \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))"
-  by (cases f h rule: Heap_cases) (auto elim!: successE simp add: bind_def)
+  by (cases f h rule: Heap_cases) (auto elim: successE simp add: bind_def)
 
 lemma success_bind_executeI:
   "execute f h = Some (x, h') \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
-  by (auto intro!: successI elim!: successE simp add: bind_def)
+  by (auto intro!: successI elim: successE simp add: bind_def)
 
 lemma success_bind_effectI [success_intros]:
   "effect f h h' x \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
diff -r 64f6b4bd52a7 -r 07901e99565c src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu Oct 02 18:10:09 2014 +0200
+++ b/src/HOL/Int.thy	Thu Oct 02 20:04:00 2014 +0200
@@ -1217,21 +1217,6 @@
   divide_less_eq_numeral eq_divide_eq_numeral divide_eq_eq_numeral
   le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
 
-text{*Division By @{text "-1"}*}
-
-lemma divide_minus1 [simp]: "(x::'a::field) / -1 = - x"
-  unfolding nonzero_minus_divide_right [OF one_neq_zero, symmetric]
-  by simp
-
-lemma half_gt_zero_iff:
-  "(0 < r/2) = (0 < (r::'a::linordered_field_inverse_zero))"
-  by auto
-
-lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2]
-
-lemma divide_Numeral1: "(x::'a::field) / Numeral1 = x"
-  by (fact divide_numeral_1)
-
 
 subsection {* The divides relation *}
 
diff -r 64f6b4bd52a7 -r 07901e99565c src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Thu Oct 02 18:10:09 2014 +0200
+++ b/src/HOL/Library/Polynomial.thy	Thu Oct 02 20:04:00 2014 +0200
@@ -1724,6 +1724,10 @@
 
 declare gcd_poly.simps [simp del]
 
+definition lcm_poly :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
+where
+  "lcm_poly a b = a * b div smult (coeff a (degree a) * coeff b (degree b)) (gcd a b)"
+
 instance ..
 
 end
diff -r 64f6b4bd52a7 -r 07901e99565c src/HOL/Num.thy
--- a/src/HOL/Num.thy	Thu Oct 02 18:10:09 2014 +0200
+++ b/src/HOL/Num.thy	Thu Oct 02 20:04:00 2014 +0200
@@ -1073,6 +1073,22 @@
 lemmas nat_1_add_1 = one_add_one [where 'a=nat] (* legacy *)
 
 
+subsection {* Particular lemmas concerning @{term 2} *}
+
+context linordered_field_inverse_zero
+begin
+
+lemma half_gt_zero_iff:
+  "0 < a / 2 \<longleftrightarrow> 0 < a" (is "?P \<longleftrightarrow> ?Q")
+  by (auto simp add: field_simps)
+
+lemma half_gt_zero [simp]:
+  "0 < a \<Longrightarrow> 0 < a / 2"
+  by (simp add: half_gt_zero_iff)
+
+end
+
+
 subsection {* Numeral equations as default simplification rules *}
 
 declare (in numeral) numeral_One [simp]
diff -r 64f6b4bd52a7 -r 07901e99565c src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Thu Oct 02 18:10:09 2014 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Thu Oct 02 20:04:00 2014 +0200
@@ -710,7 +710,7 @@
              name = "ord_frac_simproc", proc = proc3, identifier = []}
 
 val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
-           @{thm "divide_Numeral1"},
+           @{thm "divide_numeral_1"},
            @{thm "divide_zero"}, @{thm divide_zero_left},
            @{thm "divide_divide_eq_left"}, 
            @{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"},