author huffman Wed, 06 Jun 2007 17:01:33 +0200 changeset 23277 aa158e145ea3 parent 23276 a70934b63910 child 23278 375335bf619f
generalize class constraints on some lemmas
 src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions src/HOL/NatBin.thy file | annotate | diff | comparison | revisions src/HOL/SetInterval.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Finite_Set.thy	Wed Jun 06 17:00:09 2007 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Jun 06 17:01:33 2007 +0200
@@ -1405,7 +1405,7 @@
by (induct set: finite) auto

lemma setprod_zero:
-     "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==> setprod f A = 0"
+     "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0"
apply (induct set: finite, force, clarsimp)
apply (erule disjE, auto)
done
@@ -1429,24 +1429,24 @@
done

lemma setprod_nonzero [rule_format]:
-    "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
+    "(ALL x y. (x::'a::comm_semiring_1) * y = 0 --> x = 0 | y = 0) ==>
finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0"
apply (erule finite_induct, auto)
done

lemma setprod_zero_eq:
-    "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==>
+    "(ALL x y. (x::'a::comm_semiring_1) * y = 0 --> x = 0 | y = 0) ==>
finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)"
apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast)
done

lemma setprod_nonzero_field:
-    "finite A ==> (ALL x: A. f x \<noteq> (0::'a::field)) ==> setprod f A \<noteq> 0"
+    "finite A ==> (ALL x: A. f x \<noteq> (0::'a::idom)) ==> setprod f A \<noteq> 0"
apply (rule setprod_nonzero, auto)
done

lemma setprod_zero_eq_field:
-    "finite A ==> (setprod f A = (0::'a::field)) = (EX x: A. f x = 0)"
+    "finite A ==> (setprod f A = (0::'a::idom)) = (EX x: A. f x = 0)"
apply (rule setprod_zero_eq, auto)
done

@@ -1657,7 +1657,7 @@
done

lemma setsum_bounded:
-  assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{comm_semiring_1_cancel, pordered_ab_semigroup_add})"
+  assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, pordered_ab_semigroup_add})"
shows "setsum f A \<le> of_nat(card A) * K"
proof (cases "finite A")
case True```
```--- a/src/HOL/NatBin.thy	Wed Jun 06 17:00:09 2007 +0200
+++ b/src/HOL/NatBin.thy	Wed Jun 06 17:01:33 2007 +0200
@@ -274,13 +274,13 @@
We cannot prove general results about the numeral @{term "-1"}, so we have to

-lemma power2_eq_square: "(a::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = a * a"
+lemma power2_eq_square: "(a::'a::recpower)\<twosuperior> = a * a"

-lemma zero_power2 [simp]: "(0::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 0"
+lemma zero_power2 [simp]: "(0::'a::{semiring_1,recpower})\<twosuperior> = 0"

-lemma one_power2 [simp]: "(1::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 1"
+lemma one_power2 [simp]: "(1::'a::{semiring_1,recpower})\<twosuperior> = 1"

lemma power3_eq_cube: "(x::'a::recpower) ^ 3 = x * x * x"```
```--- a/src/HOL/SetInterval.thy	Wed Jun 06 17:00:09 2007 +0200
+++ b/src/HOL/SetInterval.thy	Wed Jun 06 17:01:33 2007 +0200
@@ -750,7 +750,7 @@
subsection {* The formula for arithmetic sums *}

lemma gauss_sum:
-  "((1::'a::comm_semiring_1_cancel) + 1)*(\<Sum>i\<in>{1..n}. of_nat i) =
+  "((1::'a::comm_semiring_1) + 1)*(\<Sum>i\<in>{1..n}. of_nat i) =
of_nat n*((of_nat n)+1)"
proof (induct n)
case 0
@@ -761,7 +761,7 @@
qed

theorem arith_series_general:
-  "((1::'a::comm_semiring_1_cancel) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
+  "((1::'a::comm_semiring_1) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
of_nat n * (a + (a + of_nat(n - 1)*d))"
proof cases
assume ngt1: "n > 1"```