--- 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
--- 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
--- 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
--- 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 *}
--- 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"