--- a/src/HOL/IsaMakefile Fri Jun 01 20:34:12 2007 +0200
+++ b/src/HOL/IsaMakefile Fri Jun 01 22:09:16 2007 +0200
@@ -197,7 +197,7 @@
Library/EfficientNat.thy Library/ExecutableSet.thy Library/ExecutableRat.thy \
Library/Executable_Real.thy \
Library/MLString.thy Library/Infinite_Set.thy \
- Library/FuncSet.thy Library/Library.thy Library/List_Comprehension.thy \
+ Library/FuncSet.thy Library/Library.thy \
Library/List_Prefix.thy Library/State_Monad.thy Library/Multiset.thy Library/NatPair.thy \
Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \
Library/Nat_Infinity.thy Library/Word.thy \
--- a/src/HOL/Library/Library.thy Fri Jun 01 20:34:12 2007 +0200
+++ b/src/HOL/Library/Library.thy Fri Jun 01 22:09:16 2007 +0200
@@ -17,7 +17,6 @@
FuncSet
GCD
Infinite_Set
- List_Comprehension
MLString
Multiset
NatPair
--- a/src/HOL/Library/List_Comprehension.thy Fri Jun 01 20:34:12 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,50 +0,0 @@
-(* Title: HOL/Library/List_Comprehension.thy
- ID: $Id$
- Author: Tobias Nipkow
-*)
-
-header {* List Comprehension *}
-
-theory List_Comprehension
-imports Main
-begin
-
-text{* At the moment this theory provides only the input syntax for
-list comprehension: @{text"[x. x \<leftarrow> xs, \<dots>]"} rather than
-\verb![x| x <- xs, ...]! as in Haskell.
-
-The print translation from internal form to list comprehensions would
-be nice. Unfortunately one cannot just turn the translations around
-because in the final equality @{text p} occurs twice on the
-right-hand side. Due to this restriction, the translation must be hand-coded.
-
-A more substantial extension would be proper theorem proving
-support. For example, it would be nice if
-@{text"set[f x y. x \<leftarrow> xs, y \<leftarrow> ys, P x y]"}
-produced something like
-@{term"{z. EX x: set xs. EX y:set ys. P x y \<and> z = f x y}"}. *}
-
-nonterminals lc_gentest
-
-syntax
-"_listcompr" :: "'a \<Rightarrow> idt \<Rightarrow> 'b list \<Rightarrow> lc_gentest \<Rightarrow> 'a list" ("[_ . _ \<leftarrow> __")
-"_lc_end" :: "lc_gentest" ("]")
-"_lc_gen" :: "idt \<Rightarrow> 'a list \<Rightarrow> lc_gentest \<Rightarrow> lc_gentest" (",_ \<leftarrow> __")
-"_lc_test" :: "bool \<Rightarrow> lc_gentest \<Rightarrow> lc_gentest" (",__")
-
-
-translations
- "[e. p\<leftarrow>xs]" => "map (%p. e) xs"
- "_listcompr e p xs (_lc_gen q ys GT)" =>
- "concat (map (%p. _listcompr e q ys GT) xs)"
- "_listcompr e p xs (_lc_test P GT)" => "_listcompr e p (filter (%p. P) xs) GT"
-
-(*
-term "[(x,y). x \<leftarrow> xs, x<y]"
-term "[(x,y). x \<leftarrow> xs, x<y, z\<leftarrow>zs]"
-term "[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x<y]"
-term "[(x,y,z). x \<leftarrow> xs, y \<leftarrow> ys, z\<leftarrow> zs]"
-term "[x. x \<leftarrow> xs, x < a, x > b]"
-*)
-
-end
--- a/src/HOL/List.thy Fri Jun 01 20:34:12 2007 +0200
+++ b/src/HOL/List.thy Fri Jun 01 22:09:16 2007 +0200
@@ -219,6 +219,48 @@
"allpairs f [] ys = []"
"allpairs f (x # xs) ys = map (f x) ys @ allpairs f xs ys"
+subsubsection {* List comprehehsion *}
+
+text{* At the moment this theory provides only the input syntax for
+list comprehension: @{text"[x. x \<leftarrow> xs, \<dots>]"} rather than
+\verb![x| x <- xs, ...]! as in Haskell.
+
+The print translation from internal form to list comprehensions would
+be nice. Unfortunately one cannot just turn the translations around
+because in the final equality @{text p} occurs twice on the
+right-hand side. Due to this restriction, the translation must be hand-coded.
+
+A more substantial extension would be proper theorem proving
+support. For example, it would be nice if
+@{text"set[f x y. x \<leftarrow> xs, y \<leftarrow> ys, P x y]"}
+produced something like
+@{term"{z. EX x: set xs. EX y:set ys. P x y \<and> z = f x y}"}. *}
+
+nonterminals lc_gentest
+
+syntax
+"_listcompr" :: "'a \<Rightarrow> idt \<Rightarrow> 'b list \<Rightarrow> lc_gentest \<Rightarrow> 'a list" ("[_ . _ \<leftarrow> __")
+"_listcompr" :: "'a \<Rightarrow> idt \<Rightarrow> 'b list \<Rightarrow> lc_gentest \<Rightarrow> 'a list" ("[_ . _ <- __")
+"_lc_end" :: "lc_gentest" ("]")
+"_lc_gen" :: "idt \<Rightarrow> 'a list \<Rightarrow> lc_gentest \<Rightarrow> lc_gentest" (",_ \<leftarrow> __")
+"_lc_gen" :: "idt \<Rightarrow> 'a list \<Rightarrow> lc_gentest \<Rightarrow> lc_gentest" (",_ <- __")
+"_lc_test" :: "bool \<Rightarrow> lc_gentest \<Rightarrow> lc_gentest" (",__")
+
+
+translations
+"[e. p\<leftarrow>xs]" => "map (%p. e) xs"
+"_listcompr e p xs (_lc_gen q ys GT)" =>
+ "concat (map (%p. _listcompr e q ys GT) xs)"
+"_listcompr e p xs (_lc_test P GT)" => "_listcompr e p (filter (%p. P) xs) GT"
+
+(* Some examples:
+term "[(x,y). x \<leftarrow> xs, x<y]"
+term "[(x,y). x \<leftarrow> xs, x<y, z\<leftarrow>zs]"
+term "[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x<y]"
+term "[(x,y,z). x \<leftarrow> xs, y \<leftarrow> ys, z\<leftarrow> zs]"
+term "[x. x \<leftarrow> xs, x < a, x > b]"
+*)
+
subsubsection {* @{const Nil} and @{const Cons} *}
lemma not_Cons_self [simp]: