# HG changeset patch
# User haftmann
# Date 1482244753 -3600
# Node ID 96015aecfeba6e818a8b89751220f44b3acbd261
# Parent  a331208010b61a04b7879ffcfd46e5791f38e310
emphasize dedicated rewrite rules for congruences

diff -r a331208010b6 -r 96015aecfeba 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>
 
diff -r a331208010b6 -r 96015aecfeba src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Wed Dec 21 17:37:58 2016 +0100
+++ b/src/HOL/Statespace/state_fun.ML	Tue Dec 20 15:39:13 2016 +0100
@@ -77,7 +77,7 @@
 fun string_eq_simp_tac ctxt =
   simp_tac (put_simpset HOL_basic_ss ctxt
     addsimps @{thms list.inject list.distinct Char_eq_Char_iff
-      cut_eq_simps simp_thms}
+      cong_exp_iff_simps simp_thms}
     addsimprocs [lazy_conj_simproc]
     |> Simplifier.add_cong @{thm block_conj_cong});
 
diff -r a331208010b6 -r 96015aecfeba src/HOL/String.thy
--- a/src/HOL/String.thy	Wed Dec 21 17:37:58 2016 +0100
+++ b/src/HOL/String.thy	Tue Dec 20 15:39:13 2016 +0100
@@ -114,7 +114,7 @@
   "nat_of_char (Char k) = numeral k mod 256"
   by (simp add: Char_def)
 
-lemma Char_eq_Char_iff [simp]:
+lemma Char_eq_Char_iff:
   "Char k = Char l \<longleftrightarrow> numeral k mod (256 :: nat) = numeral l mod 256" (is "?P \<longleftrightarrow> ?Q")
 proof -
   have "?P \<longleftrightarrow> nat_of_char (Char k) = nat_of_char (Char l)"
@@ -124,14 +124,25 @@
   finally show ?thesis .
 qed
 
-lemma zero_eq_Char_iff [simp]:
+lemma zero_eq_Char_iff:
   "0 = Char k \<longleftrightarrow> numeral k mod (256 :: nat) = 0"
   by (auto simp add: zero_char_def Char_def)
 
-lemma Char_eq_zero_iff [simp]:
+lemma Char_eq_zero_iff:
   "Char k = 0 \<longleftrightarrow> numeral k mod (256 :: nat) = 0"
   by (auto simp add: zero_char_def Char_def) 
 
+simproc_setup char_eq
+  ("Char m = Char n" | "Char m = 0" | "0 = Char n") = \<open>
+  let
+    val ss = put_simpset HOL_ss @{context}
+      |> fold Simplifier.add_simp @{thms Char_eq_Char_iff zero_eq_Char_iff Char_eq_zero_iff cong_exp_iff_simps}
+      |> simpset_of 
+  in
+    fn _ => fn ctxt => SOME o Simplifier.rewrite (put_simpset ss ctxt)
+  end
+\<close>
+
 definition integer_of_char :: "char \<Rightarrow> integer"
 where
   "integer_of_char = integer_of_nat \<circ> nat_of_char"