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