src/HOL/String.thy
changeset 64630 96015aecfeba
parent 63950 cdc1e59aa513
child 64994 6e4c05e8edbb
     1.1 --- a/src/HOL/String.thy	Wed Dec 21 17:37:58 2016 +0100
     1.2 +++ b/src/HOL/String.thy	Tue Dec 20 15:39:13 2016 +0100
     1.3 @@ -114,7 +114,7 @@
     1.4    "nat_of_char (Char k) = numeral k mod 256"
     1.5    by (simp add: Char_def)
     1.6  
     1.7 -lemma Char_eq_Char_iff [simp]:
     1.8 +lemma Char_eq_Char_iff:
     1.9    "Char k = Char l \<longleftrightarrow> numeral k mod (256 :: nat) = numeral l mod 256" (is "?P \<longleftrightarrow> ?Q")
    1.10  proof -
    1.11    have "?P \<longleftrightarrow> nat_of_char (Char k) = nat_of_char (Char l)"
    1.12 @@ -124,14 +124,25 @@
    1.13    finally show ?thesis .
    1.14  qed
    1.15  
    1.16 -lemma zero_eq_Char_iff [simp]:
    1.17 +lemma zero_eq_Char_iff:
    1.18    "0 = Char k \<longleftrightarrow> numeral k mod (256 :: nat) = 0"
    1.19    by (auto simp add: zero_char_def Char_def)
    1.20  
    1.21 -lemma Char_eq_zero_iff [simp]:
    1.22 +lemma Char_eq_zero_iff:
    1.23    "Char k = 0 \<longleftrightarrow> numeral k mod (256 :: nat) = 0"
    1.24    by (auto simp add: zero_char_def Char_def) 
    1.25  
    1.26 +simproc_setup char_eq
    1.27 +  ("Char m = Char n" | "Char m = 0" | "0 = Char n") = \<open>
    1.28 +  let
    1.29 +    val ss = put_simpset HOL_ss @{context}
    1.30 +      |> fold Simplifier.add_simp @{thms Char_eq_Char_iff zero_eq_Char_iff Char_eq_zero_iff cong_exp_iff_simps}
    1.31 +      |> simpset_of 
    1.32 +  in
    1.33 +    fn _ => fn ctxt => SOME o Simplifier.rewrite (put_simpset ss ctxt)
    1.34 +  end
    1.35 +\<close>
    1.36 +
    1.37  definition integer_of_char :: "char \<Rightarrow> integer"
    1.38  where
    1.39    "integer_of_char = integer_of_nat \<circ> nat_of_char"