src/HOL/Library/Indicator_Function.thy
author hoelzl
Thu Jul 01 11:48:42 2010 +0200 (2010-07-01)
changeset 37665 579258a77fec
child 45425 7fee7d7abf2f
permissions -rw-r--r--
Add theory for indicator function.
hoelzl@37665
     1
(*  Title:      HOL/Library/Indicator_Function.thy
hoelzl@37665
     2
    Author:     Johannes Hoelzl (TU Muenchen)
hoelzl@37665
     3
*)
hoelzl@37665
     4
hoelzl@37665
     5
header {* Indicator Function *}
hoelzl@37665
     6
hoelzl@37665
     7
theory Indicator_Function
hoelzl@37665
     8
imports Main
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
hoelzl@37665
    13
lemma indicator_simps[simp]:
hoelzl@37665
    14
  "x \<in> S \<Longrightarrow> indicator S x = 1"
hoelzl@37665
    15
  "x \<notin> S \<Longrightarrow> indicator S x = 0"
hoelzl@37665
    16
  unfolding indicator_def by auto
hoelzl@37665
    17
hoelzl@37665
    18
lemma
hoelzl@37665
    19
  shows indicator_pos_le[intro, simp]: "(0::'a::linordered_semidom) \<le> indicator S x"
hoelzl@37665
    20
  and indicator_le_1[intro, simp]: "indicator S x \<le> (1::'a::linordered_semidom)"
hoelzl@37665
    21
  and indicator_abs_le_1: "\<bar>indicator S x\<bar> \<le> (1::'a::linordered_idom)"
hoelzl@37665
    22
  unfolding indicator_def by auto
hoelzl@37665
    23
hoelzl@37665
    24
lemma split_indicator:
hoelzl@37665
    25
  "P (indicator S x) \<longleftrightarrow> ((x \<in> S \<longrightarrow> P 1) \<and> (x \<notin> S \<longrightarrow> P 0))"
hoelzl@37665
    26
  unfolding indicator_def by auto
hoelzl@37665
    27
hoelzl@37665
    28
lemma
hoelzl@37665
    29
  shows indicator_inter_arith: "indicator (A \<inter> B) x = indicator A x * (indicator B x::'a::semiring_1)"
hoelzl@37665
    30
  and indicator_union_arith: "indicator (A \<union> B) x =  indicator A x + indicator B x - indicator A x * (indicator B x::'a::ring_1)"
hoelzl@37665
    31
  and indicator_inter_min: "indicator (A \<inter> B) x = min (indicator A x) (indicator B x::'a::linordered_semidom)"
hoelzl@37665
    32
  and indicator_union_max: "indicator (A \<union> B) x = max (indicator A x) (indicator B x::'a::linordered_semidom)"
hoelzl@37665
    33
  and indicator_compl: "indicator (- A) x = 1 - (indicator A x::'a::ring_1)"
hoelzl@37665
    34
  and indicator_diff: "indicator (A - B) x = indicator A x * (1 - indicator B x::'a::ring_1)"
hoelzl@37665
    35
  unfolding indicator_def by (auto simp: min_def max_def)
hoelzl@37665
    36
hoelzl@37665
    37
lemma
hoelzl@37665
    38
  shows indicator_times: "indicator (A \<times> B) x = indicator A (fst x) * (indicator B (snd x)::'a::semiring_1)"
hoelzl@37665
    39
  unfolding indicator_def by (cases x) auto
hoelzl@37665
    40
hoelzl@37665
    41
lemma
hoelzl@37665
    42
  shows indicator_sum: "indicator (A <+> B) x = (case x of Inl x \<Rightarrow> indicator A x | Inr x \<Rightarrow> indicator B x)"
hoelzl@37665
    43
  unfolding indicator_def by (cases x) auto
hoelzl@37665
    44
hoelzl@37665
    45
lemma
hoelzl@37665
    46
  fixes f :: "'a \<Rightarrow> 'b::semiring_1" assumes "finite A"
hoelzl@37665
    47
  shows setsum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator B x) = (\<Sum>x \<in> A \<inter> B. f x)"
hoelzl@37665
    48
  and setsum_indicator_mult[simp]: "(\<Sum>x \<in> A. indicator B x * f x) = (\<Sum>x \<in> A \<inter> B. f x)"
hoelzl@37665
    49
  unfolding indicator_def
hoelzl@37665
    50
  using assms by (auto intro!: setsum_mono_zero_cong_right split: split_if_asm)
hoelzl@37665
    51
hoelzl@37665
    52
lemma setsum_indicator_eq_card:
hoelzl@37665
    53
  assumes "finite A"
hoelzl@37665
    54
  shows "(SUM x : A. indicator B x) = card (A Int B)"
hoelzl@37665
    55
  using setsum_mult_indicator[OF assms, of "%x. 1::nat"]
hoelzl@37665
    56
  unfolding card_eq_setsum by simp
hoelzl@37665
    57
hoelzl@37665
    58
end