src/HOL/Num.thy
changeset 61630 608520e0e8e2
parent 61169 4de9ff3ea29a
child 61799 4cf66f21b764
     1.1 --- a/src/HOL/Num.thy	Wed Nov 11 09:21:56 2015 +0100
     1.2 +++ b/src/HOL/Num.thy	Wed Nov 11 09:48:24 2015 +0100
     1.3 @@ -174,6 +174,9 @@
     1.4    using nat_of_num_pos [of n] nat_of_num_pos [of m]
     1.5    by (auto simp add: less_eq_num_def less_num_def)
     1.6  
     1.7 +lemma le_num_One_iff: "x \<le> num.One \<longleftrightarrow> x = num.One"
     1.8 +by (simp add: antisym_conv)
     1.9 +
    1.10  text \<open>Rules using @{text One} and @{text inc} as constructors\<close>
    1.11  
    1.12  lemma add_One: "x + One = inc x"
    1.13 @@ -646,6 +649,26 @@
    1.14    zero_less_numeral
    1.15    not_numeral_less_zero
    1.16  
    1.17 +lemma min_0_1 [simp]:
    1.18 +  fixes min' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" defines "min' \<equiv> min" shows
    1.19 +  "min' 0 1 = 0"
    1.20 +  "min' 1 0 = 0"
    1.21 +  "min' 0 (numeral x) = 0"
    1.22 +  "min' (numeral x) 0 = 0"
    1.23 +  "min' 1 (numeral x) = 1"
    1.24 +  "min' (numeral x) 1 = 1"
    1.25 +by(simp_all add: min'_def min_def le_num_One_iff)
    1.26 +
    1.27 +lemma max_0_1 [simp]: 
    1.28 +  fixes max' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" defines "max' \<equiv> max" shows
    1.29 +  "max' 0 1 = 1"
    1.30 +  "max' 1 0 = 1"
    1.31 +  "max' 0 (numeral x) = numeral x"
    1.32 +  "max' (numeral x) 0 = numeral x"
    1.33 +  "max' 1 (numeral x) = numeral x"
    1.34 +  "max' (numeral x) 1 = numeral x"
    1.35 +by(simp_all add: max'_def max_def le_num_One_iff)
    1.36 +
    1.37  end
    1.38  
    1.39  subsubsection \<open>