src/HOL/List.thy
changeset 50548 0aec55e63795
parent 50422 ee729dbd1b7f
child 51096 60e4b75fefe1
     1.1 --- a/src/HOL/List.thy	Fri Dec 14 18:41:56 2012 +0100
     1.2 +++ b/src/HOL/List.thy	Fri Dec 14 19:51:20 2012 +0100
     1.3 @@ -23,52 +23,42 @@
     1.4  
     1.5  subsection {* Basic list processing functions *}
     1.6  
     1.7 -primrec
     1.8 -  hd :: "'a list \<Rightarrow> 'a" where
     1.9 -  "hd (x # xs) = x"
    1.10 -
    1.11 -primrec
    1.12 -  tl :: "'a list \<Rightarrow> 'a list" where
    1.13 -    "tl [] = []"
    1.14 -  | "tl (x # xs) = xs"
    1.15 -
    1.16 -primrec
    1.17 -  last :: "'a list \<Rightarrow> 'a" where
    1.18 -  "last (x # xs) = (if xs = [] then x else last xs)"
    1.19 -
    1.20 -primrec
    1.21 -  butlast :: "'a list \<Rightarrow> 'a list" where
    1.22 -    "butlast []= []"
    1.23 -  | "butlast (x # xs) = (if xs = [] then [] else x # butlast xs)"
    1.24 -
    1.25 -primrec
    1.26 -  set :: "'a list \<Rightarrow> 'a set" where
    1.27 -    "set [] = {}"
    1.28 -  | "set (x # xs) = insert x (set xs)"
    1.29 -
    1.30 -definition
    1.31 -  coset :: "'a list \<Rightarrow> 'a set" where
    1.32 -  [simp]: "coset xs = - set xs"
    1.33 -
    1.34 -primrec
    1.35 -  map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
    1.36 -    "map f [] = []"
    1.37 -  | "map f (x # xs) = f x # map f xs"
    1.38 -
    1.39 -primrec
    1.40 -  append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) where
    1.41 -    append_Nil:"[] @ ys = ys"
    1.42 -  | append_Cons: "(x#xs) @ ys = x # xs @ ys"
    1.43 -
    1.44 -primrec
    1.45 -  rev :: "'a list \<Rightarrow> 'a list" where
    1.46 -    "rev [] = []"
    1.47 -  | "rev (x # xs) = rev xs @ [x]"
    1.48 -
    1.49 -primrec
    1.50 -  filter:: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    1.51 -    "filter P [] = []"
    1.52 -  | "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"
    1.53 +primrec hd :: "'a list \<Rightarrow> 'a" where
    1.54 +"hd (x # xs) = x"
    1.55 +
    1.56 +primrec tl :: "'a list \<Rightarrow> 'a list" where
    1.57 +"tl [] = []" |
    1.58 +"tl (x # xs) = xs"
    1.59 +
    1.60 +primrec last :: "'a list \<Rightarrow> 'a" where
    1.61 +"last (x # xs) = (if xs = [] then x else last xs)"
    1.62 +
    1.63 +primrec butlast :: "'a list \<Rightarrow> 'a list" where
    1.64 +"butlast []= []" |
    1.65 +"butlast (x # xs) = (if xs = [] then [] else x # butlast xs)"
    1.66 +
    1.67 +primrec set :: "'a list \<Rightarrow> 'a set" where
    1.68 +"set [] = {}" |
    1.69 +"set (x # xs) = insert x (set xs)"
    1.70 +
    1.71 +definition coset :: "'a list \<Rightarrow> 'a set" where
    1.72 +[simp]: "coset xs = - set xs"
    1.73 +
    1.74 +primrec map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
    1.75 +"map f [] = []" |
    1.76 +"map f (x # xs) = f x # map f xs"
    1.77 +
    1.78 +primrec append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) where
    1.79 +append_Nil: "[] @ ys = ys" |
    1.80 +append_Cons: "(x#xs) @ ys = x # xs @ ys"
    1.81 +
    1.82 +primrec rev :: "'a list \<Rightarrow> 'a list" where
    1.83 +"rev [] = []" |
    1.84 +"rev (x # xs) = rev xs @ [x]"
    1.85 +
    1.86 +primrec filter:: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    1.87 +"filter P [] = []" |
    1.88 +"filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"
    1.89  
    1.90  syntax
    1.91    -- {* Special syntax for filter *}
    1.92 @@ -82,54 +72,46 @@
    1.93  syntax (HTML output)
    1.94    "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
    1.95  
    1.96 -primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b"
    1.97 -where
    1.98 -  fold_Nil:  "fold f [] = id"
    1.99 -| fold_Cons: "fold f (x # xs) = fold f xs \<circ> f x" -- {* natural argument order *}
   1.100 -
   1.101 -primrec foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b"
   1.102 -where
   1.103 -  foldr_Nil:  "foldr f [] = id"
   1.104 -| foldr_Cons: "foldr f (x # xs) = f x \<circ> foldr f xs" -- {* natural argument order *}
   1.105 -
   1.106 -primrec foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
   1.107 -where
   1.108 -  foldl_Nil:  "foldl f a [] = a"
   1.109 -| foldl_Cons: "foldl f a (x # xs) = foldl f (f a x) xs"
   1.110 -
   1.111 -primrec
   1.112 -  concat:: "'a list list \<Rightarrow> 'a list" where
   1.113 -    "concat [] = []"
   1.114 -  | "concat (x # xs) = x @ concat xs"
   1.115 -
   1.116 -definition (in monoid_add)
   1.117 -  listsum :: "'a list \<Rightarrow> 'a" where
   1.118 -  "listsum xs = foldr plus xs 0"
   1.119 -
   1.120 -primrec
   1.121 -  drop:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   1.122 -    drop_Nil: "drop n [] = []"
   1.123 -  | drop_Cons: "drop n (x # xs) = (case n of 0 \<Rightarrow> x # xs | Suc m \<Rightarrow> drop m xs)"
   1.124 +primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
   1.125 +fold_Nil:  "fold f [] = id" |
   1.126 +fold_Cons: "fold f (x # xs) = fold f xs \<circ> f x"
   1.127 +
   1.128 +primrec foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
   1.129 +foldr_Nil:  "foldr f [] = id" |
   1.130 +foldr_Cons: "foldr f (x # xs) = f x \<circ> foldr f xs"
   1.131 +
   1.132 +primrec foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b" where
   1.133 +foldl_Nil:  "foldl f a [] = a" |
   1.134 +foldl_Cons: "foldl f a (x # xs) = foldl f (f a x) xs"
   1.135 +
   1.136 +primrec concat:: "'a list list \<Rightarrow> 'a list" where
   1.137 +"concat [] = []" |
   1.138 +"concat (x # xs) = x @ concat xs"
   1.139 +
   1.140 +definition (in monoid_add) listsum :: "'a list \<Rightarrow> 'a" where
   1.141 +"listsum xs = foldr plus xs 0"
   1.142 +
   1.143 +primrec drop:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   1.144 +drop_Nil: "drop n [] = []" |
   1.145 +drop_Cons: "drop n (x # xs) = (case n of 0 \<Rightarrow> x # xs | Suc m \<Rightarrow> drop m xs)"
   1.146    -- {*Warning: simpset does not contain this definition, but separate
   1.147         theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
   1.148  
   1.149 -primrec
   1.150 -  take:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   1.151 -    take_Nil:"take n [] = []"
   1.152 -  | take_Cons: "take n (x # xs) = (case n of 0 \<Rightarrow> [] | Suc m \<Rightarrow> x # take m xs)"
   1.153 +primrec take:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   1.154 +take_Nil:"take n [] = []" |
   1.155 +take_Cons: "take n (x # xs) = (case n of 0 \<Rightarrow> [] | Suc m \<Rightarrow> x # take m xs)"
   1.156    -- {*Warning: simpset does not contain this definition, but separate
   1.157         theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
   1.158  
   1.159 -primrec
   1.160 -  nth :: "'a list => nat => 'a" (infixl "!" 100) where
   1.161 -  nth_Cons: "(x # xs) ! n = (case n of 0 \<Rightarrow> x | Suc k \<Rightarrow> xs ! k)"
   1.162 +primrec nth :: "'a list => nat => 'a" (infixl "!" 100) where
   1.163 +nth_Cons: "(x # xs) ! n = (case n of 0 \<Rightarrow> x | Suc k \<Rightarrow> xs ! k)"
   1.164    -- {*Warning: simpset does not contain this definition, but separate
   1.165         theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
   1.166  
   1.167 -primrec
   1.168 -  list_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
   1.169 -    "list_update [] i v = []"
   1.170 -  | "list_update (x # xs) i v = (case i of 0 \<Rightarrow> v # xs | Suc j \<Rightarrow> x # list_update xs j v)"
   1.171 +primrec list_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
   1.172 +"list_update [] i v = []" |
   1.173 +"list_update (x # xs) i v =
   1.174 +  (case i of 0 \<Rightarrow> v # xs | Suc j \<Rightarrow> x # list_update xs j v)"
   1.175  
   1.176  nonterminal lupdbinds and lupdbind
   1.177  
   1.178 @@ -143,107 +125,91 @@
   1.179    "_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs"
   1.180    "xs[i:=x]" == "CONST list_update xs i x"
   1.181  
   1.182 -primrec
   1.183 -  takeWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   1.184 -    "takeWhile P [] = []"
   1.185 -  | "takeWhile P (x # xs) = (if P x then x # takeWhile P xs else [])"
   1.186 -
   1.187 -primrec
   1.188 -  dropWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   1.189 -    "dropWhile P [] = []"
   1.190 -  | "dropWhile P (x # xs) = (if P x then dropWhile P xs else x # xs)"
   1.191 -
   1.192 -primrec
   1.193 -  zip :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
   1.194 -    "zip xs [] = []"
   1.195 -  | zip_Cons: "zip xs (y # ys) = (case xs of [] => [] | z # zs => (z, y) # zip zs ys)"
   1.196 +primrec takeWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   1.197 +"takeWhile P [] = []" |
   1.198 +"takeWhile P (x # xs) = (if P x then x # takeWhile P xs else [])"
   1.199 +
   1.200 +primrec dropWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   1.201 +"dropWhile P [] = []" |
   1.202 +"dropWhile P (x # xs) = (if P x then dropWhile P xs else x # xs)"
   1.203 +
   1.204 +primrec zip :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
   1.205 +"zip xs [] = []" |
   1.206 +zip_Cons: "zip xs (y # ys) =
   1.207 +  (case xs of [] => [] | z # zs => (z, y) # zip zs ys)"
   1.208    -- {*Warning: simpset does not contain this definition, but separate
   1.209         theorems for @{text "xs = []"} and @{text "xs = z # zs"} *}
   1.210  
   1.211 -primrec
   1.212 -  product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
   1.213 -    "product [] _ = []"
   1.214 -  | "product (x#xs) ys = map (Pair x) ys @ product xs ys"
   1.215 +primrec product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
   1.216 +"product [] _ = []" |
   1.217 +"product (x#xs) ys = map (Pair x) ys @ product xs ys"
   1.218  
   1.219  hide_const (open) product
   1.220  
   1.221 -primrec 
   1.222 -  upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_..</_'])") where
   1.223 -    upt_0: "[i..<0] = []"
   1.224 -  | upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
   1.225 -
   1.226 -definition
   1.227 -  insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   1.228 -  "insert x xs = (if x \<in> set xs then xs else x # xs)"
   1.229 +primrec upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_..</_'])") where
   1.230 +upt_0: "[i..<0] = []" |
   1.231 +upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
   1.232 +
   1.233 +definition insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   1.234 +"insert x xs = (if x \<in> set xs then xs else x # xs)"
   1.235  
   1.236  hide_const (open) insert
   1.237  hide_fact (open) insert_def
   1.238  
   1.239  primrec find :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a option" where
   1.240 -  "find _ [] = None"
   1.241 -| "find P (x#xs) = (if P x then Some x else find P xs)"
   1.242 +"find _ [] = None" |
   1.243 +"find P (x#xs) = (if P x then Some x else find P xs)"
   1.244  
   1.245  hide_const (open) find
   1.246  
   1.247 -primrec
   1.248 -  remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   1.249 -    "remove1 x [] = []"
   1.250 -  | "remove1 x (y # xs) = (if x = y then xs else y # remove1 x xs)"
   1.251 -
   1.252 -primrec
   1.253 -  removeAll :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   1.254 -    "removeAll x [] = []"
   1.255 -  | "removeAll x (y # xs) = (if x = y then removeAll x xs else y # removeAll x xs)"
   1.256 -
   1.257 -primrec
   1.258 -  distinct :: "'a list \<Rightarrow> bool" where
   1.259 -    "distinct [] \<longleftrightarrow> True"
   1.260 -  | "distinct (x # xs) \<longleftrightarrow> x \<notin> set xs \<and> distinct xs"
   1.261 -
   1.262 -primrec
   1.263 -  remdups :: "'a list \<Rightarrow> 'a list" where
   1.264 -    "remdups [] = []"
   1.265 -  | "remdups (x # xs) = (if x \<in> set xs then remdups xs else x # remdups xs)"
   1.266 -
   1.267 -primrec
   1.268 -  replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
   1.269 -    replicate_0: "replicate 0 x = []"
   1.270 -  | replicate_Suc: "replicate (Suc n) x = x # replicate n x"
   1.271 +primrec remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   1.272 +"remove1 x [] = []" |
   1.273 +"remove1 x (y # xs) = (if x = y then xs else y # remove1 x xs)"
   1.274 +
   1.275 +primrec removeAll :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   1.276 +"removeAll x [] = []" |
   1.277 +"removeAll x (y # xs) = (if x = y then removeAll x xs else y # removeAll x xs)"
   1.278 +
   1.279 +primrec distinct :: "'a list \<Rightarrow> bool" where
   1.280 +"distinct [] \<longleftrightarrow> True" |
   1.281 +"distinct (x # xs) \<longleftrightarrow> x \<notin> set xs \<and> distinct xs"
   1.282 +
   1.283 +primrec remdups :: "'a list \<Rightarrow> 'a list" where
   1.284 +"remdups [] = []" |
   1.285 +"remdups (x # xs) = (if x \<in> set xs then remdups xs else x # remdups xs)"
   1.286 +
   1.287 +primrec replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
   1.288 +replicate_0: "replicate 0 x = []" |
   1.289 +replicate_Suc: "replicate (Suc n) x = x # replicate n x"
   1.290  
   1.291  text {*
   1.292    Function @{text size} is overloaded for all datatypes. Users may
   1.293    refer to the list version as @{text length}. *}
   1.294  
   1.295 -abbreviation
   1.296 -  length :: "'a list \<Rightarrow> nat" where
   1.297 -  "length \<equiv> size"
   1.298 +abbreviation length :: "'a list \<Rightarrow> nat" where
   1.299 +"length \<equiv> size"
   1.300  
   1.301  primrec rotate1 :: "'a list \<Rightarrow> 'a list" where
   1.302 -  "rotate1 [] = []" |
   1.303 -  "rotate1 (x # xs) = xs @ [x]"
   1.304 -
   1.305 -definition
   1.306 -  rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   1.307 -  "rotate n = rotate1 ^^ n"
   1.308 -
   1.309 -definition
   1.310 -  list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where
   1.311 -  "list_all2 P xs ys =
   1.312 -    (length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))"
   1.313 -
   1.314 -definition
   1.315 -  sublist :: "'a list => nat set => 'a list" where
   1.316 -  "sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
   1.317 -
   1.318 -primrec
   1.319 -  sublists :: "'a list \<Rightarrow> 'a list list" where
   1.320 -  "sublists [] = [[]]"
   1.321 -| "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
   1.322 -
   1.323 -primrec
   1.324 -  n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
   1.325 -  "n_lists 0 xs = [[]]"
   1.326 -| "n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))"
   1.327 +"rotate1 [] = []" |
   1.328 +"rotate1 (x # xs) = xs @ [x]"
   1.329 +
   1.330 +definition rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   1.331 +"rotate n = rotate1 ^^ n"
   1.332 +
   1.333 +definition list_all2 :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> bool" where
   1.334 +"list_all2 P xs ys =
   1.335 +  (length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))"
   1.336 +
   1.337 +definition sublist :: "'a list => nat set => 'a list" where
   1.338 +"sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
   1.339 +
   1.340 +primrec sublists :: "'a list \<Rightarrow> 'a list list" where
   1.341 +"sublists [] = [[]]" |
   1.342 +"sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
   1.343 +
   1.344 +primrec n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
   1.345 +"n_lists 0 xs = [[]]" |
   1.346 +"n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))"
   1.347  
   1.348  hide_const (open) n_lists
   1.349  
   1.350 @@ -335,14 +301,16 @@
   1.351    by simp_all
   1.352  
   1.353  primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
   1.354 -  "insort_key f x [] = [x]" |
   1.355 -  "insort_key f x (y#ys) = (if f x \<le> f y then (x#y#ys) else y#(insort_key f x ys))"
   1.356 +"insort_key f x [] = [x]" |
   1.357 +"insort_key f x (y#ys) =
   1.358 +  (if f x \<le> f y then (x#y#ys) else y#(insort_key f x ys))"
   1.359  
   1.360  definition sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where
   1.361 -  "sort_key f xs = foldr (insort_key f) xs []"
   1.362 +"sort_key f xs = foldr (insort_key f) xs []"
   1.363  
   1.364  definition insort_insert_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
   1.365 -  "insort_insert_key f x xs = (if f x \<in> f ` set xs then xs else insort_key f x xs)"
   1.366 +"insort_insert_key f x xs =
   1.367 +  (if f x \<in> f ` set xs then xs else insort_key f x xs)"
   1.368  
   1.369  abbreviation "sort \<equiv> sort_key (\<lambda>x. x)"
   1.370  abbreviation "insort \<equiv> insort_key (\<lambda>x. x)"
   1.371 @@ -1517,10 +1485,10 @@
   1.372  subsubsection {* List partitioning *}
   1.373  
   1.374  primrec partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> 'a list \<times> 'a list" where
   1.375 -  "partition P [] = ([], [])"
   1.376 -  | "partition P (x # xs) = 
   1.377 -      (let (yes, no) = partition P xs
   1.378 -      in if P x then (x # yes, no) else (yes, x # no))"
   1.379 +"partition P [] = ([], [])" |
   1.380 +"partition P (x # xs) = 
   1.381 +  (let (yes, no) = partition P xs
   1.382 +   in if P x then (x # yes, no) else (yes, x # no))"
   1.383  
   1.384  lemma partition_filter1:
   1.385      "fst (partition P xs) = filter P xs"
   1.386 @@ -4823,7 +4791,7 @@
   1.387  begin
   1.388  
   1.389  definition sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
   1.390 -  "sorted_list_of_set = Finite_Set.fold insort []"
   1.391 +"sorted_list_of_set = Finite_Set.fold insort []"
   1.392  
   1.393  lemma sorted_list_of_set_empty [simp]:
   1.394    "sorted_list_of_set {} = []"
   1.395 @@ -4967,9 +4935,8 @@
   1.396  text{*@{text"set_Cons A Xs"}: the set of lists with head drawn from
   1.397  @{term A} and tail drawn from @{term Xs}.*}
   1.398  
   1.399 -definition
   1.400 -  set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set" where
   1.401 -  "set_Cons A XS = {z. \<exists>x xs. z = x # xs \<and> x \<in> A \<and> xs \<in> XS}"
   1.402 +definition set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set" where
   1.403 +"set_Cons A XS = {z. \<exists>x xs. z = x # xs \<and> x \<in> A \<and> xs \<in> XS}"
   1.404  
   1.405  lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])`A"
   1.406  by (auto simp add: set_Cons_def)
   1.407 @@ -4977,10 +4944,9 @@
   1.408  text{*Yields the set of lists, all of the same length as the argument and
   1.409  with elements drawn from the corresponding element of the argument.*}
   1.410  
   1.411 -primrec
   1.412 -  listset :: "'a set list \<Rightarrow> 'a list set" where
   1.413 -     "listset [] = {[]}"
   1.414 -  |  "listset (A # As) = set_Cons A (listset As)"
   1.415 +primrec listset :: "'a set list \<Rightarrow> 'a list set" where
   1.416 +"listset [] = {[]}" |
   1.417 +"listset (A # As) = set_Cons A (listset As)"
   1.418  
   1.419  
   1.420  subsection {* Relations on Lists *}
   1.421 @@ -4992,17 +4958,16 @@
   1.422          
   1.423  primrec -- {*The lexicographic ordering for lists of the specified length*}
   1.424    lexn :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a list \<times> 'a list) set" where
   1.425 -    "lexn r 0 = {}"
   1.426 -  | "lexn r (Suc n) = (map_pair (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int
   1.427 -      {(xs, ys). length xs = Suc n \<and> length ys = Suc n}"
   1.428 -
   1.429 -definition
   1.430 -  lex :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
   1.431 -  "lex r = (\<Union>n. lexn r n)" -- {*Holds only between lists of the same length*}
   1.432 -
   1.433 -definition
   1.434 -  lenlex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set" where
   1.435 -  "lenlex r = inv_image (less_than <*lex*> lex r) (\<lambda>xs. (length xs, xs))"
   1.436 +"lexn r 0 = {}" |
   1.437 +"lexn r (Suc n) =
   1.438 +  (map_pair (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int
   1.439 +  {(xs, ys). length xs = Suc n \<and> length ys = Suc n}"
   1.440 +
   1.441 +definition lex :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
   1.442 +"lex r = (\<Union>n. lexn r n)" -- {*Holds only between lists of the same length*}
   1.443 +
   1.444 +definition lenlex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set" where
   1.445 +"lenlex r = inv_image (less_than <*lex*> lex r) (\<lambda>xs. (length xs, xs))"
   1.446          -- {*Compares lists by their length and then lexicographically*}
   1.447  
   1.448  lemma wf_lexn: "wf r ==> wf (lexn r n)"
   1.449 @@ -5074,9 +5039,8 @@
   1.450      This ordering does \emph{not} preserve well-foundedness.
   1.451       Author: N. Voelker, March 2005. *} 
   1.452  
   1.453 -definition
   1.454 -  lexord :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
   1.455 -  "lexord r = {(x,y ). \<exists> a v. y = x @ a # v \<or>
   1.456 +definition lexord :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
   1.457 +"lexord r = {(x,y). \<exists> a v. y = x @ a # v \<or>
   1.458              (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
   1.459  
   1.460  lemma lexord_Nil_left[simp]:  "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
   1.461 @@ -5187,8 +5151,7 @@
   1.462  
   1.463  text {* These are useful for termination proofs *}
   1.464  
   1.465 -definition
   1.466 -  "measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)"
   1.467 +definition "measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)"
   1.468  
   1.469  lemma wf_measures[simp]: "wf (measures fs)"
   1.470  unfolding measures_def
   1.471 @@ -5521,7 +5484,7 @@
   1.472  subsection {* Monad operation *}
   1.473  
   1.474  definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
   1.475 -  "bind xs f = concat (map f xs)"
   1.476 +"bind xs f = concat (map f xs)"
   1.477  
   1.478  hide_const (open) bind
   1.479  
   1.480 @@ -5533,20 +5496,14 @@
   1.481  
   1.482  subsection {* Transfer *}
   1.483  
   1.484 -definition
   1.485 -  embed_list :: "nat list \<Rightarrow> int list"
   1.486 -where
   1.487 -  "embed_list l = map int l"
   1.488 -
   1.489 -definition
   1.490 -  nat_list :: "int list \<Rightarrow> bool"
   1.491 -where
   1.492 -  "nat_list l = nat_set (set l)"
   1.493 -
   1.494 -definition
   1.495 -  return_list :: "int list \<Rightarrow> nat list"
   1.496 -where
   1.497 -  "return_list l = map nat l"
   1.498 +definition embed_list :: "nat list \<Rightarrow> int list" where
   1.499 +"embed_list l = map int l"
   1.500 +
   1.501 +definition nat_list :: "int list \<Rightarrow> bool" where
   1.502 +"nat_list l = nat_set (set l)"
   1.503 +
   1.504 +definition return_list :: "int list \<Rightarrow> nat list" where
   1.505 +"return_list l = map nat l"
   1.506  
   1.507  lemma transfer_nat_int_list_return_embed: "nat_list l \<longrightarrow>
   1.508      embed_list (return_list l) = l"
   1.509 @@ -5575,7 +5532,7 @@
   1.510  subsubsection {* Counterparts for set-related operations *}
   1.511  
   1.512  definition member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
   1.513 -  [code_abbrev]: "member xs x \<longleftrightarrow> x \<in> set xs"
   1.514 +[code_abbrev]: "member xs x \<longleftrightarrow> x \<in> set xs"
   1.515  
   1.516  text {*
   1.517    Use @{text member} only for generating executable code.  Otherwise use
   1.518 @@ -5592,13 +5549,13 @@
   1.519    by (simp add: member_def)
   1.520  
   1.521  definition list_all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
   1.522 -  list_all_iff [code_abbrev]: "list_all P xs \<longleftrightarrow> Ball (set xs) P"
   1.523 +list_all_iff [code_abbrev]: "list_all P xs \<longleftrightarrow> Ball (set xs) P"
   1.524  
   1.525  definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
   1.526 -  list_ex_iff [code_abbrev]: "list_ex P xs \<longleftrightarrow> Bex (set xs) P"
   1.527 +list_ex_iff [code_abbrev]: "list_ex P xs \<longleftrightarrow> Bex (set xs) P"
   1.528  
   1.529  definition list_ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
   1.530 -  list_ex1_iff [code_abbrev]: "list_ex1 P xs \<longleftrightarrow> (\<exists>! x. x \<in> set xs \<and> P x)"
   1.531 +list_ex1_iff [code_abbrev]: "list_ex1 P xs \<longleftrightarrow> (\<exists>! x. x \<in> set xs \<and> P x)"
   1.532  
   1.533  text {*
   1.534    Usually you should prefer @{text "\<forall>x\<in>set xs"}, @{text "\<exists>x\<in>set xs"}
   1.535 @@ -5661,9 +5618,8 @@
   1.536    "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_ex f xs = list_ex g ys"
   1.537  by (simp add: list_ex_iff)
   1.538  
   1.539 -definition can_select :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
   1.540 -where
   1.541 -  [code_abbrev]: "can_select P A = (\<exists>!x\<in>A. P x)"
   1.542 +definition can_select :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
   1.543 +[code_abbrev]: "can_select P A = (\<exists>!x\<in>A. P x)"
   1.544  
   1.545  lemma can_select_set_list_ex1 [code]:
   1.546    "can_select P (set A) = list_ex1 P A"