lemmas about +, *, min, max on nat
authorhaftmann
Wed Sep 07 23:07:16 2011 +0200 (2011-09-07)
changeset 44817b63e445c8f6d
parent 44816 efa1f532508b
child 44818 27ba81ad0890
lemmas about +, *, min, max on nat
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Nat.thy	Wed Sep 07 21:31:21 2011 +0200
     1.2 +++ b/src/HOL/Nat.thy	Wed Sep 07 23:07:16 2011 +0200
     1.3 @@ -657,46 +657,6 @@
     1.4  by (cases m) simp_all
     1.5  
     1.6  
     1.7 -subsubsection {* @{term min} and @{term max} *}
     1.8 -
     1.9 -lemma mono_Suc: "mono Suc"
    1.10 -by (rule monoI) simp
    1.11 -
    1.12 -lemma min_0L [simp]: "min 0 n = (0::nat)"
    1.13 -by (rule min_leastL) simp
    1.14 -
    1.15 -lemma min_0R [simp]: "min n 0 = (0::nat)"
    1.16 -by (rule min_leastR) simp
    1.17 -
    1.18 -lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)"
    1.19 -by (simp add: mono_Suc min_of_mono)
    1.20 -
    1.21 -lemma min_Suc1:
    1.22 -   "min (Suc n) m = (case m of 0 => 0 | Suc m' => Suc(min n m'))"
    1.23 -by (simp split: nat.split)
    1.24 -
    1.25 -lemma min_Suc2:
    1.26 -   "min m (Suc n) = (case m of 0 => 0 | Suc m' => Suc(min m' n))"
    1.27 -by (simp split: nat.split)
    1.28 -
    1.29 -lemma max_0L [simp]: "max 0 n = (n::nat)"
    1.30 -by (rule max_leastL) simp
    1.31 -
    1.32 -lemma max_0R [simp]: "max n 0 = (n::nat)"
    1.33 -by (rule max_leastR) simp
    1.34 -
    1.35 -lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc(max m n)"
    1.36 -by (simp add: mono_Suc max_of_mono)
    1.37 -
    1.38 -lemma max_Suc1:
    1.39 -   "max (Suc n) m = (case m of 0 => Suc n | Suc m' => Suc(max n m'))"
    1.40 -by (simp split: nat.split)
    1.41 -
    1.42 -lemma max_Suc2:
    1.43 -   "max m (Suc n) = (case m of 0 => Suc n | Suc m' => Suc(max m' n))"
    1.44 -by (simp split: nat.split)
    1.45 -
    1.46 -
    1.47  subsubsection {* Monotonicity of Addition *}
    1.48  
    1.49  lemma Suc_pred [simp]: "n>0 ==> Suc (n - Suc 0) = n"
    1.50 @@ -753,11 +713,85 @@
    1.51    fix a::nat and b::nat show "a ~= 0 \<Longrightarrow> b ~= 0 \<Longrightarrow> a * b ~= 0" by auto
    1.52  qed
    1.53  
    1.54 -lemma nat_mult_1: "(1::nat) * n = n"
    1.55 -by simp
    1.56 +
    1.57 +subsubsection {* @{term min} and @{term max} *}
    1.58 +
    1.59 +lemma mono_Suc: "mono Suc"
    1.60 +by (rule monoI) simp
    1.61 +
    1.62 +lemma min_0L [simp]: "min 0 n = (0::nat)"
    1.63 +by (rule min_leastL) simp
    1.64 +
    1.65 +lemma min_0R [simp]: "min n 0 = (0::nat)"
    1.66 +by (rule min_leastR) simp
    1.67 +
    1.68 +lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)"
    1.69 +by (simp add: mono_Suc min_of_mono)
    1.70 +
    1.71 +lemma min_Suc1:
    1.72 +   "min (Suc n) m = (case m of 0 => 0 | Suc m' => Suc(min n m'))"
    1.73 +by (simp split: nat.split)
    1.74 +
    1.75 +lemma min_Suc2:
    1.76 +   "min m (Suc n) = (case m of 0 => 0 | Suc m' => Suc(min m' n))"
    1.77 +by (simp split: nat.split)
    1.78 +
    1.79 +lemma max_0L [simp]: "max 0 n = (n::nat)"
    1.80 +by (rule max_leastL) simp
    1.81 +
    1.82 +lemma max_0R [simp]: "max n 0 = (n::nat)"
    1.83 +by (rule max_leastR) simp
    1.84 +
    1.85 +lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc(max m n)"
    1.86 +by (simp add: mono_Suc max_of_mono)
    1.87 +
    1.88 +lemma max_Suc1:
    1.89 +   "max (Suc n) m = (case m of 0 => Suc n | Suc m' => Suc(max n m'))"
    1.90 +by (simp split: nat.split)
    1.91 +
    1.92 +lemma max_Suc2:
    1.93 +   "max m (Suc n) = (case m of 0 => Suc n | Suc m' => Suc(max m' n))"
    1.94 +by (simp split: nat.split)
    1.95  
    1.96 -lemma nat_mult_1_right: "n * (1::nat) = n"
    1.97 -by simp
    1.98 +lemma nat_add_min_left:
    1.99 +  fixes m n q :: nat
   1.100 +  shows "min m n + q = min (m + q) (n + q)"
   1.101 +  by (simp add: min_def)
   1.102 +
   1.103 +lemma nat_add_min_right:
   1.104 +  fixes m n q :: nat
   1.105 +  shows "m + min n q = min (m + n) (m + q)"
   1.106 +  by (simp add: min_def)
   1.107 +
   1.108 +lemma nat_mult_min_left:
   1.109 +  fixes m n q :: nat
   1.110 +  shows "min m n * q = min (m * q) (n * q)"
   1.111 +  by (simp add: min_def not_le) (auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans)
   1.112 +
   1.113 +lemma nat_mult_min_right:
   1.114 +  fixes m n q :: nat
   1.115 +  shows "m * min n q = min (m * n) (m * q)"
   1.116 +  by (simp add: min_def not_le) (auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans)
   1.117 +
   1.118 +lemma nat_add_max_left:
   1.119 +  fixes m n q :: nat
   1.120 +  shows "max m n + q = max (m + q) (n + q)"
   1.121 +  by (simp add: max_def)
   1.122 +
   1.123 +lemma nat_add_max_right:
   1.124 +  fixes m n q :: nat
   1.125 +  shows "m + max n q = max (m + n) (m + q)"
   1.126 +  by (simp add: max_def)
   1.127 +
   1.128 +lemma nat_mult_max_left:
   1.129 +  fixes m n q :: nat
   1.130 +  shows "max m n * q = max (m * q) (n * q)"
   1.131 +  by (simp add: max_def not_le) (auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans)
   1.132 +
   1.133 +lemma nat_mult_max_right:
   1.134 +  fixes m n q :: nat
   1.135 +  shows "m * max n q = max (m * n) (m * q)"
   1.136 +  by (simp add: max_def not_le) (auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans)
   1.137  
   1.138  
   1.139  subsubsection {* Additional theorems about @{term "op \<le>"} *}
   1.140 @@ -1700,6 +1734,15 @@
   1.141  by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
   1.142  
   1.143  
   1.144 +subsection {* aliasses *}
   1.145 +
   1.146 +lemma nat_mult_1: "(1::nat) * n = n"
   1.147 +  by simp
   1.148 + 
   1.149 +lemma nat_mult_1_right: "n * (1::nat) = n"
   1.150 +  by simp
   1.151 +
   1.152 +
   1.153  subsection {* size of a datatype value *}
   1.154  
   1.155  class size =