# HG changeset patch
# User Andreas Lochbihler
# Date 1385545431 -3600
# Node ID 33a68b7f2736ba5303c5e646f16cdfb4cceb699c
# Parent  5836854ca0a8027acf3faa79339b5ee8b840ef42# Parent  4af7c82463d36cf54e195afbd8cf74c2b3c4d1f3
merged

diff -r 5836854ca0a8 -r 33a68b7f2736 src/HOL/Library/Char_ord.thy
--- a/src/HOL/Library/Char_ord.thy	Tue Nov 26 15:54:03 2013 +0100
+++ b/src/HOL/Library/Char_ord.thy	Wed Nov 27 10:43:51 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
diff -r 5836854ca0a8 -r 33a68b7f2736 src/HOL/Library/Code_Char.thy
--- a/src/HOL/Library/Code_Char.thy	Tue Nov 26 15:54:03 2013 +0100
+++ b/src/HOL/Library/Code_Char.thy	Wed Nov 27 10:43:51 2013 +0100
@@ -97,6 +97,18 @@
     and (Haskell) infix 4 "<"
     and (Scala) infixl 4 "<"
     and (Eval) infixl 6 "<"
+|  constant "Orderings.less_eq :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
+    (SML) "!((_ : string) <= _)"
+    and (OCaml) "!((_ : string) <= _)"
+    and (Haskell) infix 4 "<="
+    and (Scala) infixl 4 "<="
+    and (Eval) infixl 6 "<="
+| constant "Orderings.less :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
+    (SML) "!((_ : string) < _)"
+    and (OCaml) "!((_ : string) < _)"
+    and (Haskell) infix 4 "<"
+    and (Scala) infixl 4 "<"
+    and (Eval) infixl 6 "<"
 
 end
 
diff -r 5836854ca0a8 -r 33a68b7f2736 src/HOL/Library/List_lexord.thy
--- a/src/HOL/Library/List_lexord.thy	Tue Nov 26 15:54:03 2013 +0100
+++ b/src/HOL/Library/List_lexord.thy	Wed Nov 27 10:43:51 2013 +0100
@@ -118,4 +118,6 @@
   "(x\<Colon>'a\<Colon>{equal, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
   by simp_all
 
+code_printing class_instance String.literal :: ord \<rightharpoonup> (Haskell) -
+
 end
diff -r 5836854ca0a8 -r 33a68b7f2736 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Nov 26 15:54:03 2013 +0100
+++ b/src/HOL/List.thy	Wed Nov 27 10:43:51 2013 +0100
@@ -5390,6 +5390,176 @@
   apply (rule allI, case_tac x, simp, simp) 
   by blast
 
+text {*
+  Predicate version of lexicographic order integrated with Isabelle's order type classes.
+  Author: Andreas Lochbihler
+*}
+
+thm not_less
+context ord begin
+
+inductive lexordp :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+where
+  Nil: "lexordp [] (y # ys)"
+| Cons: "x < y \<Longrightarrow> lexordp (x # xs) (y # ys)"
+| Cons_eq:
+  "\<lbrakk> \<not> x < y; \<not> y < x; lexordp xs ys \<rbrakk> \<Longrightarrow> lexordp (x # xs) (y # ys)"
+
+lemma lexordp_simps [simp]:
+  "lexordp [] ys = (ys \<noteq> [])"
+  "lexordp xs [] = False"
+  "lexordp (x # xs) (y # ys) \<longleftrightarrow> x < y \<or> \<not> y < x \<and> lexordp xs ys"
+by(subst lexordp.simps, fastforce simp add: neq_Nil_conv)+
+
+inductive lexordp_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
+  Nil: "lexordp_eq [] ys"
+| Cons: "x < y \<Longrightarrow> lexordp_eq (x # xs) (y # ys)"
+| Cons_eq: "\<lbrakk> \<not> x < y; \<not> y < x; lexordp_eq xs ys \<rbrakk> \<Longrightarrow> lexordp_eq (x # xs) (y # ys)"
+
+lemma lexordp_eq_simps [simp]:
+  "lexordp_eq [] ys = True"
+  "lexordp_eq xs [] \<longleftrightarrow> xs = []"
+  "lexordp_eq (x # xs) [] = False"
+  "lexordp_eq (x # xs) (y # ys) \<longleftrightarrow> x < y \<or> \<not> y < x \<and> lexordp_eq xs ys"
+by(subst lexordp_eq.simps, fastforce)+
+
+lemma lexordp_append_rightI: "ys \<noteq> Nil \<Longrightarrow> lexordp xs (xs @ ys)"
+by(induct xs)(auto simp add: neq_Nil_conv)
+
+lemma lexordp_append_left_rightI: "x < y \<Longrightarrow> lexordp (us @ x # xs) (us @ y # ys)"
+by(induct us) auto
+
+lemma lexordp_eq_refl: "lexordp_eq xs xs"
+by(induct xs) simp_all
+
+lemma lexordp_append_leftI: "lexordp us vs \<Longrightarrow> lexordp (xs @ us) (xs @ vs)"
+by(induct xs) auto
+
+lemma lexordp_append_leftD: "\<lbrakk> lexordp (xs @ us) (xs @ vs); \<forall>a. \<not> a < a \<rbrakk> \<Longrightarrow> lexordp us vs"
+by(induct xs) auto
+
+lemma lexordp_irreflexive: 
+  assumes irrefl: "\<forall>x. \<not> x < x"
+  shows "\<not> lexordp xs xs"
+proof
+  assume "lexordp xs xs"
+  thus False by(induct xs ys\<equiv>xs)(simp_all add: irrefl)
+qed
+
+lemma lexordp_into_lexordp_eq:
+  assumes "lexordp xs ys"
+  shows "lexordp_eq xs ys"
+using assms by induct simp_all
+
+end
+
+declare ord.lexordp_simps [simp, code]
+declare ord.lexordp_eq_simps [code, simp]
+
+lemma lexord_code [code, code_unfold]: "lexordp = ord.lexordp less"
+unfolding lexordp_def ord.lexordp_def ..
+
+context order begin
+
+lemma lexordp_antisym:
+  assumes "lexordp xs ys" "lexordp ys xs"
+  shows False
+using assms by induct auto
+
+lemma lexordp_irreflexive': "\<not> lexordp xs xs"
+by(rule lexordp_irreflexive) simp
+
+end
+
+context linorder begin
+
+lemma lexordp_cases [consumes 1, case_names Nil Cons Cons_eq, cases pred: lexordp]:
+  assumes "lexordp xs ys"
+  obtains (Nil) y ys' where "xs = []" "ys = y # ys'"
+  | (Cons) x xs' y ys' where "xs = x # xs'" "ys = y # ys'" "x < y"
+  | (Cons_eq) x xs' ys' where "xs = x # xs'" "ys = x # ys'" "lexordp xs' ys'"
+using assms by cases (fastforce simp add: not_less_iff_gr_or_eq)+
+
+lemma lexordp_induct [consumes 1, case_names Nil Cons Cons_eq, induct pred: lexordp]:
+  assumes major: "lexordp xs ys"
+  and Nil: "\<And>y ys. P [] (y # ys)"
+  and Cons: "\<And>x xs y ys. x < y \<Longrightarrow> P (x # xs) (y # ys)"
+  and Cons_eq: "\<And>x xs ys. \<lbrakk> lexordp xs ys; P xs ys \<rbrakk> \<Longrightarrow> P (x # xs) (x # ys)"
+  shows "P xs ys"
+using major by induct (simp_all add: Nil Cons not_less_iff_gr_or_eq Cons_eq)
+
+lemma lexordp_iff:
+  "lexordp xs ys \<longleftrightarrow> (\<exists>x vs. ys = xs @ x # vs) \<or> (\<exists>us a b vs ws. a < b \<and> xs = us @ a # vs \<and> ys = us @ b # ws)"
+  (is "?lhs = ?rhs")
+proof
+  assume ?lhs thus ?rhs
+  proof induct
+    case Cons_eq thus ?case by simp (metis append.simps(2))
+  qed(fastforce intro: disjI2 del: disjCI intro: exI[where x="[]"])+
+next
+  assume ?rhs thus ?lhs
+    by(auto intro: lexordp_append_leftI[where us="[]", simplified] lexordp_append_leftI)
+qed
+
+lemma lexordp_conv_lexord:
+  "lexordp xs ys \<longleftrightarrow> (xs, ys) \<in> lexord {(x, y). x < y}"
+by(simp add: lexordp_iff lexord_def)
+
+lemma lexordp_eq_antisym: 
+  assumes "lexordp_eq xs ys" "lexordp_eq ys xs" 
+  shows "xs = ys"
+using assms by induct simp_all
+
+lemma lexordp_eq_trans:
+  assumes "lexordp_eq xs ys" and "lexordp_eq ys zs"
+  shows "lexordp_eq xs zs"
+using assms
+apply(induct arbitrary: zs)
+apply(case_tac [2-3] zs)
+apply auto
+done
+
+lemma lexordp_trans:
+  assumes "lexordp xs ys" "lexordp ys zs"
+  shows "lexordp xs zs"
+using assms
+apply(induct arbitrary: zs)
+apply(case_tac [2-3] zs)
+apply auto
+done
+
+lemma lexordp_linear: "lexordp xs ys \<or> xs = ys \<or> lexordp ys xs"
+proof(induct xs arbitrary: ys)
+  case Nil thus ?case by(cases ys) simp_all
+next
+  case Cons thus ?case by(cases ys) auto
+qed
+
+lemma lexordp_conv_lexordp_eq: "lexordp xs ys \<longleftrightarrow> lexordp_eq xs ys \<and> \<not> lexordp_eq ys xs"
+  (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  assume ?lhs
+  moreover hence "\<not> lexordp_eq ys xs" by induct simp_all
+  ultimately show ?rhs by(simp add: lexordp_into_lexordp_eq)
+next
+  assume ?rhs
+  hence "lexordp_eq xs ys" "\<not> lexordp_eq ys xs" by simp_all
+  thus ?lhs by induct simp_all
+qed
+
+lemma lexordp_eq_conv_lexord: "lexordp_eq xs ys \<longleftrightarrow> xs = ys \<or> lexordp xs ys"
+by(auto simp add: lexordp_conv_lexordp_eq lexordp_eq_refl dest: lexordp_eq_antisym)
+
+lemma lexordp_eq_linear: "lexordp_eq xs ys \<or> lexordp_eq ys xs"
+apply(induct xs arbitrary: ys)
+apply(case_tac [!] ys)
+apply auto
+done
+
+lemma lexordp_linorder: "class.linorder lexordp_eq lexordp"
+by unfold_locales(auto simp add: lexordp_conv_lexordp_eq lexordp_eq_refl lexordp_eq_antisym intro: lexordp_eq_trans del: disjCI intro: lexordp_eq_linear)
+
+end
 
 subsubsection {* Lexicographic combination of measure functions *}
 
diff -r 5836854ca0a8 -r 33a68b7f2736 src/HOL/String.thy
--- a/src/HOL/String.thy	Tue Nov 26 15:54:03 2013 +0100
+++ b/src/HOL/String.thy	Wed Nov 27 10:43:51 2013 +0100
@@ -358,6 +358,8 @@
 typedef literal = "UNIV :: string set"
   morphisms explode STR ..
 
+setup_lifting (no_code) type_definition_literal
+
 instantiation literal :: size
 begin
 
@@ -372,16 +374,14 @@
 instantiation literal :: equal
 begin
 
-definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool"
-where
-  "equal_literal s1 s2 \<longleftrightarrow> explode s1 = explode s2"
+lift_definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool" is "op =" .
 
-instance
-proof
-qed (auto simp add: equal_literal_def explode_inject)
+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"
@@ -391,7 +391,6 @@
   "STR xs = STR ys \<longleftrightarrow> xs = ys"
   by (simp add: STR_inject)
 
-
 subsection {* Code generator *}
 
 ML_file "Tools/string_code.ML"