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