# HG changeset patch
# User paulson
# Date 1169803452 -3600
# Node ID d31dec6397bef3714aea4a3430c5d665389d5859
# Parent  10278e56874101f7ab92fa0ebc035f431b07de00
simplification of Suc/numeral combinations with min, max

diff -r 10278e568741 -r d31dec6397be src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Fri Jan 26 10:22:42 2007 +0100
+++ b/src/HOL/Integ/NatBin.thy	Fri Jan 26 10:24:12 2007 +0100
@@ -443,7 +443,7 @@
 
 
 
-subsection{*Comparisons involving Suc *}
+subsection{*Comparisons involving  @{term Suc} *}
 
 lemma eq_number_of_Suc [simp]:
      "(number_of v = Suc n) =  
@@ -543,6 +543,48 @@
 
 
 
+subsection{*Max and Min Combined with @{term Suc} *}
+
+lemma max_number_of_Suc [simp]:
+     "max (Suc n) (number_of v) =  
+        (let pv = number_of (Numeral.pred v) in  
+         if neg pv then Suc n else Suc(max n (nat pv)))"
+apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
+            split add: split_if nat.split)
+apply (rule_tac x = "number_of v" in spec) 
+apply auto
+done
+ 
+lemma max_Suc_number_of [simp]:
+     "max (number_of v) (Suc n) =  
+        (let pv = number_of (Numeral.pred v) in  
+         if neg pv then Suc n else Suc(max (nat pv) n))"
+apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
+            split add: split_if nat.split)
+apply (rule_tac x = "number_of v" in spec) 
+apply auto
+done
+ 
+lemma min_number_of_Suc [simp]:
+     "min (Suc n) (number_of v) =  
+        (let pv = number_of (Numeral.pred v) in  
+         if neg pv then 0 else Suc(min n (nat pv)))"
+apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
+            split add: split_if nat.split)
+apply (rule_tac x = "number_of v" in spec) 
+apply auto
+done
+ 
+lemma min_Suc_number_of [simp]:
+     "min (number_of v) (Suc n) =  
+        (let pv = number_of (Numeral.pred v) in  
+         if neg pv then 0 else Suc(min (nat pv) n))"
+apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
+            split add: split_if nat.split)
+apply (rule_tac x = "number_of v" in spec) 
+apply auto
+done
+ 
 subsection{*Literal arithmetic involving powers*}
 
 lemma nat_power_eq: "(0::int) <= z ==> nat (z^n) = nat z ^ n"