more direct bootstrap of char type, still retaining the nibble representation for syntax
authorhaftmann
Thu Feb 18 17:52:52 2016 +0100 (2016-02-18)
changeset 623649209770bdcdf
parent 62363 7b5468422352
child 62365 8a105c235b1f
more direct bootstrap of char type, still retaining the nibble representation for syntax
src/HOL/Library/Code_Char.thy
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/String.thy
     1.1 --- a/src/HOL/Library/Code_Char.thy	Fri Feb 19 15:01:38 2016 +0100
     1.2 +++ b/src/HOL/Library/Code_Char.thy	Thu Feb 18 17:52:52 2016 +0100
     1.3 @@ -78,8 +78,8 @@
     1.4      folded fun_cong[OF integer_of_char_def, unfolded o_apply]]
     1.5  
     1.6  lemma char_of_integer_code [code]:
     1.7 -  "char_of_integer n = enum_class.enum ! (nat_of_integer n mod 256)"
     1.8 -by(simp add: char_of_integer_def char_of_nat_def)
     1.9 +  "char_of_integer n = Enum.enum ! (nat_of_integer n mod 256)"
    1.10 +  by (simp add: char_of_integer_def enum_char_unfold)
    1.11  
    1.12  code_printing
    1.13    constant integer_of_char \<rightharpoonup>
    1.14 @@ -121,4 +121,3 @@
    1.15      and (Eval) infixl 6 "<"
    1.16  
    1.17  end
    1.18 -
     2.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Feb 19 15:01:38 2016 +0100
     2.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Thu Feb 18 17:52:52 2016 +0100
     2.3 @@ -630,8 +630,12 @@
     2.4         (Code_Evaluation.term_of (\<lambda>x y. char_of_nat (nat_of_nibble x * 16 + nat_of_nibble y))) (t1 ())) (t2 ()))))"
     2.5    by (simp add: check_all_char_def)
     2.6  
     2.7 -lemma full_exhaustive_char_code [code]:
     2.8 -  "full_exhaustive_class.full_exhaustive f i =
     2.9 +instantiation char :: full_exhaustive
    2.10 +begin
    2.11 +
    2.12 +definition full_exhaustive_char
    2.13 +where
    2.14 +  "full_exhaustive f i =
    2.15       (if 0 < i then full_exhaustive_class.full_exhaustive
    2.16         (\<lambda>(a, b). full_exhaustive_class.full_exhaustive
    2.17            (\<lambda>(c, d).
    2.18 @@ -641,7 +645,10 @@
    2.19                     (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
    2.20                        (b ())) (d ()))) (i - 1)) (i - 1)
    2.21      else None)"
    2.22 -  by (simp add: typerep_fun_def typerep_char_def typerep_nibble_def String.char.full_exhaustive_char.simps)
    2.23 +
    2.24 +instance ..
    2.25 +
    2.26 +end
    2.27  
    2.28  hide_fact (open) orelse_def
    2.29  no_notation orelse (infixr "orelse" 55)
     3.1 --- a/src/HOL/String.thy	Fri Feb 19 15:01:38 2016 +0100
     3.2 +++ b/src/HOL/String.thy	Thu Feb 18 17:52:52 2016 +0100
     3.3 @@ -6,8 +6,92 @@
     3.4  imports Enum
     3.5  begin
     3.6  
     3.7 +lemma upt_conv_Cons_Cons: -- \<open>no precondition\<close> -- \<open>FIXME move\<close>
     3.8 +  "m # n # ns = [m..<q] \<longleftrightarrow> n # ns = [Suc m..<q]"
     3.9 +proof (cases "m < q")
    3.10 +  case False then show ?thesis by simp
    3.11 +next
    3.12 +  case True then show ?thesis by (simp add: upt_conv_Cons)
    3.13 +qed
    3.14 +
    3.15 +
    3.16  subsection \<open>Characters and strings\<close>
    3.17  
    3.18 +subsubsection \<open>Characters as finite algebraic type\<close>
    3.19 +
    3.20 +typedef char = "{n::nat. n < 256}"
    3.21 +  morphisms nat_of_char Abs_char
    3.22 +proof
    3.23 +  show "Suc 0 \<in> {n. n < 256}" by simp
    3.24 +qed
    3.25 +
    3.26 +definition char_of_nat :: "nat \<Rightarrow> char"
    3.27 +where
    3.28 +  "char_of_nat n = Abs_char (n mod 256)"
    3.29 +
    3.30 +lemma char_cases [case_names char_of_nat, cases type: char]:
    3.31 +  "(\<And>n. c = char_of_nat n \<Longrightarrow> n < 256 \<Longrightarrow> P) \<Longrightarrow> P"
    3.32 +  by (cases c) (simp add: char_of_nat_def)
    3.33 +
    3.34 +lemma char_of_nat_of_char [simp]:
    3.35 +  "char_of_nat (nat_of_char c) = c"
    3.36 +  by (cases c) (simp add: char_of_nat_def Abs_char_inject Abs_char_inverse)
    3.37 +
    3.38 +lemma inj_nat_of_char:
    3.39 +  "inj nat_of_char"
    3.40 +proof (rule injI)
    3.41 +  fix c d
    3.42 +  assume "nat_of_char c = nat_of_char d"
    3.43 +  then have "char_of_nat (nat_of_char c) = char_of_nat (nat_of_char d)"
    3.44 +    by simp
    3.45 +  then show "c = d"
    3.46 +    by simp
    3.47 +qed
    3.48 +  
    3.49 +lemma nat_of_char_eq_iff [simp]:
    3.50 +  "nat_of_char c = nat_of_char d \<longleftrightarrow> c = d"
    3.51 +  by (fact nat_of_char_inject)
    3.52 +
    3.53 +lemma nat_of_char_of_nat [simp]:
    3.54 +  "nat_of_char (char_of_nat n) = n mod 256"
    3.55 +  by (cases "char_of_nat n") (simp add: char_of_nat_def Abs_char_inject Abs_char_inverse)
    3.56 +
    3.57 +lemma char_of_nat_mod_256 [simp]:
    3.58 +  "char_of_nat (n mod 256) = char_of_nat n"
    3.59 +  by (cases "char_of_nat (n mod 256)") (simp add: char_of_nat_def)
    3.60 +
    3.61 +lemma char_of_nat_quasi_inj [simp]:
    3.62 +  "char_of_nat m = char_of_nat n \<longleftrightarrow> m mod 256 = n mod 256"
    3.63 +  by (simp add: char_of_nat_def Abs_char_inject)
    3.64 +
    3.65 +lemma inj_on_char_of_nat [simp]:
    3.66 +  "inj_on char_of_nat {0..<256}"
    3.67 +  by (rule inj_onI) simp
    3.68 +
    3.69 +lemma nat_of_char_mod_256 [simp]:
    3.70 +  "nat_of_char c mod 256 = nat_of_char c"
    3.71 +  by (cases c) simp
    3.72 +
    3.73 +lemma nat_of_char_less_256 [simp]:
    3.74 +  "nat_of_char c < 256"
    3.75 +proof -
    3.76 +  have "nat_of_char c mod 256 < 256"
    3.77 +    by arith
    3.78 +  then show ?thesis by simp
    3.79 +qed
    3.80 +
    3.81 +lemma UNIV_char_of_nat:
    3.82 +  "UNIV = char_of_nat ` {0..<256}"
    3.83 +proof -
    3.84 +  { fix c
    3.85 +    have "c \<in> char_of_nat ` {0..<256}"
    3.86 +      by (cases c) auto
    3.87 +  } then show ?thesis by auto
    3.88 +qed
    3.89 +
    3.90 +
    3.91 +subsubsection \<open>Traditional concrete representation of characters\<close>
    3.92 +
    3.93  datatype (plugins del: transfer) nibble =
    3.94      Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
    3.95    | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
    3.96 @@ -114,9 +198,78 @@
    3.97    "nibble_of_nat (n mod 16) = nibble_of_nat n"
    3.98    by (simp add: nibble_of_nat_def)
    3.99  
   3.100 -datatype char = Char nibble nibble
   3.101 +context
   3.102 +begin
   3.103 +
   3.104 +local_setup \<open>Local_Theory.map_background_naming (Name_Space.add_path "char")\<close>
   3.105 +
   3.106 +definition Char :: "nibble \<Rightarrow> nibble \<Rightarrow> char"
   3.107 +where
   3.108 +  "Char x y = char_of_nat (nat_of_nibble x * 16 + nat_of_nibble y)"
   3.109    \<comment> "Note: canonical order of character encoding coincides with standard term ordering"
   3.110  
   3.111 +end
   3.112 +
   3.113 +lemma nat_of_char_Char:
   3.114 +  "nat_of_char (Char x y) = nat_of_nibble x * 16 + nat_of_nibble y" (is "_ = ?rhs")
   3.115 +proof -
   3.116 +  have "?rhs < 256"
   3.117 +    using nat_of_nibble_less_16 [of x] nat_of_nibble_less_16 [of y]
   3.118 +    by arith
   3.119 +  then show ?thesis by (simp add: Char_def)
   3.120 +qed
   3.121 +
   3.122 +lemma char_of_nat_Char_nibbles:
   3.123 +  "char_of_nat n = Char (nibble_of_nat (n div 16)) (nibble_of_nat n)"
   3.124 +proof -
   3.125 +  from mod_mult2_eq [of n 16 16]
   3.126 +  have "n mod 256 = 16 * (n div 16 mod 16) + n mod 16" by simp
   3.127 +  then show ?thesis
   3.128 +    by (simp add: Char_def)
   3.129 +qed
   3.130 +
   3.131 +lemma char_of_nat_nibble_pair [simp]:
   3.132 +  "char_of_nat (nat_of_nibble a * 16 + nat_of_nibble b) = Char a b"
   3.133 +  by (simp add: nat_of_char_Char [symmetric])
   3.134 +
   3.135 +free_constructors char for Char
   3.136 +proof -
   3.137 +  fix P c
   3.138 +  assume hyp: "\<And>x y. c = Char x y \<Longrightarrow> P"
   3.139 +  have "nat_of_char c \<le> 255"
   3.140 +    using nat_of_char_less_256 [of c] by arith
   3.141 +  then have "nat_of_char c div 16 \<le> 255 div 16"
   3.142 +    by (auto intro: div_le_mono2)
   3.143 +  then have "nat_of_char c div 16 < 16"
   3.144 +    by auto
   3.145 +  then have "nat_of_char c div 16 mod 16 = nat_of_char c div 16"
   3.146 +    by simp
   3.147 +  then have "c = Char (nibble_of_nat (nat_of_char c div 16))
   3.148 +    (nibble_of_nat (nat_of_char c mod 16))"
   3.149 +    by (simp add: Char_def)
   3.150 +  then show P by (rule hyp)
   3.151 +next
   3.152 +  fix x y z w
   3.153 +  have "Char x y = Char z w
   3.154 +    \<longleftrightarrow> nat_of_char (Char x y) = nat_of_char (Char z w)"
   3.155 +    by auto
   3.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")
   3.157 +  proof
   3.158 +    assume "?Q \<and> ?R"
   3.159 +    then show ?P by (simp add: nat_of_char_Char)
   3.160 +  next
   3.161 +    assume ?P
   3.162 +    then have ?Q
   3.163 +      using nat_of_nibble_less_16 [of y] nat_of_nibble_less_16 [of w]
   3.164 +      by (simp add: nat_of_char_Char)
   3.165 +    moreover with \<open>?P\<close> have ?R by (simp add: nat_of_char_Char)
   3.166 +    ultimately show "?Q \<and> ?R" ..
   3.167 +  qed
   3.168 +  also have "\<dots> \<longleftrightarrow> x = z \<and> y = w"
   3.169 +    by (simp add: nat_of_nibble_eq_iff)
   3.170 +  finally show "Char x y = Char z w \<longleftrightarrow> x = z \<and> y = w" .
   3.171 +qed
   3.172 +
   3.173  syntax
   3.174    "_Char" :: "str_position => char"    ("CHR _")
   3.175  
   3.176 @@ -133,11 +286,6 @@
   3.177    fix x show "x \<in> image (case_prod Char) (UNIV \<times> UNIV)" by (cases x) auto
   3.178  qed
   3.179  
   3.180 -lemma size_char [code, simp]:
   3.181 -  "size_char (c::char) = 0"
   3.182 -  "size (c::char) = 0"
   3.183 -  by (cases c, simp)+
   3.184 -
   3.185  instantiation char :: enum
   3.186  begin
   3.187  
   3.188 @@ -238,13 +386,16 @@
   3.189    "card (UNIV :: char set) = 256"
   3.190    by (simp add: card_UNIV_length_enum enum_char_def)
   3.191  
   3.192 -definition nat_of_char :: "char \<Rightarrow> nat"
   3.193 -where
   3.194 -  "nat_of_char c = (case c of Char x y \<Rightarrow> nat_of_nibble x * 16 + nat_of_nibble y)"
   3.195 -
   3.196 -lemma nat_of_char_Char:
   3.197 -  "nat_of_char (Char x y) = nat_of_nibble x * 16 + nat_of_nibble y"
   3.198 -  by (simp add: nat_of_char_def)
   3.199 +lemma enum_char_unfold:
   3.200 +  "Enum.enum = map char_of_nat [0..<256]"
   3.201 +proof -
   3.202 +  have *: "Suc (Suc 0) = 2" by simp
   3.203 +  have "map nat_of_char Enum.enum = [0..<256]"
   3.204 +    by (simp add: enum_char_def nat_of_char_Char upt_conv_Cons_Cons *)
   3.205 +  then have "map char_of_nat (map nat_of_char Enum.enum) =
   3.206 +    map char_of_nat [0..<256]" by simp
   3.207 +  then show ?thesis by (simp add: comp_def)
   3.208 +qed
   3.209  
   3.210  setup \<open>
   3.211  let
   3.212 @@ -268,7 +419,7 @@
   3.213  lemma nibble_of_nat_of_char_div_16:
   3.214    "nibble_of_nat (nat_of_char c div 16) = (case c of Char x y \<Rightarrow> x)"
   3.215    by (cases c)
   3.216 -    (simp add: nat_of_char_def add.commute nat_of_nibble_less_16)
   3.217 +    (simp add: nat_of_char_Char add.commute nat_of_nibble_less_16)
   3.218  
   3.219  lemma nibble_of_nat_nat_of_char:
   3.220    "nibble_of_nat (nat_of_char c) = (case c of Char x y \<Rightarrow> y)"
   3.221 @@ -278,80 +429,19 @@
   3.222      by (simp add: nibble_of_nat_mod_16)
   3.223    then have "nibble_of_nat (nat_of_nibble y + nat_of_nibble x * 16) = y"
   3.224      by (simp only: nibble_of_nat_mod_16)
   3.225 -  with Char show ?thesis by (simp add: nat_of_char_def add.commute)
   3.226 +  with Char show ?thesis by (simp add: nat_of_char_Char add.commute)
   3.227  qed
   3.228  
   3.229  code_datatype Char \<comment> \<open>drop case certificate for char\<close>
   3.230  
   3.231  lemma case_char_code [code]:
   3.232 -  "case_char f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
   3.233 +  "char f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
   3.234    by (cases c)
   3.235      (simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.case)
   3.236  
   3.237 -lemma [code]:
   3.238 -  "rec_char = case_char"
   3.239 -  by (simp add: fun_eq_iff split: char.split)
   3.240 -
   3.241 -definition char_of_nat :: "nat \<Rightarrow> char" where
   3.242 +lemma char_of_nat_enum [code]:
   3.243    "char_of_nat n = Enum.enum ! (n mod 256)"
   3.244 -
   3.245 -lemma char_of_nat_Char_nibbles:
   3.246 -  "char_of_nat n = Char (nibble_of_nat (n div 16)) (nibble_of_nat n)"
   3.247 -proof -
   3.248 -  from mod_mult2_eq [of n 16 16]
   3.249 -  have "n mod 256 = 16 * (n div 16 mod 16) + n mod 16" by simp
   3.250 -  then show ?thesis
   3.251 -    by (simp add: char_of_nat_def enum_char_product_enum_nibble card_UNIV_nibble
   3.252 -      card_UNIV_length_enum [symmetric] nibble_of_nat_def product_nth add.commute)
   3.253 -qed
   3.254 -
   3.255 -lemma char_of_nat_of_char [simp]:
   3.256 -  "char_of_nat (nat_of_char c) = c"
   3.257 -  by (cases c)
   3.258 -    (simp add: char_of_nat_Char_nibbles nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char)
   3.259 -
   3.260 -lemma nat_of_char_of_nat [simp]:
   3.261 -  "nat_of_char (char_of_nat n) = n mod 256"
   3.262 -proof -
   3.263 -  have "n mod 256 = n mod (16 * 16)" by simp
   3.264 -  then have "n div 16 mod 16 * 16 + n mod 16 = n mod 256" by (simp only: mod_mult2_eq)
   3.265 -  then show ?thesis
   3.266 -    by (cases "char_of_nat n") (auto simp add: nat_of_char_def char_of_nat_Char_nibbles)
   3.267 -qed
   3.268 -
   3.269 -lemma char_of_nat_nibble_pair [simp]:
   3.270 -  "char_of_nat (nat_of_nibble a * 16 + nat_of_nibble b) = Char a b"
   3.271 -  by (simp add: nat_of_char_Char [symmetric])
   3.272 -
   3.273 -lemma inj_nat_of_char:
   3.274 -  "inj nat_of_char"
   3.275 -  by (rule inj_on_inverseI) (rule char_of_nat_of_char)
   3.276 -
   3.277 -lemma nat_of_char_eq_iff:
   3.278 -  "nat_of_char c = nat_of_char d \<longleftrightarrow> c = d"
   3.279 -  by (rule inj_eq) (rule inj_nat_of_char)
   3.280 -
   3.281 -lemma nat_of_char_less_256:
   3.282 -  "nat_of_char c < 256"
   3.283 -proof (cases c)
   3.284 -  case (Char x y)
   3.285 -  with nat_of_nibble_less_16 [of x] nat_of_nibble_less_16 [of y]
   3.286 -  show ?thesis by (simp add: nat_of_char_def)
   3.287 -qed
   3.288 -
   3.289 -lemma char_of_nat_mod_256:
   3.290 -  "char_of_nat (n mod 256) = char_of_nat n"
   3.291 -proof -
   3.292 -  from nibble_of_nat_mod_16 [of "n mod 256"]
   3.293 -  have "nibble_of_nat (n mod 256) = nibble_of_nat (n mod 256 mod 16)" by simp
   3.294 -  with nibble_of_nat_mod_16 [of n]
   3.295 -  have *: "nibble_of_nat (n mod 256) = nibble_of_nat n" by (simp add: mod_mod_cancel)
   3.296 -  have "n mod 256 = n mod (16 * 16)" by simp
   3.297 -  then have **: "n mod 256 = n div 16 mod 16 * 16 + n mod 16" by (simp only: mod_mult2_eq)
   3.298 -  show ?thesis
   3.299 -    by (simp add: char_of_nat_Char_nibbles *)
   3.300 -     (simp add: div_add1_eq nibble_of_nat_mod_16 [of "n div 16"] **)
   3.301 -qed
   3.302 +  by (simp add: enum_char_unfold)
   3.303  
   3.304  
   3.305  subsection \<open>Strings as dedicated type\<close>