src/HOL/ex/List_to_Set_Comprehension_Examples.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 41465 79ec1ddf49df
child 58889 5b7a9633cfa8
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     1 (*  Title:      HOL/ex/List_to_Set_Comprehension_Examples.thy
     2     Author:     Lukas Bulwahn
     3     Copyright   2011 TU Muenchen
     4 *)
     5 
     6 header {* 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