--- a/src/HOL/String.thy Fri Mar 11 17:20:14 2016 +0100
+++ b/src/HOL/String.thy Sat Mar 12 22:04:52 2016 +0100
@@ -56,7 +56,7 @@
by (simp add: char_of_nat_def Abs_char_inject)
lemma inj_on_char_of_nat [simp]:
- "inj_on char_of_nat {0..<256}"
+ "inj_on char_of_nat {..<256}"
by (rule inj_onI) simp
lemma nat_of_char_mod_256 [simp]:
@@ -72,197 +72,143 @@
qed
lemma UNIV_char_of_nat:
- "UNIV = char_of_nat ` {0..<256}"
+ "UNIV = char_of_nat ` {..<256}"
proof -
{ fix c
- have "c \<in> char_of_nat ` {0..<256}"
+ have "c \<in> char_of_nat ` {..<256}"
by (cases c) auto
} then show ?thesis by auto
qed
-
-subsubsection \<open>Traditional concrete representation of characters\<close>
-
-datatype (plugins del: transfer) nibble =
- Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
- | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
+lemma card_UNIV_char:
+ "card (UNIV :: char set) = 256"
+ by (auto simp add: UNIV_char_of_nat card_image)
-lemma UNIV_nibble:
- "UNIV = {Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
- Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF}" (is "_ = ?A")
-proof (rule UNIV_eq_I)
- fix x show "x \<in> ?A" by (cases x) simp_all
-qed
+lemma range_nat_of_char:
+ "range nat_of_char = {..<256}"
+ by (auto simp add: UNIV_char_of_nat image_image image_def)
-lemma size_nibble [code, simp]:
- "size_nibble (x::nibble) = 0"
- "size (x::nibble) = 0"
- by (cases x, simp_all)+
-instantiation nibble :: enum
+subsubsection \<open>Character literals as variant of numerals\<close>
+
+instantiation char :: zero
begin
-definition
- "Enum.enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
- Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
+definition zero_char :: char
+ where "0 = char_of_nat 0"
-definition
- "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
- \<and> P Nibble8 \<and> P Nibble9 \<and> P NibbleA \<and> P NibbleB \<and> P NibbleC \<and> P NibbleD \<and> P NibbleE \<and> P NibbleF"
-
-definition
- "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
- \<or> P Nibble8 \<or> P Nibble9 \<or> P NibbleA \<or> P NibbleB \<or> P NibbleC \<or> P NibbleD \<or> P NibbleE \<or> P NibbleF"
-
-instance proof
-qed (simp_all only: enum_nibble_def enum_all_nibble_def enum_ex_nibble_def UNIV_nibble, simp_all)
+instance ..
end
-lemma card_UNIV_nibble:
- "card (UNIV :: nibble set) = 16"
- by (simp add: card_UNIV_length_enum enum_nibble_def)
+definition Char :: "num \<Rightarrow> char"
+ where "Char k = char_of_nat (numeral k)"
+
+code_datatype "0 :: char" Char
+
+lemma nat_of_char_zero [simp]:
+ "nat_of_char 0 = 0"
+ by (simp add: zero_char_def)
+
+lemma nat_of_char_Char [simp]:
+ "nat_of_char (Char k) = numeral k mod 256"
+ by (simp add: Char_def)
-primrec nat_of_nibble :: "nibble \<Rightarrow> nat"
+lemma Char_eq_Char_iff [simp]:
+ "Char k = Char l \<longleftrightarrow> numeral k mod (256 :: nat) = numeral l mod 256" (is "?P \<longleftrightarrow> ?Q")
+proof -
+ have "?P \<longleftrightarrow> nat_of_char (Char k) = nat_of_char (Char l)"
+ by (rule sym, rule inj_eq) (fact inj_nat_of_char)
+ also have "nat_of_char (Char k) = nat_of_char (Char l) \<longleftrightarrow> ?Q"
+ by (simp only: Char_def nat_of_char_of_nat)
+ finally show ?thesis .
+qed
+
+lemma zero_eq_Char_iff [simp]:
+ "0 = Char k \<longleftrightarrow> numeral k mod (256 :: nat) = 0"
+ by (auto simp add: zero_char_def Char_def)
+
+lemma Char_eq_zero_iff [simp]:
+ "Char k = 0 \<longleftrightarrow> numeral k mod (256 :: nat) = 0"
+ by (auto simp add: zero_char_def Char_def)
+
+definition integer_of_char :: "char \<Rightarrow> integer"
where
- "nat_of_nibble Nibble0 = 0"
-| "nat_of_nibble Nibble1 = 1"
-| "nat_of_nibble Nibble2 = 2"
-| "nat_of_nibble Nibble3 = 3"
-| "nat_of_nibble Nibble4 = 4"
-| "nat_of_nibble Nibble5 = 5"
-| "nat_of_nibble Nibble6 = 6"
-| "nat_of_nibble Nibble7 = 7"
-| "nat_of_nibble Nibble8 = 8"
-| "nat_of_nibble Nibble9 = 9"
-| "nat_of_nibble NibbleA = 10"
-| "nat_of_nibble NibbleB = 11"
-| "nat_of_nibble NibbleC = 12"
-| "nat_of_nibble NibbleD = 13"
-| "nat_of_nibble NibbleE = 14"
-| "nat_of_nibble NibbleF = 15"
+ "integer_of_char = integer_of_nat \<circ> nat_of_char"
-definition nibble_of_nat :: "nat \<Rightarrow> nibble" where
- "nibble_of_nat n = Enum.enum ! (n mod 16)"
+definition char_of_integer :: "integer \<Rightarrow> char"
+where
+ "char_of_integer = char_of_nat \<circ> nat_of_integer"
+
+lemma integer_of_char_zero [simp, code]:
+ "integer_of_char 0 = 0"
+ by (simp add: integer_of_char_def integer_of_nat_def)
-lemma nibble_of_nat_simps [simp]:
- "nibble_of_nat 0 = Nibble0"
- "nibble_of_nat 1 = Nibble1"
- "nibble_of_nat 2 = Nibble2"
- "nibble_of_nat 3 = Nibble3"
- "nibble_of_nat 4 = Nibble4"
- "nibble_of_nat 5 = Nibble5"
- "nibble_of_nat 6 = Nibble6"
- "nibble_of_nat 7 = Nibble7"
- "nibble_of_nat 8 = Nibble8"
- "nibble_of_nat 9 = Nibble9"
- "nibble_of_nat 10 = NibbleA"
- "nibble_of_nat 11 = NibbleB"
- "nibble_of_nat 12 = NibbleC"
- "nibble_of_nat 13 = NibbleD"
- "nibble_of_nat 14 = NibbleE"
- "nibble_of_nat 15 = NibbleF"
- unfolding nibble_of_nat_def by (simp_all add: enum_nibble_def)
+lemma integer_of_char_Char [simp]:
+ "integer_of_char (Char k) = numeral k mod 256"
+ by (simp only: integer_of_char_def integer_of_nat_def comp_apply nat_of_char_Char map_fun_def
+ id_apply zmod_int mod_integer.abs_eq [symmetric]) simp
-lemma nibble_of_nat_of_nibble [simp]:
- "nibble_of_nat (nat_of_nibble x) = x"
- by (cases x) (simp_all add: nibble_of_nat_def enum_nibble_def)
+lemma less_256_integer_of_char_Char:
+ assumes "numeral k < (256 :: integer)"
+ shows "integer_of_char (Char k) = numeral k"
+proof -
+ have "numeral k mod 256 = (numeral k :: integer)"
+ by (rule semiring_numeral_div_class.mod_less) (insert assms, simp_all)
+ then show ?thesis using integer_of_char_Char [of k]
+ by (simp only:)
+qed
-lemma nat_of_nibble_of_nat [simp]:
- "nat_of_nibble (nibble_of_nat n) = n mod 16"
- by (cases "nibble_of_nat n")
- (simp_all add: nibble_of_nat_def enum_nibble_def nth_equal_first_eq nth_non_equal_first_eq, arith)
-
-lemma inj_nat_of_nibble:
- "inj nat_of_nibble"
- by (rule inj_on_inverseI) (rule nibble_of_nat_of_nibble)
+setup \<open>
+let
+ val chars = map_range (Thm.cterm_of @{context} o HOLogic.mk_numeral o curry (op +) 1) 255;
+ val simpset =
+ put_simpset HOL_ss @{context}
+ addsimps @{thms numeral_less_iff less_num_simps};
+ fun mk_code_eqn ct =
+ Thm.instantiate' [] [SOME ct] @{thm less_256_integer_of_char_Char}
+ |> full_simplify simpset;
+ val code_eqns = map mk_code_eqn chars;
+in
+ Global_Theory.note_thmss ""
+ [((@{binding integer_of_char_simps}, []), [(code_eqns, [])])]
+ #> snd
+end
+\<close>
-lemma nat_of_nibble_eq_iff:
- "nat_of_nibble x = nat_of_nibble y \<longleftrightarrow> x = y"
- by (rule inj_eq) (rule inj_nat_of_nibble)
+declare integer_of_char_simps [code]
+
+lemma nat_of_char_code [code]:
+ "nat_of_char = nat_of_integer \<circ> integer_of_char"
+ by (simp add: integer_of_char_def fun_eq_iff)
-lemma nat_of_nibble_less_16:
- "nat_of_nibble x < 16"
- by (cases x) auto
+lemma char_of_nat_code [code]:
+ "char_of_nat = char_of_integer \<circ> integer_of_nat"
+ by (simp add: char_of_integer_def fun_eq_iff)
-lemma nibble_of_nat_mod_16:
- "nibble_of_nat (n mod 16) = nibble_of_nat n"
- by (simp add: nibble_of_nat_def)
-
-context
+instantiation char :: equal
begin
-local_setup \<open>Local_Theory.map_background_naming (Name_Space.add_path "char")\<close>
+definition equal_char
+ where "equal_char (c :: char) d \<longleftrightarrow> c = d"
-definition Char :: "nibble \<Rightarrow> nibble \<Rightarrow> char"
-where
- "Char x y = char_of_nat (nat_of_nibble x * 16 + nat_of_nibble y)"
- \<comment> "Note: canonical order of character encoding coincides with standard term ordering"
+instance
+ by standard (simp add: equal_char_def)
end
-lemma nat_of_char_Char:
- "nat_of_char (Char x y) = nat_of_nibble x * 16 + nat_of_nibble y" (is "_ = ?rhs")
-proof -
- have "?rhs < 256"
- using nat_of_nibble_less_16 [of x] nat_of_nibble_less_16 [of y]
- by arith
- then show ?thesis by (simp add: Char_def)
-qed
-
-lemma char_of_nat_Char_nibbles:
- "char_of_nat n = Char (nibble_of_nat (n div 16)) (nibble_of_nat n)"
-proof -
- from mod_mult2_eq [of n 16 16]
- have "n mod 256 = 16 * (n div 16 mod 16) + n mod 16" by simp
- then show ?thesis
- by (simp add: Char_def)
-qed
-
-lemma char_of_nat_nibble_pair [simp]:
- "char_of_nat (nat_of_nibble a * 16 + nat_of_nibble b) = Char a b"
- by (simp add: nat_of_char_Char [symmetric])
-
-free_constructors char for Char
-proof -
- fix P c
- assume hyp: "\<And>x y. c = Char x y \<Longrightarrow> P"
- have "nat_of_char c \<le> 255"
- using nat_of_char_less_256 [of c] by arith
- then have "nat_of_char c div 16 \<le> 255 div 16"
- by (auto intro: div_le_mono2)
- then have "nat_of_char c div 16 < 16"
- by auto
- then have "nat_of_char c div 16 mod 16 = nat_of_char c div 16"
- by simp
- then have "c = Char (nibble_of_nat (nat_of_char c div 16))
- (nibble_of_nat (nat_of_char c mod 16))"
- by (simp add: Char_def)
- then show P by (rule hyp)
-next
- fix x y z w
- have "Char x y = Char z w
- \<longleftrightarrow> nat_of_char (Char x y) = nat_of_char (Char z w)"
- by auto
- 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")
- proof
- assume "?Q \<and> ?R"
- then show ?P by (simp add: nat_of_char_Char)
- next
- assume ?P
- then have ?Q
- using nat_of_nibble_less_16 [of y] nat_of_nibble_less_16 [of w]
- by (simp add: nat_of_char_Char)
- moreover with \<open>?P\<close> have ?R by (simp add: nat_of_char_Char)
- ultimately show "?Q \<and> ?R" ..
- qed
- also have "\<dots> \<longleftrightarrow> x = z \<and> y = w"
- by (simp add: nat_of_nibble_eq_iff)
- finally show "Char x y = Char z w \<longleftrightarrow> x = z \<and> y = w" .
-qed
+lemma equal_char_simps [code]:
+ "HOL.equal (0::char) 0 \<longleftrightarrow> True"
+ "HOL.equal (Char k) (Char l) \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) (numeral l mod 256)"
+ "HOL.equal 0 (Char k) \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) 0"
+ "HOL.equal (Char k) 0 \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) 0"
+ by (simp_all only: equal refl Char_eq_Char_iff zero_eq_Char_iff Char_eq_zero_iff)
syntax
- "_Char" :: "str_position => char" ("CHR _")
+ "_Char" :: "str_position \<Rightarrow> char" ("CHR _")
+
+syntax
+ "_Char_ord" :: "num_const \<Rightarrow> char" ("CHAR _")
type_synonym string = "char list"
@@ -271,84 +217,74 @@
ML_file "Tools/string_syntax.ML"
-lemma UNIV_char:
- "UNIV = image (case_prod Char) (UNIV \<times> UNIV)"
-proof (rule UNIV_eq_I)
- fix x show "x \<in> image (case_prod Char) (UNIV \<times> UNIV)" by (cases x) auto
-qed
-
instantiation char :: enum
begin
definition
- "Enum.enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
- Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
- Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,
- Char Nibble0 Nibble9, CHR ''\<newline>'', Char Nibble0 NibbleB,
- Char Nibble0 NibbleC, Char Nibble0 NibbleD, Char Nibble0 NibbleE,
- Char Nibble0 NibbleF, Char Nibble1 Nibble0, Char Nibble1 Nibble1,
- Char Nibble1 Nibble2, Char Nibble1 Nibble3, Char Nibble1 Nibble4,
- Char Nibble1 Nibble5, Char Nibble1 Nibble6, Char Nibble1 Nibble7,
- Char Nibble1 Nibble8, Char Nibble1 Nibble9, Char Nibble1 NibbleA,
- Char Nibble1 NibbleB, Char Nibble1 NibbleC, Char Nibble1 NibbleD,
- Char Nibble1 NibbleE, Char Nibble1 NibbleF, CHR '' '', CHR ''!'',
- Char Nibble2 Nibble2, CHR ''#'', CHR ''$'', CHR ''%'', CHR ''&'',
- Char Nibble2 Nibble7, CHR ''('', CHR '')'', CHR ''*'', CHR ''+'', CHR '','',
- CHR ''-'', CHR ''.'', CHR ''/'', CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
- CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9'', CHR '':'',
- CHR '';'', CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'', CHR ''@'', CHR ''A'',
- CHR ''B'', CHR ''C'', CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'', CHR ''H'',
- CHR ''I'', CHR ''J'', CHR ''K'', CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
- CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'', CHR ''T'', CHR ''U'', CHR ''V'',
- CHR ''W'', CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['', Char Nibble5 NibbleC,
- CHR '']'', CHR ''^'', CHR ''_'', Char Nibble6 Nibble0, CHR ''a'', CHR ''b'',
- CHR ''c'', CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'', CHR ''h'', CHR ''i'',
- CHR ''j'', CHR ''k'', CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'', CHR ''p'',
- CHR ''q'', CHR ''r'', CHR ''s'', CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
- CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'', CHR ''|'', CHR ''}'', CHR ''~'',
- Char Nibble7 NibbleF, Char Nibble8 Nibble0, Char Nibble8 Nibble1,
- Char Nibble8 Nibble2, Char Nibble8 Nibble3, Char Nibble8 Nibble4,
- Char Nibble8 Nibble5, Char Nibble8 Nibble6, Char Nibble8 Nibble7,
- Char Nibble8 Nibble8, Char Nibble8 Nibble9, Char Nibble8 NibbleA,
- Char Nibble8 NibbleB, Char Nibble8 NibbleC, Char Nibble8 NibbleD,
- Char Nibble8 NibbleE, Char Nibble8 NibbleF, Char Nibble9 Nibble0,
- Char Nibble9 Nibble1, Char Nibble9 Nibble2, Char Nibble9 Nibble3,
- Char Nibble9 Nibble4, Char Nibble9 Nibble5, Char Nibble9 Nibble6,
- Char Nibble9 Nibble7, Char Nibble9 Nibble8, Char Nibble9 Nibble9,
- Char Nibble9 NibbleA, Char Nibble9 NibbleB, Char Nibble9 NibbleC,
- Char Nibble9 NibbleD, Char Nibble9 NibbleE, Char Nibble9 NibbleF,
- Char NibbleA Nibble0, Char NibbleA Nibble1, Char NibbleA Nibble2,
- Char NibbleA Nibble3, Char NibbleA Nibble4, Char NibbleA Nibble5,
- Char NibbleA Nibble6, Char NibbleA Nibble7, Char NibbleA Nibble8,
- Char NibbleA Nibble9, Char NibbleA NibbleA, Char NibbleA NibbleB,
- Char NibbleA NibbleC, Char NibbleA NibbleD, Char NibbleA NibbleE,
- Char NibbleA NibbleF, Char NibbleB Nibble0, Char NibbleB Nibble1,
- Char NibbleB Nibble2, Char NibbleB Nibble3, Char NibbleB Nibble4,
- Char NibbleB Nibble5, Char NibbleB Nibble6, Char NibbleB Nibble7,
- Char NibbleB Nibble8, Char NibbleB Nibble9, Char NibbleB NibbleA,
- Char NibbleB NibbleB, Char NibbleB NibbleC, Char NibbleB NibbleD,
- Char NibbleB NibbleE, Char NibbleB NibbleF, Char NibbleC Nibble0,
- Char NibbleC Nibble1, Char NibbleC Nibble2, Char NibbleC Nibble3,
- Char NibbleC Nibble4, Char NibbleC Nibble5, Char NibbleC Nibble6,
- Char NibbleC Nibble7, Char NibbleC Nibble8, Char NibbleC Nibble9,
- Char NibbleC NibbleA, Char NibbleC NibbleB, Char NibbleC NibbleC,
- Char NibbleC NibbleD, Char NibbleC NibbleE, Char NibbleC NibbleF,
- Char NibbleD Nibble0, Char NibbleD Nibble1, Char NibbleD Nibble2,
- Char NibbleD Nibble3, Char NibbleD Nibble4, Char NibbleD Nibble5,
- Char NibbleD Nibble6, Char NibbleD Nibble7, Char NibbleD Nibble8,
- Char NibbleD Nibble9, Char NibbleD NibbleA, Char NibbleD NibbleB,
- Char NibbleD NibbleC, Char NibbleD NibbleD, Char NibbleD NibbleE,
- Char NibbleD NibbleF, Char NibbleE Nibble0, Char NibbleE Nibble1,
- Char NibbleE Nibble2, Char NibbleE Nibble3, Char NibbleE Nibble4,
- Char NibbleE Nibble5, Char NibbleE Nibble6, Char NibbleE Nibble7,
- Char NibbleE Nibble8, Char NibbleE Nibble9, Char NibbleE NibbleA,
- Char NibbleE NibbleB, Char NibbleE NibbleC, Char NibbleE NibbleD,
- Char NibbleE NibbleE, Char NibbleE NibbleF, Char NibbleF Nibble0,
- Char NibbleF Nibble1, Char NibbleF Nibble2, Char NibbleF Nibble3,
- Char NibbleF Nibble4, Char NibbleF Nibble5, Char NibbleF Nibble6,
- Char NibbleF Nibble7, Char NibbleF Nibble8, Char NibbleF Nibble9,
- Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC,
- Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
+ "Enum.enum = [0, CHAR 0x01, CHAR 0x02, CHAR 0x03,
+ CHAR 0x04, CHAR 0x05, CHAR 0x06, CHAR 0x07,
+ CHAR 0x08, CHAR 0x09, CHR ''\<newline>'', CHAR 0x0B,
+ CHAR 0x0C, CHAR 0x0D, CHAR 0x0E, CHAR 0x0F,
+ CHAR 0x10, CHAR 0x11, CHAR 0x12, CHAR 0x13,
+ CHAR 0x14, CHAR 0x15, CHAR 0x16, CHAR 0x17,
+ CHAR 0x18, CHAR 0x19, CHAR 0x1A, CHAR 0x1B,
+ CHAR 0x1C, CHAR 0x1D, CHAR 0x1E, CHAR 0x1F,
+ CHR '' '', CHR ''!'', CHAR 0x22, CHR ''#'',
+ CHR ''$'', CHR ''%'', CHR ''&'', CHAR 0x27,
+ CHR ''('', CHR '')'', CHR ''*'', CHR ''+'',
+ CHR '','', CHR ''-'', CHR ''.'', CHR ''/'',
+ CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
+ CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'',
+ CHR ''8'', CHR ''9'', CHR '':'', CHR '';'',
+ CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'',
+ CHR ''@'', CHR ''A'', CHR ''B'', CHR ''C'',
+ CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'',
+ CHR ''H'', CHR ''I'', CHR ''J'', CHR ''K'',
+ CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
+ CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'',
+ CHR ''T'', CHR ''U'', CHR ''V'', CHR ''W'',
+ CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['',
+ CHAR 0x5C, CHR '']'', CHR ''^'', CHR ''_'',
+ CHAR 0x60, CHR ''a'', CHR ''b'', CHR ''c'',
+ CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'',
+ CHR ''h'', CHR ''i'', CHR ''j'', CHR ''k'',
+ CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'',
+ CHR ''p'', CHR ''q'', CHR ''r'', CHR ''s'',
+ CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
+ CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'',
+ CHR ''|'', CHR ''}'', CHR ''~'', CHAR 0x7F,
+ CHAR 0x80, CHAR 0x81, CHAR 0x82, CHAR 0x83,
+ CHAR 0x84, CHAR 0x85, CHAR 0x86, CHAR 0x87,
+ CHAR 0x88, CHAR 0x89, CHAR 0x8A, CHAR 0x8B,
+ CHAR 0x8C, CHAR 0x8D, CHAR 0x8E, CHAR 0x8F,
+ CHAR 0x90, CHAR 0x91, CHAR 0x92, CHAR 0x93,
+ CHAR 0x94, CHAR 0x95, CHAR 0x96, CHAR 0x97,
+ CHAR 0x98, CHAR 0x99, CHAR 0x9A, CHAR 0x9B,
+ CHAR 0x9C, CHAR 0x9D, CHAR 0x9E, CHAR 0x9F,
+ CHAR 0xA0, CHAR 0xA1, CHAR 0xA2, CHAR 0xA3,
+ CHAR 0xA4, CHAR 0xA5, CHAR 0xA6, CHAR 0xA7,
+ CHAR 0xA8, CHAR 0xA9, CHAR 0xAA, CHAR 0xAB,
+ CHAR 0xAC, CHAR 0xAD, CHAR 0xAE, CHAR 0xAF,
+ CHAR 0xB0, CHAR 0xB1, CHAR 0xB2, CHAR 0xB3,
+ CHAR 0xB4, CHAR 0xB5, CHAR 0xB6, CHAR 0xB7,
+ CHAR 0xB8, CHAR 0xB9, CHAR 0xBA, CHAR 0xBB,
+ CHAR 0xBC, CHAR 0xBD, CHAR 0xBE, CHAR 0xBF,
+ CHAR 0xC0, CHAR 0xC1, CHAR 0xC2, CHAR 0xC3,
+ CHAR 0xC4, CHAR 0xC5, CHAR 0xC6, CHAR 0xC7,
+ CHAR 0xC8, CHAR 0xC9, CHAR 0xCA, CHAR 0xCB,
+ CHAR 0xCC, CHAR 0xCD, CHAR 0xCE, CHAR 0xCF,
+ CHAR 0xD0, CHAR 0xD1, CHAR 0xD2, CHAR 0xD3,
+ CHAR 0xD4, CHAR 0xD5, CHAR 0xD6, CHAR 0xD7,
+ CHAR 0xD8, CHAR 0xD9, CHAR 0xDA, CHAR 0xDB,
+ CHAR 0xDC, CHAR 0xDD, CHAR 0xDE, CHAR 0xDF,
+ CHAR 0xE0, CHAR 0xE1, CHAR 0xE2, CHAR 0xE3,
+ CHAR 0xE4, CHAR 0xE5, CHAR 0xE6, CHAR 0xE7,
+ CHAR 0xE8, CHAR 0xE9, CHAR 0xEA, CHAR 0xEB,
+ CHAR 0xEC, CHAR 0xED, CHAR 0xEE, CHAR 0xEF,
+ CHAR 0xF0, CHAR 0xF1, CHAR 0xF2, CHAR 0xF3,
+ CHAR 0xF4, CHAR 0xF5, CHAR 0xF6, CHAR 0xF7,
+ CHAR 0xF8, CHAR 0xF9, CHAR 0xFA, CHAR 0xFB,
+ CHAR 0xFC, CHAR 0xFD, CHAR 0xFE, CHAR 0xFF]"
definition
"Enum.enum_all P \<longleftrightarrow> list_all P (Enum.enum :: char list)"
@@ -356,15 +292,22 @@
definition
"Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
-lemma enum_char_product_enum_nibble:
- "(Enum.enum :: char list) = map (case_prod Char) (List.product Enum.enum Enum.enum)"
- by (simp add: enum_char_def enum_nibble_def)
+lemma enum_char_unfold:
+ "Enum.enum = map char_of_nat [0..<256]"
+proof -
+ have *: "Suc (Suc 0) = 2" by simp
+ have "map nat_of_char Enum.enum = [0..<256]"
+ by (simp add: enum_char_def upt_conv_Cons_Cons *)
+ then have "map char_of_nat (map nat_of_char Enum.enum) =
+ map char_of_nat [0..<256]" by simp
+ then show ?thesis by (simp add: comp_def)
+qed
instance proof
show UNIV: "UNIV = set (Enum.enum :: char list)"
- by (simp add: enum_char_product_enum_nibble UNIV_char enum_UNIV)
+ by (simp add: enum_char_unfold UNIV_char_of_nat atLeast0LessThan)
show "distinct (Enum.enum :: char list)"
- by (auto intro: inj_onI simp add: enum_char_product_enum_nibble distinct_map distinct_product enum_distinct)
+ by (auto simp add: enum_char_unfold distinct_map intro: inj_onI)
show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P"
by (simp add: UNIV enum_all_char_def list_all_iff)
show "\<And>P. Enum.enum_ex P \<longleftrightarrow> Bex (UNIV :: char set) P"
@@ -373,66 +316,9 @@
end
-lemma card_UNIV_char:
- "card (UNIV :: char set) = 256"
- by (simp add: card_UNIV_length_enum enum_char_def)
-
-lemma enum_char_unfold:
- "Enum.enum = map char_of_nat [0..<256]"
-proof -
- have *: "Suc (Suc 0) = 2" by simp
- have "map nat_of_char Enum.enum = [0..<256]"
- by (simp add: enum_char_def nat_of_char_Char upt_conv_Cons_Cons *)
- then have "map char_of_nat (map nat_of_char Enum.enum) =
- map char_of_nat [0..<256]" by simp
- then show ?thesis by (simp add: comp_def)
-qed
-
-setup \<open>
-let
- val nibbles = map_range (Thm.cterm_of @{context} o HOLogic.mk_nibble) 16;
- val simpset =
- put_simpset HOL_ss @{context}
- addsimps @{thms nat_of_nibble.simps mult_0 mult_1 add_0 add_0_right arith_simps numeral_plus_one};
- fun mk_code_eqn x y =
- Thm.instantiate' [] [SOME x, SOME y] @{thm nat_of_char_Char}
- |> simplify simpset;
- val code_eqns = map_product mk_code_eqn nibbles nibbles;
-in
- Global_Theory.note_thmss ""
- [((@{binding nat_of_char_simps}, []), [(code_eqns, [])])]
- #> snd
-end
-\<close>
-
-declare nat_of_char_simps [code]
-
-lemma nibble_of_nat_of_char_div_16:
- "nibble_of_nat (nat_of_char c div 16) = (case c of Char x y \<Rightarrow> x)"
- by (cases c)
- (simp add: nat_of_char_Char add.commute nat_of_nibble_less_16)
-
-lemma nibble_of_nat_nat_of_char:
- "nibble_of_nat (nat_of_char c) = (case c of Char x y \<Rightarrow> y)"
-proof (cases c)
- case (Char x y)
- then have *: "nibble_of_nat ((nat_of_nibble y + nat_of_nibble x * 16) mod 16) = y"
- by (simp add: nibble_of_nat_mod_16)
- then have "nibble_of_nat (nat_of_nibble y + nat_of_nibble x * 16) = y"
- by (simp only: nibble_of_nat_mod_16)
- with Char show ?thesis by (simp add: nat_of_char_Char add.commute)
-qed
-
-code_datatype Char \<comment> \<open>drop case certificate for char\<close>
-
-lemma case_char_code [code]:
- "char f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
- by (cases c)
- (simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.case)
-
-lemma char_of_nat_enum [code]:
- "char_of_nat n = Enum.enum ! (n mod 256)"
- by (simp add: enum_char_unfold)
+lemma char_of_integer_code [code]:
+ "char_of_integer n = Enum.enum ! (nat_of_integer n mod 256)"
+ by (simp add: char_of_integer_def enum_char_unfold)
subsection \<open>Strings as dedicated type\<close>