--- a/src/HOL/Orderings.thy Tue May 10 18:37:43 2005 +0200
+++ b/src/HOL/Orderings.thy Wed May 11 09:50:33 2005 +0200
@@ -203,7 +203,7 @@
"Least P == THE x. P x & (ALL y. P y --> x <= y)"
-- {* We can no longer use LeastM because the latter requires Hilbert-AC. *}
-lemma LeastI2:
+lemma LeastI2_order:
"[| P (x::'a::order);
!!y. P y ==> x <= y;
!!x. [| P x; ALL y. P y --> x \<le> y |] ==> Q x |]
--- a/src/HOL/Set.thy Tue May 10 18:37:43 2005 +0200
+++ b/src/HOL/Set.thy Wed May 11 09:50:33 2005 +0200
@@ -1976,8 +1976,8 @@
==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
-- {* Courtesy of Stephan Merz *}
apply clarify
- apply (erule_tac P = "%x. x : S" in LeastI2, fast)
- apply (rule LeastI2)
+ apply (erule_tac P = "%x. x : S" in LeastI2_order, fast)
+ apply (rule LeastI2_order)
apply (auto elim: monoD intro!: order_antisym)
done
--- a/src/HOL/Wellfounded_Recursion.thy Tue May 10 18:37:43 2005 +0200
+++ b/src/HOL/Wellfounded_Recursion.thy Wed May 11 09:50:33 2005 +0200
@@ -314,6 +314,20 @@
lemmas LeastI = wellorder_Least_lemma [THEN conjunct1, standard]
lemmas Least_le = wellorder_Least_lemma [THEN conjunct2, standard]
+-- "The following 3 lemmas are due to Brian Huffman"
+lemma LeastI_ex: "EX x::'a::wellorder. P x ==> P (Least P)"
+apply (erule exE)
+apply (erule LeastI)
+done
+
+lemma LeastI2:
+ "[| P (a::'a::wellorder); !!x. P x ==> Q x |] ==> Q (Least P)"
+by (blast intro: LeastI)
+
+lemma LeastI2_ex:
+ "[| EX a::'a::wellorder. P a; !!x. P x ==> Q x |] ==> Q (Least P)"
+by (blast intro: LeastI_ex)
+
lemma not_less_Least: "[| k < (LEAST x. P x) |] ==> ~P (k::'a::wellorder)"
apply (simp (no_asm_use) add: linorder_not_le [symmetric])
apply (erule contrapos_nn)