# HG changeset patch
# User hoelzl
# Date 1384280930 -3600
# Node ID 67dec4ccaabdbffe1ae9a1c1993a71d819f7811a
# Parent  e95831757903d7fdc87ac84c587533649bd40309
equation when indicator function equals 0 or 1

diff -r e95831757903 -r 67dec4ccaabd src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Tue Nov 12 14:24:34 2013 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Tue Nov 12 19:28:50 2013 +0100
@@ -156,7 +156,7 @@
 
 subsubsection "Addition"
 
-instantiation ereal :: "{one,comm_monoid_add}"
+instantiation ereal :: "{one,comm_monoid_add,zero_neq_one}"
 begin
 
 definition "0 = ereal 0"
@@ -197,6 +197,8 @@
     by (cases rule: ereal2_cases[of a b]) simp_all
   show "a + b + c = a + (b + c)"
     by (cases rule: ereal3_cases[of a b c]) simp_all
+  show "0 \<noteq> (1::ereal)"
+    by (simp add: one_ereal_def zero_ereal_def)
 qed
 
 end
diff -r e95831757903 -r 67dec4ccaabd src/HOL/Library/Indicator_Function.thy
--- a/src/HOL/Library/Indicator_Function.thy	Tue Nov 12 14:24:34 2013 +0100
+++ b/src/HOL/Library/Indicator_Function.thy	Tue Nov 12 19:28:50 2013 +0100
@@ -22,6 +22,12 @@
 lemma indicator_abs_le_1: "\<bar>indicator S x\<bar> \<le> (1::'a::linordered_idom)"
   unfolding indicator_def by auto
 
+lemma indicator_eq_0_iff: "indicator A x = (0::_::zero_neq_one) \<longleftrightarrow> x \<notin> A"
+  by (auto simp: indicator_def)
+
+lemma indicator_eq_1_iff: "indicator A x = (1::_::zero_neq_one) \<longleftrightarrow> x \<in> A"
+  by (auto simp: indicator_def)
+
 lemma split_indicator:
   "P (indicator S x) \<longleftrightarrow> ((x \<in> S \<longrightarrow> P 1) \<and> (x \<notin> S \<longrightarrow> P 0))"
   unfolding indicator_def by auto