--- 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)
--- 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