Changed argument order of nat_rec.
--- 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). *)
--- 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
--- 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'"
--- 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
--- 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)";
--- 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))"
--- 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
--- 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));
--- 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"
--- 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