src/HOL/NatDef.ML
changeset 4599 3a4348a3d6ff
parent 4535 f24cebc299e4
child 4614 122015efd4e1
equal deleted inserted replaced
4598:649bf14debe7 4599:3a4348a3d6ff
   487 
   487 
   488 goalw thy [le_def] "!!m. ~ m <= n ==> n<(m::nat)";
   488 goalw thy [le_def] "!!m. ~ m <= n ==> n<(m::nat)";
   489 by (Blast_tac 1);
   489 by (Blast_tac 1);
   490 qed "not_leE";
   490 qed "not_leE";
   491 
   491 
       
   492 goalw thy [le_def] "(~n<=m) = (m<(n::nat))";
       
   493 by (Simp_tac 1);
       
   494 qed "not_le_iff_less";
       
   495 
   492 goalw thy [le_def] "!!m. m < n ==> Suc(m) <= n";
   496 goalw thy [le_def] "!!m. m < n ==> Suc(m) <= n";
   493 by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
   497 by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
   494 by (blast_tac (claset() addSEs [less_irrefl,less_asym]) 1);
   498 by (blast_tac (claset() addSEs [less_irrefl,less_asym]) 1);
   495 qed "Suc_leI";  (*formerly called lessD*)
   499 qed "Suc_leI";  (*formerly called lessD*)
   496 
   500 
   574  by (rtac conjI 1);
   578  by (rtac conjI 1);
   575   by (etac less_imp_le 1);
   579   by (etac less_imp_le 1);
   576  by (etac (less_not_refl2 RS not_sym) 1);
   580  by (etac (less_not_refl2 RS not_sym) 1);
   577 by (blast_tac (claset() addSDs [le_imp_less_or_eq]) 1);
   581 by (blast_tac (claset() addSDs [le_imp_less_or_eq]) 1);
   578 qed "nat_less_le";
   582 qed "nat_less_le";
       
   583 
       
   584 (** max **)
       
   585 
       
   586 goalw thy [max_def] "!!z::nat. (z <= max x y) = (z <= x | z <= y)";
       
   587 by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1);
       
   588 by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
       
   589 qed "le_max_iff_disj";
       
   590 
       
   591 goalw thy [max_def] "!!z::nat. (max x y <= z) = (x <= z & y <= z)";
       
   592 by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1);
       
   593 by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
       
   594 qed "max_le_iff_conj";
       
   595 
       
   596 
       
   597 (** min **)
       
   598 
       
   599 goalw thy [min_def] "!!z::nat. (z <= min x y) = (z <= x & z <= y)";
       
   600 by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1);
       
   601 by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
       
   602 qed "le_min_iff_conj";
       
   603 
       
   604 goalw thy [min_def] "!!z::nat. (min x y <= z) = (x <= z | y <= z)";
       
   605 by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1);
       
   606 by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
       
   607 qed "min_le_iff_disj";
       
   608 
   579 
   609 
   580 (** LEAST -- the least number operator **)
   610 (** LEAST -- the least number operator **)
   581 
   611 
   582 goal thy "(! m::nat. P m --> n <= m) = (! m. m < n --> ~ P m)";
   612 goal thy "(! m::nat. P m --> n <= m) = (! m. m < n --> ~ P m)";
   583 by (blast_tac (claset() addIs [leI] addEs [leE]) 1);
   613 by (blast_tac (claset() addIs [leI] addEs [leE]) 1);