added lemma
authornipkow
Tue May 20 15:59:16 2014 +0200 (2014-05-20)
changeset 57015842bb6d36263
parent 57014 b7999893ffcc
child 57016 c44ce6f4067d
added lemma
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Nat.thy	Tue May 20 09:57:10 2014 +0200
     1.2 +++ b/src/HOL/Nat.thy	Tue May 20 15:59:16 2014 +0200
     1.3 @@ -870,6 +870,10 @@
     1.4    then show "P n" by auto
     1.5  qed
     1.6  
     1.7 +
     1.8 +lemma Least_eq_0[simp]: "P(0::nat) \<Longrightarrow> Least P = 0"
     1.9 +by (rule Least_equality[OF _ le0])
    1.10 +
    1.11  lemma Least_Suc:
    1.12       "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
    1.13    apply (cases n, auto)