src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy
author hoelzl
Thu Jan 31 11:31:27 2013 +0100 (2013-01-31)
changeset 50999 3de230ed0547
parent 49947 29cd291bfea6
child 54611 31afce809794
permissions -rw-r--r--
introduce order topology
bulwahn@48049
     1
(*  Title:      HOL/ex/Set_Comprehension_Pointfree_Tests.thy
rafal@48108
     2
    Author:     Lukas Bulwahn, Rafal Kolanski
bulwahn@48049
     3
    Copyright   2012 TU Muenchen
bulwahn@48049
     4
*)
bulwahn@48049
     5
bulwahn@48049
     6
header {* Tests for the set comprehension to pointfree simproc *}
bulwahn@48049
     7
bulwahn@48049
     8
theory Set_Comprehension_Pointfree_Tests
bulwahn@48049
     9
imports Main
bulwahn@48049
    10
begin
bulwahn@48049
    11
rafal@48108
    12
lemma
bulwahn@49851
    13
  "finite (UNIV::'a set) ==> finite {p. EX x::'a. p = (x, x)}"
bulwahn@49851
    14
  by simp
bulwahn@48049
    15
bulwahn@48049
    16
lemma
bulwahn@49851
    17
  "finite A ==> finite B ==> finite {f a b| a b. a : A \<and> b : B}"
bulwahn@49851
    18
  by simp
bulwahn@49851
    19
  
bulwahn@49851
    20
lemma
bulwahn@49851
    21
  "finite B ==> finite A' ==> finite {f a b| a b. a : A \<and> a : A' \<and> b : B}"
bulwahn@49851
    22
  by simp
bulwahn@48049
    23
bulwahn@48049
    24
lemma
bulwahn@49851
    25
  "finite A ==> finite B ==> finite {f a b| a b. a : A \<and> b : B \<and> b : B'}"
bulwahn@49851
    26
  by simp
bulwahn@48049
    27
bulwahn@48049
    28
lemma
bulwahn@49851
    29
  "finite A ==> finite B ==> finite C ==> finite {f a b c| a b c. a : A \<and> b : B \<and> c : C}"
bulwahn@49851
    30
  by simp
bulwahn@48049
    31
bulwahn@48049
    32
lemma
bulwahn@49851
    33
  "finite A ==> finite B ==> finite C ==> finite D ==>
bulwahn@49851
    34
     finite {f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D}"
bulwahn@49851
    35
  by simp
bulwahn@48049
    36
bulwahn@48049
    37
lemma
bulwahn@49851
    38
  "finite A ==> finite B ==> finite C ==> finite D ==> finite E ==>
bulwahn@49851
    39
    finite {f a b c d e | a b c d e. a : A \<and> b : B \<and> c : C \<and> d : D \<and> e : E}"
bulwahn@49851
    40
  by simp
rafal@48108
    41
bulwahn@49899
    42
lemma
bulwahn@49851
    43
  "finite A ==> finite B ==> finite C ==> finite D ==> finite E \<Longrightarrow>
bulwahn@49851
    44
    finite {f a d c b e | e b c d a. b : B \<and> a : A \<and> e : E' \<and> c : C \<and> d : D \<and> e : E \<and> b : B'}"
bulwahn@49851
    45
  by simp
rafal@48108
    46
rafal@48108
    47
lemma
rafal@48108
    48
  "\<lbrakk> finite A ; finite B ; finite C ; finite D \<rbrakk>
rafal@48108
    49
  \<Longrightarrow> finite ({f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D})"
rafal@48108
    50
  by simp
rafal@48108
    51
rafal@48108
    52
lemma
rafal@48108
    53
  "finite ((\<lambda>(a,b,c,d). f a b c d) ` (A \<times> B \<times> C \<times> D))
rafal@48108
    54
  \<Longrightarrow> finite ({f a b c d| a b c d. a : A \<and> b : B \<and> c : C \<and> d : D})"
rafal@48108
    55
  by simp
rafal@48108
    56
bulwahn@49762
    57
lemma
bulwahn@49766
    58
  "finite S ==> finite {s'. EX s:S. s' = f a e s}"
bulwahn@49766
    59
  by simp
bulwahn@49762
    60
bulwahn@49851
    61
lemma
bulwahn@49851
    62
  "finite A ==> finite B ==> finite {f a b| a b. a : A \<and> b : B \<and> a \<notin> Z}"
bulwahn@49851
    63
  by simp
bulwahn@49851
    64
bulwahn@49851
    65
lemma
bulwahn@49851
    66
  "finite A ==> finite B ==> finite R ==> finite {f a b x y| a b x y. a : A \<and> b : B \<and> (x,y) \<in> R}"
bulwahn@49851
    67
by simp
bulwahn@49851
    68
bulwahn@49851
    69
lemma
bulwahn@49851
    70
  "finite A ==> finite B ==> finite R ==> finite {f a b x y| a b x y. a : A \<and> (x,y) \<in> R \<and> b : B}"
bulwahn@49851
    71
by simp
bulwahn@49851
    72
bulwahn@49851
    73
lemma
bulwahn@49851
    74
  "finite A ==> finite B ==> finite R ==> finite {f a (x, b) y| y b x a. a : A \<and> (x,y) \<in> R \<and> b : B}"
bulwahn@49851
    75
by simp
bulwahn@49851
    76
bulwahn@49851
    77
lemma
bulwahn@49851
    78
  "finite A ==> finite AA ==> finite B ==> finite {f a b| a b. (a : A \<or> a : AA) \<and> b : B \<and> a \<notin> Z}"
bulwahn@49851
    79
by simp
bulwahn@49851
    80
bulwahn@49851
    81
lemma
bulwahn@49851
    82
  "finite A1 ==> finite A2 ==> finite A3 ==> finite A4 ==> finite A5 ==> finite B ==>
bulwahn@49851
    83
     finite {f a b c | a b c. ((a : A1 \<and> a : A2) \<or> (a : A3 \<and> (a : A4 \<or> a : A5))) \<and> b : B \<and> a \<notin> Z}"
bulwahn@49851
    84
apply simp
bulwahn@49851
    85
oops
bulwahn@49851
    86
bulwahn@49853
    87
lemma "finite B ==> finite {c. EX x. x : B & c = a * x}"
bulwahn@49853
    88
by simp
bulwahn@49853
    89
bulwahn@49853
    90
lemma
bulwahn@49853
    91
  "finite A ==> finite B ==> finite {f a * g b |a b. a : A & b : B}"
bulwahn@49853
    92
by simp
bulwahn@49853
    93
bulwahn@49876
    94
lemma
bulwahn@49876
    95
  "finite S ==> inj (%(x, y). g x y) ==> finite {f x y| x y. g x y : S}"
bulwahn@49876
    96
  by (auto intro: finite_vimageI)
bulwahn@49876
    97
bulwahn@49876
    98
lemma
bulwahn@49876
    99
  "finite A ==> finite S ==> inj (%(x, y). g x y) ==> finite {f x y z | x y z. g x y : S & z : A}"
bulwahn@49876
   100
  by (auto intro: finite_vimageI)
bulwahn@49876
   101
bulwahn@49876
   102
lemma
bulwahn@49876
   103
  "finite S ==> finite A ==> inj (%(x, y). g x y) ==> inj (%(x, y). h x y)
bulwahn@49876
   104
    ==> finite {f a b c d | a b c d. g a c : S & h b d : A}"
bulwahn@49876
   105
  by (auto intro: finite_vimageI)
bulwahn@49876
   106
bulwahn@49899
   107
lemma
bulwahn@49899
   108
  assumes "finite S" shows "finite {(a,b,c,d). ([a, b], [c, d]) : S}"
bulwahn@49899
   109
using assms by (auto intro!: finite_vimageI simp add: inj_on_def)
bulwahn@49899
   110
  (* injectivity to be automated with further rules and automation *)
bulwahn@49876
   111
rafal@48108
   112
schematic_lemma (* check interaction with schematics *)
rafal@48108
   113
  "finite {x :: ?'A \<Rightarrow> ?'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b}
bulwahn@49851
   114
   = finite ((\<lambda>(b :: ?'B, a:: ?'A). Pair_Rep a b) ` (UNIV \<times> UNIV))"
rafal@48108
   115
  by simp
bulwahn@48049
   116
bulwahn@48174
   117
bulwahn@49876
   118
section {* Testing simproc in code generation *}
bulwahn@49876
   119
bulwahn@49876
   120
definition union :: "nat set => nat set => nat set"
bulwahn@49876
   121
where
bulwahn@49876
   122
  "union A B = {x. x : A \<or> x : B}"
bulwahn@49876
   123
bulwahn@49876
   124
definition common_subsets :: "nat set => nat set => nat set set"
bulwahn@49876
   125
where
bulwahn@49876
   126
  "common_subsets S1 S2 = {S. S \<subseteq> S1 \<and> S \<subseteq> S2}"
bulwahn@49876
   127
bulwahn@49947
   128
definition products :: "nat set => nat set => nat set"
bulwahn@49947
   129
where
bulwahn@49947
   130
  "products A B = {c. EX a b. a : A & b : B & c = a * b}"
bulwahn@49947
   131
bulwahn@49947
   132
export_code products in Haskell file -
bulwahn@49947
   133
bulwahn@49947
   134
export_code union common_subsets products in Haskell file -
bulwahn@49876
   135
bulwahn@48049
   136
end