emphasize dedicated rewrite rules for congruences
authorhaftmann
Tue Dec 20 15:39:13 2016 +0100 (2016-12-20)
changeset 6463096015aecfeba
parent 64629 a331208010b6
child 64631 7705926ee595
emphasize dedicated rewrite rules for congruences
src/HOL/Divides.thy
src/HOL/Statespace/state_fun.ML
src/HOL/String.thy
     1.1 --- a/src/HOL/Divides.thy	Wed Dec 21 17:37:58 2016 +0100
     1.2 +++ b/src/HOL/Divides.thy	Tue Dec 20 15:39:13 2016 +0100
     1.3 @@ -781,7 +781,38 @@
     1.4  lemma one_mod_numeral [simp]:
     1.5    "1 mod numeral n = snd (divmod num.One n)"
     1.6    by (simp add: snd_divmod)
     1.7 -  
     1.8 +
     1.9 +text \<open>Computing congruences modulo \<open>2 ^ q\<close>\<close>
    1.10 +
    1.11 +lemma cong_exp_iff_simps:
    1.12 +  "numeral n mod numeral Num.One = 0
    1.13 +    \<longleftrightarrow> True"
    1.14 +  "numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = 0
    1.15 +    \<longleftrightarrow> numeral n mod numeral q = 0"
    1.16 +  "numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = 0
    1.17 +    \<longleftrightarrow> False"
    1.18 +  "numeral m mod numeral Num.One = (numeral n mod numeral Num.One)
    1.19 +    \<longleftrightarrow> True"
    1.20 +  "numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
    1.21 +    \<longleftrightarrow> True"
    1.22 +  "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
    1.23 +    \<longleftrightarrow> False"
    1.24 +  "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
    1.25 +    \<longleftrightarrow> (numeral n mod numeral q) = 0"
    1.26 +  "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
    1.27 +    \<longleftrightarrow> False"
    1.28 +  "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
    1.29 +    \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
    1.30 +  "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
    1.31 +    \<longleftrightarrow> False"
    1.32 +  "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
    1.33 +    \<longleftrightarrow> (numeral m mod numeral q) = 0"
    1.34 +  "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
    1.35 +    \<longleftrightarrow> False"
    1.36 +  "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
    1.37 +    \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
    1.38 +  by (auto simp add: case_prod_beta dest: arg_cong [of _ _ even])
    1.39 +
    1.40  end
    1.41  
    1.42  
    1.43 @@ -1636,37 +1667,6 @@
    1.44    shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
    1.45    by (simp_all add: snd_divmod)
    1.46  
    1.47 -lemma cut_eq_simps: \<comment> \<open>rewriting equivalence on \<open>n mod 2 ^ q\<close>\<close>
    1.48 -  fixes m n q :: num
    1.49 -  shows
    1.50 -    "numeral n mod numeral Num.One = (0::nat)
    1.51 -      \<longleftrightarrow> True"
    1.52 -    "numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = (0::nat)
    1.53 -      \<longleftrightarrow> numeral n mod numeral q = (0::nat)"
    1.54 -    "numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = (0::nat)
    1.55 -      \<longleftrightarrow> False"
    1.56 -    "numeral m mod numeral Num.One = (numeral n mod numeral Num.One :: nat)
    1.57 -      \<longleftrightarrow> True"
    1.58 -    "numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q) :: nat)
    1.59 -      \<longleftrightarrow> True"
    1.60 -    "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) :: nat)
    1.61 -      \<longleftrightarrow> False"
    1.62 -    "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) :: nat)
    1.63 -      \<longleftrightarrow> (numeral n mod numeral q :: nat) = 0"
    1.64 -    "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q) :: nat)
    1.65 -      \<longleftrightarrow> False"
    1.66 -    "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) :: nat)
    1.67 -      \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q :: nat)"
    1.68 -    "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) :: nat)
    1.69 -      \<longleftrightarrow> False"
    1.70 -    "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q) :: nat)
    1.71 -      \<longleftrightarrow> (numeral m mod numeral q :: nat) = 0"
    1.72 -    "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) :: nat)
    1.73 -      \<longleftrightarrow> False"
    1.74 -    "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) :: nat)
    1.75 -      \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q :: nat)"
    1.76 -  by (auto simp add: case_prod_beta Suc_double_not_eq_double double_not_eq_Suc_double)
    1.77 -
    1.78  
    1.79  subsection \<open>Division on @{typ int}\<close>
    1.80  
     2.1 --- a/src/HOL/Statespace/state_fun.ML	Wed Dec 21 17:37:58 2016 +0100
     2.2 +++ b/src/HOL/Statespace/state_fun.ML	Tue Dec 20 15:39:13 2016 +0100
     2.3 @@ -77,7 +77,7 @@
     2.4  fun string_eq_simp_tac ctxt =
     2.5    simp_tac (put_simpset HOL_basic_ss ctxt
     2.6      addsimps @{thms list.inject list.distinct Char_eq_Char_iff
     2.7 -      cut_eq_simps simp_thms}
     2.8 +      cong_exp_iff_simps simp_thms}
     2.9      addsimprocs [lazy_conj_simproc]
    2.10      |> Simplifier.add_cong @{thm block_conj_cong});
    2.11  
     3.1 --- a/src/HOL/String.thy	Wed Dec 21 17:37:58 2016 +0100
     3.2 +++ b/src/HOL/String.thy	Tue Dec 20 15:39:13 2016 +0100
     3.3 @@ -114,7 +114,7 @@
     3.4    "nat_of_char (Char k) = numeral k mod 256"
     3.5    by (simp add: Char_def)
     3.6  
     3.7 -lemma Char_eq_Char_iff [simp]:
     3.8 +lemma Char_eq_Char_iff:
     3.9    "Char k = Char l \<longleftrightarrow> numeral k mod (256 :: nat) = numeral l mod 256" (is "?P \<longleftrightarrow> ?Q")
    3.10  proof -
    3.11    have "?P \<longleftrightarrow> nat_of_char (Char k) = nat_of_char (Char l)"
    3.12 @@ -124,14 +124,25 @@
    3.13    finally show ?thesis .
    3.14  qed
    3.15  
    3.16 -lemma zero_eq_Char_iff [simp]:
    3.17 +lemma zero_eq_Char_iff:
    3.18    "0 = Char k \<longleftrightarrow> numeral k mod (256 :: nat) = 0"
    3.19    by (auto simp add: zero_char_def Char_def)
    3.20  
    3.21 -lemma Char_eq_zero_iff [simp]:
    3.22 +lemma Char_eq_zero_iff:
    3.23    "Char k = 0 \<longleftrightarrow> numeral k mod (256 :: nat) = 0"
    3.24    by (auto simp add: zero_char_def Char_def) 
    3.25  
    3.26 +simproc_setup char_eq
    3.27 +  ("Char m = Char n" | "Char m = 0" | "0 = Char n") = \<open>
    3.28 +  let
    3.29 +    val ss = put_simpset HOL_ss @{context}
    3.30 +      |> fold Simplifier.add_simp @{thms Char_eq_Char_iff zero_eq_Char_iff Char_eq_zero_iff cong_exp_iff_simps}
    3.31 +      |> simpset_of 
    3.32 +  in
    3.33 +    fn _ => fn ctxt => SOME o Simplifier.rewrite (put_simpset ss ctxt)
    3.34 +  end
    3.35 +\<close>
    3.36 +
    3.37  definition integer_of_char :: "char \<Rightarrow> integer"
    3.38  where
    3.39    "integer_of_char = integer_of_nat \<circ> nat_of_char"