--- a/NEWS Wed Jan 11 16:28:48 2017 +0100
+++ b/NEWS Wed Jan 11 16:43:31 2017 +0100
@@ -58,6 +58,8 @@
mod_diff_eq. INCOMPATIBILITY.
* Generalized some facts:
+ measure_induct_rule
+ measure_induct
zminus_zmod ~> mod_minus_eq
zdiff_zmod_left ~> mod_diff_left_eq
zdiff_zmod_right ~> mod_diff_right_eq
--- a/src/HOL/Nat.thy Wed Jan 11 16:28:48 2017 +0100
+++ b/src/HOL/Nat.thy Wed Jan 11 16:43:31 2017 +0100
@@ -1013,14 +1013,14 @@
using assms less_induct by blast
lemma measure_induct_rule [case_names less]:
- fixes f :: "'a \<Rightarrow> nat"
+ fixes f :: "'a \<Rightarrow> 'b::wellorder"
assumes step: "\<And>x. (\<And>y. f y < f x \<Longrightarrow> P y) \<Longrightarrow> P x"
shows "P a"
by (induct m \<equiv> "f a" arbitrary: a rule: less_induct) (auto intro: step)
text \<open>old style induction rules:\<close>
lemma measure_induct:
- fixes f :: "'a \<Rightarrow> nat"
+ fixes f :: "'a \<Rightarrow> 'b::wellorder"
shows "(\<And>x. \<forall>y. f y < f x \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a"
by (rule measure_induct_rule [of f P a]) iprover