moved wellorder_LeastI,wellorder_Least_le,wellorder_not_less_Least
authoroheimb
Thu Feb 15 16:01:07 2001 +0100 (2001-02-15)
changeset 11139b092ad5cd510
parent 11138 bdfb9ec76a0a
child 11140 a46eaedbeb2d
moved wellorder_LeastI,wellorder_Least_le,wellorder_not_less_Least
from Nat.ML to Wellfounded_Recursion.ML
moved Least_equality from Nat.ML to Ord.thy
moved wf_less from Nat.ML to NatDef.ML
added wellorder axclass
nonempty_has_least of Nat.ML -> ex_has_least_nat of Wellfounded_Relations.ML
added min_of_mono, max_of_mono, max_leastL, max_leastR to Ord.thy
src/HOL/Nat.ML
     1.1 --- a/src/HOL/Nat.ML	Thu Feb 15 16:00:44 2001 +0100
     1.2 +++ b/src/HOL/Nat.ML	Thu Feb 15 16:01:07 2001 +0100
     1.3 @@ -75,56 +75,11 @@
     1.4  by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans])));
     1.5  qed "nat_induct2";
     1.6  
     1.7 -
     1.8 -(*** LEAST -- the least number operator ***)
     1.9 -
    1.10 -(*This version is polymorphic over type class "order"! *) 
    1.11 -Goalw [Least_def]
    1.12 -     "[| P(k::'a::order);  ALL x. P x --> k <= x |] ==> (LEAST x. P(x)) = k";
    1.13 -by (blast_tac (claset() addIs [some_equality, order_antisym]) 1); 
    1.14 -bind_thm ("Least_equality", allI RSN (2, result()));
    1.15 -
    1.16 -(*LEAST and wellorderings*)
    1.17 -Goal "wf({(x,y::'a). x<y}) \
    1.18 -\     ==> P(k::'a::linorder) --> P(LEAST x. P(x)) & (LEAST x. P(x)) <= k";
    1.19 -by (eres_inst_tac [("a","k")] wf_induct 1);
    1.20 -by (rtac impI 1);
    1.21 -by (rtac classical 1);
    1.22 -by (res_inst_tac [("s","x")] (Least_equality RS ssubst) 1);
    1.23 -by Auto_tac;  
    1.24 -by (auto_tac (claset(), simpset() addsimps [linorder_not_less RS sym]));  
    1.25 -by (blast_tac (claset() addIs [order_less_trans]) 1);
    1.26 -bind_thm("wellorder_LeastI",   result() RS mp RS conjunct1);
    1.27 -bind_thm("wellorder_Least_le", result() RS mp RS conjunct2);
    1.28 -
    1.29 -Goal "[| wf({(x,y::'a). x<y});  k < (LEAST x. P(x)) |] \
    1.30 -\     ==> ~P(k::'a::linorder)";
    1.31 -by (rtac notI 1);
    1.32 -by (dtac wellorder_Least_le 1); 
    1.33 -by (asm_full_simp_tac (simpset() addsimps [linorder_not_le RS sym]) 2);
    1.34 -by (fast_tac (claset() addIs []) 2); 
    1.35 -by (assume_tac 1); 
    1.36 -qed "wellorder_not_less_Least";
    1.37 -
    1.38  (** LEAST theorems for type "nat" by specialization **)
    1.39  
    1.40 -Goalw [less_def] "wf {(x,y::nat). x<y}"; 
    1.41 -by (rtac (wf_pred_nat RS wf_trancl RS wf_subset) 1);
    1.42 -by (Blast_tac 1); 
    1.43 -qed "wf_less";
    1.44 -
    1.45 -bind_thm("LeastI",   wf_less RS wellorder_LeastI);
    1.46 -bind_thm("Least_le", wf_less RS wellorder_Least_le);
    1.47 -bind_thm("not_less_Least", wf_less RS wellorder_not_less_Least);
    1.48 -
    1.49 -Goal "(S::nat set) ~= {} ==> EX x:S. ALL y:S. x <= y";
    1.50 -by (cut_facts_tac [wf_pred_nat RS wf_trancl RS (wf_eq_minimal RS iffD1)] 1);
    1.51 -by (dres_inst_tac [("x","S")] spec 1);
    1.52 -by (Asm_full_simp_tac 1);
    1.53 -by (etac impE 1);
    1.54 -by (Force_tac 1);
    1.55 -by (force_tac (claset(), simpset() addsimps [less_eq,not_le_iff_less]) 1);
    1.56 -qed "nonempty_has_least";
    1.57 +bind_thm("LeastI", wellorder_LeastI);
    1.58 +bind_thm("Least_le", wellorder_Least_le);
    1.59 +bind_thm("not_less_Least", wellorder_not_less_Least);
    1.60  
    1.61  Goal "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))";
    1.62  by (case_tac "n" 1);
    1.63 @@ -152,22 +107,24 @@
    1.64  by (Simp_tac 1);
    1.65  qed "min_0R";
    1.66  
    1.67 -Goalw [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
    1.68 -by (Simp_tac 1);
    1.69 +Goal "min (Suc m) (Suc n) = Suc (min m n)";
    1.70 +by (simp_tac (simpset() addsimps [min_of_mono]) 1);
    1.71  qed "min_Suc_Suc";
    1.72  
    1.73  Addsimps [min_0L,min_0R,min_Suc_Suc];
    1.74  
    1.75 -Goalw [max_def] "max 0 n = (n::nat)";
    1.76 +Goal "max 0 n = (n::nat)";
    1.77 +by (rtac max_leastL 1);
    1.78  by (Simp_tac 1);
    1.79  qed "max_0L";
    1.80  
    1.81 -Goalw [max_def] "max n 0 = (n::nat)";
    1.82 +Goal "max n 0 = (n::nat)";
    1.83 +by (rtac max_leastR 1);
    1.84  by (Simp_tac 1);
    1.85  qed "max_0R";
    1.86  
    1.87 -Goalw [max_def] "max (Suc m) (Suc n) = Suc(max m n)";
    1.88 -by (Simp_tac 1);
    1.89 +Goal "max (Suc m) (Suc n) = Suc(max m n)";
    1.90 +by (simp_tac (simpset() addsimps [max_of_mono]) 1);
    1.91  qed "max_Suc_Suc";
    1.92  
    1.93  Addsimps [max_0L,max_0R,max_Suc_Suc];