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