src/HOL/Nat.thy
changeset 63113 fe31996e3898
parent 63111 caa0c513bbca
child 63145 703edebd1d92
equal deleted inserted replaced
63112:6813818baa67 63113:fe31996e3898
   524   unfolding not_less less_Suc_eq_le by (rule antisym)
   524   unfolding not_less less_Suc_eq_le by (rule antisym)
   525 
   525 
   526 lemma nat_neq_iff: "m \<noteq> n \<longleftrightarrow> m < n \<or> n < m" for m n :: nat
   526 lemma nat_neq_iff: "m \<noteq> n \<longleftrightarrow> m < n \<or> n < m" for m n :: nat
   527   by (rule linorder_neq_iff)
   527   by (rule linorder_neq_iff)
   528 
   528 
   529 lemma nat_less_cases:
       
   530   fixes m n :: nat
       
   531   assumes major: "m < n \<Longrightarrow> P n m"
       
   532     and eq: "m = n \<Longrightarrow> P n m"
       
   533     and less: "n < m \<Longrightarrow> P n m"
       
   534   shows "P n m"
       
   535   apply (rule less_linear [THEN disjE])
       
   536   apply (erule_tac [2] disjE)
       
   537   apply (erule less)
       
   538   apply (erule sym [THEN eq])
       
   539   apply (erule major)
       
   540   done
       
   541 
       
   542 
   529 
   543 subsubsection \<open>Inductive (?) properties\<close>
   530 subsubsection \<open>Inductive (?) properties\<close>
   544 
   531 
   545 lemma Suc_lessI: "m < n \<Longrightarrow> Suc m \<noteq> n \<Longrightarrow> Suc m < n"
   532 lemma Suc_lessI: "m < n \<Longrightarrow> Suc m \<noteq> n \<Longrightarrow> Suc m < n"
   546   unfolding less_eq_Suc_le [of m] le_less by simp
   533   unfolding less_eq_Suc_le [of m] le_less by simp
  1238 
  1225 
  1239 text \<open>Lemma for \<open>gcd\<close>\<close>
  1226 text \<open>Lemma for \<open>gcd\<close>\<close>
  1240 lemma mult_eq_self_implies_10: "m = m * n \<Longrightarrow> n = 1 \<or> m = 0" for m n :: nat
  1227 lemma mult_eq_self_implies_10: "m = m * n \<Longrightarrow> n = 1 \<or> m = 0" for m n :: nat
  1241   apply (drule sym)
  1228   apply (drule sym)
  1242   apply (rule disjCI)
  1229   apply (rule disjCI)
  1243   apply (rule nat_less_cases, erule_tac [2] _)
  1230   apply (rule linorder_cases, erule_tac [2] _)
  1244    apply (drule_tac [2] mult_less_mono2)
  1231    apply (drule_tac [2] mult_less_mono2)
  1245     apply (auto)
  1232     apply (auto)
  1246   done
  1233   done
  1247 
  1234 
  1248 lemma mono_times_nat:
  1235 lemma mono_times_nat: