(*  Title:      HOL/List.thy

    Author:     Tobias Nipkow

*)

header {* The datatype of finite lists *}

theory List

imports Presburger Code_Numeral Quotient ATP Lifting_Set Lifting_Option Lifting_Product

begin

datatype 'a list =

    Nil    ("[]")

  | Cons 'a  "'a list"    (infixr "#" 65)

syntax

  -- {* list Enumeration *}

  "_list" :: "args => 'a list"    ("[(_)]")

translations

  "[x, xs]" == "x#[xs]"

  "[x]" == "x#[]"

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)"

syntax

  -- {* Special syntax for filter *}

  "_filter" :: "[pttrn, 'a list, bool] => 'a list"    ("(1[_<-_./ _])")

translations

  "[x<-xs . P]"== "CONST filter (%x. P) xs"

syntax (xsymbols)

  "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")

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"

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)"

  -- {*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)"

  -- {*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)"

nonterminal lupdbinds and lupdbind

syntax

  "_lupdbind":: "['a, 'a] => lupdbind"    ("(2_ :=/ _)")

  "" :: "lupdbind => lupdbinds"    ("_")

  "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds"    ("_,/ _")

  "_LUpdate" :: "['a, lupdbinds] => 'a"    ("_/[(_)]" [900,0] 900)

translations

  "_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)"

  -- {*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"

hide_const (open) product

primrec product_lists :: "'a list list \<Rightarrow> 'a list list" where

"product_lists [] = [[]]" |

"product_lists (xs # xss) = concat (map (\<lambda>x. map (Cons x) (product_lists xss)) 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)"

hide_const (open) find

primrec those :: "'a option list \<Rightarrow> 'a list option"

where

"those [] = Some []" |

"those (x # xs) = (case x of

  None \<Rightarrow> None

| Some y \<Rightarrow> Option.map (Cons y) (those xs))"

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)"

fun remdups_adj :: "'a list \<Rightarrow> 'a list" where

"remdups_adj [] = []" |

"remdups_adj [x] = [x]" |

"remdups_adj (x # y # xs) = (if x = y then remdups_adj (x # xs) else x # remdups_adj (y # 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"

definition enumerate :: "nat \<Rightarrow> 'a list \<Rightarrow> (nat \<times> 'a) list" where

enumerate_eq_zip: "enumerate n xs = zip [n..<n + length xs] xs"

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 \<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

fun splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where

"splice [] ys = ys" |

"splice xs [] = xs" |

"splice (x#xs) (y#ys) = x # y # splice xs ys"

text{*

\begin{figure}[htbp]

\fbox{

\begin{tabular}{l}

@{lemma "[a,b]@[c,d] = [a,b,c,d]" by simp}\\

@{lemma "length [a,b,c] = 3" by simp}\\

@{lemma "set [a,b,c] = {a,b,c}" by simp}\\

@{lemma "map f [a,b,c] = [f a, f b, f c]" by simp}\\

@{lemma "rev [a,b,c] = [c,b,a]" by simp}\\

@{lemma "hd [a,b,c,d] = a" by simp}\\

@{lemma "tl [a,b,c,d] = [b,c,d]" by simp}\\

@{lemma "last [a,b,c,d] = d" by simp}\\

@{lemma "butlast [a,b,c,d] = [a,b,c]" by simp}\\

@{lemma[source] "filter (\<lambda>n::nat. n<2) [0,2,1] = [0,1]" by simp}\\

@{lemma "concat [[a,b],[c,d,e],[],[f]] = [a,b,c,d,e,f]" by simp}\\

@{lemma "fold f [a,b,c] x = f c (f b (f a x))" by simp}\\

@{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by simp}\\

@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\

@{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\

@{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\

@{lemma "enumerate 3 [a,b,c] = [(3,a),(4,b),(5,c)]" by normalization}\\

@{lemma "List.product [a,b] [c,d] = [(a, c), (a, d), (b, c), (b, d)]" by simp}\\

@{lemma "product_lists [[a,b], [c], [d,e]] = [[a,c,d], [a,c,e], [b,c,d], [b,c,e]]" by simp}\\

@{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\

@{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\

@{lemma "take 2 [a,b,c,d] = [a,b]" by simp}\\

@{lemma "take 6 [a,b,c,d] = [a,b,c,d]" by simp}\\

@{lemma "drop 2 [a,b,c,d] = [c,d]" by simp}\\

@{lemma "drop 6 [a,b,c,d] = []" by simp}\\

@{lemma "takeWhile (%n::nat. n<3) [1,2,3,0] = [1,2]" by simp}\\

@{lemma "dropWhile (%n::nat. n<3) [1,2,3,0] = [3,0]" by simp}\\

@{lemma "distinct [2,0,1::nat]" by simp}\\

@{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" by simp}\\

@{lemma "remdups_adj [2,2,3,1,1::nat,2,1] = [2,3,1,2,1]" by simp}\\

@{lemma "List.insert 2 [0::nat,1,2] = [0,1,2]" by (simp add: List.insert_def)}\\

@{lemma "List.insert 3 [0::nat,1,2] = [3,0,1,2]" by (simp add: List.insert_def)}\\

@{lemma "List.find (%i::int. i>0) [0,0] = None" by simp}\\

@{lemma "List.find (%i::int. i>0) [0,1,0,2] = Some 1" by simp}\\

@{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\

@{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\

@{lemma "nth [a,b,c,d] 2 = c" by simp}\\

@{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\

@{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\

@{lemma "sublists [a,b] = [[a, b], [a], [b], []]" by simp}\\

@{lemma "List.n_lists 2 [a,b,c] = [[a, a], [b, a], [c, a], [a, b], [b, b], [c, b], [a, c], [b, c], [c, c]]" by (simp add: eval_nat_numeral)}\\

@{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by simp}\\

@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate_def eval_nat_numeral)}\\

@{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\

@{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}\\

@{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def)}

\end{tabular}}

\caption{Characteristic examples}

\label{fig:Characteristic}

\end{figure}

Figure~\ref{fig:Characteristic} shows characteristic examples

that should give an intuitive understanding of the above functions.

*}

text{* The following simple sort functions are intended for proofs,

not for efficient implementations. *}

context linorder

begin

inductive sorted :: "'a list \<Rightarrow> bool" where

  Nil [iff]: "sorted []"

| Cons: "\<forall>y\<in>set xs. x \<le> y \<Longrightarrow> sorted xs \<Longrightarrow> sorted (x # xs)"

lemma sorted_single [iff]:

  "sorted [x]"

  by (rule sorted.Cons) auto

lemma sorted_many:

  "x \<le> y \<Longrightarrow> sorted (y # zs) \<Longrightarrow> sorted (x # y # zs)"

  by (rule sorted.Cons) (cases "y # zs" rule: sorted.cases, auto)

lemma sorted_many_eq [simp, code]:

  "sorted (x # y # zs) \<longleftrightarrow> x \<le> y \<and> sorted (y # zs)"

  by (auto intro: sorted_many elim: sorted.cases)

lemma [code]:

  "sorted [] \<longleftrightarrow> True"

  "sorted [x] \<longleftrightarrow> True"

  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))"

definition sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where

"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)"

abbreviation "sort \<equiv> sort_key (\<lambda>x. x)"

abbreviation "insort \<equiv> insort_key (\<lambda>x. x)"

abbreviation "insort_insert \<equiv> insort_insert_key (\<lambda>x. x)"

end

subsubsection {* List comprehension *}

text{* Input syntax for Haskell-like list comprehension notation.

Typical example: @{text"[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x \<noteq> y]"},

the list of all pairs of distinct elements from @{text xs} and @{text ys}.

The syntax is as in Haskell, except that @{text"|"} becomes a dot

(like in Isabelle's set comprehension): @{text"[e. x \<leftarrow> xs, \<dots>]"} rather than

\verb![e| x <- xs, ...]!.

The qualifiers after the dot are

\begin{description}

\item[generators] @{text"p \<leftarrow> xs"},

 where @{text p} is a pattern and @{text xs} an expression of list type, or

\item[guards] @{text"b"}, where @{text b} is a boolean expression.

%\item[local bindings] @ {text"let x = e"}.

\end{description}

Just like in Haskell, list comprehension is just a shorthand. To avoid

misunderstandings, the translation into desugared form is not reversed

upon output. Note that the translation of @{text"[e. x \<leftarrow> xs]"} is

optmized to @{term"map (%x. e) xs"}.

It is easy to write short list comprehensions which stand for complex

expressions. During proofs, they may become unreadable (and

mangled). In such cases it can be advisable to introduce separate

definitions for the list comprehensions in question.  *}

nonterminal lc_qual and lc_quals

syntax

  "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  ("[_ . __")

  "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ <- _")

  "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")

  (*"_lc_let" :: "letbinds => lc_qual"  ("let _")*)

  "_lc_end" :: "lc_quals" ("]")

  "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals"  (", __")

  "_lc_abs" :: "'a => 'b list => 'b list"

(* These are easier than ML code but cannot express the optimized

   translation of [e. p<-xs]

translations

  "[e. p<-xs]" => "concat(map (_lc_abs p [e]) xs)"

  "_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)"

   => "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)"

  "[e. P]" => "if P then [e] else []"

  "_listcompr e (_lc_test P) (_lc_quals Q Qs)"

   => "if P then (_listcompr e Q Qs) else []"

  "_listcompr e (_lc_let b) (_lc_quals Q Qs)"

   => "_Let b (_listcompr e Q Qs)"

*)

syntax (xsymbols)

  "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ \<leftarrow> _")

syntax (HTML output)

  "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ \<leftarrow> _")

parse_translation {*

  let

    val NilC = Syntax.const @{const_syntax Nil};

    val ConsC = Syntax.const @{const_syntax Cons};

    val mapC = Syntax.const @{const_syntax map};

    val concatC = Syntax.const @{const_syntax concat};

    val IfC = Syntax.const @{const_syntax If};

    fun single x = ConsC $ x $ NilC;

    fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)

      let

        (* FIXME proper name context!? *)

        val x =

          Free (singleton (Name.variant_list (fold Term.add_free_names [p, e] [])) "x", dummyT);

        val e = if opti then single e else e;

        val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e;

        val case2 =

          Syntax.const @{syntax_const "_case1"} $

            Syntax.const @{const_syntax dummy_pattern} $ NilC;

        val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;

      in Syntax_Trans.abs_tr [x, Case_Translation.case_tr false ctxt [x, cs]] end;

    fun abs_tr ctxt p e opti =

      (case Term_Position.strip_positions p of

        Free (s, T) =>

          let

            val thy = Proof_Context.theory_of ctxt;

            val s' = Proof_Context.intern_const ctxt s;

          in

            if Sign.declared_const thy s'

            then (pat_tr ctxt p e opti, false)

            else (Syntax_Trans.abs_tr [p, e], true)

          end

      | _ => (pat_tr ctxt p e opti, false));

    fun lc_tr ctxt [e, Const (@{syntax_const "_lc_test"}, _) $ b, qs] =

          let

            val res =

              (case qs of

                Const (@{syntax_const "_lc_end"}, _) => single e

              | Const (@{syntax_const "_lc_quals"}, _) $ q $ qs => lc_tr ctxt [e, q, qs]);

          in IfC $ b $ res $ NilC end

      | lc_tr ctxt

            [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,

              Const(@{syntax_const "_lc_end"}, _)] =

          (case abs_tr ctxt p e true of

            (f, true) => mapC $ f $ es

          | (f, false) => concatC $ (mapC $ f $ es))

      | lc_tr ctxt

            [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,

              Const (@{syntax_const "_lc_quals"}, _) $ q $ qs] =

          let val e' = lc_tr ctxt [e, q, qs];

          in concatC $ (mapC $ (fst (abs_tr ctxt p e' false)) $ es) end;

  in [(@{syntax_const "_listcompr"}, lc_tr)] end

*}

ML_val {*

  let

    val read = Syntax.read_term @{context};

    fun check s1 s2 = read s1 aconv read s2 orelse error ("Check failed: " ^ quote s1);

  in

    check "[(x,y,z). b]" "if b then [(x, y, z)] else []";

    check "[(x,y,z). x\<leftarrow>xs]" "map (\<lambda>x. (x, y, z)) xs";

    check "[e x y. x\<leftarrow>xs, y\<leftarrow>ys]" "concat (map (\<lambda>x. map (\<lambda>y. e x y) ys) xs)";

    check "[(x,y,z). x<a, x>b]" "if x < a then if b < x then [(x, y, z)] else [] else []";

    check "[(x,y,z). x\<leftarrow>xs, x>b]" "concat (map (\<lambda>x. if b < x then [(x, y, z)] else []) xs)";

    check "[(x,y,z). x<a, x\<leftarrow>xs]" "if x < a then map (\<lambda>x. (x, y, z)) xs else []";

    check "[(x,y). Cons True x \<leftarrow> xs]"

      "concat (map (\<lambda>xa. case xa of [] \<Rightarrow> [] | True # x \<Rightarrow> [(x, y)] | False # x \<Rightarrow> []) xs)";

    check "[(x,y,z). Cons x [] \<leftarrow> xs]"

      "concat (map (\<lambda>xa. case xa of [] \<Rightarrow> [] | [x] \<Rightarrow> [(x, y, z)] | x # aa # lista \<Rightarrow> []) xs)";

    check "[(x,y,z). x<a, x>b, x=d]"

      "if x < a then if b < x then if x = d then [(x, y, z)] else [] else [] else []";

    check "[(x,y,z). x<a, x>b, y\<leftarrow>ys]"

      "if x < a then if b < x then map (\<lambda>y. (x, y, z)) ys else [] else []";

    check "[(x,y,z). x<a, x\<leftarrow>xs,y>b]"

      "if x < a then concat (map (\<lambda>x. if b < y then [(x, y, z)] else []) xs) else []";

    check "[(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys]"

      "if x < a then concat (map (\<lambda>x. map (\<lambda>y. (x, y, z)) ys) xs) else []";

    check "[(x,y,z). x\<leftarrow>xs, x>b, y<a]"

      "concat (map (\<lambda>x. if b < x then if y < a then [(x, y, z)] else [] else []) xs)";

    check "[(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys]"

      "concat (map (\<lambda>x. if b < x then map (\<lambda>y. (x, y, z)) ys else []) xs)";

    check "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x]"

      "concat (map (\<lambda>x. concat (map (\<lambda>y. if x < y then [(x, y, z)] else []) ys)) xs)";

    check "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs]"

      "concat (map (\<lambda>x. concat (map (\<lambda>y. map (\<lambda>z. (x, y, z)) zs) ys)) xs)"

  end;

*}

(*

term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]"

*)

ML {*

(* Simproc for rewriting list comprehensions applied to List.set to set

   comprehension. *)

signature LIST_TO_SET_COMPREHENSION =

sig

  val simproc : Proof.context -> cterm -> thm option

end

structure List_to_Set_Comprehension : LIST_TO_SET_COMPREHENSION =

struct

(* conversion *)

fun all_exists_conv cv ctxt ct =

  (case Thm.term_of ct of

    Const (@{const_name HOL.Ex}, _) $ Abs _ =>

      Conv.arg_conv (Conv.abs_conv (all_exists_conv cv o #2) ctxt) ct

  | _ => cv ctxt ct)

fun all_but_last_exists_conv cv ctxt ct =

  (case Thm.term_of ct of

    Const (@{const_name HOL.Ex}, _) $ Abs (_, _, Const (@{const_name HOL.Ex}, _) $ _) =>

      Conv.arg_conv (Conv.abs_conv (all_but_last_exists_conv cv o #2) ctxt) ct

  | _ => cv ctxt ct)

fun Collect_conv cv ctxt ct =

  (case Thm.term_of ct of

    Const (@{const_name Set.Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct

  | _ => raise CTERM ("Collect_conv", [ct]))

fun rewr_conv' th = Conv.rewr_conv (mk_meta_eq th)

fun conjunct_assoc_conv ct =

  Conv.try_conv

    (rewr_conv' @{thm conj_assoc} then_conv HOLogic.conj_conv Conv.all_conv conjunct_assoc_conv) ct

fun right_hand_set_comprehension_conv conv ctxt =

  HOLogic.Trueprop_conv (HOLogic.eq_conv Conv.all_conv

    (Collect_conv (all_exists_conv conv o #2) ctxt))

(* term abstraction of list comprehension patterns *)

datatype termlets = If | Case of (typ * int)

fun simproc ctxt redex =

  let

    val set_Nil_I = @{thm trans} OF [@{thm set.simps(1)}, @{thm empty_def}]

    val set_singleton = @{lemma "set [a] = {x. x = a}" by simp}

    val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp}

    val del_refl_eq = @{lemma "(t = t & P) == P" by simp}

    fun mk_set T = Const (@{const_name List.set}, HOLogic.listT T --> HOLogic.mk_setT T)

    fun dest_set (Const (@{const_name List.set}, _) $ xs) = xs

    fun dest_singleton_list (Const (@{const_name List.Cons}, _)

          $ t $ (Const (@{const_name List.Nil}, _))) = t

      | dest_singleton_list t = raise TERM ("dest_singleton_list", [t])

    (* We check that one case returns a singleton list and all other cases

       return [], and return the index of the one singleton list case *)

    fun possible_index_of_singleton_case cases =

      let

        fun check (i, case_t) s =

          (case strip_abs_body case_t of

            (Const (@{const_name List.Nil}, _)) => s

          | _ => (case s of SOME NONE => SOME (SOME i) | _ => NONE))

      in

        fold_index check cases (SOME NONE) |> the_default NONE

      end

    (* returns (case_expr type index chosen_case constr_name) option  *)

    fun dest_case case_term =

      let

        val (case_const, args) = strip_comb case_term

      in

        (case try dest_Const case_const of

          SOME (c, T) =>

            (case Ctr_Sugar.ctr_sugar_of_case ctxt c of

              SOME {ctrs, ...} =>

                (case possible_index_of_singleton_case (fst (split_last args)) of

                  SOME i =>

                    let

                      val constr_names = map (fst o dest_Const) ctrs

                      val (Ts, _) = strip_type T

                      val T' = List.last Ts

                    in SOME (List.last args, T', i, nth args i, nth constr_names i) end

                | NONE => NONE)

            | NONE => NONE)

        | NONE => NONE)

      end

    (* returns condition continuing term option *)

    fun dest_if (Const (@{const_name If}, _) $ cond $ then_t $ Const (@{const_name Nil}, _)) =

          SOME (cond, then_t)

      | dest_if _ = NONE

    fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1

      | tac ctxt (If :: cont) =

          Splitter.split_tac [@{thm split_if}] 1

          THEN rtac @{thm conjI} 1

          THEN rtac @{thm impI} 1

          THEN Subgoal.FOCUS (fn {prems, context, ...} =>

            CONVERSION (right_hand_set_comprehension_conv (K

              (HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv

               then_conv

               rewr_conv' @{lemma "(True & P) = P" by simp})) context) 1) ctxt 1

          THEN tac ctxt cont

          THEN rtac @{thm impI} 1

          THEN Subgoal.FOCUS (fn {prems, context, ...} =>

              CONVERSION (right_hand_set_comprehension_conv (K

                (HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv

                 then_conv rewr_conv' @{lemma "(False & P) = False" by simp})) context) 1) ctxt 1

          THEN rtac set_Nil_I 1

      | tac ctxt (Case (T, i) :: cont) =

          let

            val SOME {injects, distincts, case_thms, split, ...} =

              Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type T))

          in

            (* do case distinction *)

            Splitter.split_tac [split] 1

            THEN EVERY (map_index (fn (i', _) =>

              (if i' < length case_thms - 1 then rtac @{thm conjI} 1 else all_tac)

              THEN REPEAT_DETERM (rtac @{thm allI} 1)

              THEN rtac @{thm impI} 1

              THEN (if i' = i then

                (* continue recursively *)

                Subgoal.FOCUS (fn {prems, context, ...} =>

                  CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K

                      ((HOLogic.conj_conv

                        (HOLogic.eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_conv

                          (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq injects))))

                        Conv.all_conv)

                        then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq))

                        then_conv conjunct_assoc_conv)) context

                    then_conv (HOLogic.Trueprop_conv (HOLogic.eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>

                      Conv.repeat_conv

                        (all_but_last_exists_conv

                          (K (rewr_conv'

                            @{lemma "(EX x. x = t & P x) = P t" by simp})) ctxt)) context)))) 1) ctxt 1

                THEN tac ctxt cont

              else

                Subgoal.FOCUS (fn {prems, context, ...} =>

                  CONVERSION

                    (right_hand_set_comprehension_conv (K

                      (HOLogic.conj_conv

                        ((HOLogic.eq_conv Conv.all_conv

                          (rewr_conv' (List.last prems))) then_conv

                          (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) distincts)))

                        Conv.all_conv then_conv

                        (rewr_conv' @{lemma "(False & P) = False" by simp}))) context then_conv

                      HOLogic.Trueprop_conv

                        (HOLogic.eq_conv Conv.all_conv

                          (Collect_conv (fn (_, ctxt) =>

                            Conv.repeat_conv

                              (Conv.bottom_conv

                                (K (rewr_conv'

                                  @{lemma "(EX x. P) = P" by simp})) ctxt)) context))) 1) ctxt 1

                THEN rtac set_Nil_I 1)) case_thms)

          end

    fun make_inner_eqs bound_vs Tis eqs t =

      (case dest_case t of

        SOME (x, T, i, cont, constr_name) =>

          let

            val (vs, body) = strip_abs (Envir.eta_long (map snd bound_vs) cont)

            val x' = incr_boundvars (length vs) x

            val eqs' = map (incr_boundvars (length vs)) eqs

            val constr_t =

              list_comb

                (Const (constr_name, map snd vs ---> T), map Bound (((length vs) - 1) downto 0))

            val constr_eq = Const (@{const_name HOL.eq}, T --> T --> @{typ bool}) $ constr_t $ x'

          in

            make_inner_eqs (rev vs @ bound_vs) (Case (T, i) :: Tis) (constr_eq :: eqs') body

          end

      | NONE =>

          (case dest_if t of

            SOME (condition, cont) => make_inner_eqs bound_vs (If :: Tis) (condition :: eqs) cont

          | NONE =>

            if eqs = [] then NONE (* no rewriting, nothing to be done *)

            else

              let

                val Type (@{type_name List.list}, [rT]) = fastype_of1 (map snd bound_vs, t)

                val pat_eq =

                  (case try dest_singleton_list t of

                    SOME t' =>

                      Const (@{const_name HOL.eq}, rT --> rT --> @{typ bool}) $

                        Bound (length bound_vs) $ t'

                  | NONE =>

                      Const (@{const_name Set.member}, rT --> HOLogic.mk_setT rT --> @{typ bool}) $

                        Bound (length bound_vs) $ (mk_set rT $ t))

                val reverse_bounds = curry subst_bounds

                  ((map Bound ((length bound_vs - 1) downto 0)) @ [Bound (length bound_vs)])

                val eqs' = map reverse_bounds eqs

                val pat_eq' = reverse_bounds pat_eq

                val inner_t =

                  fold (fn (_, T) => fn t => HOLogic.exists_const T $ absdummy T t)

                    (rev bound_vs) (fold (curry HOLogic.mk_conj) eqs' pat_eq')

                val lhs = term_of redex

                val rhs = HOLogic.mk_Collect ("x", rT, inner_t)

                val rewrite_rule_t = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))

              in

                SOME

                  ((Goal.prove ctxt [] [] rewrite_rule_t

                    (fn {context, ...} => tac context (rev Tis))) RS @{thm eq_reflection})

              end))

  in

    make_inner_eqs [] [] [] (dest_set (term_of redex))

  end

end

*}

simproc_setup list_to_set_comprehension ("set xs") = {* K List_to_Set_Comprehension.simproc *}

code_datatype set coset

hide_const (open) coset

subsubsection {* @{const Nil} and @{const Cons} *}

lemma not_Cons_self [simp]:

  "xs \<noteq> x # xs"

by (induct xs) auto

lemma not_Cons_self2 [simp]:

  "x # xs \<noteq> xs"

by (rule not_Cons_self [symmetric])

lemma neq_Nil_conv: "(xs \<noteq> []) = (\<exists>y ys. xs = y # ys)"

by (induct xs) auto

lemma tl_Nil: "tl xs = [] \<longleftrightarrow> xs = [] \<or> (EX x. xs = [x])"

by (cases xs) auto

lemma Nil_tl: "[] = tl xs \<longleftrightarrow> xs = [] \<or> (EX x. xs = [x])"

by (cases xs) auto

lemma length_induct:

  "(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs"

by (fact measure_induct)

lemma list_nonempty_induct [consumes 1, case_names single cons]:

  assumes "xs \<noteq> []"

  assumes single: "\<And>x. P [x]"

  assumes cons: "\<And>x xs. xs \<noteq> [] \<Longrightarrow> P xs \<Longrightarrow> P (x # xs)"

  shows "P xs"

using `xs \<noteq> []` proof (induct xs)

  case Nil then show ?case by simp

next

  case (Cons x xs)

  show ?case

  proof (cases xs)

    case Nil

    with single show ?thesis by simp

  next

    case Cons

    show ?thesis

    proof (rule cons)

      from Cons show "xs \<noteq> []" by simp

      with Cons.hyps show "P xs" .

    qed

  qed

qed

lemma inj_split_Cons: "inj_on (\<lambda>(xs, n). n#xs) X"

  by (auto intro!: inj_onI)

subsubsection {* @{const length} *}

text {*

  Needs to come before @{text "@"} because of theorem @{text

  append_eq_append_conv}.

*}

lemma length_append [simp]: "length (xs @ ys) = length xs + length ys"

by (induct xs) auto

lemma length_map [simp]: "length (map f xs) = length xs"

by (induct xs) auto

lemma length_rev [simp]: "length (rev xs) = length xs"

by (induct xs) auto

lemma length_tl [simp]: "length (tl xs) = length xs - 1"

by (cases xs) auto

lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])"

by (induct xs) auto

lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])"

by (induct xs) auto

lemma length_pos_if_in_set: "x : set xs \<Longrightarrow> length xs > 0"

by auto

lemma length_Suc_conv:

"(length xs = Suc n) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"

by (induct xs) auto

lemma Suc_length_conv:

"(Suc n = length xs) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"

apply (induct xs, simp, simp)

apply blast

done

lemma impossible_Cons: "length xs <= length ys ==> xs = x # ys = False"

  by (induct xs) auto

lemma list_induct2 [consumes 1, case_names Nil Cons]:

  "length xs = length ys \<Longrightarrow> P [] [] \<Longrightarrow>

   (\<And>x xs y ys. length xs = length ys \<Longrightarrow> P xs ys \<Longrightarrow> P (x#xs) (y#ys))

   \<Longrightarrow> P xs ys"

proof (induct xs arbitrary: ys)

  case Nil then show ?case by simp

next

  case (Cons x xs ys) then show ?case by (cases ys) simp_all

qed

lemma list_induct3 [consumes 2, case_names Nil Cons]:

  "length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> P [] [] [] \<Longrightarrow>

   (\<And>x xs y ys z zs. length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> P xs ys zs \<Longrightarrow> P (x#xs) (y#ys) (z#zs))

   \<Longrightarrow> P xs ys zs"

proof (induct xs arbitrary: ys zs)

  case Nil then show ?case by simp

next

  case (Cons x xs ys zs) then show ?case by (cases ys, simp_all)

    (cases zs, simp_all)

qed

lemma list_induct4 [consumes 3, case_names Nil Cons]:

  "length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> length zs = length ws \<Longrightarrow>

   P [] [] [] [] \<Longrightarrow> (\<And>x xs y ys z zs w ws. length xs = length ys \<Longrightarrow>

   length ys = length zs \<Longrightarrow> length zs = length ws \<Longrightarrow> P xs ys zs ws \<Longrightarrow>

   P (x#xs) (y#ys) (z#zs) (w#ws)) \<Longrightarrow> P xs ys zs ws"

proof (induct xs arbitrary: ys zs ws)

  case Nil then show ?case by simp

next

  case (Cons x xs ys zs ws) then show ?case by ((cases ys, simp_all), (cases zs,simp_all)) (cases ws, simp_all)

qed

lemma list_induct2': 

  "\<lbrakk> P [] [];

  \<And>x xs. P (x#xs) [];

  \<And>y ys. P [] (y#ys);

   \<And>x xs y ys. P xs ys  \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk>

 \<Longrightarrow> P xs ys"

by (induct xs arbitrary: ys) (case_tac x, auto)+

lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False"

by (rule Eq_FalseI) auto

simproc_setup list_neq ("(xs::'a list) = ys") = {*

(*

Reduces xs=ys to False if xs and ys cannot be of the same length.

This is the case if the atomic sublists of one are a submultiset

of those of the other list and there are fewer Cons's in one than the other.

*)

let

fun len (Const(@{const_name Nil},_)) acc = acc

  | len (Const(@{const_name Cons},_) $ _ $ xs) (ts,n) = len xs (ts,n+1)

  | len (Const(@{const_name append},_) $ xs $ ys) acc = len xs (len ys acc)

  | len (Const(@{const_name rev},_) $ xs) acc = len xs acc

  | len (Const(@{const_name map},_) $ _ $ xs) acc = len xs acc

  | len t (ts,n) = (t::ts,n);

val ss = simpset_of @{context};

fun list_neq ctxt ct =

  let

    val (Const(_,eqT) $ lhs $ rhs) = Thm.term_of ct;

    val (ls,m) = len lhs ([],0) and (rs,n) = len rhs ([],0);

    fun prove_neq() =

      let

        val Type(_,listT::_) = eqT;

        val size = HOLogic.size_const listT;

        val eq_len = HOLogic.mk_eq (size $ lhs, size $ rhs);

        val neq_len = HOLogic.mk_Trueprop (HOLogic.Not $ eq_len);

        val thm = Goal.prove ctxt [] [] neq_len

          (K (simp_tac (put_simpset ss ctxt) 1));

      in SOME (thm RS @{thm neq_if_length_neq}) end

  in

    if m < n andalso submultiset (op aconv) (ls,rs) orelse

       n < m andalso submultiset (op aconv) (rs,ls)

    then prove_neq() else NONE

  end;

in K list_neq end;

*}

subsubsection {* @{text "@"} -- append *}

lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"

by (induct xs) auto

lemma append_Nil2 [simp]: "xs @ [] = xs"

by (induct xs) auto

lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"

by (induct xs) auto

lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])"

by (induct xs) auto

lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])"

by (induct xs) auto

lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])"

by (induct xs) auto

lemma append_eq_append_conv [simp]:

 "length xs = length ys \<or> length us = length vs

 ==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"

apply (induct xs arbitrary: ys)

 apply (case_tac ys, simp, force)

apply (case_tac ys, force, simp)

done

lemma append_eq_append_conv2: "(xs @ ys = zs @ ts) =

  (EX us. xs = zs @ us & us @ ys = ts | xs @ us = zs & ys = us@ ts)"

apply (induct xs arbitrary: ys zs ts)

 apply fastforce

apply(case_tac zs)

 apply simp

apply fastforce

done

lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)"

by simp

lemma append1_eq_conv [iff]: "(xs @ [x] = ys @ [y]) = (xs = ys \<and> x = y)"

by simp

lemma append_same_eq [iff, induct_simp]: "(ys @ xs = zs @ xs) = (ys = zs)"

by simp

lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])"

using append_same_eq [of _ _ "[]"] by auto

lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"

using append_same_eq [of "[]"] by auto

lemma hd_Cons_tl [simp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"

by (induct xs) auto

lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"

by (induct xs) auto

lemma hd_append2 [simp]: "xs \<noteq> [] ==> hd (xs @ ys) = hd xs"

by (simp add: hd_append split: list.split)

lemma tl_append: "tl (xs @ ys) = (case xs of [] => tl ys | z#zs => zs @ ys)"

by (simp split: list.split)

lemma tl_append2 [simp]: "xs \<noteq> [] ==> tl (xs @ ys) = tl xs @ ys"

by (simp add: tl_append split: list.split)

lemma Cons_eq_append_conv: "x#xs = ys@zs =

 (ys = [] & x#xs = zs | (EX ys'. x#ys' = ys & xs = ys'@zs))"

by(cases ys) auto

lemma append_eq_Cons_conv: "(ys@zs = x#xs) =

 (ys = [] & zs = x#xs | (EX ys'. ys = x#ys' & ys'@zs = xs))"

by(cases ys) auto

text {* Trivial rules for solving @{text "@"}-equations automatically. *}

lemma eq_Nil_appendI: "xs = ys ==> xs = [] @ ys"

by simp

lemma Cons_eq_appendI:

"[| x # xs1 = ys; xs = xs1 @ zs |] ==> x # xs = ys @ zs"

by (drule sym) simp

lemma append_eq_appendI:

"[| xs @ xs1 = zs; ys = xs1 @ us |] ==> xs @ ys = zs @ us"

by (drule sym) simp

text {*

Simplification procedure for all list equalities.

Currently only tries to rearrange @{text "@"} to see if

- both lists end in a singleton list,

- or both lists end in the same list.

*}

simproc_setup list_eq ("(xs::'a list) = ys")  = {*

  let

    fun last (cons as Const (@{const_name Cons}, _) $ _ $ xs) =

          (case xs of Const (@{const_name Nil}, _) => cons | _ => last xs)

      | last (Const(@{const_name append},_) $ _ $ ys) = last ys

      | last t = t;

    fun list1 (Const(@{const_name Cons},_) $ _ $ Const(@{const_name Nil},_)) = true

      | list1 _ = false;

    fun butlast ((cons as Const(@{const_name Cons},_) $ x) $ xs) =