Moved list comprehension into List
authornipkow
Fri Jun 01 22:09:16 2007 +0200 (2007-06-01)
changeset 23192ec73b9707d48
parent 23191 b7f3a30f3d7f
child 23193 1f2d94b6a8ef
Moved list comprehension into List
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
src/HOL/Library/List_Comprehension.thy
src/HOL/List.thy
     1.1 --- a/src/HOL/IsaMakefile	Fri Jun 01 20:34:12 2007 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Jun 01 22:09:16 2007 +0200
     1.3 @@ -197,7 +197,7 @@
     1.4    Library/EfficientNat.thy Library/ExecutableSet.thy Library/ExecutableRat.thy \
     1.5    Library/Executable_Real.thy \
     1.6    Library/MLString.thy Library/Infinite_Set.thy \
     1.7 -  Library/FuncSet.thy Library/Library.thy Library/List_Comprehension.thy \
     1.8 +  Library/FuncSet.thy Library/Library.thy \
     1.9    Library/List_Prefix.thy Library/State_Monad.thy Library/Multiset.thy Library/NatPair.thy \
    1.10    Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \
    1.11    Library/Nat_Infinity.thy Library/Word.thy \
     2.1 --- a/src/HOL/Library/Library.thy	Fri Jun 01 20:34:12 2007 +0200
     2.2 +++ b/src/HOL/Library/Library.thy	Fri Jun 01 22:09:16 2007 +0200
     2.3 @@ -17,7 +17,6 @@
     2.4    FuncSet
     2.5    GCD
     2.6    Infinite_Set
     2.7 -  List_Comprehension
     2.8    MLString
     2.9    Multiset
    2.10    NatPair
     3.1 --- a/src/HOL/Library/List_Comprehension.thy	Fri Jun 01 20:34:12 2007 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,50 +0,0 @@
     3.4 -(*  Title:      HOL/Library/List_Comprehension.thy
     3.5 -    ID:         $Id$
     3.6 -    Author:     Tobias Nipkow
     3.7 -*)
     3.8 -
     3.9 -header {* List Comprehension *}
    3.10 -
    3.11 -theory List_Comprehension
    3.12 -imports Main
    3.13 -begin
    3.14 -
    3.15 -text{* At the moment this theory provides only the input syntax for
    3.16 -list comprehension: @{text"[x. x \<leftarrow> xs, \<dots>]"} rather than
    3.17 -\verb![x| x <- xs, ...]! as in Haskell.
    3.18 -
    3.19 -The print translation from internal form to list comprehensions would
    3.20 -be nice. Unfortunately one cannot just turn the translations around
    3.21 -because in the final equality @{text p} occurs twice on the
    3.22 -right-hand side. Due to this restriction, the translation must be hand-coded.
    3.23 -
    3.24 -A more substantial extension would be proper theorem proving
    3.25 -support. For example, it would be nice if
    3.26 -@{text"set[f x y. x \<leftarrow> xs, y \<leftarrow> ys, P x y]"}
    3.27 -produced something like
    3.28 -@{term"{z. EX x: set xs. EX y:set ys. P x y \<and> z = f x y}"}.  *}
    3.29 -
    3.30 -nonterminals lc_gentest
    3.31 -
    3.32 -syntax
    3.33 -"_listcompr" :: "'a \<Rightarrow> idt \<Rightarrow> 'b list \<Rightarrow> lc_gentest \<Rightarrow> 'a list" ("[_ . _ \<leftarrow> __")
    3.34 -"_lc_end" :: "lc_gentest" ("]")
    3.35 -"_lc_gen" :: "idt \<Rightarrow> 'a list \<Rightarrow> lc_gentest \<Rightarrow> lc_gentest" (",_ \<leftarrow> __")
    3.36 -"_lc_test" :: "bool \<Rightarrow> lc_gentest \<Rightarrow> lc_gentest" (",__")
    3.37 -
    3.38 -
    3.39 -translations
    3.40 - "[e. p\<leftarrow>xs]" => "map (%p. e) xs"
    3.41 - "_listcompr e p xs (_lc_gen q ys GT)" =>
    3.42 -  "concat (map (%p. _listcompr e q ys GT) xs)"
    3.43 - "_listcompr e p xs (_lc_test P GT)" => "_listcompr e p (filter (%p. P) xs) GT"
    3.44 -
    3.45 -(*
    3.46 -term "[(x,y). x \<leftarrow> xs, x<y]"
    3.47 -term "[(x,y). x \<leftarrow> xs, x<y, z\<leftarrow>zs]"
    3.48 -term "[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x<y]"
    3.49 -term "[(x,y,z). x \<leftarrow> xs, y \<leftarrow> ys, z\<leftarrow> zs]"
    3.50 -term "[x. x \<leftarrow> xs, x < a, x > b]"
    3.51 -*)
    3.52 -
    3.53 -end
     4.1 --- a/src/HOL/List.thy	Fri Jun 01 20:34:12 2007 +0200
     4.2 +++ b/src/HOL/List.thy	Fri Jun 01 22:09:16 2007 +0200
     4.3 @@ -219,6 +219,48 @@
     4.4  "allpairs f [] ys = []"
     4.5  "allpairs f (x # xs) ys = map (f x) ys @ allpairs f xs ys"
     4.6  
     4.7 +subsubsection {* List comprehehsion *}
     4.8 +
     4.9 +text{* At the moment this theory provides only the input syntax for
    4.10 +list comprehension: @{text"[x. x \<leftarrow> xs, \<dots>]"} rather than
    4.11 +\verb![x| x <- xs, ...]! as in Haskell.
    4.12 +
    4.13 +The print translation from internal form to list comprehensions would
    4.14 +be nice. Unfortunately one cannot just turn the translations around
    4.15 +because in the final equality @{text p} occurs twice on the
    4.16 +right-hand side. Due to this restriction, the translation must be hand-coded.
    4.17 +
    4.18 +A more substantial extension would be proper theorem proving
    4.19 +support. For example, it would be nice if
    4.20 +@{text"set[f x y. x \<leftarrow> xs, y \<leftarrow> ys, P x y]"}
    4.21 +produced something like
    4.22 +@{term"{z. EX x: set xs. EX y:set ys. P x y \<and> z = f x y}"}.  *}
    4.23 +
    4.24 +nonterminals lc_gentest
    4.25 +
    4.26 +syntax
    4.27 +"_listcompr" :: "'a \<Rightarrow> idt \<Rightarrow> 'b list \<Rightarrow> lc_gentest \<Rightarrow> 'a list" ("[_ . _ \<leftarrow> __")
    4.28 +"_listcompr" :: "'a \<Rightarrow> idt \<Rightarrow> 'b list \<Rightarrow> lc_gentest \<Rightarrow> 'a list" ("[_ . _ <- __")
    4.29 +"_lc_end" :: "lc_gentest" ("]")
    4.30 +"_lc_gen" :: "idt \<Rightarrow> 'a list \<Rightarrow> lc_gentest \<Rightarrow> lc_gentest" (",_ \<leftarrow> __")
    4.31 +"_lc_gen" :: "idt \<Rightarrow> 'a list \<Rightarrow> lc_gentest \<Rightarrow> lc_gentest" (",_ <- __")
    4.32 +"_lc_test" :: "bool \<Rightarrow> lc_gentest \<Rightarrow> lc_gentest" (",__")
    4.33 +
    4.34 +
    4.35 +translations
    4.36 +"[e. p\<leftarrow>xs]" => "map (%p. e) xs"
    4.37 +"_listcompr e p xs (_lc_gen q ys GT)" =>
    4.38 + "concat (map (%p. _listcompr e q ys GT) xs)"
    4.39 +"_listcompr e p xs (_lc_test P GT)" => "_listcompr e p (filter (%p. P) xs) GT"
    4.40 +
    4.41 +(* Some examples:
    4.42 +term "[(x,y). x \<leftarrow> xs, x<y]"
    4.43 +term "[(x,y). x \<leftarrow> xs, x<y, z\<leftarrow>zs]"
    4.44 +term "[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x<y]"
    4.45 +term "[(x,y,z). x \<leftarrow> xs, y \<leftarrow> ys, z\<leftarrow> zs]"
    4.46 +term "[x. x \<leftarrow> xs, x < a, x > b]"
    4.47 +*)
    4.48 +
    4.49  subsubsection {* @{const Nil} and @{const Cons} *}
    4.50  
    4.51  lemma not_Cons_self [simp]: