removed 2 qed_goals
authorpaulson
Wed Jul 21 15:23:18 1999 +0200 (1999-07-21)
changeset 70588dfea70eb6b7
parent 7057 b9ddbb925939
child 7059 71e9ea2198e0
removed 2 qed_goals
src/HOL/Nat.ML
     1.1 --- a/src/HOL/Nat.ML	Wed Jul 21 15:22:11 1999 +0200
     1.2 +++ b/src/HOL/Nat.ML	Wed Jul 21 15:23:18 1999 +0200
     1.3 @@ -60,49 +60,49 @@
     1.4  by Auto_tac;
     1.5  qed "less_Suc_eq_0_disj";
     1.6  
     1.7 -qed_goalw "Least_Suc" thy [Least_nat_def]
     1.8 - "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
     1.9 - (fn _ => [
    1.10 -        rtac select_equality 1,
    1.11 -        fold_goals_tac [Least_nat_def],
    1.12 -        safe_tac (claset() addSEs [LeastI]),
    1.13 -        rename_tac "j" 1,
    1.14 -        exhaust_tac "j" 1,
    1.15 -        Blast_tac 1,
    1.16 -        blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1,
    1.17 -        rename_tac "k n" 1,
    1.18 -        exhaust_tac "k" 1,
    1.19 -        Blast_tac 1,
    1.20 -        hyp_subst_tac 1,
    1.21 -        rewtac Least_nat_def,
    1.22 -        rtac (select_equality RS arg_cong RS sym) 1,
    1.23 -        Safe_tac,
    1.24 -        dtac Suc_mono 1,
    1.25 -        Blast_tac 1,
    1.26 -        cut_facts_tac [less_linear] 1,
    1.27 -        Safe_tac,
    1.28 -        atac 2,
    1.29 -        Blast_tac 2,
    1.30 -        dtac Suc_mono 1,
    1.31 -        Blast_tac 1]);
    1.32 +Goalw [Least_nat_def]
    1.33 + "[| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))";
    1.34 +by (rtac select_equality 1);
    1.35 +by (fold_goals_tac [Least_nat_def]);
    1.36 +by (safe_tac (claset() addSEs [LeastI]));
    1.37 +by (rename_tac "j" 1);
    1.38 +by (exhaust_tac "j" 1);
    1.39 +by (Blast_tac 1);
    1.40 +by (blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1);
    1.41 +by (rename_tac "k n" 1);
    1.42 +by (exhaust_tac "k" 1);
    1.43 +by (Blast_tac 1);
    1.44 +by (hyp_subst_tac 1);
    1.45 +by (rewtac Least_nat_def);
    1.46 +by (rtac (select_equality RS arg_cong RS sym) 1);
    1.47 +by (Safe_tac);
    1.48 +by (dtac Suc_mono 1);
    1.49 +by (Blast_tac 1);
    1.50 +by (cut_facts_tac [less_linear] 1);
    1.51 +by (Safe_tac);
    1.52 +by (atac 2);
    1.53 +by (Blast_tac 2);
    1.54 +by (dtac Suc_mono 1);
    1.55 +by (Blast_tac 1);
    1.56 +qed "Least_Suc";
    1.57  
    1.58 -qed_goal "nat_induct2" thy 
    1.59 -"[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n" (fn prems => [
    1.60 -        cut_facts_tac prems 1,
    1.61 -        rtac less_induct 1,
    1.62 -        exhaust_tac "n" 1,
    1.63 -         hyp_subst_tac 1,
    1.64 -         atac 1,
    1.65 -        hyp_subst_tac 1,
    1.66 -        exhaust_tac "nat" 1,
    1.67 -         hyp_subst_tac 1,
    1.68 -         atac 1,
    1.69 -        hyp_subst_tac 1,
    1.70 -        resolve_tac prems 1,
    1.71 -        dtac spec 1,
    1.72 -        etac mp 1,
    1.73 -        rtac (lessI RS less_trans) 1,
    1.74 -        rtac (lessI RS Suc_mono) 1]);
    1.75 +val prems = Goal "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
    1.76 +by (cut_facts_tac prems 1);
    1.77 +by (rtac less_induct 1);
    1.78 +by (exhaust_tac "n" 1);
    1.79 +by (hyp_subst_tac 1);
    1.80 +by (atac 1);
    1.81 +by (hyp_subst_tac 1);
    1.82 +by (exhaust_tac "nat" 1);
    1.83 +by (hyp_subst_tac 1);
    1.84 +by (atac 1);
    1.85 +by (hyp_subst_tac 1);
    1.86 +by (resolve_tac prems 1);
    1.87 +by (dtac spec 1);
    1.88 +by (etac mp 1);
    1.89 +by (rtac (lessI RS less_trans) 1);
    1.90 +by (rtac (lessI RS Suc_mono) 1);
    1.91 +qed "nat_induct2";
    1.92  
    1.93  Goal "min 0 n = 0";
    1.94  by (rtac min_leastL 1);