# HG changeset patch
# User paulson
# Date 979121670 -3600
# Node ID e1a793957a8f43326a09f33293fc6762667bbf66
# Parent  de981d0037edc590a5db346eefebf8409af684a3
generalizing the LEAST theorems from "nat" to linear
orderings and wellorderings

diff -r de981d0037ed -r e1a793957a8f src/HOL/Datatype_Universe.ML
--- a/src/HOL/Datatype_Universe.ML	Wed Jan 10 11:13:11 2001 +0100
+++ b/src/HOL/Datatype_Universe.ML	Wed Jan 10 11:14:30 2001 +0100
@@ -209,15 +209,14 @@
 Goalw [ndepth_def] "ndepth (Abs_Node(%k. Inr 0, x)) = 0";
 by (EVERY1[stac (Node_K0_I RS Abs_Node_inverse), stac split]);
 by (rtac Least_equality 1);
-by (rtac refl 1);
-by (etac less_zeroE 1);
+by Auto_tac;  
 qed "ndepth_K0";
 
-Goal "k < Suc(LEAST x. f x = Inr 0) --> nat_case (Inr (Suc i)) f k ~= Inr 0";
+Goal "nat_case (Inr (Suc i)) f k = Inr 0 --> Suc(LEAST x. f x = Inr 0) <= k";
 by (induct_tac "k" 1);
 by (ALLGOALS Simp_tac);
-by (rtac impI 1);
-by (etac not_less_Least 1);
+by (rtac impI 1); 
+by (etac Least_le 1);
 val lemma = result();
 
 Goalw [ndepth_def,Push_Node_def]
@@ -229,9 +228,8 @@
 by (Simp_tac 1);
 by (rtac Least_equality 1);
 by (rewtac Push_def);
-by (rtac (nat_case_Suc RS trans) 1);
+by (auto_tac (claset(), simpset() addsimps [lemma]));  
 by (etac LeastI 1);
-by (asm_simp_tac (simpset() addsimps [lemma]) 1);
 qed "ndepth_Push_Node";
 
 
diff -r de981d0037ed -r e1a793957a8f src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Wed Jan 10 11:13:11 2001 +0100
+++ b/src/HOL/Nat.ML	Wed Jan 10 11:14:30 2001 +0100
@@ -68,26 +68,6 @@
 by Auto_tac;
 qed "less_Suc_eq_0_disj";
 
-Goalw [Least_nat_def]
- "[| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))";
-by (rtac some_equality 1);
-by (fold_goals_tac [Least_nat_def]);
-by (safe_tac (claset() addSEs [LeastI]));
-by (rename_tac "j" 1);
-by (case_tac "j" 1);
-by (Blast_tac 1);
-by (blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1);
-by (rename_tac "k n" 1);
-by (case_tac "k" 1);
-by (Blast_tac 1);
-by (hyp_subst_tac 1);
-by (rewtac Least_nat_def);
-by (rtac (some_equality RS arg_cong RS sym) 1);
-by (blast_tac (claset() addDs [Suc_mono]) 1);
-by (cut_inst_tac [("m","m")] less_linear 1);
-by (blast_tac (claset() addIs [Suc_mono]) 1);
-qed "Least_Suc";
-
 val prems = Goal "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
 by (rtac nat_less_induct 1);
 by (case_tac "n" 1);
@@ -95,6 +75,73 @@
 by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans])));
 qed "nat_induct2";
 
+
+(*** LEAST -- the least number operator ***)
+
+(*This version is polymorphic over type class "order"! *) 
+Goalw [Least_def]
+     "[| P(k::'a::order);  ALL x. P x --> k <= x |] ==> (LEAST x. P(x)) = k";
+by (blast_tac (claset() addIs [some_equality, order_antisym]) 1); 
+bind_thm ("Least_equality", allI RSN (2, result()));
+
+(*LEAST and wellorderings*)
+Goal "wf({(x,y::'a). x<y}) \
+\     ==> P(k::'a::linorder) --> P(LEAST x. P(x)) & (LEAST x. P(x)) <= k";
+by (eres_inst_tac [("a","k")] wf_induct 1);
+by (rtac impI 1);
+by (rtac classical 1);
+by (res_inst_tac [("s","x")] (Least_equality RS ssubst) 1);
+by Auto_tac;  
+by (auto_tac (claset(), simpset() addsimps [linorder_not_less RS sym]));  
+by (blast_tac (claset() addIs [order_less_trans]) 1);
+bind_thm("wellorder_LeastI",   result() RS mp RS conjunct1);
+bind_thm("wellorder_Least_le", result() RS mp RS conjunct2);
+
+Goal "[| wf({(x,y::'a). x<y});  k < (LEAST x. P(x)) |] \
+\     ==> ~P(k::'a::linorder)";
+by (rtac notI 1);
+by (dtac wellorder_Least_le 1); 
+by (asm_full_simp_tac (simpset() addsimps [linorder_not_le RS sym]) 2);
+by (fast_tac (claset() addIs []) 2); 
+by (assume_tac 1); 
+qed "wellorder_not_less_Least";
+
+(** LEAST theorems for type "nat" by specialization **)
+
+Goalw [less_def] "wf {(x,y::nat). x<y}"; 
+by (rtac (wf_pred_nat RS wf_trancl RS wf_subset) 1);
+by (Blast_tac 1); 
+qed "wf_less";
+
+bind_thm("LeastI",   wf_less RS wellorder_LeastI);
+bind_thm("Least_le", wf_less RS wellorder_Least_le);
+bind_thm("not_less_Least", wf_less RS wellorder_not_less_Least);
+
+Goal "(S::nat set) ~= {} ==> EX x:S. ALL y:S. x <= y";
+by (cut_facts_tac [wf_pred_nat RS wf_trancl RS (wf_eq_minimal RS iffD1)] 1);
+by (dres_inst_tac [("x","S")] spec 1);
+by (Asm_full_simp_tac 1);
+by (etac impE 1);
+by (Force_tac 1);
+by (force_tac (claset(), simpset() addsimps [less_eq,not_le_iff_less]) 1);
+qed "nonempty_has_least";
+
+Goal "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))";
+by (case_tac "n" 1);
+by Auto_tac;  
+by (ftac LeastI 1); 
+by (dres_inst_tac [("P","%x. P (Suc x)")] LeastI 1);
+by (subgoal_tac "(LEAST x. P x) <= Suc (LEAST x. P (Suc x))" 1); 
+by (etac Least_le 2); 
+by (case_tac "LEAST x. P x" 1);
+by Auto_tac;  
+by (dres_inst_tac [("P","%x. P (Suc x)")] Least_le 1);
+by (blast_tac (claset() addIs [order_antisym]) 1); 
+qed "Least_Suc";
+
+
+(** min and max **)
+
 Goal "min 0 n = (0::nat)";
 by (rtac min_leastL 1);
 by (Simp_tac 1);
diff -r de981d0037ed -r e1a793957a8f src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Wed Jan 10 11:13:11 2001 +0100
+++ b/src/HOL/NatDef.ML	Wed Jan 10 11:14:30 2001 +0100
@@ -462,65 +462,6 @@
   Not suitable as default simprules because they often lead to looping*)
 bind_thms ("not_less_simps", [not_less_less_Suc_eq, leD RS not_less_less_Suc_eq]);
 
-(** LEAST -- the least number operator **)
-
-Goal "(ALL m::nat. P m --> n <= m) = (ALL m. m < n --> ~ P m)";
-by (blast_tac (claset() addIs [leI] addEs [leE]) 1);
-val lemma = result();
-
-(* This is an old def of Least for nat, which is derived for compatibility *)
-Goalw [Least_def]
-  "(LEAST n::nat. P n) == (@n. P(n) & (ALL m. m < n --> ~P(m)))";
-by (simp_tac (simpset() addsimps [lemma]) 1);
-qed "Least_nat_def";
-
-val [prem1,prem2] = Goalw [Least_nat_def]
-    "[| P(k::nat);  !!x. x<k ==> ~P(x) |] ==> (LEAST x. P(x)) = k";
-by (rtac some_equality 1);
-by (blast_tac (claset() addSIs [prem1,prem2]) 1);
-by (cut_facts_tac [less_linear] 1);
-by (blast_tac (claset() addSIs [prem1] addSDs [prem2]) 1);
-qed "Least_equality";
-
-Goal "P(k::nat) ==> P(LEAST x. P(x))";
-by (etac rev_mp 1);
-by (res_inst_tac [("n","k")] nat_less_induct 1);
-by (rtac impI 1);
-by (rtac classical 1);
-by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
-by (assume_tac 1);
-by (assume_tac 2);
-by (Blast_tac 1);
-qed "LeastI";
-
-(*Proof is almost identical to the one above!*)
-Goal "P(k::nat) ==> (LEAST x. P(x)) <= k";
-by (etac rev_mp 1);
-by (res_inst_tac [("n","k")] nat_less_induct 1);
-by (rtac impI 1);
-by (rtac classical 1);
-by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
-by (assume_tac 1);
-by (rtac le_refl 2);
-by (blast_tac (claset() addIs [less_imp_le,le_trans]) 1);
-qed "Least_le";
-
-Goal "k < (LEAST x. P(x)) ==> ~P(k::nat)";
-by (rtac notI 1);
-by (etac (rewrite_rule [le_def] Least_le RS notE) 1 THEN assume_tac 1);
-qed "not_less_Least";
-
-(* [| m ~= n; m < n ==> P; n < m ==> P |] ==> P *)
-bind_thm("nat_neqE", nat_neq_iff RS iffD1 RS disjE);
-
-Goal "(S::nat set) ~= {} ==> EX x:S. ALL y:S. x <= y";
-by (cut_facts_tac [wf_pred_nat RS wf_trancl RS (wf_eq_minimal RS iffD1)] 1);
-by (dres_inst_tac [("x","S")] spec 1);
-by (Asm_full_simp_tac 1);
-by (etac impE 1);
-by (Force_tac 1);
-by (force_tac (claset(), simpset() addsimps [less_eq,not_le_iff_less]) 1);
-qed "nonempty_has_least";
 
 (** Re-orientation of the equations 0=x and Suc n = x. *