src/HOL/Library/Indicator_Function.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (4 months ago)
changeset 69946 494934c30f38
parent 69313 b021008c5397
child 70381 b151d1f00204
permissions -rw-r--r--
improved code equations taken over from AFP
hoelzl@37665
     1
(*  Title:      HOL/Library/Indicator_Function.thy
hoelzl@37665
     2
    Author:     Johannes Hoelzl (TU Muenchen)
hoelzl@37665
     3
*)
hoelzl@37665
     4
wenzelm@60500
     5
section \<open>Indicator Function\<close>
hoelzl@37665
     6
hoelzl@37665
     7
theory Indicator_Function
eberlm@63099
     8
imports Complex_Main Disjoint_Sets
hoelzl@37665
     9
begin
hoelzl@37665
    10
hoelzl@37665
    11
definition "indicator S x = (if x \<in> S then 1 else 0)"
hoelzl@37665
    12
lp15@67683
    13
text\<open>Type constrained version\<close>
lp15@67683
    14
abbreviation indicat_real :: "'a set \<Rightarrow> 'a \<Rightarrow> real" where "indicat_real S \<equiv> indicator S"
lp15@67683
    15
hoelzl@37665
    16
lemma indicator_simps[simp]:
hoelzl@37665
    17
  "x \<in> S \<Longrightarrow> indicator S x = 1"
hoelzl@37665
    18
  "x \<notin> S \<Longrightarrow> indicator S x = 0"
hoelzl@37665
    19
  unfolding indicator_def by auto
hoelzl@37665
    20
wenzelm@45425
    21
lemma indicator_pos_le[intro, simp]: "(0::'a::linordered_semidom) \<le> indicator S x"
hoelzl@37665
    22
  and indicator_le_1[intro, simp]: "indicator S x \<le> (1::'a::linordered_semidom)"
wenzelm@45425
    23
  unfolding indicator_def by auto
wenzelm@45425
    24
wenzelm@45425
    25
lemma indicator_abs_le_1: "\<bar>indicator S x\<bar> \<le> (1::'a::linordered_idom)"
hoelzl@37665
    26
  unfolding indicator_def by auto
hoelzl@37665
    27
wenzelm@63309
    28
lemma indicator_eq_0_iff: "indicator A x = (0::'a::zero_neq_one) \<longleftrightarrow> x \<notin> A"
hoelzl@54408
    29
  by (auto simp: indicator_def)
hoelzl@54408
    30
wenzelm@63309
    31
lemma indicator_eq_1_iff: "indicator A x = (1::'a::zero_neq_one) \<longleftrightarrow> x \<in> A"
hoelzl@54408
    32
  by (auto simp: indicator_def)
hoelzl@54408
    33
hoelzl@63958
    34
lemma indicator_UNIV [simp]: "indicator UNIV = (\<lambda>x. 1)"
hoelzl@63958
    35
  by auto
hoelzl@63958
    36
eberlm@63099
    37
lemma indicator_leI:
wenzelm@63309
    38
  "(x \<in> A \<Longrightarrow> y \<in> B) \<Longrightarrow> (indicator A x :: 'a::linordered_nonzero_semiring) \<le> indicator B y"
eberlm@63099
    39
  by (auto simp: indicator_def)
eberlm@63099
    40
hoelzl@57446
    41
lemma split_indicator: "P (indicator S x) \<longleftrightarrow> ((x \<in> S \<longrightarrow> P 1) \<and> (x \<notin> S \<longrightarrow> P 0))"
hoelzl@57446
    42
  unfolding indicator_def by auto
hoelzl@57446
    43
hoelzl@57446
    44
lemma split_indicator_asm: "P (indicator S x) \<longleftrightarrow> (\<not> (x \<in> S \<and> \<not> P 1 \<or> x \<notin> S \<and> \<not> P 0))"
hoelzl@37665
    45
  unfolding indicator_def by auto
hoelzl@37665
    46
wenzelm@45425
    47
lemma indicator_inter_arith: "indicator (A \<inter> B) x = indicator A x * (indicator B x::'a::semiring_1)"
wenzelm@45425
    48
  unfolding indicator_def by (auto simp: min_def max_def)
wenzelm@45425
    49
wenzelm@63309
    50
lemma indicator_union_arith:
wenzelm@63309
    51
  "indicator (A \<union> B) x = indicator A x + indicator B x - indicator A x * (indicator B x :: 'a::ring_1)"
wenzelm@45425
    52
  unfolding indicator_def by (auto simp: min_def max_def)
wenzelm@45425
    53
wenzelm@45425
    54
lemma indicator_inter_min: "indicator (A \<inter> B) x = min (indicator A x) (indicator B x::'a::linordered_semidom)"
hoelzl@37665
    55
  and indicator_union_max: "indicator (A \<union> B) x = max (indicator A x) (indicator B x::'a::linordered_semidom)"
wenzelm@45425
    56
  unfolding indicator_def by (auto simp: min_def max_def)
wenzelm@45425
    57
wenzelm@63309
    58
lemma indicator_disj_union:
wenzelm@63309
    59
  "A \<inter> B = {} \<Longrightarrow> indicator (A \<union> B) x = (indicator A x + indicator B x :: 'a::linordered_semidom)"
hoelzl@57446
    60
  by (auto split: split_indicator)
hoelzl@57446
    61
wenzelm@63309
    62
lemma indicator_compl: "indicator (- A) x = 1 - (indicator A x :: 'a::ring_1)"
wenzelm@63309
    63
  and indicator_diff: "indicator (A - B) x = indicator A x * (1 - indicator B x ::'a::ring_1)"
hoelzl@37665
    64
  unfolding indicator_def by (auto simp: min_def max_def)
hoelzl@37665
    65
wenzelm@63309
    66
lemma indicator_times:
wenzelm@63309
    67
  "indicator (A \<times> B) x = indicator A (fst x) * (indicator B (snd x) :: 'a::semiring_1)"
hoelzl@37665
    68
  unfolding indicator_def by (cases x) auto
hoelzl@37665
    69
wenzelm@63309
    70
lemma indicator_sum:
wenzelm@63309
    71
  "indicator (A <+> B) x = (case x of Inl x \<Rightarrow> indicator A x | Inr x \<Rightarrow> indicator B x)"
hoelzl@37665
    72
  unfolding indicator_def by (cases x) auto
hoelzl@37665
    73
hoelzl@59002
    74
lemma indicator_image: "inj f \<Longrightarrow> indicator (f ` X) (f x) = (indicator X x::_::zero_neq_one)"
wenzelm@64966
    75
  by (auto simp: indicator_def inj_def)
hoelzl@59002
    76
Andreas@61633
    77
lemma indicator_vimage: "indicator (f -` A) x = indicator A (f x)"
wenzelm@63309
    78
  by (auto split: split_indicator)
Andreas@61633
    79
wenzelm@63309
    80
lemma  (* FIXME unnamed!? *)
wenzelm@63309
    81
  fixes f :: "'a \<Rightarrow> 'b::semiring_1"
wenzelm@63309
    82
  assumes "finite A"
nipkow@64267
    83
  shows sum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator B x) = (\<Sum>x \<in> A \<inter> B. f x)"
nipkow@64267
    84
    and sum_indicator_mult[simp]: "(\<Sum>x \<in> A. indicator B x * f x) = (\<Sum>x \<in> A \<inter> B. f x)"
hoelzl@37665
    85
  unfolding indicator_def
nipkow@64267
    86
  using assms by (auto intro!: sum.mono_neutral_cong_right split: if_split_asm)
hoelzl@37665
    87
nipkow@64267
    88
lemma sum_indicator_eq_card:
hoelzl@37665
    89
  assumes "finite A"
wenzelm@61954
    90
  shows "(\<Sum>x \<in> A. indicator B x) = card (A Int B)"
nipkow@64267
    91
  using sum_mult_indicator [OF assms, of "\<lambda>x. 1::nat"]
nipkow@64267
    92
  unfolding card_eq_sum by simp
hoelzl@37665
    93
nipkow@64267
    94
lemma sum_indicator_scaleR[simp]:
hoelzl@56993
    95
  "finite A \<Longrightarrow>
wenzelm@63309
    96
    (\<Sum>x \<in> A. indicator (B x) (g x) *\<^sub>R f x) = (\<Sum>x \<in> {x\<in>A. g x \<in> B x}. f x :: 'a::real_vector)"
nipkow@64267
    97
  by (auto intro!: sum.mono_neutral_cong_right split: if_split_asm simp: indicator_def)
hoelzl@56993
    98
hoelzl@57446
    99
lemma LIMSEQ_indicator_incseq:
hoelzl@57446
   100
  assumes "incseq A"
wenzelm@63309
   101
  shows "(\<lambda>i. indicator (A i) x :: 'a::{topological_space,one,zero}) \<longlonglongrightarrow> indicator (\<Union>i. A i) x"
wenzelm@63309
   102
proof (cases "\<exists>i. x \<in> A i")
wenzelm@63309
   103
  case True
hoelzl@57446
   104
  then obtain i where "x \<in> A i"
hoelzl@57446
   105
    by auto
wenzelm@63649
   106
  then have *:
hoelzl@57446
   107
    "\<And>n. (indicator (A (n + i)) x :: 'a) = 1"
wenzelm@60585
   108
    "(indicator (\<Union>i. A i) x :: 'a) = 1"
wenzelm@60500
   109
    using incseqD[OF \<open>incseq A\<close>, of i "n + i" for n] \<open>x \<in> A i\<close> by (auto simp: indicator_def)
wenzelm@63649
   110
  show ?thesis
wenzelm@63649
   111
    by (rule LIMSEQ_offset[of _ i]) (use * in simp)
wenzelm@63309
   112
next
wenzelm@63309
   113
  case False
wenzelm@63309
   114
  then show ?thesis by (simp add: indicator_def)
wenzelm@63309
   115
qed
hoelzl@57446
   116
hoelzl@57446
   117
lemma LIMSEQ_indicator_UN:
wenzelm@63309
   118
  "(\<lambda>k. indicator (\<Union>i<k. A i) x :: 'a::{topological_space,one,zero}) \<longlonglongrightarrow> indicator (\<Union>i. A i) x"
hoelzl@57446
   119
proof -
wenzelm@61969
   120
  have "(\<lambda>k. indicator (\<Union>i<k. A i) x::'a) \<longlonglongrightarrow> indicator (\<Union>k. \<Union>i<k. A i) x"
hoelzl@57446
   121
    by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def intro: less_le_trans)
wenzelm@60585
   122
  also have "(\<Union>k. \<Union>i<k. A i) = (\<Union>i. A i)"
hoelzl@57446
   123
    by auto
hoelzl@57446
   124
  finally show ?thesis .
hoelzl@57446
   125
qed
hoelzl@57446
   126
hoelzl@57446
   127
lemma LIMSEQ_indicator_decseq:
hoelzl@57446
   128
  assumes "decseq A"
wenzelm@63309
   129
  shows "(\<lambda>i. indicator (A i) x :: 'a::{topological_space,one,zero}) \<longlonglongrightarrow> indicator (\<Inter>i. A i) x"
wenzelm@63309
   130
proof (cases "\<exists>i. x \<notin> A i")
wenzelm@63309
   131
  case True
hoelzl@57446
   132
  then obtain i where "x \<notin> A i"
hoelzl@57446
   133
    by auto
wenzelm@63649
   134
  then have *:
hoelzl@57446
   135
    "\<And>n. (indicator (A (n + i)) x :: 'a) = 0"
hoelzl@57446
   136
    "(indicator (\<Inter>i. A i) x :: 'a) = 0"
wenzelm@60500
   137
    using decseqD[OF \<open>decseq A\<close>, of i "n + i" for n] \<open>x \<notin> A i\<close> by (auto simp: indicator_def)
wenzelm@63649
   138
  show ?thesis
wenzelm@63649
   139
    by (rule LIMSEQ_offset[of _ i]) (use * in simp)
wenzelm@63309
   140
next
wenzelm@63309
   141
  case False
wenzelm@63309
   142
  then show ?thesis by (simp add: indicator_def)
wenzelm@63309
   143
qed
hoelzl@57446
   144
hoelzl@57446
   145
lemma LIMSEQ_indicator_INT:
wenzelm@63309
   146
  "(\<lambda>k. indicator (\<Inter>i<k. A i) x :: 'a::{topological_space,one,zero}) \<longlonglongrightarrow> indicator (\<Inter>i. A i) x"
hoelzl@57446
   147
proof -
wenzelm@61969
   148
  have "(\<lambda>k. indicator (\<Inter>i<k. A i) x::'a) \<longlonglongrightarrow> indicator (\<Inter>k. \<Inter>i<k. A i) x"
hoelzl@57446
   149
    by (intro LIMSEQ_indicator_decseq) (auto simp: decseq_def intro: less_le_trans)
wenzelm@60585
   150
  also have "(\<Inter>k. \<Inter>i<k. A i) = (\<Inter>i. A i)"
hoelzl@57446
   151
    by auto
hoelzl@57446
   152
  finally show ?thesis .
hoelzl@57446
   153
qed
hoelzl@57446
   154
hoelzl@57446
   155
lemma indicator_add:
hoelzl@57446
   156
  "A \<inter> B = {} \<Longrightarrow> (indicator A x::_::monoid_add) + indicator B x = indicator (A \<union> B) x"
hoelzl@57446
   157
  unfolding indicator_def by auto
hoelzl@57446
   158
hoelzl@57446
   159
lemma of_real_indicator: "of_real (indicator A x) = indicator A x"
hoelzl@57446
   160
  by (simp split: split_indicator)
hoelzl@57446
   161
hoelzl@57446
   162
lemma real_of_nat_indicator: "real (indicator A x :: nat) = indicator A x"
hoelzl@57446
   163
  by (simp split: split_indicator)
hoelzl@57446
   164
hoelzl@57446
   165
lemma abs_indicator: "\<bar>indicator A x :: 'a::linordered_idom\<bar> = indicator A x"
hoelzl@57446
   166
  by (simp split: split_indicator)
hoelzl@57446
   167
hoelzl@57446
   168
lemma mult_indicator_subset:
wenzelm@63309
   169
  "A \<subseteq> B \<Longrightarrow> indicator A x * indicator B x = (indicator A x :: 'a::comm_semiring_1)"
hoelzl@57446
   170
  by (auto split: split_indicator simp: fun_eq_iff)
hoelzl@57446
   171
hoelzl@62648
   172
lemma indicator_sums:
hoelzl@57447
   173
  assumes "\<And>i j. i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
hoelzl@57447
   174
  shows "(\<lambda>i. indicator (A i) x::real) sums indicator (\<Union>i. A i) x"
wenzelm@63309
   175
proof (cases "\<exists>i. x \<in> A i")
wenzelm@63309
   176
  case True
hoelzl@57447
   177
  then obtain i where i: "x \<in> A i" ..
hoelzl@57447
   178
  with assms have "(\<lambda>i. indicator (A i) x::real) sums (\<Sum>i\<in>{i}. indicator (A i) x)"
hoelzl@57447
   179
    by (intro sums_finite) (auto split: split_indicator)
hoelzl@57447
   180
  also have "(\<Sum>i\<in>{i}. indicator (A i) x) = indicator (\<Union>i. A i) x"
hoelzl@57447
   181
    using i by (auto split: split_indicator)
hoelzl@57447
   182
  finally show ?thesis .
wenzelm@63309
   183
next
wenzelm@63309
   184
  case False
wenzelm@63309
   185
  then show ?thesis by simp
wenzelm@63309
   186
qed
hoelzl@57447
   187
eberlm@63099
   188
text \<open>
wenzelm@63309
   189
  The indicator function of the union of a disjoint family of sets is the
eberlm@63099
   190
  sum over all the individual indicators.
eberlm@63099
   191
\<close>
wenzelm@63309
   192
eberlm@63099
   193
lemma indicator_UN_disjoint:
haftmann@69313
   194
  "finite A \<Longrightarrow> disjoint_family_on f A \<Longrightarrow> indicator (\<Union>(f ` A)) x = (\<Sum>y\<in>A. indicator (f y) x)"
wenzelm@63309
   195
  by (induct A rule: finite_induct)
wenzelm@63309
   196
    (auto simp: disjoint_family_on_def indicator_def split: if_splits)
eberlm@63099
   197
hoelzl@57446
   198
end