--- 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
--- 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
--- 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 +
--- 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)"
--- 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"
--- 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 *}
--- 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
--- 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]
--- 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"},