# HG changeset patch
# User lcp
# Date 777204471 -7200
# Node ID c53c19fb22cb23eaecf55ffc0797ae5e8104676f
# Parent  82c4117aff7f011151f6ee9fc8348e88f3aec1af
HOL/Nat: rotated arguments of nat_case; added translation for case macro
HOL/Nat/nat_ss0: new, for first definition of nat_ss

diff -r 82c4117aff7f -r c53c19fb22cb Nat.ML
--- 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];
diff -r 82c4117aff7f -r c53c19fb22cb Nat.thy
--- 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