src/HOL/Nat.thy
changeset 66295 1ec601d9c829
parent 66290 88714f2e40e8
child 66386 962c12353c67
     1.1 --- a/src/HOL/Nat.thy	Mon Jul 24 16:50:46 2017 +0100
     1.2 +++ b/src/HOL/Nat.thy	Wed Jul 26 13:36:36 2017 +0100
     1.3 @@ -2143,6 +2143,12 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +lemma transitive_stepwise_le:
     1.8 +  assumes "m \<le> n" "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" and "\<And>n. R n (Suc n)"
     1.9 +  shows "R m n"
    1.10 +using \<open>m \<le> n\<close>  
    1.11 +  by (induction rule: dec_induct) (use assms in blast)+
    1.12 +
    1.13  
    1.14  subsubsection \<open>Greatest operator\<close>
    1.15