author paulson Tue Apr 05 13:05:38 2005 +0200 (2005-04-05 ago) changeset 15656 988f91b9c4ef parent 15655 157f3988f775 child 15657 bd946fbc7c2b
lexicographic order by Norbert Voelker
 src/HOL/List.thy file | annotate | diff | revisions
     1.1 --- a/src/HOL/List.thy	Tue Apr 05 13:05:20 2005 +0200
1.2 +++ b/src/HOL/List.thy	Tue Apr 05 13:05:38 2005 +0200
1.3 @@ -1889,24 +1889,29 @@
1.4     "listset(A#As) = set_Cons A (listset As)"
1.5
1.6
1.7 -subsection{*Relations on lists*}
1.8 -
1.9 -subsubsection {* Lexicographic orderings on lists *}
1.10 -
1.11 -consts
1.12 -lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
1.13 +subsection{*Relations on Lists*}
1.14 +
1.15 +subsubsection {* Length Lexicographic Ordering *}
1.16 +
1.17 +text{*These orderings preserve well-foundedness: shorter lists
1.18 +  precede longer lists. These ordering are not used in dictionaries.*}
1.19 +
1.20 +consts lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
1.21 +        --{*The lexicographic ordering for lists of the specified length*}
1.22  primrec
1.23 -"lexn r 0 = {}"
1.24 -"lexn r (Suc n) =
1.25 -(prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs)  (r <*lex*> lexn r n)) Int
1.26 -{(xs,ys). length xs = Suc n \<and> length ys = Suc n}"
1.27 +  "lexn r 0 = {}"
1.28 +  "lexn r (Suc n) =
1.29 +    (prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs)  (r <*lex*> lexn r n)) Int
1.30 +    {(xs,ys). length xs = Suc n \<and> length ys = Suc n}"
1.31
1.32  constdefs
1.33 -lex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
1.34 -"lex r == \<Union>n. lexn r n"
1.35 -
1.36 -lexico :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
1.37 -"lexico r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
1.38 +  lex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
1.39 +    "lex r == \<Union>n. lexn r n"
1.40 +        --{*Holds only between lists of the same length*}
1.41 +
1.42 +  lexico :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
1.43 +    "lexico r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
1.44 +        --{*Compares lists by their length and then lexicographically*}
1.45
1.46
1.47  lemma wf_lexn: "wf r ==> wf (lexn r n)"
1.48 @@ -1932,9 +1937,9 @@
1.49  done
1.50
1.51  lemma lexn_conv:
1.52 -"lexn r n =
1.53 -{(xs,ys). length xs = n \<and> length ys = n \<and>
1.54 -(\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y):r)}"
1.55 +  "lexn r n =
1.56 +    {(xs,ys). length xs = n \<and> length ys = n \<and>
1.57 +    (\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y):r)}"
1.58  apply (induct n, simp, blast)
1.59  apply (simp add: image_Collect lex_prod_def, safe, blast)
1.60   apply (rule_tac x = "ab # xys" in exI, simp)
1.61 @@ -1942,17 +1947,17 @@
1.62  done
1.63
1.64  lemma lex_conv:
1.65 -"lex r =
1.66 -{(xs,ys). length xs = length ys \<and>
1.67 -(\<exists>xys x y xs' ys'. xs = xys @ x # xs' \<and> ys = xys @ y # ys' \<and> (x, y):r)}"
1.68 +  "lex r =
1.69 +    {(xs,ys). length xs = length ys \<and>
1.70 +    (\<exists>xys x y xs' ys'. xs = xys @ x # xs' \<and> ys = xys @ y # ys' \<and> (x, y):r)}"
1.71  by (force simp add: lex_def lexn_conv)
1.72
1.73  lemma wf_lexico [intro!]: "wf r ==> wf (lexico r)"
1.74  by (unfold lexico_def) blast
1.75
1.76  lemma lexico_conv:
1.77 -"lexico r = {(xs,ys). length xs < length ys |
1.78 -length xs = length ys \<and> (xs, ys) : lex r}"
1.79 +    "lexico r = {(xs,ys). length xs < length ys |
1.80 +                 length xs = length ys \<and> (xs, ys) : lex r}"
1.81  by (simp add: lexico_def diag_def lex_prod_def measure_def inv_image_def)
1.82
1.83  lemma Nil_notin_lex [iff]: "([], ys) \<notin> lex r"
1.84 @@ -1962,8 +1967,8 @@
1.86
1.87  lemma Cons_in_lex [iff]:
1.88 -"((x # xs, y # ys) : lex r) =
1.89 -((x, y) : r \<and> length xs = length ys | x = y \<and> (xs, ys) : lex r)"
1.90 +    "((x # xs, y # ys) : lex r) =
1.91 +      ((x, y) : r \<and> length xs = length ys | x = y \<and> (xs, ys) : lex r)"
1.93  apply (rule iffI)
1.94   prefer 2 apply (blast intro: Cons_eq_appendI, clarify)
1.95 @@ -1972,6 +1977,101 @@
1.96  done
1.97
1.98
1.99 +subsubsection {* Lexicographic Ordering *}
1.100 +
1.101 +text {* Classical lexicographic ordering on lists, ie. "a" < "ab" < "b".
1.102 +    This ordering does \emph{not} preserve well-foundedness.
1.103 +     Author: N. Voelker, March 2005 *}
1.104 +
1.105 +constdefs
1.106 +  lexord :: "('a * 'a)set \<Rightarrow> ('a list * 'a list) set"
1.107 +  "lexord  r == {(x,y). \<exists> a v. y = x @ a # v \<or>
1.108 +            (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
1.109 +
1.110 +lemma lexord_Nil_left[simp]:  "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
1.111 +  by (unfold lexord_def, induct_tac y, auto)
1.112 +
1.113 +lemma lexord_Nil_right[simp]: "(x,[]) \<notin> lexord r"
1.114 +  by (unfold lexord_def, induct_tac x, auto)
1.115 +
1.116 +lemma lexord_cons_cons[simp]:
1.117 +     "((a # x, b # y) \<in> lexord r) = ((a,b)\<in> r | (a = b & (x,y)\<in> lexord r))"
1.118 +  apply (unfold lexord_def, safe, simp_all)
1.119 +  apply (case_tac u, simp, simp)
1.120 +  apply (case_tac u, simp, clarsimp, blast, blast, clarsimp)
1.121 +  apply (erule_tac x="b # u" in allE)
1.122 +  by force
1.123 +
1.124 +lemmas lexord_simps = lexord_Nil_left lexord_Nil_right lexord_cons_cons
1.125 +
1.126 +lemma lexord_append_rightI: "\<exists> b z. y = b # z \<Longrightarrow> (x, x @ y) \<in> lexord r"
1.127 +  by (induct_tac x, auto)
1.128 +
1.129 +lemma lexord_append_left_rightI:
1.130 +     "(a,b) \<in> r \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"
1.131 +  by (induct_tac u, auto)
1.132 +
1.133 +lemma lexord_append_leftI: " (u,v) \<in> lexord r \<Longrightarrow> (x @ u, x @ v) \<in> lexord r"
1.134 +  by (induct x, auto)
1.135 +
1.136 +lemma lexord_append_leftD:
1.137 +     "\<lbrakk> (x @ u, x @ v) \<in> lexord r; (! a. (a,a) \<notin> r) \<rbrakk> \<Longrightarrow> (u,v) \<in> lexord r"
1.138 +  by (erule rev_mp, induct_tac x, auto)
1.139 +
1.140 +lemma lexord_take_index_conv:
1.141 +   "((x,y) : lexord r) =
1.142 +    ((length x < length y \<and> take (length x) y = x) \<or>
1.143 +     (\<exists>i. i < min(length x)(length y) & take i x = take i y & (x!i,y!i) \<in> r))"
1.144 +  apply (unfold lexord_def Let_def, clarsimp)
1.145 +  apply (rule_tac f = "(% a b. a \<or> b)" in arg_cong2)
1.146 +  apply auto
1.147 +  apply (rule_tac x="hd (drop (length x) y)" in exI)
1.148 +  apply (rule_tac x="tl (drop (length x) y)" in exI)
1.149 +  apply (erule subst, simp add: min_def)
1.150 +  apply (rule_tac x ="length u" in exI, simp)
1.151 +  apply (rule_tac x ="take i x" in exI)
1.152 +  apply (rule_tac x ="x ! i" in exI)
1.153 +  apply (rule_tac x ="y ! i" in exI, safe)
1.154 +  apply (rule_tac x="drop (Suc i) x" in exI)
1.155 +  apply (drule sym, simp add: drop_Suc_conv_tl)
1.156 +  apply (rule_tac x="drop (Suc i) y" in exI)
1.157 +  by (simp add: drop_Suc_conv_tl)
1.158 +
1.159 +-- {* lexord is extension of partial ordering List.lex *}
1.160 +lemma lexord_lex: " (x,y) \<in> lex r = ((x,y) \<in> lexord r \<and> length x = length y)"
1.161 +  apply (rule_tac x = y in spec)
1.162 +  apply (induct_tac x, clarsimp)
1.163 +  by (clarify, case_tac x, simp, force)
1.164 +
1.165 +lemma lexord_irreflexive: "(! x. (x,x) \<notin> r) \<Longrightarrow> (y,y) \<notin> lexord r"
1.166 +  by (induct y, auto)
1.167 +
1.168 +lemma lexord_trans:
1.169 +    "\<lbrakk> (x, y) \<in> lexord r; (y, z) \<in> lexord r; trans r \<rbrakk> \<Longrightarrow> (x, z) \<in> lexord r"
1.170 +   apply (erule rev_mp)+
1.171 +   apply (rule_tac x = x in spec)
1.172 +  apply (rule_tac x = z in spec)
1.173 +  apply ( induct_tac y, simp, clarify)
1.174 +  apply (case_tac xa, erule ssubst)
1.175 +  apply (erule allE, erule allE) -- {* avoid simp recursion *}
1.176 +  apply (case_tac x, simp, simp)
1.177 +  apply (case_tac x, erule allE, erule allE, simp)
1.178 +  apply (erule_tac x = listb in allE)
1.179 +  apply (erule_tac x = lista in allE, simp)
1.180 +  apply (unfold trans_def)
1.181 +  by blast
1.182 +
1.183 +lemma lexord_transI:  "trans r \<Longrightarrow> trans (lexord r)"
1.184 +  by (rule transI, drule lexord_trans, blast)
1.185 +
1.186 +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"
1.187 +  apply (rule_tac x = y in spec)
1.188 +  apply (induct_tac x, rule allI)
1.189 +  apply (case_tac x, simp, simp)
1.190 +  apply (rule allI, case_tac x, simp, simp)
1.191 +  by blast
1.192 +
1.193 +
1.194  subsubsection{*Lifting a Relation on List Elements to the Lists*}
1.195
1.196  consts  listrel :: "('a * 'a)set => ('a list * 'a list)set"