src/ZF/Nat.ML
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 15 6c6d2f6e3185
     1.1 --- a/src/ZF/Nat.ML	Fri Sep 17 12:53:53 1993 +0200
     1.2 +++ b/src/ZF/Nat.ML	Fri Sep 17 16:16:38 1993 +0200
     1.3 @@ -95,8 +95,8 @@
     1.4  \    |] ==> m <= n --> P(m) --> P(n)";
     1.5  by (nat_ind_tac "n" prems 1);
     1.6  by (ALLGOALS
     1.7 -    (ASM_SIMP_TAC
     1.8 -     (ZF_ss addrews (prems@distrib_rews@[subset_empty_iff, subset_succ_iff, 
     1.9 +    (asm_simp_tac
    1.10 +     (ZF_ss addsimps (prems@distrib_rews@[subset_empty_iff, subset_succ_iff, 
    1.11  					 Ord_nat RS Ord_in_Ord]))));
    1.12  val nat_induct_from_lemma = result();
    1.13  
    1.14 @@ -127,17 +127,17 @@
    1.15  
    1.16  (** nat_case **)
    1.17  
    1.18 -goalw Nat.thy [nat_case_def] "nat_case(0,a,b) = a";
    1.19 +goalw Nat.thy [nat_case_def] "nat_case(a,b,0) = a";
    1.20  by (fast_tac (ZF_cs addIs [the_equality]) 1);
    1.21  val nat_case_0 = result();
    1.22  
    1.23 -goalw Nat.thy [nat_case_def] "nat_case(succ(m),a,b) = b(m)";
    1.24 +goalw Nat.thy [nat_case_def] "nat_case(a,b,succ(m)) = b(m)";
    1.25  by (fast_tac (ZF_cs addIs [the_equality]) 1);
    1.26  val nat_case_succ = result();
    1.27  
    1.28  val major::prems = goal Nat.thy
    1.29      "[| n: nat;  a: C(0);  !!m. m: nat ==> b(m): C(succ(m))  \
    1.30 -\    |] ==> nat_case(n,a,b) : C(n)";
    1.31 +\    |] ==> nat_case(a,b,n) : C(n)";
    1.32  by (rtac (major RS nat_induct) 1);
    1.33  by (REPEAT (resolve_tac [nat_case_0 RS ssubst,
    1.34  			 nat_case_succ RS ssubst] 1 
    1.35 @@ -145,13 +145,6 @@
    1.36  by (assume_tac 1);
    1.37  val nat_case_type = result();
    1.38  
    1.39 -val prems = goalw Nat.thy [nat_case_def]
    1.40 -    "[| n=n';  a=a';  !!m z. b(m)=b'(m)  \
    1.41 -\    |] ==> nat_case(n,a,b)=nat_case(n',a',b')";
    1.42 -by (REPEAT (resolve_tac [the_cong,disj_cong,ex_cong] 1
    1.43 -     ORELSE EVERY1 (map rtac ((prems RL [ssubst]) @ [iff_refl]))));
    1.44 -val nat_case_cong = result();
    1.45 -
    1.46  
    1.47  (** nat_rec -- used to define eclose and transrec, then obsolete **)
    1.48  
    1.49 @@ -165,11 +158,10 @@
    1.50  val [prem] = goal Nat.thy 
    1.51      "m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))";
    1.52  val nat_rec_ss = ZF_ss 
    1.53 -      addcongs (mk_typed_congs Nat.thy [("b", "[i,i]=>i")])
    1.54 -      addrews [prem, nat_case_succ, nat_succI, Memrel_iff, 
    1.55 -	       vimage_singleton_iff];
    1.56 +      addsimps [prem, nat_case_succ, nat_succI, Memrel_iff, 
    1.57 +		vimage_singleton_iff];
    1.58  by (rtac nat_rec_trans 1);
    1.59 -by (SIMP_TAC nat_rec_ss 1);
    1.60 +by (simp_tac nat_rec_ss 1);
    1.61  val nat_rec_succ = result();
    1.62  
    1.63  (** The union of two natural numbers is a natural number -- their maximum **)