equal
deleted
inserted
replaced
201 constdefs |
201 constdefs |
202 Least :: "('a::ord => bool) => 'a" (binder "LEAST " 10) |
202 Least :: "('a::ord => bool) => 'a" (binder "LEAST " 10) |
203 "Least P == THE x. P x & (ALL y. P y --> x <= y)" |
203 "Least P == THE x. P x & (ALL y. P y --> x <= y)" |
204 -- {* We can no longer use LeastM because the latter requires Hilbert-AC. *} |
204 -- {* We can no longer use LeastM because the latter requires Hilbert-AC. *} |
205 |
205 |
206 lemma LeastI2: |
206 lemma LeastI2_order: |
207 "[| P (x::'a::order); |
207 "[| P (x::'a::order); |
208 !!y. P y ==> x <= y; |
208 !!y. P y ==> x <= y; |
209 !!x. [| P x; ALL y. P y --> x \<le> y |] ==> Q x |] |
209 !!x. [| P x; ALL y. P y --> x \<le> y |] ==> Q x |] |
210 ==> Q (Least P)" |
210 ==> Q (Least P)" |
211 apply (unfold Least_def) |
211 apply (unfold Least_def) |