equal
deleted
inserted
replaced
562 apply (case_tac n) |
562 apply (case_tac n) |
563 apply (case_tac [2] nat) |
563 apply (case_tac [2] nat) |
564 apply (blast intro: less_trans)+ |
564 apply (blast intro: less_trans)+ |
565 done |
565 done |
566 |
566 |
567 subsection {* @{text LEAST} theorems for type @{typ nat} by specialization *} |
567 subsection {* @{text LEAST} theorems for type @{typ nat}*} |
568 |
|
569 lemmas LeastI = wellorder_LeastI |
|
570 lemmas Least_le = wellorder_Least_le |
|
571 lemmas not_less_Least = wellorder_not_less_Least |
|
572 |
568 |
573 lemma Least_Suc: |
569 lemma Least_Suc: |
574 "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))" |
570 "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))" |
575 apply (case_tac "n", auto) |
571 apply (case_tac "n", auto) |
576 apply (frule LeastI) |
572 apply (frule LeastI) |