proper datatype for 8-bit characters
authorhaftmann
Tue Apr 24 14:17:58 2018 +0000 (14 months ago)
changeset 680281f9f973eed2a
parent 68027 64559e1ca05b
child 68029 df9044efd054
child 68031 eda52f4cd4e4
proper datatype for 8-bit characters
CONTRIBUTORS
NEWS
src/Doc/Codegen/Adaptation.thy
src/Doc/Codegen/Computations.thy
src/HOL/Code_Evaluation.thy
src/HOL/Code_Numeral.thy
src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Imperative_HOL/ex/SatChecker.thy
src/HOL/Library/Cardinality.thy
src/HOL/Library/Char_ord.thy
src/HOL/Library/Code_Char.thy
src/HOL/Library/Code_Target_Int.thy
src/HOL/Library/Code_Target_Nat.thy
src/HOL/Library/Code_Test.thy
src/HOL/Library/Countable.thy
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
src/HOL/List.thy
src/HOL/Parity.thy
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/ROOT
src/HOL/Statespace/state_fun.ML
src/HOL/String.thy
src/HOL/Tools/hologic.ML
src/HOL/Tools/literal.ML
src/HOL/Tools/numeral.ML
src/HOL/Tools/string_code.ML
src/HOL/Tools/string_syntax.ML
src/HOL/ex/Cartouche_Examples.thy
src/Pure/General/integer.ML
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_printer.ML
src/Tools/Code/code_scala.ML
     1.1 --- a/CONTRIBUTORS	Tue Apr 24 14:17:57 2018 +0000
     1.2 +++ b/CONTRIBUTORS	Tue Apr 24 14:17:58 2018 +0000
     1.3 @@ -6,6 +6,9 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* May 2018: Florian Haftmann
     1.8 +  Consolidation of string-like types in HOL.
     1.9 +
    1.10  * March 2018: Florian Haftmann
    1.11    Abstract bit operations push_bit, take_bit, drop_bit, alongside
    1.12    with an algebraic foundation for bit strings and word types in
     2.1 --- a/NEWS	Tue Apr 24 14:17:57 2018 +0000
     2.2 +++ b/NEWS	Tue Apr 24 14:17:58 2018 +0000
     2.3 @@ -196,6 +196,36 @@
     2.4  
     2.5  *** HOL ***
     2.6  
     2.7 +* Clarified relationship of characters, strings and code generation:
     2.8 +
     2.9 +  * Type "char" is now a proper datatype of 8-bit values.
    2.10 +
    2.11 +  * Conversions "nat_of_char" and "char_of_nat" are gone; use more
    2.12 +    general conversions "of_char" and "char_of" with suitable
    2.13 +    type constraints instead.
    2.14 +
    2.15 +  * The zero character is just written "CHR 0x00", not
    2.16 +    "0" any longer.
    2.17 +
    2.18 +  * Type "String.literal" (for code generation) is now isomorphic
    2.19 +    to lists of 7-bit (ASCII) values; concrete values can be written
    2.20 +    as "STR ''...''" for sequences of printable characters and
    2.21 +    "ASCII 0x..." for one single ASCII code point given
    2.22 +    as hexadecimal numeral.
    2.23 +
    2.24 +  * Type "String.literal" supports concatenation "... + ..."
    2.25 +    for all standard target languages.
    2.26 +
    2.27 +  * Theory Library/Code_Char is gone; study the explanations concerning
    2.28 +    "String.literal" in the tutorial on code generation to get an idea
    2.29 +    how target-language string literals can be converted to HOL string
    2.30 +    values and vice versa.
    2.31 +
    2.32 +  * Imperative-HOL: operation "raise" directly takes a value of type
    2.33 +    "String.literal" as argument, not type "string".
    2.34 +
    2.35 +INCOMPATIBILITY.
    2.36 +
    2.37  * Abstract bit operations as part of Main: push_bit, take_bit,
    2.38  drop_bit.
    2.39  
     3.1 --- a/src/Doc/Codegen/Adaptation.thy	Tue Apr 24 14:17:57 2018 +0000
     3.2 +++ b/src/Doc/Codegen/Adaptation.thy	Tue Apr 24 14:17:58 2018 +0000
     3.3 @@ -168,6 +168,35 @@
     3.4         Useful for code setups which involve e.g.~indexing
     3.5         of target-language arrays.  Part of @{text "HOL-Main"}.
     3.6  
     3.7 +    \item[@{theory "String"}] provides an additional datatype @{typ
     3.8 +       String.literal} which is isomorphic to lists of 7-bit (ASCII) characters;
     3.9 +       @{typ String.literal}s are mapped to target-language strings.
    3.10 +
    3.11 +       Literal values of type @{typ String.literal} can be written
    3.12 +       as @{text "STR ''\<dots>''"} for sequences of printable characters and
    3.13 +       @{text "ASCII 0x\<dots>"} for one single ASCII code point given
    3.14 +       as hexadecimal numeral; @{typ String.literal} supports concatenation
    3.15 +       @{text "\<dots> + \<dots>"} for all standard target languages.
    3.16 +
    3.17 +       Note that the particular notion of \qt{string} is target-language
    3.18 +       specific (sequence of 8-bit units, sequence of unicode code points, \ldots);
    3.19 +       hence ASCII is the only reliable common base e.g.~for
    3.20 +       printing (error) messages; more sophisticated applications
    3.21 +       like verifying parsing algorithms require a dedicated
    3.22 +       target-language specific model.
    3.23 +
    3.24 +       Nevertheless @{typ String.literal}s can be analyzed; the core operations
    3.25 +       for this are @{term_type String.asciis_of_literal} and
    3.26 +       @{term_type String.literal_of_asciis} which are implemented
    3.27 +       in a target-language-specific way; particularly @{const String.asciis_of_literal}
    3.28 +       checks its argument at runtime to make sure that it does
    3.29 +       not contain non-ASCII-characters, to safeguard consistency.
    3.30 +       On top of these, more abstract conversions like @{term_type
    3.31 +       String.explode} and @{term_type String.implode}
    3.32 +       are implemented.
    3.33 +       
    3.34 +       Part of @{text "HOL-Main"}.
    3.35 +
    3.36      \item[@{text "Code_Target_Int"}] implements type @{typ int}
    3.37         by @{typ integer} and thus by target-language built-in integers.
    3.38  
    3.39 @@ -186,17 +215,6 @@
    3.40         containing both @{text "Code_Target_Nat"} and
    3.41         @{text "Code_Target_Int"}.
    3.42  
    3.43 -    \item[@{theory "String"}] provides an additional datatype @{typ
    3.44 -       String.literal} which is isomorphic to strings; @{typ
    3.45 -       String.literal}s are mapped to target-language strings.  Useful
    3.46 -       for code setups which involve e.g.~printing (error) messages.
    3.47 -       Part of @{text "HOL-Main"}.
    3.48 -
    3.49 -    \item[@{text "Code_Char"}] represents @{text HOL} characters by
    3.50 -       character literals in target languages.  \emph{Warning:} This
    3.51 -       modifies adaptation in a non-conservative manner and thus
    3.52 -       should always be imported \emph{last} in a theory header.
    3.53 -
    3.54      \item[@{theory "IArray"}] provides a type @{typ "'a iarray"}
    3.55         isomorphic to lists but implemented by (effectively immutable)
    3.56         arrays \emph{in SML only}.
     4.1 --- a/src/Doc/Codegen/Computations.thy	Tue Apr 24 14:17:57 2018 +0000
     4.2 +++ b/src/Doc/Codegen/Computations.thy	Tue Apr 24 14:17:58 2018 +0000
     4.3 @@ -472,20 +472,20 @@
     4.4    check_int @{context} @{cprop "even ((0::int) + 1 + 2 + 3 + -1 + -2 + -3)"}
     4.5  \<close>
     4.6    
     4.7 -paragraph \<open>An example for @{typ char}\<close>
     4.8 +paragraph \<open>An example for @{typ String.literal}\<close>
     4.9  
    4.10 -definition %quote is_cap_letter :: "char \<Rightarrow> bool"
    4.11 -  where "is_cap_letter c \<longleftrightarrow> (let n = nat_of_char c in 65 \<le> n \<and> n \<le> 90)" (*<*)
    4.12 +definition %quote is_cap_letter :: "String.literal \<Rightarrow> bool"
    4.13 +  where "is_cap_letter s \<longleftrightarrow> (case String.asciis_of_literal s
    4.14 +    of [] \<Rightarrow> False | k # _ \<Rightarrow> 65 \<le> k \<and> k \<le> 90)" (*<*)
    4.15  
    4.16  (*>*) ML %quotetypewriter \<open>
    4.17 -  val check_char = @{computation_check terms:
    4.18 -    Trueprop is_cap_letter
    4.19 -    Char datatypes: num
    4.20 +  val check_literal = @{computation_check terms:
    4.21 +    Trueprop is_cap_letter datatypes: bool String.literal
    4.22    }
    4.23  \<close>
    4.24  
    4.25  ML_val %quotetypewriter \<open>
    4.26 -  check_char @{context} @{cprop "is_cap_letter (CHR ''Y'')"}
    4.27 +  check_literal @{context} @{cprop "is_cap_letter (STR ''Q'')"}
    4.28  \<close>
    4.29  
    4.30    
     5.1 --- a/src/HOL/Code_Evaluation.thy	Tue Apr 24 14:17:57 2018 +0000
     5.2 +++ b/src/HOL/Code_Evaluation.thy	Tue Apr 24 14:17:58 2018 +0000
     5.3 @@ -101,7 +101,7 @@
     5.4  ML_file "~~/src/HOL/Tools/value_command.ML"
     5.5  
     5.6  
     5.7 -subsection \<open>\<open>term_of\<close> instances\<close>
     5.8 +subsection \<open>Dedicated \<open>term_of\<close> instances\<close>
     5.9  
    5.10  instantiation "fun" :: (typerep, typerep) term_of
    5.11  begin
    5.12 @@ -119,21 +119,6 @@
    5.13    "term_of :: typerep \<Rightarrow> _" "term_of :: term \<Rightarrow> _" "term_of :: String.literal \<Rightarrow> _"
    5.14    "term_of :: _ Predicate.pred \<Rightarrow> term" "term_of :: _ Predicate.seq \<Rightarrow> term"]]
    5.15  
    5.16 -definition case_char :: "'a \<Rightarrow> (num \<Rightarrow> 'a) \<Rightarrow> char \<Rightarrow> 'a"
    5.17 -  where "case_char f g c = (if c = 0 then f else g (num_of_nat (nat_of_char c)))"
    5.18 -
    5.19 -lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_num_def, code]:
    5.20 -  "term_of =
    5.21 -    case_char (Const (STR ''Groups.zero_class.zero'') (TYPEREP(char)))
    5.22 -    (\<lambda>k. App (Const (STR ''String.Char'') (TYPEREP(num \<Rightarrow> char))) (term_of k))"
    5.23 -  by (rule ext) (rule term_of_anything [THEN meta_eq_to_obj_eq])
    5.24 -
    5.25 -lemma term_of_string [code]:
    5.26 -   "term_of s = App (Const (STR ''STR'')
    5.27 -     (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''list'') [Typerep.Typerep (STR ''char'') []],
    5.28 -       Typerep.Typerep (STR ''String.literal'') []])) (term_of (String.explode s))"
    5.29 -  by (subst term_of_anything) rule 
    5.30 -  
    5.31  code_printing
    5.32    constant "term_of :: integer \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_number/ HOLogic.code'_integerT"
    5.33  | constant "term_of :: String.literal \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_literal"
     6.1 --- a/src/HOL/Code_Numeral.thy	Tue Apr 24 14:17:57 2018 +0000
     6.2 +++ b/src/HOL/Code_Numeral.thy	Tue Apr 24 14:17:58 2018 +0000
     6.3 @@ -516,6 +516,20 @@
     6.4    "k mod l = snd (divmod_integer k l)"
     6.5    by simp
     6.6  
     6.7 +definition bit_cut_integer :: "integer \<Rightarrow> integer \<times> bool"
     6.8 +  where "bit_cut_integer k = (k div 2, odd k)"
     6.9 +
    6.10 +lemma bit_cut_integer_code [code]:
    6.11 +  "bit_cut_integer k = (if k = 0 then (0, False)
    6.12 +     else let (r, s) = Code_Numeral.divmod_abs k 2
    6.13 +       in (if k > 0 then r else - r - s, s = 1))"
    6.14 +proof -
    6.15 +  have "bit_cut_integer k = (let (r, s) = divmod_integer k 2 in (r, s = 1))"
    6.16 +    by (simp add: divmod_integer_def bit_cut_integer_def odd_iff_mod_2_eq_one)
    6.17 +  then show ?thesis
    6.18 +    by (simp add: divmod_integer_code) (auto simp add: split_def)
    6.19 +qed
    6.20 +
    6.21  lemma equal_integer_code [code]:
    6.22    "HOL.equal 0 (0::integer) \<longleftrightarrow> True"
    6.23    "HOL.equal 0 (Pos l) \<longleftrightarrow> False"
     7.1 --- a/src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy	Tue Apr 24 14:17:57 2018 +0000
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,21 +0,0 @@
     7.4 -
     7.5 -(* Author: Florian Haftmann, TU Muenchen *)
     7.6 -
     7.7 -section \<open>Pervasive test of code generator\<close>
     7.8 -
     7.9 -theory Generate_Pretty_Char
    7.10 -imports
    7.11 -  Candidates
    7.12 -  "HOL-Library.AList_Mapping"
    7.13 -  "HOL-Library.Finite_Lattice"
    7.14 -  "HOL-Library.Code_Char"
    7.15 -begin
    7.16 -
    7.17 -text \<open>
    7.18 -  If any of the checks fails, inspect the code generated
    7.19 -  by a corresponding \<open>export_code\<close> command.
    7.20 -\<close>
    7.21 -
    7.22 -export_code _ checking SML OCaml? Haskell? Scala
    7.23 -
    7.24 -end
     8.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Apr 24 14:17:57 2018 +0000
     8.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Apr 24 14:17:58 2018 +0000
     8.3 @@ -230,8 +230,10 @@
     8.4    obtains "r = x" "h' = h"
     8.5    using assms by (rule effectE) (simp add: execute_simps)
     8.6  
     8.7 -definition raise :: "string \<Rightarrow> 'a Heap" where \<comment> \<open>the string is just decoration\<close>
     8.8 -  [code del]: "raise s = Heap (\<lambda>_. None)"
     8.9 +definition raise :: "String.literal \<Rightarrow> 'a Heap" \<comment> \<open>the literal is just decoration\<close>
    8.10 +  where "raise s = Heap (\<lambda>_. None)"
    8.11 +
    8.12 +code_datatype raise \<comment> \<open>avoid @{const "Heap"} formally\<close>
    8.13  
    8.14  lemma execute_raise [execute_simps]:
    8.15    "execute (raise s) = (\<lambda>_. None)"
    8.16 @@ -309,7 +311,7 @@
    8.17  subsubsection \<open>Assertions\<close>
    8.18  
    8.19  definition assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap" where
    8.20 -  "assert P x = (if P x then return x else raise ''assert'')"
    8.21 +  "assert P x = (if P x then return x else raise STR ''assert'')"
    8.22  
    8.23  lemma execute_assert [execute_simps]:
    8.24    "P x \<Longrightarrow> execute (assert P x) h = Some (x, h)"
    8.25 @@ -516,32 +518,17 @@
    8.26  
    8.27  subsection \<open>Code generator setup\<close>
    8.28  
    8.29 -subsubsection \<open>Logical intermediate layer\<close>
    8.30 -
    8.31 -definition raise' :: "String.literal \<Rightarrow> 'a Heap" where
    8.32 -  [code del]: "raise' s = raise (String.explode s)"
    8.33 -
    8.34 -lemma [code_abbrev]: "raise' (STR s) = raise s"
    8.35 -  unfolding raise'_def by (simp add: STR_inverse)
    8.36 -
    8.37 -lemma raise_raise': (* FIXME delete candidate *)
    8.38 -  "raise s = raise' (STR s)"
    8.39 -  unfolding raise'_def by (simp add: STR_inverse)
    8.40 -
    8.41 -code_datatype raise' \<comment> \<open>avoid @{const "Heap"} formally\<close>
    8.42 -
    8.43 -
    8.44  subsubsection \<open>SML and OCaml\<close>
    8.45  
    8.46  code_printing type_constructor Heap \<rightharpoonup> (SML) "(unit/ ->/ _)"
    8.47  code_printing constant bind \<rightharpoonup> (SML) "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())"
    8.48  code_printing constant return \<rightharpoonup> (SML) "!(fn/ ()/ =>/ _)"
    8.49 -code_printing constant Heap_Monad.raise' \<rightharpoonup> (SML) "!(raise/ Fail/ _)"
    8.50 +code_printing constant Heap_Monad.raise \<rightharpoonup> (SML) "!(raise/ Fail/ _)"
    8.51  
    8.52  code_printing type_constructor Heap \<rightharpoonup> (OCaml) "(unit/ ->/ _)"
    8.53  code_printing constant bind \<rightharpoonup> (OCaml) "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())"
    8.54  code_printing constant return \<rightharpoonup> (OCaml) "!(fun/ ()/ ->/ _)"
    8.55 -code_printing constant Heap_Monad.raise' \<rightharpoonup> (OCaml) "failwith"
    8.56 +code_printing constant Heap_Monad.raise \<rightharpoonup> (OCaml) "failwith"
    8.57  
    8.58  
    8.59  subsubsection \<open>Haskell\<close>
    8.60 @@ -588,7 +575,7 @@
    8.61  code_printing type_constructor Heap \<rightharpoonup> (Haskell) "Heap.ST/ Heap.RealWorld/ _"
    8.62  code_monad bind Haskell
    8.63  code_printing constant return \<rightharpoonup> (Haskell) "return"
    8.64 -code_printing constant Heap_Monad.raise' \<rightharpoonup> (Haskell) "error"
    8.65 +code_printing constant Heap_Monad.raise \<rightharpoonup> (Haskell) "error"
    8.66  
    8.67  
    8.68  subsubsection \<open>Scala\<close>
    8.69 @@ -633,7 +620,7 @@
    8.70  code_printing type_constructor Heap \<rightharpoonup> (Scala) "(Unit/ =>/ _)"
    8.71  code_printing constant bind \<rightharpoonup> (Scala) "Heap.bind"
    8.72  code_printing constant return \<rightharpoonup> (Scala) "('_: Unit)/ =>/ _"
    8.73 -code_printing constant Heap_Monad.raise' \<rightharpoonup> (Scala) "!sys.error((_))"
    8.74 +code_printing constant Heap_Monad.raise \<rightharpoonup> (Scala) "!sys.error((_))"
    8.75  
    8.76  
    8.77  subsubsection \<open>Target variants with less units\<close>
    8.78 @@ -703,7 +690,7 @@
    8.79  
    8.80  \<close>
    8.81  
    8.82 -hide_const (open) Heap heap guard raise' fold_map
    8.83 +hide_const (open) Heap heap guard fold_map
    8.84  
    8.85  end
    8.86  
     9.1 --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Apr 24 14:17:57 2018 +0000
     9.2 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Apr 24 14:17:58 2018 +0000
     9.3 @@ -173,7 +173,7 @@
     9.4  
     9.5  primrec res_mem :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause Heap"
     9.6  where
     9.7 -  "res_mem l [] = raise ''MiniSatChecked.res_thm: Cannot find literal''"
     9.8 +  "res_mem l [] = raise STR ''MiniSatChecked.res_thm: Cannot find literal''"
     9.9  | "res_mem l (x#xs) = (if (x = l) then return xs else do { v \<leftarrow> res_mem l xs; return (x # v) })"
    9.10  
    9.11  fun resolve1 :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause \<Rightarrow> Clause Heap"
    9.12 @@ -183,7 +183,7 @@
    9.13    else (if (x < y) then do { v \<leftarrow> resolve1 l xs (y#ys); return (x # v) }
    9.14    else (if (x > y) then do { v \<leftarrow> resolve1 l (x#xs) ys; return (y # v) }
    9.15    else do { v \<leftarrow> resolve1 l xs ys; return (x # v) })))"
    9.16 -| "resolve1 l [] ys = raise ''MiniSatChecked.res_thm: Cannot find literal''"
    9.17 +| "resolve1 l [] ys = raise STR ''MiniSatChecked.res_thm: Cannot find literal''"
    9.18  | "resolve1 l xs [] = res_mem l xs"
    9.19  
    9.20  fun resolve2 :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause \<Rightarrow> Clause Heap" 
    9.21 @@ -193,7 +193,7 @@
    9.22    else (if (x < y) then do { v \<leftarrow> resolve2 l xs (y#ys); return (x # v) }
    9.23    else (if (x > y) then do { v \<leftarrow> resolve2 l (x#xs) ys; return (y # v) }
    9.24    else do { v \<leftarrow> resolve2 l xs ys; return (x # v) })))"
    9.25 -  | "resolve2 l xs [] = raise ''MiniSatChecked.res_thm: Cannot find literal''"
    9.26 +  | "resolve2 l xs [] = raise STR ''MiniSatChecked.res_thm: Cannot find literal''"
    9.27    | "resolve2 l [] ys = res_mem l ys"
    9.28  
    9.29  fun res_thm' :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause \<Rightarrow> Clause Heap"
    9.30 @@ -204,8 +204,8 @@
    9.31    else (if (x < y) then (res_thm' l xs (y#ys)) \<bind> (\<lambda>v. return (x # v))
    9.32    else (if (x > y) then (res_thm' l (x#xs) ys) \<bind> (\<lambda>v. return (y # v))
    9.33    else (res_thm' l xs ys) \<bind> (\<lambda>v. return (x # v))))))"
    9.34 -| "res_thm' l [] ys = raise (''MiniSatChecked.res_thm: Cannot find literal'')"
    9.35 -| "res_thm' l xs [] = raise (''MiniSatChecked.res_thm: Cannot find literal'')"
    9.36 +| "res_thm' l [] ys = raise STR ''MiniSatChecked.res_thm: Cannot find literal''"
    9.37 +| "res_thm' l xs [] = raise STR ''MiniSatChecked.res_thm: Cannot find literal''"
    9.38  
    9.39  declare res_mem.simps [simp del] resolve1.simps [simp del] resolve2.simps [simp del] res_thm'.simps [simp del]
    9.40  
    9.41 @@ -414,7 +414,7 @@
    9.42  where
    9.43    "get_clause a i = 
    9.44         do { c \<leftarrow> Array.nth a i;
    9.45 -           (case c of None \<Rightarrow> raise (''Clause not found'')
    9.46 +           (case c of None \<Rightarrow> raise STR ''Clause not found''
    9.47                      | Some x \<Rightarrow> return x)
    9.48         }"
    9.49  
    9.50 @@ -422,7 +422,7 @@
    9.51  primrec res_thm2 :: "Clause option array \<Rightarrow> (Lit * ClauseId) \<Rightarrow> Clause \<Rightarrow> Clause Heap"
    9.52  where
    9.53    "res_thm2 a (l, j) cli =
    9.54 -  ( if l = 0 then raise(''Illegal literal'')
    9.55 +  ( if l = 0 then raise STR ''Illegal literal''
    9.56      else
    9.57       do { clj \<leftarrow> get_clause a j;
    9.58           res_thm' l cli clj
    9.59 @@ -445,8 +445,8 @@
    9.60    }"
    9.61  | "doProofStep2 a (Delete cid) rcs = do { Array.upd cid None a; return rcs }"
    9.62  | "doProofStep2 a (Root cid clause) rcs = do { Array.upd cid (Some (remdups (sort clause))) a; return (clause # rcs) }"
    9.63 -| "doProofStep2 a (Xstep cid1 cid2) rcs = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''"
    9.64 -| "doProofStep2 a (ProofDone b) rcs = raise ''MiniSatChecked.doProofStep: ProofDone constructor found.''"
    9.65 +| "doProofStep2 a (Xstep cid1 cid2) rcs = raise STR ''MiniSatChecked.doProofStep: Xstep constructor found.''"
    9.66 +| "doProofStep2 a (ProofDone b) rcs = raise STR ''MiniSatChecked.doProofStep: ProofDone constructor found.''"
    9.67  
    9.68  definition checker :: "nat \<Rightarrow> ProofStep list \<Rightarrow> nat \<Rightarrow> Clause list Heap"
    9.69  where
    9.70 @@ -456,7 +456,7 @@
    9.71       rcs \<leftarrow> foldM (doProofStep2 a) p [];
    9.72       ec \<leftarrow> Array.nth a i;
    9.73       (if ec = Some [] then return rcs 
    9.74 -                else raise(''No empty clause''))
    9.75 +                else raise STR ''No empty clause'')
    9.76    }"
    9.77  
    9.78  lemma effect_case_option:
    9.79 @@ -641,24 +641,24 @@
    9.80  primrec lres_thm :: "Clause option list \<Rightarrow> (Lit * ClauseId) \<Rightarrow> Clause \<Rightarrow> Clause Heap" 
    9.81  where
    9.82    "lres_thm xs (l, j) cli = (if (j < List.length xs) then (case (xs ! j) of
    9.83 -  None \<Rightarrow> raise (''MiniSatChecked.res_thm: No resolvant clause in thms array for Conflict step.'')
    9.84 +  None \<Rightarrow> raise STR ''MiniSatChecked.res_thm: No resolvant clause in thms array for Conflict step.''
    9.85    | Some clj \<Rightarrow> res_thm' l cli clj
    9.86 - ) else raise ''Error'')"
    9.87 + ) else raise STR ''Error'')"
    9.88  
    9.89  
    9.90  fun ldoProofStep :: " ProofStep \<Rightarrow> (Clause option list  * Clause list) \<Rightarrow> (Clause option list * Clause list) Heap"
    9.91  where
    9.92    "ldoProofStep (Conflict saveTo (i, rs)) (xs, rcl) =
    9.93       (case (xs ! i) of
    9.94 -       None \<Rightarrow> raise (''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'')
    9.95 +       None \<Rightarrow> raise STR ''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.''
    9.96       | Some cli \<Rightarrow> do {
    9.97                        result \<leftarrow> foldM (lres_thm xs) rs cli ;
    9.98                        return ((xs[saveTo:=Some result]), rcl)
    9.99                     })"
   9.100  | "ldoProofStep (Delete cid) (xs, rcl) = return (xs[cid:=None], rcl)"
   9.101  | "ldoProofStep (Root cid clause) (xs, rcl) = return (xs[cid:=Some (sort clause)], (remdups(sort clause)) # rcl)"
   9.102 -| "ldoProofStep (Xstep cid1 cid2) (xs, rcl) = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''"
   9.103 -| "ldoProofStep (ProofDone b) (xs, rcl) = raise ''MiniSatChecked.doProofStep: ProofDone constructor found.''"
   9.104 +| "ldoProofStep (Xstep cid1 cid2) (xs, rcl) = raise STR ''MiniSatChecked.doProofStep: Xstep constructor found.''"
   9.105 +| "ldoProofStep (ProofDone b) (xs, rcl) = raise STR ''MiniSatChecked.doProofStep: ProofDone constructor found.''"
   9.106  
   9.107  definition lchecker :: "nat \<Rightarrow> ProofStep list \<Rightarrow> nat \<Rightarrow> Clause list Heap"
   9.108  where
   9.109 @@ -666,7 +666,7 @@
   9.110    do {
   9.111       rcs \<leftarrow> foldM (ldoProofStep) p ([], []);
   9.112       (if (fst rcs ! i) = Some [] then return (snd rcs) 
   9.113 -                else raise(''No empty clause''))
   9.114 +                else raise STR ''No empty clause'')
   9.115    }"
   9.116  
   9.117  
   9.118 @@ -676,22 +676,22 @@
   9.119  where
   9.120    "tres_thm t (l, j) cli =
   9.121    (case (rbt_lookup t j) of 
   9.122 -     None \<Rightarrow> raise (''MiniSatChecked.res_thm: No resolvant clause in thms array for Conflict step.'')
   9.123 +     None \<Rightarrow> raise STR ''MiniSatChecked.res_thm: No resolvant clause in thms array for Conflict step.''
   9.124     | Some clj \<Rightarrow> res_thm' l cli clj)"
   9.125  
   9.126  fun tdoProofStep :: " ProofStep \<Rightarrow> ((ClauseId, Clause) RBT_Impl.rbt * Clause list) \<Rightarrow> ((ClauseId, Clause) RBT_Impl.rbt * Clause list) Heap"
   9.127  where
   9.128    "tdoProofStep (Conflict saveTo (i, rs)) (t, rcl) =
   9.129       (case (rbt_lookup t i) of
   9.130 -       None \<Rightarrow> raise (''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'')
   9.131 +       None \<Rightarrow> raise STR ''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.''
   9.132       | Some cli \<Rightarrow> do {
   9.133                        result \<leftarrow> foldM (tres_thm t) rs cli;
   9.134                        return ((rbt_insert saveTo result t), rcl)
   9.135                     })"
   9.136  | "tdoProofStep (Delete cid) (t, rcl) = return ((rbt_delete cid t), rcl)"
   9.137  | "tdoProofStep (Root cid clause) (t, rcl) = return (rbt_insert cid (sort clause) t, (remdups(sort clause)) # rcl)"
   9.138 -| "tdoProofStep (Xstep cid1 cid2) (t, rcl) = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''"
   9.139 -| "tdoProofStep (ProofDone b) (t, rcl) = raise ''MiniSatChecked.doProofStep: ProofDone constructor found.''"
   9.140 +| "tdoProofStep (Xstep cid1 cid2) (t, rcl) = raise STR ''MiniSatChecked.doProofStep: Xstep constructor found.''"
   9.141 +| "tdoProofStep (ProofDone b) (t, rcl) = raise STR ''MiniSatChecked.doProofStep: ProofDone constructor found.''"
   9.142  
   9.143  definition tchecker :: "nat \<Rightarrow> ProofStep list \<Rightarrow> nat \<Rightarrow> Clause list Heap"
   9.144  where
   9.145 @@ -699,7 +699,7 @@
   9.146    do {
   9.147       rcs \<leftarrow> foldM (tdoProofStep) p (RBT_Impl.Empty, []);
   9.148       (if (rbt_lookup (fst rcs) i) = Some [] then return (snd rcs) 
   9.149 -                else raise(''No empty clause''))
   9.150 +                else raise STR ''No empty clause'')
   9.151    }"
   9.152  
   9.153  export_code checker tchecker lchecker checking SML
    10.1 --- a/src/HOL/Library/Cardinality.thy	Tue Apr 24 14:17:57 2018 +0000
    10.2 +++ b/src/HOL/Library/Cardinality.thy	Tue Apr 24 14:17:58 2018 +0000
    10.3 @@ -27,12 +27,6 @@
    10.4  lemma (in type_definition) card: "card (UNIV :: 'b set) = card A"
    10.5    by (simp add: univ card_image inj_on_def Abs_inject)
    10.6  
    10.7 -lemma infinite_literal: "\<not> finite (UNIV :: String.literal set)"
    10.8 -proof -
    10.9 -  have "inj STR" by(auto intro: injI)
   10.10 -  thus ?thesis
   10.11 -    by(auto simp add: type_definition.univ[OF type_definition_literal] infinite_UNIV_listI dest: finite_imageD)
   10.12 -qed
   10.13  
   10.14  subsection \<open>Cardinalities of types\<close>
   10.15  
    11.1 --- a/src/HOL/Library/Char_ord.thy	Tue Apr 24 14:17:57 2018 +0000
    11.2 +++ b/src/HOL/Library/Char_ord.thy	Tue Apr 24 14:17:58 2018 +0000
    11.3 @@ -11,27 +11,29 @@
    11.4  instantiation char :: linorder
    11.5  begin
    11.6  
    11.7 -definition "c1 \<le> c2 \<longleftrightarrow> nat_of_char c1 \<le> nat_of_char c2"
    11.8 -definition "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2"
    11.9 +definition less_eq_char :: "char \<Rightarrow> char \<Rightarrow> bool"
   11.10 +  where "c1 \<le> c2 \<longleftrightarrow> of_char c1 \<le> (of_char c2 :: nat)"
   11.11 +
   11.12 +definition less_char :: "char \<Rightarrow> char \<Rightarrow> bool"
   11.13 +  where "c1 < c2 \<longleftrightarrow> of_char c1 < (of_char c2 :: nat)"
   11.14 +
   11.15  
   11.16  instance
   11.17    by standard (auto simp add: less_eq_char_def less_char_def)
   11.18  
   11.19  end
   11.20  
   11.21 -lemma less_eq_char_simps:
   11.22 -  "0 \<le> c"
   11.23 -  "Char k \<le> 0 \<longleftrightarrow> numeral k mod 256 = (0 :: nat)"
   11.24 -  "Char k \<le> Char l \<longleftrightarrow> numeral k mod 256 \<le> (numeral l mod 256 :: nat)"
   11.25 -  for c :: char
   11.26 -  by (simp_all add: Char_def less_eq_char_def)
   11.27 +lemma less_eq_char_simp [simp]:
   11.28 +  "Char b0 b1 b2 b3 b4 b5 b6 b7 \<le> Char c0 c1 c2 c3 c4 c5 c6 c7
   11.29 +    \<longleftrightarrow> foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0
   11.30 +      \<le> foldr (\<lambda>b k. of_bool b + k * 2) [c0, c1, c2, c3, c4, c5, c6, c7] (0::nat)"
   11.31 +  by (simp add: less_eq_char_def)
   11.32  
   11.33 -lemma less_char_simps:
   11.34 -  "\<not> c < 0"
   11.35 -  "0 < Char k \<longleftrightarrow> (0 :: nat) < numeral k mod 256"
   11.36 -  "Char k < Char l \<longleftrightarrow> numeral k mod 256 < (numeral l mod 256 :: nat)"
   11.37 -  for c :: char
   11.38 -  by (simp_all add: Char_def less_char_def)
   11.39 +lemma less_char_simp [simp]:
   11.40 +  "Char b0 b1 b2 b3 b4 b5 b6 b7 < Char c0 c1 c2 c3 c4 c5 c6 c7
   11.41 +    \<longleftrightarrow> foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0
   11.42 +      < foldr (\<lambda>b k. of_bool b + k * 2) [c0, c1, c2, c3, c4, c5, c6, c7] (0::nat)"
   11.43 +  by (simp add: less_char_def)
   11.44  
   11.45  instantiation char :: distrib_lattice
   11.46  begin
   11.47 @@ -44,39 +46,4 @@
   11.48  
   11.49  end
   11.50  
   11.51 -instantiation String.literal :: linorder
   11.52 -begin
   11.53 -
   11.54 -context includes literal.lifting
   11.55 -begin
   11.56 -
   11.57 -lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
   11.58 -  is "ord.lexordp (<)" .
   11.59 -
   11.60 -lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
   11.61 -  is "ord.lexordp_eq (<)" .
   11.62 -
   11.63 -instance
   11.64 -proof -
   11.65 -  interpret linorder "ord.lexordp_eq (<)" "ord.lexordp (<) :: string \<Rightarrow> string \<Rightarrow> bool"
   11.66 -    by (rule linorder.lexordp_linorder[where less_eq="(\<le>)"]) unfold_locales
   11.67 -  show "PROP ?thesis"
   11.68 -    by intro_classes (transfer, simp add: less_le_not_le linear)+
   11.69 -qed
   11.70 -
   11.71  end
   11.72 -
   11.73 -end
   11.74 -
   11.75 -lemma less_literal_code [code]:
   11.76 -  "(<) = (\<lambda>xs ys. ord.lexordp (<) (String.explode xs) (String.explode ys))"
   11.77 -  by (simp add: less_literal.rep_eq fun_eq_iff)
   11.78 -
   11.79 -lemma less_eq_literal_code [code]:
   11.80 -  "(\<le>) = (\<lambda>xs ys. ord.lexordp_eq (<) (String.explode xs) (String.explode ys))"
   11.81 -  by (simp add: less_eq_literal.rep_eq fun_eq_iff)
   11.82 -
   11.83 -lifting_update literal.lifting
   11.84 -lifting_forget literal.lifting
   11.85 -
   11.86 -end
    12.1 --- a/src/HOL/Library/Code_Char.thy	Tue Apr 24 14:17:57 2018 +0000
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,96 +0,0 @@
    12.4 -(*  Title:      HOL/Library/Code_Char.thy
    12.5 -    Author:     Florian Haftmann
    12.6 -*)
    12.7 -
    12.8 -section \<open>Code generation of pretty characters (and strings)\<close>
    12.9 -
   12.10 -theory Code_Char
   12.11 -imports Main Char_ord
   12.12 -begin
   12.13 -
   12.14 -code_printing
   12.15 -  type_constructor char \<rightharpoonup>
   12.16 -    (SML) "char"
   12.17 -    and (OCaml) "char"
   12.18 -    and (Haskell) "Prelude.Char"
   12.19 -    and (Scala) "Char"
   12.20 -
   12.21 -setup \<open>
   12.22 -  fold String_Code.add_literal_char ["SML", "OCaml", "Haskell", "Scala"]
   12.23 -  #> String_Code.add_literal_list_string "Haskell"
   12.24 -\<close>
   12.25 -
   12.26 -code_printing
   12.27 -  constant integer_of_char \<rightharpoonup>
   12.28 -    (SML) "!(IntInf.fromInt o Char.ord)"
   12.29 -    and (OCaml) "Big'_int.big'_int'_of'_int (Char.code _)"
   12.30 -    and (Haskell) "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))"
   12.31 -    and (Scala) "BigInt(_.toInt)"
   12.32 -| constant char_of_integer \<rightharpoonup>
   12.33 -    (SML) "!(Char.chr o IntInf.toInt)"
   12.34 -    and (OCaml) "Char.chr (Big'_int.int'_of'_big'_int _)"
   12.35 -    and (Haskell) "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)"
   12.36 -    and (Scala) "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else sys.error(\"character value out of range\"))"
   12.37 -| class_instance char :: equal \<rightharpoonup>
   12.38 -    (Haskell) -
   12.39 -| constant "HOL.equal :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
   12.40 -    (SML) "!((_ : char) = _)"
   12.41 -    and (OCaml) "!((_ : char) = _)"
   12.42 -    and (Haskell) infix 4 "=="
   12.43 -    and (Scala) infixl 5 "=="
   12.44 -| constant "Code_Evaluation.term_of :: char \<Rightarrow> term" \<rightharpoonup>
   12.45 -    (Eval) "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))"
   12.46 -
   12.47 -code_reserved SML
   12.48 -  char
   12.49 -
   12.50 -code_reserved OCaml
   12.51 -  char
   12.52 -
   12.53 -code_reserved Scala
   12.54 -  char
   12.55 -
   12.56 -code_reserved SML String
   12.57 -
   12.58 -code_printing
   12.59 -  constant String.implode \<rightharpoonup>
   12.60 -    (SML) "String.implode"
   12.61 -    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)"
   12.62 -    and (Haskell) "_"
   12.63 -    and (Scala) "!(\"\" ++/ _)"
   12.64 -| constant String.explode \<rightharpoonup>
   12.65 -    (SML) "String.explode"
   12.66 -    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) [])"
   12.67 -    and (Haskell) "_"
   12.68 -    and (Scala) "!(_.toList)"
   12.69 -
   12.70 -code_printing
   12.71 -  constant "Orderings.less_eq :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
   12.72 -    (SML) "!((_ : char) <= _)"
   12.73 -    and (OCaml) "!((_ : char) <= _)"
   12.74 -    and (Haskell) infix 4 "<="
   12.75 -    and (Scala) infixl 4 "<="
   12.76 -    and (Eval) infixl 6 "<="
   12.77 -| constant "Orderings.less :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
   12.78 -    (SML) "!((_ : char) < _)"
   12.79 -    and (OCaml) "!((_ : char) < _)"
   12.80 -    and (Haskell) infix 4 "<"
   12.81 -    and (Scala) infixl 4 "<"
   12.82 -    and (Eval) infixl 6 "<"
   12.83 -|  constant "Orderings.less_eq :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
   12.84 -    (SML) "!((_ : string) <= _)"
   12.85 -    and (OCaml) "!((_ : string) <= _)"
   12.86 -    \<comment> \<open>Order operations for @{typ String.literal} work in Haskell only
   12.87 -          if no type class instance needs to be generated, because String = [Char] in Haskell
   12.88 -          and @{typ "char list"} need not have the same order as @{typ String.literal}.\<close>
   12.89 -    and (Haskell) infix 4 "<="
   12.90 -    and (Scala) infixl 4 "<="
   12.91 -    and (Eval) infixl 6 "<="
   12.92 -| constant "Orderings.less :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
   12.93 -    (SML) "!((_ : string) < _)"
   12.94 -    and (OCaml) "!((_ : string) < _)"
   12.95 -    and (Haskell) infix 4 "<"
   12.96 -    and (Scala) infixl 4 "<"
   12.97 -    and (Eval) infixl 6 "<"
   12.98 -
   12.99 -end
    13.1 --- a/src/HOL/Library/Code_Target_Int.thy	Tue Apr 24 14:17:57 2018 +0000
    13.2 +++ b/src/HOL/Library/Code_Target_Int.thy	Tue Apr 24 14:17:58 2018 +0000
    13.3 @@ -143,6 +143,22 @@
    13.4    "nat = nat_of_integer \<circ> of_int"
    13.5    including integer.lifting by transfer (simp add: fun_eq_iff)
    13.6  
    13.7 +definition char_of_int :: "int \<Rightarrow> char"
    13.8 +  where [code_abbrev]: "char_of_int = char_of"
    13.9 +
   13.10 +definition int_of_char :: "char \<Rightarrow> int"
   13.11 +  where [code_abbrev]: "int_of_char = of_char"
   13.12 +
   13.13 +lemma [code]:
   13.14 +  "char_of_int = char_of_integer \<circ> integer_of_int"
   13.15 +  including integer.lifting unfolding char_of_integer_def char_of_int_def
   13.16 +  by transfer (simp add: fun_eq_iff)
   13.17 +
   13.18 +lemma [code]:
   13.19 +  "int_of_char = int_of_integer \<circ> integer_of_char"
   13.20 +  including integer.lifting unfolding integer_of_char_def int_of_char_def
   13.21 +  by transfer (simp add: fun_eq_iff)
   13.22 +
   13.23  code_identifier
   13.24    code_module Code_Target_Int \<rightharpoonup>
   13.25      (SML) Arith and (OCaml) Arith and (Haskell) Arith
    14.1 --- a/src/HOL/Library/Code_Target_Nat.thy	Tue Apr 24 14:17:57 2018 +0000
    14.2 +++ b/src/HOL/Library/Code_Target_Nat.thy	Tue Apr 24 14:17:58 2018 +0000
    14.3 @@ -147,6 +147,21 @@
    14.4    "integer_of_nat (nat k) = max 0 (integer_of_int k)"
    14.5    including integer.lifting by transfer auto
    14.6  
    14.7 +definition char_of_nat :: "nat \<Rightarrow> char"
    14.8 +  where [code_abbrev]: "char_of_nat = char_of"
    14.9 +
   14.10 +definition nat_of_char :: "char \<Rightarrow> nat"
   14.11 +  where [code_abbrev]: "nat_of_char = of_char"
   14.12 +
   14.13 +lemma [code]:
   14.14 +  "char_of_nat = char_of_integer \<circ> integer_of_nat"
   14.15 +  including integer.lifting unfolding char_of_integer_def char_of_nat_def
   14.16 +  by transfer (simp add: fun_eq_iff)
   14.17 +
   14.18 +lemma [code abstract]:
   14.19 +  "integer_of_nat (nat_of_char c) = integer_of_char c"
   14.20 +  by (cases c) (simp add: nat_of_char_def integer_of_char_def integer_of_nat_eq_of_nat)
   14.21 +
   14.22  lemma term_of_nat_code [code]:
   14.23    \<comment> \<open>Use @{term Code_Numeral.nat_of_integer} in term reconstruction
   14.24          instead of @{term Code_Target_Nat.Nat} such that reconstructed
    15.1 --- a/src/HOL/Library/Code_Test.thy	Tue Apr 24 14:17:57 2018 +0000
    15.2 +++ b/src/HOL/Library/Code_Test.thy	Tue Apr 24 14:17:58 2018 +0000
    15.3 @@ -84,8 +84,8 @@
    15.4  
    15.5  definition list where "list f xs = map (node \<circ> f) xs"
    15.6  
    15.7 -definition X :: yxml_of_term where "X = yot_literal (STR [Char (num.Bit1 (num.Bit0 num.One))])"
    15.8 -definition Y :: yxml_of_term where "Y = yot_literal (STR [Char (num.Bit0 (num.Bit1 num.One))])"
    15.9 +definition X :: yxml_of_term where "X = yot_literal (ASCII 0x05)"
   15.10 +definition Y :: yxml_of_term where "Y = yot_literal (ASCII 0x06)"
   15.11  definition XY :: yxml_of_term where "XY = yot_append X Y"
   15.12  definition XYX :: yxml_of_term where "XYX = yot_append XY X"
   15.13  
    16.1 --- a/src/HOL/Library/Countable.thy	Tue Apr 24 14:17:57 2018 +0000
    16.2 +++ b/src/HOL/Library/Countable.thy	Tue Apr 24 14:17:58 2018 +0000
    16.3 @@ -256,7 +256,7 @@
    16.4  text \<open>String literals\<close>
    16.5  
    16.6  instance String.literal :: countable
    16.7 -  by (rule countable_classI [of "to_nat \<circ> String.explode"]) (auto simp add: explode_inject)
    16.8 +  by (rule countable_classI [of "to_nat \<circ> String.explode"]) (simp add: String.explode_inject)
    16.9  
   16.10  text \<open>Functions\<close>
   16.11  
    17.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Tue Apr 24 14:17:57 2018 +0000
    17.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Tue Apr 24 14:17:58 2018 +0000
    17.3 @@ -244,7 +244,7 @@
    17.4  
    17.5  section \<open>Setup for String.literal\<close>
    17.6  
    17.7 -setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name "STR"}]\<close>
    17.8 +setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name String.Literal}]\<close>
    17.9  
   17.10  section \<open>Simplification rules for optimisation\<close>
   17.11  
    18.1 --- a/src/HOL/List.thy	Tue Apr 24 14:17:57 2018 +0000
    18.2 +++ b/src/HOL/List.thy	Tue Apr 24 14:17:58 2018 +0000
    18.3 @@ -6980,10 +6980,6 @@
    18.4  
    18.5  signature LIST_CODE =
    18.6  sig
    18.7 -  val implode_list: Code_Thingol.iterm -> Code_Thingol.iterm list option
    18.8 -  val default_list: int * string
    18.9 -    -> (Code_Printer.fixity -> Code_Thingol.iterm -> Pretty.T)
   18.10 -    -> Code_Printer.fixity -> Code_Thingol.iterm -> Code_Thingol.iterm -> Pretty.T
   18.11    val add_literal_list: string -> theory -> theory
   18.12  end;
   18.13  
   18.14 @@ -7002,7 +6998,7 @@
   18.15      | _ => NONE
   18.16    end;
   18.17  
   18.18 -fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
   18.19 +fun print_list (target_fxy, target_cons) pr fxy t1 t2 =
   18.20    Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy (
   18.21      pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
   18.22      Code_Printer.str target_cons,
   18.23 @@ -7016,7 +7012,7 @@
   18.24         of SOME ts =>
   18.25              Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
   18.26          | NONE =>
   18.27 -            default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
   18.28 +            print_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
   18.29    in
   18.30      Code_Target.set_printings (Code_Symbol.Constant (@{const_name Cons},
   18.31        [(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))]))
    19.1 --- a/src/HOL/Parity.thy	Tue Apr 24 14:17:57 2018 +0000
    19.2 +++ b/src/HOL/Parity.thy	Tue Apr 24 14:17:58 2018 +0000
    19.3 @@ -407,6 +407,18 @@
    19.4      by (simp add: div_mult2_eq' mult_commute)
    19.5  qed
    19.6  
    19.7 +lemma div_mult2_numeral_eq:
    19.8 +  "a div numeral k div numeral l = a div numeral (k * l)" (is "?A = ?B")
    19.9 +proof -
   19.10 +  have "?A = a div of_nat (numeral k) div of_nat (numeral l)"
   19.11 +    by simp
   19.12 +  also have "\<dots> = a div (of_nat (numeral k) * of_nat (numeral l))"
   19.13 +    by (fact div_mult2_eq' [symmetric])
   19.14 +  also have "\<dots> = ?B"
   19.15 +    by simp
   19.16 +  finally show ?thesis .
   19.17 +qed
   19.18 +
   19.19  end
   19.20  
   19.21  class ring_parity = ring + semiring_parity
    20.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Tue Apr 24 14:17:57 2018 +0000
    20.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Tue Apr 24 14:17:58 2018 +0000
    20.3 @@ -714,24 +714,6 @@
    20.4  
    20.5  ML_file "Tools/Quickcheck/abstract_generators.ML"
    20.6  
    20.7 -instantiation char :: full_exhaustive
    20.8 -begin
    20.9 -
   20.10 -definition full_exhaustive_char
   20.11 -where
   20.12 -  "full_exhaustive_char f i =
   20.13 -     (if 0 < i then
   20.14 -      case f (0, \<lambda>_ :: unit. Code_Evaluation.Const (STR ''Groups.zero_class.zero'') (TYPEREP(char))) of
   20.15 -          Some x \<Rightarrow> Some x
   20.16 -      | None \<Rightarrow> full_exhaustive_class.full_exhaustive
   20.17 -          (\<lambda>(num, t). f (char_of_nat (nat_of_num num), \<lambda>_ :: unit. Code_Evaluation.App (Code_Evaluation.Const (STR ''String.Char'') TYPEREP(num \<Rightarrow> char)) (t ())))
   20.18 -          (min (i - 1) 8) \<comment> \<open>generate at most 8 bits\<close>
   20.19 -      else None)"
   20.20 -
   20.21 -instance ..
   20.22 -
   20.23 -end
   20.24 -
   20.25  hide_fact (open) orelse_def
   20.26  no_notation orelse  (infixr "orelse" 55)
   20.27  
    21.1 --- a/src/HOL/ROOT	Tue Apr 24 14:17:57 2018 +0000
    21.2 +++ b/src/HOL/ROOT	Tue Apr 24 14:17:58 2018 +0000
    21.3 @@ -39,7 +39,6 @@
    21.4      (*data refinements and dependent applications*)
    21.5      AList_Mapping
    21.6      Code_Binary_Nat
    21.7 -    Code_Char
    21.8      Code_Prolog
    21.9      Code_Real_Approx_By_Float
   21.10      Code_Target_Numeral
   21.11 @@ -248,7 +247,6 @@
   21.12      Generate_Binary_Nat
   21.13      Generate_Target_Nat
   21.14      Generate_Efficient_Datastructures
   21.15 -    Generate_Pretty_Char
   21.16      Code_Test_PolyML
   21.17      Code_Test_Scala
   21.18    theories [condition = ISABELLE_GHC]
    22.1 --- a/src/HOL/Statespace/state_fun.ML	Tue Apr 24 14:17:57 2018 +0000
    22.2 +++ b/src/HOL/Statespace/state_fun.ML	Tue Apr 24 14:17:58 2018 +0000
    22.3 @@ -76,7 +76,7 @@
    22.4  
    22.5  fun string_eq_simp_tac ctxt =
    22.6    simp_tac (put_simpset HOL_basic_ss ctxt
    22.7 -    addsimps @{thms list.inject list.distinct Char_eq_Char_iff
    22.8 +    addsimps @{thms list.inject list.distinct char.inject
    22.9        cong_exp_iff_simps simp_thms}
   22.10      addsimprocs [lazy_conj_simproc]
   22.11      |> Simplifier.add_cong @{thm block_conj_cong});
   22.12 @@ -85,7 +85,7 @@
   22.13  
   22.14  val lookup_ss =
   22.15    simpset_of (put_simpset HOL_basic_ss @{context}
   22.16 -    addsimps (@{thms list.inject} @ @{thms Char_eq_Char_iff}
   22.17 +    addsimps (@{thms list.inject} @ @{thms char.inject}
   22.18        @ @{thms list.distinct} @ @{thms simp_thms}
   22.19        @ [@{thm StateFun.lookup_update_id_same}, @{thm StateFun.id_id_cancel},
   22.20          @{thm StateFun.lookup_update_same}, @{thm StateFun.lookup_update_other}])
   22.21 @@ -161,7 +161,7 @@
   22.22  val meta_ext = @{thm StateFun.meta_ext};
   22.23  val ss' =
   22.24    simpset_of (put_simpset HOL_ss @{context} addsimps
   22.25 -    (@{thm StateFun.update_apply} :: @{thm Fun.o_apply} :: @{thms list.inject} @ @{thms Char_eq_Char_iff}
   22.26 +    (@{thm StateFun.update_apply} :: @{thm Fun.o_apply} :: @{thms list.inject} @ @{thms char.inject}
   22.27        @ @{thms list.distinct})
   22.28      addsimprocs [lazy_conj_simproc, StateSpace.distinct_simproc]
   22.29      |> fold Simplifier.add_cong @{thms block_conj_cong});
    23.1 --- a/src/HOL/String.thy	Tue Apr 24 14:17:57 2018 +0000
    23.2 +++ b/src/HOL/String.thy	Tue Apr 24 14:17:58 2018 +0000
    23.3 @@ -6,191 +6,190 @@
    23.4  imports Enum
    23.5  begin
    23.6  
    23.7 -subsection \<open>Characters and strings\<close>
    23.8 +subsection \<open>Strings as list of bytes\<close>
    23.9 +
   23.10 +text \<open>
   23.11 +  When modelling strings, we follow the approach given
   23.12 +  in @{url "http://utf8everywhere.org/"}:
   23.13 +
   23.14 +  \<^item> Strings are a list of bytes (8 bit).
   23.15 +
   23.16 +  \<^item> Byte values from 0 to 127 are US-ASCII.
   23.17  
   23.18 -subsubsection \<open>Characters as finite algebraic type\<close>
   23.19 +  \<^item> Byte values from 128 to 255 are uninterpreted blobs.
   23.20 +\<close>
   23.21 +
   23.22 +subsubsection \<open>Bytes as datatype\<close>
   23.23 +
   23.24 +datatype char =
   23.25 +  Char (digit0: bool) (digit1: bool) (digit2: bool) (digit3: bool)
   23.26 +       (digit4: bool) (digit5: bool) (digit6: bool) (digit7: bool)
   23.27 +
   23.28 +context comm_semiring_1
   23.29 +begin
   23.30  
   23.31 -typedef char = "{n::nat. n < 256}"
   23.32 -  morphisms nat_of_char Abs_char
   23.33 -proof
   23.34 -  show "Suc 0 \<in> {n. n < 256}" by simp
   23.35 +definition of_char :: "char \<Rightarrow> 'a"
   23.36 +  where "of_char c = ((((((of_bool (digit7 c) * 2
   23.37 +    + of_bool (digit6 c)) * 2
   23.38 +    + of_bool (digit5 c)) * 2
   23.39 +    + of_bool (digit4 c)) * 2
   23.40 +    + of_bool (digit3 c)) * 2
   23.41 +    + of_bool (digit2 c)) * 2
   23.42 +    + of_bool (digit1 c)) * 2
   23.43 +    + of_bool (digit0 c)"
   23.44 +
   23.45 +lemma of_char_Char [simp]:
   23.46 +  "of_char (Char b0 b1 b2 b3 b4 b5 b6 b7) =
   23.47 +    foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0"
   23.48 +  by (simp add: of_char_def ac_simps)
   23.49 +
   23.50 +end
   23.51 +
   23.52 +context semiring_parity
   23.53 +begin
   23.54 +
   23.55 +definition char_of :: "'a \<Rightarrow> char"
   23.56 +  where "char_of n = Char (odd n) (odd (drop_bit 1 n))
   23.57 +    (odd (drop_bit 2 n)) (odd (drop_bit 3 n))
   23.58 +    (odd (drop_bit 4 n)) (odd (drop_bit 5 n))
   23.59 +    (odd (drop_bit 6 n)) (odd (drop_bit 7 n))"
   23.60 +
   23.61 +lemma char_of_char [simp]:
   23.62 +  "char_of (of_char c) = c"
   23.63 +proof (cases c)
   23.64 +  have **: "drop_bit n (q * 2 + of_bool d) = drop_bit (n - 1) q + drop_bit n (of_bool d)"
   23.65 +    if "n > 0" for q :: 'a and n :: nat and d :: bool
   23.66 +    using that by (cases n) simp_all
   23.67 +  case (Char d0 d1 d2 d3 d4 d5 d6 d7)
   23.68 +  then show ?thesis
   23.69 +    by (simp only: of_char_def char_of_def char.simps char.sel drop_bit_of_bool **) simp
   23.70  qed
   23.71  
   23.72 -setup_lifting type_definition_char
   23.73 -
   23.74 -definition char_of_nat :: "nat \<Rightarrow> char"
   23.75 -where
   23.76 -  "char_of_nat n = Abs_char (n mod 256)"
   23.77 +lemma char_of_comp_of_char [simp]:
   23.78 +  "char_of \<circ> of_char = id"
   23.79 +  by (simp add: fun_eq_iff)
   23.80  
   23.81 -lemma char_cases [case_names char_of_nat, cases type: char]:
   23.82 -  "(\<And>n. c = char_of_nat n \<Longrightarrow> n < 256 \<Longrightarrow> P) \<Longrightarrow> P"
   23.83 -  by (cases c) (simp add: char_of_nat_def)
   23.84 -
   23.85 -lemma char_of_nat_of_char [simp]:
   23.86 -  "char_of_nat (nat_of_char c) = c"
   23.87 -  by (cases c) (simp add: char_of_nat_def Abs_char_inject Abs_char_inverse)
   23.88 -
   23.89 -lemma inj_nat_of_char:
   23.90 -  "inj nat_of_char"
   23.91 +lemma inj_of_char:
   23.92 +  "inj of_char"
   23.93  proof (rule injI)
   23.94    fix c d
   23.95 -  assume "nat_of_char c = nat_of_char d"
   23.96 -  then have "char_of_nat (nat_of_char c) = char_of_nat (nat_of_char d)"
   23.97 +  assume "of_char c = of_char d"
   23.98 +  then have "char_of (of_char c) = char_of (of_char d)"
   23.99      by simp
  23.100    then show "c = d"
  23.101      by simp
  23.102  qed
  23.103    
  23.104 -lemma nat_of_char_eq_iff [simp]:
  23.105 -  "nat_of_char c = nat_of_char d \<longleftrightarrow> c = d"
  23.106 -  by (fact nat_of_char_inject)
  23.107 +lemma of_char_eq_iff [simp]:
  23.108 +  "of_char c = of_char d \<longleftrightarrow> c = d"
  23.109 +  by (simp add: inj_eq inj_of_char)
  23.110  
  23.111 -lemma nat_of_char_of_nat [simp]:
  23.112 -  "nat_of_char (char_of_nat n) = n mod 256"
  23.113 -  by (cases "char_of_nat n") (simp add: char_of_nat_def Abs_char_inject Abs_char_inverse)
  23.114 +lemma of_char_of [simp]:
  23.115 +  "of_char (char_of a) = a mod 256"
  23.116 +proof -
  23.117 +  have *: "{0::nat..<8} = {0, 1, 2, 3, 4, 5, 6, 7}"
  23.118 +    by auto
  23.119 +  have "of_char (char_of (take_bit 8 a)) =
  23.120 +    (\<Sum>k\<in>{0, 1, 2, 3, 4, 5, 6, 7}. push_bit k (of_bool (odd (drop_bit k a))))"
  23.121 +    by (simp add: of_char_def char_of_def push_bit_of_1 drop_bit_take_bit)
  23.122 +  also have "\<dots> = take_bit 8 a"
  23.123 +    using * take_bit_sum [of 8 a] by simp
  23.124 +  also have "char_of(take_bit 8 a) = char_of a"
  23.125 +    by (simp add: char_of_def drop_bit_take_bit)
  23.126 +  finally show ?thesis
  23.127 +    by (simp add: take_bit_eq_mod)
  23.128 +qed
  23.129  
  23.130 -lemma char_of_nat_mod_256 [simp]:
  23.131 -  "char_of_nat (n mod 256) = char_of_nat n"
  23.132 -  by (cases "char_of_nat (n mod 256)") (simp add: char_of_nat_def)
  23.133 +lemma char_of_mod_256 [simp]:
  23.134 +  "char_of (n mod 256) = char_of n"
  23.135 +  by (metis char_of_char of_char_of)
  23.136 +
  23.137 +lemma of_char_mod_256 [simp]:
  23.138 +  "of_char c mod 256 = of_char c"
  23.139 +  by (metis char_of_char of_char_of)
  23.140  
  23.141 -lemma char_of_nat_quasi_inj [simp]:
  23.142 -  "char_of_nat m = char_of_nat n \<longleftrightarrow> m mod 256 = n mod 256"
  23.143 -  by (simp add: char_of_nat_def Abs_char_inject)
  23.144 +lemma char_of_quasi_inj [simp]:
  23.145 +  "char_of m = char_of n \<longleftrightarrow> m mod 256 = n mod 256"
  23.146 +  by (metis char_of_mod_256 of_char_of)
  23.147 +
  23.148 +lemma char_of_nat_eq_iff:
  23.149 +  "char_of n = c \<longleftrightarrow> take_bit 8 n = of_char c"
  23.150 +  by (simp add: take_bit_eq_mod) (use of_char_eq_iff in fastforce)
  23.151 +
  23.152 +lemma char_of_nat [simp]:
  23.153 +  "char_of (of_nat n) = char_of n"
  23.154 +  by (simp add: char_of_def String.char_of_def drop_bit_of_nat)
  23.155 +	
  23.156 +end
  23.157  
  23.158  lemma inj_on_char_of_nat [simp]:
  23.159 -  "inj_on char_of_nat {..<256}"
  23.160 +  "inj_on char_of {0::nat..<256}"
  23.161    by (rule inj_onI) simp
  23.162  
  23.163 -lemma nat_of_char_mod_256 [simp]:
  23.164 -  "nat_of_char c mod 256 = nat_of_char c"
  23.165 -  by (cases c) simp
  23.166 -
  23.167  lemma nat_of_char_less_256 [simp]:
  23.168 -  "nat_of_char c < 256"
  23.169 +  "of_char c < (256 :: nat)"
  23.170  proof -
  23.171 -  have "nat_of_char c mod 256 < 256"
  23.172 +  have "of_char c mod (256 :: nat) < 256"
  23.173      by arith
  23.174    then show ?thesis by simp
  23.175  qed
  23.176  
  23.177 +lemma range_nat_of_char:
  23.178 +  "range of_char = {0::nat..<256}"
  23.179 +proof (rule; rule)
  23.180 +  fix n :: nat
  23.181 +  assume "n \<in> range of_char"
  23.182 +  then show "n \<in> {0..<256}"
  23.183 +    by auto
  23.184 +next
  23.185 +  fix n :: nat
  23.186 +  assume "n \<in> {0..<256}"
  23.187 +  then have "n = of_char (char_of n)"
  23.188 +    by simp
  23.189 +  then show "n \<in> range of_char"
  23.190 +    by (rule range_eqI)
  23.191 +qed
  23.192 +
  23.193  lemma UNIV_char_of_nat:
  23.194 -  "UNIV = char_of_nat ` {..<256}"
  23.195 +  "UNIV = char_of ` {0::nat..<256}"
  23.196  proof -
  23.197 -  { fix c
  23.198 -    have "c \<in> char_of_nat ` {..<256}"
  23.199 -      by (cases c) auto
  23.200 -  } then show ?thesis by auto
  23.201 +  have "range (of_char :: char \<Rightarrow> nat) = of_char ` char_of ` {0::nat..<256}"
  23.202 +    by (auto simp add: range_nat_of_char intro!: image_eqI)
  23.203 +  with inj_of_char [where ?'a = nat] show ?thesis 
  23.204 +    by (simp add: inj_image_eq_iff)
  23.205  qed
  23.206  
  23.207  lemma card_UNIV_char:
  23.208    "card (UNIV :: char set) = 256"
  23.209    by (auto simp add: UNIV_char_of_nat card_image)
  23.210  
  23.211 -lemma range_nat_of_char:
  23.212 -  "range nat_of_char = {..<256}"
  23.213 -  by (auto simp add: UNIV_char_of_nat image_image image_def)
  23.214 -
  23.215 -
  23.216 -subsubsection \<open>Character literals as variant of numerals\<close>
  23.217 -
  23.218 -instantiation char :: zero
  23.219 +context
  23.220 +  includes lifting_syntax integer.lifting natural.lifting
  23.221  begin
  23.222  
  23.223 -definition zero_char :: char
  23.224 -  where "0 = char_of_nat 0"
  23.225 +lemma [transfer_rule]:
  23.226 +  "(pcr_integer ===> (=)) (char_of :: int \<Rightarrow> char) (char_of :: integer \<Rightarrow> char)"
  23.227 +  by (unfold char_of_def [abs_def]) transfer_prover
  23.228 +
  23.229 +lemma [transfer_rule]:
  23.230 +  "((=) ===> pcr_integer) (of_char :: char \<Rightarrow> int) (of_char :: char \<Rightarrow> integer)"
  23.231 +  by (unfold of_char_def [abs_def]) transfer_prover
  23.232  
  23.233 -instance ..
  23.234 +lemma [transfer_rule]:
  23.235 +  "(pcr_natural ===> (=)) (char_of :: nat \<Rightarrow> char) (char_of :: natural \<Rightarrow> char)"
  23.236 +  by (unfold char_of_def [abs_def]) transfer_prover
  23.237 +
  23.238 +lemma [transfer_rule]:
  23.239 +  "((=) ===> pcr_natural) (of_char :: char \<Rightarrow> nat) (of_char :: char \<Rightarrow> natural)"
  23.240 +  by (unfold of_char_def [abs_def]) transfer_prover
  23.241  
  23.242  end
  23.243  
  23.244 -definition Char :: "num \<Rightarrow> char"
  23.245 -  where "Char k = char_of_nat (numeral k)"
  23.246 -
  23.247 -code_datatype "0 :: char" Char
  23.248 -
  23.249 -lemma nat_of_char_zero [simp]:
  23.250 -  "nat_of_char 0 = 0"
  23.251 -  by (simp add: zero_char_def)
  23.252 -
  23.253 -lemma nat_of_char_Char [simp]:
  23.254 -  "nat_of_char (Char k) = numeral k mod 256"
  23.255 -  by (simp add: Char_def)
  23.256 -
  23.257 -lemma Char_eq_Char_iff:
  23.258 -  "Char k = Char l \<longleftrightarrow> numeral k mod (256 :: nat) = numeral l mod 256" (is "?P \<longleftrightarrow> ?Q")
  23.259 -proof -
  23.260 -  have "?P \<longleftrightarrow> nat_of_char (Char k) = nat_of_char (Char l)"
  23.261 -    by (rule sym, rule inj_eq) (fact inj_nat_of_char)
  23.262 -  also have "nat_of_char (Char k) = nat_of_char (Char l) \<longleftrightarrow> ?Q"
  23.263 -    by (simp only: Char_def nat_of_char_of_nat)
  23.264 -  finally show ?thesis .
  23.265 -qed
  23.266 -
  23.267 -lemma zero_eq_Char_iff:
  23.268 -  "0 = Char k \<longleftrightarrow> numeral k mod (256 :: nat) = 0"
  23.269 -  by (auto simp add: zero_char_def Char_def)
  23.270 -
  23.271 -lemma Char_eq_zero_iff:
  23.272 -  "Char k = 0 \<longleftrightarrow> numeral k mod (256 :: nat) = 0"
  23.273 -  by (auto simp add: zero_char_def Char_def) 
  23.274 -
  23.275 -simproc_setup char_eq
  23.276 -  ("Char m = Char n" | "Char m = 0" | "0 = Char n") = \<open>
  23.277 -  let
  23.278 -    val ss = put_simpset HOL_ss @{context}
  23.279 -      |> fold Simplifier.add_simp @{thms Char_eq_Char_iff zero_eq_Char_iff Char_eq_zero_iff cong_exp_iff_simps}
  23.280 -      |> simpset_of 
  23.281 -  in
  23.282 -    fn _ => fn ctxt => SOME o Simplifier.rewrite (put_simpset ss ctxt)
  23.283 -  end
  23.284 -\<close>
  23.285 +lifting_update integer.lifting
  23.286 +lifting_forget integer.lifting
  23.287  
  23.288 -definition integer_of_char :: "char \<Rightarrow> integer"
  23.289 -where
  23.290 -  "integer_of_char = integer_of_nat \<circ> nat_of_char"
  23.291 -
  23.292 -definition char_of_integer :: "integer \<Rightarrow> char"
  23.293 -where
  23.294 -  "char_of_integer = char_of_nat \<circ> nat_of_integer"
  23.295 -
  23.296 -lemma integer_of_char_zero [simp, code]:
  23.297 -  "integer_of_char 0 = 0"
  23.298 -  by (simp add: integer_of_char_def integer_of_nat_def)
  23.299 -
  23.300 -lemma integer_of_char_Char [simp]:
  23.301 -  "integer_of_char (Char k) = numeral k mod 256"
  23.302 -  by (simp only: integer_of_char_def integer_of_nat_def comp_apply nat_of_char_Char map_fun_def
  23.303 -    id_apply zmod_int modulo_integer.abs_eq [symmetric]) simp
  23.304 -
  23.305 -lemma integer_of_char_Char_code [code]:
  23.306 -  "integer_of_char (Char k) = integer_of_num k mod 256"
  23.307 -  by simp
  23.308 -  
  23.309 -lemma nat_of_char_code [code]:
  23.310 -  "nat_of_char = nat_of_integer \<circ> integer_of_char"
  23.311 -  by (simp add: integer_of_char_def fun_eq_iff)
  23.312 -
  23.313 -lemma char_of_nat_code [code]:
  23.314 -  "char_of_nat = char_of_integer \<circ> integer_of_nat"
  23.315 -  by (simp add: char_of_integer_def fun_eq_iff)
  23.316 -
  23.317 -instantiation char :: equal
  23.318 -begin
  23.319 -
  23.320 -definition equal_char
  23.321 -  where "equal_char (c :: char) d \<longleftrightarrow> c = d"
  23.322 -
  23.323 -instance
  23.324 -  by standard (simp add: equal_char_def)
  23.325 -
  23.326 -end
  23.327 -
  23.328 -lemma equal_char_simps [code]:
  23.329 -  "HOL.equal (0::char) 0 \<longleftrightarrow> True"
  23.330 -  "HOL.equal (Char k) (Char l) \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) (numeral l mod 256)"
  23.331 -  "HOL.equal 0 (Char k) \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) 0"
  23.332 -  "HOL.equal (Char k) 0 \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) 0"
  23.333 -  by (simp_all only: equal refl Char_eq_Char_iff zero_eq_Char_iff Char_eq_zero_iff)
  23.334 +lifting_update natural.lifting
  23.335 +lifting_forget natural.lifting
  23.336  
  23.337  syntax
  23.338    "_Char" :: "str_position \<Rightarrow> char"    ("CHR _")
  23.339 @@ -199,7 +198,7 @@
  23.340  type_synonym string = "char list"
  23.341  
  23.342  syntax
  23.343 -  "_String" :: "str_position => string"    ("_")
  23.344 +  "_String" :: "str_position \<Rightarrow> string"    ("_")
  23.345  
  23.346  ML_file "Tools/string_syntax.ML"
  23.347  
  23.348 @@ -207,7 +206,8 @@
  23.349  begin
  23.350  
  23.351  definition
  23.352 -  "Enum.enum = [0, CHR 0x01, CHR 0x02, CHR 0x03,
  23.353 +  "Enum.enum = [
  23.354 +    CHR 0x00, CHR 0x01, CHR 0x02, CHR 0x03,
  23.355      CHR 0x04, CHR 0x05, CHR 0x06, CHR 0x07,
  23.356      CHR 0x08, CHR 0x09, CHR ''\<newline>'', CHR 0x0B,
  23.357      CHR 0x0C, CHR 0x0D, CHR 0x0E, CHR 0x0F,
  23.358 @@ -279,14 +279,15 @@
  23.359    "Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
  23.360  
  23.361  lemma enum_char_unfold:
  23.362 -  "Enum.enum = map char_of_nat [0..<256]"
  23.363 +  "Enum.enum = map char_of [0..<256]"
  23.364  proof -
  23.365 -  have *: "Suc (Suc 0) = 2" by simp
  23.366 -  have "map nat_of_char Enum.enum = [0..<256]"
  23.367 -    by (simp add: enum_char_def upt_conv_Cons_Cons *)
  23.368 -  then have "map char_of_nat (map nat_of_char Enum.enum) =
  23.369 -    map char_of_nat [0..<256]" by simp
  23.370 -  then show ?thesis by (simp add: comp_def)
  23.371 +  have "map (of_char :: char \<Rightarrow> nat) Enum.enum = [0..<256]"
  23.372 +    by (simp add: enum_char_def of_char_def upt_conv_Cons_Cons numeral_2_eq_2 [symmetric])
  23.373 +  then have "map char_of (map (of_char :: char \<Rightarrow> nat) Enum.enum) =
  23.374 +    map char_of [0..<256]"
  23.375 +    by simp
  23.376 +  then show ?thesis
  23.377 +    by simp
  23.378  qed
  23.379  
  23.380  instance proof
  23.381 @@ -302,157 +303,413 @@
  23.382  
  23.383  end
  23.384  
  23.385 +lemma linorder_char:
  23.386 +  "class.linorder (\<lambda>c d. of_char c \<le> (of_char d :: nat)) (\<lambda>c d. of_char c < (of_char d :: nat))"
  23.387 +  by standard auto
  23.388 +
  23.389 +text \<open>Optimized version for execution\<close>
  23.390 +
  23.391 +definition char_of_integer :: "integer \<Rightarrow> char"
  23.392 +  where [code_abbrev]: "char_of_integer = char_of"
  23.393 +
  23.394 +definition integer_of_char :: "char \<Rightarrow> integer"
  23.395 +  where [code_abbrev]: "integer_of_char = of_char"
  23.396 +
  23.397  lemma char_of_integer_code [code]:
  23.398 -  "char_of_integer n = Enum.enum ! (nat_of_integer n mod 256)"
  23.399 -  by (simp add: char_of_integer_def enum_char_unfold)
  23.400 +  "char_of_integer k = (let
  23.401 +     (q0, b0) = bit_cut_integer k;
  23.402 +     (q1, b1) = bit_cut_integer q0;
  23.403 +     (q2, b2) = bit_cut_integer q1;
  23.404 +     (q3, b3) = bit_cut_integer q2;
  23.405 +     (q4, b4) = bit_cut_integer q3;
  23.406 +     (q5, b5) = bit_cut_integer q4;
  23.407 +     (q6, b6) = bit_cut_integer q5;
  23.408 +     (_, b7) = bit_cut_integer q6
  23.409 +    in Char b0 b1 b2 b3 b4 b5 b6 b7)"
  23.410 +  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)
  23.411  
  23.412 -lifting_update char.lifting
  23.413 -lifting_forget char.lifting
  23.414 +lemma integer_of_char_code [code]:
  23.415 +  "integer_of_char (Char b0 b1 b2 b3 b4 b5 b6 b7) =
  23.416 +    ((((((of_bool b7 * 2 + of_bool b6) * 2 +
  23.417 +      of_bool b5) * 2 + of_bool b4) * 2 +
  23.418 +        of_bool b3) * 2 + of_bool b2) * 2 +
  23.419 +          of_bool b1) * 2 + of_bool b0"
  23.420 +  by (simp only: integer_of_char_def of_char_def char.sel)
  23.421  
  23.422  
  23.423 -subsection \<open>Strings as dedicated type\<close>
  23.424 +subsection \<open>Strings as dedicated type for target language code generation\<close>
  23.425 +
  23.426 +subsubsection \<open>Logical specification\<close>
  23.427 +
  23.428 +context
  23.429 +begin
  23.430 +
  23.431 +qualified definition ascii_of :: "char \<Rightarrow> char"
  23.432 +  where "ascii_of c = Char (digit0 c) (digit1 c) (digit2 c) (digit3 c) (digit4 c) (digit5 c) (digit6 c) False"
  23.433  
  23.434 -typedef literal = "UNIV :: string set"
  23.435 -  morphisms explode STR ..
  23.436 +qualified lemma ascii_of_Char [simp]:
  23.437 +  "ascii_of (Char b0 b1 b2 b3 b4 b5 b6 b7) = Char b0 b1 b2 b3 b4 b5 b6 False"
  23.438 +  by (simp add: ascii_of_def)
  23.439 +
  23.440 +qualified lemma not_digit7_ascii_of [simp]:
  23.441 +  "\<not> digit7 (ascii_of c)"
  23.442 +  by (simp add: ascii_of_def)
  23.443 +
  23.444 +qualified lemma ascii_of_idem:
  23.445 +  "ascii_of c = c" if "\<not> digit7 c"
  23.446 +  using that by (cases c) simp
  23.447  
  23.448 -setup_lifting type_definition_literal
  23.449 +qualified lemma char_of_ascii_of [simp]:
  23.450 +  "of_char (ascii_of c) = take_bit 7 (of_char c :: nat)"
  23.451 +  by (cases c)
  23.452 +    (simp add: numeral_3_eq_3 [symmetric] numeral_2_eq_2 [symmetric])
  23.453 +
  23.454 +qualified typedef literal = "{cs. \<forall>c\<in>set cs. \<not> digit7 c}"
  23.455 +  morphisms explode Abs_literal
  23.456 +proof
  23.457 +  show "[] \<in> {cs. \<forall>c\<in>set cs. \<not> digit7 c}"
  23.458 +    by simp
  23.459 +qed
  23.460 +
  23.461 +qualified setup_lifting type_definition_literal
  23.462  
  23.463 -lemma STR_inject' [simp]:
  23.464 -  "STR s = STR t \<longleftrightarrow> s = t"
  23.465 +qualified lift_definition implode :: "string \<Rightarrow> literal"
  23.466 +  is "map ascii_of"
  23.467 +  by auto
  23.468 +
  23.469 +qualified lemma implode_explode_eq [simp]:
  23.470 +  "String.implode (String.explode s) = s"
  23.471 +proof transfer
  23.472 +  fix cs
  23.473 +  show "map ascii_of cs = cs" if "\<forall>c\<in>set cs. \<not> digit7 c"
  23.474 +    using that
  23.475 +      by (induction cs) (simp_all add: ascii_of_idem)
  23.476 +qed
  23.477 +
  23.478 +qualified lemma explode_implode_eq [simp]:
  23.479 +  "String.explode (String.implode cs) = map ascii_of cs"
  23.480    by transfer rule
  23.481  
  23.482 -definition implode :: "string \<Rightarrow> String.literal"
  23.483 -where
  23.484 -  [code del]: "implode = STR"
  23.485 +end
  23.486 +
  23.487 +
  23.488 +subsubsection \<open>Syntactic representation\<close>
  23.489 +
  23.490 +text \<open>
  23.491 +  Logical ground representations for literals are:
  23.492 +
  23.493 +  \<^enum> @{text 0} for the empty literal;
  23.494  
  23.495 -instantiation literal :: size
  23.496 +  \<^enum> @{text "Literal b0 \<dots> b6 s"} for a literal starting with one
  23.497 +    character and continued by another literal.
  23.498 +
  23.499 +  Syntactic representations for literals are:
  23.500 +
  23.501 +  \<^enum> Printable text as string prefixed with @{text STR};
  23.502 +
  23.503 +  \<^enum> A single ascii value as numerical value prefixed with @{text ASCII}.
  23.504 +\<close>
  23.505 +
  23.506 +instantiation String.literal :: zero
  23.507  begin
  23.508  
  23.509 -definition size_literal :: "literal \<Rightarrow> nat"
  23.510 -where
  23.511 -  [code]: "size_literal (s::literal) = 0"
  23.512 +context
  23.513 +begin
  23.514 +
  23.515 +qualified lift_definition zero_literal :: String.literal
  23.516 +  is Nil
  23.517 +  by simp
  23.518  
  23.519  instance ..
  23.520  
  23.521  end
  23.522  
  23.523 -instantiation literal :: equal
  23.524 +end
  23.525 +
  23.526 +context
  23.527  begin
  23.528  
  23.529 -lift_definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool" is "(=)" .
  23.530 +qualified abbreviation (output) empty_literal :: String.literal
  23.531 +  where "empty_literal \<equiv> 0"
  23.532 +
  23.533 +qualified lift_definition Literal :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> String.literal \<Rightarrow> String.literal"
  23.534 +  is "\<lambda>b0 b1 b2 b3 b4 b5 b6 cs. Char b0 b1 b2 b3 b4 b5 b6 False # cs"
  23.535 +  by auto
  23.536  
  23.537 -instance by intro_classes (transfer, simp)
  23.538 +qualified lemma Literal_eq_iff [simp]:
  23.539 +  "Literal b0 b1 b2 b3 b4 b5 b6 s = Literal c0 c1 c2 c3 c4 c5 c6 t
  23.540 +     \<longleftrightarrow> (b0 \<longleftrightarrow> c0) \<and> (b1 \<longleftrightarrow> c1) \<and> (b2 \<longleftrightarrow> c2) \<and> (b3 \<longleftrightarrow> c3)
  23.541 +         \<and> (b4 \<longleftrightarrow> c4) \<and> (b5 \<longleftrightarrow> c5) \<and> (b6 \<longleftrightarrow> c6) \<and> s = t"
  23.542 +  by transfer simp
  23.543 +
  23.544 +qualified lemma empty_neq_Literal [simp]:
  23.545 +  "empty_literal \<noteq> Literal b0 b1 b2 b3 b4 b5 b6 s"
  23.546 +  by transfer simp
  23.547 +
  23.548 +qualified lemma Literal_neq_empty [simp]:
  23.549 +  "Literal b0 b1 b2 b3 b4 b5 b6 s \<noteq> empty_literal"
  23.550 +  by transfer simp
  23.551  
  23.552  end
  23.553  
  23.554 -declare equal_literal.rep_eq[code]
  23.555 +code_datatype "0 :: String.literal" String.Literal
  23.556 +
  23.557 +syntax
  23.558 +  "_Ascii" :: "num_const \<Rightarrow> String.literal"        ("ASCII _")
  23.559 +  "_Literal" :: "str_position \<Rightarrow> String.literal"   ("STR _")
  23.560  
  23.561 -lemma [code nbe]:
  23.562 -  fixes s :: "String.literal"
  23.563 -  shows "HOL.equal s s \<longleftrightarrow> True"
  23.564 -  by (simp add: equal)
  23.565 +ML_file "Tools/literal.ML"
  23.566 +
  23.567  
  23.568 -instantiation literal :: zero
  23.569 +subsubsection \<open>Operations\<close>
  23.570 +
  23.571 +instantiation String.literal :: plus
  23.572  begin
  23.573  
  23.574 -lift_definition zero_literal :: "literal"
  23.575 -  is "[]"
  23.576 -  .
  23.577 +context
  23.578 +begin
  23.579 +
  23.580 +qualified lift_definition plus_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> String.literal"
  23.581 +  is "(@)"
  23.582 +  by auto
  23.583  
  23.584  instance ..
  23.585  
  23.586  end
  23.587  
  23.588 -lemma [code]:
  23.589 -  "0 = STR ''''"
  23.590 -  by (fact zero_literal.abs_eq)
  23.591 +end
  23.592  
  23.593 -instantiation literal :: plus
  23.594 +instance String.literal :: monoid_add
  23.595 +  by (standard; transfer) simp_all
  23.596 +
  23.597 +instantiation String.literal :: size
  23.598  begin
  23.599  
  23.600 -lift_definition plus_literal :: "literal \<Rightarrow> literal \<Rightarrow> literal"
  23.601 -  is "(@)"
  23.602 -  .
  23.603 +context
  23.604 +  includes literal.lifting
  23.605 +begin
  23.606 +
  23.607 +lift_definition size_literal :: "String.literal \<Rightarrow> nat"
  23.608 +  is length .
  23.609 +
  23.610 +end
  23.611  
  23.612  instance ..
  23.613  
  23.614  end
  23.615  
  23.616 -lemma [code]:
  23.617 -  "s + t = String.implode (String.explode s @ String.explode t)"
  23.618 -  using plus_literal.abs_eq [of "String.explode s" "String.explode t"]
  23.619 -  by (simp add: explode_inverse implode_def)
  23.620 +instantiation String.literal :: equal
  23.621 +begin
  23.622 +
  23.623 +context
  23.624 +begin
  23.625 +
  23.626 +qualified lift_definition equal_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
  23.627 +  is HOL.equal .
  23.628 +
  23.629 +instance
  23.630 +  by (standard; transfer) (simp add: equal)
  23.631 +
  23.632 +end
  23.633 +
  23.634 +end
  23.635 +
  23.636 +instantiation String.literal :: linorder
  23.637 +begin
  23.638  
  23.639 -instance literal :: monoid_add
  23.640 -  by standard (transfer; simp)+
  23.641 +context
  23.642 +begin
  23.643 +
  23.644 +qualified lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
  23.645 +  is "ord.lexordp_eq (\<lambda>c d. of_char c < (of_char d :: nat))"
  23.646 +  .
  23.647 +
  23.648 +qualified lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
  23.649 +  is "ord.lexordp (\<lambda>c d. of_char c < (of_char d :: nat))"
  23.650 +  .
  23.651 +
  23.652 +instance proof -
  23.653 +  from linorder_char interpret linorder "ord.lexordp_eq (\<lambda>c d. of_char c < (of_char d :: nat))"
  23.654 +    "ord.lexordp (\<lambda>c d. of_char c < (of_char d :: nat)) :: string \<Rightarrow> string \<Rightarrow> bool"
  23.655 +    by (rule linorder.lexordp_linorder)
  23.656 +  show "PROP ?thesis"
  23.657 +    by (standard; transfer) (simp_all add: less_le_not_le linear)
  23.658 +qed
  23.659 +
  23.660 +end
  23.661 +
  23.662 +end
  23.663  
  23.664 -lifting_update literal.lifting
  23.665 -lifting_forget literal.lifting
  23.666 +lemma infinite_literal:
  23.667 +  "infinite (UNIV :: String.literal set)"
  23.668 +proof -
  23.669 +  define S where "S = range (\<lambda>n. replicate n CHR ''A'')"
  23.670 +  have "inj_on String.implode S"
  23.671 +  proof (rule inj_onI)
  23.672 +    fix cs ds
  23.673 +    assume "String.implode cs = String.implode ds"
  23.674 +    then have "String.explode (String.implode cs) = String.explode (String.implode ds)"
  23.675 +      by simp
  23.676 +    moreover assume "cs \<in> S" and "ds \<in> S"
  23.677 +    ultimately show "cs = ds"
  23.678 +      by (auto simp add: S_def)
  23.679 +  qed
  23.680 +  moreover have "infinite S"
  23.681 +    by (auto simp add: S_def dest: finite_range_imageI [of _ length])
  23.682 +  ultimately have "infinite (String.implode ` S)"
  23.683 +    by (simp add: finite_image_iff)
  23.684 +  then show ?thesis
  23.685 +    by (auto intro: finite_subset)
  23.686 +qed
  23.687 +
  23.688 +
  23.689 +subsubsection \<open>Executable conversions\<close>
  23.690 +
  23.691 +context
  23.692 +begin
  23.693 +
  23.694 +qualified lift_definition asciis_of_literal :: "String.literal \<Rightarrow> integer list"
  23.695 +  is "map of_char"
  23.696 +  .
  23.697 +
  23.698 +qualified lift_definition literal_of_asciis :: "integer list \<Rightarrow> String.literal"
  23.699 +  is "map (String.ascii_of \<circ> char_of)"
  23.700 +  by auto
  23.701  
  23.702 -  
  23.703 -subsection \<open>Dedicated conversion for generated computations\<close>
  23.704 +qualified lemma literal_of_asciis_of_literal [simp]:
  23.705 +  "literal_of_asciis (asciis_of_literal s) = s"
  23.706 +proof transfer
  23.707 +  fix cs
  23.708 +  assume "\<forall>c\<in>set cs. \<not> digit7 c"
  23.709 +  then show "map (String.ascii_of \<circ> char_of) (map of_char cs) = cs"
  23.710 +    by (induction cs) (simp_all add: String.ascii_of_idem) 
  23.711 +qed
  23.712 +
  23.713 +qualified lemma explode_code [code]:
  23.714 +  "String.explode s = map char_of (asciis_of_literal s)"
  23.715 +  by transfer simp
  23.716 +
  23.717 +qualified lemma implode_code [code]:
  23.718 +  "String.implode cs = literal_of_asciis (map of_char cs)"
  23.719 +  by transfer simp
  23.720  
  23.721 -definition char_of_num :: "num \<Rightarrow> char"
  23.722 -  where "char_of_num = char_of_nat \<circ> nat_of_num"
  23.723 +end
  23.724 +
  23.725 +declare [[code drop: String.literal_of_asciis String.asciis_of_literal]]
  23.726 +
  23.727 +
  23.728 +subsubsection \<open>Technical code generation setup\<close>
  23.729 +
  23.730 +text \<open>Alternative constructor for generated computations\<close>
  23.731 +
  23.732 +context
  23.733 +begin  
  23.734 +
  23.735 +qualified definition Literal' :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> String.literal \<Rightarrow> String.literal"
  23.736 +  where [simp]: "Literal' = String.Literal"
  23.737 +
  23.738 +lemma [code]:
  23.739 +  "Literal' b0 b1 b2 b3 b4 b5 b6 s = String.literal_of_asciis
  23.740 +    [foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6] 0] + s" 
  23.741 +  unfolding Literal'_def by transfer (simp add: char_of_def)
  23.742  
  23.743  lemma [code_computation_unfold]:
  23.744 -  "Char = char_of_num"
  23.745 -  by (simp add: fun_eq_iff char_of_num_def nat_of_num_numeral Char_def)
  23.746 -
  23.747 +  "String.Literal = Literal'"
  23.748 +  by simp
  23.749  
  23.750 -subsection \<open>Code generator\<close>
  23.751 +end
  23.752  
  23.753 -ML_file "Tools/string_code.ML"
  23.754 -
  23.755 -code_reserved SML string
  23.756 -code_reserved OCaml string
  23.757 +code_reserved SML string Char
  23.758 +code_reserved OCaml string String Char List
  23.759 +code_reserved Haskell Prelude
  23.760  code_reserved Scala string
  23.761  
  23.762  code_printing
  23.763 -  type_constructor literal \<rightharpoonup>
  23.764 +  type_constructor String.literal \<rightharpoonup>
  23.765      (SML) "string"
  23.766      and (OCaml) "string"
  23.767      and (Haskell) "String"
  23.768      and (Scala) "String"
  23.769 +| constant "STR ''''" \<rightharpoonup>
  23.770 +    (SML) "\"\""
  23.771 +    and (OCaml) "\"\""
  23.772 +    and (Haskell) "\"\""
  23.773 +    and (Scala) "\"\""
  23.774  
  23.775  setup \<open>
  23.776 -  fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
  23.777 +  fold Literal.add_code ["SML", "OCaml", "Haskell", "Scala"]
  23.778  \<close>
  23.779  
  23.780  code_printing
  23.781 -  class_instance literal :: equal \<rightharpoonup>
  23.782 +  constant "(+) :: String.literal \<Rightarrow> String.literal \<Rightarrow> String.literal" \<rightharpoonup>
  23.783 +    (SML) infixl 18 "^"
  23.784 +    and (OCaml) infixr 6 "^"
  23.785 +    and (Haskell) infixr 5 "++"
  23.786 +    and (Scala) infixl 7 "+"
  23.787 +| constant String.literal_of_asciis \<rightharpoonup>
  23.788 +    (SML) "!(String.implode/ o map (fn k => if 0 <= k andalso k < 128 then (Char.chr o IntInf.toInt) k else raise Fail \"Non-ASCII character in literal\"))"
  23.789 +    and (OCaml) "!(let ks = _ in let res = Bytes.create (List.length ks) in let rec imp i = function | [] -> res | k :: ks ->
  23.790 +      let l = Big'_int.int'_of'_big'_int k in if 0 <= l && l < 128 then Bytes.set res i (Char.chr l) else failwith \"Non-ASCII character in literal\"; imp (i + 1) ks in imp 0 ks)"
  23.791 +    and (Haskell) "map/ (let chr k | (0 <= k && k < 128) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)"
  23.792 +    and (Scala) "\"\"/ ++/ _.map((k: BigInt) => if (BigInt(0) <= k && k < BigInt(128)) k.charValue else sys.error(\"Non-ASCII character in literal\"))"
  23.793 +| constant String.asciis_of_literal \<rightharpoonup>
  23.794 +    (SML) "!(map (fn c => let val k = Char.ord c in if k < 128 then IntInf.fromInt k else raise Fail \"Non-ASCII character in literal\" end) /o String.explode)"
  23.795 +    and (OCaml) "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (let k = Char.code (Bytes.get s i) in
  23.796 +      if k < 128 then Big'_int.big'_int'_of'_int k :: l else failwith \"Non-ASCII character in literal\") in exp (Bytes.length s - 1) [])"
  23.797 +    and (Haskell) "map/ (let ord k | (k < 128) = Prelude.toInteger k in ord . (Prelude.fromEnum :: Prelude.Char -> Prelude.Int))"
  23.798 +    and (Scala) "!(_.toList.map(c => { val k: Int = c.toInt; if (k < 128) BigInt(k) else sys.error(\"Non-ASCII character in literal\") }))"
  23.799 +| class_instance String.literal :: equal \<rightharpoonup>
  23.800      (Haskell) -
  23.801 -| constant "HOL.equal :: literal \<Rightarrow> literal \<Rightarrow> bool" \<rightharpoonup>
  23.802 +| constant "HOL.equal :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
  23.803      (SML) "!((_ : string) = _)"
  23.804      and (OCaml) "!((_ : string) = _)"
  23.805      and (Haskell) infix 4 "=="
  23.806      and (Scala) infixl 5 "=="
  23.807 +| constant "(\<le>) :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
  23.808 +    (SML) "!((_ : string) <= _)"
  23.809 +    and (OCaml) "!((_ : string) <= _)"
  23.810 +    \<comment> \<open>Order operations for @{typ String.literal} work in Haskell only
  23.811 +          if no type class instance needs to be generated, because String = [Char] in Haskell
  23.812 +          and @{typ "char list"} need not have the same order as @{typ String.literal}.\<close>
  23.813 +    and (Haskell) infix 4 "<="
  23.814 +    and (Scala) infixl 4 "<="
  23.815 +    and (Eval) infixl 6 "<="
  23.816 +| constant "(<) :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
  23.817 +    (SML) "!((_ : string) < _)"
  23.818 +    and (OCaml) "!((_ : string) < _)"
  23.819 +    and (Haskell) infix 4 "<"
  23.820 +    and (Scala) infixl 4 "<"
  23.821 +    and (Eval) infixl 6 "<"
  23.822 +
  23.823 +
  23.824 +subsubsection \<open>Code generation utility\<close>
  23.825  
  23.826  setup \<open>Sign.map_naming (Name_Space.mandatory_path "Code")\<close>
  23.827  
  23.828 -definition abort :: "literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a"
  23.829 -where [simp, code del]: "abort _ f = f ()"
  23.830 +definition abort :: "String.literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a"
  23.831 +  where [simp]: "abort _ f = f ()"
  23.832  
  23.833 -lemma abort_cong: "msg = msg' ==> Code.abort msg f = Code.abort msg' f"
  23.834 -by simp
  23.835 +declare [[code drop: Code.abort]]
  23.836 +
  23.837 +lemma abort_cong:
  23.838 +  "msg = msg' \<Longrightarrow> Code.abort msg f = Code.abort msg' f"
  23.839 +  by simp
  23.840  
  23.841  setup \<open>Sign.map_naming Name_Space.parent_path\<close>
  23.842  
  23.843  setup \<open>Code_Simp.map_ss (Simplifier.add_cong @{thm Code.abort_cong})\<close>
  23.844  
  23.845 -code_printing constant Code.abort \<rightharpoonup>
  23.846 +code_printing
  23.847 +  constant Code.abort \<rightharpoonup>
  23.848      (SML) "!(raise/ Fail/ _)"
  23.849      and (OCaml) "failwith"
  23.850      and (Haskell) "!(error/ ::/ forall a./ String -> (() -> a) -> a)"
  23.851 -    and (Scala) "!{/ sys.error((_));/  ((_)).apply(())/ }"
  23.852 -| constant "(+) :: literal \<Rightarrow> literal \<Rightarrow> literal" \<rightharpoonup>
  23.853 -    (SML) infixl 18 "^"
  23.854 -    and (OCaml) infixr 6 "@"
  23.855 -    and (Haskell) infixr 5 "++"
  23.856 -    and (Scala) infixl 7 "+"
  23.857 +    and (Scala) "!{/ sys.error((_));/ ((_)).apply(())/ }"
  23.858 +
  23.859  
  23.860 -hide_type (open) literal
  23.861 +subsubsection \<open>Finally\<close>
  23.862  
  23.863 -hide_const (open) implode explode
  23.864 +lifting_update literal.lifting
  23.865 +lifting_forget literal.lifting
  23.866  
  23.867  end
    24.1 --- a/src/HOL/Tools/hologic.ML	Tue Apr 24 14:17:57 2018 +0000
    24.2 +++ b/src/HOL/Tools/hologic.ML	Tue Apr 24 14:17:58 2018 +0000
    24.3 @@ -98,8 +98,6 @@
    24.4    val one_const: term
    24.5    val bit0_const: term
    24.6    val bit1_const: term
    24.7 -  val mk_bit: int -> term
    24.8 -  val dest_bit: term -> int
    24.9    val mk_numeral: int -> term
   24.10    val dest_numeral: term -> int
   24.11    val numeral_const: typ -> term
   24.12 @@ -519,18 +517,15 @@
   24.13  and bit0_const = Const ("Num.num.Bit0", numT --> numT)
   24.14  and bit1_const = Const ("Num.num.Bit1", numT --> numT);
   24.15  
   24.16 -fun mk_bit 0 = bit0_const
   24.17 -  | mk_bit 1 = bit1_const
   24.18 -  | mk_bit _ = raise TERM ("mk_bit", []);
   24.19 -
   24.20 -fun dest_bit (Const ("Num.num.Bit0", _)) = 0
   24.21 -  | dest_bit (Const ("Num.num.Bit1", _)) = 1
   24.22 -  | dest_bit t = raise TERM ("dest_bit", [t]);
   24.23 -
   24.24  fun mk_numeral i =
   24.25 -  let fun mk 1 = one_const
   24.26 -        | mk i = let val (q, r) = Integer.div_mod i 2 in mk_bit r $ mk q end
   24.27 -  in if i > 0 then mk i else raise TERM ("mk_numeral: " ^ string_of_int i, [])
   24.28 +  let
   24.29 +    fun mk 1 = one_const
   24.30 +      | mk i =
   24.31 +          let
   24.32 +            val (q, r) = Integer.div_mod i 2
   24.33 +          in (if r = 0 then bit0_const else bit1_const) $ mk q end
   24.34 +  in
   24.35 +    if i > 0 then mk i else raise TERM ("mk_numeral: " ^ string_of_int i, [])
   24.36    end
   24.37  
   24.38  fun dest_numeral (Const ("Num.num.One", _)) = 1
   24.39 @@ -555,7 +550,7 @@
   24.40    | dest_number (Const ("Groups.one_class.one", T)) = (T, 1)
   24.41    | dest_number (Const ("Num.numeral_class.numeral", Type ("fun", [_, T])) $ t) =
   24.42        (T, dest_numeral t)
   24.43 -  | dest_number (Const ("Groups.uminus_class.uminus", Type ("fun", [_, T])) $ t) =
   24.44 +  | dest_number (Const ("Groups.uminus_class.uminus", Type ("fun", _)) $ t) =
   24.45        apsnd (op ~) (dest_number t)
   24.46    | dest_number t = raise TERM ("dest_number", [t]);
   24.47  
   24.48 @@ -594,27 +589,35 @@
   24.49    | dest_list t = raise TERM ("dest_list", [t]);
   24.50  
   24.51  
   24.52 +(* booleans as bits *)
   24.53 +
   24.54 +fun mk_bit b = if b = 0 then @{term False}
   24.55 +  else if b = 1 then @{term True}
   24.56 +  else raise TERM ("mk_bit", []);
   24.57 +
   24.58 +fun mk_bits len = map mk_bit o Integer.radicify 2 len;
   24.59 +
   24.60 +fun dest_bit @{term False} = 0
   24.61 +  | dest_bit @{term True} = 1
   24.62 +  | dest_bit _ = raise TERM ("dest_bit", []);
   24.63 +
   24.64 +val dest_bits = Integer.eval_radix 2 o map dest_bit;
   24.65 +
   24.66 +
   24.67  (* char *)
   24.68  
   24.69  val charT = Type ("String.char", []);
   24.70  
   24.71 -val Char_const = Const ("String.Char", numT --> charT);
   24.72 -
   24.73 -fun mk_char 0 = Const ("Groups.zero_class.zero", charT)
   24.74 -  | mk_char i =
   24.75 -      if 1 <= i andalso i <= 255 then Char_const $ mk_numeral i
   24.76 -      else raise TERM ("mk_char", []);
   24.77 +val Char_const = Const ("String.char.Char", replicate 8 boolT ---> charT);
   24.78  
   24.79 -fun dest_char t =
   24.80 -  let
   24.81 -    val (T, n) = case t of
   24.82 -      Const ("Groups.zero_class.zero", T) => (T, 0)
   24.83 -    | (Const ("String.Char", Type ("fun", [_, T])) $ t) => (T, dest_numeral t)
   24.84 -    | _ => raise TERM ("dest_char", [t]);
   24.85 -  in
   24.86 -    if T = charT then n
   24.87 -    else raise TERM ("dest_char", [t])
   24.88 -  end;
   24.89 +fun mk_char i =
   24.90 +  if 0 <= i andalso i <= 255
   24.91 +  then list_comb (Char_const, mk_bits 8 i)
   24.92 +  else raise TERM ("mk_char", [])
   24.93 +
   24.94 +fun dest_char (Const ("String.char.Char", _) $ b0 $ b1 $ b2 $ b3 $ b4 $ b5 $ b6 $ b7) =
   24.95 +      dest_bits [b0, b1, b2, b3, b4, b5, b6, b7]
   24.96 +  | dest_char t = raise TERM ("dest_char", [t]);
   24.97  
   24.98  
   24.99  (* string *)
  24.100 @@ -629,11 +632,28 @@
  24.101  
  24.102  val literalT = Type ("String.literal", []);
  24.103  
  24.104 -fun mk_literal s = Const ("String.literal.STR", stringT --> literalT)
  24.105 -      $ mk_string s;
  24.106 -fun dest_literal (Const ("String.literal.STR", _) $ t) =
  24.107 -      dest_string t
  24.108 -  | dest_literal t = raise TERM ("dest_literal", [t]);
  24.109 +val Literal_const = Const ("String.Literal", replicate 7 boolT ---> literalT --> literalT);
  24.110 +
  24.111 +fun mk_literal s = 
  24.112 +  let
  24.113 +    fun mk [] =
  24.114 +          Const ("Groups.zero_class.zero", literalT)
  24.115 +      | mk (c :: cs) =
  24.116 +          list_comb (Literal_const, mk_bits 7 c) $ mk cs;
  24.117 +    val cs = map ord (raw_explode s);
  24.118 +  in
  24.119 +    if forall (fn c => c < 128) cs
  24.120 +    then mk cs
  24.121 +    else raise TERM ("mk_literal", [])
  24.122 +  end;
  24.123 +
  24.124 +val dest_literal =
  24.125 +  let
  24.126 +    fun dest (Const ("Groups.zero_class.zero", Type ("String.literal", []))) = []
  24.127 +      | dest (Const ("String.Literal", _) $ b0 $ b1 $ b2 $ b3 $ b4 $ b5 $ b6 $ t) =
  24.128 +          chr (dest_bits [b0, b1, b2, b3, b4, b5, b6]) :: dest t
  24.129 +      | dest t = raise TERM ("dest_literal", [t]);
  24.130 +  in implode o dest end;
  24.131  
  24.132  
  24.133  (* typerep and term *)
    25.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.2 +++ b/src/HOL/Tools/literal.ML	Tue Apr 24 14:17:58 2018 +0000
    25.3 @@ -0,0 +1,123 @@
    25.4 +(*  Title:      HOL/Tools/literal.ML
    25.5 +    Author:     Florian Haftmann, TU Muenchen
    25.6 +
    25.7 +Logical and syntactic operations on literals (see also HOL/Tools/hologic.ML).
    25.8 +*)
    25.9 +
   25.10 +signature LITERAL =
   25.11 +sig
   25.12 +  val add_code: string -> theory -> theory
   25.13 +end
   25.14 +
   25.15 +structure Literal: LITERAL =
   25.16 +struct
   25.17 +
   25.18 +datatype character = datatype String_Syntax.character;
   25.19 +
   25.20 +fun mk_literal_syntax [] = Syntax.const @{const_syntax String.empty_literal}
   25.21 +  | mk_literal_syntax (c :: cs) =
   25.22 +      list_comb (Syntax.const @{const_syntax String.Literal}, String_Syntax.mk_bits_syntax 7 c)
   25.23 +        $ mk_literal_syntax cs;
   25.24 +
   25.25 +val dest_literal_syntax =
   25.26 +  let
   25.27 +    fun dest (Const (@{const_syntax String.empty_literal}, _)) = []
   25.28 +      | dest (Const (@{const_syntax String.Literal}, _) $ b0 $ b1 $ b2 $ b3 $ b4 $ b5 $ b6 $ t) =
   25.29 +          String_Syntax.classify_character (String_Syntax.dest_bits_syntax [b0, b1, b2, b3, b4, b5, b6]) :: dest t
   25.30 +      | dest t = raise Match;
   25.31 +  in dest end;
   25.32 +
   25.33 +fun ascii_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
   25.34 +      c $ ascii_tr [t] $ u
   25.35 +  | ascii_tr [Const (num, _)] =
   25.36 +      (mk_literal_syntax o single o (fn n => n mod 128) o #value o Lexicon.read_num) num
   25.37 +  | ascii_tr ts = raise TERM ("ascii_tr", ts);
   25.38 +
   25.39 +fun literal_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
   25.40 +      c $ literal_tr [t] $ u
   25.41 +  | literal_tr [Free (str, _)] =
   25.42 +      (mk_literal_syntax o map ord o String_Syntax.plain_strings_of) str
   25.43 +  | literal_tr ts = raise TERM ("literal_tr", ts);
   25.44 +
   25.45 +fun ascii k = Syntax.const @{syntax_const "_Ascii"}
   25.46 +  $ Syntax.free (String_Syntax.hex k);
   25.47 +
   25.48 +fun literal cs = Syntax.const @{syntax_const "_Literal"}
   25.49 +  $ Syntax.const (Lexicon.implode_str cs);
   25.50 +
   25.51 +fun empty_literal_tr' _ = literal [];
   25.52 +
   25.53 +fun literal_tr' [b0, b1, b2, b3, b4, b5, b6, t] =
   25.54 +      let
   25.55 +        val cs =
   25.56 +          dest_literal_syntax (list_comb (Syntax.const @{const_syntax String.Literal}, [b0, b1, b2, b3, b4, b5, b6, t]))
   25.57 +        fun is_printable (Char _) = true
   25.58 +          | is_printable (Ord _) = false;
   25.59 +        fun the_char (Char c) = c;
   25.60 +        fun the_ascii [Ord i] = i;
   25.61 +      in
   25.62 +        if forall is_printable cs
   25.63 +        then literal (map the_char cs)
   25.64 +        else if length cs = 1
   25.65 +        then ascii (the_ascii cs)
   25.66 +        else raise Match
   25.67 +      end
   25.68 +  | literal_tr' _ = raise Match;
   25.69 +
   25.70 +open Basic_Code_Thingol;
   25.71 +
   25.72 +fun map_partial g f =
   25.73 +  let
   25.74 +    fun mapp [] = SOME []
   25.75 +      | mapp (x :: xs) =
   25.76 +          (case f x of
   25.77 +            NONE => NONE
   25.78 +          | SOME y => 
   25.79 +            (case mapp xs of
   25.80 +              NONE => NONE
   25.81 +            | SOME ys => SOME (y :: ys)))
   25.82 +  in Option.map g o mapp end;
   25.83 +
   25.84 +fun implode_bit (IConst { sym = Code_Symbol.Constant @{const_name False}, ... }) = SOME 0
   25.85 +  | implode_bit (IConst { sym = Code_Symbol.Constant @{const_name True}, ... }) = SOME 1
   25.86 +  | implode_bit _ = NONE
   25.87 +
   25.88 +fun implode_ascii (b0, b1, b2, b3, b4, b5, b6) =
   25.89 +  map_partial (chr o Integer.eval_radix 2) implode_bit [b0, b1, b2, b3, b4, b5, b6];
   25.90 +
   25.91 +fun implode_literal b0 b1 b2 b3 b4 b5 b6 t =
   25.92 +  let
   25.93 +    fun dest_literal (IConst { sym = Code_Symbol.Constant @{const_name String.Literal}, ... }
   25.94 +          `$ b0 `$ b1 `$ b2 `$ b3 `$ b4 `$ b5 `$ b6 `$ t) = SOME ((b0, b1, b2, b3, b4, b5, b6), t)
   25.95 +      | dest_literal _ = NONE;
   25.96 +    val (bss', t') = Code_Thingol.unfoldr dest_literal t;
   25.97 +    val bss = (b0, b1, b2, b3, b4, b5, b6) :: bss';
   25.98 +  in
   25.99 +    case t' of
  25.100 +      IConst { sym = Code_Symbol.Constant @{const_name String.zero_literal_inst.zero_literal}, ... }
  25.101 +        => map_partial implode implode_ascii bss
  25.102 +    | _ => NONE
  25.103 +  end;
  25.104 +
  25.105 +fun add_code target thy =
  25.106 +  let
  25.107 +    fun pretty literals _ thm _ _ [(b0, _), (b1, _), (b2, _), (b3, _), (b4, _), (b5, _), (b6, _), (t, _)] =
  25.108 +      case implode_literal b0 b1 b2 b3 b4 b5 b6 t of
  25.109 +        SOME s => (Code_Printer.str o Code_Printer.literal_string literals) s
  25.110 +      | NONE => Code_Printer.eqn_error thy thm "Illegal string literal expression";
  25.111 +  in
  25.112 +    thy
  25.113 +    |> Code_Target.set_printings (Code_Symbol.Constant (@{const_name String.Literal},
  25.114 +      [(target, SOME (Code_Printer.complex_const_syntax (8, pretty)))]))
  25.115 +  end;
  25.116 +
  25.117 +val _ =
  25.118 +  Theory.setup
  25.119 +   (Sign.parse_translation
  25.120 +     [(@{syntax_const "_Ascii"}, K ascii_tr),
  25.121 +      (@{syntax_const "_Literal"}, K literal_tr)] #>
  25.122 +    Sign.print_translation
  25.123 +     [(@{const_syntax String.Literal}, K literal_tr'),
  25.124 +      (@{const_syntax String.empty_literal}, K empty_literal_tr')]);
  25.125 +
  25.126 +end
    26.1 --- a/src/HOL/Tools/numeral.ML	Tue Apr 24 14:17:57 2018 +0000
    26.2 +++ b/src/HOL/Tools/numeral.ML	Tue Apr 24 14:17:58 2018 +0000
    26.3 @@ -1,17 +1,14 @@
    26.4  (*  Title:      HOL/Tools/numeral.ML
    26.5      Author:     Makarius
    26.6  
    26.7 -Logical operations on numerals (see also HOL/Tools/hologic.ML).
    26.8 +Logical and syntactic operations on numerals (see also HOL/Tools/hologic.ML).
    26.9  *)
   26.10  
   26.11  signature NUMERAL =
   26.12  sig
   26.13    val mk_cnumber: ctyp -> int -> cterm
   26.14    val mk_number_syntax: int -> term
   26.15 -  val mk_cnumeral: int -> cterm
   26.16 -  val mk_num_syntax: int -> term
   26.17    val dest_num_syntax: term -> int
   26.18 -  val dest_num: Code_Thingol.iterm -> int option
   26.19    val add_code: string -> (int -> int) -> (Code_Printer.literals -> int -> string) -> string -> theory -> theory
   26.20  end;
   26.21  
   26.22 @@ -92,25 +89,23 @@
   26.23  
   26.24  local open Basic_Code_Thingol in
   26.25  
   26.26 -fun dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.One}, ... }) = SOME 1
   26.27 -  | dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit0}, ... } `$ t) =
   26.28 -     (case dest_num t of
   26.29 +fun dest_num_code (IConst { sym = Code_Symbol.Constant @{const_name Num.One}, ... }) = SOME 1
   26.30 +  | dest_num_code (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit0}, ... } `$ t) =
   26.31 +     (case dest_num_code t of
   26.32          SOME n => SOME (2 * n)
   26.33        | _ => NONE)
   26.34 -  | dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit1}, ... } `$ t) =
   26.35 -     (case dest_num t of
   26.36 +  | dest_num_code (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit1}, ... } `$ t) =
   26.37 +     (case dest_num_code t of
   26.38          SOME n => SOME (2 * n + 1)
   26.39        | _ => NONE)
   26.40 -  | dest_num _ = NONE;
   26.41 +  | dest_num_code _ = NONE;
   26.42  
   26.43  fun add_code number_of preproc print target thy =
   26.44    let
   26.45      fun pretty literals _ thm _ _ [(t, _)] =
   26.46 -      let
   26.47 -        val n = case dest_num t of
   26.48 -          SOME n => n
   26.49 -        | NONE => Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal term"
   26.50 -      in (Code_Printer.str o print literals o preproc) n end;
   26.51 +      case dest_num_code t of
   26.52 +        SOME n => (Code_Printer.str o print literals o preproc) n
   26.53 +      | NONE => Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal term";
   26.54    in
   26.55      thy |> Code_Target.set_printings (Code_Symbol.Constant (number_of,
   26.56        [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))]))
    27.1 --- a/src/HOL/Tools/string_code.ML	Tue Apr 24 14:17:57 2018 +0000
    27.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    27.3 @@ -1,85 +0,0 @@
    27.4 -(*  Title:      HOL/Tools/string_code.ML
    27.5 -    Author:     Florian Haftmann, TU Muenchen
    27.6 -
    27.7 -Code generation for character and string literals.
    27.8 -*)
    27.9 -
   27.10 -signature STRING_CODE =
   27.11 -sig
   27.12 -  val add_literal_list_string: string -> theory -> theory
   27.13 -  val add_literal_char: string -> theory -> theory
   27.14 -  val add_literal_string: string -> theory -> theory
   27.15 -end;
   27.16 -
   27.17 -structure String_Code : STRING_CODE =
   27.18 -struct
   27.19 -
   27.20 -open Basic_Code_Thingol;
   27.21 -
   27.22 -fun decode_char_nonzero t =
   27.23 -  case Numeral.dest_num t of
   27.24 -    SOME n => if 0 < n andalso n < 256 then SOME n else NONE
   27.25 -  | _ => NONE;
   27.26 -
   27.27 -fun decode_char (IConst { sym = Code_Symbol.Constant @{const_name String.zero_char_inst.zero_char}, ... }) =
   27.28 -     SOME 0
   27.29 -  | decode_char (IConst { sym = Code_Symbol.Constant @{const_name Char}, ... } `$ t) =
   27.30 -      decode_char_nonzero t
   27.31 -  | decode_char _ = NONE
   27.32 -
   27.33 -fun implode_string literals ts =
   27.34 -  let
   27.35 -    val is = map_filter decode_char ts;
   27.36 -  in if length ts = length is
   27.37 -    then (SOME o Code_Printer.str o Code_Printer.literal_string literals o implode o map chr) is
   27.38 -    else NONE
   27.39 -  end;
   27.40 -
   27.41 -fun add_literal_list_string target =
   27.42 -  let
   27.43 -    fun pretty literals pr _ vars fxy [(t1, _), (t2, _)] =
   27.44 -      case Option.map (cons t1) (List_Code.implode_list t2)
   27.45 -       of SOME ts => (case implode_string literals ts
   27.46 -             of SOME p => p
   27.47 -              | NONE =>
   27.48 -                  Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts))
   27.49 -        | NONE =>
   27.50 -            List_Code.default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
   27.51 -  in
   27.52 -    Code_Target.set_printings (Code_Symbol.Constant (@{const_name Cons},
   27.53 -      [(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))]))
   27.54 -  end;
   27.55 -
   27.56 -fun add_literal_char target thy =
   27.57 -  let
   27.58 -    fun pr literals =
   27.59 -      Code_Printer.str o Code_Printer.literal_char literals o chr;
   27.60 -    fun pretty_zero literals _ _ _ _ [] =
   27.61 -      pr literals 0
   27.62 -    fun pretty_Char literals _ thm _ _ [(t, _)] =
   27.63 -      case decode_char_nonzero t
   27.64 -       of SOME i => pr literals i
   27.65 -        | NONE => Code_Printer.eqn_error thy thm "Illegal character expression";
   27.66 -  in
   27.67 -    thy
   27.68 -    |> Code_Target.set_printings (Code_Symbol.Constant (@{const_name String.zero_char_inst.zero_char},
   27.69 -      [(target, SOME (Code_Printer.complex_const_syntax (0, pretty_zero)))]))
   27.70 -    |> Code_Target.set_printings (Code_Symbol.Constant (@{const_name Char},
   27.71 -      [(target, SOME (Code_Printer.complex_const_syntax (1, pretty_Char)))]))
   27.72 -  end;
   27.73 -
   27.74 -fun add_literal_string target thy =
   27.75 -  let
   27.76 -    fun pretty literals _ thm _ _ [(t, _)] =
   27.77 -      case List_Code.implode_list t
   27.78 -       of SOME ts => (case implode_string literals ts
   27.79 -             of SOME p => p
   27.80 -              | NONE => Code_Printer.eqn_error thy thm "Illegal string literal expression")
   27.81 -        | NONE => Code_Printer.eqn_error thy thm "Illegal string literal expression";
   27.82 -  in
   27.83 -    thy
   27.84 -    |> Code_Target.set_printings (Code_Symbol.Constant (@{const_name STR},
   27.85 -      [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))]))
   27.86 -  end;
   27.87 -
   27.88 -end;
    28.1 --- a/src/HOL/Tools/string_syntax.ML	Tue Apr 24 14:17:57 2018 +0000
    28.2 +++ b/src/HOL/Tools/string_syntax.ML	Tue Apr 24 14:17:58 2018 +0000
    28.3 @@ -1,10 +1,19 @@
    28.4  (*  Title:      HOL/Tools/string_syntax.ML
    28.5      Author:     Makarius
    28.6  
    28.7 -Concrete syntax for chars and strings.
    28.8 +Concrete syntax for characters and strings.
    28.9  *)
   28.10  
   28.11 -structure String_Syntax: sig end =
   28.12 +signature STRING_SYNTAX = sig
   28.13 +  val hex: int -> string
   28.14 +  val mk_bits_syntax: int -> int -> term list
   28.15 +  val dest_bits_syntax: term list -> int
   28.16 +  val plain_strings_of: string -> string list
   28.17 +  datatype character = Char of string | Ord of int
   28.18 +  val classify_character: int -> character
   28.19 +end
   28.20 +
   28.21 +structure String_Syntax: STRING_SYNTAX =
   28.22  struct
   28.23  
   28.24  (* numeral *)
   28.25 @@ -22,47 +31,59 @@
   28.26  fun hex n = hex_prefix (map hex_digit (radixpand (16, n)));
   28.27  
   28.28  
   28.29 +(* booleans as bits *)
   28.30 +
   28.31 +fun mk_bit_syntax b =
   28.32 +  Syntax.const (if b = 1 then @{const_syntax True} else @{const_syntax False});
   28.33 +
   28.34 +fun mk_bits_syntax len = map mk_bit_syntax o Integer.radicify 2 len;
   28.35 +
   28.36 +fun dest_bit_syntax (Const (@{const_syntax True}, _)) = 1 
   28.37 +  | dest_bit_syntax (Const (@{const_syntax False}, _)) = 0
   28.38 +  | dest_bit_syntax _ = raise Match;
   28.39 +
   28.40 +val dest_bits_syntax = Integer.eval_radix 2 o map dest_bit_syntax;
   28.41 +
   28.42 +
   28.43  (* char *)
   28.44  
   28.45 -fun mk_char_syntax n =
   28.46 -  if n = 0 then Syntax.const @{const_name Groups.zero}
   28.47 -  else Syntax.const @{const_syntax Char} $ Numeral.mk_num_syntax n;
   28.48 +fun mk_char_syntax i =
   28.49 +  list_comb (Syntax.const @{const_syntax Char}, mk_bits_syntax 8 i);
   28.50  
   28.51  fun mk_char_syntax' c =
   28.52    if Symbol.is_ascii c then mk_char_syntax (ord c)
   28.53    else if c = "\<newline>" then mk_char_syntax 10
   28.54    else error ("Bad character: " ^ quote c);
   28.55  
   28.56 -fun plain_string_of str =
   28.57 +fun plain_strings_of str =
   28.58    map fst (Lexicon.explode_str (str, Position.none));
   28.59  
   28.60 -datatype character = Char of string | Ord of int | Unprintable;
   28.61 +datatype character = Char of string | Ord of int;
   28.62  
   28.63  val specials = raw_explode "\\\"`'";
   28.64  
   28.65 -fun dest_char_syntax c =
   28.66 -  case try Numeral.dest_num_syntax c of
   28.67 -    SOME n =>
   28.68 -      if n < 256 then
   28.69 -        let
   28.70 -          val s = chr n
   28.71 -        in
   28.72 -          if not (member (op =) specials s) andalso Symbol.is_ascii s andalso Symbol.is_printable s
   28.73 -          then Char s
   28.74 -          else if s = "\n" then Char "\<newline>"
   28.75 -          else Ord n
   28.76 -        end
   28.77 -      else Unprintable
   28.78 -  | NONE => Unprintable;
   28.79 +fun classify_character i =
   28.80 +  let
   28.81 +    val c = chr i
   28.82 +  in
   28.83 +    if not (member (op =) specials c) andalso Symbol.is_ascii c andalso Symbol.is_printable c
   28.84 +    then Char c
   28.85 +    else if c = "\n"
   28.86 +    then Char "\<newline>"
   28.87 +    else Ord i
   28.88 +  end;
   28.89 +
   28.90 +fun dest_char_syntax b0 b1 b2 b3 b4 b5 b6 b7 =
   28.91 +  classify_character (dest_bits_syntax [b0, b1, b2, b3, b4, b5, b6, b7])
   28.92  
   28.93  fun dest_char_ast (Ast.Appl [Ast.Constant @{syntax_const "_Char"}, Ast.Constant s]) =
   28.94 -      plain_string_of s
   28.95 +      plain_strings_of s
   28.96    | dest_char_ast _ = raise Match;
   28.97  
   28.98  fun char_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
   28.99        c $ char_tr [t] $ u
  28.100    | char_tr [Free (str, _)] =
  28.101 -      (case plain_string_of str of
  28.102 +      (case plain_strings_of str of
  28.103          [c] => mk_char_syntax' c
  28.104        | _ => error ("Single character expected: " ^ str))
  28.105    | char_tr ts = raise TERM ("char_tr", ts);
  28.106 @@ -73,15 +94,12 @@
  28.107        (mk_char_syntax o #value o Lexicon.read_num) num
  28.108    | char_ord_tr ts = raise TERM ("char_ord_tr", ts);
  28.109  
  28.110 -fun char_tr' [t] = (case dest_char_syntax t of
  28.111 +fun char_tr' [b1, b2, b3, b4, b5, b6, b7, b8] =
  28.112 +      (case dest_char_syntax b1 b2 b3 b4 b5 b6 b7 b8 of
  28.113          Char s => Syntax.const @{syntax_const "_Char"} $
  28.114            Syntax.const (Lexicon.implode_str [s])
  28.115 -      | Ord n => 
  28.116 -          if n = 0
  28.117 -          then Syntax.const @{const_syntax Groups.zero}
  28.118 -          else Syntax.const @{syntax_const "_Char_ord"} $
  28.119 -            Syntax.free (hex n)
  28.120 -      | _ => raise Match)
  28.121 +      | Ord n => Syntax.const @{syntax_const "_Char_ord"} $
  28.122 +          Syntax.free (hex n))
  28.123    | char_tr' _ = raise Match;
  28.124  
  28.125  
  28.126 @@ -98,7 +116,7 @@
  28.127  fun string_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
  28.128        c $ string_tr [t] $ u
  28.129    | string_tr [Free (str, _)] =
  28.130 -      mk_string_syntax (plain_string_of str)
  28.131 +      mk_string_syntax (plain_strings_of str)
  28.132    | string_tr ts = raise TERM ("char_tr", ts);
  28.133  
  28.134  fun list_ast_tr' [args] =
  28.135 @@ -120,4 +138,4 @@
  28.136      Sign.print_ast_translation
  28.137       [(@{syntax_const "_list"}, K list_ast_tr')]);
  28.138  
  28.139 -end;
  28.140 +end
    29.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Tue Apr 24 14:17:57 2018 +0000
    29.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Tue Apr 24 14:17:58 2018 +0000
    29.3 @@ -61,7 +61,7 @@
    29.4            if Symbol.is_ascii s then ord s
    29.5            else if s = "\<newline>" then 10
    29.6            else error ("String literal contains illegal symbol: " ^ quote s ^ Position.here pos);
    29.7 -      in Syntax.const @{const_syntax Char} $ HOLogic.mk_numeral c end;
    29.8 +      in list_comb (Syntax.const @{const_syntax Char}, String_Syntax.mk_bits_syntax 8 c) end;
    29.9  
   29.10      fun mk_string [] = Const (@{const_syntax Nil}, @{typ string})
   29.11        | mk_string (s :: ss) =
    30.1 --- a/src/Pure/General/integer.ML	Tue Apr 24 14:17:57 2018 +0000
    30.2 +++ b/src/Pure/General/integer.ML	Tue Apr 24 14:17:58 2018 +0000
    30.3 @@ -20,6 +20,8 @@
    30.4    val lcm: int -> int -> int
    30.5    val gcds: int list -> int
    30.6    val lcms: int list -> int
    30.7 +  val radicify: int -> int -> int -> int list (* base -> number of positions -> value -> coefficients *)
    30.8 +  val eval_radix: int -> int list -> int (* base -> coefficients -> value *)
    30.9  end;
   30.10  
   30.11  structure Integer : INTEGER =
   30.12 @@ -64,6 +66,16 @@
   30.13  fun lcms [] = 1
   30.14    | lcms (x :: xs) = abs (Library.foldl PolyML.IntInf.lcm (x, xs));
   30.15  
   30.16 +fun radicify base len k =
   30.17 +  let
   30.18 +    val _ = if base < 2
   30.19 +      then error ("Bad radix base: " ^ string_of_int base) else ();
   30.20 +    fun shift i = swap (div_mod i base);
   30.21 +  in funpow_yield len shift k |> fst end;
   30.22 +
   30.23 +fun eval_radix base ks =
   30.24 +  fold_rev (fn k => fn i => k + i * base) ks 0;
   30.25 +
   30.26  end;
   30.27  
   30.28  (*slightly faster than Poly/ML 5.7.1 library implementation, notably on 32bit multicore*)
    31.1 --- a/src/Tools/Code/code_haskell.ML	Tue Apr 24 14:17:57 2018 +0000
    31.2 +++ b/src/Tools/Code/code_haskell.ML	Tue Apr 24 14:17:58 2018 +0000
    31.3 @@ -35,6 +35,16 @@
    31.4  
    31.5  (** Haskell serializer **)
    31.6  
    31.7 +val print_haskell_string =
    31.8 +  let
    31.9 +    fun char c =
   31.10 +      let
   31.11 +        val _ = if Symbol.is_ascii c then ()
   31.12 +          else error "non-ASCII byte in Haskell string literal";
   31.13 +        val s = ML_Syntax.print_char c;
   31.14 +      in if s = "'" then "\\'" else s end;
   31.15 +  in quote o translate_string char end;
   31.16 +
   31.17  fun print_haskell_stmt class_syntax tyco_syntax const_syntax
   31.18      reserved deresolve deriving_show =
   31.19    let
   31.20 @@ -134,7 +144,7 @@
   31.21                  :: replicate n "_"
   31.22                  @ "="
   31.23                  :: "error"
   31.24 -                @@ ML_Syntax.print_string const
   31.25 +                @@ print_haskell_string const
   31.26                );
   31.27              fun print_eqn ((ts, t), (some_thm, _)) =
   31.28                let
   31.29 @@ -426,18 +436,12 @@
   31.30  
   31.31  fun print_numeral typ = Library.enclose "(" (" :: " ^ typ ^ ")") o signed_string_of_int;
   31.32  
   31.33 -val literals = let
   31.34 -  fun char_haskell c =
   31.35 -    let
   31.36 -      val s = ML_Syntax.print_char c;
   31.37 -    in if s = "'" then "\\'" else s end;
   31.38 -in Literals {
   31.39 -  literal_char = Library.enclose "'" "'" o char_haskell,
   31.40 -  literal_string = quote o translate_string char_haskell,
   31.41 +val literals = Literals {
   31.42 +  literal_string = print_haskell_string,
   31.43    literal_numeral = print_numeral "Integer",
   31.44    literal_list = enum "," "[" "]",
   31.45    infix_cons = (5, ":")
   31.46 -} end;
   31.47 +};
   31.48  
   31.49  
   31.50  (** optional monad syntax **)
    32.1 --- a/src/Tools/Code/code_ml.ML	Tue Apr 24 14:17:57 2018 +0000
    32.2 +++ b/src/Tools/Code/code_ml.ML	Tue Apr 24 14:17:58 2018 +0000
    32.3 @@ -51,10 +51,14 @@
    32.4  
    32.5  (** SML serializer **)
    32.6  
    32.7 -fun print_char_any_ml s =
    32.8 -  if Symbol.is_char s then ML_Syntax.print_char s else "\\092" ^ unprefix "\\" s;
    32.9 +fun print_sml_char c =
   32.10 +  if c = "\\"
   32.11 +  then "\\092" (*produce strings suitable for both SML as well as Isabelle/ML*)
   32.12 +  else if Symbol.is_ascii c
   32.13 +  then ML_Syntax.print_char c
   32.14 +  else error "non-ASCII byte in SML string literal";
   32.15  
   32.16 -val print_string_any_ml = quote o implode o map print_char_any_ml o Symbol.explode;
   32.17 +val print_sml_string = quote o translate_string print_sml_char;
   32.18  
   32.19  fun print_sml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
   32.20    let
   32.21 @@ -255,7 +259,7 @@
   32.22              @ "="
   32.23              :: "raise"
   32.24              :: "Fail"
   32.25 -            @@ print_string_any_ml const
   32.26 +            @@ print_sml_string const
   32.27            ))
   32.28        | print_stmt _ (ML_Val binding) =
   32.29            let
   32.30 @@ -358,8 +362,7 @@
   32.31    );
   32.32  
   32.33  val literals_sml = Literals {
   32.34 -  literal_char = prefix "#" o quote o ML_Syntax.print_char,
   32.35 -  literal_string = print_string_any_ml,
   32.36 +  literal_string = print_sml_string,
   32.37    literal_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
   32.38    literal_list = enum "," "[" "]",
   32.39    infix_cons = (7, "::")
   32.40 @@ -368,6 +371,23 @@
   32.41  
   32.42  (** OCaml serializer **)
   32.43  
   32.44 +val print_ocaml_string =
   32.45 +  let
   32.46 +    fun chr i =
   32.47 +      let
   32.48 +        val xs = string_of_int i;
   32.49 +        val ys = replicate_string (3 - length (raw_explode xs)) "0";
   32.50 +      in "\\" ^ ys ^ xs end;
   32.51 +    fun char c =
   32.52 +      let
   32.53 +        val i = ord c;
   32.54 +        val s =
   32.55 +          if i >= 128 then error "non-ASCII byte in OCaml string literal"
   32.56 +          else if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126
   32.57 +          then chr i else c
   32.58 +      in s end;
   32.59 +  in quote o translate_string char end;
   32.60 +
   32.61  fun print_ocaml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
   32.62    let
   32.63      val deresolve_const = deresolve o Constant;
   32.64 @@ -600,7 +620,7 @@
   32.65              :: replicate n "_"
   32.66              @ "="
   32.67              :: "failwith"
   32.68 -            @@ ML_Syntax.print_string const
   32.69 +            @@ print_ocaml_string const
   32.70            ))
   32.71        | print_stmt _ (ML_Val binding) =
   32.72            let
   32.73 @@ -696,25 +716,13 @@
   32.74    );
   32.75  
   32.76  val literals_ocaml = let
   32.77 -  fun chr i =
   32.78 -    let
   32.79 -      val xs = string_of_int i;
   32.80 -      val ys = replicate_string (3 - length (raw_explode xs)) "0";
   32.81 -    in "\\" ^ ys ^ xs end;
   32.82 -  fun char_ocaml c =
   32.83 -    let
   32.84 -      val i = ord c;
   32.85 -      val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126
   32.86 -        then chr i else c
   32.87 -    in s end;
   32.88    fun numeral_ocaml k = if k < 0
   32.89      then "(Big_int.minus_big_int " ^ numeral_ocaml (~ k) ^ ")"
   32.90      else if k <= 1073741823
   32.91        then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
   32.92        else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")"
   32.93  in Literals {
   32.94 -  literal_char = Library.enclose "'" "'" o char_ocaml,
   32.95 -  literal_string = quote o translate_string char_ocaml,
   32.96 +  literal_string = print_ocaml_string,
   32.97    literal_numeral = numeral_ocaml,
   32.98    literal_list = enum ";" "[" "]",
   32.99    infix_cons = (6, "::")
    33.1 --- a/src/Tools/Code/code_printer.ML	Tue Apr 24 14:17:57 2018 +0000
    33.2 +++ b/src/Tools/Code/code_printer.ML	Tue Apr 24 14:17:58 2018 +0000
    33.3 @@ -39,11 +39,10 @@
    33.4    val aux_params: var_ctxt -> iterm list list -> string list
    33.5  
    33.6    type literals
    33.7 -  val Literals: { literal_char: string -> string, literal_string: string -> string,
    33.8 +  val Literals: { literal_string: string -> string,
    33.9          literal_numeral: int -> string,
   33.10          literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string }
   33.11      -> literals
   33.12 -  val literal_char: literals -> string -> string
   33.13    val literal_string: literals -> string -> string
   33.14    val literal_numeral: literals -> int -> string
   33.15    val literal_list: literals -> Pretty.T list -> Pretty.T
   33.16 @@ -215,7 +214,6 @@
   33.17  (** pretty literals **)
   33.18  
   33.19  datatype literals = Literals of {
   33.20 -  literal_char: string -> string,
   33.21    literal_string: string -> string,
   33.22    literal_numeral: int -> string,
   33.23    literal_list: Pretty.T list -> Pretty.T,
   33.24 @@ -224,7 +222,6 @@
   33.25  
   33.26  fun dest_Literals (Literals lits) = lits;
   33.27  
   33.28 -val literal_char = #literal_char o dest_Literals;
   33.29  val literal_string = #literal_string o dest_Literals;
   33.30  val literal_numeral = #literal_numeral o dest_Literals;
   33.31  val literal_list = #literal_list o dest_Literals;
    34.1 --- a/src/Tools/Code/code_scala.ML	Tue Apr 24 14:17:57 2018 +0000
    34.2 +++ b/src/Tools/Code/code_scala.ML	Tue Apr 24 14:17:58 2018 +0000
    34.3 @@ -23,6 +23,24 @@
    34.4  
    34.5  val target = "Scala";
    34.6  
    34.7 +val print_scala_string =
    34.8 +  let
    34.9 +    fun chr i = "\\u" ^ align_right "0" 4 (Int.fmt StringCvt.HEX i)
   34.10 +    fun char c = if c = "'" then "\\'"
   34.11 +      else if c = "\"" then "\\\""
   34.12 +      else if c = "\\" then "\\\\"
   34.13 +      else
   34.14 +        let
   34.15 +          val i = ord c
   34.16 +        in
   34.17 +          if i < 32 orelse i > 126
   34.18 +          then chr i
   34.19 +          else if i >= 128
   34.20 +          then error "non-ASCII byte in Haskell string literal"
   34.21 +          else c
   34.22 +        end
   34.23 +  in quote o translate_string char end;
   34.24 +
   34.25  datatype scala_stmt = Fun of typscheme * ((iterm list * iterm) * (thm option * bool)) list
   34.26    | Datatype of vname list * ((string * vname list) * itype list) list
   34.27    | Class of (vname * ((class * class) list * (string * itype) list))
   34.28 @@ -189,7 +207,7 @@
   34.29              val vars = intro_vars params reserved;
   34.30            in
   34.31              concat [print_defhead tyvars vars const vs params tys ty',
   34.32 -              str ("sys.error(\"" ^ const ^ "\")")]
   34.33 +              str ("sys.error(" ^ print_scala_string const ^ ")")]
   34.34            end
   34.35        | print_def const (vs, ty) eqs =
   34.36            let
   34.37 @@ -432,19 +450,12 @@
   34.38      >> (fn case_insensitive => serialize_scala case_insensitive));
   34.39  
   34.40  val literals = let
   34.41 -  fun char_scala c = if c = "'" then "\\'"
   34.42 -    else if c = "\"" then "\\\""
   34.43 -    else if c = "\\" then "\\\\"
   34.44 -    else let val k = ord c
   34.45 -    in if k < 32 orelse k > 126
   34.46 -    then "\\u" ^ align_right "0" 4 (Int.fmt StringCvt.HEX k) else c end
   34.47    fun numeral_scala k =
   34.48      if ~2147483647 < k andalso k <= 2147483647
   34.49      then signed_string_of_int k
   34.50      else quote (signed_string_of_int k)
   34.51  in Literals {
   34.52 -  literal_char = Library.enclose "'" "'" o char_scala,
   34.53 -  literal_string = quote o translate_string char_scala,
   34.54 +  literal_string = print_scala_string,
   34.55    literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
   34.56    literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
   34.57    infix_cons = (6, "::")