src/HOL/Divides.thy

--- a/src/HOL/Divides.thy	Wed Dec 21 17:37:58 2016 +0100
+++ b/src/HOL/Divides.thy	Tue Dec 20 15:39:13 2016 +0100
@@ -781,7 +781,38 @@
 lemma one_mod_numeral [simp]:
   "1 mod numeral n = snd (divmod num.One n)"
   by (simp add: snd_divmod)
-  
+
+text \<open>Computing congruences modulo \<open>2 ^ q\<close>\<close>
+
+lemma cong_exp_iff_simps:
+  "numeral n mod numeral Num.One = 0
+    \<longleftrightarrow> True"
+  "numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = 0
+    \<longleftrightarrow> numeral n mod numeral q = 0"
+  "numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = 0
+    \<longleftrightarrow> False"
+  "numeral m mod numeral Num.One = (numeral n mod numeral Num.One)
+    \<longleftrightarrow> True"
+  "numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> True"
+  "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> False"
+  "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> (numeral n mod numeral q) = 0"
+  "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> False"
+  "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
+  "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> False"
+  "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> (numeral m mod numeral q) = 0"
+  "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> False"
+  "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
+    \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
+  by (auto simp add: case_prod_beta dest: arg_cong [of _ _ even])
+
 end
 
 
@@ -1636,37 +1667,6 @@
   shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
   by (simp_all add: snd_divmod)
 
-lemma cut_eq_simps: \<comment> \<open>rewriting equivalence on \<open>n mod 2 ^ q\<close>\<close>
-  fixes m n q :: num
-  shows
-    "numeral n mod numeral Num.One = (0::nat)
-      \<longleftrightarrow> True"
-    "numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = (0::nat)
-      \<longleftrightarrow> numeral n mod numeral q = (0::nat)"
-    "numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = (0::nat)
-      \<longleftrightarrow> False"
-    "numeral m mod numeral Num.One = (numeral n mod numeral Num.One :: nat)
-      \<longleftrightarrow> True"
-    "numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q) :: nat)
-      \<longleftrightarrow> True"
-    "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) :: nat)
-      \<longleftrightarrow> False"
-    "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) :: nat)
-      \<longleftrightarrow> (numeral n mod numeral q :: nat) = 0"
-    "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q) :: nat)
-      \<longleftrightarrow> False"
-    "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) :: nat)
-      \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q :: nat)"
-    "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) :: nat)
-      \<longleftrightarrow> False"
-    "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q) :: nat)
-      \<longleftrightarrow> (numeral m mod numeral q :: nat) = 0"
-    "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) :: nat)
-      \<longleftrightarrow> False"
-    "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) :: nat)
-      \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q :: nat)"
-  by (auto simp add: case_prod_beta Suc_double_not_eq_double double_not_eq_Suc_double)
-
 
 subsection \<open>Division on @{typ int}\<close>