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