equal
deleted
inserted
replaced
868 qed |
868 qed |
869 qed |
869 qed |
870 then show "P n" by auto |
870 then show "P n" by auto |
871 qed |
871 qed |
872 |
872 |
|
873 |
|
874 lemma Least_eq_0[simp]: "P(0::nat) \<Longrightarrow> Least P = 0" |
|
875 by (rule Least_equality[OF _ le0]) |
|
876 |
873 lemma Least_Suc: |
877 lemma Least_Suc: |
874 "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))" |
878 "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))" |
875 apply (cases n, auto) |
879 apply (cases n, auto) |
876 apply (frule LeastI) |
880 apply (frule LeastI) |
877 apply (drule_tac P = "%x. P (Suc x) " in LeastI) |
881 apply (drule_tac P = "%x. P (Suc x) " in LeastI) |