# HG changeset patch
# User Andreas Lochbihler
# Date 1384942355 -3600
# Node ID a2eeeb335a48dafb81d415a3410237a74ddc9788
# Parent  a2d1522cdd54ac0b34233d5c2c4c1252c065c485
instantiate linorder for String.literal by lexicographic order

diff -r a2d1522cdd54 -r a2eeeb335a48 src/HOL/Library/Char_ord.thy
--- a/src/HOL/Library/Char_ord.thy	Wed Nov 20 11:10:05 2013 +0100
+++ b/src/HOL/Library/Char_ord.thy	Wed Nov 20 11:12:35 2013 +0100
@@ -94,6 +94,30 @@
 
 end
 
+instantiation String.literal :: linorder
+begin
+
+lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp op <" .
+lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp_eq op <" .
+
+instance
+proof -
+  interpret linorder "ord.lexordp_eq op <" "ord.lexordp op < :: string \<Rightarrow> string \<Rightarrow> bool"
+    by(rule linorder.lexordp_linorder[where less_eq="op \<le>"])(unfold_locales)
+  show "PROP ?thesis"
+    by(intro_classes)(transfer, simp add: less_le_not_le linear)+
+qed
+
+end
+
+lemma less_literal_code [code]: 
+  "op < = (\<lambda>xs ys. ord.lexordp op < (explode xs) (explode ys))"
+by(simp add: less_literal.rep_eq fun_eq_iff)
+
+lemma less_eq_literal_code [code]:
+  "op \<le> = (\<lambda>xs ys. ord.lexordp_eq op < (explode xs) (explode ys))"
+by(simp add: less_eq_literal.rep_eq fun_eq_iff)
+
 text {* Legacy aliasses *}
 
 lemmas nibble_less_eq_def = less_eq_nibble_def