# HG changeset patch
# User bulwahn
# Date 1294420243 -3600
# Node ID 79ec1ddf49dfa2362d1fc8ac1c21d9885f57cbba
# Parent  cb2e3e651893eb98875be4bb86638e4bb3378f7c
adding example theory for list comprehension to set comprehension simproc

diff -r cb2e3e651893 -r 79ec1ddf49df src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Jan 07 18:10:42 2011 +0100
+++ b/src/HOL/IsaMakefile	Fri Jan 07 18:10:43 2011 +0100
@@ -1041,7 +1041,8 @@
   ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy		\
   ex/Higher_Order_Logic.thy ex/Iff_Oracle.thy ex/Induction_Schema.thy	\
   ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy		\
-  ex/Intuitionistic.thy ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy	\
+  ex/Intuitionistic.thy ex/Lagrange.thy \
+  ex/List_to_Set_Comprehension_Examples.thy ex/LocaleTest2.thy ex/MT.thy	\
   ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy			\
   ex/Multiquote.thy ex/NatSum.thy ex/Normalization_by_Evaluation.thy	\
   ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy		\
diff -r cb2e3e651893 -r 79ec1ddf49df src/HOL/ex/List_to_Set_Comprehension_Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/List_to_Set_Comprehension_Examples.thy	Fri Jan 07 18:10:43 2011 +0100
@@ -0,0 +1,84 @@
+(*  Title:      HOL/ex/List_to_Set_Comprehension_Examples.thy
+    Author:     Lukas Bulwahn
+    Copyright   2011 TU Muenchen
+*)
+
+header {* Examples for the list comprehension to set comprehension simproc *}
+
+theory List_to_Set_Comprehension_Examples
+imports Main
+begin
+
+text {*
+Examples that show and test the simproc that rewrites list comprehensions
+applied to List.set to set comprehensions.
+*}
+
+subsection {* Some own examples for set (case ..) simpproc *}
+
+lemma "set [(x, xs). x # xs <- as] = {(x, xs). x # xs \<in> set as}"
+by auto
+
+lemma "set [(x, y, ys). x # y # ys <- as] = {(x, y, ys). x # y # ys \<in> set as}"
+by auto
+
+lemma "set [(x, y, z, zs). x # y # z # zs <- as] = {(x, y, z, zs). x # y # z # zs \<in> set as}"
+by auto
+
+lemma "set [(zs, x, z, y). x # (y, z) # zs <- as] = {(zs, x, z, y). x # (y, z) # zs \<in> set as}" 
+by auto
+
+lemma "set [(x, y). x # y <- zs, x = x'] = {(x, y). x # y \<in> set zs & x = x'}"
+by auto
+
+subsection {* Existing examples from the List theory *}
+
+lemma "set [(x,y,z). b] = {(x', y', z'). x = x' & y = y' & z = z' & b}"
+by auto
+
+lemma "set [(x,y,z). x\<leftarrow>xs] = {(x, y', z'). x \<in> set xs & y' = y & z = z'}"
+by auto
+
+lemma "set [e x y. x\<leftarrow>xs, y\<leftarrow>ys] = {z. \<exists> x y. z = e x y & x \<in> set xs & y \<in> set ys}"
+by auto
+
+lemma "set [(x,y,z). x<a, x>b] = {(x', y', z'). x' = x & y' = y & z = z' & x < a & x>b}"
+by auto
+
+lemma "set [(x,y,z). x\<leftarrow>xs, x>b] = {(x', y', z'). y = y' & z = z' & x' \<in> set xs & x' > b}"
+by auto
+
+lemma "set [(x,y,z). x<a, x\<leftarrow>xs] = {(x', y', z'). y = y' & z = z' & x' \<in> set xs & x < a}"
+by auto
+
+lemma "set [(x,y). Cons True x \<leftarrow> xs] = {(x, y'). y = y' & Cons True x \<in> set xs}"
+by auto
+
+lemma "set [(x,y,z). Cons x [] \<leftarrow> xs] = {(x, y', z'). y = y' & z = z' & Cons x [] \<in> set xs}"
+by auto
+
+lemma "set [(x,y,z). x<a, x>b, x=d] = {(x', y', z'). x = x' & y = y' & z = z' & x < a & x > b & x = d}"
+by auto
+
+lemma "set [(x,y,z). x<a, x>b, y\<leftarrow>ys] = {(x', y, z'). x = x' & y \<in> set ys & z = z' & x < a & x > b}"
+by auto
+
+lemma "set [(x,y,z). x<a, x\<leftarrow>xs,y>b] = {(x',y',z'). x' \<in> set xs & y = y' & z = z' & x < a & y > b}"
+by auto
+
+lemma "set [(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys] = {(x', y', z'). z = z' & x < a & x' \<in> set xs & y' \<in> set ys}"
+by auto
+
+lemma "set [(x,y,z). x\<leftarrow>xs, x>b, y<a] = {(x', y', z'). y = y' & z = z' & x' \<in> set xs & x' > b & y < a}"
+by auto
+
+lemma "set [(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys] = {(x', y', z'). z = z' & x' \<in> set xs & x' > b & y' \<in> set ys}"
+by auto
+
+lemma "set [(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x] = {(x', y', z'). z = z' & x' \<in> set xs & y' \<in> set ys & y' > x'}"
+by auto
+
+lemma "set [(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs] = {(x', y', z'). x' \<in> set xs & y' \<in> set ys & z' \<in> set zs}"
+by auto
+
+end
diff -r cb2e3e651893 -r 79ec1ddf49df src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri Jan 07 18:10:42 2011 +0100
+++ b/src/HOL/ex/ROOT.ML	Fri Jan 07 18:10:43 2011 +0100
@@ -71,7 +71,8 @@
   "Gauge_Integration",
   "Dedekind_Real",
   "Quicksort",
-  "Birthday_Paradoxon"
+  "Birthday_Paradoxon",
+  "List_to_Set_Comprehension_Examples"
 ];
 
 use_thy "SVC_Oracle";