# HG changeset patch # User haftmann # Date 1455814372 -3600 # Node ID 9209770bdcdf9332a67fe133fb732096dbf914d3 # Parent 7b5468422352fd106a4d305c7aec73d3e90bea5c more direct bootstrap of char type, still retaining the nibble representation for syntax diff -r 7b5468422352 -r 9209770bdcdf src/HOL/Library/Code_Char.thy --- a/src/HOL/Library/Code_Char.thy Fri Feb 19 15:01:38 2016 +0100 +++ b/src/HOL/Library/Code_Char.thy Thu Feb 18 17:52:52 2016 +0100 @@ -78,8 +78,8 @@ folded fun_cong[OF integer_of_char_def, unfolded o_apply]] lemma char_of_integer_code [code]: - "char_of_integer n = enum_class.enum ! (nat_of_integer n mod 256)" -by(simp add: char_of_integer_def char_of_nat_def) + "char_of_integer n = Enum.enum ! (nat_of_integer n mod 256)" + by (simp add: char_of_integer_def enum_char_unfold) code_printing constant integer_of_char \ @@ -121,4 +121,3 @@ and (Eval) infixl 6 "<" end - diff -r 7b5468422352 -r 9209770bdcdf src/HOL/Quickcheck_Exhaustive.thy --- a/src/HOL/Quickcheck_Exhaustive.thy Fri Feb 19 15:01:38 2016 +0100 +++ b/src/HOL/Quickcheck_Exhaustive.thy Thu Feb 18 17:52:52 2016 +0100 @@ -630,8 +630,12 @@ (Code_Evaluation.term_of (\x y. char_of_nat (nat_of_nibble x * 16 + nat_of_nibble y))) (t1 ())) (t2 ()))))" by (simp add: check_all_char_def) -lemma full_exhaustive_char_code [code]: - "full_exhaustive_class.full_exhaustive f i = +instantiation char :: full_exhaustive +begin + +definition full_exhaustive_char +where + "full_exhaustive f i = (if 0 < i then full_exhaustive_class.full_exhaustive (\(a, b). full_exhaustive_class.full_exhaustive (\(c, d). @@ -641,7 +645,10 @@ (TYPEREP(nibble \ nibble \ char))) (b ())) (d ()))) (i - 1)) (i - 1) else None)" - by (simp add: typerep_fun_def typerep_char_def typerep_nibble_def String.char.full_exhaustive_char.simps) + +instance .. + +end hide_fact (open) orelse_def no_notation orelse (infixr "orelse" 55) diff -r 7b5468422352 -r 9209770bdcdf src/HOL/String.thy --- a/src/HOL/String.thy Fri Feb 19 15:01:38 2016 +0100 +++ b/src/HOL/String.thy Thu Feb 18 17:52:52 2016 +0100 @@ -6,8 +6,92 @@ imports Enum begin +lemma upt_conv_Cons_Cons: -- \no precondition\ -- \FIXME move\ + "m # n # ns = [m.. n # ns = [Suc m..Characters and strings\ +subsubsection \Characters as finite algebraic type\ + +typedef char = "{n::nat. n < 256}" + morphisms nat_of_char Abs_char +proof + show "Suc 0 \ {n. n < 256}" by simp +qed + +definition char_of_nat :: "nat \ char" +where + "char_of_nat n = Abs_char (n mod 256)" + +lemma char_cases [case_names char_of_nat, cases type: char]: + "(\n. c = char_of_nat n \ n < 256 \ P) \ P" + by (cases c) (simp add: char_of_nat_def) + +lemma char_of_nat_of_char [simp]: + "char_of_nat (nat_of_char c) = c" + by (cases c) (simp add: char_of_nat_def Abs_char_inject Abs_char_inverse) + +lemma inj_nat_of_char: + "inj nat_of_char" +proof (rule injI) + fix c d + assume "nat_of_char c = nat_of_char d" + then have "char_of_nat (nat_of_char c) = char_of_nat (nat_of_char d)" + by simp + then show "c = d" + by simp +qed + +lemma nat_of_char_eq_iff [simp]: + "nat_of_char c = nat_of_char d \ c = d" + by (fact nat_of_char_inject) + +lemma nat_of_char_of_nat [simp]: + "nat_of_char (char_of_nat n) = n mod 256" + by (cases "char_of_nat n") (simp add: char_of_nat_def Abs_char_inject Abs_char_inverse) + +lemma char_of_nat_mod_256 [simp]: + "char_of_nat (n mod 256) = char_of_nat n" + by (cases "char_of_nat (n mod 256)") (simp add: char_of_nat_def) + +lemma char_of_nat_quasi_inj [simp]: + "char_of_nat m = char_of_nat n \ m mod 256 = n mod 256" + by (simp add: char_of_nat_def Abs_char_inject) + +lemma inj_on_char_of_nat [simp]: + "inj_on char_of_nat {0..<256}" + by (rule inj_onI) simp + +lemma nat_of_char_mod_256 [simp]: + "nat_of_char c mod 256 = nat_of_char c" + by (cases c) simp + +lemma nat_of_char_less_256 [simp]: + "nat_of_char c < 256" +proof - + have "nat_of_char c mod 256 < 256" + by arith + then show ?thesis by simp +qed + +lemma UNIV_char_of_nat: + "UNIV = char_of_nat ` {0..<256}" +proof - + { fix c + have "c \ char_of_nat ` {0..<256}" + by (cases c) auto + } then show ?thesis by auto +qed + + +subsubsection \Traditional concrete representation of characters\ + datatype (plugins del: transfer) nibble = Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7 | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF @@ -114,9 +198,78 @@ "nibble_of_nat (n mod 16) = nibble_of_nat n" by (simp add: nibble_of_nat_def) -datatype char = Char nibble nibble +context +begin + +local_setup \Local_Theory.map_background_naming (Name_Space.add_path "char")\ + +definition Char :: "nibble \ nibble \ char" +where + "Char x y = char_of_nat (nat_of_nibble x * 16 + nat_of_nibble y)" \ "Note: canonical order of character encoding coincides with standard term ordering" +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: "\x y. c = Char x y \ P" + have "nat_of_char c \ 255" + using nat_of_char_less_256 [of c] by arith + then have "nat_of_char c div 16 \ 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 + \ nat_of_char (Char x y) = nat_of_char (Char z w)" + by auto + also have "\ \ nat_of_nibble x = nat_of_nibble z \ nat_of_nibble y = nat_of_nibble w" (is "?P \ ?Q \ ?R") + proof + assume "?Q \ ?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 \?P\ have ?R by (simp add: nat_of_char_Char) + ultimately show "?Q \ ?R" .. + qed + also have "\ \ x = z \ y = w" + by (simp add: nat_of_nibble_eq_iff) + finally show "Char x y = Char z w \ x = z \ y = w" . +qed + syntax "_Char" :: "str_position => char" ("CHR _") @@ -133,11 +286,6 @@ fix x show "x \ image (case_prod Char) (UNIV \ UNIV)" by (cases x) auto qed -lemma size_char [code, simp]: - "size_char (c::char) = 0" - "size (c::char) = 0" - by (cases c, simp)+ - instantiation char :: enum begin @@ -238,13 +386,16 @@ "card (UNIV :: char set) = 256" by (simp add: card_UNIV_length_enum enum_char_def) -definition nat_of_char :: "char \ nat" -where - "nat_of_char c = (case c of Char x y \ nat_of_nibble x * 16 + nat_of_nibble y)" - -lemma nat_of_char_Char: - "nat_of_char (Char x y) = nat_of_nibble x * 16 + nat_of_nibble y" - by (simp add: nat_of_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 \ let @@ -268,7 +419,7 @@ lemma nibble_of_nat_of_char_div_16: "nibble_of_nat (nat_of_char c div 16) = (case c of Char x y \ x)" by (cases c) - (simp add: nat_of_char_def add.commute nat_of_nibble_less_16) + (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 \ y)" @@ -278,80 +429,19 @@ 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_def add.commute) + with Char show ?thesis by (simp add: nat_of_char_Char add.commute) qed code_datatype Char \ \drop case certificate for char\ lemma case_char_code [code]: - "case_char f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))" + "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 [code]: - "rec_char = case_char" - by (simp add: fun_eq_iff split: char.split) - -definition char_of_nat :: "nat \ char" where +lemma char_of_nat_enum [code]: "char_of_nat n = Enum.enum ! (n mod 256)" - -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_of_nat_def enum_char_product_enum_nibble card_UNIV_nibble - card_UNIV_length_enum [symmetric] nibble_of_nat_def product_nth add.commute) -qed - -lemma char_of_nat_of_char [simp]: - "char_of_nat (nat_of_char c) = c" - by (cases c) - (simp add: char_of_nat_Char_nibbles nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char) - -lemma nat_of_char_of_nat [simp]: - "nat_of_char (char_of_nat n) = n mod 256" -proof - - have "n mod 256 = n mod (16 * 16)" by simp - then have "n div 16 mod 16 * 16 + n mod 16 = n mod 256" by (simp only: mod_mult2_eq) - then show ?thesis - by (cases "char_of_nat n") (auto simp add: nat_of_char_def char_of_nat_Char_nibbles) -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]) - -lemma inj_nat_of_char: - "inj nat_of_char" - by (rule inj_on_inverseI) (rule char_of_nat_of_char) - -lemma nat_of_char_eq_iff: - "nat_of_char c = nat_of_char d \ c = d" - by (rule inj_eq) (rule inj_nat_of_char) - -lemma nat_of_char_less_256: - "nat_of_char c < 256" -proof (cases c) - case (Char x y) - with nat_of_nibble_less_16 [of x] nat_of_nibble_less_16 [of y] - show ?thesis by (simp add: nat_of_char_def) -qed - -lemma char_of_nat_mod_256: - "char_of_nat (n mod 256) = char_of_nat n" -proof - - from nibble_of_nat_mod_16 [of "n mod 256"] - have "nibble_of_nat (n mod 256) = nibble_of_nat (n mod 256 mod 16)" by simp - with nibble_of_nat_mod_16 [of n] - have *: "nibble_of_nat (n mod 256) = nibble_of_nat n" by (simp add: mod_mod_cancel) - have "n mod 256 = n mod (16 * 16)" by simp - then have **: "n mod 256 = n div 16 mod 16 * 16 + n mod 16" by (simp only: mod_mult2_eq) - show ?thesis - by (simp add: char_of_nat_Char_nibbles *) - (simp add: div_add1_eq nibble_of_nat_mod_16 [of "n div 16"] **) -qed + by (simp add: enum_char_unfold) subsection \Strings as dedicated type\