generalized types in lemmas
authorblanchet
Wed Jan 11 16:43:31 2017 +0100 (2017-01-11)
changeset 6487665a247444100
parent 64875 4efffde18a90
child 64877 31e9920a0dc1
generalized types in lemmas
NEWS
src/HOL/Nat.thy
     1.1 --- a/NEWS	Wed Jan 11 16:28:48 2017 +0100
     1.2 +++ b/NEWS	Wed Jan 11 16:43:31 2017 +0100
     1.3 @@ -58,6 +58,8 @@
     1.4  mod_diff_eq.  INCOMPATIBILITY.
     1.5  
     1.6  * Generalized some facts:
     1.7 +    measure_induct_rule
     1.8 +    measure_induct
     1.9      zminus_zmod ~> mod_minus_eq
    1.10      zdiff_zmod_left ~> mod_diff_left_eq
    1.11      zdiff_zmod_right ~> mod_diff_right_eq
     2.1 --- a/src/HOL/Nat.thy	Wed Jan 11 16:28:48 2017 +0100
     2.2 +++ b/src/HOL/Nat.thy	Wed Jan 11 16:43:31 2017 +0100
     2.3 @@ -1013,14 +1013,14 @@
     2.4    using assms less_induct by blast
     2.5  
     2.6  lemma measure_induct_rule [case_names less]:
     2.7 -  fixes f :: "'a \<Rightarrow> nat"
     2.8 +  fixes f :: "'a \<Rightarrow> 'b::wellorder"
     2.9    assumes step: "\<And>x. (\<And>y. f y < f x \<Longrightarrow> P y) \<Longrightarrow> P x"
    2.10    shows "P a"
    2.11    by (induct m \<equiv> "f a" arbitrary: a rule: less_induct) (auto intro: step)
    2.12  
    2.13  text \<open>old style induction rules:\<close>
    2.14  lemma measure_induct:
    2.15 -  fixes f :: "'a \<Rightarrow> nat"
    2.16 +  fixes f :: "'a \<Rightarrow> 'b::wellorder"
    2.17    shows "(\<And>x. \<forall>y. f y < f x \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a"
    2.18    by (rule measure_induct_rule [of f P a]) iprover
    2.19