src/HOL/List.thy
changeset 15656 988f91b9c4ef
parent 15570 8d8c70b41bab
child 15693 3a67e61c6e96
     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.85  by (simp add:lex_conv)
    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.92  apply (simp add: lex_conv)
    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"