# HG changeset patch
# User wenzelm
# Date 1320854920 -3600
# Node ID 7fee7d7abf2f3419e49df0a0082ee17794b31ee9
# Parent  01d75cf044979de7049bb90fce77487126ed772d
avoid inconsistent sort constraints;

diff -r 01d75cf04497 -r 7fee7d7abf2f src/HOL/Library/Indicator_Function.thy
--- a/src/HOL/Library/Indicator_Function.thy	Wed Nov 09 15:18:39 2011 +0100
+++ b/src/HOL/Library/Indicator_Function.thy	Wed Nov 09 17:08:40 2011 +0100
@@ -15,31 +15,35 @@
   "x \<notin> S \<Longrightarrow> indicator S x = 0"
   unfolding indicator_def by auto
 
-lemma
-  shows indicator_pos_le[intro, simp]: "(0::'a::linordered_semidom) \<le> indicator S x"
+lemma indicator_pos_le[intro, simp]: "(0::'a::linordered_semidom) \<le> indicator S x"
   and indicator_le_1[intro, simp]: "indicator S x \<le> (1::'a::linordered_semidom)"
-  and indicator_abs_le_1: "\<bar>indicator S x\<bar> \<le> (1::'a::linordered_idom)"
+  unfolding indicator_def by auto
+
+lemma indicator_abs_le_1: "\<bar>indicator S x\<bar> \<le> (1::'a::linordered_idom)"
   unfolding indicator_def by auto
 
 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
 
-lemma
-  shows indicator_inter_arith: "indicator (A \<inter> B) x = indicator A x * (indicator B x::'a::semiring_1)"
-  and indicator_union_arith: "indicator (A \<union> B) x =  indicator A x + indicator B x - indicator A x * (indicator B x::'a::ring_1)"
-  and indicator_inter_min: "indicator (A \<inter> B) x = min (indicator A x) (indicator B x::'a::linordered_semidom)"
+lemma indicator_inter_arith: "indicator (A \<inter> B) x = indicator A x * (indicator B x::'a::semiring_1)"
+  unfolding indicator_def by (auto simp: min_def max_def)
+
+lemma indicator_union_arith: "indicator (A \<union> B) x =  indicator A x + indicator B x - indicator A x * (indicator B x::'a::ring_1)"
+  unfolding indicator_def by (auto simp: min_def max_def)
+
+lemma indicator_inter_min: "indicator (A \<inter> B) x = min (indicator A x) (indicator B x::'a::linordered_semidom)"
   and indicator_union_max: "indicator (A \<union> B) x = max (indicator A x) (indicator B x::'a::linordered_semidom)"
-  and indicator_compl: "indicator (- A) x = 1 - (indicator A x::'a::ring_1)"
+  unfolding indicator_def by (auto simp: min_def max_def)
+
+lemma indicator_compl: "indicator (- A) x = 1 - (indicator A x::'a::ring_1)"
   and indicator_diff: "indicator (A - B) x = indicator A x * (1 - indicator B x::'a::ring_1)"
   unfolding indicator_def by (auto simp: min_def max_def)
 
-lemma
-  shows indicator_times: "indicator (A \<times> B) x = indicator A (fst x) * (indicator B (snd x)::'a::semiring_1)"
+lemma indicator_times: "indicator (A \<times> B) x = indicator A (fst x) * (indicator B (snd x)::'a::semiring_1)"
   unfolding indicator_def by (cases x) auto
 
-lemma
-  shows indicator_sum: "indicator (A <+> B) x = (case x of Inl x \<Rightarrow> indicator A x | Inr x \<Rightarrow> indicator B x)"
+lemma indicator_sum: "indicator (A <+> B) x = (case x of Inl x \<Rightarrow> indicator A x | Inr x \<Rightarrow> indicator B x)"
   unfolding indicator_def by (cases x) auto
 
 lemma
diff -r 01d75cf04497 -r 7fee7d7abf2f src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Wed Nov 09 15:18:39 2011 +0100
+++ b/src/HOL/Presburger.thy	Wed Nov 09 17:08:40 2011 +0100
@@ -25,8 +25,8 @@
   "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<le> t) = True"
   "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x > t) = False"
   "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<ge> t) = False"
-  "\<exists>z.\<forall>(x::'a::{linorder,plus,Rings.dvd})<z. (d dvd x + s) = (d dvd x + s)"
-  "\<exists>z.\<forall>(x::'a::{linorder,plus,Rings.dvd})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
+  "\<exists>z.\<forall>(x::'b::{linorder,plus,Rings.dvd})<z. (d dvd x + s) = (d dvd x + s)"
+  "\<exists>z.\<forall>(x::'b::{linorder,plus,Rings.dvd})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
   "\<exists>z.\<forall>x<z. F = F"
   by ((erule exE, erule exE,rule_tac x="min z za" in exI,simp)+, (rule_tac x="t" in exI,fastforce)+) simp_all
 
@@ -41,8 +41,8 @@
   "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<le> t) = False"
   "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x > t) = True"
   "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<ge> t) = True"
-  "\<exists>z.\<forall>(x::'a::{linorder,plus,Rings.dvd})>z. (d dvd x + s) = (d dvd x + s)"
-  "\<exists>z.\<forall>(x::'a::{linorder,plus,Rings.dvd})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
+  "\<exists>z.\<forall>(x::'b::{linorder,plus,Rings.dvd})>z. (d dvd x + s) = (d dvd x + s)"
+  "\<exists>z.\<forall>(x::'b::{linorder,plus,Rings.dvd})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
   "\<exists>z.\<forall>x>z. F = F"
   by ((erule exE, erule exE,rule_tac x="max z za" in exI,simp)+,(rule_tac x="t" in exI,fastforce)+) simp_all