src/HOL/Nat.thy
changeset 71841 f4626b1f1b96
parent 71836 c095d3143047
child 71851 34ecb540a079
equal deleted inserted replaced
71840:8ed78bb0b915 71841:f4626b1f1b96
   898   by (simp split: nat.split)
   898   by (simp split: nat.split)
   899 
   899 
   900 lemma max_Suc2: "max m (Suc n) = (case m of 0 \<Rightarrow> Suc n | Suc m' \<Rightarrow> Suc (max m' n))"
   900 lemma max_Suc2: "max m (Suc n) = (case m of 0 \<Rightarrow> Suc n | Suc m' \<Rightarrow> Suc (max m' n))"
   901   by (simp split: nat.split)
   901   by (simp split: nat.split)
   902 
   902 
       
   903 lemma max_0_iff[simp]: "max m n = (0::nat) \<longleftrightarrow> m = 0 \<and> n = 0"
       
   904 by(cases m, auto simp: max_Suc1 split: nat.split)
       
   905 
   903 lemma nat_mult_min_left: "min m n * q = min (m * q) (n * q)"
   906 lemma nat_mult_min_left: "min m n * q = min (m * q) (n * q)"
   904   for m n q :: nat
   907   for m n q :: nat
   905   by (simp add: min_def not_le)
   908   by (simp add: min_def not_le)
   906     (auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans)
   909     (auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans)
   907 
   910