src/HOL/String.thy

 subsection {* Strings as dedicated type *}
 
 typedef literal = "UNIV :: string set"
   morphisms explode STR ..
 
+setup_lifting (no_code) type_definition_literal
+
 instantiation literal :: size
 begin
 
 definition size_literal :: "literal \<Rightarrow> nat"
 where

 end
 
 instantiation literal :: equal
 begin
 
-definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool"
-where
-  "equal_literal s1 s2 \<longleftrightarrow> explode s1 = explode s2"
-
-instance
-proof
-qed (auto simp add: equal_literal_def explode_inject)
-
-end
+lift_definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool" is "op =" .
+
+instance by intro_classes (transfer, simp)
+
+end
+
+declare equal_literal.rep_eq[code]
 
 lemma [code nbe]:
   fixes s :: "String.literal"
   shows "HOL.equal s s \<longleftrightarrow> True"
   by (simp add: equal)
 
 lemma STR_inject' [simp]:
   "STR xs = STR ys \<longleftrightarrow> xs = ys"
   by (simp add: STR_inject)
-
 
 subsection {* Code generator *}
 
 ML_file "Tools/string_code.ML"