haftmann@31051: (* Author: Tobias Nipkow, Florian Haftmann, TU Muenchen *)
haftmann@31051: 
haftmann@31051: header {* Character and string types *}
haftmann@31051: 
haftmann@31051: theory String
haftmann@49972: imports List Enum
haftmann@31051: begin
haftmann@31051: 
haftmann@49972: subsection {* Characters and strings *}
haftmann@31051: 
haftmann@31051: datatype nibble =
haftmann@31051:     Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
haftmann@31051:   | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
haftmann@31051: 
haftmann@31051: lemma UNIV_nibble:
haftmann@31051:   "UNIV = {Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
haftmann@31051:     Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF}" (is "_ = ?A")
haftmann@31051: proof (rule UNIV_eq_I)
haftmann@31051:   fix x show "x \<in> ?A" by (cases x) simp_all
haftmann@31051: qed
haftmann@31051: 
haftmann@49972: lemma size_nibble [code, simp]:
haftmann@49972:   "size (x::nibble) = 0" by (cases x) simp_all
haftmann@49972: 
haftmann@49972: lemma nibble_size [code, simp]:
haftmann@49972:   "nibble_size (x::nibble) = 0" by (cases x) simp_all
haftmann@49972: 
haftmann@49972: instantiation nibble :: enum
haftmann@49972: begin
haftmann@49972: 
haftmann@49972: definition
haftmann@49972:   "Enum.enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
haftmann@49972:     Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
haftmann@49972: 
haftmann@49972: definition
haftmann@49972:   "Enum.enum_all P \<longleftrightarrow> P Nibble0 \<and> P Nibble1 \<and> P Nibble2 \<and> P Nibble3 \<and> P Nibble4 \<and> P Nibble5 \<and> P Nibble6 \<and> P Nibble7
haftmann@49972:      \<and> P Nibble8 \<and> P Nibble9 \<and> P NibbleA \<and> P NibbleB \<and> P NibbleC \<and> P NibbleD \<and> P NibbleE \<and> P NibbleF"
haftmann@49972: 
haftmann@49972: definition
haftmann@49972:   "Enum.enum_ex P \<longleftrightarrow> P Nibble0 \<or> P Nibble1 \<or> P Nibble2 \<or> P Nibble3 \<or> P Nibble4 \<or> P Nibble5 \<or> P Nibble6 \<or> P Nibble7
haftmann@49972:      \<or> P Nibble8 \<or> P Nibble9 \<or> P NibbleA \<or> P NibbleB \<or> P NibbleC \<or> P NibbleD \<or> P NibbleE \<or> P NibbleF"
haftmann@49972: 
haftmann@49972: instance proof
haftmann@49972: qed (simp_all only: enum_nibble_def enum_all_nibble_def enum_ex_nibble_def UNIV_nibble, simp_all)
haftmann@49972: 
haftmann@49972: end
haftmann@49972: 
haftmann@49972: lemma card_UNIV_nibble:
haftmann@49972:   "card (UNIV :: nibble set) = 16"
haftmann@49972:   by (simp add: card_UNIV_length_enum enum_nibble_def)
haftmann@31051: 
haftmann@51160: primrec nat_of_nibble :: "nibble \<Rightarrow> nat"
haftmann@51160: where
haftmann@51160:   "nat_of_nibble Nibble0 = 0"
haftmann@51160: | "nat_of_nibble Nibble1 = 1"
haftmann@51160: | "nat_of_nibble Nibble2 = 2"
haftmann@51160: | "nat_of_nibble Nibble3 = 3"
haftmann@51160: | "nat_of_nibble Nibble4 = 4"
haftmann@51160: | "nat_of_nibble Nibble5 = 5"
haftmann@51160: | "nat_of_nibble Nibble6 = 6"
haftmann@51160: | "nat_of_nibble Nibble7 = 7"
haftmann@51160: | "nat_of_nibble Nibble8 = 8"
haftmann@51160: | "nat_of_nibble Nibble9 = 9"
haftmann@51160: | "nat_of_nibble NibbleA = 10"
haftmann@51160: | "nat_of_nibble NibbleB = 11"
haftmann@51160: | "nat_of_nibble NibbleC = 12"
haftmann@51160: | "nat_of_nibble NibbleD = 13"
haftmann@51160: | "nat_of_nibble NibbleE = 14"
haftmann@51160: | "nat_of_nibble NibbleF = 15"
haftmann@51160: 
haftmann@51160: definition nibble_of_nat :: "nat \<Rightarrow> nibble" where
haftmann@51160:   "nibble_of_nat n = Enum.enum ! (n mod 16)"
haftmann@51160: 
haftmann@51160: lemma nibble_of_nat_simps [simp]:
haftmann@51160:   "nibble_of_nat  0 = Nibble0"
haftmann@51160:   "nibble_of_nat  1 = Nibble1"
haftmann@51160:   "nibble_of_nat  2 = Nibble2"
haftmann@51160:   "nibble_of_nat  3 = Nibble3"
haftmann@51160:   "nibble_of_nat  4 = Nibble4"
haftmann@51160:   "nibble_of_nat  5 = Nibble5"
haftmann@51160:   "nibble_of_nat  6 = Nibble6"
haftmann@51160:   "nibble_of_nat  7 = Nibble7"
haftmann@51160:   "nibble_of_nat  8 = Nibble8"
haftmann@51160:   "nibble_of_nat  9 = Nibble9"
haftmann@51160:   "nibble_of_nat 10 = NibbleA"
haftmann@51160:   "nibble_of_nat 11 = NibbleB"
haftmann@51160:   "nibble_of_nat 12 = NibbleC"
haftmann@51160:   "nibble_of_nat 13 = NibbleD"
haftmann@51160:   "nibble_of_nat 14 = NibbleE"
haftmann@51160:   "nibble_of_nat 15 = NibbleF"
haftmann@51160:   unfolding nibble_of_nat_def by (simp_all add: enum_nibble_def)
haftmann@51160: 
haftmann@51160: lemma nibble_of_nat_of_nibble [simp]:
haftmann@51160:   "nibble_of_nat (nat_of_nibble x) = x"
haftmann@51160:   by (cases x) (simp_all add: nibble_of_nat_def enum_nibble_def)
haftmann@51160: 
haftmann@51160: lemma nat_of_nibble_of_nat [simp]:
haftmann@51160:   "nat_of_nibble (nibble_of_nat n) = n mod 16"
haftmann@51160:   by (cases "nibble_of_nat n")
haftmann@51160:      (simp_all add: nibble_of_nat_def enum_nibble_def nth_equal_first_eq nth_non_equal_first_eq, arith)
haftmann@51160: 
haftmann@51160: lemma inj_nat_of_nibble:
haftmann@51160:   "inj nat_of_nibble"
haftmann@51160:   by (rule inj_on_inverseI) (rule nibble_of_nat_of_nibble)
haftmann@51160: 
haftmann@51160: lemma nat_of_nibble_eq_iff:
haftmann@51160:   "nat_of_nibble x = nat_of_nibble y \<longleftrightarrow> x = y"
haftmann@51160:   by (rule inj_eq) (rule inj_nat_of_nibble)
haftmann@51160: 
haftmann@51160: lemma nat_of_nibble_less_16:
haftmann@51160:   "nat_of_nibble x < 16"
haftmann@51160:   by (cases x) auto
haftmann@51160: 
haftmann@51160: lemma nibble_of_nat_mod_16:
haftmann@51160:   "nibble_of_nat (n mod 16) = nibble_of_nat n"
haftmann@51160:   by (simp add: nibble_of_nat_def)
haftmann@51160: 
haftmann@31051: datatype char = Char nibble nibble
haftmann@31051:   -- "Note: canonical order of character encoding coincides with standard term ordering"
haftmann@31051: 
haftmann@31051: syntax
wenzelm@46483:   "_Char" :: "str_position => char"    ("CHR _")
haftmann@31051: 
bulwahn@42163: type_synonym string = "char list"
haftmann@31051: 
haftmann@31051: syntax
wenzelm@46483:   "_String" :: "str_position => string"    ("_")
haftmann@31051: 
wenzelm@48891: ML_file "Tools/string_syntax.ML"
wenzelm@35123: setup String_Syntax.setup
haftmann@31051: 
haftmann@49972: lemma UNIV_char:
haftmann@49972:   "UNIV = image (split Char) (UNIV \<times> UNIV)"
haftmann@49972: proof (rule UNIV_eq_I)
haftmann@49972:   fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
haftmann@49972: qed
haftmann@49972: 
haftmann@49972: lemma size_char [code, simp]:
haftmann@49972:   "size (c::char) = 0" by (cases c) simp
haftmann@49972: 
haftmann@49972: lemma char_size [code, simp]:
haftmann@49972:   "char_size (c::char) = 0" by (cases c) simp
haftmann@49972: 
haftmann@49972: instantiation char :: enum
haftmann@49972: begin
haftmann@49972: 
haftmann@49972: definition
haftmann@49972:   "Enum.enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
haftmann@31484:   Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
haftmann@31484:   Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,
haftmann@31484:   Char Nibble0 Nibble9, Char Nibble0 NibbleA, Char Nibble0 NibbleB,
haftmann@31484:   Char Nibble0 NibbleC, Char Nibble0 NibbleD, Char Nibble0 NibbleE,
haftmann@31484:   Char Nibble0 NibbleF, Char Nibble1 Nibble0, Char Nibble1 Nibble1,
haftmann@31484:   Char Nibble1 Nibble2, Char Nibble1 Nibble3, Char Nibble1 Nibble4,
haftmann@31484:   Char Nibble1 Nibble5, Char Nibble1 Nibble6, Char Nibble1 Nibble7,
haftmann@31484:   Char Nibble1 Nibble8, Char Nibble1 Nibble9, Char Nibble1 NibbleA,
haftmann@31484:   Char Nibble1 NibbleB, Char Nibble1 NibbleC, Char Nibble1 NibbleD,
haftmann@31484:   Char Nibble1 NibbleE, Char Nibble1 NibbleF, CHR '' '', CHR ''!'',
haftmann@31484:   Char Nibble2 Nibble2, CHR ''#'', CHR ''$'', CHR ''%'', CHR ''&'',
haftmann@31484:   Char Nibble2 Nibble7, CHR ''('', CHR '')'', CHR ''*'', CHR ''+'', CHR '','',
haftmann@31484:   CHR ''-'', CHR ''.'', CHR ''/'', CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
haftmann@31484:   CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9'', CHR '':'',
haftmann@31484:   CHR '';'', CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'', CHR ''@'', CHR ''A'',
haftmann@31484:   CHR ''B'', CHR ''C'', CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'', CHR ''H'',
haftmann@31484:   CHR ''I'', CHR ''J'', CHR ''K'', CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
haftmann@31484:   CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'', CHR ''T'', CHR ''U'', CHR ''V'',
haftmann@31484:   CHR ''W'', CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['', Char Nibble5 NibbleC,
haftmann@31484:   CHR '']'', CHR ''^'', CHR ''_'', Char Nibble6 Nibble0, CHR ''a'', CHR ''b'',
haftmann@31484:   CHR ''c'', CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'', CHR ''h'', CHR ''i'',
haftmann@31484:   CHR ''j'', CHR ''k'', CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'', CHR ''p'',
haftmann@31484:   CHR ''q'', CHR ''r'', CHR ''s'', CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
haftmann@31484:   CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'', CHR ''|'', CHR ''}'', CHR ''~'',
haftmann@31484:   Char Nibble7 NibbleF, Char Nibble8 Nibble0, Char Nibble8 Nibble1,
haftmann@31484:   Char Nibble8 Nibble2, Char Nibble8 Nibble3, Char Nibble8 Nibble4,
haftmann@31484:   Char Nibble8 Nibble5, Char Nibble8 Nibble6, Char Nibble8 Nibble7,
haftmann@31484:   Char Nibble8 Nibble8, Char Nibble8 Nibble9, Char Nibble8 NibbleA,
haftmann@31484:   Char Nibble8 NibbleB, Char Nibble8 NibbleC, Char Nibble8 NibbleD,
haftmann@31484:   Char Nibble8 NibbleE, Char Nibble8 NibbleF, Char Nibble9 Nibble0,
haftmann@31484:   Char Nibble9 Nibble1, Char Nibble9 Nibble2, Char Nibble9 Nibble3,
haftmann@31484:   Char Nibble9 Nibble4, Char Nibble9 Nibble5, Char Nibble9 Nibble6,
haftmann@31484:   Char Nibble9 Nibble7, Char Nibble9 Nibble8, Char Nibble9 Nibble9,
haftmann@31484:   Char Nibble9 NibbleA, Char Nibble9 NibbleB, Char Nibble9 NibbleC,
haftmann@31484:   Char Nibble9 NibbleD, Char Nibble9 NibbleE, Char Nibble9 NibbleF,
haftmann@31484:   Char NibbleA Nibble0, Char NibbleA Nibble1, Char NibbleA Nibble2,
haftmann@31484:   Char NibbleA Nibble3, Char NibbleA Nibble4, Char NibbleA Nibble5,
haftmann@31484:   Char NibbleA Nibble6, Char NibbleA Nibble7, Char NibbleA Nibble8,
haftmann@31484:   Char NibbleA Nibble9, Char NibbleA NibbleA, Char NibbleA NibbleB,
haftmann@31484:   Char NibbleA NibbleC, Char NibbleA NibbleD, Char NibbleA NibbleE,
haftmann@31484:   Char NibbleA NibbleF, Char NibbleB Nibble0, Char NibbleB Nibble1,
haftmann@31484:   Char NibbleB Nibble2, Char NibbleB Nibble3, Char NibbleB Nibble4,
haftmann@31484:   Char NibbleB Nibble5, Char NibbleB Nibble6, Char NibbleB Nibble7,
haftmann@31484:   Char NibbleB Nibble8, Char NibbleB Nibble9, Char NibbleB NibbleA,
haftmann@31484:   Char NibbleB NibbleB, Char NibbleB NibbleC, Char NibbleB NibbleD,
haftmann@31484:   Char NibbleB NibbleE, Char NibbleB NibbleF, Char NibbleC Nibble0,
haftmann@31484:   Char NibbleC Nibble1, Char NibbleC Nibble2, Char NibbleC Nibble3,
haftmann@31484:   Char NibbleC Nibble4, Char NibbleC Nibble5, Char NibbleC Nibble6,
haftmann@31484:   Char NibbleC Nibble7, Char NibbleC Nibble8, Char NibbleC Nibble9,
haftmann@31484:   Char NibbleC NibbleA, Char NibbleC NibbleB, Char NibbleC NibbleC,
haftmann@31484:   Char NibbleC NibbleD, Char NibbleC NibbleE, Char NibbleC NibbleF,
haftmann@31484:   Char NibbleD Nibble0, Char NibbleD Nibble1, Char NibbleD Nibble2,
haftmann@31484:   Char NibbleD Nibble3, Char NibbleD Nibble4, Char NibbleD Nibble5,
haftmann@31484:   Char NibbleD Nibble6, Char NibbleD Nibble7, Char NibbleD Nibble8,
haftmann@31484:   Char NibbleD Nibble9, Char NibbleD NibbleA, Char NibbleD NibbleB,
haftmann@31484:   Char NibbleD NibbleC, Char NibbleD NibbleD, Char NibbleD NibbleE,
haftmann@31484:   Char NibbleD NibbleF, Char NibbleE Nibble0, Char NibbleE Nibble1,
haftmann@31484:   Char NibbleE Nibble2, Char NibbleE Nibble3, Char NibbleE Nibble4,
haftmann@31484:   Char NibbleE Nibble5, Char NibbleE Nibble6, Char NibbleE Nibble7,
haftmann@31484:   Char NibbleE Nibble8, Char NibbleE Nibble9, Char NibbleE NibbleA,
haftmann@31484:   Char NibbleE NibbleB, Char NibbleE NibbleC, Char NibbleE NibbleD,
haftmann@31484:   Char NibbleE NibbleE, Char NibbleE NibbleF, Char NibbleF Nibble0,
haftmann@31484:   Char NibbleF Nibble1, Char NibbleF Nibble2, Char NibbleF Nibble3,
haftmann@31484:   Char NibbleF Nibble4, Char NibbleF Nibble5, Char NibbleF Nibble6,
haftmann@31484:   Char NibbleF Nibble7, Char NibbleF Nibble8, Char NibbleF Nibble9,
haftmann@31484:   Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC,
haftmann@31484:   Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
haftmann@31484: 
haftmann@49972: definition
haftmann@49972:   "Enum.enum_all P \<longleftrightarrow> list_all P (Enum.enum :: char list)"
haftmann@49972: 
haftmann@49972: definition
haftmann@49972:   "Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
haftmann@49972: 
haftmann@51160: lemma enum_char_product_enum_nibble:
haftmann@51160:   "(Enum.enum :: char list) = map (split Char) (List.product Enum.enum Enum.enum)"
haftmann@51160:   by (simp add: enum_char_def enum_nibble_def)
haftmann@51160: 
haftmann@49972: instance proof
haftmann@49972:   show UNIV: "UNIV = set (Enum.enum :: char list)"
haftmann@51160:     by (simp add: enum_char_product_enum_nibble UNIV_char product_list_set enum_UNIV)
haftmann@49972:   show "distinct (Enum.enum :: char list)"
haftmann@51160:     by (auto intro: inj_onI simp add: enum_char_product_enum_nibble distinct_map distinct_product enum_distinct)
haftmann@49972:   show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P"
haftmann@49972:     by (simp add: UNIV enum_all_char_def list_all_iff)
haftmann@49972:   show "\<And>P. Enum.enum_ex P \<longleftrightarrow> Bex (UNIV :: char set) P"
haftmann@49972:     by (simp add: UNIV enum_ex_char_def list_ex_iff)
haftmann@49972: qed
haftmann@49972: 
haftmann@49972: end
haftmann@49972: 
haftmann@49972: lemma card_UNIV_char:
haftmann@49972:   "card (UNIV :: char set) = 256"
haftmann@49972:   by (simp add: card_UNIV_length_enum enum_char_def)
haftmann@49948: 
haftmann@51160: definition nat_of_char :: "char \<Rightarrow> nat"
haftmann@51160: where
haftmann@51160:   "nat_of_char c = (case c of Char x y \<Rightarrow> nat_of_nibble x * 16 + nat_of_nibble y)"
haftmann@51160: 
haftmann@51160: lemma nat_of_char_Char:
haftmann@51160:   "nat_of_char (Char x y) = nat_of_nibble x * 16 + nat_of_nibble y"
haftmann@51160:   by (simp add: nat_of_char_def)
haftmann@49972: 
haftmann@49972: setup {*
haftmann@49972: let
haftmann@49972:   val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16;
wenzelm@51717:   val simpset =
wenzelm@51717:     put_simpset HOL_ss @{context}
wenzelm@51717:       addsimps @{thms nat_of_nibble.simps mult_0 mult_1 add_0 add_0_right arith_simps numeral_plus_one};
haftmann@51160:   fun mk_code_eqn x y =
haftmann@51160:     Drule.instantiate' [] [SOME x, SOME y] @{thm nat_of_char_Char}
haftmann@51160:     |> simplify simpset;
haftmann@51160:   val code_eqns = map_product mk_code_eqn nibbles nibbles;
haftmann@49972: in
haftmann@49972:   Global_Theory.note_thmss ""
haftmann@51160:     [((@{binding nat_of_char_simps}, []), [(code_eqns, [])])]
haftmann@51160:   #> snd
haftmann@49972: end
haftmann@49972: *}
haftmann@49972: 
haftmann@51160: declare nat_of_char_simps [code]
haftmann@51160: 
haftmann@51160: lemma nibble_of_nat_of_char_div_16:
haftmann@51160:   "nibble_of_nat (nat_of_char c div 16) = (case c of Char x y \<Rightarrow> x)"
haftmann@51160:   by (cases c)
haftmann@51160:     (simp add: nat_of_char_def add_commute nat_of_nibble_less_16)
haftmann@51160: 
haftmann@51160: lemma nibble_of_nat_nat_of_char:
haftmann@51160:   "nibble_of_nat (nat_of_char c) = (case c of Char x y \<Rightarrow> y)"
haftmann@51160: proof (cases c)
haftmann@51160:   case (Char x y)
haftmann@51160:   then have *: "nibble_of_nat ((nat_of_nibble y + nat_of_nibble x * 16) mod 16) = y"
haftmann@51160:     by (simp add: nibble_of_nat_mod_16)
haftmann@51160:   then have "nibble_of_nat (nat_of_nibble y + nat_of_nibble x * 16) = y"
haftmann@51160:     by (simp only: nibble_of_nat_mod_16)
haftmann@51160:   with Char show ?thesis by (simp add: nat_of_char_def add_commute)
haftmann@51160: qed
haftmann@51160: 
haftmann@51160: code_datatype Char -- {* drop case certificate for char *}
haftmann@51160: 
haftmann@51160: lemma char_case_code [code]:
haftmann@51160:   "char_case f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
haftmann@51160:   by (cases c)
haftmann@51160:     (simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.cases)
haftmann@51160: 
haftmann@51160: lemma [code]:
haftmann@51160:   "char_rec = char_case"
haftmann@49972:   by (simp add: fun_eq_iff split: char.split)
haftmann@49972: 
haftmann@51160: definition char_of_nat :: "nat \<Rightarrow> char" where
haftmann@51160:   "char_of_nat n = Enum.enum ! (n mod 256)"
haftmann@51160: 
haftmann@51160: lemma char_of_nat_Char_nibbles:
haftmann@51160:   "char_of_nat n = Char (nibble_of_nat (n div 16)) (nibble_of_nat n)"
haftmann@51160: proof -
haftmann@51160:   from mod_mult2_eq [of n 16 16]
haftmann@51160:   have "n mod 256 = 16 * (n div 16 mod 16) + n mod 16" by simp
haftmann@51160:   then show ?thesis
haftmann@51160:     by (simp add: char_of_nat_def enum_char_product_enum_nibble card_UNIV_nibble
haftmann@51160:       card_UNIV_length_enum [symmetric] nibble_of_nat_def product_nth add_commute)
haftmann@51160: qed
haftmann@51160: 
haftmann@51160: lemma char_of_nat_of_char [simp]:
haftmann@51160:   "char_of_nat (nat_of_char c) = c"
haftmann@51160:   by (cases c)
haftmann@51160:     (simp add: char_of_nat_Char_nibbles nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char)
haftmann@51160: 
haftmann@51160: lemma nat_of_char_of_nat [simp]:
haftmann@51160:   "nat_of_char (char_of_nat n) = n mod 256"
haftmann@51160: proof -
haftmann@51160:   have "n mod 256 = n mod (16 * 16)" by simp
haftmann@51160:   then have "n div 16 mod 16 * 16 + n mod 16 = n mod 256" by (simp only: mod_mult2_eq)
haftmann@51160:   then show ?thesis
haftmann@51160:     by (cases "char_of_nat n") (auto simp add: nat_of_char_def char_of_nat_Char_nibbles)
haftmann@51160: qed
haftmann@51160: 
haftmann@51160: lemma inj_nat_of_char:
haftmann@51160:   "inj nat_of_char"
haftmann@51160:   by (rule inj_on_inverseI) (rule char_of_nat_of_char)
haftmann@51160: 
haftmann@51160: lemma nat_of_char_eq_iff:
haftmann@51160:   "nat_of_char c = nat_of_char d \<longleftrightarrow> c = d"
haftmann@51160:   by (rule inj_eq) (rule inj_nat_of_char)
haftmann@51160: 
haftmann@51160: lemma nat_of_char_less_256:
haftmann@51160:   "nat_of_char c < 256"
haftmann@51160: proof (cases c)
haftmann@51160:   case (Char x y)
haftmann@51160:   with nat_of_nibble_less_16 [of x] nat_of_nibble_less_16 [of y]
haftmann@51160:   show ?thesis by (simp add: nat_of_char_def)
haftmann@51160: qed
haftmann@51160: 
haftmann@51160: lemma char_of_nat_mod_256:
haftmann@51160:   "char_of_nat (n mod 256) = char_of_nat n"
haftmann@51160: proof -
haftmann@51160:   from nibble_of_nat_mod_16 [of "n mod 256"]
haftmann@51160:   have "nibble_of_nat (n mod 256) = nibble_of_nat (n mod 256 mod 16)" by simp
haftmann@51160:   with nibble_of_nat_mod_16 [of n]
haftmann@51160:   have *: "nibble_of_nat (n mod 256) = nibble_of_nat n" by (simp add: mod_mod_cancel)
haftmann@51160:   have "n mod 256 = n mod (16 * 16)" by simp
haftmann@51160:   then have **: "n mod 256 = n div 16 mod 16 * 16 + n mod 16" by (simp only: mod_mult2_eq)
haftmann@51160:   show ?thesis
haftmann@51160:     by (simp add: char_of_nat_Char_nibbles *)
haftmann@51160:      (simp add: div_add1_eq nibble_of_nat_mod_16 [of "n div 16"] **)
haftmann@51160: qed
haftmann@49948: 
haftmann@31051: 
bulwahn@39250: subsection {* Strings as dedicated type *}
bulwahn@39250: 
wenzelm@49834: typedef literal = "UNIV :: string set"
bulwahn@39250:   morphisms explode STR ..
bulwahn@39250: 
bulwahn@39250: instantiation literal :: size
bulwahn@39250: begin
haftmann@31051: 
bulwahn@39250: definition size_literal :: "literal \<Rightarrow> nat"
bulwahn@39250: where
bulwahn@39250:   [code]: "size_literal (s\<Colon>literal) = 0"
haftmann@31051: 
bulwahn@39250: instance ..
bulwahn@39250: 
bulwahn@39250: end
bulwahn@39250: 
bulwahn@39250: instantiation literal :: equal
bulwahn@39250: begin
haftmann@31051: 
bulwahn@39250: definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool"
bulwahn@39250: where
bulwahn@39250:   "equal_literal s1 s2 \<longleftrightarrow> explode s1 = explode s2"
haftmann@31051: 
bulwahn@39250: instance
bulwahn@39250: proof
bulwahn@39250: qed (auto simp add: equal_literal_def explode_inject)
bulwahn@39250: 
bulwahn@39250: end
haftmann@31051: 
haftmann@52365: lemma [code nbe]:
haftmann@52365:   fixes s :: "String.literal"
haftmann@52365:   shows "HOL.equal s s \<longleftrightarrow> True"
haftmann@52365:   by (simp add: equal)
haftmann@52365: 
haftmann@51160: lemma STR_inject' [simp]:
haftmann@51160:   "STR xs = STR ys \<longleftrightarrow> xs = ys"
haftmann@51160:   by (simp add: STR_inject)
bulwahn@39274: 
bulwahn@39274: 
haftmann@31051: subsection {* Code generator *}
haftmann@31051: 
wenzelm@48891: ML_file "Tools/string_code.ML"
haftmann@31051: 
haftmann@33237: code_reserved SML string
haftmann@33237: code_reserved OCaml string
haftmann@34886: code_reserved Scala string
haftmann@33237: 
haftmann@52435: code_printing
haftmann@52435:   type_constructor literal \<rightharpoonup>
haftmann@52435:     (SML) "string"
haftmann@52435:     and (OCaml) "string"
haftmann@52435:     and (Haskell) "String"
haftmann@52435:     and (Scala) "String"
haftmann@31051: 
haftmann@31051: setup {*
haftmann@34886:   fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
haftmann@31051: *}
haftmann@31051: 
haftmann@52435: code_printing
haftmann@52435:   class_instance literal :: equal \<rightharpoonup>
haftmann@52435:     (Haskell) -
haftmann@52435: | constant "HOL.equal :: literal \<Rightarrow> literal \<Rightarrow> bool" \<rightharpoonup>
haftmann@52435:     (SML) "!((_ : string) = _)"
haftmann@52435:     and (OCaml) "!((_ : string) = _)"
haftmann@52435:     and (Haskell) infix 4 "=="
haftmann@52435:     and (Scala) infixl 5 "=="
haftmann@31051: 
Andreas@52910: setup {* Sign.map_naming (Name_Space.mandatory_path "Code") *}
Andreas@52910: 
Andreas@52910: definition abort :: "literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a"
Andreas@52910: where [simp, code del]: "abort _ f = f ()"
Andreas@52910: 
Andreas@52910: setup {* Sign.map_naming Name_Space.parent_path *}
Andreas@52910: 
Andreas@52910: code_printing constant Code.abort \<rightharpoonup>
Andreas@52910:     (SML) "!(raise/ Fail/ _)"
Andreas@52910:     and (OCaml) "failwith"
Andreas@52910:     and (Haskell) "error"
Andreas@52910:     and (Scala) "!{/ sys.error((_));/  ((_)).apply(())/ }"
Andreas@52910: 
wenzelm@36176: hide_type (open) literal
haftmann@31205: 
bulwahn@39250: end
haftmann@49948: