equal
deleted
inserted
replaced
7 theory Indicator_Function |
7 theory Indicator_Function |
8 imports Complex_Main Disjoint_Sets |
8 imports Complex_Main Disjoint_Sets |
9 begin |
9 begin |
10 |
10 |
11 definition "indicator S x = (if x \<in> S then 1 else 0)" |
11 definition "indicator S x = (if x \<in> S then 1 else 0)" |
|
12 |
|
13 text\<open>Type constrained version\<close> |
|
14 abbreviation indicat_real :: "'a set \<Rightarrow> 'a \<Rightarrow> real" where "indicat_real S \<equiv> indicator S" |
12 |
15 |
13 lemma indicator_simps[simp]: |
16 lemma indicator_simps[simp]: |
14 "x \<in> S \<Longrightarrow> indicator S x = 1" |
17 "x \<in> S \<Longrightarrow> indicator S x = 1" |
15 "x \<notin> S \<Longrightarrow> indicator S x = 0" |
18 "x \<notin> S \<Longrightarrow> indicator S x = 0" |
16 unfolding indicator_def by auto |
19 unfolding indicator_def by auto |