src/HOL/Nat.ML
changeset 10850 e1a793957a8f
parent 10710 0c8d58332658
child 11139 b092ad5cd510
     1.1 --- a/src/HOL/Nat.ML	Wed Jan 10 11:13:11 2001 +0100
     1.2 +++ b/src/HOL/Nat.ML	Wed Jan 10 11:14:30 2001 +0100
     1.3 @@ -68,26 +68,6 @@
     1.4  by Auto_tac;
     1.5  qed "less_Suc_eq_0_disj";
     1.6  
     1.7 -Goalw [Least_nat_def]
     1.8 - "[| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))";
     1.9 -by (rtac some_equality 1);
    1.10 -by (fold_goals_tac [Least_nat_def]);
    1.11 -by (safe_tac (claset() addSEs [LeastI]));
    1.12 -by (rename_tac "j" 1);
    1.13 -by (case_tac "j" 1);
    1.14 -by (Blast_tac 1);
    1.15 -by (blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1);
    1.16 -by (rename_tac "k n" 1);
    1.17 -by (case_tac "k" 1);
    1.18 -by (Blast_tac 1);
    1.19 -by (hyp_subst_tac 1);
    1.20 -by (rewtac Least_nat_def);
    1.21 -by (rtac (some_equality RS arg_cong RS sym) 1);
    1.22 -by (blast_tac (claset() addDs [Suc_mono]) 1);
    1.23 -by (cut_inst_tac [("m","m")] less_linear 1);
    1.24 -by (blast_tac (claset() addIs [Suc_mono]) 1);
    1.25 -qed "Least_Suc";
    1.26 -
    1.27  val prems = Goal "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
    1.28  by (rtac nat_less_induct 1);
    1.29  by (case_tac "n" 1);
    1.30 @@ -95,6 +75,73 @@
    1.31  by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans])));
    1.32  qed "nat_induct2";
    1.33  
    1.34 +
    1.35 +(*** LEAST -- the least number operator ***)
    1.36 +
    1.37 +(*This version is polymorphic over type class "order"! *) 
    1.38 +Goalw [Least_def]
    1.39 +     "[| P(k::'a::order);  ALL x. P x --> k <= x |] ==> (LEAST x. P(x)) = k";
    1.40 +by (blast_tac (claset() addIs [some_equality, order_antisym]) 1); 
    1.41 +bind_thm ("Least_equality", allI RSN (2, result()));
    1.42 +
    1.43 +(*LEAST and wellorderings*)
    1.44 +Goal "wf({(x,y::'a). x<y}) \
    1.45 +\     ==> P(k::'a::linorder) --> P(LEAST x. P(x)) & (LEAST x. P(x)) <= k";
    1.46 +by (eres_inst_tac [("a","k")] wf_induct 1);
    1.47 +by (rtac impI 1);
    1.48 +by (rtac classical 1);
    1.49 +by (res_inst_tac [("s","x")] (Least_equality RS ssubst) 1);
    1.50 +by Auto_tac;  
    1.51 +by (auto_tac (claset(), simpset() addsimps [linorder_not_less RS sym]));  
    1.52 +by (blast_tac (claset() addIs [order_less_trans]) 1);
    1.53 +bind_thm("wellorder_LeastI",   result() RS mp RS conjunct1);
    1.54 +bind_thm("wellorder_Least_le", result() RS mp RS conjunct2);
    1.55 +
    1.56 +Goal "[| wf({(x,y::'a). x<y});  k < (LEAST x. P(x)) |] \
    1.57 +\     ==> ~P(k::'a::linorder)";
    1.58 +by (rtac notI 1);
    1.59 +by (dtac wellorder_Least_le 1); 
    1.60 +by (asm_full_simp_tac (simpset() addsimps [linorder_not_le RS sym]) 2);
    1.61 +by (fast_tac (claset() addIs []) 2); 
    1.62 +by (assume_tac 1); 
    1.63 +qed "wellorder_not_less_Least";
    1.64 +
    1.65 +(** LEAST theorems for type "nat" by specialization **)
    1.66 +
    1.67 +Goalw [less_def] "wf {(x,y::nat). x<y}"; 
    1.68 +by (rtac (wf_pred_nat RS wf_trancl RS wf_subset) 1);
    1.69 +by (Blast_tac 1); 
    1.70 +qed "wf_less";
    1.71 +
    1.72 +bind_thm("LeastI",   wf_less RS wellorder_LeastI);
    1.73 +bind_thm("Least_le", wf_less RS wellorder_Least_le);
    1.74 +bind_thm("not_less_Least", wf_less RS wellorder_not_less_Least);
    1.75 +
    1.76 +Goal "(S::nat set) ~= {} ==> EX x:S. ALL y:S. x <= y";
    1.77 +by (cut_facts_tac [wf_pred_nat RS wf_trancl RS (wf_eq_minimal RS iffD1)] 1);
    1.78 +by (dres_inst_tac [("x","S")] spec 1);
    1.79 +by (Asm_full_simp_tac 1);
    1.80 +by (etac impE 1);
    1.81 +by (Force_tac 1);
    1.82 +by (force_tac (claset(), simpset() addsimps [less_eq,not_le_iff_less]) 1);
    1.83 +qed "nonempty_has_least";
    1.84 +
    1.85 +Goal "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))";
    1.86 +by (case_tac "n" 1);
    1.87 +by Auto_tac;  
    1.88 +by (ftac LeastI 1); 
    1.89 +by (dres_inst_tac [("P","%x. P (Suc x)")] LeastI 1);
    1.90 +by (subgoal_tac "(LEAST x. P x) <= Suc (LEAST x. P (Suc x))" 1); 
    1.91 +by (etac Least_le 2); 
    1.92 +by (case_tac "LEAST x. P x" 1);
    1.93 +by Auto_tac;  
    1.94 +by (dres_inst_tac [("P","%x. P (Suc x)")] Least_le 1);
    1.95 +by (blast_tac (claset() addIs [order_antisym]) 1); 
    1.96 +qed "Least_Suc";
    1.97 +
    1.98 +
    1.99 +(** min and max **)
   1.100 +
   1.101  Goal "min 0 n = (0::nat)";
   1.102  by (rtac min_leastL 1);
   1.103  by (Simp_tac 1);