Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
avoid inconsistent sort constraints;
authorwenzelm
Wed, 09 Nov 2011 17:08:40 +0100
changeset 45425 7fee7d7abf2f
parent 45424 01d75cf04497
child 45426 4548b8e1ba12
avoid inconsistent sort constraints;
src/HOL/Library/Indicator_Function.thy file | annotate | diff | comparison | revisions
src/HOL/Presburger.thy file | annotate | diff | comparison | revisions 
--- 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
--- 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
isabelle