# HG changeset patch
# User blanchet
# Date 1484149411 -3600
# Node ID 65a2474441004d3db26b0c4343f023d131a00c94
# Parent  4efffde18a901e28ed6b9f703d19e5a02b2b5ef3
generalized types in lemmas

diff -r 4efffde18a90 -r 65a247444100 NEWS
--- 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
diff -r 4efffde18a90 -r 65a247444100 src/HOL/Nat.thy
--- 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