# HG changeset patch
# User haftmann
# Date 1519645973 0
# Node ID f91c437f6f6893ea911a4fde572cbf94524b7f64
# Parent  5152afa6258fb419b5f6d82f8495e6174850be18
new lemma

diff -r 5152afa6258f -r f91c437f6f68 src/HOL/Library/More_List.thy
--- a/src/HOL/Library/More_List.thy	Mon Feb 26 11:52:52 2018 +0000
+++ b/src/HOL/Library/More_List.thy	Mon Feb 26 11:52:53 2018 +0000
@@ -268,6 +268,11 @@
   "nth_default dflt xs k = dflt \<longleftrightarrow> (k < length xs \<longrightarrow> xs ! k = dflt)"
   by (simp add: nth_default_def)
 
+lemma nth_default_take_eq:
+  "nth_default dflt (take m xs) n =
+    (if n < m then nth_default dflt xs n else dflt)"
+  by (simp add: nth_default_def)
+
 lemma in_enumerate_iff_nth_default_eq:
   "x \<noteq> dflt \<Longrightarrow> (n, x) \<in> set (enumerate 0 xs) \<longleftrightarrow> nth_default dflt xs n = x"
   by (auto simp add: nth_default_def in_set_conv_nth enumerate_eq_zip)
diff -r 5152afa6258f -r f91c437f6f68 src/HOL/String.thy
--- a/src/HOL/String.thy	Mon Feb 26 11:52:52 2018 +0000
+++ b/src/HOL/String.thy	Mon Feb 26 11:52:53 2018 +0000
@@ -352,6 +352,21 @@
   shows "HOL.equal s s \<longleftrightarrow> True"
   by (simp add: equal)
 
+instantiation literal :: zero
+begin
+
+lift_definition zero_literal :: "literal"
+  is "[]"
+  .
+
+instance ..
+
+end
+
+lemma [code]:
+  "0 = STR ''''"
+  by (fact zero_literal.abs_eq)
+
 instantiation literal :: plus
 begin
 
@@ -368,6 +383,9 @@
   using plus_literal.abs_eq [of "String.explode s" "String.explode t"]
   by (simp add: explode_inverse implode_def)
 
+instance literal :: monoid_add
+  by standard (transfer; simp)+
+
 lifting_update literal.lifting
 lifting_forget literal.lifting