src/HOL/NatDef.ML
changeset 3236 882e125ed7da
parent 3143 d60e49b86c6a
child 3282 c31e6239d4c9
     1.1 --- a/src/HOL/NatDef.ML	Tue May 20 11:38:50 1997 +0200
     1.2 +++ b/src/HOL/NatDef.ML	Tue May 20 11:39:32 1997 +0200
     1.3 @@ -131,6 +131,12 @@
     1.4  
     1.5  bind_thm ("Suc_n_not_n", n_not_Suc_n RS not_sym);
     1.6  
     1.7 +goal thy "!!n. n ~= 0 ==> EX m. n = Suc m";
     1.8 +br natE 1;
     1.9 +by (REPEAT (Blast_tac 1));
    1.10 +qed "not0_implies_Suc";
    1.11 +
    1.12 +
    1.13  (*** nat_case -- the selection operator for nat ***)
    1.14  
    1.15  goalw thy [nat_case_def] "nat_case a f 0 = a";
    1.16 @@ -141,24 +147,10 @@
    1.17  by (blast_tac (!claset addIs [select_equality]) 1);
    1.18  qed "nat_case_Suc";
    1.19  
    1.20 -(** Introduction rules for 'pred_nat' **)
    1.21 -
    1.22 -goalw thy [pred_nat_def] "(n, Suc(n)) : pred_nat";
    1.23 -by (Blast_tac 1);
    1.24 -qed "pred_natI";
    1.25 -
    1.26 -val major::prems = goalw thy [pred_nat_def]
    1.27 -    "[| p : pred_nat;  !!x n. [| p = (n, Suc(n)) |] ==> R \
    1.28 -\    |] ==> R";
    1.29 -by (rtac (major RS CollectE) 1);
    1.30 -by (REPEAT (eresolve_tac ([asm_rl,exE]@prems) 1));
    1.31 -qed "pred_natE";
    1.32 -
    1.33 -goalw thy [wf_def] "wf(pred_nat)";
    1.34 +goalw thy [wf_def, pred_nat_def] "wf(pred_nat)";
    1.35  by (strip_tac 1);
    1.36  by (nat_ind_tac "x" 1);
    1.37 -by (blast_tac (!claset addSEs [mp, pred_natE]) 2);
    1.38 -by (blast_tac (!claset addSEs [mp, pred_natE]) 1);
    1.39 +by (ALLGOALS Blast_tac);
    1.40  qed "wf_pred_nat";
    1.41  
    1.42  
    1.43 @@ -185,7 +177,7 @@
    1.44  
    1.45  goal thy "nat_rec c h (Suc n) = h n (nat_rec c h n)";
    1.46  by (rtac (nat_rec_unfold RS trans) 1);
    1.47 -by (simp_tac (!simpset addsimps [nat_case_Suc, pred_natI, cut_apply]) 1);
    1.48 +by (simp_tac (!simpset addsimps [nat_case_Suc, pred_nat_def, cut_apply]) 1);
    1.49  qed "nat_rec_Suc";
    1.50  
    1.51  (*These 2 rules ease the use of primitive recursion.  NOTE USE OF == *)
    1.52 @@ -216,8 +208,8 @@
    1.53  by (resolve_tac prems 1);
    1.54  qed "less_trans";
    1.55  
    1.56 -goalw thy [less_def] "n < Suc(n)";
    1.57 -by (rtac (pred_natI RS r_into_trancl) 1);
    1.58 +goalw thy [less_def, pred_nat_def] "n < Suc(n)";
    1.59 +by (simp_tac (!simpset addsimps [r_into_trancl]) 1);
    1.60  qed "lessI";
    1.61  AddIffs [lessI];
    1.62  
    1.63 @@ -255,13 +247,13 @@
    1.64  qed "less_not_refl2";
    1.65  
    1.66  
    1.67 -val major::prems = goalw thy [less_def]
    1.68 +val major::prems = goalw thy [less_def, pred_nat_def]
    1.69      "[| i<k;  k=Suc(i) ==> P;  !!j. [| i<j;  k=Suc(j) |] ==> P \
    1.70  \    |] ==> P";
    1.71  by (rtac (major RS tranclE) 1);
    1.72 +by (ALLGOALS Full_simp_tac); 
    1.73  by (REPEAT_FIRST (bound_hyp_subst_tac ORELSE'
    1.74 -                  eresolve_tac (prems@[pred_natE, Pair_inject])));
    1.75 -by (rtac refl 1);
    1.76 +                  eresolve_tac (prems@[asm_rl, Pair_inject])));
    1.77  qed "lessE";
    1.78  
    1.79  goal thy "~ n<0";