# HG changeset patch
# User oheimb
# Date 982249294 -3600
# Node ID 0d4ca3b3741f4264d2c8a4353df2f5054f70d458
# Parent  a46eaedbeb2d9da4d480272a9b299019c22c38ff
supressed some warnings on identical proofstate
moved wellorder_LeastI,wellorder_Least_le,wellorder_not_less_Least
from Nat.ML to Wellfounded_Recursion.ML
added wellorder axclass

diff -r a46eaedbeb2d -r 0d4ca3b3741f src/HOL/Wellfounded_Recursion.ML
--- a/src/HOL/Wellfounded_Recursion.ML	Thu Feb 15 16:01:22 2001 +0100
+++ b/src/HOL/Wellfounded_Recursion.ML	Thu Feb 15 16:01:34 2001 +0100
@@ -123,8 +123,7 @@
 by Safe_tac;
 by (EVERY1[rtac allE, assume_tac, etac impE, Blast_tac]);
 by (etac bexE 1);
-by (rename_tac "a" 1);
-by (case_tac "a = x" 1);
+by (rename_tac "a" 1 THEN case_tac "a = x" 1);
  by (res_inst_tac [("x","a")]bexI 2);
   by (assume_tac 3);
  by (Blast_tac 2);
@@ -163,8 +162,7 @@
 \     |] ==> wf(UN i:I. r i)";
 by (asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
 by (Clarify_tac 1);
-by (rename_tac "A a" 1);
-by (case_tac "EX i:I. EX a:A. EX b:A. (b,a) : r i" 1);
+by (rename_tac "A a" 1 THEN case_tac "EX i:I. EX a:A. EX b:A. (b,a) : r i" 1);
  by (Asm_full_simp_tac 2);
  by (Best_tac 2);  (*much faster than Blast_tac*)
 by (Clarify_tac 1);
@@ -368,3 +366,24 @@
 by (Clarify_tac 1);
 by (etac wfrec 1);
 qed "tfl_wfrec";
+
+(*LEAST and wellorderings*)
+(* ### see also wf_linord_ex_has_least and its consequences in Wellfounded_Relations.ML *)
+
+Goal "P (k::'a::wellorder) --> P (LEAST x. P(x)) & (LEAST x. P(x)) <= k";
+by (res_inst_tac [("a","k")] (wf RS 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 "[| k < (LEAST x. P x) |] ==> ~P (k::'a::wellorder)";
+by (full_simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
+by (etac contrapos_nn 1);
+by (etac wellorder_Least_le 1);
+qed "wellorder_not_less_Least";
+