src/HOL/String.thy
changeset 62364 9209770bdcdf
parent 61799 4cf66f21b764
child 62580 7011429f44f9
     1.1 --- a/src/HOL/String.thy	Fri Feb 19 15:01:38 2016 +0100
     1.2 +++ b/src/HOL/String.thy	Thu Feb 18 17:52:52 2016 +0100
     1.3 @@ -6,8 +6,92 @@
     1.4  imports Enum
     1.5  begin
     1.6  
     1.7 +lemma upt_conv_Cons_Cons: -- \<open>no precondition\<close> -- \<open>FIXME move\<close>
     1.8 +  "m # n # ns = [m..<q] \<longleftrightarrow> n # ns = [Suc m..<q]"
     1.9 +proof (cases "m < q")
    1.10 +  case False then show ?thesis by simp
    1.11 +next
    1.12 +  case True then show ?thesis by (simp add: upt_conv_Cons)
    1.13 +qed
    1.14 +
    1.15 +
    1.16  subsection \<open>Characters and strings\<close>
    1.17  
    1.18 +subsubsection \<open>Characters as finite algebraic type\<close>
    1.19 +
    1.20 +typedef char = "{n::nat. n < 256}"
    1.21 +  morphisms nat_of_char Abs_char
    1.22 +proof
    1.23 +  show "Suc 0 \<in> {n. n < 256}" by simp
    1.24 +qed
    1.25 +
    1.26 +definition char_of_nat :: "nat \<Rightarrow> char"
    1.27 +where
    1.28 +  "char_of_nat n = Abs_char (n mod 256)"
    1.29 +
    1.30 +lemma char_cases [case_names char_of_nat, cases type: char]:
    1.31 +  "(\<And>n. c = char_of_nat n \<Longrightarrow> n < 256 \<Longrightarrow> P) \<Longrightarrow> P"
    1.32 +  by (cases c) (simp add: char_of_nat_def)
    1.33 +
    1.34 +lemma char_of_nat_of_char [simp]:
    1.35 +  "char_of_nat (nat_of_char c) = c"
    1.36 +  by (cases c) (simp add: char_of_nat_def Abs_char_inject Abs_char_inverse)
    1.37 +
    1.38 +lemma inj_nat_of_char:
    1.39 +  "inj nat_of_char"
    1.40 +proof (rule injI)
    1.41 +  fix c d
    1.42 +  assume "nat_of_char c = nat_of_char d"
    1.43 +  then have "char_of_nat (nat_of_char c) = char_of_nat (nat_of_char d)"
    1.44 +    by simp
    1.45 +  then show "c = d"
    1.46 +    by simp
    1.47 +qed
    1.48 +  
    1.49 +lemma nat_of_char_eq_iff [simp]:
    1.50 +  "nat_of_char c = nat_of_char d \<longleftrightarrow> c = d"
    1.51 +  by (fact nat_of_char_inject)
    1.52 +
    1.53 +lemma nat_of_char_of_nat [simp]:
    1.54 +  "nat_of_char (char_of_nat n) = n mod 256"
    1.55 +  by (cases "char_of_nat n") (simp add: char_of_nat_def Abs_char_inject Abs_char_inverse)
    1.56 +
    1.57 +lemma char_of_nat_mod_256 [simp]:
    1.58 +  "char_of_nat (n mod 256) = char_of_nat n"
    1.59 +  by (cases "char_of_nat (n mod 256)") (simp add: char_of_nat_def)
    1.60 +
    1.61 +lemma char_of_nat_quasi_inj [simp]:
    1.62 +  "char_of_nat m = char_of_nat n \<longleftrightarrow> m mod 256 = n mod 256"
    1.63 +  by (simp add: char_of_nat_def Abs_char_inject)
    1.64 +
    1.65 +lemma inj_on_char_of_nat [simp]:
    1.66 +  "inj_on char_of_nat {0..<256}"
    1.67 +  by (rule inj_onI) simp
    1.68 +
    1.69 +lemma nat_of_char_mod_256 [simp]:
    1.70 +  "nat_of_char c mod 256 = nat_of_char c"
    1.71 +  by (cases c) simp
    1.72 +
    1.73 +lemma nat_of_char_less_256 [simp]:
    1.74 +  "nat_of_char c < 256"
    1.75 +proof -
    1.76 +  have "nat_of_char c mod 256 < 256"
    1.77 +    by arith
    1.78 +  then show ?thesis by simp
    1.79 +qed
    1.80 +
    1.81 +lemma UNIV_char_of_nat:
    1.82 +  "UNIV = char_of_nat ` {0..<256}"
    1.83 +proof -
    1.84 +  { fix c
    1.85 +    have "c \<in> char_of_nat ` {0..<256}"
    1.86 +      by (cases c) auto
    1.87 +  } then show ?thesis by auto
    1.88 +qed
    1.89 +
    1.90 +
    1.91 +subsubsection \<open>Traditional concrete representation of characters\<close>
    1.92 +
    1.93  datatype (plugins del: transfer) nibble =
    1.94      Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
    1.95    | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
    1.96 @@ -114,9 +198,78 @@
    1.97    "nibble_of_nat (n mod 16) = nibble_of_nat n"
    1.98    by (simp add: nibble_of_nat_def)
    1.99  
   1.100 -datatype char = Char nibble nibble
   1.101 +context
   1.102 +begin
   1.103 +
   1.104 +local_setup \<open>Local_Theory.map_background_naming (Name_Space.add_path "char")\<close>
   1.105 +
   1.106 +definition Char :: "nibble \<Rightarrow> nibble \<Rightarrow> char"
   1.107 +where
   1.108 +  "Char x y = char_of_nat (nat_of_nibble x * 16 + nat_of_nibble y)"
   1.109    \<comment> "Note: canonical order of character encoding coincides with standard term ordering"
   1.110  
   1.111 +end
   1.112 +
   1.113 +lemma nat_of_char_Char:
   1.114 +  "nat_of_char (Char x y) = nat_of_nibble x * 16 + nat_of_nibble y" (is "_ = ?rhs")
   1.115 +proof -
   1.116 +  have "?rhs < 256"
   1.117 +    using nat_of_nibble_less_16 [of x] nat_of_nibble_less_16 [of y]
   1.118 +    by arith
   1.119 +  then show ?thesis by (simp add: Char_def)
   1.120 +qed
   1.121 +
   1.122 +lemma char_of_nat_Char_nibbles:
   1.123 +  "char_of_nat n = Char (nibble_of_nat (n div 16)) (nibble_of_nat n)"
   1.124 +proof -
   1.125 +  from mod_mult2_eq [of n 16 16]
   1.126 +  have "n mod 256 = 16 * (n div 16 mod 16) + n mod 16" by simp
   1.127 +  then show ?thesis
   1.128 +    by (simp add: Char_def)
   1.129 +qed
   1.130 +
   1.131 +lemma char_of_nat_nibble_pair [simp]:
   1.132 +  "char_of_nat (nat_of_nibble a * 16 + nat_of_nibble b) = Char a b"
   1.133 +  by (simp add: nat_of_char_Char [symmetric])
   1.134 +
   1.135 +free_constructors char for Char
   1.136 +proof -
   1.137 +  fix P c
   1.138 +  assume hyp: "\<And>x y. c = Char x y \<Longrightarrow> P"
   1.139 +  have "nat_of_char c \<le> 255"
   1.140 +    using nat_of_char_less_256 [of c] by arith
   1.141 +  then have "nat_of_char c div 16 \<le> 255 div 16"
   1.142 +    by (auto intro: div_le_mono2)
   1.143 +  then have "nat_of_char c div 16 < 16"
   1.144 +    by auto
   1.145 +  then have "nat_of_char c div 16 mod 16 = nat_of_char c div 16"
   1.146 +    by simp
   1.147 +  then have "c = Char (nibble_of_nat (nat_of_char c div 16))
   1.148 +    (nibble_of_nat (nat_of_char c mod 16))"
   1.149 +    by (simp add: Char_def)
   1.150 +  then show P by (rule hyp)
   1.151 +next
   1.152 +  fix x y z w
   1.153 +  have "Char x y = Char z w
   1.154 +    \<longleftrightarrow> nat_of_char (Char x y) = nat_of_char (Char z w)"
   1.155 +    by auto
   1.156 +  also have "\<dots> \<longleftrightarrow> nat_of_nibble x = nat_of_nibble z \<and> nat_of_nibble y = nat_of_nibble w" (is "?P \<longleftrightarrow> ?Q \<and> ?R")
   1.157 +  proof
   1.158 +    assume "?Q \<and> ?R"
   1.159 +    then show ?P by (simp add: nat_of_char_Char)
   1.160 +  next
   1.161 +    assume ?P
   1.162 +    then have ?Q
   1.163 +      using nat_of_nibble_less_16 [of y] nat_of_nibble_less_16 [of w]
   1.164 +      by (simp add: nat_of_char_Char)
   1.165 +    moreover with \<open>?P\<close> have ?R by (simp add: nat_of_char_Char)
   1.166 +    ultimately show "?Q \<and> ?R" ..
   1.167 +  qed
   1.168 +  also have "\<dots> \<longleftrightarrow> x = z \<and> y = w"
   1.169 +    by (simp add: nat_of_nibble_eq_iff)
   1.170 +  finally show "Char x y = Char z w \<longleftrightarrow> x = z \<and> y = w" .
   1.171 +qed
   1.172 +
   1.173  syntax
   1.174    "_Char" :: "str_position => char"    ("CHR _")
   1.175  
   1.176 @@ -133,11 +286,6 @@
   1.177    fix x show "x \<in> image (case_prod Char) (UNIV \<times> UNIV)" by (cases x) auto
   1.178  qed
   1.179  
   1.180 -lemma size_char [code, simp]:
   1.181 -  "size_char (c::char) = 0"
   1.182 -  "size (c::char) = 0"
   1.183 -  by (cases c, simp)+
   1.184 -
   1.185  instantiation char :: enum
   1.186  begin
   1.187  
   1.188 @@ -238,13 +386,16 @@
   1.189    "card (UNIV :: char set) = 256"
   1.190    by (simp add: card_UNIV_length_enum enum_char_def)
   1.191  
   1.192 -definition nat_of_char :: "char \<Rightarrow> nat"
   1.193 -where
   1.194 -  "nat_of_char c = (case c of Char x y \<Rightarrow> nat_of_nibble x * 16 + nat_of_nibble y)"
   1.195 -
   1.196 -lemma nat_of_char_Char:
   1.197 -  "nat_of_char (Char x y) = nat_of_nibble x * 16 + nat_of_nibble y"
   1.198 -  by (simp add: nat_of_char_def)
   1.199 +lemma enum_char_unfold:
   1.200 +  "Enum.enum = map char_of_nat [0..<256]"
   1.201 +proof -
   1.202 +  have *: "Suc (Suc 0) = 2" by simp
   1.203 +  have "map nat_of_char Enum.enum = [0..<256]"
   1.204 +    by (simp add: enum_char_def nat_of_char_Char upt_conv_Cons_Cons *)
   1.205 +  then have "map char_of_nat (map nat_of_char Enum.enum) =
   1.206 +    map char_of_nat [0..<256]" by simp
   1.207 +  then show ?thesis by (simp add: comp_def)
   1.208 +qed
   1.209  
   1.210  setup \<open>
   1.211  let
   1.212 @@ -268,7 +419,7 @@
   1.213  lemma nibble_of_nat_of_char_div_16:
   1.214    "nibble_of_nat (nat_of_char c div 16) = (case c of Char x y \<Rightarrow> x)"
   1.215    by (cases c)
   1.216 -    (simp add: nat_of_char_def add.commute nat_of_nibble_less_16)
   1.217 +    (simp add: nat_of_char_Char add.commute nat_of_nibble_less_16)
   1.218  
   1.219  lemma nibble_of_nat_nat_of_char:
   1.220    "nibble_of_nat (nat_of_char c) = (case c of Char x y \<Rightarrow> y)"
   1.221 @@ -278,80 +429,19 @@
   1.222      by (simp add: nibble_of_nat_mod_16)
   1.223    then have "nibble_of_nat (nat_of_nibble y + nat_of_nibble x * 16) = y"
   1.224      by (simp only: nibble_of_nat_mod_16)
   1.225 -  with Char show ?thesis by (simp add: nat_of_char_def add.commute)
   1.226 +  with Char show ?thesis by (simp add: nat_of_char_Char add.commute)
   1.227  qed
   1.228  
   1.229  code_datatype Char \<comment> \<open>drop case certificate for char\<close>
   1.230  
   1.231  lemma case_char_code [code]:
   1.232 -  "case_char f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
   1.233 +  "char f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
   1.234    by (cases c)
   1.235      (simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.case)
   1.236  
   1.237 -lemma [code]:
   1.238 -  "rec_char = case_char"
   1.239 -  by (simp add: fun_eq_iff split: char.split)
   1.240 -
   1.241 -definition char_of_nat :: "nat \<Rightarrow> char" where
   1.242 +lemma char_of_nat_enum [code]:
   1.243    "char_of_nat n = Enum.enum ! (n mod 256)"
   1.244 -
   1.245 -lemma char_of_nat_Char_nibbles:
   1.246 -  "char_of_nat n = Char (nibble_of_nat (n div 16)) (nibble_of_nat n)"
   1.247 -proof -
   1.248 -  from mod_mult2_eq [of n 16 16]
   1.249 -  have "n mod 256 = 16 * (n div 16 mod 16) + n mod 16" by simp
   1.250 -  then show ?thesis
   1.251 -    by (simp add: char_of_nat_def enum_char_product_enum_nibble card_UNIV_nibble
   1.252 -      card_UNIV_length_enum [symmetric] nibble_of_nat_def product_nth add.commute)
   1.253 -qed
   1.254 -
   1.255 -lemma char_of_nat_of_char [simp]:
   1.256 -  "char_of_nat (nat_of_char c) = c"
   1.257 -  by (cases c)
   1.258 -    (simp add: char_of_nat_Char_nibbles nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char)
   1.259 -
   1.260 -lemma nat_of_char_of_nat [simp]:
   1.261 -  "nat_of_char (char_of_nat n) = n mod 256"
   1.262 -proof -
   1.263 -  have "n mod 256 = n mod (16 * 16)" by simp
   1.264 -  then have "n div 16 mod 16 * 16 + n mod 16 = n mod 256" by (simp only: mod_mult2_eq)
   1.265 -  then show ?thesis
   1.266 -    by (cases "char_of_nat n") (auto simp add: nat_of_char_def char_of_nat_Char_nibbles)
   1.267 -qed
   1.268 -
   1.269 -lemma char_of_nat_nibble_pair [simp]:
   1.270 -  "char_of_nat (nat_of_nibble a * 16 + nat_of_nibble b) = Char a b"
   1.271 -  by (simp add: nat_of_char_Char [symmetric])
   1.272 -
   1.273 -lemma inj_nat_of_char:
   1.274 -  "inj nat_of_char"
   1.275 -  by (rule inj_on_inverseI) (rule char_of_nat_of_char)
   1.276 -
   1.277 -lemma nat_of_char_eq_iff:
   1.278 -  "nat_of_char c = nat_of_char d \<longleftrightarrow> c = d"
   1.279 -  by (rule inj_eq) (rule inj_nat_of_char)
   1.280 -
   1.281 -lemma nat_of_char_less_256:
   1.282 -  "nat_of_char c < 256"
   1.283 -proof (cases c)
   1.284 -  case (Char x y)
   1.285 -  with nat_of_nibble_less_16 [of x] nat_of_nibble_less_16 [of y]
   1.286 -  show ?thesis by (simp add: nat_of_char_def)
   1.287 -qed
   1.288 -
   1.289 -lemma char_of_nat_mod_256:
   1.290 -  "char_of_nat (n mod 256) = char_of_nat n"
   1.291 -proof -
   1.292 -  from nibble_of_nat_mod_16 [of "n mod 256"]
   1.293 -  have "nibble_of_nat (n mod 256) = nibble_of_nat (n mod 256 mod 16)" by simp
   1.294 -  with nibble_of_nat_mod_16 [of n]
   1.295 -  have *: "nibble_of_nat (n mod 256) = nibble_of_nat n" by (simp add: mod_mod_cancel)
   1.296 -  have "n mod 256 = n mod (16 * 16)" by simp
   1.297 -  then have **: "n mod 256 = n div 16 mod 16 * 16 + n mod 16" by (simp only: mod_mult2_eq)
   1.298 -  show ?thesis
   1.299 -    by (simp add: char_of_nat_Char_nibbles *)
   1.300 -     (simp add: div_add1_eq nibble_of_nat_mod_16 [of "n div 16"] **)
   1.301 -qed
   1.302 +  by (simp add: enum_char_unfold)
   1.303  
   1.304  
   1.305  subsection \<open>Strings as dedicated type\<close>