src/HOL/Nat.ML
changeset 1823 e1458e1a9f80
parent 1817 3994d37b16ae
child 1824 44254696843a
equal deleted inserted replaced
1822:c192d7dc22e7 1823:e1458e1a9f80
   460 (* stronger version of Suc_leD *)
   460 (* stronger version of Suc_leD *)
   461 goalw Nat.thy [le_def] 
   461 goalw Nat.thy [le_def] 
   462         "!!m. Suc m <= n ==> m < n";
   462         "!!m. Suc m <= n ==> m < n";
   463 by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
   463 by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
   464 by (cut_facts_tac [less_linear] 1);
   464 by (cut_facts_tac [less_linear] 1);
   465 by (fast_tac HOL_cs 1);
   465 by (Fast_tac 1);
   466 qed "Suc_le_lessD";
   466 qed "Suc_le_lessD";
   467 
   467 
   468 goal Nat.thy "(Suc m <= n) = (m < n)";
   468 goal Nat.thy "(Suc m <= n) = (m < n)";
   469 by (fast_tac (!claset addIs [lessD, Suc_le_lessD]) 1);
   469 by (fast_tac (!claset addIs [lessD, Suc_le_lessD]) 1);
   470 qed "Suc_le_eq";
   470 qed "Suc_le_eq";