# HG changeset patch
# User haftmann
# Date 1388261184 -3600
# Node ID af81b2357e089c8e3e5ed403b018d7d0bc742204
# Parent  51612b889361fd4e12c75670594ab7eede5a80e7
postpone dis"useful" lemmas

diff -r 51612b889361 -r af81b2357e08 src/HOL/Word/Misc_Numeric.thy
--- a/src/HOL/Word/Misc_Numeric.thy	Sat Dec 28 21:06:22 2013 +0100
+++ b/src/HOL/Word/Misc_Numeric.thy	Sat Dec 28 21:06:24 2013 +0100
@@ -8,32 +8,6 @@
 imports Main Parity
 begin
 
-declare iszero_0 [intro]
-
-lemma min_pm [simp]:
-  "min a b + (a - b) = (a :: nat)"
-  by arith
-  
-lemma min_pm1 [simp]:
-  "a - b + min a b = (a :: nat)"
-  by arith
-
-lemma rev_min_pm [simp]:
-  "min b a + (a - b) = (a :: nat)"
-  by arith
-
-lemma rev_min_pm1 [simp]:
-  "a - b + min b a = (a :: nat)"
-  by arith
-
-lemma min_minus [simp]:
-  "min m (m - k) = (m - k :: nat)"
-  by arith
-  
-lemma min_minus' [simp]:
-  "min (m - k) m = (m - k :: nat)"
-  by arith
-
 lemma mod_2_neq_1_eq_eq_0:
   fixes k :: int
   shows "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0"
diff -r 51612b889361 -r af81b2357e08 src/HOL/Word/Word_Miscellaneous.thy
--- a/src/HOL/Word/Word_Miscellaneous.thy	Sat Dec 28 21:06:22 2013 +0100
+++ b/src/HOL/Word/Word_Miscellaneous.thy	Sat Dec 28 21:06:24 2013 +0100
@@ -377,5 +377,31 @@
   apply (auto intro: pos_imp_zdiv_nonneg_iff [THEN iffD2])
   done
 
+declare iszero_0 [intro]
+
+lemma min_pm [simp]:
+  "min a b + (a - b) = (a :: nat)"
+  by arith
+  
+lemma min_pm1 [simp]:
+  "a - b + min a b = (a :: nat)"
+  by arith
+
+lemma rev_min_pm [simp]:
+  "min b a + (a - b) = (a :: nat)"
+  by arith
+
+lemma rev_min_pm1 [simp]:
+  "a - b + min b a = (a :: nat)"
+  by arith
+
+lemma min_minus [simp]:
+  "min m (m - k) = (m - k :: nat)"
+  by arith
+  
+lemma min_minus' [simp]:
+  "min (m - k) m = (m - k :: nat)"
+  by arith
+
 end