# HG changeset patch
# User paulson
# Date 1112699138 -7200
# Node ID 988f91b9c4efd9bd4f5e9af002fffebfe5538737
# Parent  157f3988f7752bf325e6bc67b202f28aa3dcb5ef
lexicographic order by Norbert Voelker

diff -r 157f3988f775 -r 988f91b9c4ef src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Apr 05 13:05:20 2005 +0200
+++ b/src/HOL/List.thy	Tue Apr 05 13:05:38 2005 +0200
@@ -1889,24 +1889,29 @@
    "listset(A#As) = set_Cons A (listset As)"
 
 
-subsection{*Relations on lists*}
-
-subsubsection {* Lexicographic orderings on lists *}
-
-consts
-lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
+subsection{*Relations on Lists*}
+
+subsubsection {* Length Lexicographic Ordering *}
+
+text{*These orderings preserve well-foundedness: shorter lists 
+  precede longer lists. These ordering are not used in dictionaries.*}
+
+consts lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
+        --{*The lexicographic ordering for lists of the specified length*}
 primrec
-"lexn r 0 = {}"
-"lexn r (Suc n) =
-(prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) ` (r <*lex*> lexn r n)) Int
-{(xs,ys). length xs = Suc n \<and> length ys = Suc n}"
+  "lexn r 0 = {}"
+  "lexn r (Suc n) =
+    (prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) ` (r <*lex*> lexn r n)) Int
+    {(xs,ys). length xs = Suc n \<and> length ys = Suc n}"
 
 constdefs
-lex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
-"lex r == \<Union>n. lexn r n"
-
-lexico :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
-"lexico r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
+  lex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
+    "lex r == \<Union>n. lexn r n"
+        --{*Holds only between lists of the same length*}
+
+  lexico :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
+    "lexico r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
+        --{*Compares lists by their length and then lexicographically*}
 
 
 lemma wf_lexn: "wf r ==> wf (lexn r n)"
@@ -1932,9 +1937,9 @@
 done
 
 lemma lexn_conv:
-"lexn r n =
-{(xs,ys). length xs = n \<and> length ys = n \<and>
-(\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y):r)}"
+  "lexn r n =
+    {(xs,ys). length xs = n \<and> length ys = n \<and>
+    (\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y):r)}"
 apply (induct n, simp, blast)
 apply (simp add: image_Collect lex_prod_def, safe, blast)
  apply (rule_tac x = "ab # xys" in exI, simp)
@@ -1942,17 +1947,17 @@
 done
 
 lemma lex_conv:
-"lex r =
-{(xs,ys). length xs = length ys \<and>
-(\<exists>xys x y xs' ys'. xs = xys @ x # xs' \<and> ys = xys @ y # ys' \<and> (x, y):r)}"
+  "lex r =
+    {(xs,ys). length xs = length ys \<and>
+    (\<exists>xys x y xs' ys'. xs = xys @ x # xs' \<and> ys = xys @ y # ys' \<and> (x, y):r)}"
 by (force simp add: lex_def lexn_conv)
 
 lemma wf_lexico [intro!]: "wf r ==> wf (lexico r)"
 by (unfold lexico_def) blast
 
 lemma lexico_conv:
-"lexico r = {(xs,ys). length xs < length ys |
-length xs = length ys \<and> (xs, ys) : lex r}"
+    "lexico r = {(xs,ys). length xs < length ys |
+                 length xs = length ys \<and> (xs, ys) : lex r}"
 by (simp add: lexico_def diag_def lex_prod_def measure_def inv_image_def)
 
 lemma Nil_notin_lex [iff]: "([], ys) \<notin> lex r"
@@ -1962,8 +1967,8 @@
 by (simp add:lex_conv)
 
 lemma Cons_in_lex [iff]:
-"((x # xs, y # ys) : lex r) =
-((x, y) : r \<and> length xs = length ys | x = y \<and> (xs, ys) : lex r)"
+    "((x # xs, y # ys) : lex r) =
+      ((x, y) : r \<and> length xs = length ys | x = y \<and> (xs, ys) : lex r)"
 apply (simp add: lex_conv)
 apply (rule iffI)
  prefer 2 apply (blast intro: Cons_eq_appendI, clarify)
@@ -1972,6 +1977,101 @@
 done
 
 
+subsubsection {* Lexicographic Ordering *}
+
+text {* Classical lexicographic ordering on lists, ie. "a" < "ab" < "b".
+    This ordering does \emph{not} preserve well-foundedness.
+     Author: N. Voelker, March 2005 *} 
+
+constdefs 
+  lexord :: "('a * 'a)set \<Rightarrow> ('a list * 'a list) set" 
+  "lexord  r == {(x,y). \<exists> a v. y = x @ a # v \<or> 
+            (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
+
+lemma lexord_Nil_left[simp]:  "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
+  by (unfold lexord_def, induct_tac y, auto) 
+
+lemma lexord_Nil_right[simp]: "(x,[]) \<notin> lexord r"
+  by (unfold lexord_def, induct_tac x, auto)
+
+lemma lexord_cons_cons[simp]:
+     "((a # x, b # y) \<in> lexord r) = ((a,b)\<in> r | (a = b & (x,y)\<in> lexord r))"
+  apply (unfold lexord_def, safe, simp_all)
+  apply (case_tac u, simp, simp)
+  apply (case_tac u, simp, clarsimp, blast, blast, clarsimp)
+  apply (erule_tac x="b # u" in allE)
+  by force
+
+lemmas lexord_simps = lexord_Nil_left lexord_Nil_right lexord_cons_cons
+
+lemma lexord_append_rightI: "\<exists> b z. y = b # z \<Longrightarrow> (x, x @ y) \<in> lexord r"
+  by (induct_tac x, auto)  
+
+lemma lexord_append_left_rightI:
+     "(a,b) \<in> r \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"
+  by (induct_tac u, auto)
+
+lemma lexord_append_leftI: " (u,v) \<in> lexord r \<Longrightarrow> (x @ u, x @ v) \<in> lexord r"
+  by (induct x, auto)
+
+lemma lexord_append_leftD:
+     "\<lbrakk> (x @ u, x @ v) \<in> lexord r; (! a. (a,a) \<notin> r) \<rbrakk> \<Longrightarrow> (u,v) \<in> lexord r"
+  by (erule rev_mp, induct_tac x, auto)
+
+lemma lexord_take_index_conv: 
+   "((x,y) : lexord r) = 
+    ((length x < length y \<and> take (length x) y = x) \<or> 
+     (\<exists>i. i < min(length x)(length y) & take i x = take i y & (x!i,y!i) \<in> r))"
+  apply (unfold lexord_def Let_def, clarsimp) 
+  apply (rule_tac f = "(% a b. a \<or> b)" in arg_cong2)
+  apply auto 
+  apply (rule_tac x="hd (drop (length x) y)" in exI)
+  apply (rule_tac x="tl (drop (length x) y)" in exI)
+  apply (erule subst, simp add: min_def) 
+  apply (rule_tac x ="length u" in exI, simp) 
+  apply (rule_tac x ="take i x" in exI) 
+  apply (rule_tac x ="x ! i" in exI) 
+  apply (rule_tac x ="y ! i" in exI, safe) 
+  apply (rule_tac x="drop (Suc i) x" in exI)
+  apply (drule sym, simp add: drop_Suc_conv_tl) 
+  apply (rule_tac x="drop (Suc i) y" in exI)
+  by (simp add: drop_Suc_conv_tl) 
+
+-- {* lexord is extension of partial ordering List.lex *} 
+lemma lexord_lex: " (x,y) \<in> lex r = ((x,y) \<in> lexord r \<and> length x = length y)"
+  apply (rule_tac x = y in spec) 
+  apply (induct_tac x, clarsimp) 
+  by (clarify, case_tac x, simp, force)
+
+lemma lexord_irreflexive: "(! x. (x,x) \<notin> r) \<Longrightarrow> (y,y) \<notin> lexord r"
+  by (induct y, auto)
+
+lemma lexord_trans: 
+    "\<lbrakk> (x, y) \<in> lexord r; (y, z) \<in> lexord r; trans r \<rbrakk> \<Longrightarrow> (x, z) \<in> lexord r"
+   apply (erule rev_mp)+
+   apply (rule_tac x = x in spec) 
+  apply (rule_tac x = z in spec) 
+  apply ( induct_tac y, simp, clarify)
+  apply (case_tac xa, erule ssubst) 
+  apply (erule allE, erule allE) -- {* avoid simp recursion *} 
+  apply (case_tac x, simp, simp) 
+  apply (case_tac x, erule allE, erule allE, simp) 
+  apply (erule_tac x = listb in allE) 
+  apply (erule_tac x = lista in allE, simp)
+  apply (unfold trans_def)
+  by blast
+
+lemma lexord_transI:  "trans r \<Longrightarrow> trans (lexord r)"
+  by (rule transI, drule lexord_trans, blast) 
+
+lemma lexord_linear: "(! a b. (a,b)\<in> r | a = b | (b,a) \<in> r) \<Longrightarrow> (x,y) : lexord r | x = y | (y,x) : lexord r"
+  apply (rule_tac x = y in spec) 
+  apply (induct_tac x, rule allI) 
+  apply (case_tac x, simp, simp) 
+  apply (rule allI, case_tac x, simp, simp) 
+  by blast
+
+
 subsubsection{*Lifting a Relation on List Elements to the Lists*}
 
 consts  listrel :: "('a * 'a)set => ('a list * 'a list)set"