src/HOL/Library/Indicator_Function.thy
author wenzelm
Sat, 12 Jan 2013 14:53:56 +0100
changeset 50843 1465521b92a1
parent 45425 7fee7d7abf2f
child 54408 67dec4ccaabd
permissions -rw-r--r--
removed unused/non-portable bash_output_fifo;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37665
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
     1
(*  Title:      HOL/Library/Indicator_Function.thy
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
     2
    Author:     Johannes Hoelzl (TU Muenchen)
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
     3
*)
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
     4
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
     5
header {* Indicator Function *}
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
     6
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
     7
theory Indicator_Function
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
     8
imports Main
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
     9
begin
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    10
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    11
definition "indicator S x = (if x \<in> S then 1 else 0)"
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    12
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    13
lemma indicator_simps[simp]:
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    14
  "x \<in> S \<Longrightarrow> indicator S x = 1"
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    15
  "x \<notin> S \<Longrightarrow> indicator S x = 0"
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    16
  unfolding indicator_def by auto
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    17
45425
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    18
lemma indicator_pos_le[intro, simp]: "(0::'a::linordered_semidom) \<le> indicator S x"
37665
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    19
  and indicator_le_1[intro, simp]: "indicator S x \<le> (1::'a::linordered_semidom)"
45425
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    20
  unfolding indicator_def by auto
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    21
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    22
lemma indicator_abs_le_1: "\<bar>indicator S x\<bar> \<le> (1::'a::linordered_idom)"
37665
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    23
  unfolding indicator_def by auto
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    24
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    25
lemma split_indicator:
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    26
  "P (indicator S x) \<longleftrightarrow> ((x \<in> S \<longrightarrow> P 1) \<and> (x \<notin> S \<longrightarrow> P 0))"
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    27
  unfolding indicator_def by auto
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    28
45425
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    29
lemma indicator_inter_arith: "indicator (A \<inter> B) x = indicator A x * (indicator B x::'a::semiring_1)"
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    30
  unfolding indicator_def by (auto simp: min_def max_def)
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    31
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    32
lemma indicator_union_arith: "indicator (A \<union> B) x =  indicator A x + indicator B x - indicator A x * (indicator B x::'a::ring_1)"
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    33
  unfolding indicator_def by (auto simp: min_def max_def)
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    34
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    35
lemma indicator_inter_min: "indicator (A \<inter> B) x = min (indicator A x) (indicator B x::'a::linordered_semidom)"
37665
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    36
  and indicator_union_max: "indicator (A \<union> B) x = max (indicator A x) (indicator B x::'a::linordered_semidom)"
45425
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    37
  unfolding indicator_def by (auto simp: min_def max_def)
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    38
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    39
lemma indicator_compl: "indicator (- A) x = 1 - (indicator A x::'a::ring_1)"
37665
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    40
  and indicator_diff: "indicator (A - B) x = indicator A x * (1 - indicator B x::'a::ring_1)"
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    41
  unfolding indicator_def by (auto simp: min_def max_def)
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    42
45425
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    43
lemma indicator_times: "indicator (A \<times> B) x = indicator A (fst x) * (indicator B (snd x)::'a::semiring_1)"
37665
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    44
  unfolding indicator_def by (cases x) auto
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    45
45425
7fee7d7abf2f avoid inconsistent sort constraints;
wenzelm
parents: 37665
diff changeset
    46
lemma indicator_sum: "indicator (A <+> B) x = (case x of Inl x \<Rightarrow> indicator A x | Inr x \<Rightarrow> indicator B x)"
37665
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    47
  unfolding indicator_def by (cases x) auto
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    48
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    49
lemma
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    50
  fixes f :: "'a \<Rightarrow> 'b::semiring_1" assumes "finite A"
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    51
  shows setsum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator B x) = (\<Sum>x \<in> A \<inter> B. f x)"
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    52
  and setsum_indicator_mult[simp]: "(\<Sum>x \<in> A. indicator B x * f x) = (\<Sum>x \<in> A \<inter> B. f x)"
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    53
  unfolding indicator_def
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    54
  using assms by (auto intro!: setsum_mono_zero_cong_right split: split_if_asm)
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    55
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    56
lemma setsum_indicator_eq_card:
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    57
  assumes "finite A"
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    58
  shows "(SUM x : A. indicator B x) = card (A Int B)"
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    59
  using setsum_mult_indicator[OF assms, of "%x. 1::nat"]
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    60
  unfolding card_eq_setsum by simp
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    61
579258a77fec Add theory for indicator function.
hoelzl
parents:
diff changeset
    62
end