# HG changeset patch
# User nipkow
# Date 1115797833 -7200
# Node ID 5c067c956a20f282b430829f57db8b472f3e5852
# Parent  fd02dd265b783f40a03029bc24fa81f09d1448a0
Added thms by Brian Huffmann

diff -r fd02dd265b78 -r 5c067c956a20 src/HOL/Orderings.thy
--- 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 |]
diff -r fd02dd265b78 -r 5c067c956a20 src/HOL/Set.thy
--- 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
 
diff -r fd02dd265b78 -r 5c067c956a20 src/HOL/Wellfounded_Recursion.thy
--- 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)