# HG changeset patch
# User berghofe
# Date 835701089 -7200
# Node ID 44254696843a28fd847502d8ebc838230cf55cf0
# Parent  e1458e1a9f80290fc66ac42b431ffaa3a1cb7115
Changed argument order of nat_rec.

diff -r e1458e1a9f80 -r 44254696843a src/HOL/Arith.thy
--- a/src/HOL/Arith.thy	Fri Jun 21 13:51:09 1996 +0200
+++ b/src/HOL/Arith.thy	Tue Jun 25 13:11:29 1996 +0200
@@ -16,10 +16,10 @@
   div, mod  :: [nat, nat] => nat  (infixl 70)
 
 defs
-  pred_def  "pred(m) == nat_rec m 0 (%n r.n)"
-  add_def   "m+n == nat_rec m n (%u v. Suc(v))"
-  diff_def  "m-n == nat_rec n m (%u v. pred(v))"
-  mult_def  "m*n == nat_rec m 0 (%u v. n + v)"
+  pred_def  "pred(m) == nat_rec 0 (%n r.n) m"
+  add_def   "m+n == nat_rec n (%u v. Suc(v)) m"
+  diff_def  "m-n == nat_rec m (%u v. pred(v)) n"
+  mult_def  "m*n == nat_rec 0 (%u v. n + v) m"
 
   mod_def   "m mod n == wfrec (trancl pred_nat)
                           (%f j. if j<n then j else f (j-n)) m"
@@ -30,5 +30,5 @@
 (*"Difference" is subtraction of natural numbers.
   There are no negative numbers; we have
      m - n = 0  iff  m<=n   and     m - n = Suc(k) iff m)n.
-  Also, nat_rec(m, 0, %z w.z) is pred(m).   *)
+  Also, nat_rec(0, %z w.z, m) is pred(m).   *)
 
diff -r e1458e1a9f80 -r 44254696843a src/HOL/Hoare/Arith2.thy
--- a/src/HOL/Hoare/Arith2.thy	Fri Jun 21 13:51:09 1996 +0200
+++ b/src/HOL/Hoare/Arith2.thy	Tue Jun 25 13:11:29 1996 +0200
@@ -19,9 +19,9 @@
   "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
 
   pow     :: [nat, nat] => nat                              (infixl 75)
-  "m pow n     == nat_rec n (Suc 0) (%u v.m*v)"
+  "m pow n     == nat_rec (Suc 0) (%u v.m*v) n"
 
   fac     :: nat => nat
-  "fac m       == nat_rec m (Suc 0) (%u v.(Suc u)*v)"
+  "fac m       == nat_rec (Suc 0) (%u v.(Suc u)*v) m"
 
 end
diff -r e1458e1a9f80 -r 44254696843a src/HOL/Hoare/Hoare.thy
--- a/src/HOL/Hoare/Hoare.thy	Fri Jun 21 13:51:09 1996 +0200
+++ b/src/HOL/Hoare/Hoare.thy	Tue Jun 25 13:11:29 1996 +0200
@@ -46,8 +46,8 @@
   "While b inv c s s' == ? n. Iter n b c s s'"
 
   Iter          :: [nat, 'a bexp, 'a com] => 'a com
-  "Iter n b c == nat_rec n (%s s'.~b(s) & (s=s'))
-             (%n_rec iter_rec.%s s'.b(s) & Seq c iter_rec s s')"
+  "Iter n b c == nat_rec (%s s'.~b(s) & (s=s'))
+             (%n_rec iter_rec.%s s'.b(s) & Seq c iter_rec s s') n"
 
   Spec          :: ['a bexp, 'a com, 'a bexp] => bool
   "Spec p c q == !s s'. c s s' --> p s --> q s'"
diff -r e1458e1a9f80 -r 44254696843a src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Jun 21 13:51:09 1996 +0200
+++ b/src/HOL/List.thy	Tue Jun 25 13:11:29 1996 +0200
@@ -93,5 +93,5 @@
   take_Nil  "take n [] = []"
   take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
 defs
-  nth_def  "nth(n) == nat_rec n hd (%m r xs. r(tl(xs)))"
+  nth_def  "nth(n) == nat_rec hd (%m r xs. r(tl(xs))) n"
 end
diff -r e1458e1a9f80 -r 44254696843a src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Fri Jun 21 13:51:09 1996 +0200
+++ b/src/HOL/Nat.ML	Tue Jun 25 13:11:29 1996 +0200
@@ -162,7 +162,7 @@
 
 (* The unrolling rule for nat_rec *)
 goal Nat.thy
-   "(%n. nat_rec n c d) = wfrec pred_nat (%f. nat_case ?c (%m. ?d m (f m)))";
+   "(%n. nat_rec c d n) = wfrec pred_nat (%f. nat_case ?c (%m. ?d m (f m)))";
   by (simp_tac (HOL_ss addsimps [nat_rec_def]) 1);
 bind_thm("nat_rec_unfold", wf_pred_nat RS 
                             ((result() RS eq_reflection) RS def_wfrec));
@@ -174,25 +174,25 @@
 
 (** conversion rules **)
 
-goal Nat.thy "nat_rec 0 c h = c";
+goal Nat.thy "nat_rec c h 0 = c";
 by (rtac (nat_rec_unfold RS trans) 1);
 by (simp_tac (!simpset addsimps [nat_case_0]) 1);
 qed "nat_rec_0";
 
-goal Nat.thy "nat_rec (Suc n) c h = h n (nat_rec n c h)";
+goal Nat.thy "nat_rec c h (Suc n) = h n (nat_rec c h n)";
 by (rtac (nat_rec_unfold RS trans) 1);
 by (simp_tac (!simpset addsimps [nat_case_Suc, pred_natI, cut_apply]) 1);
 qed "nat_rec_Suc";
 
 (*These 2 rules ease the use of primitive recursion.  NOTE USE OF == *)
 val [rew] = goal Nat.thy
-    "[| !!n. f(n) == nat_rec n c h |] ==> f(0) = c";
+    "[| !!n. f(n) == nat_rec c h n |] ==> f(0) = c";
 by (rewtac rew);
 by (rtac nat_rec_0 1);
 qed "def_nat_rec_0";
 
 val [rew] = goal Nat.thy
-    "[| !!n. f(n) == nat_rec n c h |] ==> f(Suc(n)) = h n (f n)";
+    "[| !!n. f(n) == nat_rec c h n |] ==> f(Suc(n)) = h n (f n)";
 by (rewtac rew);
 by (rtac nat_rec_Suc 1);
 qed "def_nat_rec_Suc";
@@ -426,7 +426,7 @@
   (fn [prem] => [rtac (prem RS arg_cong) 1]);
 
 qed_goal "nat_rec_weak_cong" Nat.thy
-  "m=n ==> nat_rec m a f = nat_rec n a f"
+  "m=n ==> nat_rec a f m = nat_rec a f n"
   (fn [prem] => [rtac (prem RS arg_cong) 1]);
 
 val prems = goalw Nat.thy [le_def] "~n<m ==> m<=(n::nat)";
diff -r e1458e1a9f80 -r 44254696843a src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Fri Jun 21 13:51:09 1996 +0200
+++ b/src/HOL/Nat.thy	Tue Jun 25 13:11:29 1996 +0200
@@ -49,7 +49,7 @@
   Suc       :: nat => nat
   nat_case  :: ['a, nat => 'a, nat] => 'a
   pred_nat  :: "(nat * nat) set"
-  nat_rec   :: [nat, 'a, [nat, 'a] => 'a] => 'a
+  nat_rec   :: ['a, [nat, 'a] => 'a, nat] => 'a
 
   Least     :: (nat=>bool) => nat    (binder "LEAST " 10)
 
@@ -71,8 +71,8 @@
 
   le_def        "m<=(n::nat) == ~(n<m)"
 
-  nat_rec_def   "nat_rec n c d ==
-                 wfrec pred_nat (%f. nat_case c (%m. d m (f m))) n"
+  nat_rec_def   "nat_rec c d ==
+                 wfrec pred_nat (%f. nat_case c (%m. d m (f m)))"
   (*least number operator*)
   Least_def     "Least(P) == @k. P(k) & (ALL j. j<k --> ~P(j))"
 
diff -r e1458e1a9f80 -r 44254696843a src/HOL/RelPow.thy
--- a/src/HOL/RelPow.thy	Fri Jun 21 13:51:09 1996 +0200
+++ b/src/HOL/RelPow.thy	Tue Jun 25 13:11:29 1996 +0200
@@ -11,5 +11,5 @@
 consts
   "^" :: "('a * 'a) set => nat => ('a * 'a) set" (infixr 100)
 defs
-  rel_pow_def "R^n == nat_rec n id (%m S. R O S)"
+  rel_pow_def "R^n == nat_rec id (%m S. R O S) n"
 end
diff -r e1458e1a9f80 -r 44254696843a src/HOL/ex/LList.ML
--- a/src/HOL/ex/LList.ML	Fri Jun 21 13:51:09 1996 +0200
+++ b/src/HOL/ex/LList.ML	Tue Jun 25 13:11:29 1996 +0200
@@ -753,13 +753,13 @@
 (** Two lemmas about natrec n x (%m.g), which is essentially (g^n)(x) **)
 
 goal LList.thy
-    "nat_rec n (LCons b l) (%m. lmap(f)) =      \
-\    LCons (nat_rec n b (%m. f)) (nat_rec n l (%m. lmap(f)))";
+    "nat_rec (LCons b l) (%m. lmap(f)) n =      \
+\    LCons (nat_rec b (%m. f) n) (nat_rec l (%m. lmap(f)) n)";
 by (nat_ind_tac "n" 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [lmap_LCons])));
 qed "fun_power_lmap";
 
-goal Nat.thy "nat_rec n (g x) (%m. g) = nat_rec (Suc n) x (%m. g)";
+goal Nat.thy "nat_rec (g x) (%m. g) n = nat_rec x (%m. g) (Suc n)";
 by (nat_ind_tac "n" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "fun_power_Suc";
@@ -773,8 +773,8 @@
     "(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)";
 by (rtac ext 1);
 by (res_inst_tac [("r", 
-   "UN u. range(%n. (nat_rec n (h u) (%m y.lmap f y), \
-\                    nat_rec n (iterates f u) (%m y.lmap f y)))")] 
+   "UN u. range(%n. (nat_rec (h u) (%m y.lmap f y) n, \
+\                    nat_rec (iterates f u) (%m y.lmap f y) n))")] 
     llist_equalityI 1);
 by (REPEAT (resolve_tac [UN1_I, range_eqI, Pair_cong, nat_rec_0 RS sym] 1));
 by (safe_tac (!claset));
diff -r e1458e1a9f80 -r 44254696843a src/HOL/ex/LList.thy
--- a/src/HOL/ex/LList.thy	Fri Jun 21 13:51:09 1996 +0200
+++ b/src/HOL/ex/LList.thy	Tue Jun 25 13:11:29 1996 +0200
@@ -93,8 +93,8 @@
 
   LList_corec_fun_def
     "LList_corec_fun k f == 
-     nat_rec k (%x. {})                         
-              (%j r x. sum_case (%u.NIL) (split(%z w. CONS z (r w))) (f x))"
+     nat_rec (%x. {})                         
+              (%j r x. sum_case (%u.NIL) (split(%z w. CONS z (r w))) (f x)) k"
 
   LList_corec_def
     "LList_corec a f == UN k. LList_corec_fun k f a"
diff -r e1458e1a9f80 -r 44254696843a src/HOL/ex/Mutil.thy
--- a/src/HOL/ex/Mutil.thy	Fri Jun 21 13:51:09 1996 +0200
+++ b/src/HOL/ex/Mutil.thy	Tue Jun 25 13:11:29 1996 +0200
@@ -26,7 +26,7 @@
     Un     "[| a: A;  t: tiling A;  a Int t = {} |] ==> a Un t : tiling A"
 
 defs
-  below_def  "below n    == nat_rec n {} insert"
+  below_def  "below n    == nat_rec {} insert n"
   evnodd_def "evnodd A b == A Int {(i,j). (i+j) mod 2 = b}"
 
 end