# HG changeset patch # Parent 3f3dc4b4504d8396c15a6a2396760ec9e4c9267c proper datatype for 8-bit characters diff -r 3f3dc4b4504d CONTRIBUTORS --- a/CONTRIBUTORS Tue Apr 24 11:38:01 2018 +0200 +++ b/CONTRIBUTORS Tue Apr 24 11:39:32 2018 +0200 @@ -6,6 +6,9 @@ Contributions to this Isabelle version -------------------------------------- +* May 2018: Florian Haftmann + Consolidation of string-like types in HOL. + * March 2018: Florian Haftmann Abstract bit operations push_bit, take_bit, drop_bit, alongside with an algebraic foundation for bit strings and word types in diff -r 3f3dc4b4504d NEWS --- a/NEWS Tue Apr 24 11:38:01 2018 +0200 +++ b/NEWS Tue Apr 24 11:39:32 2018 +0200 @@ -196,6 +196,36 @@ *** HOL *** +* Clarified relationship of characters, strings and code generation: + + * Type "char" is now a proper datatype of 8-bit values. + + * Conversions "nat_of_char" and "char_of_nat" are gone; use more + general conversions "of_char" and "char_of" with suitable + type constraints instead. + + * The zero character is just written "CHR 0x00", not + "0" any longer. + + * Type "String.literal" (for code generation) is now isomorphic + to lists of 7-bit (ASCII) values; concrete values can be written + as "STR ''...''" for sequences of printable characters and + "ASCII 0x..." for one single ASCII code point given + as hexadecimal numeral. + + * Type "String.literal" supports concatenation "... + ..." + for all standard target languages. + + * Theory Library/Code_Char is gone; study the explanations concerning + "String.literal" in the tutorial on code generation to get an idea + how target-language string literals can be converted to HOL string + values and vice versa. + + * Imperative-HOL: operation "raise" directly takes a value of type + "String.literal" as argument, not type "string". + +INCOMPATIBILITY. + * Abstract bit operations as part of Main: push_bit, take_bit, drop_bit. diff -r 3f3dc4b4504d src/Doc/Codegen/Adaptation.thy --- a/src/Doc/Codegen/Adaptation.thy Tue Apr 24 11:38:01 2018 +0200 +++ b/src/Doc/Codegen/Adaptation.thy Tue Apr 24 11:39:32 2018 +0200 @@ -168,6 +168,35 @@ Useful for code setups which involve e.g.~indexing of target-language arrays. Part of @{text "HOL-Main"}. + \item[@{theory "String"}] provides an additional datatype @{typ + String.literal} which is isomorphic to lists of 7-bit (ASCII) characters; + @{typ String.literal}s are mapped to target-language strings. + + Literal values of type @{typ String.literal} can be written + as @{text "STR ''\''"} for sequences of printable characters and + @{text "ASCII 0x\"} for one single ASCII code point given + as hexadecimal numeral; @{typ String.literal} supports concatenation + @{text "\ + \"} for all standard target languages. + + Note that the particular notion of \qt{string} is target-language + specific (sequence of 8-bit units, sequence of unicode code points, \ldots); + hence ASCII is the only reliable common base e.g.~for + printing (error) messages; more sophisticated applications + like verifying parsing algorithms require a dedicated + target-language specific model. + + Nevertheless @{typ String.literal}s can be analyzed; the core operations + for this are @{term_type String.asciis_of_literal} and + @{term_type String.literal_of_asciis} which are implemented + in a target-language-specific way; particularly @{const String.asciis_of_literal} + checks its argument at runtime to make sure that it does + not contain non-ASCII-characters, to safeguard consistency. + On top of these, more abstract conversions like @{term_type + String.explode} and @{term_type String.implode} + are implemented. + + Part of @{text "HOL-Main"}. + \item[@{text "Code_Target_Int"}] implements type @{typ int} by @{typ integer} and thus by target-language built-in integers. @@ -186,17 +215,6 @@ containing both @{text "Code_Target_Nat"} and @{text "Code_Target_Int"}. - \item[@{theory "String"}] provides an additional datatype @{typ - String.literal} which is isomorphic to strings; @{typ - String.literal}s are mapped to target-language strings. Useful - for code setups which involve e.g.~printing (error) messages. - Part of @{text "HOL-Main"}. - - \item[@{text "Code_Char"}] represents @{text HOL} characters by - character literals in target languages. \emph{Warning:} This - modifies adaptation in a non-conservative manner and thus - should always be imported \emph{last} in a theory header. - \item[@{theory "IArray"}] provides a type @{typ "'a iarray"} isomorphic to lists but implemented by (effectively immutable) arrays \emph{in SML only}. diff -r 3f3dc4b4504d src/Doc/Codegen/Computations.thy --- a/src/Doc/Codegen/Computations.thy Tue Apr 24 11:38:01 2018 +0200 +++ b/src/Doc/Codegen/Computations.thy Tue Apr 24 11:39:32 2018 +0200 @@ -472,20 +472,20 @@ check_int @{context} @{cprop "even ((0::int) + 1 + 2 + 3 + -1 + -2 + -3)"} \ -paragraph \An example for @{typ char}\ +paragraph \An example for @{typ String.literal}\ -definition %quote is_cap_letter :: "char \ bool" - where "is_cap_letter c \ (let n = nat_of_char c in 65 \ n \ n \ 90)" (*<*) +definition %quote is_cap_letter :: "String.literal \ bool" + where "is_cap_letter s \ (case String.asciis_of_literal s + of [] \ False | k # _ \ 65 \ k \ k \ 90)" (*<*) (*>*) ML %quotetypewriter \ - val check_char = @{computation_check terms: - Trueprop is_cap_letter - Char datatypes: num + val check_literal = @{computation_check terms: + Trueprop is_cap_letter datatypes: bool String.literal } \ ML_val %quotetypewriter \ - check_char @{context} @{cprop "is_cap_letter (CHR ''Y'')"} + check_literal @{context} @{cprop "is_cap_letter (STR ''Q'')"} \ diff -r 3f3dc4b4504d src/HOL/Code_Evaluation.thy --- a/src/HOL/Code_Evaluation.thy Tue Apr 24 11:38:01 2018 +0200 +++ b/src/HOL/Code_Evaluation.thy Tue Apr 24 11:39:32 2018 +0200 @@ -101,7 +101,7 @@ ML_file "~~/src/HOL/Tools/value_command.ML" -subsection \\term_of\ instances\ +subsection \Dedicated \term_of\ instances\ instantiation "fun" :: (typerep, typerep) term_of begin @@ -119,21 +119,6 @@ "term_of :: typerep \ _" "term_of :: term \ _" "term_of :: String.literal \ _" "term_of :: _ Predicate.pred \ term" "term_of :: _ Predicate.seq \ term"]] -definition case_char :: "'a \ (num \ 'a) \ char \ 'a" - where "case_char f g c = (if c = 0 then f else g (num_of_nat (nat_of_char c)))" - -lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_num_def, code]: - "term_of = - case_char (Const (STR ''Groups.zero_class.zero'') (TYPEREP(char))) - (\k. App (Const (STR ''String.Char'') (TYPEREP(num \ char))) (term_of k))" - by (rule ext) (rule term_of_anything [THEN meta_eq_to_obj_eq]) - -lemma term_of_string [code]: - "term_of s = App (Const (STR ''STR'') - (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''list'') [Typerep.Typerep (STR ''char'') []], - Typerep.Typerep (STR ''String.literal'') []])) (term_of (String.explode s))" - by (subst term_of_anything) rule - code_printing constant "term_of :: integer \ term" \ (Eval) "HOLogic.mk'_number/ HOLogic.code'_integerT" | constant "term_of :: String.literal \ term" \ (Eval) "HOLogic.mk'_literal" diff -r 3f3dc4b4504d src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Tue Apr 24 11:38:01 2018 +0200 +++ b/src/HOL/Code_Numeral.thy Tue Apr 24 11:39:32 2018 +0200 @@ -516,6 +516,20 @@ "k mod l = snd (divmod_integer k l)" by simp +definition bit_cut_integer :: "integer \ integer \ bool" + where "bit_cut_integer k = (k div 2, odd k)" + +lemma bit_cut_integer_code [code]: + "bit_cut_integer k = (if k = 0 then (0, False) + else let (r, s) = Code_Numeral.divmod_abs k 2 + in (if k > 0 then r else - r - s, s = 1))" +proof - + have "bit_cut_integer k = (let (r, s) = divmod_integer k 2 in (r, s = 1))" + by (simp add: divmod_integer_def bit_cut_integer_def odd_iff_mod_2_eq_one) + then show ?thesis + by (simp add: divmod_integer_code) (auto simp add: split_def) +qed + lemma equal_integer_code [code]: "HOL.equal 0 (0::integer) \ True" "HOL.equal 0 (Pos l) \ False" diff -r 3f3dc4b4504d src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy --- a/src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy Tue Apr 24 11:38:01 2018 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,21 +0,0 @@ - -(* Author: Florian Haftmann, TU Muenchen *) - -section \Pervasive test of code generator\ - -theory Generate_Pretty_Char -imports - Candidates - "HOL-Library.AList_Mapping" - "HOL-Library.Finite_Lattice" - "HOL-Library.Code_Char" -begin - -text \ - If any of the checks fails, inspect the code generated - by a corresponding \export_code\ command. -\ - -export_code _ checking SML OCaml? Haskell? Scala - -end diff -r 3f3dc4b4504d src/HOL/Imperative_HOL/Heap_Monad.thy --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Apr 24 11:38:01 2018 +0200 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Apr 24 11:39:32 2018 +0200 @@ -230,8 +230,10 @@ obtains "r = x" "h' = h" using assms by (rule effectE) (simp add: execute_simps) -definition raise :: "string \ 'a Heap" where \ \the string is just decoration\ - [code del]: "raise s = Heap (\_. None)" +definition raise :: "String.literal \ 'a Heap" \ \the literal is just decoration\ + where "raise s = Heap (\_. None)" + +code_datatype raise \ \avoid @{const "Heap"} formally\ lemma execute_raise [execute_simps]: "execute (raise s) = (\_. None)" @@ -309,7 +311,7 @@ subsubsection \Assertions\ definition assert :: "('a \ bool) \ 'a \ 'a Heap" where - "assert P x = (if P x then return x else raise ''assert'')" + "assert P x = (if P x then return x else raise STR ''assert'')" lemma execute_assert [execute_simps]: "P x \ execute (assert P x) h = Some (x, h)" @@ -516,32 +518,17 @@ subsection \Code generator setup\ -subsubsection \Logical intermediate layer\ - -definition raise' :: "String.literal \ 'a Heap" where - [code del]: "raise' s = raise (String.explode s)" - -lemma [code_abbrev]: "raise' (STR s) = raise s" - unfolding raise'_def by (simp add: STR_inverse) - -lemma raise_raise': (* FIXME delete candidate *) - "raise s = raise' (STR s)" - unfolding raise'_def by (simp add: STR_inverse) - -code_datatype raise' \ \avoid @{const "Heap"} formally\ - - subsubsection \SML and OCaml\ code_printing type_constructor Heap \ (SML) "(unit/ ->/ _)" code_printing constant bind \ (SML) "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())" code_printing constant return \ (SML) "!(fn/ ()/ =>/ _)" -code_printing constant Heap_Monad.raise' \ (SML) "!(raise/ Fail/ _)" +code_printing constant Heap_Monad.raise \ (SML) "!(raise/ Fail/ _)" code_printing type_constructor Heap \ (OCaml) "(unit/ ->/ _)" code_printing constant bind \ (OCaml) "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())" code_printing constant return \ (OCaml) "!(fun/ ()/ ->/ _)" -code_printing constant Heap_Monad.raise' \ (OCaml) "failwith" +code_printing constant Heap_Monad.raise \ (OCaml) "failwith" subsubsection \Haskell\ @@ -588,7 +575,7 @@ code_printing type_constructor Heap \ (Haskell) "Heap.ST/ Heap.RealWorld/ _" code_monad bind Haskell code_printing constant return \ (Haskell) "return" -code_printing constant Heap_Monad.raise' \ (Haskell) "error" +code_printing constant Heap_Monad.raise \ (Haskell) "error" subsubsection \Scala\ @@ -633,7 +620,7 @@ code_printing type_constructor Heap \ (Scala) "(Unit/ =>/ _)" code_printing constant bind \ (Scala) "Heap.bind" code_printing constant return \ (Scala) "('_: Unit)/ =>/ _" -code_printing constant Heap_Monad.raise' \ (Scala) "!sys.error((_))" +code_printing constant Heap_Monad.raise \ (Scala) "!sys.error((_))" subsubsection \Target variants with less units\ @@ -703,7 +690,7 @@ \ -hide_const (open) Heap heap guard raise' fold_map +hide_const (open) Heap heap guard fold_map end diff -r 3f3dc4b4504d src/HOL/Imperative_HOL/ex/SatChecker.thy --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy Tue Apr 24 11:38:01 2018 +0200 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy Tue Apr 24 11:39:32 2018 +0200 @@ -173,7 +173,7 @@ primrec res_mem :: "Lit \ Clause \ Clause Heap" where - "res_mem l [] = raise ''MiniSatChecked.res_thm: Cannot find literal''" + "res_mem l [] = raise STR ''MiniSatChecked.res_thm: Cannot find literal''" | "res_mem l (x#xs) = (if (x = l) then return xs else do { v \ res_mem l xs; return (x # v) })" fun resolve1 :: "Lit \ Clause \ Clause \ Clause Heap" @@ -183,7 +183,7 @@ else (if (x < y) then do { v \ resolve1 l xs (y#ys); return (x # v) } else (if (x > y) then do { v \ resolve1 l (x#xs) ys; return (y # v) } else do { v \ resolve1 l xs ys; return (x # v) })))" -| "resolve1 l [] ys = raise ''MiniSatChecked.res_thm: Cannot find literal''" +| "resolve1 l [] ys = raise STR ''MiniSatChecked.res_thm: Cannot find literal''" | "resolve1 l xs [] = res_mem l xs" fun resolve2 :: "Lit \ Clause \ Clause \ Clause Heap" @@ -193,7 +193,7 @@ else (if (x < y) then do { v \ resolve2 l xs (y#ys); return (x # v) } else (if (x > y) then do { v \ resolve2 l (x#xs) ys; return (y # v) } else do { v \ resolve2 l xs ys; return (x # v) })))" - | "resolve2 l xs [] = raise ''MiniSatChecked.res_thm: Cannot find literal''" + | "resolve2 l xs [] = raise STR ''MiniSatChecked.res_thm: Cannot find literal''" | "resolve2 l [] ys = res_mem l ys" fun res_thm' :: "Lit \ Clause \ Clause \ Clause Heap" @@ -204,8 +204,8 @@ else (if (x < y) then (res_thm' l xs (y#ys)) \ (\v. return (x # v)) else (if (x > y) then (res_thm' l (x#xs) ys) \ (\v. return (y # v)) else (res_thm' l xs ys) \ (\v. return (x # v))))))" -| "res_thm' l [] ys = raise (''MiniSatChecked.res_thm: Cannot find literal'')" -| "res_thm' l xs [] = raise (''MiniSatChecked.res_thm: Cannot find literal'')" +| "res_thm' l [] ys = raise STR ''MiniSatChecked.res_thm: Cannot find literal''" +| "res_thm' l xs [] = raise STR ''MiniSatChecked.res_thm: Cannot find literal''" declare res_mem.simps [simp del] resolve1.simps [simp del] resolve2.simps [simp del] res_thm'.simps [simp del] @@ -414,7 +414,7 @@ where "get_clause a i = do { c \ Array.nth a i; - (case c of None \ raise (''Clause not found'') + (case c of None \ raise STR ''Clause not found'' | Some x \ return x) }" @@ -422,7 +422,7 @@ primrec res_thm2 :: "Clause option array \ (Lit * ClauseId) \ Clause \ Clause Heap" where "res_thm2 a (l, j) cli = - ( if l = 0 then raise(''Illegal literal'') + ( if l = 0 then raise STR ''Illegal literal'' else do { clj \ get_clause a j; res_thm' l cli clj @@ -445,8 +445,8 @@ }" | "doProofStep2 a (Delete cid) rcs = do { Array.upd cid None a; return rcs }" | "doProofStep2 a (Root cid clause) rcs = do { Array.upd cid (Some (remdups (sort clause))) a; return (clause # rcs) }" -| "doProofStep2 a (Xstep cid1 cid2) rcs = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''" -| "doProofStep2 a (ProofDone b) rcs = raise ''MiniSatChecked.doProofStep: ProofDone constructor found.''" +| "doProofStep2 a (Xstep cid1 cid2) rcs = raise STR ''MiniSatChecked.doProofStep: Xstep constructor found.''" +| "doProofStep2 a (ProofDone b) rcs = raise STR ''MiniSatChecked.doProofStep: ProofDone constructor found.''" definition checker :: "nat \ ProofStep list \ nat \ Clause list Heap" where @@ -456,7 +456,7 @@ rcs \ foldM (doProofStep2 a) p []; ec \ Array.nth a i; (if ec = Some [] then return rcs - else raise(''No empty clause'')) + else raise STR ''No empty clause'') }" lemma effect_case_option: @@ -641,24 +641,24 @@ primrec lres_thm :: "Clause option list \ (Lit * ClauseId) \ Clause \ Clause Heap" where "lres_thm xs (l, j) cli = (if (j < List.length xs) then (case (xs ! j) of - None \ raise (''MiniSatChecked.res_thm: No resolvant clause in thms array for Conflict step.'') + None \ raise STR ''MiniSatChecked.res_thm: No resolvant clause in thms array for Conflict step.'' | Some clj \ res_thm' l cli clj - ) else raise ''Error'')" + ) else raise STR ''Error'')" fun ldoProofStep :: " ProofStep \ (Clause option list * Clause list) \ (Clause option list * Clause list) Heap" where "ldoProofStep (Conflict saveTo (i, rs)) (xs, rcl) = (case (xs ! i) of - None \ raise (''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'') + None \ raise STR ''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'' | Some cli \ do { result \ foldM (lres_thm xs) rs cli ; return ((xs[saveTo:=Some result]), rcl) })" | "ldoProofStep (Delete cid) (xs, rcl) = return (xs[cid:=None], rcl)" | "ldoProofStep (Root cid clause) (xs, rcl) = return (xs[cid:=Some (sort clause)], (remdups(sort clause)) # rcl)" -| "ldoProofStep (Xstep cid1 cid2) (xs, rcl) = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''" -| "ldoProofStep (ProofDone b) (xs, rcl) = raise ''MiniSatChecked.doProofStep: ProofDone constructor found.''" +| "ldoProofStep (Xstep cid1 cid2) (xs, rcl) = raise STR ''MiniSatChecked.doProofStep: Xstep constructor found.''" +| "ldoProofStep (ProofDone b) (xs, rcl) = raise STR ''MiniSatChecked.doProofStep: ProofDone constructor found.''" definition lchecker :: "nat \ ProofStep list \ nat \ Clause list Heap" where @@ -666,7 +666,7 @@ do { rcs \ foldM (ldoProofStep) p ([], []); (if (fst rcs ! i) = Some [] then return (snd rcs) - else raise(''No empty clause'')) + else raise STR ''No empty clause'') }" @@ -676,22 +676,22 @@ where "tres_thm t (l, j) cli = (case (rbt_lookup t j) of - None \ raise (''MiniSatChecked.res_thm: No resolvant clause in thms array for Conflict step.'') + None \ raise STR ''MiniSatChecked.res_thm: No resolvant clause in thms array for Conflict step.'' | Some clj \ res_thm' l cli clj)" fun tdoProofStep :: " ProofStep \ ((ClauseId, Clause) RBT_Impl.rbt * Clause list) \ ((ClauseId, Clause) RBT_Impl.rbt * Clause list) Heap" where "tdoProofStep (Conflict saveTo (i, rs)) (t, rcl) = (case (rbt_lookup t i) of - None \ raise (''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'') + None \ raise STR ''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'' | Some cli \ do { result \ foldM (tres_thm t) rs cli; return ((rbt_insert saveTo result t), rcl) })" | "tdoProofStep (Delete cid) (t, rcl) = return ((rbt_delete cid t), rcl)" | "tdoProofStep (Root cid clause) (t, rcl) = return (rbt_insert cid (sort clause) t, (remdups(sort clause)) # rcl)" -| "tdoProofStep (Xstep cid1 cid2) (t, rcl) = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''" -| "tdoProofStep (ProofDone b) (t, rcl) = raise ''MiniSatChecked.doProofStep: ProofDone constructor found.''" +| "tdoProofStep (Xstep cid1 cid2) (t, rcl) = raise STR ''MiniSatChecked.doProofStep: Xstep constructor found.''" +| "tdoProofStep (ProofDone b) (t, rcl) = raise STR ''MiniSatChecked.doProofStep: ProofDone constructor found.''" definition tchecker :: "nat \ ProofStep list \ nat \ Clause list Heap" where @@ -699,7 +699,7 @@ do { rcs \ foldM (tdoProofStep) p (RBT_Impl.Empty, []); (if (rbt_lookup (fst rcs) i) = Some [] then return (snd rcs) - else raise(''No empty clause'')) + else raise STR ''No empty clause'') }" export_code checker tchecker lchecker checking SML diff -r 3f3dc4b4504d src/HOL/Library/Cardinality.thy --- a/src/HOL/Library/Cardinality.thy Tue Apr 24 11:38:01 2018 +0200 +++ b/src/HOL/Library/Cardinality.thy Tue Apr 24 11:39:32 2018 +0200 @@ -27,12 +27,6 @@ lemma (in type_definition) card: "card (UNIV :: 'b set) = card A" by (simp add: univ card_image inj_on_def Abs_inject) -lemma infinite_literal: "\ finite (UNIV :: String.literal set)" -proof - - have "inj STR" by(auto intro: injI) - thus ?thesis - by(auto simp add: type_definition.univ[OF type_definition_literal] infinite_UNIV_listI dest: finite_imageD) -qed subsection \Cardinalities of types\ diff -r 3f3dc4b4504d src/HOL/Library/Char_ord.thy --- a/src/HOL/Library/Char_ord.thy Tue Apr 24 11:38:01 2018 +0200 +++ b/src/HOL/Library/Char_ord.thy Tue Apr 24 11:39:32 2018 +0200 @@ -11,27 +11,29 @@ instantiation char :: linorder begin -definition "c1 \ c2 \ nat_of_char c1 \ nat_of_char c2" -definition "c1 < c2 \ nat_of_char c1 < nat_of_char c2" +definition less_eq_char :: "char \ char \ bool" + where "c1 \ c2 \ of_char c1 \ (of_char c2 :: nat)" + +definition less_char :: "char \ char \ bool" + where "c1 < c2 \ of_char c1 < (of_char c2 :: nat)" + instance by standard (auto simp add: less_eq_char_def less_char_def) end -lemma less_eq_char_simps: - "0 \ c" - "Char k \ 0 \ numeral k mod 256 = (0 :: nat)" - "Char k \ Char l \ numeral k mod 256 \ (numeral l mod 256 :: nat)" - for c :: char - by (simp_all add: Char_def less_eq_char_def) +lemma less_eq_char_simp [simp]: + "Char b0 b1 b2 b3 b4 b5 b6 b7 \ Char c0 c1 c2 c3 c4 c5 c6 c7 + \ foldr (\b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0 + \ foldr (\b k. of_bool b + k * 2) [c0, c1, c2, c3, c4, c5, c6, c7] (0::nat)" + by (simp add: less_eq_char_def) -lemma less_char_simps: - "\ c < 0" - "0 < Char k \ (0 :: nat) < numeral k mod 256" - "Char k < Char l \ numeral k mod 256 < (numeral l mod 256 :: nat)" - for c :: char - by (simp_all add: Char_def less_char_def) +lemma less_char_simp [simp]: + "Char b0 b1 b2 b3 b4 b5 b6 b7 < Char c0 c1 c2 c3 c4 c5 c6 c7 + \ foldr (\b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0 + < foldr (\b k. of_bool b + k * 2) [c0, c1, c2, c3, c4, c5, c6, c7] (0::nat)" + by (simp add: less_char_def) instantiation char :: distrib_lattice begin @@ -44,39 +46,4 @@ end -instantiation String.literal :: linorder -begin - -context includes literal.lifting -begin - -lift_definition less_literal :: "String.literal \ String.literal \ bool" - is "ord.lexordp (<)" . - -lift_definition less_eq_literal :: "String.literal \ String.literal \ bool" - is "ord.lexordp_eq (<)" . - -instance -proof - - interpret linorder "ord.lexordp_eq (<)" "ord.lexordp (<) :: string \ string \ bool" - by (rule linorder.lexordp_linorder[where less_eq="(\)"]) unfold_locales - show "PROP ?thesis" - by intro_classes (transfer, simp add: less_le_not_le linear)+ -qed - end - -end - -lemma less_literal_code [code]: - "(<) = (\xs ys. ord.lexordp (<) (String.explode xs) (String.explode ys))" - by (simp add: less_literal.rep_eq fun_eq_iff) - -lemma less_eq_literal_code [code]: - "(\) = (\xs ys. ord.lexordp_eq (<) (String.explode xs) (String.explode ys))" - by (simp add: less_eq_literal.rep_eq fun_eq_iff) - -lifting_update literal.lifting -lifting_forget literal.lifting - -end diff -r 3f3dc4b4504d src/HOL/Library/Code_Char.thy --- a/src/HOL/Library/Code_Char.thy Tue Apr 24 11:38:01 2018 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,96 +0,0 @@ -(* Title: HOL/Library/Code_Char.thy - Author: Florian Haftmann -*) - -section \Code generation of pretty characters (and strings)\ - -theory Code_Char -imports Main Char_ord -begin - -code_printing - type_constructor char \ - (SML) "char" - and (OCaml) "char" - and (Haskell) "Prelude.Char" - and (Scala) "Char" - -setup \ - fold String_Code.add_literal_char ["SML", "OCaml", "Haskell", "Scala"] - #> String_Code.add_literal_list_string "Haskell" -\ - -code_printing - constant integer_of_char \ - (SML) "!(IntInf.fromInt o Char.ord)" - and (OCaml) "Big'_int.big'_int'_of'_int (Char.code _)" - and (Haskell) "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))" - and (Scala) "BigInt(_.toInt)" -| constant char_of_integer \ - (SML) "!(Char.chr o IntInf.toInt)" - and (OCaml) "Char.chr (Big'_int.int'_of'_big'_int _)" - and (Haskell) "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)" - and (Scala) "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else sys.error(\"character value out of range\"))" -| class_instance char :: equal \ - (Haskell) - -| constant "HOL.equal :: char \ char \ bool" \ - (SML) "!((_ : char) = _)" - and (OCaml) "!((_ : char) = _)" - and (Haskell) infix 4 "==" - and (Scala) infixl 5 "==" -| constant "Code_Evaluation.term_of :: char \ term" \ - (Eval) "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))" - -code_reserved SML - char - -code_reserved OCaml - char - -code_reserved Scala - char - -code_reserved SML String - -code_printing - constant String.implode \ - (SML) "String.implode" - and (OCaml) "!(let l = _ in let res = String.create (List.length l) in let rec imp i = function | [] -> res | c :: l -> String.set res i c; imp (i + 1) l in imp 0 l)" - and (Haskell) "_" - and (Scala) "!(\"\" ++/ _)" -| constant String.explode \ - (SML) "String.explode" - and (OCaml) "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (String.get s i :: l) in exp (String.length s - 1) [])" - and (Haskell) "_" - and (Scala) "!(_.toList)" - -code_printing - constant "Orderings.less_eq :: char \ char \ bool" \ - (SML) "!((_ : char) <= _)" - and (OCaml) "!((_ : char) <= _)" - and (Haskell) infix 4 "<=" - and (Scala) infixl 4 "<=" - and (Eval) infixl 6 "<=" -| constant "Orderings.less :: char \ char \ bool" \ - (SML) "!((_ : char) < _)" - and (OCaml) "!((_ : char) < _)" - and (Haskell) infix 4 "<" - and (Scala) infixl 4 "<" - and (Eval) infixl 6 "<" -| constant "Orderings.less_eq :: String.literal \ String.literal \ bool" \ - (SML) "!((_ : string) <= _)" - and (OCaml) "!((_ : string) <= _)" - \ \Order operations for @{typ String.literal} work in Haskell only - if no type class instance needs to be generated, because String = [Char] in Haskell - and @{typ "char list"} need not have the same order as @{typ String.literal}.\ - and (Haskell) infix 4 "<=" - and (Scala) infixl 4 "<=" - and (Eval) infixl 6 "<=" -| constant "Orderings.less :: String.literal \ String.literal \ bool" \ - (SML) "!((_ : string) < _)" - and (OCaml) "!((_ : string) < _)" - and (Haskell) infix 4 "<" - and (Scala) infixl 4 "<" - and (Eval) infixl 6 "<" - -end diff -r 3f3dc4b4504d src/HOL/Library/Code_Target_Int.thy --- a/src/HOL/Library/Code_Target_Int.thy Tue Apr 24 11:38:01 2018 +0200 +++ b/src/HOL/Library/Code_Target_Int.thy Tue Apr 24 11:39:32 2018 +0200 @@ -143,6 +143,22 @@ "nat = nat_of_integer \ of_int" including integer.lifting by transfer (simp add: fun_eq_iff) +definition char_of_int :: "int \ char" + where [code_abbrev]: "char_of_int = char_of" + +definition int_of_char :: "char \ int" + where [code_abbrev]: "int_of_char = of_char" + +lemma [code]: + "char_of_int = char_of_integer \ integer_of_int" + including integer.lifting unfolding char_of_integer_def char_of_int_def + by transfer (simp add: fun_eq_iff) + +lemma [code]: + "int_of_char = int_of_integer \ integer_of_char" + including integer.lifting unfolding integer_of_char_def int_of_char_def + by transfer (simp add: fun_eq_iff) + code_identifier code_module Code_Target_Int \ (SML) Arith and (OCaml) Arith and (Haskell) Arith diff -r 3f3dc4b4504d src/HOL/Library/Code_Target_Nat.thy --- a/src/HOL/Library/Code_Target_Nat.thy Tue Apr 24 11:38:01 2018 +0200 +++ b/src/HOL/Library/Code_Target_Nat.thy Tue Apr 24 11:39:32 2018 +0200 @@ -147,6 +147,21 @@ "integer_of_nat (nat k) = max 0 (integer_of_int k)" including integer.lifting by transfer auto +definition char_of_nat :: "nat \ char" + where [code_abbrev]: "char_of_nat = char_of" + +definition nat_of_char :: "char \ nat" + where [code_abbrev]: "nat_of_char = of_char" + +lemma [code]: + "char_of_nat = char_of_integer \ integer_of_nat" + including integer.lifting unfolding char_of_integer_def char_of_nat_def + by transfer (simp add: fun_eq_iff) + +lemma [code abstract]: + "integer_of_nat (nat_of_char c) = integer_of_char c" + by (cases c) (simp add: nat_of_char_def integer_of_char_def integer_of_nat_eq_of_nat) + lemma term_of_nat_code [code]: \ \Use @{term Code_Numeral.nat_of_integer} in term reconstruction instead of @{term Code_Target_Nat.Nat} such that reconstructed diff -r 3f3dc4b4504d src/HOL/Library/Code_Test.thy --- a/src/HOL/Library/Code_Test.thy Tue Apr 24 11:38:01 2018 +0200 +++ b/src/HOL/Library/Code_Test.thy Tue Apr 24 11:39:32 2018 +0200 @@ -84,8 +84,8 @@ definition list where "list f xs = map (node \ f) xs" -definition X :: yxml_of_term where "X = yot_literal (STR [Char (num.Bit1 (num.Bit0 num.One))])" -definition Y :: yxml_of_term where "Y = yot_literal (STR [Char (num.Bit0 (num.Bit1 num.One))])" +definition X :: yxml_of_term where "X = yot_literal (ASCII 0x05)" +definition Y :: yxml_of_term where "Y = yot_literal (ASCII 0x06)" definition XY :: yxml_of_term where "XY = yot_append X Y" definition XYX :: yxml_of_term where "XYX = yot_append XY X" diff -r 3f3dc4b4504d src/HOL/Library/Countable.thy --- a/src/HOL/Library/Countable.thy Tue Apr 24 11:38:01 2018 +0200 +++ b/src/HOL/Library/Countable.thy Tue Apr 24 11:39:32 2018 +0200 @@ -256,7 +256,7 @@ text \String literals\ instance String.literal :: countable - by (rule countable_classI [of "to_nat \ String.explode"]) (auto simp add: explode_inject) + by (rule countable_classI [of "to_nat \ String.explode"]) (simp add: String.explode_inject) text \Functions\ diff -r 3f3dc4b4504d src/HOL/Library/Predicate_Compile_Alternative_Defs.thy --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Tue Apr 24 11:38:01 2018 +0200 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Tue Apr 24 11:39:32 2018 +0200 @@ -244,7 +244,7 @@ section \Setup for String.literal\ -setup \Predicate_Compile_Data.ignore_consts [@{const_name "STR"}]\ +setup \Predicate_Compile_Data.ignore_consts [@{const_name String.Literal}]\ section \Simplification rules for optimisation\ diff -r 3f3dc4b4504d src/HOL/List.thy --- a/src/HOL/List.thy Tue Apr 24 11:38:01 2018 +0200 +++ b/src/HOL/List.thy Tue Apr 24 11:39:32 2018 +0200 @@ -6980,10 +6980,6 @@ signature LIST_CODE = sig - val implode_list: Code_Thingol.iterm -> Code_Thingol.iterm list option - val default_list: int * string - -> (Code_Printer.fixity -> Code_Thingol.iterm -> Pretty.T) - -> Code_Printer.fixity -> Code_Thingol.iterm -> Code_Thingol.iterm -> Pretty.T val add_literal_list: string -> theory -> theory end; @@ -7002,7 +6998,7 @@ | _ => NONE end; -fun default_list (target_fxy, target_cons) pr fxy t1 t2 = +fun print_list (target_fxy, target_cons) pr fxy t1 t2 = Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy ( pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1, Code_Printer.str target_cons, @@ -7016,7 +7012,7 @@ of SOME ts => Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts) | NONE => - default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2; + print_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2; in Code_Target.set_printings (Code_Symbol.Constant (@{const_name Cons}, [(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))])) diff -r 3f3dc4b4504d src/HOL/Parity.thy --- a/src/HOL/Parity.thy Tue Apr 24 11:38:01 2018 +0200 +++ b/src/HOL/Parity.thy Tue Apr 24 11:39:32 2018 +0200 @@ -407,6 +407,18 @@ by (simp add: div_mult2_eq' mult_commute) qed +lemma div_mult2_numeral_eq: + "a div numeral k div numeral l = a div numeral (k * l)" (is "?A = ?B") +proof - + have "?A = a div of_nat (numeral k) div of_nat (numeral l)" + by simp + also have "\ = a div (of_nat (numeral k) * of_nat (numeral l))" + by (fact div_mult2_eq' [symmetric]) + also have "\ = ?B" + by simp + finally show ?thesis . +qed + end class ring_parity = ring + semiring_parity diff -r 3f3dc4b4504d src/HOL/Quickcheck_Exhaustive.thy --- a/src/HOL/Quickcheck_Exhaustive.thy Tue Apr 24 11:38:01 2018 +0200 +++ b/src/HOL/Quickcheck_Exhaustive.thy Tue Apr 24 11:39:32 2018 +0200 @@ -714,24 +714,6 @@ ML_file "Tools/Quickcheck/abstract_generators.ML" -instantiation char :: full_exhaustive -begin - -definition full_exhaustive_char -where - "full_exhaustive_char f i = - (if 0 < i then - case f (0, \_ :: unit. Code_Evaluation.Const (STR ''Groups.zero_class.zero'') (TYPEREP(char))) of - Some x \ Some x - | None \ full_exhaustive_class.full_exhaustive - (\(num, t). f (char_of_nat (nat_of_num num), \_ :: unit. Code_Evaluation.App (Code_Evaluation.Const (STR ''String.Char'') TYPEREP(num \ char)) (t ()))) - (min (i - 1) 8) \ \generate at most 8 bits\ - else None)" - -instance .. - -end - hide_fact (open) orelse_def no_notation orelse (infixr "orelse" 55) diff -r 3f3dc4b4504d src/HOL/ROOT --- a/src/HOL/ROOT Tue Apr 24 11:38:01 2018 +0200 +++ b/src/HOL/ROOT Tue Apr 24 11:39:32 2018 +0200 @@ -39,7 +39,6 @@ (*data refinements and dependent applications*) AList_Mapping Code_Binary_Nat - Code_Char Code_Prolog Code_Real_Approx_By_Float Code_Target_Numeral @@ -248,7 +247,6 @@ Generate_Binary_Nat Generate_Target_Nat Generate_Efficient_Datastructures - Generate_Pretty_Char Code_Test_PolyML Code_Test_Scala theories [condition = ISABELLE_GHC] diff -r 3f3dc4b4504d src/HOL/Statespace/state_fun.ML --- a/src/HOL/Statespace/state_fun.ML Tue Apr 24 11:38:01 2018 +0200 +++ b/src/HOL/Statespace/state_fun.ML Tue Apr 24 11:39:32 2018 +0200 @@ -76,7 +76,7 @@ fun string_eq_simp_tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt - addsimps @{thms list.inject list.distinct Char_eq_Char_iff + addsimps @{thms list.inject list.distinct char.inject cong_exp_iff_simps simp_thms} addsimprocs [lazy_conj_simproc] |> Simplifier.add_cong @{thm block_conj_cong}); @@ -85,7 +85,7 @@ val lookup_ss = simpset_of (put_simpset HOL_basic_ss @{context} - addsimps (@{thms list.inject} @ @{thms Char_eq_Char_iff} + addsimps (@{thms list.inject} @ @{thms char.inject} @ @{thms list.distinct} @ @{thms simp_thms} @ [@{thm StateFun.lookup_update_id_same}, @{thm StateFun.id_id_cancel}, @{thm StateFun.lookup_update_same}, @{thm StateFun.lookup_update_other}]) @@ -161,7 +161,7 @@ val meta_ext = @{thm StateFun.meta_ext}; val ss' = simpset_of (put_simpset HOL_ss @{context} addsimps - (@{thm StateFun.update_apply} :: @{thm Fun.o_apply} :: @{thms list.inject} @ @{thms Char_eq_Char_iff} + (@{thm StateFun.update_apply} :: @{thm Fun.o_apply} :: @{thms list.inject} @ @{thms char.inject} @ @{thms list.distinct}) addsimprocs [lazy_conj_simproc, StateSpace.distinct_simproc] |> fold Simplifier.add_cong @{thms block_conj_cong}); diff -r 3f3dc4b4504d src/HOL/String.thy --- a/src/HOL/String.thy Tue Apr 24 11:38:01 2018 +0200 +++ b/src/HOL/String.thy Tue Apr 24 11:39:32 2018 +0200 @@ -6,191 +6,190 @@ imports Enum begin -subsection \Characters and strings\ +subsection \Strings as list of bytes\ -subsubsection \Characters as finite algebraic type\ +text \ + When modelling strings, we follow the approach given + in @{url "http://utf8everywhere.org/"}: -typedef char = "{n::nat. n < 256}" - morphisms nat_of_char Abs_char -proof - show "Suc 0 \ {n. n < 256}" by simp + \<^item> Strings are a list of bytes (8 bit). + + \<^item> Byte values from 0 to 127 are US-ASCII. + + \<^item> Byte values from 128 to 255 are uninterpreted blobs. +\ + +subsubsection \Bytes as datatype\ + +datatype char = + Char (digit0: bool) (digit1: bool) (digit2: bool) (digit3: bool) + (digit4: bool) (digit5: bool) (digit6: bool) (digit7: bool) + +context comm_semiring_1 +begin + +definition of_char :: "char \ 'a" + where "of_char c = ((((((of_bool (digit7 c) * 2 + + of_bool (digit6 c)) * 2 + + of_bool (digit5 c)) * 2 + + of_bool (digit4 c)) * 2 + + of_bool (digit3 c)) * 2 + + of_bool (digit2 c)) * 2 + + of_bool (digit1 c)) * 2 + + of_bool (digit0 c)" + +lemma of_char_Char [simp]: + "of_char (Char b0 b1 b2 b3 b4 b5 b6 b7) = + foldr (\b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0" + by (simp add: of_char_def ac_simps) + +end + +context semiring_parity +begin + +definition char_of :: "'a \ char" + where "char_of n = Char (odd n) (odd (drop_bit 1 n)) + (odd (drop_bit 2 n)) (odd (drop_bit 3 n)) + (odd (drop_bit 4 n)) (odd (drop_bit 5 n)) + (odd (drop_bit 6 n)) (odd (drop_bit 7 n))" + +lemma char_of_char [simp]: + "char_of (of_char c) = c" +proof (cases c) + have **: "drop_bit n (q * 2 + of_bool d) = drop_bit (n - 1) q + drop_bit n (of_bool d)" + if "n > 0" for q :: 'a and n :: nat and d :: bool + using that by (cases n) simp_all + case (Char d0 d1 d2 d3 d4 d5 d6 d7) + then show ?thesis + by (simp only: of_char_def char_of_def char.simps char.sel drop_bit_of_bool **) simp qed -setup_lifting type_definition_char +lemma char_of_comp_of_char [simp]: + "char_of \ of_char = id" + by (simp add: fun_eq_iff) -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" +lemma inj_of_char: + "inj 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)" + assume "of_char c = of_char d" + then have "char_of (of_char c) = char_of (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 of_char_eq_iff [simp]: + "of_char c = of_char d \ c = d" + by (simp add: inj_eq inj_of_char) -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 of_char_of [simp]: + "of_char (char_of a) = a mod 256" +proof - + have *: "{0::nat..<8} = {0, 1, 2, 3, 4, 5, 6, 7}" + by auto + have "of_char (char_of (take_bit 8 a)) = + (\k\{0, 1, 2, 3, 4, 5, 6, 7}. push_bit k (of_bool (odd (drop_bit k a))))" + by (simp add: of_char_def char_of_def push_bit_of_1 drop_bit_take_bit) + also have "\ = take_bit 8 a" + using * take_bit_sum [of 8 a] by simp + also have "char_of(take_bit 8 a) = char_of a" + by (simp add: char_of_def drop_bit_take_bit) + finally show ?thesis + by (simp add: take_bit_eq_mod) +qed -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_mod_256 [simp]: + "char_of (n mod 256) = char_of n" + by (metis char_of_char of_char_of) -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 of_char_mod_256 [simp]: + "of_char c mod 256 = of_char c" + by (metis char_of_char of_char_of) + +lemma char_of_quasi_inj [simp]: + "char_of m = char_of n \ m mod 256 = n mod 256" + by (metis char_of_mod_256 of_char_of) + +lemma char_of_nat_eq_iff: + "char_of n = c \ take_bit 8 n = of_char c" + by (simp add: take_bit_eq_mod) (use of_char_eq_iff in fastforce) + +lemma char_of_nat [simp]: + "char_of (of_nat n) = char_of n" + by (simp add: char_of_def String.char_of_def drop_bit_of_nat) + +end lemma inj_on_char_of_nat [simp]: - "inj_on char_of_nat {..<256}" + "inj_on char_of {0::nat..<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" + "of_char c < (256 :: nat)" proof - - have "nat_of_char c mod 256 < 256" + have "of_char c mod (256 :: nat) < 256" by arith then show ?thesis by simp qed +lemma range_nat_of_char: + "range of_char = {0::nat..<256}" +proof (rule; rule) + fix n :: nat + assume "n \ range of_char" + then show "n \ {0..<256}" + by auto +next + fix n :: nat + assume "n \ {0..<256}" + then have "n = of_char (char_of n)" + by simp + then show "n \ range of_char" + by (rule range_eqI) +qed + lemma UNIV_char_of_nat: - "UNIV = char_of_nat ` {..<256}" + "UNIV = char_of ` {0::nat..<256}" proof - - { fix c - have "c \ char_of_nat ` {..<256}" - by (cases c) auto - } then show ?thesis by auto + have "range (of_char :: char \ nat) = of_char ` char_of ` {0::nat..<256}" + by (auto simp add: range_nat_of_char intro!: image_eqI) + with inj_of_char [where ?'a = nat] show ?thesis + by (simp add: inj_image_eq_iff) qed lemma card_UNIV_char: "card (UNIV :: char set) = 256" by (auto simp add: UNIV_char_of_nat card_image) -lemma range_nat_of_char: - "range nat_of_char = {..<256}" - by (auto simp add: UNIV_char_of_nat image_image image_def) - - -subsubsection \Character literals as variant of numerals\ - -instantiation char :: zero +context + includes lifting_syntax integer.lifting natural.lifting begin -definition zero_char :: char - where "0 = char_of_nat 0" +lemma [transfer_rule]: + "(pcr_integer ===> (=)) (char_of :: int \ char) (char_of :: integer \ char)" + by (unfold char_of_def [abs_def]) transfer_prover -instance .. +lemma [transfer_rule]: + "((=) ===> pcr_integer) (of_char :: char \ int) (of_char :: char \ integer)" + by (unfold of_char_def [abs_def]) transfer_prover + +lemma [transfer_rule]: + "(pcr_natural ===> (=)) (char_of :: nat \ char) (char_of :: natural \ char)" + by (unfold char_of_def [abs_def]) transfer_prover + +lemma [transfer_rule]: + "((=) ===> pcr_natural) (of_char :: char \ nat) (of_char :: char \ natural)" + by (unfold of_char_def [abs_def]) transfer_prover end -definition Char :: "num \ char" - where "Char k = char_of_nat (numeral k)" +lifting_update integer.lifting +lifting_forget integer.lifting -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) - -lemma Char_eq_Char_iff: - "Char k = Char l \ numeral k mod (256 :: nat) = numeral l mod 256" (is "?P \ ?Q") -proof - - have "?P \ 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) \ ?Q" - by (simp only: Char_def nat_of_char_of_nat) - finally show ?thesis . -qed - -lemma zero_eq_Char_iff: - "0 = Char k \ numeral k mod (256 :: nat) = 0" - by (auto simp add: zero_char_def Char_def) - -lemma Char_eq_zero_iff: - "Char k = 0 \ numeral k mod (256 :: nat) = 0" - by (auto simp add: zero_char_def Char_def) - -simproc_setup char_eq - ("Char m = Char n" | "Char m = 0" | "0 = Char n") = \ - let - val ss = put_simpset HOL_ss @{context} - |> fold Simplifier.add_simp @{thms Char_eq_Char_iff zero_eq_Char_iff Char_eq_zero_iff cong_exp_iff_simps} - |> simpset_of - in - fn _ => fn ctxt => SOME o Simplifier.rewrite (put_simpset ss ctxt) - end -\ - -definition integer_of_char :: "char \ integer" -where - "integer_of_char = integer_of_nat \ nat_of_char" - -definition char_of_integer :: "integer \ char" -where - "char_of_integer = char_of_nat \ 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 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 modulo_integer.abs_eq [symmetric]) simp - -lemma integer_of_char_Char_code [code]: - "integer_of_char (Char k) = integer_of_num k mod 256" - by simp - -lemma nat_of_char_code [code]: - "nat_of_char = nat_of_integer \ integer_of_char" - by (simp add: integer_of_char_def fun_eq_iff) - -lemma char_of_nat_code [code]: - "char_of_nat = char_of_integer \ integer_of_nat" - by (simp add: char_of_integer_def fun_eq_iff) - -instantiation char :: equal -begin - -definition equal_char - where "equal_char (c :: char) d \ c = d" - -instance - by standard (simp add: equal_char_def) - -end - -lemma equal_char_simps [code]: - "HOL.equal (0::char) 0 \ True" - "HOL.equal (Char k) (Char l) \ HOL.equal (numeral k mod 256 :: nat) (numeral l mod 256)" - "HOL.equal 0 (Char k) \ HOL.equal (numeral k mod 256 :: nat) 0" - "HOL.equal (Char k) 0 \ 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) +lifting_update natural.lifting +lifting_forget natural.lifting syntax "_Char" :: "str_position \ char" ("CHR _") @@ -199,7 +198,7 @@ type_synonym string = "char list" syntax - "_String" :: "str_position => string" ("_") + "_String" :: "str_position \ string" ("_") ML_file "Tools/string_syntax.ML" @@ -207,7 +206,8 @@ begin definition - "Enum.enum = [0, CHR 0x01, CHR 0x02, CHR 0x03, + "Enum.enum = [ + CHR 0x00, CHR 0x01, CHR 0x02, CHR 0x03, CHR 0x04, CHR 0x05, CHR 0x06, CHR 0x07, CHR 0x08, CHR 0x09, CHR ''\'', CHR 0x0B, CHR 0x0C, CHR 0x0D, CHR 0x0E, CHR 0x0F, @@ -279,14 +279,15 @@ "Enum.enum_ex P \ list_ex P (Enum.enum :: char list)" lemma enum_char_unfold: - "Enum.enum = map char_of_nat [0..<256]" + "Enum.enum = map char_of [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) + have "map (of_char :: char \ nat) Enum.enum = [0..<256]" + by (simp add: enum_char_def of_char_def upt_conv_Cons_Cons numeral_2_eq_2 [symmetric]) + then have "map char_of (map (of_char :: char \ nat) Enum.enum) = + map char_of [0..<256]" + by simp + then show ?thesis + by simp qed instance proof @@ -302,157 +303,413 @@ end +lemma linorder_char: + "class.linorder (\c d. of_char c \ (of_char d :: nat)) (\c d. of_char c < (of_char d :: nat))" + by standard auto + +text \Optimized version for execution\ + +definition char_of_integer :: "integer \ char" + where [code_abbrev]: "char_of_integer = char_of" + +definition integer_of_char :: "char \ integer" + where [code_abbrev]: "integer_of_char = of_char" + 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) + "char_of_integer k = (let + (q0, b0) = bit_cut_integer k; + (q1, b1) = bit_cut_integer q0; + (q2, b2) = bit_cut_integer q1; + (q3, b3) = bit_cut_integer q2; + (q4, b4) = bit_cut_integer q3; + (q5, b5) = bit_cut_integer q4; + (q6, b6) = bit_cut_integer q5; + (_, b7) = bit_cut_integer q6 + in Char b0 b1 b2 b3 b4 b5 b6 b7)" + by (simp add: bit_cut_integer_def char_of_integer_def char_of_def div_mult2_numeral_eq odd_iff_mod_2_eq_one drop_bit_eq_div) -lifting_update char.lifting -lifting_forget char.lifting +lemma integer_of_char_code [code]: + "integer_of_char (Char b0 b1 b2 b3 b4 b5 b6 b7) = + ((((((of_bool b7 * 2 + of_bool b6) * 2 + + of_bool b5) * 2 + of_bool b4) * 2 + + of_bool b3) * 2 + of_bool b2) * 2 + + of_bool b1) * 2 + of_bool b0" + by (simp only: integer_of_char_def of_char_def char.sel) -subsection \Strings as dedicated type\ +subsection \Strings as dedicated type for target language code generation\ -typedef literal = "UNIV :: string set" - morphisms explode STR .. +subsubsection \Logical specification\ -setup_lifting type_definition_literal +context +begin -lemma STR_inject' [simp]: - "STR s = STR t \ s = t" +qualified definition ascii_of :: "char \ char" + where "ascii_of c = Char (digit0 c) (digit1 c) (digit2 c) (digit3 c) (digit4 c) (digit5 c) (digit6 c) False" + +qualified lemma ascii_of_Char [simp]: + "ascii_of (Char b0 b1 b2 b3 b4 b5 b6 b7) = Char b0 b1 b2 b3 b4 b5 b6 False" + by (simp add: ascii_of_def) + +qualified lemma not_digit7_ascii_of [simp]: + "\ digit7 (ascii_of c)" + by (simp add: ascii_of_def) + +qualified lemma ascii_of_idem: + "ascii_of c = c" if "\ digit7 c" + using that by (cases c) simp + +qualified lemma char_of_ascii_of [simp]: + "of_char (ascii_of c) = take_bit 7 (of_char c :: nat)" + by (cases c) + (simp add: numeral_3_eq_3 [symmetric] numeral_2_eq_2 [symmetric]) + +qualified typedef literal = "{cs. \c\set cs. \ digit7 c}" + morphisms explode Abs_literal +proof + show "[] \ {cs. \c\set cs. \ digit7 c}" + by simp +qed + +qualified setup_lifting type_definition_literal + +qualified lift_definition implode :: "string \ literal" + is "map ascii_of" + by auto + +qualified lemma implode_explode_eq [simp]: + "String.implode (String.explode s) = s" +proof transfer + fix cs + show "map ascii_of cs = cs" if "\c\set cs. \ digit7 c" + using that + by (induction cs) (simp_all add: ascii_of_idem) +qed + +qualified lemma explode_implode_eq [simp]: + "String.explode (String.implode cs) = map ascii_of cs" by transfer rule -definition implode :: "string \ String.literal" -where - [code del]: "implode = STR" +end -instantiation literal :: size + +subsubsection \Syntactic representation\ + +text \ + Logical ground representations for literals are: + + \<^enum> @{text 0} for the empty literal; + + \<^enum> @{text "Literal b0 \ b6 s"} for a literal starting with one + character and continued by another literal. + + Syntactic representations for literals are: + + \<^enum> Printable text as string prefixed with @{text STR}; + + \<^enum> A single ascii value as numerical value prefixed with @{text ASCII}. +\ + +instantiation String.literal :: zero begin -definition size_literal :: "literal \ nat" -where - [code]: "size_literal (s::literal) = 0" +context +begin + +qualified lift_definition zero_literal :: String.literal + is Nil + by simp instance .. end -instantiation literal :: equal +end + +context begin -lift_definition equal_literal :: "literal \ literal \ bool" is "(=)" . +qualified abbreviation (output) empty_literal :: String.literal + where "empty_literal \ 0" -instance by intro_classes (transfer, simp) +qualified lift_definition Literal :: "bool \ bool \ bool \ bool \