37665
|
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 |
|
45425
|
18 |
lemma indicator_pos_le[intro, simp]: "(0::'a::linordered_semidom) \<le> indicator S x"
|
37665
|
19 |
and indicator_le_1[intro, simp]: "indicator S x \<le> (1::'a::linordered_semidom)"
|
45425
|
20 |
unfolding indicator_def by auto
|
|
21 |
|
|
22 |
lemma indicator_abs_le_1: "\<bar>indicator S x\<bar> \<le> (1::'a::linordered_idom)"
|
37665
|
23 |
unfolding indicator_def by auto
|
|
24 |
|
|
25 |
lemma split_indicator:
|
|
26 |
"P (indicator S x) \<longleftrightarrow> ((x \<in> S \<longrightarrow> P 1) \<and> (x \<notin> S \<longrightarrow> P 0))"
|
|
27 |
unfolding indicator_def by auto
|
|
28 |
|
45425
|
29 |
lemma indicator_inter_arith: "indicator (A \<inter> B) x = indicator A x * (indicator B x::'a::semiring_1)"
|
|
30 |
unfolding indicator_def by (auto simp: min_def max_def)
|
|
31 |
|
|
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)"
|
|
33 |
unfolding indicator_def by (auto simp: min_def max_def)
|
|
34 |
|
|
35 |
lemma indicator_inter_min: "indicator (A \<inter> B) x = min (indicator A x) (indicator B x::'a::linordered_semidom)"
|
37665
|
36 |
and indicator_union_max: "indicator (A \<union> B) x = max (indicator A x) (indicator B x::'a::linordered_semidom)"
|
45425
|
37 |
unfolding indicator_def by (auto simp: min_def max_def)
|
|
38 |
|
|
39 |
lemma indicator_compl: "indicator (- A) x = 1 - (indicator A x::'a::ring_1)"
|
37665
|
40 |
and indicator_diff: "indicator (A - B) x = indicator A x * (1 - indicator B x::'a::ring_1)"
|
|
41 |
unfolding indicator_def by (auto simp: min_def max_def)
|
|
42 |
|
45425
|
43 |
lemma indicator_times: "indicator (A \<times> B) x = indicator A (fst x) * (indicator B (snd x)::'a::semiring_1)"
|
37665
|
44 |
unfolding indicator_def by (cases x) auto
|
|
45 |
|
45425
|
46 |
lemma indicator_sum: "indicator (A <+> B) x = (case x of Inl x \<Rightarrow> indicator A x | Inr x \<Rightarrow> indicator B x)"
|
37665
|
47 |
unfolding indicator_def by (cases x) auto
|
|
48 |
|
|
49 |
lemma
|
|
50 |
fixes f :: "'a \<Rightarrow> 'b::semiring_1" assumes "finite A"
|
|
51 |
shows setsum_mult_indicator[simp]: "(\<Sum>x \<in> A. f x * indicator B x) = (\<Sum>x \<in> A \<inter> B. f x)"
|
|
52 |
and setsum_indicator_mult[simp]: "(\<Sum>x \<in> A. indicator B x * f x) = (\<Sum>x \<in> A \<inter> B. f x)"
|
|
53 |
unfolding indicator_def
|
|
54 |
using assms by (auto intro!: setsum_mono_zero_cong_right split: split_if_asm)
|
|
55 |
|
|
56 |
lemma setsum_indicator_eq_card:
|
|
57 |
assumes "finite A"
|
|
58 |
shows "(SUM x : A. indicator B x) = card (A Int B)"
|
|
59 |
using setsum_mult_indicator[OF assms, of "%x. 1::nat"]
|
|
60 |
unfolding card_eq_setsum by simp
|
|
61 |
|
|
62 |
end |