Restructured List and added "rotate"
authornipkow
Sun Nov 21 12:52:03 2004 +0100 (2004-11-21)
changeset 15302a643fcbc3468
parent 15301 26724034de5e
child 15303 eedbb8d22ca2
Restructured List and added "rotate"
src/HOL/Equiv_Relations.thy
src/HOL/List.thy
     1.1 --- a/src/HOL/Equiv_Relations.thy	Fri Nov 19 17:52:07 2004 +0100
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Sun Nov 21 12:52:03 2004 +0100
     1.3 @@ -143,6 +143,15 @@
     1.4  by(simp add: quotient_def)
     1.5  
     1.6  
     1.7 +lemma singleton_quotient: "{x}//r = {r `` {x}}"
     1.8 +by(simp add:quotient_def)
     1.9 +
    1.10 +lemma quotient_diff1:
    1.11 +  "\<lbrakk> inj_on (%a. {a}//r) A; a \<in> A \<rbrakk> \<Longrightarrow> (A - {a})//r = A//r - {a}//r"
    1.12 +apply(simp add:quotient_def inj_on_def)
    1.13 +apply blast
    1.14 +done
    1.15 +
    1.16  subsection {* Defining unary operations upon equivalence classes *}
    1.17  
    1.18  text{*A congruence-preserving function*}
     2.1 --- a/src/HOL/List.thy	Fri Nov 19 17:52:07 2004 +0100
     2.2 +++ b/src/HOL/List.thy	Sun Nov 21 12:52:03 2004 +0100
     2.3 @@ -13,6 +13,8 @@
     2.4      Nil    ("[]")
     2.5    | Cons 'a  "'a list"    (infixr "#" 65)
     2.6  
     2.7 +section{*Basic list processing functions*}
     2.8 +
     2.9  consts
    2.10    "@" :: "'a list => 'a list => 'a list"    (infixr 65)
    2.11    filter:: "('a => bool) => 'a list => 'a list"
    2.12 @@ -42,6 +44,10 @@
    2.13    null:: "'a list => bool"
    2.14    "distinct":: "'a list => bool"
    2.15    replicate :: "nat => 'a => 'a list"
    2.16 +  rotate1 :: "'a list \<Rightarrow> 'a list"
    2.17 +  rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
    2.18 +  sublist :: "'a list => nat set => 'a list"
    2.19 +
    2.20  
    2.21  nonterminals lupdbinds lupdbind
    2.22  
    2.23 @@ -92,6 +98,7 @@
    2.24    in [("size", size_tr')] end
    2.25  *}
    2.26  
    2.27 +
    2.28  primrec
    2.29  "hd(x#xs) = x"
    2.30  primrec
    2.31 @@ -181,29 +188,15 @@
    2.32  replicate_0: "replicate 0 x = []"
    2.33  replicate_Suc: "replicate (Suc n) x = x # replicate n x"
    2.34  defs
    2.35 - list_all2_def:
    2.36 - "list_all2 P xs ys == length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y)"
    2.37 -
    2.38 -
    2.39 -subsection {* Lexicographic orderings on lists *}
    2.40 -
    2.41 -consts
    2.42 -lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
    2.43 -primrec
    2.44 -"lexn r 0 = {}"
    2.45 -"lexn r (Suc n) =
    2.46 -(prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) ` (r <*lex*> lexn r n)) Int
    2.47 -{(xs,ys). length xs = Suc n \<and> length ys = Suc n}"
    2.48 -
    2.49 -constdefs
    2.50 -lex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
    2.51 -"lex r == \<Union>n. lexn r n"
    2.52 -
    2.53 -lexico :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
    2.54 -"lexico r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
    2.55 -
    2.56 -sublist :: "'a list => nat set => 'a list"
    2.57 -"sublist xs A == map fst (filter (%p. snd p : A) (zip xs [0..size xs(]))"
    2.58 +rotate1_def: "rotate1 xs == (case xs of [] \<Rightarrow> [] | x#xs \<Rightarrow> xs @ [x])"
    2.59 +rotate_def:  "rotate n == rotate1 ^ n"
    2.60 +
    2.61 +list_all2_def:
    2.62 + "list_all2 P xs ys ==
    2.63 +  length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y)"
    2.64 +
    2.65 +sublist_def:
    2.66 + "sublist xs A == map fst (filter (%p. snd p : A) (zip xs [0..size xs(]))"
    2.67  
    2.68  
    2.69  lemma not_Cons_self [simp]: "xs \<noteq> x # xs"
    2.70 @@ -219,34 +212,6 @@
    2.71  by (rule measure_induct [of length]) rules
    2.72  
    2.73  
    2.74 -subsection {* @{text lists}: the list-forming operator over sets *}
    2.75 -
    2.76 -consts lists :: "'a set => 'a list set"
    2.77 -inductive "lists A"
    2.78 - intros
    2.79 -  Nil [intro!]: "[]: lists A"
    2.80 -  Cons [intro!]: "[| a: A;l: lists A|] ==> a#l : lists A"
    2.81 -
    2.82 -inductive_cases listsE [elim!]: "x#l : lists A"
    2.83 -
    2.84 -lemma lists_mono [mono]: "A \<subseteq> B ==> lists A \<subseteq> lists B"
    2.85 -by (unfold lists.defs) (blast intro!: lfp_mono)
    2.86 -
    2.87 -lemma lists_IntI:
    2.88 -  assumes l: "l: lists A" shows "l: lists B ==> l: lists (A Int B)" using l
    2.89 -  by induct blast+
    2.90 -
    2.91 -lemma lists_Int_eq [simp]: "lists (A \<inter> B) = lists A \<inter> lists B"
    2.92 -proof (rule mono_Int [THEN equalityI])
    2.93 -  show "mono lists" by (simp add: mono_def lists_mono)
    2.94 -  show "lists A \<inter> lists B \<subseteq> lists (A \<inter> B)" by (blast intro: lists_IntI)
    2.95 -qed
    2.96 -
    2.97 -lemma append_in_lists_conv [iff]:
    2.98 -     "(xs @ ys : lists A) = (xs : lists A \<and> ys : lists A)"
    2.99 -by (induct xs) auto
   2.100 -
   2.101 -
   2.102  subsection {* @{text length} *}
   2.103  
   2.104  text {*
   2.105 @@ -645,19 +610,6 @@
   2.106    qed
   2.107  qed
   2.108  
   2.109 -lemma in_lists_conv_set: "(xs : lists A) = (\<forall>x \<in> set xs. x : A)"
   2.110 --- {* eliminate @{text lists} in favour of @{text set} *}
   2.111 -by (induct xs) auto
   2.112 -
   2.113 -lemma in_listsD [dest!]: "xs \<in> lists A ==> \<forall>x\<in>set xs. x \<in> A"
   2.114 -by (rule in_lists_conv_set [THEN iffD1])
   2.115 -
   2.116 -lemma in_listsI [intro!]: "\<forall>x\<in>set xs. x \<in> A ==> xs \<in> lists A"
   2.117 -by (rule in_lists_conv_set [THEN iffD2])
   2.118 -
   2.119 -lemma lists_UNIV [simp]: "lists UNIV = UNIV"
   2.120 -by auto
   2.121 -
   2.122  lemma finite_list: "finite A ==> EX l. set l = A"
   2.123  apply (erule finite_induct, auto)
   2.124  apply (rule_tac x="x#l" in exI, auto)
   2.125 @@ -667,84 +619,12 @@
   2.126  by (induct xs) (auto simp add: card_insert_if)
   2.127  
   2.128  
   2.129 -subsection{*Sets of Lists*}
   2.130 -
   2.131 -text{*Resembles a Cartesian product: it denotes the set of lists with head
   2.132 -  drawn from @{term A} and tail drawn from @{term Xs}.*}
   2.133 -constdefs
   2.134 -  set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set"
   2.135 -   "set_Cons A XS == {z. \<exists>x xs. z = x#xs & x \<in> A & xs \<in> XS}"
   2.136 -
   2.137 -lemma [simp]: "set_Cons A {[]} = (%x. [x])`A"
   2.138 -by (auto simp add: set_Cons_def)
   2.139 -
   2.140 -text{*Yields the set of lists, all of the same length as the argument and
   2.141 -with elements drawn from the corresponding element of the argument.*}
   2.142 -consts  listset :: "'a set list \<Rightarrow> 'a list set"
   2.143 -primrec
   2.144 -   "listset []    = {[]}"
   2.145 -   "listset(A#As) = set_Cons A (listset As)"
   2.146 -
   2.147 -
   2.148 -subsection{*Lifting a Relation on List Elements to the Lists*}
   2.149 -consts  listrel :: "('a * 'a)set => ('a list * 'a list)set"
   2.150 -
   2.151 -inductive "listrel(r)"
   2.152 - intros
   2.153 -   Nil:  "([],[]) \<in> listrel r"
   2.154 -   Cons: "[| (x,y) \<in> r; (xs,ys) \<in> listrel r |] ==> (x#xs, y#ys) \<in> listrel r"
   2.155 -
   2.156 -inductive_cases listrel_Nil1 [elim!]: "([],xs) \<in> listrel r"
   2.157 -inductive_cases listrel_Nil2 [elim!]: "(xs,[]) \<in> listrel r"
   2.158 -inductive_cases listrel_Cons1 [elim!]: "(y#ys,xs) \<in> listrel r"
   2.159 -inductive_cases listrel_Cons2 [elim!]: "(xs,y#ys) \<in> listrel r"
   2.160 -
   2.161 -
   2.162 -lemma listrel_mono: "r \<subseteq> s \<Longrightarrow> listrel r \<subseteq> listrel s"
   2.163 -apply clarify  
   2.164 -apply (erule listrel.induct)
   2.165 -apply (blast intro: listrel.intros)+
   2.166 -done
   2.167 -
   2.168 -lemma listrel_subset: "r \<subseteq> A \<times> A \<Longrightarrow> listrel r \<subseteq> lists A \<times> lists A"
   2.169 -apply clarify 
   2.170 -apply (erule listrel.induct, auto) 
   2.171 -done
   2.172 -
   2.173 -lemma listrel_refl: "refl A r \<Longrightarrow> refl (lists A) (listrel r)" 
   2.174 -apply (simp add: refl_def listrel_subset Ball_def)
   2.175 -apply (rule allI) 
   2.176 -apply (induct_tac x) 
   2.177 -apply (auto intro: listrel.intros)
   2.178 -done
   2.179 -
   2.180 -lemma listrel_sym: "sym r \<Longrightarrow> sym (listrel r)" 
   2.181 -apply (auto simp add: sym_def)
   2.182 -apply (erule listrel.induct) 
   2.183 -apply (blast intro: listrel.intros)+
   2.184 -done
   2.185 -
   2.186 -lemma listrel_trans: "trans r \<Longrightarrow> trans (listrel r)" 
   2.187 -apply (simp add: trans_def)
   2.188 -apply (intro allI) 
   2.189 -apply (rule impI) 
   2.190 -apply (erule listrel.induct) 
   2.191 -apply (blast intro: listrel.intros)+
   2.192 -done
   2.193 -
   2.194 -theorem equiv_listrel: "equiv A r \<Longrightarrow> equiv (lists A) (listrel r)"
   2.195 -by (simp add: equiv_def listrel_refl listrel_sym listrel_trans) 
   2.196 -
   2.197 -lemma listrel_Nil [simp]: "listrel r `` {[]} = {[]}"
   2.198 -by (blast intro: listrel.intros)
   2.199 -
   2.200 -lemma listrel_Cons:
   2.201 -     "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})";
   2.202 -by (auto simp add: set_Cons_def intro: listrel.intros) 
   2.203 -
   2.204 -
   2.205  subsection {* @{text mem} *}
   2.206  
   2.207 +text{* Only use @{text mem} for generating executable code.  Otherwise
   2.208 +use @{prop"x : set xs"} instead --- it is much easier to reason
   2.209 +about. *}
   2.210 +
   2.211  lemma set_mem_eq: "(x mem xs) = (x : set xs)"
   2.212  by (induct xs) auto
   2.213  
   2.214 @@ -1544,6 +1424,22 @@
   2.215  done
   2.216  
   2.217  
   2.218 +lemma take_Cons':
   2.219 +     "take n (x # xs) = (if n = 0 then [] else x # take (n - 1) xs)"
   2.220 +by (cases n) simp_all
   2.221 +
   2.222 +lemma drop_Cons':
   2.223 +     "drop n (x # xs) = (if n = 0 then x # xs else drop (n - 1) xs)"
   2.224 +by (cases n) simp_all
   2.225 +
   2.226 +lemma nth_Cons': "(x # xs)!n = (if n = 0 then x else xs!(n - 1))"
   2.227 +by (cases n) simp_all
   2.228 +
   2.229 +lemmas [simp] = take_Cons'[of "number_of v",standard]
   2.230 +                drop_Cons'[of "number_of v",standard]
   2.231 +                nth_Cons'[of _ _ "number_of v",standard]
   2.232 +
   2.233 +
   2.234  subsection {* @{text "distinct"} and @{text remdups} *}
   2.235  
   2.236  lemma distinct_append [simp]:
   2.237 @@ -1704,69 +1600,82 @@
   2.238  by (simp add: set_replicate_conv_if split: split_if_asm)
   2.239  
   2.240  
   2.241 -subsection {* Lexicographic orderings on lists *}
   2.242 -
   2.243 -lemma wf_lexn: "wf r ==> wf (lexn r n)"
   2.244 -apply (induct n, simp, simp)
   2.245 -apply(rule wf_subset)
   2.246 - prefer 2 apply (rule Int_lower1)
   2.247 -apply(rule wf_prod_fun_image)
   2.248 - prefer 2 apply (rule inj_onI, auto)
   2.249 -done
   2.250 -
   2.251 -lemma lexn_length:
   2.252 -     "!!xs ys. (xs, ys) : lexn r n ==> length xs = n \<and> length ys = n"
   2.253 -by (induct n) auto
   2.254 -
   2.255 -lemma wf_lex [intro!]: "wf r ==> wf (lex r)"
   2.256 -apply (unfold lex_def)
   2.257 -apply (rule wf_UN)
   2.258 -apply (blast intro: wf_lexn, clarify)
   2.259 -apply (rename_tac m n)
   2.260 -apply (subgoal_tac "m \<noteq> n")
   2.261 - prefer 2 apply blast
   2.262 -apply (blast dest: lexn_length not_sym)
   2.263 +subsection{*@{text rotate1} and @{text rotate}*}
   2.264 +
   2.265 +lemma rotate_simps[simp]: "rotate1 [] = [] \<and> rotate1 (x#xs) = xs @ [x]"
   2.266 +by(simp add:rotate1_def)
   2.267 +
   2.268 +lemma rotate0[simp]: "rotate 0 = id"
   2.269 +by(simp add:rotate_def)
   2.270 +
   2.271 +lemma rotate_Suc[simp]: "rotate (Suc n) xs = rotate1(rotate n xs)"
   2.272 +by(simp add:rotate_def)
   2.273 +
   2.274 +lemma rotate_add:
   2.275 +  "rotate (m+n) = rotate m o rotate n"
   2.276 +by(simp add:rotate_def funpow_add)
   2.277 +
   2.278 +lemma rotate_rotate: "rotate m (rotate n xs) = rotate (m+n) xs"
   2.279 +by(simp add:rotate_add)
   2.280 +
   2.281 +lemma rotate1_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate1 xs = xs"
   2.282 +by(cases xs) simp_all
   2.283 +
   2.284 +lemma rotate_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate n xs = xs"
   2.285 +apply(induct n)
   2.286 + apply simp
   2.287 +apply (simp add:rotate_def)
   2.288  done
   2.289  
   2.290 -lemma lexn_conv:
   2.291 -"lexn r n =
   2.292 -{(xs,ys). length xs = n \<and> length ys = n \<and>
   2.293 -(\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y):r)}"
   2.294 -apply (induct n, simp, blast)
   2.295 -apply (simp add: image_Collect lex_prod_def, safe, blast)
   2.296 - apply (rule_tac x = "ab # xys" in exI, simp)
   2.297 -apply (case_tac xys, simp_all, blast)
   2.298 +lemma rotate1_hd_tl: "xs \<noteq> [] \<Longrightarrow> rotate1 xs = tl xs @ [hd xs]"
   2.299 +by(simp add:rotate1_def split:list.split)
   2.300 +
   2.301 +lemma rotate_drop_take:
   2.302 +  "rotate n xs = drop (n mod length xs) xs @ take (n mod length xs) xs"
   2.303 +apply(induct n)
   2.304 + apply simp
   2.305 +apply(simp add:rotate_def)
   2.306 +apply(cases "xs = []")
   2.307 + apply (simp)
   2.308 +apply(case_tac "n mod length xs = 0")
   2.309 + apply(simp add:mod_Suc)
   2.310 + apply(simp add: rotate1_hd_tl drop_Suc take_Suc)
   2.311 +apply(simp add:mod_Suc rotate1_hd_tl drop_Suc[symmetric] drop_tl[symmetric]
   2.312 +                take_hd_drop linorder_not_le)
   2.313  done
   2.314  
   2.315 -lemma lex_conv:
   2.316 -"lex r =
   2.317 -{(xs,ys). length xs = length ys \<and>
   2.318 -(\<exists>xys x y xs' ys'. xs = xys @ x # xs' \<and> ys = xys @ y # ys' \<and> (x, y):r)}"
   2.319 -by (force simp add: lex_def lexn_conv)
   2.320 -
   2.321 -lemma wf_lexico [intro!]: "wf r ==> wf (lexico r)"
   2.322 -by (unfold lexico_def) blast
   2.323 -
   2.324 -lemma lexico_conv:
   2.325 -"lexico r = {(xs,ys). length xs < length ys |
   2.326 -length xs = length ys \<and> (xs, ys) : lex r}"
   2.327 -by (simp add: lexico_def diag_def lex_prod_def measure_def inv_image_def)
   2.328 -
   2.329 -lemma Nil_notin_lex [iff]: "([], ys) \<notin> lex r"
   2.330 -by (simp add: lex_conv)
   2.331 -
   2.332 -lemma Nil2_notin_lex [iff]: "(xs, []) \<notin> lex r"
   2.333 -by (simp add:lex_conv)
   2.334 -
   2.335 -lemma Cons_in_lex [iff]:
   2.336 -"((x # xs, y # ys) : lex r) =
   2.337 -((x, y) : r \<and> length xs = length ys | x = y \<and> (xs, ys) : lex r)"
   2.338 -apply (simp add: lex_conv)
   2.339 -apply (rule iffI)
   2.340 - prefer 2 apply (blast intro: Cons_eq_appendI, clarify)
   2.341 -apply (case_tac xys, simp, simp)
   2.342 -apply blast
   2.343 -done
   2.344 +lemma rotate_conv_mod: "rotate n xs = rotate (n mod length xs) xs"
   2.345 +by(simp add:rotate_drop_take)
   2.346 +
   2.347 +lemma rotate_id[simp]: "n mod length xs = 0 \<Longrightarrow> rotate n xs = xs"
   2.348 +by(simp add:rotate_drop_take)
   2.349 +
   2.350 +lemma length_rotate1[simp]: "length(rotate1 xs) = length xs"
   2.351 +by(simp add:rotate1_def split:list.split)
   2.352 +
   2.353 +lemma length_rotate[simp]: "!!xs. length(rotate n xs) = length xs"
   2.354 +by (induct n) (simp_all add:rotate_def)
   2.355 +
   2.356 +lemma distinct1_rotate[simp]: "distinct(rotate1 xs) = distinct xs"
   2.357 +by(simp add:rotate1_def split:list.split) blast
   2.358 +
   2.359 +lemma distinct_rotate[simp]: "distinct(rotate n xs) = distinct xs"
   2.360 +by (induct n) (simp_all add:rotate_def)
   2.361 +
   2.362 +lemma rotate_map: "rotate n (map f xs) = map f (rotate n xs)"
   2.363 +by(simp add:rotate_drop_take take_map drop_map)
   2.364 +
   2.365 +lemma set_rotate1[simp]: "set(rotate1 xs) = set xs"
   2.366 +by(simp add:rotate1_def split:list.split)
   2.367 +
   2.368 +lemma set_rotate[simp]: "set(rotate n xs) = set xs"
   2.369 +by (induct n) (simp_all add:rotate_def)
   2.370 +
   2.371 +lemma rotate1_is_Nil_conv[simp]: "(rotate1 xs = []) = (xs = [])"
   2.372 +by(simp add:rotate1_def split:list.split)
   2.373 +
   2.374 +lemma rotate_is_Nil_conv[simp]: "(rotate n xs = []) = (xs = [])"
   2.375 +by (induct n) (simp_all add:rotate_def)
   2.376  
   2.377  
   2.378  subsection {* @{text sublist} --- a generalization of @{text nth} to sets *}
   2.379 @@ -1847,40 +1756,212 @@
   2.380  done
   2.381  
   2.382  
   2.383 -lemma take_Cons':
   2.384 -     "take n (x # xs) = (if n = 0 then [] else x # take (n - 1) xs)"
   2.385 -by (cases n) simp_all
   2.386 -
   2.387 -lemma drop_Cons':
   2.388 -     "drop n (x # xs) = (if n = 0 then x # xs else drop (n - 1) xs)"
   2.389 -by (cases n) simp_all
   2.390 -
   2.391 -lemma nth_Cons': "(x # xs)!n = (if n = 0 then x else xs!(n - 1))"
   2.392 -by (cases n) simp_all
   2.393 -
   2.394 -lemmas [simp] = take_Cons'[of "number_of v",standard]
   2.395 -                drop_Cons'[of "number_of v",standard]
   2.396 -                nth_Cons'[of _ _ "number_of v",standard]
   2.397 -
   2.398 -
   2.399 -lemma "card (set xs) = size xs \<Longrightarrow> distinct xs"
   2.400 -proof (induct xs)
   2.401 -  case Nil thus ?case by simp
   2.402 -next
   2.403 -  case (Cons x xs)
   2.404 -  show ?case
   2.405 -  proof (cases "x \<in> set xs")
   2.406 -    case False with Cons show ?thesis by simp
   2.407 -  next
   2.408 -    case True with Cons.prems
   2.409 -    have "card (set xs) = Suc (length xs)" 
   2.410 -      by (simp add: card_insert_if split: split_if_asm)
   2.411 -    moreover have "card (set xs) \<le> length xs" by (rule card_length)
   2.412 -    ultimately have False by simp
   2.413 -    thus ?thesis ..
   2.414 -  qed
   2.415 +subsection{*Sets of Lists*}
   2.416 +
   2.417 +subsection {* @{text lists}: the list-forming operator over sets *}
   2.418 +
   2.419 +consts lists :: "'a set => 'a list set"
   2.420 +inductive "lists A"
   2.421 + intros
   2.422 +  Nil [intro!]: "[]: lists A"
   2.423 +  Cons [intro!]: "[| a: A;l: lists A|] ==> a#l : lists A"
   2.424 +
   2.425 +inductive_cases listsE [elim!]: "x#l : lists A"
   2.426 +
   2.427 +lemma lists_mono [mono]: "A \<subseteq> B ==> lists A \<subseteq> lists B"
   2.428 +by (unfold lists.defs) (blast intro!: lfp_mono)
   2.429 +
   2.430 +lemma lists_IntI:
   2.431 +  assumes l: "l: lists A" shows "l: lists B ==> l: lists (A Int B)" using l
   2.432 +  by induct blast+
   2.433 +
   2.434 +lemma lists_Int_eq [simp]: "lists (A \<inter> B) = lists A \<inter> lists B"
   2.435 +proof (rule mono_Int [THEN equalityI])
   2.436 +  show "mono lists" by (simp add: mono_def lists_mono)
   2.437 +  show "lists A \<inter> lists B \<subseteq> lists (A \<inter> B)" by (blast intro: lists_IntI)
   2.438  qed
   2.439  
   2.440 +lemma append_in_lists_conv [iff]:
   2.441 +     "(xs @ ys : lists A) = (xs : lists A \<and> ys : lists A)"
   2.442 +by (induct xs) auto
   2.443 +
   2.444 +lemma in_lists_conv_set: "(xs : lists A) = (\<forall>x \<in> set xs. x : A)"
   2.445 +-- {* eliminate @{text lists} in favour of @{text set} *}
   2.446 +by (induct xs) auto
   2.447 +
   2.448 +lemma in_listsD [dest!]: "xs \<in> lists A ==> \<forall>x\<in>set xs. x \<in> A"
   2.449 +by (rule in_lists_conv_set [THEN iffD1])
   2.450 +
   2.451 +lemma in_listsI [intro!]: "\<forall>x\<in>set xs. x \<in> A ==> xs \<in> lists A"
   2.452 +by (rule in_lists_conv_set [THEN iffD2])
   2.453 +
   2.454 +lemma lists_UNIV [simp]: "lists UNIV = UNIV"
   2.455 +by auto
   2.456 +
   2.457 +subsection{*Lists as Cartesian products*}
   2.458 +
   2.459 +text{*@{text"set_Cons A Xs"}: the set of lists with head drawn from
   2.460 +@{term A} and tail drawn from @{term Xs}.*}
   2.461 +
   2.462 +constdefs
   2.463 +  set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set"
   2.464 +  "set_Cons A XS == {z. \<exists>x xs. z = x#xs & x \<in> A & xs \<in> XS}"
   2.465 +
   2.466 +lemma [simp]: "set_Cons A {[]} = (%x. [x])`A"
   2.467 +by (auto simp add: set_Cons_def)
   2.468 +
   2.469 +text{*Yields the set of lists, all of the same length as the argument and
   2.470 +with elements drawn from the corresponding element of the argument.*}
   2.471 +
   2.472 +consts  listset :: "'a set list \<Rightarrow> 'a list set"
   2.473 +primrec
   2.474 +   "listset []    = {[]}"
   2.475 +   "listset(A#As) = set_Cons A (listset As)"
   2.476 +
   2.477 +
   2.478 +section{*Relations on lists*}
   2.479 +
   2.480 +subsection {* Lexicographic orderings on lists *}
   2.481 +
   2.482 +consts
   2.483 +lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
   2.484 +primrec
   2.485 +"lexn r 0 = {}"
   2.486 +"lexn r (Suc n) =
   2.487 +(prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) ` (r <*lex*> lexn r n)) Int
   2.488 +{(xs,ys). length xs = Suc n \<and> length ys = Suc n}"
   2.489 +
   2.490 +constdefs
   2.491 +lex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
   2.492 +"lex r == \<Union>n. lexn r n"
   2.493 +
   2.494 +lexico :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
   2.495 +"lexico r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
   2.496 +
   2.497 +
   2.498 +lemma wf_lexn: "wf r ==> wf (lexn r n)"
   2.499 +apply (induct n, simp, simp)
   2.500 +apply(rule wf_subset)
   2.501 + prefer 2 apply (rule Int_lower1)
   2.502 +apply(rule wf_prod_fun_image)
   2.503 + prefer 2 apply (rule inj_onI, auto)
   2.504 +done
   2.505 +
   2.506 +lemma lexn_length:
   2.507 +     "!!xs ys. (xs, ys) : lexn r n ==> length xs = n \<and> length ys = n"
   2.508 +by (induct n) auto
   2.509 +
   2.510 +lemma wf_lex [intro!]: "wf r ==> wf (lex r)"
   2.511 +apply (unfold lex_def)
   2.512 +apply (rule wf_UN)
   2.513 +apply (blast intro: wf_lexn, clarify)
   2.514 +apply (rename_tac m n)
   2.515 +apply (subgoal_tac "m \<noteq> n")
   2.516 + prefer 2 apply blast
   2.517 +apply (blast dest: lexn_length not_sym)
   2.518 +done
   2.519 +
   2.520 +lemma lexn_conv:
   2.521 +"lexn r n =
   2.522 +{(xs,ys). length xs = n \<and> length ys = n \<and>
   2.523 +(\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y):r)}"
   2.524 +apply (induct n, simp, blast)
   2.525 +apply (simp add: image_Collect lex_prod_def, safe, blast)
   2.526 + apply (rule_tac x = "ab # xys" in exI, simp)
   2.527 +apply (case_tac xys, simp_all, blast)
   2.528 +done
   2.529 +
   2.530 +lemma lex_conv:
   2.531 +"lex r =
   2.532 +{(xs,ys). length xs = length ys \<and>
   2.533 +(\<exists>xys x y xs' ys'. xs = xys @ x # xs' \<and> ys = xys @ y # ys' \<and> (x, y):r)}"
   2.534 +by (force simp add: lex_def lexn_conv)
   2.535 +
   2.536 +lemma wf_lexico [intro!]: "wf r ==> wf (lexico r)"
   2.537 +by (unfold lexico_def) blast
   2.538 +
   2.539 +lemma lexico_conv:
   2.540 +"lexico r = {(xs,ys). length xs < length ys |
   2.541 +length xs = length ys \<and> (xs, ys) : lex r}"
   2.542 +by (simp add: lexico_def diag_def lex_prod_def measure_def inv_image_def)
   2.543 +
   2.544 +lemma Nil_notin_lex [iff]: "([], ys) \<notin> lex r"
   2.545 +by (simp add: lex_conv)
   2.546 +
   2.547 +lemma Nil2_notin_lex [iff]: "(xs, []) \<notin> lex r"
   2.548 +by (simp add:lex_conv)
   2.549 +
   2.550 +lemma Cons_in_lex [iff]:
   2.551 +"((x # xs, y # ys) : lex r) =
   2.552 +((x, y) : r \<and> length xs = length ys | x = y \<and> (xs, ys) : lex r)"
   2.553 +apply (simp add: lex_conv)
   2.554 +apply (rule iffI)
   2.555 + prefer 2 apply (blast intro: Cons_eq_appendI, clarify)
   2.556 +apply (case_tac xys, simp, simp)
   2.557 +apply blast
   2.558 +done
   2.559 +
   2.560 +
   2.561 +subsection{*Lifting a Relation on List Elements to the Lists*}
   2.562 +
   2.563 +consts  listrel :: "('a * 'a)set => ('a list * 'a list)set"
   2.564 +
   2.565 +inductive "listrel(r)"
   2.566 + intros
   2.567 +   Nil:  "([],[]) \<in> listrel r"
   2.568 +   Cons: "[| (x,y) \<in> r; (xs,ys) \<in> listrel r |] ==> (x#xs, y#ys) \<in> listrel r"
   2.569 +
   2.570 +inductive_cases listrel_Nil1 [elim!]: "([],xs) \<in> listrel r"
   2.571 +inductive_cases listrel_Nil2 [elim!]: "(xs,[]) \<in> listrel r"
   2.572 +inductive_cases listrel_Cons1 [elim!]: "(y#ys,xs) \<in> listrel r"
   2.573 +inductive_cases listrel_Cons2 [elim!]: "(xs,y#ys) \<in> listrel r"
   2.574 +
   2.575 +
   2.576 +lemma listrel_mono: "r \<subseteq> s \<Longrightarrow> listrel r \<subseteq> listrel s"
   2.577 +apply clarify  
   2.578 +apply (erule listrel.induct)
   2.579 +apply (blast intro: listrel.intros)+
   2.580 +done
   2.581 +
   2.582 +lemma listrel_subset: "r \<subseteq> A \<times> A \<Longrightarrow> listrel r \<subseteq> lists A \<times> lists A"
   2.583 +apply clarify 
   2.584 +apply (erule listrel.induct, auto) 
   2.585 +done
   2.586 +
   2.587 +lemma listrel_refl: "refl A r \<Longrightarrow> refl (lists A) (listrel r)" 
   2.588 +apply (simp add: refl_def listrel_subset Ball_def)
   2.589 +apply (rule allI) 
   2.590 +apply (induct_tac x) 
   2.591 +apply (auto intro: listrel.intros)
   2.592 +done
   2.593 +
   2.594 +lemma listrel_sym: "sym r \<Longrightarrow> sym (listrel r)" 
   2.595 +apply (auto simp add: sym_def)
   2.596 +apply (erule listrel.induct) 
   2.597 +apply (blast intro: listrel.intros)+
   2.598 +done
   2.599 +
   2.600 +lemma listrel_trans: "trans r \<Longrightarrow> trans (listrel r)" 
   2.601 +apply (simp add: trans_def)
   2.602 +apply (intro allI) 
   2.603 +apply (rule impI) 
   2.604 +apply (erule listrel.induct) 
   2.605 +apply (blast intro: listrel.intros)+
   2.606 +done
   2.607 +
   2.608 +theorem equiv_listrel: "equiv A r \<Longrightarrow> equiv (lists A) (listrel r)"
   2.609 +by (simp add: equiv_def listrel_refl listrel_sym listrel_trans) 
   2.610 +
   2.611 +lemma listrel_Nil [simp]: "listrel r `` {[]} = {[]}"
   2.612 +by (blast intro: listrel.intros)
   2.613 +
   2.614 +lemma listrel_Cons:
   2.615 +     "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})";
   2.616 +by (auto simp add: set_Cons_def intro: listrel.intros) 
   2.617 +
   2.618 +
   2.619 +section{*Miscellany*}
   2.620 +
   2.621  subsection {* Characters and strings *}
   2.622  
   2.623  datatype nibble =