HOL/Nat: rotated arguments of nat_case; added translation for case macro
HOL/Nat/nat_ss0: new, for first definition of nat_ss
--- a/Nat.ML Thu Aug 18 11:54:20 1994 +0200
+++ b/Nat.ML Thu Aug 18 12:07:51 1994 +0200
@@ -126,11 +126,11 @@
(*** nat_case -- the selection operator for nat ***)
-goalw Nat.thy [nat_case_def] "nat_case(0, a, f) = a";
+goalw Nat.thy [nat_case_def] "nat_case(a, f, 0) = a";
by (fast_tac (set_cs addIs [select_equality] addEs [Zero_neq_Suc]) 1);
val nat_case_0 = result();
-goalw Nat.thy [nat_case_def] "nat_case(Suc(k), a, f) = f(k)";
+goalw Nat.thy [nat_case_def] "nat_case(a, f, Suc(k)) = f(k)";
by (fast_tac (set_cs addIs [select_equality]
addEs [make_elim Suc_inject, Suc_neq_Zero]) 1);
val nat_case_Suc = result();
@@ -165,13 +165,12 @@
goal Nat.thy "nat_rec(0,c,h) = c";
by (rtac (nat_rec_unfold RS trans) 1);
-by (rtac nat_case_0 1);
+by (simp_tac (HOL_ss addsimps [nat_case_0]) 1);
val nat_rec_0 = result();
goal Nat.thy "nat_rec(Suc(n), c, h) = h(n, nat_rec(n,c,h))";
by (rtac (nat_rec_unfold RS trans) 1);
-by (rtac (nat_case_Suc RS trans) 1);
-by(simp_tac (HOL_ss addsimps [pred_natI,cut_apply]) 1);
+by (simp_tac (HOL_ss addsimps [nat_case_Suc, pred_natI, cut_apply]) 1);
val nat_rec_Suc = result();
(*These 2 rules ease the use of primitive recursion. NOTE USE OF == *)
@@ -348,16 +347,16 @@
val le0 = result();
val nat_simps = [not_less0, less_not_refl, zero_less_Suc, lessI,
- Suc_less_eq, less_Suc_eq, le0, not_Suc_n_less_n,
- Suc_not_Zero, Zero_not_Suc, Suc_Suc_eq,
- n_not_Suc_n, Suc_n_not_n,
- nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
+ Suc_less_eq, less_Suc_eq, le0, not_Suc_n_less_n,
+ Suc_not_Zero, Zero_not_Suc, Suc_Suc_eq,
+ n_not_Suc_n, Suc_n_not_n,
+ nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
-val nat_ss = sum_ss addsimps nat_simps;
+val nat_ss0 = sum_ss addsimps nat_simps;
(*Prevents simplification of f and g: much faster*)
val nat_case_weak_cong = prove_goal Nat.thy
- "m=n ==> nat_case(m,a,f) = nat_case(n,a,f)"
+ "m=n ==> nat_case(a,f,m) = nat_case(a,f,n)"
(fn [prem] => [rtac (prem RS arg_cong) 1]);
val nat_rec_weak_cong = prove_goal Nat.thy
@@ -379,12 +378,12 @@
val not_leE = result();
goalw Nat.thy [le_def] "!!m. m < n ==> Suc(m) <= n";
-by(simp_tac nat_ss 1);
+by(simp_tac nat_ss0 1);
by (fast_tac (HOL_cs addEs [less_anti_refl,less_asym]) 1);
val lessD = result();
goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
-by(asm_full_simp_tac nat_ss 1);
+by(asm_full_simp_tac nat_ss0 1);
by(fast_tac HOL_cs 1);
val Suc_leD = result();
@@ -426,4 +425,4 @@
fast_tac (HOL_cs addEs [less_anti_refl,less_asym])]);
val le_anti_sym = result();
-val nat_ss = nat_ss addsimps [le_refl];
+val nat_ss = nat_ss0 addsimps [le_refl];
--- a/Nat.thy Thu Aug 18 11:54:20 1994 +0200
+++ b/Nat.thy Thu Aug 18 12:07:51 1994 +0200
@@ -25,11 +25,14 @@
Rep_Nat :: "nat => ind"
Abs_Nat :: "ind => nat"
Suc :: "nat => nat"
- nat_case :: "[nat, 'a, nat=>'a] =>'a"
+ nat_case :: "['a, nat=>'a, nat] =>'a"
pred_nat :: "(nat*nat) set"
nat_rec :: "[nat, 'a, [nat, 'a]=>'a] => 'a"
"0" :: "nat" ("0")
+translations
+ "case p of 0 => a | Suc(y) => b" == "nat_case(a, %y.b, p)"
+
rules
(*the axiom of infinity in 2 parts*)
inj_Suc_Rep "inj(Suc_Rep)"
@@ -43,8 +46,8 @@
Zero_def "0 == Abs_Nat(Zero_Rep)"
Suc_def "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
(*nat operations and recursion*)
- nat_case_def "nat_case == (%n a f. @z. (n=0 --> z=a) \
-\ & (!x. n=Suc(x) --> z=f(x)))"
+ nat_case_def "nat_case(a,f,n) == @z. (n=0 --> z=a) \
+\ & (!x. n=Suc(x) --> z=f(x))"
pred_nat_def "pred_nat == {p. ? n. p = <n, Suc(n)>}"
less_def "m<n == <m,n>:trancl(pred_nat)"
@@ -52,5 +55,5 @@
le_def "m<=(n::nat) == ~(n<m)"
nat_rec_def "nat_rec(n,c,d) == wfrec(pred_nat, n, \
-\ %l g. nat_case(l, c, %m. d(m,g(m))))"
+\ nat_case(%g.c, %m g. d(m,g(m))))"
end