src/HOL/Nat.ML
changeset 1824 44254696843a
parent 1823 e1458e1a9f80
child 1919 d94c12235878
     1.1 --- a/src/HOL/Nat.ML	Fri Jun 21 13:51:09 1996 +0200
     1.2 +++ b/src/HOL/Nat.ML	Tue Jun 25 13:11:29 1996 +0200
     1.3 @@ -162,7 +162,7 @@
     1.4  
     1.5  (* The unrolling rule for nat_rec *)
     1.6  goal Nat.thy
     1.7 -   "(%n. nat_rec n c d) = wfrec pred_nat (%f. nat_case ?c (%m. ?d m (f m)))";
     1.8 +   "(%n. nat_rec c d n) = wfrec pred_nat (%f. nat_case ?c (%m. ?d m (f m)))";
     1.9    by (simp_tac (HOL_ss addsimps [nat_rec_def]) 1);
    1.10  bind_thm("nat_rec_unfold", wf_pred_nat RS 
    1.11                              ((result() RS eq_reflection) RS def_wfrec));
    1.12 @@ -174,25 +174,25 @@
    1.13  
    1.14  (** conversion rules **)
    1.15  
    1.16 -goal Nat.thy "nat_rec 0 c h = c";
    1.17 +goal Nat.thy "nat_rec c h 0 = c";
    1.18  by (rtac (nat_rec_unfold RS trans) 1);
    1.19  by (simp_tac (!simpset addsimps [nat_case_0]) 1);
    1.20  qed "nat_rec_0";
    1.21  
    1.22 -goal Nat.thy "nat_rec (Suc n) c h = h n (nat_rec n c h)";
    1.23 +goal Nat.thy "nat_rec c h (Suc n) = h n (nat_rec c h n)";
    1.24  by (rtac (nat_rec_unfold RS trans) 1);
    1.25  by (simp_tac (!simpset addsimps [nat_case_Suc, pred_natI, cut_apply]) 1);
    1.26  qed "nat_rec_Suc";
    1.27  
    1.28  (*These 2 rules ease the use of primitive recursion.  NOTE USE OF == *)
    1.29  val [rew] = goal Nat.thy
    1.30 -    "[| !!n. f(n) == nat_rec n c h |] ==> f(0) = c";
    1.31 +    "[| !!n. f(n) == nat_rec c h n |] ==> f(0) = c";
    1.32  by (rewtac rew);
    1.33  by (rtac nat_rec_0 1);
    1.34  qed "def_nat_rec_0";
    1.35  
    1.36  val [rew] = goal Nat.thy
    1.37 -    "[| !!n. f(n) == nat_rec n c h |] ==> f(Suc(n)) = h n (f n)";
    1.38 +    "[| !!n. f(n) == nat_rec c h n |] ==> f(Suc(n)) = h n (f n)";
    1.39  by (rewtac rew);
    1.40  by (rtac nat_rec_Suc 1);
    1.41  qed "def_nat_rec_Suc";
    1.42 @@ -426,7 +426,7 @@
    1.43    (fn [prem] => [rtac (prem RS arg_cong) 1]);
    1.44  
    1.45  qed_goal "nat_rec_weak_cong" Nat.thy
    1.46 -  "m=n ==> nat_rec m a f = nat_rec n a f"
    1.47 +  "m=n ==> nat_rec a f m = nat_rec a f n"
    1.48    (fn [prem] => [rtac (prem RS arg_cong) 1]);
    1.49  
    1.50  val prems = goalw Nat.thy [le_def] "~n<m ==> m<=(n::nat)";