author | wenzelm |
Thu, 30 May 2013 20:38:50 +0200 | |
changeset 52252 | 81fcc11d8c65 |
parent 41465 | 79ec1ddf49df |
child 58889 | 5b7a9633cfa8 |
permissions | -rw-r--r-- |
41465
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
1 |
(* Title: HOL/ex/List_to_Set_Comprehension_Examples.thy |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
2 |
Author: Lukas Bulwahn |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
3 |
Copyright 2011 TU Muenchen |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
4 |
*) |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
5 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
6 |
header {* Examples for the list comprehension to set comprehension simproc *} |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
7 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
8 |
theory List_to_Set_Comprehension_Examples |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
9 |
imports Main |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
10 |
begin |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
11 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
12 |
text {* |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
13 |
Examples that show and test the simproc that rewrites list comprehensions |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
14 |
applied to List.set to set comprehensions. |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
15 |
*} |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
16 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
17 |
subsection {* Some own examples for set (case ..) simpproc *} |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
18 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
19 |
lemma "set [(x, xs). x # xs <- as] = {(x, xs). x # xs \<in> set as}" |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
20 |
by auto |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
21 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
22 |
lemma "set [(x, y, ys). x # y # ys <- as] = {(x, y, ys). x # y # ys \<in> set as}" |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
23 |
by auto |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
24 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
25 |
lemma "set [(x, y, z, zs). x # y # z # zs <- as] = {(x, y, z, zs). x # y # z # zs \<in> set as}" |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
26 |
by auto |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
27 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
28 |
lemma "set [(zs, x, z, y). x # (y, z) # zs <- as] = {(zs, x, z, y). x # (y, z) # zs \<in> set as}" |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
29 |
by auto |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
30 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
31 |
lemma "set [(x, y). x # y <- zs, x = x'] = {(x, y). x # y \<in> set zs & x = x'}" |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
32 |
by auto |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
33 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
34 |
subsection {* Existing examples from the List theory *} |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
35 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
36 |
lemma "set [(x,y,z). b] = {(x', y', z'). x = x' & y = y' & z = z' & b}" |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
37 |
by auto |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
38 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
39 |
lemma "set [(x,y,z). x\<leftarrow>xs] = {(x, y', z'). x \<in> set xs & y' = y & z = z'}" |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
40 |
by auto |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
41 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
42 |
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}" |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
43 |
by auto |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
44 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
45 |
lemma "set [(x,y,z). x<a, x>b] = {(x', y', z'). x' = x & y' = y & z = z' & x < a & x>b}" |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
46 |
by auto |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
47 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
48 |
lemma "set [(x,y,z). x\<leftarrow>xs, x>b] = {(x', y', z'). y = y' & z = z' & x' \<in> set xs & x' > b}" |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
49 |
by auto |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
50 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
51 |
lemma "set [(x,y,z). x<a, x\<leftarrow>xs] = {(x', y', z'). y = y' & z = z' & x' \<in> set xs & x < a}" |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
52 |
by auto |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
53 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
54 |
lemma "set [(x,y). Cons True x \<leftarrow> xs] = {(x, y'). y = y' & Cons True x \<in> set xs}" |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
55 |
by auto |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
56 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
57 |
lemma "set [(x,y,z). Cons x [] \<leftarrow> xs] = {(x, y', z'). y = y' & z = z' & Cons x [] \<in> set xs}" |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
58 |
by auto |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
59 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
60 |
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}" |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
61 |
by auto |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
62 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
63 |
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}" |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
64 |
by auto |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
65 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
66 |
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}" |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
67 |
by auto |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
68 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
69 |
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}" |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
70 |
by auto |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
71 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
72 |
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}" |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
73 |
by auto |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
74 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
75 |
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}" |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
76 |
by auto |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
77 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
78 |
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'}" |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
79 |
by auto |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
80 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
81 |
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}" |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
82 |
by auto |
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
83 |
|
79ec1ddf49df
adding example theory for list comprehension to set comprehension simproc
bulwahn
parents:
diff
changeset
|
84 |
end |