src/HOL/NatDef.ML
changeset 4614 122015efd4e1
parent 4599 3a4348a3d6ff
child 4635 c448e09d0fca
equal deleted inserted replaced
4613:67a726003cf8 4614:122015efd4e1
   298 by (rtac natE 1);
   298 by (rtac natE 1);
   299  by (contr_tac 1);
   299  by (contr_tac 1);
   300 by (etac ssubst 1);
   300 by (etac ssubst 1);
   301 by (rtac zero_less_Suc 1);
   301 by (rtac zero_less_Suc 1);
   302 qed "neq0_conv";
   302 qed "neq0_conv";
   303 Addsimps [neq0_conv];
   303 AddIffs [neq0_conv];
   304 AddSDs [neq0_conv RS iffD1];
   304 
   305 
   305 
   306 bind_thm("gr0I", notI RS (neq0_conv RS iffD1));
   306 bind_thm("gr0I", notI RS (neq0_conv RS iffD1));
   307 
   307 
   308 goal thy "(~(0 < n)) = (n=0)";
   308 goal thy "(~(0 < n)) = (n=0)";
   309 by (rtac iffI 1);
   309 by (rtac iffI 1);
   435 
   435 
   436 goalw thy [le_def] "(i <= 0) = (i = 0)";
   436 goalw thy [le_def] "(i <= 0) = (i = 0)";
   437 by (nat_ind_tac "i" 1);
   437 by (nat_ind_tac "i" 1);
   438 by (ALLGOALS Asm_simp_tac);
   438 by (ALLGOALS Asm_simp_tac);
   439 qed "le_0_eq";
   439 qed "le_0_eq";
       
   440 AddIffs [le_0_eq];
   440 
   441 
   441 Addsimps [(*less_Suc_eq, makes simpset non-confluent*) le0, le_0_eq,
   442 Addsimps [(*less_Suc_eq, makes simpset non-confluent*) le0, le_0_eq,
   442           Suc_n_not_le_n,
   443           Suc_n_not_le_n,
   443           n_not_Suc_n, Suc_n_not_n,
   444           n_not_Suc_n, Suc_n_not_n,
   444           nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
   445           nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
   445 
   446 
   446 goal thy "!!m. (m <= Suc(n)) = (m<=n | m = Suc n)";
   447 goal thy "!!m. (m <= Suc(n)) = (m<=n | m = Suc n)";
   447 by (simp_tac (simpset() addsimps [le_eq_less_Suc]) 1);
   448 by (simp_tac (simpset() addsimps [le_eq_less_Suc]) 1);
   448 by (blast_tac (claset() addSEs [less_SucE] addIs [less_SucI]) 1);
   449 by (blast_tac (claset() addSEs [less_SucE] addIs [less_SucI]) 1);
   449 qed "le_Suc_eq";
   450 qed "le_Suc_eq";
       
   451 
       
   452 (* [| m <= Suc n;  m <= n ==> R;  m = Suc n ==> R |] ==> R *)
       
   453 bind_thm ("le_SucE", le_Suc_eq RS iffD1 RS disjE);
   450 
   454 
   451 (*
   455 (*
   452 goal thy "(Suc m < n | Suc m = n) = (m < n)";
   456 goal thy "(Suc m < n | Suc m = n) = (m < n)";
   453 by (stac (less_Suc_eq RS sym) 1);
   457 by (stac (less_Suc_eq RS sym) 1);
   454 by (rtac Suc_less_eq 1);
   458 by (rtac Suc_less_eq 1);