Theory List_to_Set_Comprehension_Examples

(*  Title:      HOL/ex/List_to_Set_Comprehension_Examples.thy
    Author:     Lukas Bulwahn
    Copyright   2011 TU Muenchen
*)

section ‹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 ∈ set as}"
by auto

lemma "set [(x, y, ys). x # y # ys <- as] = {(x, y, ys). x # y # ys ∈ set as}"
by auto

lemma "set [(x, y, z, zs). x # y # z # zs <- as] = {(x, y, z, zs). x # y # z # zs ∈ set as}"
by auto

lemma "set [(zs, x, z, y). x # (y, z) # zs <- as] = {(zs, x, z, y). x # (y, z) # zs ∈ set as}" 
by auto

lemma "set [(x, y). x # y <- zs, x = x'] = {(x, y). x # y ∈ 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←xs] = {(x, y', z'). x ∈ set xs & y' = y & z = z'}"
by auto

lemma "set [e x y. x←xs, y←ys] = {z. ∃ x y. z = e x y & x ∈ set xs & y ∈ 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←xs, x>b] = {(x', y', z'). y = y' & z = z' & x' ∈ set xs & x' > b}"
by auto

lemma "set [(x,y,z). x<a, x←xs] = {(x', y', z'). y = y' & z = z' & x' ∈ set xs & x < a}"
by auto

lemma "set [(x,y). Cons True x ← xs] = {(x, y'). y = y' & Cons True x ∈ set xs}"
by auto

lemma "set [(x,y,z). Cons x [] ← xs] = {(x, y', z'). y = y' & z = z' & Cons x [] ∈ 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←ys] = {(x', y, z'). x = x' & y ∈ set ys & z = z' & x < a & x > b}"
by auto

lemma "set [(x,y,z). x<a, x←xs,y>b] = {(x',y',z'). x' ∈ set xs & y = y' & z = z' & x < a & y > b}"
by auto

lemma "set [(x,y,z). x<a, x←xs, y←ys] = {(x', y', z'). z = z' & x < a & x' ∈ set xs & y' ∈ set ys}"
by auto

lemma "set [(x,y,z). x←xs, x>b, y<a] = {(x', y', z'). y = y' & z = z' & x' ∈ set xs & x' > b & y < a}"
by auto

lemma "set [(x,y,z). x←xs, x>b, y←ys] = {(x', y', z'). z = z' & x' ∈ set xs & x' > b & y' ∈ set ys}"
by auto

lemma "set [(x,y,z). x←xs, y←ys,y>x] = {(x', y', z'). z = z' & x' ∈ set xs & y' ∈ set ys & y' > x'}"
by auto

lemma "set [(x,y,z). x←xs, y←ys,z←zs] = {(x', y', z'). x' ∈ set xs & y' ∈ set ys & z' ∈ set zs}"
by auto

end