src/HOL/Library/Set_Idioms.thy
author haftmann
Sun Nov 18 18:07:51 2018 +0000 (7 months ago)
changeset 69313 b021008c5397
parent 69004 f6a0c8115e9c
child 69325 4b6ddc5989fc
permissions -rw-r--r--
removed legacy input syntax
lp15@69004
     1
(*  Title:      HOL/Library/Set_Idioms.thy
lp15@69004
     2
    Author:     Lawrence Paulson (but borrowed from HOL Light)
lp15@69004
     3
*)
lp15@69004
     4
lp15@69004
     5
section \<open>Set Idioms\<close>
lp15@69004
     6
lp15@69004
     7
theory Set_Idioms
lp15@69004
     8
imports Countable_Set
lp15@69004
     9
lp15@69004
    10
begin
lp15@69004
    11
lp15@69004
    12
lp15@69004
    13
subsection\<open>Idioms for being a suitable union/intersection of something\<close>
lp15@69004
    14
lp15@69004
    15
definition union_of :: "('a set set \<Rightarrow> bool) \<Rightarrow> ('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
lp15@69004
    16
  (infixr "union'_of" 60)
lp15@69004
    17
  where "P union_of Q \<equiv> \<lambda>S. \<exists>\<U>. P \<U> \<and> \<U> \<subseteq> Collect Q \<and> \<Union>\<U> = S"
lp15@69004
    18
lp15@69004
    19
definition intersection_of :: "('a set set \<Rightarrow> bool) \<Rightarrow> ('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
lp15@69004
    20
  (infixr "intersection'_of" 60)
lp15@69004
    21
  where "P intersection_of Q \<equiv> \<lambda>S. \<exists>\<U>. P \<U> \<and> \<U> \<subseteq> Collect Q \<and> \<Inter>\<U> = S"
lp15@69004
    22
lp15@69004
    23
definition arbitrary:: "'a set set \<Rightarrow> bool" where "arbitrary \<U> \<equiv> True"
lp15@69004
    24
lp15@69004
    25
lemma union_of_inc: "\<lbrakk>P {S}; Q S\<rbrakk> \<Longrightarrow> (P union_of Q) S"
lp15@69004
    26
  by (auto simp: union_of_def)
lp15@69004
    27
lp15@69004
    28
lemma intersection_of_inc:
lp15@69004
    29
   "\<lbrakk>P {S}; Q S\<rbrakk> \<Longrightarrow> (P intersection_of Q) S"
lp15@69004
    30
  by (auto simp: intersection_of_def)
lp15@69004
    31
lp15@69004
    32
lemma union_of_mono:
lp15@69004
    33
   "\<lbrakk>(P union_of Q) S; \<And>x. Q x \<Longrightarrow> Q' x\<rbrakk> \<Longrightarrow> (P union_of Q') S"
lp15@69004
    34
  by (auto simp: union_of_def)
lp15@69004
    35
lp15@69004
    36
lemma intersection_of_mono:
lp15@69004
    37
   "\<lbrakk>(P intersection_of Q) S; \<And>x. Q x \<Longrightarrow> Q' x\<rbrakk> \<Longrightarrow> (P intersection_of Q') S"
lp15@69004
    38
  by (auto simp: intersection_of_def)
lp15@69004
    39
lp15@69004
    40
lemma all_union_of:
lp15@69004
    41
     "(\<forall>S. (P union_of Q) S \<longrightarrow> R S) \<longleftrightarrow> (\<forall>T. P T \<and> T \<subseteq> Collect Q \<longrightarrow> R(\<Union>T))"
lp15@69004
    42
  by (auto simp: union_of_def)
lp15@69004
    43
lp15@69004
    44
lemma all_intersection_of:
lp15@69004
    45
     "(\<forall>S. (P intersection_of Q) S \<longrightarrow> R S) \<longleftrightarrow> (\<forall>T. P T \<and> T \<subseteq> Collect Q \<longrightarrow> R(\<Inter>T))"
lp15@69004
    46
  by (auto simp: intersection_of_def)
lp15@69004
    47
lp15@69004
    48
lemma union_of_empty:
lp15@69004
    49
     "P {} \<Longrightarrow> (P union_of Q) {}"
lp15@69004
    50
  by (auto simp: union_of_def)
lp15@69004
    51
lp15@69004
    52
lemma intersection_of_empty:
lp15@69004
    53
     "P {} \<Longrightarrow> (P intersection_of Q) UNIV"
lp15@69004
    54
  by (auto simp: intersection_of_def)
lp15@69004
    55
lp15@69004
    56
text\<open> The arbitrary and finite cases\<close>
lp15@69004
    57
lp15@69004
    58
lemma arbitrary_union_of_alt:
lp15@69004
    59
   "(arbitrary union_of Q) S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>U. Q U \<and> x \<in> U \<and> U \<subseteq> S)"
lp15@69004
    60
 (is "?lhs = ?rhs")
lp15@69004
    61
proof
lp15@69004
    62
  assume ?lhs
lp15@69004
    63
  then show ?rhs
lp15@69004
    64
    by (force simp: union_of_def arbitrary_def)
lp15@69004
    65
next
lp15@69004
    66
  assume ?rhs
lp15@69004
    67
  then have "{U. Q U \<and> U \<subseteq> S} \<subseteq> Collect Q" "\<Union>{U. Q U \<and> U \<subseteq> S} = S"
lp15@69004
    68
    by auto
lp15@69004
    69
  then show ?lhs
lp15@69004
    70
    unfolding union_of_def arbitrary_def by blast
lp15@69004
    71
qed
lp15@69004
    72
lp15@69004
    73
lemma arbitrary_union_of_empty [simp]: "(arbitrary union_of P) {}"
lp15@69004
    74
  by (force simp: union_of_def arbitrary_def)
lp15@69004
    75
lp15@69004
    76
lemma arbitrary_intersection_of_empty [simp]:
lp15@69004
    77
  "(arbitrary intersection_of P) UNIV"
lp15@69004
    78
  by (force simp: intersection_of_def arbitrary_def)
lp15@69004
    79
lp15@69004
    80
lemma arbitrary_union_of_inc:
lp15@69004
    81
  "P S \<Longrightarrow> (arbitrary union_of P) S"
lp15@69004
    82
  by (force simp: union_of_inc arbitrary_def)
lp15@69004
    83
lp15@69004
    84
lemma arbitrary_intersection_of_inc:
lp15@69004
    85
  "P S \<Longrightarrow> (arbitrary intersection_of P) S"
lp15@69004
    86
  by (force simp: intersection_of_inc arbitrary_def)
lp15@69004
    87
lp15@69004
    88
lemma arbitrary_union_of_complement:
lp15@69004
    89
   "(arbitrary union_of P) S \<longleftrightarrow> (arbitrary intersection_of (\<lambda>S. P(- S))) (- S)"  (is "?lhs = ?rhs")
lp15@69004
    90
proof
lp15@69004
    91
  assume ?lhs
lp15@69004
    92
  then obtain \<U> where "\<U> \<subseteq> Collect P" "S = \<Union>\<U>"
lp15@69004
    93
    by (auto simp: union_of_def arbitrary_def)
lp15@69004
    94
  then show ?rhs
lp15@69004
    95
    unfolding intersection_of_def arbitrary_def
lp15@69004
    96
    by (rule_tac x="uminus ` \<U>" in exI) auto
lp15@69004
    97
next
lp15@69004
    98
  assume ?rhs
lp15@69004
    99
  then obtain \<U> where "\<U> \<subseteq> {S. P (- S)}" "\<Inter>\<U> = - S"
lp15@69004
   100
    by (auto simp: union_of_def intersection_of_def arbitrary_def)
lp15@69004
   101
  then show ?lhs
lp15@69004
   102
    unfolding union_of_def arbitrary_def
lp15@69004
   103
    by (rule_tac x="uminus ` \<U>" in exI) auto
lp15@69004
   104
qed
lp15@69004
   105
lp15@69004
   106
lemma arbitrary_intersection_of_complement:
lp15@69004
   107
   "(arbitrary intersection_of P) S \<longleftrightarrow> (arbitrary union_of (\<lambda>S. P(- S))) (- S)"
lp15@69004
   108
  by (simp add: arbitrary_union_of_complement)
lp15@69004
   109
lp15@69004
   110
lemma arbitrary_union_of_idempot [simp]:
lp15@69004
   111
  "arbitrary union_of arbitrary union_of P = arbitrary union_of P"
lp15@69004
   112
proof -
lp15@69004
   113
  have 1: "\<exists>\<U>'\<subseteq>Collect P. \<Union>\<U>' = \<Union>\<U>" if "\<U> \<subseteq> {S. \<exists>\<V>\<subseteq>Collect P. \<Union>\<V> = S}" for \<U>
lp15@69004
   114
  proof -
lp15@69004
   115
    let ?\<W> = "{V. \<exists>\<V>. \<V>\<subseteq>Collect P \<and> V \<in> \<V> \<and> (\<exists>S \<in> \<U>. \<Union>\<V> = S)}"
lp15@69004
   116
    have *: "\<And>x U. \<lbrakk>x \<in> U; U \<in> \<U>\<rbrakk> \<Longrightarrow> x \<in> \<Union>?\<W>"
lp15@69004
   117
      using that
lp15@69004
   118
      apply simp
lp15@69004
   119
      apply (drule subsetD, assumption, auto)
lp15@69004
   120
      done
lp15@69004
   121
    show ?thesis
lp15@69004
   122
    apply (rule_tac x="{V. \<exists>\<V>. \<V>\<subseteq>Collect P \<and> V \<in> \<V> \<and> (\<exists>S \<in> \<U>. \<Union>\<V> = S)}" in exI)
lp15@69004
   123
      using that by (blast intro: *)
lp15@69004
   124
  qed
lp15@69004
   125
  have 2: "\<exists>\<U>'\<subseteq>{S. \<exists>\<U>\<subseteq>Collect P. \<Union>\<U> = S}. \<Union>\<U>' = \<Union>\<U>" if "\<U> \<subseteq> Collect P" for \<U>
lp15@69004
   126
    by (metis (mono_tags, lifting) union_of_def arbitrary_union_of_inc that)
lp15@69004
   127
  show ?thesis
lp15@69004
   128
    unfolding union_of_def arbitrary_def by (force simp: 1 2)
lp15@69004
   129
qed
lp15@69004
   130
lp15@69004
   131
lemma arbitrary_intersection_of_idempot:
lp15@69004
   132
   "arbitrary intersection_of arbitrary intersection_of P = arbitrary intersection_of P" (is "?lhs = ?rhs")
lp15@69004
   133
proof -
lp15@69004
   134
  have "- ?lhs = - ?rhs"
lp15@69004
   135
    unfolding arbitrary_intersection_of_complement by simp
lp15@69004
   136
  then show ?thesis
lp15@69004
   137
    by simp
lp15@69004
   138
qed
lp15@69004
   139
lp15@69004
   140
lemma arbitrary_union_of_Union:
lp15@69004
   141
   "(\<And>S. S \<in> \<U> \<Longrightarrow> (arbitrary union_of P) S) \<Longrightarrow> (arbitrary union_of P) (\<Union>\<U>)"
lp15@69004
   142
  by (metis union_of_def arbitrary_def arbitrary_union_of_idempot mem_Collect_eq subsetI)
lp15@69004
   143
lp15@69004
   144
lemma arbitrary_union_of_Un:
lp15@69004
   145
   "\<lbrakk>(arbitrary union_of P) S; (arbitrary union_of P) T\<rbrakk>
lp15@69004
   146
           \<Longrightarrow> (arbitrary union_of P) (S \<union> T)"
lp15@69004
   147
  using arbitrary_union_of_Union [of "{S,T}"] by auto
lp15@69004
   148
lp15@69004
   149
lemma arbitrary_intersection_of_Inter:
lp15@69004
   150
   "(\<And>S. S \<in> \<U> \<Longrightarrow> (arbitrary intersection_of P) S) \<Longrightarrow> (arbitrary intersection_of P) (\<Inter>\<U>)"
lp15@69004
   151
  by (metis intersection_of_def arbitrary_def arbitrary_intersection_of_idempot mem_Collect_eq subsetI)
lp15@69004
   152
lp15@69004
   153
lemma arbitrary_intersection_of_Int:
lp15@69004
   154
   "\<lbrakk>(arbitrary intersection_of P) S; (arbitrary intersection_of P) T\<rbrakk>
lp15@69004
   155
           \<Longrightarrow> (arbitrary intersection_of P) (S \<inter> T)"
lp15@69004
   156
  using arbitrary_intersection_of_Inter [of "{S,T}"] by auto
lp15@69004
   157
lp15@69004
   158
lemma arbitrary_union_of_Int_eq:
lp15@69004
   159
  "(\<forall>S T. (arbitrary union_of P) S \<and> (arbitrary union_of P) T
lp15@69004
   160
               \<longrightarrow> (arbitrary union_of P) (S \<inter> T))
lp15@69004
   161
   \<longleftrightarrow> (\<forall>S T. P S \<and> P T \<longrightarrow> (arbitrary union_of P) (S \<inter> T))"  (is "?lhs = ?rhs")
lp15@69004
   162
proof
lp15@69004
   163
  assume ?lhs
lp15@69004
   164
  then show ?rhs
lp15@69004
   165
    by (simp add: arbitrary_union_of_inc)
lp15@69004
   166
next
lp15@69004
   167
  assume R: ?rhs
lp15@69004
   168
  show ?lhs
lp15@69004
   169
  proof clarify
lp15@69004
   170
    fix S :: "'a set" and T :: "'a set"
lp15@69004
   171
    assume "(arbitrary union_of P) S" and "(arbitrary union_of P) T"
lp15@69004
   172
    then obtain \<U> \<V> where *: "\<U> \<subseteq> Collect P" "\<Union>\<U> = S" "\<V> \<subseteq> Collect P" "\<Union>\<V> = T"
lp15@69004
   173
      by (auto simp: union_of_def)
lp15@69004
   174
    then have "(arbitrary union_of P) (\<Union>C\<in>\<U>. \<Union>D\<in>\<V>. C \<inter> D)"
lp15@69004
   175
     using R by (blast intro: arbitrary_union_of_Union)
lp15@69004
   176
   then show "(arbitrary union_of P) (S \<inter> T)"
lp15@69004
   177
     by (simp add: Int_UN_distrib2 *)
lp15@69004
   178
 qed
lp15@69004
   179
qed
lp15@69004
   180
lp15@69004
   181
lemma arbitrary_intersection_of_Un_eq:
lp15@69004
   182
   "(\<forall>S T. (arbitrary intersection_of P) S \<and> (arbitrary intersection_of P) T
lp15@69004
   183
               \<longrightarrow> (arbitrary intersection_of P) (S \<union> T)) \<longleftrightarrow>
lp15@69004
   184
        (\<forall>S T. P S \<and> P T \<longrightarrow> (arbitrary intersection_of P) (S \<union> T))"
lp15@69004
   185
  apply (simp add: arbitrary_intersection_of_complement)
lp15@69004
   186
  using arbitrary_union_of_Int_eq [of "\<lambda>S. P (- S)"]
lp15@69004
   187
  by (metis (no_types, lifting) arbitrary_def double_compl union_of_inc)
lp15@69004
   188
lp15@69004
   189
lemma finite_union_of_empty [simp]: "(finite union_of P) {}"
lp15@69004
   190
  by (simp add: union_of_empty)
lp15@69004
   191
lp15@69004
   192
lemma finite_intersection_of_empty [simp]: "(finite intersection_of P) UNIV"
lp15@69004
   193
  by (simp add: intersection_of_empty)
lp15@69004
   194
lp15@69004
   195
lemma finite_union_of_inc:
lp15@69004
   196
   "P S \<Longrightarrow> (finite union_of P) S"
lp15@69004
   197
  by (simp add: union_of_inc)
lp15@69004
   198
lp15@69004
   199
lemma finite_intersection_of_inc:
lp15@69004
   200
   "P S \<Longrightarrow> (finite intersection_of P) S"
lp15@69004
   201
  by (simp add: intersection_of_inc)
lp15@69004
   202
lp15@69004
   203
lemma finite_union_of_complement:
lp15@69004
   204
  "(finite union_of P) S \<longleftrightarrow> (finite intersection_of (\<lambda>S. P(- S))) (- S)"
lp15@69004
   205
  unfolding union_of_def intersection_of_def
lp15@69004
   206
  apply safe
lp15@69004
   207
   apply (rule_tac x="uminus ` \<U>" in exI, fastforce)+
lp15@69004
   208
  done
lp15@69004
   209
lp15@69004
   210
lemma finite_intersection_of_complement:
lp15@69004
   211
   "(finite intersection_of P) S \<longleftrightarrow> (finite union_of (\<lambda>S. P(- S))) (- S)"
lp15@69004
   212
  by (simp add: finite_union_of_complement)
lp15@69004
   213
lp15@69004
   214
lemma finite_union_of_idempot [simp]:
lp15@69004
   215
  "finite union_of finite union_of P = finite union_of P"
lp15@69004
   216
proof -
lp15@69004
   217
  have "(finite union_of P) S" if S: "(finite union_of finite union_of P) S" for S
lp15@69004
   218
  proof -
lp15@69004
   219
    obtain \<U> where "finite \<U>" "S = \<Union>\<U>" and \<U>: "\<forall>U\<in>\<U>. \<exists>\<U>. finite \<U> \<and> (\<U> \<subseteq> Collect P) \<and> \<Union>\<U> = U"
lp15@69004
   220
      using S unfolding union_of_def by (auto simp: subset_eq)
lp15@69004
   221
    then obtain f where "\<forall>U\<in>\<U>. finite (f U) \<and> (f U \<subseteq> Collect P) \<and> \<Union>(f U) = U"
lp15@69004
   222
      by metis
lp15@69004
   223
    then show ?thesis
lp15@69004
   224
      unfolding union_of_def \<open>S = \<Union>\<U>\<close>
lp15@69004
   225
      by (rule_tac x = "snd ` Sigma \<U> f" in exI) (fastforce simp: \<open>finite \<U>\<close>)
lp15@69004
   226
  qed
lp15@69004
   227
  moreover
lp15@69004
   228
  have "(finite union_of finite union_of P) S" if "(finite union_of P) S" for S
lp15@69004
   229
    by (simp add: finite_union_of_inc that)
lp15@69004
   230
  ultimately show ?thesis
lp15@69004
   231
    by force
lp15@69004
   232
qed
lp15@69004
   233
lp15@69004
   234
lemma finite_intersection_of_idempot [simp]:
lp15@69004
   235
   "finite intersection_of finite intersection_of P = finite intersection_of P"
lp15@69004
   236
  by (force simp: finite_intersection_of_complement)
lp15@69004
   237
lp15@69004
   238
lemma finite_union_of_Union:
lp15@69004
   239
   "\<lbrakk>finite \<U>; \<And>S. S \<in> \<U> \<Longrightarrow> (finite union_of P) S\<rbrakk> \<Longrightarrow> (finite union_of P) (\<Union>\<U>)"
lp15@69004
   240
  using finite_union_of_idempot [of P]
lp15@69004
   241
  by (metis mem_Collect_eq subsetI union_of_def)
lp15@69004
   242
lp15@69004
   243
lemma finite_union_of_Un:
lp15@69004
   244
   "\<lbrakk>(finite union_of P) S; (finite union_of P) T\<rbrakk> \<Longrightarrow> (finite union_of P) (S \<union> T)"
lp15@69004
   245
  by (auto simp: union_of_def)
lp15@69004
   246
lp15@69004
   247
lemma finite_intersection_of_Inter:
lp15@69004
   248
   "\<lbrakk>finite \<U>; \<And>S. S \<in> \<U> \<Longrightarrow> (finite intersection_of P) S\<rbrakk> \<Longrightarrow> (finite intersection_of P) (\<Inter>\<U>)"
lp15@69004
   249
  using finite_intersection_of_idempot [of P]
lp15@69004
   250
  by (metis intersection_of_def mem_Collect_eq subsetI)
lp15@69004
   251
lp15@69004
   252
lemma finite_intersection_of_Int:
lp15@69004
   253
   "\<lbrakk>(finite intersection_of P) S; (finite intersection_of P) T\<rbrakk>
lp15@69004
   254
           \<Longrightarrow> (finite intersection_of P) (S \<inter> T)"
lp15@69004
   255
  by (auto simp: intersection_of_def)
lp15@69004
   256
lp15@69004
   257
lemma finite_union_of_Int_eq:
lp15@69004
   258
   "(\<forall>S T. (finite union_of P) S \<and> (finite union_of P) T \<longrightarrow> (finite union_of P) (S \<inter> T))
lp15@69004
   259
    \<longleftrightarrow> (\<forall>S T. P S \<and> P T \<longrightarrow> (finite union_of P) (S \<inter> T))"
lp15@69004
   260
(is "?lhs = ?rhs")
lp15@69004
   261
proof
lp15@69004
   262
  assume ?lhs
lp15@69004
   263
  then show ?rhs
lp15@69004
   264
    by (simp add: finite_union_of_inc)
lp15@69004
   265
next
lp15@69004
   266
  assume R: ?rhs
lp15@69004
   267
  show ?lhs
lp15@69004
   268
  proof clarify
lp15@69004
   269
    fix S :: "'a set" and T :: "'a set"
lp15@69004
   270
    assume "(finite union_of P) S" and "(finite union_of P) T"
lp15@69004
   271
    then obtain \<U> \<V> where *: "\<U> \<subseteq> Collect P" "\<Union>\<U> = S" "finite \<U>" "\<V> \<subseteq> Collect P" "\<Union>\<V> = T" "finite \<V>"
lp15@69004
   272
      by (auto simp: union_of_def)
lp15@69004
   273
    then have "(finite union_of P) (\<Union>C\<in>\<U>. \<Union>D\<in>\<V>. C \<inter> D)"
lp15@69004
   274
      using R
lp15@69004
   275
      by (blast intro: finite_union_of_Union)
lp15@69004
   276
   then show "(finite union_of P) (S \<inter> T)"
lp15@69004
   277
     by (simp add: Int_UN_distrib2 *)
lp15@69004
   278
 qed
lp15@69004
   279
qed
lp15@69004
   280
lp15@69004
   281
lemma finite_intersection_of_Un_eq:
lp15@69004
   282
   "(\<forall>S T. (finite intersection_of P) S \<and>
lp15@69004
   283
               (finite intersection_of P) T
lp15@69004
   284
               \<longrightarrow> (finite intersection_of P) (S \<union> T)) \<longleftrightarrow>
lp15@69004
   285
        (\<forall>S T. P S \<and> P T \<longrightarrow> (finite intersection_of P) (S \<union> T))"
lp15@69004
   286
  apply (simp add: finite_intersection_of_complement)
lp15@69004
   287
  using finite_union_of_Int_eq [of "\<lambda>S. P (- S)"]
lp15@69004
   288
  by (metis (no_types, lifting) double_compl)
lp15@69004
   289
lp15@69004
   290
lp15@69004
   291
abbreviation finite' :: "'a set \<Rightarrow> bool"
lp15@69004
   292
  where "finite' A \<equiv> finite A \<and> A \<noteq> {}"
lp15@69004
   293
lp15@69004
   294
lemma finite'_intersection_of_Int:
lp15@69004
   295
   "\<lbrakk>(finite' intersection_of P) S; (finite' intersection_of P) T\<rbrakk>
lp15@69004
   296
           \<Longrightarrow> (finite' intersection_of P) (S \<inter> T)"
lp15@69004
   297
  by (auto simp: intersection_of_def)
lp15@69004
   298
lp15@69004
   299
lemma finite'_intersection_of_inc:
lp15@69004
   300
   "P S \<Longrightarrow> (finite' intersection_of P) S"
lp15@69004
   301
  by (simp add: intersection_of_inc)
lp15@69004
   302
lp15@69004
   303
lp15@69004
   304
subsection \<open>The ``Relative to'' operator\<close>
lp15@69004
   305
lp15@69004
   306
text\<open>A somewhat cheap but handy way of getting localized forms of various topological concepts
lp15@69004
   307
(open, closed, borel, fsigma, gdelta etc.)\<close>
lp15@69004
   308
lp15@69004
   309
definition relative_to :: "['a set \<Rightarrow> bool, 'a set, 'a set] \<Rightarrow> bool" (infixl "relative'_to" 55)
lp15@69004
   310
  where "P relative_to S \<equiv> \<lambda>T. \<exists>U. P U \<and> S \<inter> U = T"
lp15@69004
   311
lp15@69004
   312
lemma relative_to_UNIV [simp]: "(P relative_to UNIV) S \<longleftrightarrow> P S"
lp15@69004
   313
  by (simp add: relative_to_def)
lp15@69004
   314
lp15@69004
   315
lemma relative_to_imp_subset:
lp15@69004
   316
   "(P relative_to S) T \<Longrightarrow> T \<subseteq> S"
lp15@69004
   317
  by (auto simp: relative_to_def)
lp15@69004
   318
lp15@69004
   319
lemma all_relative_to: "(\<forall>S. (P relative_to U) S \<longrightarrow> Q S) \<longleftrightarrow> (\<forall>S. P S \<longrightarrow> Q(U \<inter> S))"
lp15@69004
   320
  by (auto simp: relative_to_def)
lp15@69004
   321
lp15@69004
   322
lemma relative_to_inc:
lp15@69004
   323
   "P S \<Longrightarrow> (P relative_to U) (U \<inter> S)"
lp15@69004
   324
  by (auto simp: relative_to_def)
lp15@69004
   325
lp15@69004
   326
lemma relative_to_relative_to [simp]:
lp15@69004
   327
   "P relative_to S relative_to T = P relative_to (S \<inter> T)"
lp15@69004
   328
  unfolding relative_to_def
lp15@69004
   329
  by auto
lp15@69004
   330
lp15@69004
   331
lemma relative_to_compl:
lp15@69004
   332
   "S \<subseteq> U \<Longrightarrow> ((P relative_to U) (U - S) \<longleftrightarrow> ((\<lambda>c. P(- c)) relative_to U) S)"
lp15@69004
   333
  unfolding relative_to_def
lp15@69004
   334
  by (metis Diff_Diff_Int Diff_eq double_compl inf.absorb_iff2)
lp15@69004
   335
lp15@69004
   336
lemma relative_to_subset:
lp15@69004
   337
   "S \<subseteq> T \<and> P S \<Longrightarrow> (P relative_to T) S"
lp15@69004
   338
  unfolding relative_to_def by auto
lp15@69004
   339
lp15@69004
   340
lemma relative_to_subset_trans:
lp15@69004
   341
   "(P relative_to U) S \<and> S \<subseteq> T \<and> T \<subseteq> U \<Longrightarrow> (P relative_to T) S"
lp15@69004
   342
  unfolding relative_to_def by auto
lp15@69004
   343
lp15@69004
   344
lemma relative_to_mono:
lp15@69004
   345
   "\<lbrakk>(P relative_to U) S; \<And>S. P S \<Longrightarrow> Q S\<rbrakk> \<Longrightarrow> (Q relative_to U) S"
lp15@69004
   346
  unfolding relative_to_def by auto
lp15@69004
   347
lp15@69004
   348
lemma relative_to_subset_inc: "\<lbrakk>S \<subseteq> U; P S\<rbrakk> \<Longrightarrow> (P relative_to U) S"
lp15@69004
   349
  unfolding relative_to_def by auto
lp15@69004
   350
lp15@69004
   351
lemma relative_to_Int:
lp15@69004
   352
   "\<lbrakk>(P relative_to S) C; (P relative_to S) D; \<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P(X \<inter> Y)\<rbrakk>
lp15@69004
   353
         \<Longrightarrow>  (P relative_to S) (C \<inter> D)"
lp15@69004
   354
  unfolding relative_to_def by auto
lp15@69004
   355
lp15@69004
   356
lemma relative_to_Un:
lp15@69004
   357
   "\<lbrakk>(P relative_to S) C; (P relative_to S) D; \<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P(X \<union> Y)\<rbrakk>
lp15@69004
   358
         \<Longrightarrow>  (P relative_to S) (C \<union> D)"
lp15@69004
   359
  unfolding relative_to_def by auto
lp15@69004
   360
lp15@69004
   361
lemma arbitrary_union_of_relative_to:
lp15@69004
   362
  "((arbitrary union_of P) relative_to U) = (arbitrary union_of (P relative_to U))" (is "?lhs = ?rhs")
lp15@69004
   363
proof -
lp15@69004
   364
  have "?rhs S" if L: "?lhs S" for S
lp15@69004
   365
  proof -
lp15@69004
   366
    obtain \<U> where "S = U \<inter> \<Union>\<U>" "\<U> \<subseteq> Collect P"
lp15@69004
   367
      using L unfolding relative_to_def union_of_def by auto
lp15@69004
   368
    then show ?thesis
lp15@69004
   369
      unfolding relative_to_def union_of_def arbitrary_def
lp15@69004
   370
      by (rule_tac x="(\<lambda>X. U \<inter> X) ` \<U>" in exI) auto
lp15@69004
   371
  qed
lp15@69004
   372
  moreover have "?lhs S" if R: "?rhs S" for S
lp15@69004
   373
  proof -
lp15@69004
   374
    obtain \<U> where "S = \<Union>\<U>" "\<forall>T\<in>\<U>. \<exists>V. P V \<and> U \<inter> V = T"
lp15@69004
   375
      using R unfolding relative_to_def union_of_def by auto
lp15@69004
   376
    then obtain f where f: "\<And>T. T \<in> \<U> \<Longrightarrow> P (f T)" "\<And>T. T \<in> \<U> \<Longrightarrow> U \<inter> (f T) = T"
lp15@69004
   377
      by metis
lp15@69004
   378
    then have "\<exists>\<U>'\<subseteq>Collect P. \<Union>\<U>' = UNION \<U> f"
lp15@69004
   379
      by (metis image_subset_iff mem_Collect_eq)
lp15@69004
   380
    moreover have eq: "U \<inter> UNION \<U> f = \<Union>\<U>"
lp15@69004
   381
      using f by auto
lp15@69004
   382
    ultimately show ?thesis
lp15@69004
   383
      unfolding relative_to_def union_of_def arbitrary_def \<open>S = \<Union>\<U>\<close>
lp15@69004
   384
      by metis
lp15@69004
   385
  qed
lp15@69004
   386
  ultimately show ?thesis
lp15@69004
   387
    by blast
lp15@69004
   388
qed
lp15@69004
   389
lp15@69004
   390
lemma finite_union_of_relative_to:
lp15@69004
   391
  "((finite union_of P) relative_to U) = (finite union_of (P relative_to U))" (is "?lhs = ?rhs")
lp15@69004
   392
proof -
lp15@69004
   393
  have "?rhs S" if L: "?lhs S" for S
lp15@69004
   394
  proof -
lp15@69004
   395
    obtain \<U> where "S = U \<inter> \<Union>\<U>" "\<U> \<subseteq> Collect P" "finite \<U>"
lp15@69004
   396
      using L unfolding relative_to_def union_of_def by auto
lp15@69004
   397
    then show ?thesis
lp15@69004
   398
      unfolding relative_to_def union_of_def
lp15@69004
   399
      by (rule_tac x="(\<lambda>X. U \<inter> X) ` \<U>" in exI) auto
lp15@69004
   400
  qed
lp15@69004
   401
  moreover have "?lhs S" if R: "?rhs S" for S
lp15@69004
   402
  proof -
lp15@69004
   403
    obtain \<U> where "S = \<Union>\<U>" "\<forall>T\<in>\<U>. \<exists>V. P V \<and> U \<inter> V = T" "finite \<U>"
lp15@69004
   404
      using R unfolding relative_to_def union_of_def by auto
lp15@69004
   405
    then obtain f where f: "\<And>T. T \<in> \<U> \<Longrightarrow> P (f T)" "\<And>T. T \<in> \<U> \<Longrightarrow> U \<inter> (f T) = T"
lp15@69004
   406
      by metis
lp15@69004
   407
    then have "\<exists>\<U>'\<subseteq>Collect P. \<Union>\<U>' = UNION \<U> f"
lp15@69004
   408
      by (metis image_subset_iff mem_Collect_eq)
lp15@69004
   409
    moreover have eq: "U \<inter> UNION \<U> f = \<Union>\<U>"
lp15@69004
   410
      using f by auto
lp15@69004
   411
    ultimately show ?thesis
lp15@69004
   412
      using \<open>finite \<U>\<close> f
lp15@69004
   413
      unfolding relative_to_def union_of_def \<open>S = \<Union>\<U>\<close>
lp15@69004
   414
      by (rule_tac x="UNION \<U> f" in exI) (metis finite_imageI image_subsetI mem_Collect_eq)
lp15@69004
   415
  qed
lp15@69004
   416
  ultimately show ?thesis
lp15@69004
   417
    by blast
lp15@69004
   418
qed
lp15@69004
   419
lp15@69004
   420
lemma countable_union_of_relative_to:
lp15@69004
   421
  "((countable union_of P) relative_to U) = (countable union_of (P relative_to U))" (is "?lhs = ?rhs")
lp15@69004
   422
proof -
lp15@69004
   423
  have "?rhs S" if L: "?lhs S" for S
lp15@69004
   424
  proof -
lp15@69004
   425
    obtain \<U> where "S = U \<inter> \<Union>\<U>" "\<U> \<subseteq> Collect P" "countable \<U>"
lp15@69004
   426
      using L unfolding relative_to_def union_of_def by auto
lp15@69004
   427
    then show ?thesis
lp15@69004
   428
      unfolding relative_to_def union_of_def
lp15@69004
   429
      by (rule_tac x="(\<lambda>X. U \<inter> X) ` \<U>" in exI) auto
lp15@69004
   430
  qed
lp15@69004
   431
  moreover have "?lhs S" if R: "?rhs S" for S
lp15@69004
   432
  proof -
lp15@69004
   433
    obtain \<U> where "S = \<Union>\<U>" "\<forall>T\<in>\<U>. \<exists>V. P V \<and> U \<inter> V = T" "countable \<U>"
lp15@69004
   434
      using R unfolding relative_to_def union_of_def by auto
lp15@69004
   435
    then obtain f where f: "\<And>T. T \<in> \<U> \<Longrightarrow> P (f T)" "\<And>T. T \<in> \<U> \<Longrightarrow> U \<inter> (f T) = T"
lp15@69004
   436
      by metis
lp15@69004
   437
    then have "\<exists>\<U>'\<subseteq>Collect P. \<Union>\<U>' = UNION \<U> f"
lp15@69004
   438
      by (metis image_subset_iff mem_Collect_eq)
lp15@69004
   439
    moreover have eq: "U \<inter> UNION \<U> f = \<Union>\<U>"
lp15@69004
   440
      using f by auto
lp15@69004
   441
    ultimately show ?thesis
lp15@69004
   442
      using \<open>countable \<U>\<close> f
lp15@69004
   443
      unfolding relative_to_def union_of_def \<open>S = \<Union>\<U>\<close>
lp15@69004
   444
      by (rule_tac x="UNION \<U> f" in exI) (metis countable_image image_subsetI mem_Collect_eq)
lp15@69004
   445
  qed
lp15@69004
   446
  ultimately show ?thesis
lp15@69004
   447
    by blast
lp15@69004
   448
qed
lp15@69004
   449
lp15@69004
   450
lp15@69004
   451
lemma arbitrary_intersection_of_relative_to:
lp15@69004
   452
  "((arbitrary intersection_of P) relative_to U) = ((arbitrary intersection_of (P relative_to U)) relative_to U)" (is "?lhs = ?rhs")
lp15@69004
   453
proof -
lp15@69004
   454
  have "?rhs S" if L: "?lhs S" for S
lp15@69004
   455
  proof -
lp15@69004
   456
    obtain \<U> where \<U>: "S = U \<inter> \<Inter>\<U>" "\<U> \<subseteq> Collect P"
lp15@69004
   457
      using L unfolding relative_to_def intersection_of_def by auto
lp15@69004
   458
    show ?thesis
lp15@69004
   459
      unfolding relative_to_def intersection_of_def arbitrary_def
lp15@69004
   460
    proof (intro exI conjI)
lp15@69004
   461
      show "U \<inter> (\<Inter>X\<in>\<U>. U \<inter> X) = S" "(\<inter>) U ` \<U> \<subseteq> {T. \<exists>Ua. P Ua \<and> U \<inter> Ua = T}"
lp15@69004
   462
        using \<U> by blast+
lp15@69004
   463
    qed auto
lp15@69004
   464
  qed
lp15@69004
   465
  moreover have "?lhs S" if R: "?rhs S" for S
lp15@69004
   466
  proof -
lp15@69004
   467
    obtain \<U> where "S = U \<inter> \<Inter>\<U>" "\<forall>T\<in>\<U>. \<exists>V. P V \<and> U \<inter> V = T"
lp15@69004
   468
      using R unfolding relative_to_def intersection_of_def  by auto
lp15@69004
   469
    then obtain f where f: "\<And>T. T \<in> \<U> \<Longrightarrow> P (f T)" "\<And>T. T \<in> \<U> \<Longrightarrow> U \<inter> (f T) = T"
lp15@69004
   470
      by metis
haftmann@69313
   471
    then have "f `  \<U> \<subseteq> Collect P"
haftmann@69313
   472
      by auto
haftmann@69313
   473
    moreover have eq: "U \<inter> \<Inter>(f ` \<U>) = U \<inter> \<Inter>\<U>"
lp15@69004
   474
      using f by auto
lp15@69004
   475
    ultimately show ?thesis
lp15@69004
   476
      unfolding relative_to_def intersection_of_def arbitrary_def \<open>S = U \<inter> \<Inter>\<U>\<close>
haftmann@69313
   477
      by auto
lp15@69004
   478
  qed
lp15@69004
   479
  ultimately show ?thesis
lp15@69004
   480
    by blast
lp15@69004
   481
qed
lp15@69004
   482
lp15@69004
   483
lemma finite_intersection_of_relative_to:
lp15@69004
   484
  "((finite intersection_of P) relative_to U) = ((finite intersection_of (P relative_to U)) relative_to U)" (is "?lhs = ?rhs")
lp15@69004
   485
proof -
lp15@69004
   486
  have "?rhs S" if L: "?lhs S" for S
lp15@69004
   487
  proof -
lp15@69004
   488
    obtain \<U> where \<U>: "S = U \<inter> \<Inter>\<U>" "\<U> \<subseteq> Collect P" "finite \<U>"
lp15@69004
   489
      using L unfolding relative_to_def intersection_of_def by auto
lp15@69004
   490
    show ?thesis
lp15@69004
   491
      unfolding relative_to_def intersection_of_def
lp15@69004
   492
    proof (intro exI conjI)
lp15@69004
   493
      show "U \<inter> (\<Inter>X\<in>\<U>. U \<inter> X) = S" "(\<inter>) U ` \<U> \<subseteq> {T. \<exists>Ua. P Ua \<and> U \<inter> Ua = T}"
lp15@69004
   494
        using \<U> by blast+
lp15@69004
   495
      show "finite ((\<inter>) U ` \<U>)"
lp15@69004
   496
        by (simp add: \<open>finite \<U>\<close>)
lp15@69004
   497
    qed auto
lp15@69004
   498
  qed
lp15@69004
   499
  moreover have "?lhs S" if R: "?rhs S" for S
lp15@69004
   500
  proof -
lp15@69004
   501
    obtain \<U> where "S = U \<inter> \<Inter>\<U>" "\<forall>T\<in>\<U>. \<exists>V. P V \<and> U \<inter> V = T" "finite \<U>"
lp15@69004
   502
      using R unfolding relative_to_def intersection_of_def  by auto
lp15@69004
   503
    then obtain f where f: "\<And>T. T \<in> \<U> \<Longrightarrow> P (f T)" "\<And>T. T \<in> \<U> \<Longrightarrow> U \<inter> (f T) = T"
lp15@69004
   504
      by metis
haftmann@69313
   505
    then have "f `  \<U> \<subseteq> Collect P"
haftmann@69313
   506
      by auto
haftmann@69313
   507
    moreover have eq: "U \<inter> \<Inter> (f ` \<U>) = U \<inter> \<Inter> \<U>"
lp15@69004
   508
      using f by auto
lp15@69004
   509
    ultimately show ?thesis
lp15@69004
   510
      unfolding relative_to_def intersection_of_def \<open>S = U \<inter> \<Inter>\<U>\<close>
haftmann@69313
   511
      using \<open>finite \<U>\<close>
haftmann@69313
   512
      by auto
lp15@69004
   513
  qed
lp15@69004
   514
  ultimately show ?thesis
lp15@69004
   515
    by blast
lp15@69004
   516
qed
lp15@69004
   517
lp15@69004
   518
lemma countable_intersection_of_relative_to:
lp15@69004
   519
  "((countable intersection_of P) relative_to U) = ((countable intersection_of (P relative_to U)) relative_to U)" (is "?lhs = ?rhs")
lp15@69004
   520
proof -
lp15@69004
   521
  have "?rhs S" if L: "?lhs S" for S
lp15@69004
   522
  proof -
lp15@69004
   523
    obtain \<U> where \<U>: "S = U \<inter> \<Inter>\<U>" "\<U> \<subseteq> Collect P" "countable \<U>"
lp15@69004
   524
      using L unfolding relative_to_def intersection_of_def by auto
lp15@69004
   525
    show ?thesis
lp15@69004
   526
      unfolding relative_to_def intersection_of_def
lp15@69004
   527
    proof (intro exI conjI)
lp15@69004
   528
      show "U \<inter> (\<Inter>X\<in>\<U>. U \<inter> X) = S" "(\<inter>) U ` \<U> \<subseteq> {T. \<exists>Ua. P Ua \<and> U \<inter> Ua = T}"
lp15@69004
   529
        using \<U> by blast+
lp15@69004
   530
      show "countable ((\<inter>) U ` \<U>)"
lp15@69004
   531
        by (simp add: \<open>countable \<U>\<close>)
lp15@69004
   532
    qed auto
lp15@69004
   533
  qed
lp15@69004
   534
  moreover have "?lhs S" if R: "?rhs S" for S
lp15@69004
   535
  proof -
lp15@69004
   536
    obtain \<U> where "S = U \<inter> \<Inter>\<U>" "\<forall>T\<in>\<U>. \<exists>V. P V \<and> U \<inter> V = T" "countable \<U>"
lp15@69004
   537
      using R unfolding relative_to_def intersection_of_def  by auto
lp15@69004
   538
    then obtain f where f: "\<And>T. T \<in> \<U> \<Longrightarrow> P (f T)" "\<And>T. T \<in> \<U> \<Longrightarrow> U \<inter> (f T) = T"
lp15@69004
   539
      by metis
haftmann@69313
   540
    then have "f `  \<U> \<subseteq> Collect P"
haftmann@69313
   541
      by auto
haftmann@69313
   542
    moreover have eq: "U \<inter> \<Inter> (f ` \<U>) = U \<inter> \<Inter> \<U>"
lp15@69004
   543
      using f by auto
lp15@69004
   544
    ultimately show ?thesis
lp15@69004
   545
      unfolding relative_to_def intersection_of_def \<open>S = U \<inter> \<Inter>\<U>\<close>
haftmann@69313
   546
      using \<open>countable \<U>\<close> countable_image
haftmann@69313
   547
      by auto
lp15@69004
   548
  qed
lp15@69004
   549
  ultimately show ?thesis
lp15@69004
   550
    by blast
lp15@69004
   551
qed
lp15@69004
   552
lp15@69004
   553
end