# HG changeset patch
# User haftmann
# Date 1519645972 0
# Node ID 5152afa6258fb419b5f6d82f8495e6174850be18
# Parent  d97a28a006f9d1aaaa4df1d64407d7bea61a2f5b
dedicated append function for string literals

diff -r d97a28a006f9 -r 5152afa6258f src/HOL/String.thy
--- a/src/HOL/String.thy	Mon Feb 26 09:58:47 2018 +0100
+++ b/src/HOL/String.thy	Mon Feb 26 11:52:52 2018 +0000
@@ -352,6 +352,22 @@
   shows "HOL.equal s s \<longleftrightarrow> True"
   by (simp add: equal)
 
+instantiation literal :: plus
+begin
+
+lift_definition plus_literal :: "literal \<Rightarrow> literal \<Rightarrow> literal"
+  is "(@)"
+  .
+
+instance ..
+
+end
+
+lemma [code]:
+  "s + t = String.implode (String.explode s @ String.explode t)"
+  using plus_literal.abs_eq [of "String.explode s" "String.explode t"]
+  by (simp add: explode_inverse implode_def)
+
 lifting_update literal.lifting
 lifting_forget literal.lifting
 
@@ -411,6 +427,11 @@
     and (OCaml) "failwith"
     and (Haskell) "!(error/ ::/ forall a./ String -> (() -> a) -> a)"
     and (Scala) "!{/ sys.error((_));/  ((_)).apply(())/ }"
+| constant "(+) :: literal \<Rightarrow> literal \<Rightarrow> literal" \<rightharpoonup>
+    (SML) infixl 18 "^"
+    and (OCaml) infixr 6 "@"
+    and (Haskell) infixr 5 "++"
+    and (Scala) infixl 7 "+"
 
 hide_type (open) literal