equation when indicator function equals 0 or 1
authorhoelzl
Tue Nov 12 19:28:50 2013 +0100 (2013-11-12)
changeset 5440867dec4ccaabd
parent 54407 e95831757903
child 54409 2e501a90dec7
equation when indicator function equals 0 or 1
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Indicator_Function.thy
     1.1 --- a/src/HOL/Library/Extended_Real.thy	Tue Nov 12 14:24:34 2013 +0100
     1.2 +++ b/src/HOL/Library/Extended_Real.thy	Tue Nov 12 19:28:50 2013 +0100
     1.3 @@ -156,7 +156,7 @@
     1.4  
     1.5  subsubsection "Addition"
     1.6  
     1.7 -instantiation ereal :: "{one,comm_monoid_add}"
     1.8 +instantiation ereal :: "{one,comm_monoid_add,zero_neq_one}"
     1.9  begin
    1.10  
    1.11  definition "0 = ereal 0"
    1.12 @@ -197,6 +197,8 @@
    1.13      by (cases rule: ereal2_cases[of a b]) simp_all
    1.14    show "a + b + c = a + (b + c)"
    1.15      by (cases rule: ereal3_cases[of a b c]) simp_all
    1.16 +  show "0 \<noteq> (1::ereal)"
    1.17 +    by (simp add: one_ereal_def zero_ereal_def)
    1.18  qed
    1.19  
    1.20  end
     2.1 --- a/src/HOL/Library/Indicator_Function.thy	Tue Nov 12 14:24:34 2013 +0100
     2.2 +++ b/src/HOL/Library/Indicator_Function.thy	Tue Nov 12 19:28:50 2013 +0100
     2.3 @@ -22,6 +22,12 @@
     2.4  lemma indicator_abs_le_1: "\<bar>indicator S x\<bar> \<le> (1::'a::linordered_idom)"
     2.5    unfolding indicator_def by auto
     2.6  
     2.7 +lemma indicator_eq_0_iff: "indicator A x = (0::_::zero_neq_one) \<longleftrightarrow> x \<notin> A"
     2.8 +  by (auto simp: indicator_def)
     2.9 +
    2.10 +lemma indicator_eq_1_iff: "indicator A x = (1::_::zero_neq_one) \<longleftrightarrow> x \<in> A"
    2.11 +  by (auto simp: indicator_def)
    2.12 +
    2.13  lemma split_indicator:
    2.14    "P (indicator S x) \<longleftrightarrow> ((x \<in> S \<longrightarrow> P 1) \<and> (x \<notin> S \<longrightarrow> P 0))"
    2.15    unfolding indicator_def by auto