qualified String.explode and String.implode
authorhaftmann
Mon Jun 30 08:00:36 2014 +0200 (2014-06-30)
changeset 574370baf08c075b9
parent 57436 995f7ebd50ae
child 57438 663037c5d848
qualified String.explode and String.implode
NEWS
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Library/Char_ord.thy
src/HOL/Library/Code_Char.thy
src/HOL/Library/Countable.thy
src/HOL/String.thy
     1.1 --- a/NEWS	Sun Jun 29 21:07:53 2014 +0200
     1.2 +++ b/NEWS	Mon Jun 30 08:00:36 2014 +0200
     1.3 @@ -178,6 +178,8 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Qualified String.implode and String.explode.  INCOMPATIBILITY.
     1.8 +
     1.9  * Command and antiquotation ''value'' are hardcoded against nbe and
    1.10  ML now.  Minor INCOMPATIBILITY.
    1.11  
     2.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Sun Jun 29 21:07:53 2014 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jun 30 08:00:36 2014 +0200
     2.3 @@ -546,7 +546,7 @@
     2.4  subsubsection {* Logical intermediate layer *}
     2.5  
     2.6  definition raise' :: "String.literal \<Rightarrow> 'a Heap" where
     2.7 -  [code del]: "raise' s = raise (explode s)"
     2.8 +  [code del]: "raise' s = raise (String.explode s)"
     2.9  
    2.10  lemma [code_abbrev]: "raise' (STR s) = raise s"
    2.11    unfolding raise'_def by (simp add: STR_inverse)
     3.1 --- a/src/HOL/Library/Char_ord.thy	Sun Jun 29 21:07:53 2014 +0200
     3.2 +++ b/src/HOL/Library/Char_ord.thy	Mon Jun 30 08:00:36 2014 +0200
     3.3 @@ -113,11 +113,11 @@
     3.4  end
     3.5  
     3.6  lemma less_literal_code [code]: 
     3.7 -  "op < = (\<lambda>xs ys. ord.lexordp op < (explode xs) (explode ys))"
     3.8 +  "op < = (\<lambda>xs ys. ord.lexordp op < (String.explode xs) (String.explode ys))"
     3.9  by(simp add: less_literal.rep_eq fun_eq_iff)
    3.10  
    3.11  lemma less_eq_literal_code [code]:
    3.12 -  "op \<le> = (\<lambda>xs ys. ord.lexordp_eq op < (explode xs) (explode ys))"
    3.13 +  "op \<le> = (\<lambda>xs ys. ord.lexordp_eq op < (String.explode xs) (String.explode ys))"
    3.14  by(simp add: less_eq_literal.rep_eq fun_eq_iff)
    3.15  
    3.16  lifting_update literal.lifting
     4.1 --- a/src/HOL/Library/Code_Char.thy	Sun Jun 29 21:07:53 2014 +0200
     4.2 +++ b/src/HOL/Library/Code_Char.thy	Mon Jun 30 08:00:36 2014 +0200
     4.3 @@ -40,18 +40,15 @@
     4.4  code_reserved Scala
     4.5    char
     4.6  
     4.7 -definition implode :: "string \<Rightarrow> String.literal" where
     4.8 -  "implode = STR"
     4.9 -
    4.10  code_reserved SML String
    4.11  
    4.12  code_printing
    4.13 -  constant implode \<rightharpoonup>
    4.14 +  constant String.implode \<rightharpoonup>
    4.15      (SML) "String.implode"
    4.16      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)"
    4.17      and (Haskell) "_"
    4.18      and (Scala) "!(\"\" ++/ _)"
    4.19 -| constant explode \<rightharpoonup>
    4.20 +| constant String.explode \<rightharpoonup>
    4.21      (SML) "String.explode"
    4.22      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) [])"
    4.23      and (Haskell) "_"
     5.1 --- a/src/HOL/Library/Countable.thy	Sun Jun 29 21:07:53 2014 +0200
     5.2 +++ b/src/HOL/Library/Countable.thy	Mon Jun 30 08:00:36 2014 +0200
     5.3 @@ -104,7 +104,7 @@
     5.4  text {* Further *}
     5.5  
     5.6  instance String.literal :: countable
     5.7 -  by (rule countable_classI [of "to_nat o explode"])
     5.8 +  by (rule countable_classI [of "to_nat o String.explode"])
     5.9      (auto simp add: explode_inject)
    5.10  
    5.11  text {* Functions *}
     6.1 --- a/src/HOL/String.thy	Sun Jun 29 21:07:53 2014 +0200
     6.2 +++ b/src/HOL/String.thy	Mon Jun 30 08:00:36 2014 +0200
     6.3 @@ -358,6 +358,10 @@
     6.4  
     6.5  setup_lifting (no_code) type_definition_literal
     6.6  
     6.7 +definition implode :: "string \<Rightarrow> String.literal"
     6.8 +where
     6.9 +  "implode = STR"
    6.10 +
    6.11  instantiation literal :: size
    6.12  begin
    6.13  
    6.14 @@ -440,4 +444,6 @@
    6.15  
    6.16  hide_type (open) literal
    6.17  
    6.18 +hide_const (open) implode explode
    6.19 +
    6.20  end