Theory Indicator_Function

theory Indicator_Function
imports Main
(*  Title:      HOL/Library/Indicator_Function.thy
Author: Johannes Hoelzl (TU Muenchen)
*)


header {* Indicator Function *}

theory Indicator_Function
imports Main
begin

definition "indicator S x = (if x ∈ S then 1 else 0)"

lemma indicator_simps[simp]:
"x ∈ S ==> indicator S x = 1"
"x ∉ S ==> indicator S x = 0"
unfolding indicator_def by auto

lemma indicator_pos_le[intro, simp]: "(0::'a::linordered_semidom) ≤ indicator S x"
and indicator_le_1[intro, simp]: "indicator S x ≤ (1::'a::linordered_semidom)"
unfolding indicator_def by auto

lemma indicator_abs_le_1: "¦indicator S x¦ ≤ (1::'a::linordered_idom)"
unfolding indicator_def by auto

lemma split_indicator:
"P (indicator S x) <-> ((x ∈ S --> P 1) ∧ (x ∉ S --> P 0))"
unfolding indicator_def by auto

lemma indicator_inter_arith: "indicator (A ∩ B) x = indicator A x * (indicator B x::'a::semiring_1)"
unfolding indicator_def by (auto simp: min_def max_def)

lemma indicator_union_arith: "indicator (A ∪ B) x = indicator A x + indicator B x - indicator A x * (indicator B x::'a::ring_1)"
unfolding indicator_def by (auto simp: min_def max_def)

lemma indicator_inter_min: "indicator (A ∩ B) x = min (indicator A x) (indicator B x::'a::linordered_semidom)"
and indicator_union_max: "indicator (A ∪ B) x = max (indicator A x) (indicator B x::'a::linordered_semidom)"
unfolding indicator_def by (auto simp: min_def max_def)

lemma indicator_compl: "indicator (- A) x = 1 - (indicator A x::'a::ring_1)"
and indicator_diff: "indicator (A - B) x = indicator A x * (1 - indicator B x::'a::ring_1)"
unfolding indicator_def by (auto simp: min_def max_def)

lemma indicator_times: "indicator (A × B) x = indicator A (fst x) * (indicator B (snd x)::'a::semiring_1)"
unfolding indicator_def by (cases x) auto

lemma indicator_sum: "indicator (A <+> B) x = (case x of Inl x => indicator A x | Inr x => indicator B x)"
unfolding indicator_def by (cases x) auto

lemma
fixes f :: "'a => 'b::semiring_1" assumes "finite A"
shows setsum_mult_indicator[simp]: "(∑x ∈ A. f x * indicator B x) = (∑x ∈ A ∩ B. f x)"
and setsum_indicator_mult[simp]: "(∑x ∈ A. indicator B x * f x) = (∑x ∈ A ∩ B. f x)"
unfolding indicator_def
using assms by (auto intro!: setsum_mono_zero_cong_right split: split_if_asm)

lemma setsum_indicator_eq_card:
assumes "finite A"
shows "(SUM x : A. indicator B x) = card (A Int B)"
using setsum_mult_indicator[OF assms, of "%x. 1::nat"]
unfolding card_eq_setsum by simp

end