src/HOL/List.thy
 changeset 50548 0aec55e63795 parent 50422 ee729dbd1b7f child 51096 60e4b75fefe1
--- a/src/HOL/List.thy	Fri Dec 14 18:41:56 2012 +0100
+++ b/src/HOL/List.thy	Fri Dec 14 19:51:20 2012 +0100
@@ -23,52 +23,42 @@

subsection {* Basic list processing functions *}

-primrec
-  hd :: "'a list \<Rightarrow> 'a" where
-  "hd (x # xs) = x"
-
-primrec
-  tl :: "'a list \<Rightarrow> 'a list" where
-    "tl [] = []"
-  | "tl (x # xs) = xs"
-
-primrec
-  last :: "'a list \<Rightarrow> 'a" where
-  "last (x # xs) = (if xs = [] then x else last xs)"
-
-primrec
-  butlast :: "'a list \<Rightarrow> 'a list" where
-    "butlast []= []"
-  | "butlast (x # xs) = (if xs = [] then [] else x # butlast xs)"
-
-primrec
-  set :: "'a list \<Rightarrow> 'a set" where
-    "set [] = {}"
-  | "set (x # xs) = insert x (set xs)"
-
-definition
-  coset :: "'a list \<Rightarrow> 'a set" where
-  [simp]: "coset xs = - set xs"
-
-primrec
-  map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
-    "map f [] = []"
-  | "map f (x # xs) = f x # map f xs"
-
-primrec
-  append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) where
-    append_Nil:"[] @ ys = ys"
-  | append_Cons: "(x#xs) @ ys = x # xs @ ys"
-
-primrec
-  rev :: "'a list \<Rightarrow> 'a list" where
-    "rev [] = []"
-  | "rev (x # xs) = rev xs @ [x]"
-
-primrec
-  filter:: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-    "filter P [] = []"
-  | "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"
+primrec hd :: "'a list \<Rightarrow> 'a" where
+"hd (x # xs) = x"
+
+primrec tl :: "'a list \<Rightarrow> 'a list" where
+"tl [] = []" |
+"tl (x # xs) = xs"
+
+primrec last :: "'a list \<Rightarrow> 'a" where
+"last (x # xs) = (if xs = [] then x else last xs)"
+
+primrec butlast :: "'a list \<Rightarrow> 'a list" where
+"butlast []= []" |
+"butlast (x # xs) = (if xs = [] then [] else x # butlast xs)"
+
+primrec set :: "'a list \<Rightarrow> 'a set" where
+"set [] = {}" |
+"set (x # xs) = insert x (set xs)"
+
+definition coset :: "'a list \<Rightarrow> 'a set" where
+[simp]: "coset xs = - set xs"
+
+primrec map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
+"map f [] = []" |
+"map f (x # xs) = f x # map f xs"
+
+primrec append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) where
+append_Nil: "[] @ ys = ys" |
+append_Cons: "(x#xs) @ ys = x # xs @ ys"
+
+primrec rev :: "'a list \<Rightarrow> 'a list" where
+"rev [] = []" |
+"rev (x # xs) = rev xs @ [x]"
+
+primrec filter:: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"filter P [] = []" |
+"filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"

syntax
-- {* Special syntax for filter *}
@@ -82,54 +72,46 @@
syntax (HTML output)
"_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")

-primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b"
-where
-  fold_Nil:  "fold f [] = id"
-| fold_Cons: "fold f (x # xs) = fold f xs \<circ> f x" -- {* natural argument order *}
-
-primrec foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b"
-where
-  foldr_Nil:  "foldr f [] = id"
-| foldr_Cons: "foldr f (x # xs) = f x \<circ> foldr f xs" -- {* natural argument order *}
-
-primrec foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
-where
-  foldl_Nil:  "foldl f a [] = a"
-| foldl_Cons: "foldl f a (x # xs) = foldl f (f a x) xs"
-
-primrec
-  concat:: "'a list list \<Rightarrow> 'a list" where
-    "concat [] = []"
-  | "concat (x # xs) = x @ concat xs"
-
-  listsum :: "'a list \<Rightarrow> 'a" where
-  "listsum xs = foldr plus xs 0"
-
-primrec
-  drop:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-    drop_Nil: "drop n [] = []"
-  | drop_Cons: "drop n (x # xs) = (case n of 0 \<Rightarrow> x # xs | Suc m \<Rightarrow> drop m xs)"
+primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
+fold_Nil:  "fold f [] = id" |
+fold_Cons: "fold f (x # xs) = fold f xs \<circ> f x"
+
+primrec foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
+foldr_Nil:  "foldr f [] = id" |
+foldr_Cons: "foldr f (x # xs) = f x \<circ> foldr f xs"
+
+primrec foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b" where
+foldl_Nil:  "foldl f a [] = a" |
+foldl_Cons: "foldl f a (x # xs) = foldl f (f a x) xs"
+
+primrec concat:: "'a list list \<Rightarrow> 'a list" where
+"concat [] = []" |
+"concat (x # xs) = x @ concat xs"
+
+definition (in monoid_add) listsum :: "'a list \<Rightarrow> 'a" where
+"listsum xs = foldr plus xs 0"
+
+primrec drop:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+drop_Nil: "drop n [] = []" |
+drop_Cons: "drop n (x # xs) = (case n of 0 \<Rightarrow> x # xs | Suc m \<Rightarrow> drop m xs)"
-- {*Warning: simpset does not contain this definition, but separate
theorems for @{text "n = 0"} and @{text "n = Suc k"} *}

-primrec
-  take:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-    take_Nil:"take n [] = []"
-  | take_Cons: "take n (x # xs) = (case n of 0 \<Rightarrow> [] | Suc m \<Rightarrow> x # take m xs)"
+primrec take:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+take_Nil:"take n [] = []" |
+take_Cons: "take n (x # xs) = (case n of 0 \<Rightarrow> [] | Suc m \<Rightarrow> x # take m xs)"
-- {*Warning: simpset does not contain this definition, but separate
theorems for @{text "n = 0"} and @{text "n = Suc k"} *}

-primrec
-  nth :: "'a list => nat => 'a" (infixl "!" 100) where
-  nth_Cons: "(x # xs) ! n = (case n of 0 \<Rightarrow> x | Suc k \<Rightarrow> xs ! k)"
+primrec nth :: "'a list => nat => 'a" (infixl "!" 100) where
+nth_Cons: "(x # xs) ! n = (case n of 0 \<Rightarrow> x | Suc k \<Rightarrow> xs ! k)"
-- {*Warning: simpset does not contain this definition, but separate
theorems for @{text "n = 0"} and @{text "n = Suc k"} *}

-primrec
-  list_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
-    "list_update [] i v = []"
-  | "list_update (x # xs) i v = (case i of 0 \<Rightarrow> v # xs | Suc j \<Rightarrow> x # list_update xs j v)"
+primrec list_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
+"list_update [] i v = []" |
+"list_update (x # xs) i v =
+  (case i of 0 \<Rightarrow> v # xs | Suc j \<Rightarrow> x # list_update xs j v)"

nonterminal lupdbinds and lupdbind

@@ -143,107 +125,91 @@
"_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs"
"xs[i:=x]" == "CONST list_update xs i x"

-primrec
-  takeWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-    "takeWhile P [] = []"
-  | "takeWhile P (x # xs) = (if P x then x # takeWhile P xs else [])"
-
-primrec
-  dropWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-    "dropWhile P [] = []"
-  | "dropWhile P (x # xs) = (if P x then dropWhile P xs else x # xs)"
-
-primrec
-  zip :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
-    "zip xs [] = []"
-  | zip_Cons: "zip xs (y # ys) = (case xs of [] => [] | z # zs => (z, y) # zip zs ys)"
+primrec takeWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"takeWhile P [] = []" |
+"takeWhile P (x # xs) = (if P x then x # takeWhile P xs else [])"
+
+primrec dropWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"dropWhile P [] = []" |
+"dropWhile P (x # xs) = (if P x then dropWhile P xs else x # xs)"
+
+primrec zip :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
+"zip xs [] = []" |
+zip_Cons: "zip xs (y # ys) =
+  (case xs of [] => [] | z # zs => (z, y) # zip zs ys)"
-- {*Warning: simpset does not contain this definition, but separate
theorems for @{text "xs = []"} and @{text "xs = z # zs"} *}

-primrec
-  product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
-    "product [] _ = []"
-  | "product (x#xs) ys = map (Pair x) ys @ product xs ys"
+primrec product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
+"product [] _ = []" |
+"product (x#xs) ys = map (Pair x) ys @ product xs ys"

hide_const (open) product

-primrec
-  upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_..</_'])") where
-    upt_0: "[i..<0] = []"
-  | upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
-
-definition
-  insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-  "insert x xs = (if x \<in> set xs then xs else x # xs)"
+primrec upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_..</_'])") where
+upt_0: "[i..<0] = []" |
+upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
+
+definition insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"insert x xs = (if x \<in> set xs then xs else x # xs)"

hide_const (open) insert
hide_fact (open) insert_def

primrec find :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a option" where
-  "find _ [] = None"
-| "find P (x#xs) = (if P x then Some x else find P xs)"
+"find _ [] = None" |
+"find P (x#xs) = (if P x then Some x else find P xs)"

hide_const (open) find

-primrec
-  remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-    "remove1 x [] = []"
-  | "remove1 x (y # xs) = (if x = y then xs else y # remove1 x xs)"
-
-primrec
-  removeAll :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-    "removeAll x [] = []"
-  | "removeAll x (y # xs) = (if x = y then removeAll x xs else y # removeAll x xs)"
-
-primrec
-  distinct :: "'a list \<Rightarrow> bool" where
-    "distinct [] \<longleftrightarrow> True"
-  | "distinct (x # xs) \<longleftrightarrow> x \<notin> set xs \<and> distinct xs"
-
-primrec
-  remdups :: "'a list \<Rightarrow> 'a list" where
-    "remdups [] = []"
-  | "remdups (x # xs) = (if x \<in> set xs then remdups xs else x # remdups xs)"
-
-primrec
-  replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
-    replicate_0: "replicate 0 x = []"
-  | replicate_Suc: "replicate (Suc n) x = x # replicate n x"
+primrec remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"remove1 x [] = []" |
+"remove1 x (y # xs) = (if x = y then xs else y # remove1 x xs)"
+
+primrec removeAll :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"removeAll x [] = []" |
+"removeAll x (y # xs) = (if x = y then removeAll x xs else y # removeAll x xs)"
+
+primrec distinct :: "'a list \<Rightarrow> bool" where
+"distinct [] \<longleftrightarrow> True" |
+"distinct (x # xs) \<longleftrightarrow> x \<notin> set xs \<and> distinct xs"
+
+primrec remdups :: "'a list \<Rightarrow> 'a list" where
+"remdups [] = []" |
+"remdups (x # xs) = (if x \<in> set xs then remdups xs else x # remdups xs)"
+
+primrec replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
+replicate_0: "replicate 0 x = []" |
+replicate_Suc: "replicate (Suc n) x = x # replicate n x"

text {*
Function @{text size} is overloaded for all datatypes. Users may
refer to the list version as @{text length}. *}

-abbreviation
-  length :: "'a list \<Rightarrow> nat" where
-  "length \<equiv> size"
+abbreviation length :: "'a list \<Rightarrow> nat" where
+"length \<equiv> size"

primrec rotate1 :: "'a list \<Rightarrow> 'a list" where
-  "rotate1 [] = []" |
-  "rotate1 (x # xs) = xs @ [x]"
-
-definition
-  rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-  "rotate n = rotate1 ^^ n"
-
-definition
-  list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where
-  "list_all2 P xs ys =
-    (length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))"
-
-definition
-  sublist :: "'a list => nat set => 'a list" where
-  "sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
-
-primrec
-  sublists :: "'a list \<Rightarrow> 'a list list" where
-  "sublists [] = [[]]"
-| "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
-
-primrec
-  n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
-  "n_lists 0 xs = [[]]"
-| "n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))"
+"rotate1 [] = []" |
+"rotate1 (x # xs) = xs @ [x]"
+
+definition rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"rotate n = rotate1 ^^ n"
+
+definition list_all2 :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> bool" where
+"list_all2 P xs ys =
+  (length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))"
+
+definition sublist :: "'a list => nat set => 'a list" where
+"sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
+
+primrec sublists :: "'a list \<Rightarrow> 'a list list" where
+"sublists [] = [[]]" |
+"sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
+
+primrec n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
+"n_lists 0 xs = [[]]" |
+"n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))"

hide_const (open) n_lists

@@ -335,14 +301,16 @@
by simp_all

primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
-  "insort_key f x [] = [x]" |
-  "insort_key f x (y#ys) = (if f x \<le> f y then (x#y#ys) else y#(insort_key f x ys))"
+"insort_key f x [] = [x]" |
+"insort_key f x (y#ys) =
+  (if f x \<le> f y then (x#y#ys) else y#(insort_key f x ys))"

definition sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where
-  "sort_key f xs = foldr (insort_key f) xs []"
+"sort_key f xs = foldr (insort_key f) xs []"

definition insort_insert_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
-  "insort_insert_key f x xs = (if f x \<in> f  set xs then xs else insort_key f x xs)"
+"insort_insert_key f x xs =
+  (if f x \<in> f  set xs then xs else insort_key f x xs)"

abbreviation "sort \<equiv> sort_key (\<lambda>x. x)"
abbreviation "insort \<equiv> insort_key (\<lambda>x. x)"
@@ -1517,10 +1485,10 @@
subsubsection {* List partitioning *}

primrec partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> 'a list \<times> 'a list" where
-  "partition P [] = ([], [])"
-  | "partition P (x # xs) =
-      (let (yes, no) = partition P xs
-      in if P x then (x # yes, no) else (yes, x # no))"
+"partition P [] = ([], [])" |
+"partition P (x # xs) =
+  (let (yes, no) = partition P xs
+   in if P x then (x # yes, no) else (yes, x # no))"

lemma partition_filter1:
"fst (partition P xs) = filter P xs"
@@ -4823,7 +4791,7 @@
begin

definition sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
-  "sorted_list_of_set = Finite_Set.fold insort []"
+"sorted_list_of_set = Finite_Set.fold insort []"

lemma sorted_list_of_set_empty [simp]:
"sorted_list_of_set {} = []"
@@ -4967,9 +4935,8 @@
text{*@{text"set_Cons A Xs"}: the set of lists with head drawn from
@{term A} and tail drawn from @{term Xs}.*}

-definition
-  set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set" where
-  "set_Cons A XS = {z. \<exists>x xs. z = x # xs \<and> x \<in> A \<and> xs \<in> XS}"
+definition set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set" where
+"set_Cons A XS = {z. \<exists>x xs. z = x # xs \<and> x \<in> A \<and> xs \<in> XS}"

lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])A"
@@ -4977,10 +4944,9 @@
text{*Yields the set of lists, all of the same length as the argument and
with elements drawn from the corresponding element of the argument.*}

-primrec
-  listset :: "'a set list \<Rightarrow> 'a list set" where
-     "listset [] = {[]}"
-  |  "listset (A # As) = set_Cons A (listset As)"
+primrec listset :: "'a set list \<Rightarrow> 'a list set" where
+"listset [] = {[]}" |
+"listset (A # As) = set_Cons A (listset As)"

subsection {* Relations on Lists *}
@@ -4992,17 +4958,16 @@

primrec -- {*The lexicographic ordering for lists of the specified length*}
lexn :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a list \<times> 'a list) set" where
-    "lexn r 0 = {}"
-  | "lexn r (Suc n) = (map_pair (%(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}"
-
-definition
-  lex :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
-  "lex r = (\<Union>n. lexn r n)" -- {*Holds only between lists of the same length*}
-
-definition
-  lenlex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set" where
-  "lenlex r = inv_image (less_than <*lex*> lex r) (\<lambda>xs. (length xs, xs))"
+"lexn r 0 = {}" |
+"lexn r (Suc n) =
+  (map_pair (%(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}"
+
+definition lex :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
+"lex r = (\<Union>n. lexn r n)" -- {*Holds only between lists of the same length*}
+
+definition lenlex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set" where
+"lenlex r = inv_image (less_than <*lex*> lex r) (\<lambda>xs. (length xs, xs))"
-- {*Compares lists by their length and then lexicographically*}

lemma wf_lexn: "wf r ==> wf (lexn r n)"
@@ -5074,9 +5039,8 @@
This ordering does \emph{not} preserve well-foundedness.
Author: N. Voelker, March 2005. *}

-definition
-  lexord :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
-  "lexord r = {(x,y ). \<exists> a v. y = x @ a # v \<or>
+definition lexord :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
+"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)"
@@ -5187,8 +5151,7 @@

text {* These are useful for termination proofs *}

-definition
-  "measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)"
+definition "measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)"

lemma wf_measures[simp]: "wf (measures fs)"
unfolding measures_def
@@ -5521,7 +5484,7 @@

definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
-  "bind xs f = concat (map f xs)"
+"bind xs f = concat (map f xs)"

hide_const (open) bind

@@ -5533,20 +5496,14 @@

subsection {* Transfer *}

-definition
-  embed_list :: "nat list \<Rightarrow> int list"
-where
-  "embed_list l = map int l"
-
-definition
-  nat_list :: "int list \<Rightarrow> bool"
-where
-  "nat_list l = nat_set (set l)"
-
-definition
-  return_list :: "int list \<Rightarrow> nat list"
-where
-  "return_list l = map nat l"
+definition embed_list :: "nat list \<Rightarrow> int list" where
+"embed_list l = map int l"
+
+definition nat_list :: "int list \<Rightarrow> bool" where
+"nat_list l = nat_set (set l)"
+
+definition return_list :: "int list \<Rightarrow> nat list" where
+"return_list l = map nat l"

lemma transfer_nat_int_list_return_embed: "nat_list l \<longrightarrow>
embed_list (return_list l) = l"
@@ -5575,7 +5532,7 @@
subsubsection {* Counterparts for set-related operations *}

definition member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
-  [code_abbrev]: "member xs x \<longleftrightarrow> x \<in> set xs"
+[code_abbrev]: "member xs x \<longleftrightarrow> x \<in> set xs"

text {*
Use @{text member} only for generating executable code.  Otherwise use
@@ -5592,13 +5549,13 @@

definition list_all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
-  list_all_iff [code_abbrev]: "list_all P xs \<longleftrightarrow> Ball (set xs) P"
+list_all_iff [code_abbrev]: "list_all P xs \<longleftrightarrow> Ball (set xs) P"

definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
-  list_ex_iff [code_abbrev]: "list_ex P xs \<longleftrightarrow> Bex (set xs) P"
+list_ex_iff [code_abbrev]: "list_ex P xs \<longleftrightarrow> Bex (set xs) P"

definition list_ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
-  list_ex1_iff [code_abbrev]: "list_ex1 P xs \<longleftrightarrow> (\<exists>! x. x \<in> set xs \<and> P x)"
+list_ex1_iff [code_abbrev]: "list_ex1 P xs \<longleftrightarrow> (\<exists>! x. x \<in> set xs \<and> P x)"

text {*
Usually you should prefer @{text "\<forall>x\<in>set xs"}, @{text "\<exists>x\<in>set xs"}
@@ -5661,9 +5618,8 @@
"xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_ex f xs = list_ex g ys"
"can_select P (set A) = list_ex1 P A"`