src/HOL/Library/Indicator_Function.thy
 author Andreas Lochbihler Wed Feb 27 10:33:30 2013 +0100 (2013-02-27) changeset 51288 be7e9a675ec9 parent 45425 7fee7d7abf2f child 54408 67dec4ccaabd permissions -rw-r--r--
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
```     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 indicator_pos_le[intro, simp]: "(0::'a::linordered_semidom) \<le> indicator S x"
```
```    19   and indicator_le_1[intro, simp]: "indicator S x \<le> (1::'a::linordered_semidom)"
```
```    20   unfolding indicator_def by auto
```
```    21
```
```    22 lemma indicator_abs_le_1: "\<bar>indicator S x\<bar> \<le> (1::'a::linordered_idom)"
```
```    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
```
```    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)"
```
```    36   and indicator_union_max: "indicator (A \<union> B) x = max (indicator A x) (indicator B x::'a::linordered_semidom)"
```
```    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)"
```
```    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
```
```    43 lemma indicator_times: "indicator (A \<times> B) x = indicator A (fst x) * (indicator B (snd x)::'a::semiring_1)"
```
```    44   unfolding indicator_def by (cases x) auto
```
```    45
```
```    46 lemma indicator_sum: "indicator (A <+> B) x = (case x of Inl x \<Rightarrow> indicator A x | Inr x \<Rightarrow> indicator B x)"
```
```    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`