--- a/src/HOL/Complex/CLim.thy Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Complex/CLim.thy Thu Mar 04 12:06:07 2004 +0100
@@ -858,8 +858,7 @@
apply (simp (no_asm_simp))
apply (rule capprox_mult_hcomplex_of_complex)
apply (auto intro!: NSCDERIVD1 intro: capprox_minus_iff [THEN iffD2]
- simp add: diff_minus [symmetric]
- divide_inverse_zero [symmetric])
+ simp add: diff_minus [symmetric] divide_inverse [symmetric])
apply (blast intro: NSCDERIVD2)
done
@@ -968,8 +967,10 @@
apply (simp add: complex_diff_def)
apply (drule_tac f = g in CDERIV_inverse_fun)
apply (drule_tac [2] CDERIV_mult, assumption+)
-apply (simp add: divide_inverse_zero right_distrib power_inverse minus_mult_left mult_ac
- del: complexpow_Suc minus_mult_right [symmetric] minus_mult_left [symmetric])
+apply (simp add: divide_inverse right_distrib power_inverse minus_mult_left
+ mult_ac
+ del: minus_mult_right [symmetric] minus_mult_left [symmetric]
+ complexpow_Suc)
done
lemma NSCDERIV_quotient:
--- a/src/HOL/Complex/CStar.thy Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Complex/CStar.thy Thu Mar 04 12:06:07 2004 +0100
@@ -489,18 +489,17 @@
done
lemma starfunC_divide: "( *fc* f) y / ( *fc* g) y = ( *fc* (%x. f x / g x)) y"
-by (simp add: divide_inverse_zero)
+by (simp add: divide_inverse)
declare starfunC_divide [symmetric, simp]
lemma starfunCR_divide:
"( *fcR* f) y / ( *fcR* g) y = ( *fcR* (%x. f x / g x)) y"
-by (simp add: divide_inverse_zero)
+by (simp add: divide_inverse)
declare starfunCR_divide [symmetric, simp]
lemma starfunRC_divide:
"( *fRc* f) y / ( *fRc* g) y = ( *fRc* (%x. f x / g x)) y"
-apply (simp add: divide_inverse_zero)
-done
+by (simp add: divide_inverse)
declare starfunRC_divide [symmetric, simp]
--- a/src/HOL/Complex/Complex.thy Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Complex/Complex.thy Thu Mar 04 12:06:07 2004 +0100
@@ -1,4 +1,5 @@
(* Title: Complex.thy
+ ID: $Id$
Author: Jacques D. Fleuriot
Copyright: 2001 University of Edinburgh
Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
@@ -216,7 +217,7 @@
apply (induct z)
apply (rename_tac x y)
apply (auto simp add: complex_mult complex_inverse complex_one_def
- complex_zero_def add_divide_distrib [symmetric] power2_eq_square mult_ac)
+ complex_zero_def add_divide_distrib [symmetric] power2_eq_square mult_ac)
apply (drule_tac y = y in real_sum_squares_not_zero)
apply (drule_tac [2] x = x in real_sum_squares_not_zero2, auto)
done
@@ -248,20 +249,17 @@
show "(u + v) * w = u * w + v * w"
by (simp add: complex_mult_def complex_add_def left_distrib
diff_minus add_ac)
- assume neq: "w \<noteq> 0"
- thus "z / w = z * inverse w"
+ show "z / w = z * inverse w"
by (simp add: complex_divide_def)
- show "inverse w * w = 1"
- by (simp add: neq complex_mult_inv_left)
+ assume "w \<noteq> 0"
+ thus "inverse w * w = 1"
+ by (simp add: complex_mult_inv_left)
qed
instance complex :: division_by_zero
proof
- show inv: "inverse 0 = (0::complex)"
+ show "inverse 0 = (0::complex)"
by (simp add: complex_inverse_def complex_zero_def)
- fix x :: complex
- show "x/0 = 0"
- by (simp add: complex_divide_def inv)
qed
@@ -789,7 +787,7 @@
complex_diff_def)
lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
-by (simp add: divide_inverse_zero rcis_def complex_of_real_inverse)
+by (simp add: divide_inverse rcis_def complex_of_real_inverse)
lemma cis_divide: "cis a / cis b = cis (a - b)"
by (simp add: complex_divide_def cis_mult real_diff_def)
--- a/src/HOL/Complex/NSCA.thy Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Complex/NSCA.thy Thu Mar 04 12:06:07 2004 +0100
@@ -56,7 +56,7 @@
done
lemma SComplex_divide: "[| x \<in> SComplex; y \<in> SComplex |] ==> x/y \<in> SComplex"
-by (simp add: SComplex_mult SComplex_inverse divide_inverse_zero)
+by (simp add: SComplex_mult SComplex_inverse divide_inverse)
lemma SComplex_minus: "x \<in> SComplex ==> -x \<in> SComplex"
apply (simp add: SComplex_def)
@@ -98,7 +98,7 @@
lemma SComplex_divide_number_of:
"r \<in> SComplex ==> r/(number_of w::hcomplex) \<in> SComplex"
-apply (simp only: divide_inverse_zero)
+apply (simp only: divide_inverse)
apply (blast intro!: SComplex_number_of SComplex_mult SComplex_inverse)
done
@@ -618,7 +618,7 @@
lemma CInfinitesimal_ratio:
"[| y \<noteq> 0; y \<in> CInfinitesimal; x/y \<in> CFinite |] ==> x \<in> CInfinitesimal"
apply (drule CInfinitesimal_CFinite_mult2, assumption)
-apply (simp add: divide_inverse_zero hcomplex_mult_assoc)
+apply (simp add: divide_inverse hcomplex_mult_assoc)
done
lemma SComplex_capprox_iff:
@@ -1126,7 +1126,7 @@
lemma stc_divide [simp]:
"[| x \<in> CFinite; y \<in> CFinite; stc y \<noteq> 0 |]
==> stc(x/y) = (stc x) / (stc y)"
-by (simp add: divide_inverse_zero stc_mult stc_not_CInfinitesimal CFinite_inverse stc_inverse)
+by (simp add: divide_inverse stc_mult stc_not_CInfinitesimal CFinite_inverse stc_inverse)
lemma stc_idempotent [simp]: "x \<in> CFinite ==> stc(stc(x)) = stc(x)"
by (blast intro: stc_CFinite stc_capprox_self capprox_stc_eq)
--- a/src/HOL/Complex/NSComplex.thy Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Complex/NSComplex.thy Thu Mar 04 12:06:07 2004 +0100
@@ -1,9 +1,12 @@
(* Title: NSComplex.thy
+ ID: $Id$
Author: Jacques D. Fleuriot
Copyright: 2001 University of Edinburgh
- Description: Nonstandard Complex numbers
+ Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
*)
+header{*Nonstandard Complex Numbers*}
+
theory NSComplex = NSInduct:
constdefs
@@ -394,20 +397,17 @@
by (rule hcomplex_zero_not_eq_one)
show "(u + v) * w = u * w + v * w"
by (simp add: hcomplex_add_mult_distrib)
- assume neq: "w \<noteq> 0"
- thus "z / w = z * inverse w"
+ show "z / w = z * inverse w"
by (simp add: hcomplex_divide_def)
- show "inverse w * w = 1"
+ assume "w \<noteq> 0"
+ thus "inverse w * w = 1"
by (rule hcomplex_mult_inv_left)
qed
instance hcomplex :: division_by_zero
proof
- show inv: "inverse 0 = (0::hcomplex)"
+ show "inverse 0 = (0::hcomplex)"
by (simp add: hcomplex_inverse hcomplex_zero_def)
- fix x :: hcomplex
- show "x/0 = 0"
- by (simp add: hcomplex_divide_def inv)
qed
--- a/src/HOL/Divides.thy Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Divides.thy Thu Mar 04 12:06:07 2004 +0100
@@ -14,8 +14,6 @@
div < type
instance nat :: div ..
-instance nat :: plus_ac0
-proof qed (rule add_commute add_assoc add_0)+
consts
div :: "'a::div \<Rightarrow> 'a \<Rightarrow> 'a" (infixl 70)
--- a/src/HOL/Finite_Set.thy Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Finite_Set.thy Thu Mar 04 12:06:07 2004 +0100
@@ -1,6 +1,7 @@
(* Title: HOL/Finite_Set.thy
ID: $Id$
Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
+ Additions by Jeremy Avigad in Feb 2004
License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
@@ -8,6 +9,65 @@
theory Finite_Set = Divides + Power + Inductive + SetInterval:
+subsection {* Types Classes @{text plus_ac0} and @{text times_ac1} *}
+
+axclass plus_ac0 < plus, zero
+ commute: "x + y = y + x"
+ assoc: "(x + y) + z = x + (y + z)"
+ zero [simp]: "0 + x = x"
+
+lemma plus_ac0_left_commute: "x + (y+z) = y + ((x+z)::'a::plus_ac0)"
+apply (rule plus_ac0.commute [THEN trans])
+apply (rule plus_ac0.assoc [THEN trans])
+apply (rule plus_ac0.commute [THEN arg_cong])
+done
+
+lemma plus_ac0_zero_right [simp]: "x + 0 = (x ::'a::plus_ac0)"
+apply (rule plus_ac0.commute [THEN trans])
+apply (rule plus_ac0.zero)
+done
+
+lemmas plus_ac0 = plus_ac0.assoc plus_ac0.commute plus_ac0_left_commute
+ plus_ac0.zero plus_ac0_zero_right
+
+instance semiring < plus_ac0
+proof qed (rule add_commute add_assoc almost_semiring.add_0)+
+
+axclass times_ac1 < times, one
+ commute: "x * y = y * x"
+ assoc: "(x * y) * z = x * (y * z)"
+ one: "1 * x = x"
+
+theorem times_ac1_left_commute: "(x::'a::times_ac1) * ((y::'a) * z) =
+ y * (x * z)"
+proof -
+ have "(x::'a::times_ac1) * (y * z) = (x * y) * z"
+ by (rule times_ac1.assoc [THEN sym])
+ also have "x * y = y * x"
+ by (rule times_ac1.commute)
+ also have "(y * x) * z = y * (x * z)"
+ by (rule times_ac1.assoc)
+ finally show ?thesis .
+qed
+
+theorem times_ac1_one_right: "(x::'a::times_ac1) * 1 = x"
+proof -
+ have "x * 1 = 1 * x"
+ by (rule times_ac1.commute)
+ also have "... = x"
+ by (rule times_ac1.one)
+ finally show ?thesis .
+qed
+
+instance semiring < times_ac1
+ apply intro_classes
+ apply (rule mult_commute)
+ apply (rule mult_assoc, simp)
+ done
+
+theorems times_ac1 = times_ac1.assoc times_ac1.commute times_ac1_left_commute
+ times_ac1.one times_ac1_one_right
+
subsection {* Collection of finite sets *}
consts Finites :: "'a set set"
@@ -25,8 +85,8 @@
finite: "finite UNIV"
lemma ex_new_if_finite: -- "does not depend on def of finite at all"
- "\<lbrakk> ~finite(UNIV::'a set); finite A \<rbrakk> \<Longrightarrow> \<exists>a::'a. a ~: A"
-by(subgoal_tac "A ~= UNIV", blast, blast)
+ "[| ~finite(UNIV::'a set); finite A |] ==> \<exists>a::'a. a \<notin> A"
+by(subgoal_tac "A \<noteq> UNIV", blast, blast)
lemma finite_induct [case_names empty insert, induct set: Finites]:
@@ -167,6 +227,11 @@
-- {* The image of a finite set is finite. *}
by (induct set: Finites) simp_all
+lemma finite_surj: "finite A ==> B <= f ` A ==> finite B"
+ apply (frule finite_imageI)
+ apply (erule finite_subset, assumption)
+ done
+
lemma finite_range_imageI:
"finite (range g) ==> finite (range (%x. f (g x)))"
apply (drule finite_imageI, simp)
@@ -195,16 +260,16 @@
lemma inj_vimage_singleton: "inj f ==> f-`{a} \<subseteq> {THE x. f x = a}"
-- {* The inverse image of a singleton under an injective function
is included in a singleton. *}
- apply (auto simp add: inj_on_def)
- apply (blast intro: the_equality [symmetric])
+ apply (auto simp add: inj_on_def)
+ apply (blast intro: the_equality [symmetric])
done
lemma finite_vimageI: "[|finite F; inj h|] ==> finite (h -` F)"
-- {* The inverse image of a finite set under an injective function
is finite. *}
- apply (induct set: Finites, simp_all)
- apply (subst vimage_insert)
- apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton])
+ apply (induct set: Finites, simp_all)
+ apply (subst vimage_insert)
+ apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton])
done
@@ -215,10 +280,10 @@
text {*
Strengthen RHS to
- @{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x ~= {}})"}?
+ @{prop "((ALL x:A. finite (B x)) & finite {x. x:A & B x \<noteq> {}})"}?
We'd need to prove
- @{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x ~= {}}"}
+ @{prop "finite C ==> ALL A B. (UNION A B) <= C --> finite {x. x:A & B x \<noteq> {}}"}
by induction. *}
lemma finite_UN [simp]: "finite A ==> finite (UNION A B) = (ALL x:A. finite (B x))"
@@ -281,6 +346,9 @@
apply simp
done
+
+subsubsection {* Intervals of nats *}
+
lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..k(}"
by (induct k) (simp_all add: lessThan_Suc)
@@ -337,6 +405,10 @@
apply (auto simp add: finite_Field)
done
+lemma finite_cartesian_product: "[| finite A; finite B |] ==>
+ finite (A <*> B)"
+ by (rule finite_SigmaI)
+
subsection {* Finite cardinality *}
@@ -521,8 +593,7 @@
done
lemma card_image: "finite A ==> inj_on f A ==> card (f ` A) = card A"
- apply (induct set: Finites, simp_all, atomize)
- apply safe
+ apply (induct set: Finites, simp_all, atomize, safe)
apply (unfold inj_on_def, blast)
apply (subst card_insert_disjoint)
apply (erule finite_imageI, blast, blast)
@@ -553,7 +624,7 @@
lemma dvd_partition:
"finite C ==> finite (Union C) ==>
ALL c : C. k dvd card c ==>
- (ALL c1: C. ALL c2: C. c1 ~= c2 --> c1 Int c2 = {}) ==>
+ (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==>
k dvd card (Union C)"
apply (induct set: Finites, simp_all, clarify)
apply (subst card_Un_disjoint)
@@ -784,10 +855,6 @@
apply (erule finite_induct, auto)
done
-lemma setsum_eq_0_iff [simp]:
- "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
- by (induct set: Finites) auto
-
lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
apply (case_tac "finite A")
prefer 2 apply (simp add: setsum_def)
@@ -825,6 +892,14 @@
apply (simp add: setsum_Un_disjoint)
done
+lemma setsum_Union_disjoint:
+ "finite C ==> (ALL A:C. finite A) ==>
+ (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
+ setsum f (Union C) = setsum (setsum f) C"
+ apply (frule setsum_UN_disjoint [of C id f])
+ apply (unfold Union_def id_def, assumption+)
+ done
+
lemma setsum_addf: "setsum (\<lambda>x. f x + g x) A = (setsum f A + setsum g A)"
apply (case_tac "finite A")
prefer 2 apply (simp add: setsum_def)
@@ -832,21 +907,6 @@
apply (simp add: plus_ac0)
done
-lemma setsum_Un: "finite A ==> finite B ==>
- (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
- -- {* For the natural numbers, we have subtraction. *}
- apply (subst setsum_Un_Int [symmetric], auto)
- done
-
-lemma setsum_diff1: "(setsum f (A - {a}) :: nat) =
- (if a:A then setsum f A - f a else setsum f A)"
- apply (case_tac "finite A")
- prefer 2 apply (simp add: setsum_def)
- apply (erule finite_induct)
- apply (auto simp add: insert_Diff_if)
- apply (drule_tac a = a in mk_disjoint_insert, auto)
- done
-
lemma setsum_cong:
"A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
apply (case_tac "finite B")
@@ -865,12 +925,356 @@
apply (simp add: Ball_def del:insert_Diff_single)
done
-subsubsection{* Min and Max of finite linearly ordered sets *}
+lemma card_UN_disjoint:
+ fixes f :: "'a => 'b::plus_ac0"
+ shows
+ "finite I ==> (ALL i:I. finite (A i)) ==>
+ (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
+ card (UNION I A) = setsum (\<lambda>i. card (A i)) I"
+ apply (subst card_eq_setsum)
+ apply (subst finite_UN, assumption+)
+ apply (subgoal_tac "setsum (\<lambda>i. card (A i)) I =
+ setsum (%i. (setsum (%x. 1) (A i))) I")
+ apply (erule ssubst)
+ apply (erule setsum_UN_disjoint, assumption+)
+ apply (rule setsum_cong)
+ apply (simp, simp add: card_eq_setsum)
+ done
+
+lemma card_Union_disjoint:
+ "finite C ==> (ALL A:C. finite A) ==>
+ (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
+ card (Union C) = setsum card C"
+ apply (frule card_UN_disjoint [of C id])
+ apply (unfold Union_def id_def, assumption+)
+ done
+
+lemma setsum_0': "ALL a:F. f a = 0 ==> setsum f F = 0"
+ apply (subgoal_tac "setsum f F = setsum (%x. 0) F")
+ apply (erule ssubst, rule setsum_0)
+ apply (rule setsum_cong, auto)
+ done
+
+
+subsubsection {* Reindexing sums *}
+
+lemma setsum_reindex [rule_format]: "finite B ==>
+ inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B"
+apply (rule finite_induct, assumption, force)
+apply (rule impI, auto)
+apply (simp add: inj_on_def)
+apply (subgoal_tac "f x \<notin> f ` F")
+apply (subgoal_tac "finite (f ` F)")
+apply (auto simp add: setsum_insert)
+apply (simp add: inj_on_def)
+ done
+
+lemma setsum_reindex_id: "finite B ==> inj_on f B ==>
+ setsum f B = setsum id (f ` B)"
+by (auto simp add: setsum_reindex id_o)
+
+
+subsubsection {* Properties in more restricted classes of structures *}
+
+lemma setsum_eq_0_iff [simp]:
+ "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
+ by (induct set: Finites) auto
+
+lemma setsum_constant_nat:
+ "finite A ==> (\<Sum>x: A. y) = (card A) * y"
+ -- {* Later generalized to any semiring. *}
+ by (erule finite_induct, auto)
+
+lemma setsum_Un: "finite A ==> finite B ==>
+ (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
+ -- {* For the natural numbers, we have subtraction. *}
+ by (subst setsum_Un_Int [symmetric], auto)
+
+lemma setsum_Un_ring: "finite A ==> finite B ==>
+ (setsum f (A Un B) :: 'a :: ring) =
+ setsum f A + setsum f B - setsum f (A Int B)"
+ apply (subst setsum_Un_Int [symmetric], auto)
+ apply (simp add: compare_rls)
+ done
+
+lemma setsum_diff1: "(setsum f (A - {a}) :: nat) =
+ (if a:A then setsum f A - f a else setsum f A)"
+ apply (case_tac "finite A")
+ prefer 2 apply (simp add: setsum_def)
+ apply (erule finite_induct)
+ apply (auto simp add: insert_Diff_if)
+ apply (drule_tac a = a in mk_disjoint_insert, auto)
+ done
+
+lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::ring) A =
+ - setsum f A"
+ by (induct set: Finites, auto)
+
+lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::ring) - g x) A =
+ setsum f A - setsum g A"
+ by (simp add: diff_minus setsum_addf setsum_negf)
+
+lemma setsum_nonneg: "[| finite A;
+ \<forall>x \<in> A. (0::'a::ordered_semiring) \<le> f x |] ==>
+ 0 \<le> setsum f A";
+ apply (induct set: Finites, auto)
+ apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp)
+ apply (blast intro: add_mono)
+ done
+
+subsubsection {* Cardinality of Sigma and Cartesian product *}
+
+lemma SigmaI_insert: "y \<notin> A ==>
+ (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
+ by auto
+
+lemma card_cartesian_product_singleton [simp]: "finite A ==>
+ card({x} <*> A) = card(A)"
+ apply (subgoal_tac "inj_on (%y .(x,y)) A")
+ apply (frule card_image, assumption)
+ apply (subgoal_tac "(Pair x ` A) = {x} <*> A")
+ apply (auto simp add: inj_on_def)
+ done
+
+lemma card_SigmaI [rule_format,simp]: "finite A ==>
+ (ALL a:A. finite (B a)) -->
+ card (SIGMA x: A. B x) = (\<Sum>a: A. card (B a))"
+ apply (erule finite_induct, auto)
+ apply (subst SigmaI_insert, assumption)
+ apply (subst card_Un_disjoint)
+ apply (auto intro: finite_SigmaI)
+ done
+
+lemma card_cartesian_product [simp]: "[| finite A; finite B |] ==>
+ card (A <*> B) = card(A) * card(B)"
+ apply (subst card_SigmaI, assumption+)
+ apply (simp add: setsum_constant_nat)
+ done
+
+
+subsection {* Generalized product over a set *}
+
+constdefs
+ setprod :: "('a => 'b) => 'a set => 'b::times_ac1"
+ "setprod f A == if finite A then fold (op * o f) 1 A else 1"
+
+syntax
+ "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
+ ("\<Prod>_:_. _" [0, 51, 10] 10)
+
+syntax (xsymbols)
+ "_setprod" :: "idt => 'a set => 'b => 'b::plus_ac0"
+ ("\<Prod>_\<in>_. _" [0, 51, 10] 10)
+translations
+ "\<Prod>i:A. b" == "setprod (%i. b) A" -- {* Beware of argument permutation! *}
+
+
+lemma setprod_empty [simp]: "setprod f {} = 1"
+ by (auto simp add: setprod_def)
+
+lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
+ setprod f (insert a A) = f a * setprod f A"
+ by (auto simp add: setprod_def LC_def LC.fold_insert
+ times_ac1_left_commute)
+
+lemma setprod_1: "setprod (\<lambda>i. 1) A = 1"
+ apply (case_tac "finite A")
+ apply (erule finite_induct, auto simp add: times_ac1)
+ apply (simp add: setprod_def)
+ done
+
+lemma setprod_Un_Int: "finite A ==> finite B
+ ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
+ apply (induct set: Finites, simp)
+ apply (simp add: times_ac1 insert_absorb)
+ apply (simp add: times_ac1 Int_insert_left insert_absorb)
+ done
+
+lemma setprod_Un_disjoint: "finite A ==> finite B
+ ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
+ apply (subst setprod_Un_Int [symmetric], auto simp add: times_ac1)
+ done
+
+lemma setprod_UN_disjoint:
+ fixes f :: "'a => 'b::times_ac1"
+ shows
+ "finite I ==> (ALL i:I. finite (A i)) ==>
+ (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
+ setprod f (UNION I A) = setprod (\<lambda>i. setprod f (A i)) I"
+ apply (induct set: Finites, simp, atomize)
+ apply (subgoal_tac "ALL i:F. x \<noteq> i")
+ prefer 2 apply blast
+ apply (subgoal_tac "A x Int UNION F A = {}")
+ prefer 2 apply blast
+ apply (simp add: setprod_Un_disjoint)
+ done
+
+lemma setprod_Union_disjoint:
+ "finite C ==> (ALL A:C. finite A) ==>
+ (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
+ setprod f (Union C) = setprod (setprod f) C"
+ apply (frule setprod_UN_disjoint [of C id f])
+ apply (unfold Union_def id_def, assumption+)
+ done
+
+lemma setprod_timesf: "setprod (\<lambda>x. f x * g x) A =
+ (setprod f A * setprod g A)"
+ apply (case_tac "finite A")
+ prefer 2 apply (simp add: setprod_def times_ac1)
+ apply (erule finite_induct, auto)
+ apply (simp add: times_ac1)
+ apply (simp add: times_ac1)
+ done
+
+lemma setprod_cong:
+ "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
+ apply (case_tac "finite B")
+ prefer 2 apply (simp add: setprod_def, simp)
+ apply (subgoal_tac "ALL C. C <= B --> (ALL x:C. f x = g x) --> setprod f C = setprod g C")
+ apply simp
+ apply (erule finite_induct, simp)
+ apply (simp add: subset_insert_iff, clarify)
+ apply (subgoal_tac "finite C")
+ prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
+ apply (subgoal_tac "C = insert x (C - {x})")
+ prefer 2 apply blast
+ apply (erule ssubst)
+ apply (drule spec)
+ apply (erule (1) notE impE)
+ apply (simp add: Ball_def del:insert_Diff_single)
+ done
+
+lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1"
+ apply (subgoal_tac "setprod f F = setprod (%x. 1) F")
+ apply (erule ssubst, rule setprod_1)
+ apply (rule setprod_cong, auto)
+ done
+
+
+subsubsection {* Reindexing products *}
+
+lemma setprod_reindex [rule_format]: "finite B ==>
+ inj_on f B --> setprod h (f ` B) = setprod (h \<circ> f) B"
+apply (rule finite_induct, assumption, force)
+apply (rule impI, auto)
+apply (simp add: inj_on_def)
+apply (subgoal_tac "f x \<notin> f ` F")
+apply (subgoal_tac "finite (f ` F)")
+apply (auto simp add: setprod_insert)
+apply (simp add: inj_on_def)
+ done
+
+lemma setprod_reindex_id: "finite B ==> inj_on f B ==>
+ setprod f B = setprod id (f ` B)"
+by (auto simp add: setprod_reindex id_o)
+
+
+subsubsection {* Properties in more restricted classes of structures *}
+
+lemma setprod_eq_1_iff [simp]:
+ "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))"
+ by (induct set: Finites) auto
+
+lemma setprod_constant: "finite A ==> (\<Prod>x: A. (y::'a::ringpower)) =
+ y^(card A)"
+ apply (erule finite_induct)
+ apply (auto simp add: power_Suc)
+ done
+
+lemma setprod_zero: "finite A ==> EX x: A. f x = (0::'a::semiring) ==>
+ setprod f A = 0"
+ apply (induct set: Finites, force, clarsimp)
+ apply (erule disjE, auto)
+ done
+
+lemma setprod_nonneg [rule_format]: "(ALL x: A. (0::'a::ordered_ring) \<le> f x)
+ --> 0 \<le> setprod f A"
+ apply (case_tac "finite A")
+ apply (induct set: Finites, force, clarsimp)
+ apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force)
+ apply (rule mult_mono, assumption+)
+ apply (auto simp add: setprod_def)
+ done
+
+lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_ring) < f x)
+ --> 0 < setprod f A"
+ apply (case_tac "finite A")
+ apply (induct set: Finites, force, clarsimp)
+ apply (subgoal_tac "0 * 0 < f x * setprod f F", force)
+ apply (rule mult_strict_mono, assumption+)
+ apply (auto simp add: setprod_def)
+ done
+
+lemma setprod_nonzero [rule_format]:
+ "(ALL x y. (x::'a::semiring) * 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::semiring) * 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"
+ 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)"
+ apply (rule setprod_zero_eq, auto)
+ done
+
+lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
+ (setprod f (A Un B) :: 'a ::{field})
+ = setprod f A * setprod f B / setprod f (A Int B)"
+ apply (subst setprod_Un_Int [symmetric], auto)
+ apply (subgoal_tac "finite (A Int B)")
+ apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
+ apply (subst times_divide_eq_right [THEN sym], auto)
+ done
+
+lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
+ (setprod f (A - {a}) :: 'a :: {field}) =
+ (if a:A then setprod f A / f a else setprod f A)"
+ apply (erule finite_induct)
+ apply (auto simp add: insert_Diff_if)
+ apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a")
+ apply (erule ssubst)
+ apply (subst times_divide_eq_right [THEN sym])
+ apply (auto simp add: mult_ac)
+ done
+
+lemma setprod_inversef: "finite A ==>
+ ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
+ setprod (inverse \<circ> f) A = inverse (setprod f A)"
+ apply (erule finite_induct)
+ apply (simp, simp)
+ done
+
+lemma setprod_dividef:
+ "[|finite A;
+ \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|]
+ ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
+ apply (subgoal_tac
+ "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
+ apply (erule ssubst)
+ apply (subst divide_inverse)
+ apply (subst setprod_timesf)
+ apply (subst setprod_inversef, assumption+, rule refl)
+ apply (rule setprod_cong, rule refl)
+ apply (subst divide_inverse, auto)
+ done
+
+
+subsection{* Min and Max of finite linearly ordered sets *}
text{* Seemed easier to define directly than via fold. *}
lemma ex_Max: fixes S :: "('a::linorder)set"
- assumes fin: "finite S" shows "S \<noteq> {} \<Longrightarrow> \<exists>m\<in>S. \<forall>s \<in> S. s \<le> m"
+ assumes fin: "finite S" shows "S \<noteq> {} ==> \<exists>m\<in>S. \<forall>s \<in> S. s \<le> m"
using fin
proof (induct)
case empty thus ?case by simp
@@ -886,14 +1290,14 @@
proof (cases)
assume "x \<le> m" thus ?thesis using m by blast
next
- assume "\<not> x \<le> m" thus ?thesis using m
+ assume "~ x \<le> m" thus ?thesis using m
by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
qed
qed
qed
lemma ex_Min: fixes S :: "('a::linorder)set"
- assumes fin: "finite S" shows "S \<noteq> {} \<Longrightarrow> \<exists>m\<in>S. \<forall>s \<in> S. m \<le> s"
+ assumes fin: "finite S" shows "S \<noteq> {} ==> \<exists>m\<in>S. \<forall>s \<in> S. m \<le> s"
using fin
proof (induct)
case empty thus ?case by simp
@@ -909,18 +1313,18 @@
proof (cases)
assume "m \<le> x" thus ?thesis using m by blast
next
- assume "\<not> m \<le> x" thus ?thesis using m
+ assume "~ m \<le> x" thus ?thesis using m
by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
qed
qed
qed
constdefs
- Min :: "('a::linorder)set \<Rightarrow> 'a"
-"Min S \<equiv> THE m. m \<in> S \<and> (\<forall>s \<in> S. m \<le> s)"
+ Min :: "('a::linorder)set => 'a"
+"Min S == THE m. m \<in> S \<and> (\<forall>s \<in> S. m \<le> s)"
- Max :: "('a::linorder)set \<Rightarrow> 'a"
-"Max S \<equiv> THE m. m \<in> S \<and> (\<forall>s \<in> S. s \<le> m)"
+ Max :: "('a::linorder)set => 'a"
+"Max S == THE m. m \<in> S \<and> (\<forall>s \<in> S. s \<le> m)"
lemma Min[simp]: assumes a: "finite S" "S \<noteq> {}"
shows "Min S \<in> S \<and> (\<forall>s \<in> S. Min S \<le> s)" (is "?P(Min S)")
@@ -946,6 +1350,7 @@
qed
qed
+subsection {* Theorems about @{text "choose"} *}
text {*
\medskip Basic theorem about @{text "choose"}. By Florian
@@ -965,7 +1370,7 @@
apply safe
apply (auto intro: finite_subset [THEN card_insert_disjoint])
apply (drule_tac x = "xa - {x}" in spec)
- apply (subgoal_tac "x ~: xa", auto)
+ apply (subgoal_tac "x \<notin> xa", auto)
apply (erule rev_mp, subst card_Diff_singleton)
apply (auto intro: finite_subset)
done
@@ -974,8 +1379,8 @@
"[|inj_on f A; f ` A \<subseteq> B; finite A; finite B |] ==> card A <= card B"
by (auto intro: card_mono simp add: card_image [symmetric])
-lemma card_bij_eq:
- "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
+lemma card_bij_eq:
+ "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
finite A; finite B |] ==> card A = card B"
by (auto intro: le_anti_sym card_inj_on_le)
--- a/src/HOL/HOL.thy Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/HOL.thy Thu Mar 04 12:06:07 2004 +0100
@@ -197,11 +197,6 @@
syntax (HTML output)
abs :: "'a::minus => 'a" ("\<bar>_\<bar>")
-axclass plus_ac0 < plus, zero
- commute: "x + y = y + x"
- assoc: "(x + y) + z = x + (y + z)"
- zero: "0 + x = x"
-
subsection {* Theory and package setup *}
--- a/src/HOL/HOL_lemmas.ML Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/HOL_lemmas.ML Thu Mar 04 12:06:07 2004 +0100
@@ -446,21 +446,6 @@
by (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1)) ;
qed "exCI";
-Goal "x + (y+z) = y + ((x+z)::'a::plus_ac0)";
-by (rtac (thm"plus_ac0.commute" RS trans) 1);
-by (rtac (thm"plus_ac0.assoc" RS trans) 1);
-by (rtac (thm"plus_ac0.commute" RS arg_cong) 1);
-qed "plus_ac0_left_commute";
-
-Goal "x + 0 = (x ::'a::plus_ac0)";
-by (rtac (thm"plus_ac0.commute" RS trans) 1);
-by (rtac (thm"plus_ac0.zero") 1);
-qed "plus_ac0_zero_right";
-
-bind_thms ("plus_ac0", [thm"plus_ac0.assoc", thm"plus_ac0.commute",
- plus_ac0_left_commute,
- thm"plus_ac0.zero", plus_ac0_zero_right]);
-
(* case distinction *)
val [prem1,prem2] = Goal "[| P ==> Q; ~P ==> Q |] ==> Q";
--- a/src/HOL/Hyperreal/EvenOdd.ML Thu Mar 04 10:06:13 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,366 +0,0 @@
-(* Title : Even.ML
- Author : Jacques D. Fleuriot
- Copyright : 1999 University of Edinburgh
- Description : Even numbers defined
-*)
-
-Goal "even(Suc(Suc n)) = (even(n))";
-by (Auto_tac);
-qed "even_Suc_Suc";
-Addsimps [even_Suc_Suc];
-
-Goal "(even(n)) = (~odd(n))";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed "even_not_odd";
-
-Goal "(odd(n)) = (~even(n))";
-by (simp_tac (simpset() addsimps [even_not_odd]) 1);
-qed "odd_not_even";
-
-Goal "even(2*n)";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed "even_mult_two";
-Addsimps [even_mult_two];
-
-Goal "even(n*2)";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed "even_mult_two'";
-Addsimps [even_mult_two'];
-
-Goal "even(n + n)";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed "even_sum_self";
-Addsimps [even_sum_self];
-
-Goal "~odd(2*n)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "not_odd_self_mult2";
-Addsimps [not_odd_self_mult2];
-
-Goal "~odd(n + n)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "not_odd_sum_self";
-Addsimps [not_odd_sum_self];
-
-Goal "~even(Suc(n + n))";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "not_even_Suc_sum_self";
-Addsimps [not_even_Suc_sum_self];
-
-Goal "odd(Suc(2*n))";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed "odd_mult_two_add_one";
-Addsimps [odd_mult_two_add_one];
-
-Goal "odd(Suc(n + n))";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed "odd_sum_Suc_self";
-Addsimps [odd_sum_Suc_self];
-
-Goal "even(Suc n) = odd(n)";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed "even_Suc_odd_iff";
-
-Goal "odd(Suc n) = even(n)";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed "odd_Suc_even_iff";
-
-Goal "even n | odd n";
-by (simp_tac (simpset() addsimps [even_not_odd]) 1);
-qed "even_odd_disj";
-
-(* could be proved automatically before: spoiled by numeral arith! *)
-Goal "EX m. (n = 2*m | n = Suc(2*m))";
-by (induct_tac "n" 1 THEN Auto_tac);
-by (res_inst_tac [("x","Suc m")] exI 1 THEN Auto_tac);
-qed "nat_mult_two_Suc_disj";
-
-Goal "even(n) = (EX m. n = 2*m)";
-by (cut_inst_tac [("n","n")] nat_mult_two_Suc_disj 1);
-by (Auto_tac);
-qed "even_mult_two_ex";
-
-Goal "odd(n) = (EX m. n = Suc (2*m))";
-by (cut_inst_tac [("n","n")] nat_mult_two_Suc_disj 1);
-by (Auto_tac);
-qed "odd_Suc_mult_two_ex";
-
-Goal "even(n) ==> even(m*n)";
-by (auto_tac (claset(),
- simpset() addsimps [add_mult_distrib2, even_mult_two_ex]));
-qed "even_mult_even";
-Addsimps [even_mult_even];
-
-Goal "(m + m) div 2 = (m::nat)";
-by (arith_tac 1);
-qed "div_add_self_two_is_m";
-Addsimps [div_add_self_two_is_m];
-
-Goal "Suc(Suc(m*2)) div 2 = Suc m";
-by (arith_tac 1);
-qed "div_mult_self_Suc_Suc";
-Addsimps [div_mult_self_Suc_Suc];
-
-Goal "Suc(Suc(2*m)) div 2 = Suc m";
-by (arith_tac 1);
-qed "div_mult_self_Suc_Suc2";
-Addsimps [div_mult_self_Suc_Suc2];
-
-Goal "Suc(Suc(m + m)) div 2 = Suc m";
-by (arith_tac 1);
-qed "div_add_self_Suc_Suc";
-Addsimps [div_add_self_Suc_Suc];
-
-Goal "~ even n ==> (Suc n) div 2 = Suc((n - 1) div 2)";
-by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym,
- odd_Suc_mult_two_ex]));
-qed "not_even_imp_Suc_Suc_diff_one_eq";
-Addsimps [not_even_imp_Suc_Suc_diff_one_eq];
-
-Goal "even(m + n) = (even m = even n)";
-by (induct_tac "m" 1);
-by Auto_tac;
-qed "even_add";
-AddIffs [even_add];
-
-Goal "even(m * n) = (even m | even n)";
-by (induct_tac "m" 1);
-by Auto_tac;
-qed "even_mult";
-
-Goal "even (m ^ n) = (even m & n ~= 0)";
-by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps [even_mult]));
-qed "even_pow";
-AddIffs [even_pow];
-
-Goal "odd(m + n) = (odd m ~= odd n)";
-by (induct_tac "m" 1);
-by Auto_tac;
-qed "odd_add";
-AddIffs [odd_add];
-
-Goal "odd(m * n) = (odd m & odd n)";
-by (induct_tac "m" 1);
-by Auto_tac;
-qed "odd_mult";
-AddIffs [odd_mult];
-
-Goal "odd (m ^ n) = (odd m | n = 0)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "odd_pow";
-
-Goal "0 < n --> ~even (n + n - 1)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed_spec_mp "not_even_2n_minus_1";
-Addsimps [not_even_2n_minus_1];
-
-Goal "Suc (2 * m) mod 2 = 1";
-by (induct_tac "m" 1);
-by (auto_tac (claset(),simpset() addsimps [mod_Suc]));
-qed "mod_two_Suc_2m";
-Addsimps [mod_two_Suc_2m];
-
-Goal "(Suc (Suc (2 * m)) div 2) = Suc m";
-by (arith_tac 1);
-qed "div_two_Suc_Suc_2m";
-Addsimps [div_two_Suc_Suc_2m];
-
-Goal "even n ==> 2 * ((n + 1) div 2) = n";
-by (auto_tac (claset(),simpset() addsimps [mult_div_cancel,
- even_mult_two_ex]));
-qed "lemma_even_div";
-Addsimps [lemma_even_div];
-
-Goal "~even n ==> 2 * ((n + 1) div 2) = Suc n";
-by (auto_tac (claset(),simpset() addsimps [even_not_odd,
- odd_Suc_mult_two_ex]));
-qed "lemma_not_even_div";
-Addsimps [lemma_not_even_div];
-
-Goal "Suc n div 2 <= Suc (Suc n) div 2";
-by (arith_tac 1);
-qed "Suc_n_le_Suc_Suc_n_div_2";
-Addsimps [Suc_n_le_Suc_Suc_n_div_2];
-
-Goal "(0::nat) < n --> 0 < (n + 1) div 2";
-by (arith_tac 1);
-qed_spec_mp "Suc_n_div_2_gt_zero";
-Addsimps [Suc_n_div_2_gt_zero];
-
-Goal "0 < n & even n --> 1 < n";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed_spec_mp "even_gt_zero_gt_one_aux";
-bind_thm ("even_gt_zero_gt_one",conjI RS even_gt_zero_gt_one_aux);
-
-(* more general *)
-Goal "n div 2 <= (Suc n) div 2";
-by (arith_tac 1);
-qed "le_Suc_n_div_2";
-Addsimps [le_Suc_n_div_2];
-
-Goal "(1::nat) < n --> 0 < n div 2";
-by (arith_tac 1);
-qed_spec_mp "div_2_gt_zero";
-Addsimps [div_2_gt_zero];
-
-Goal "even n ==> (n + 1) div 2 = n div 2";
-by (rtac (CLAIM "2 * x = 2 * y ==> x = (y::nat)") 1);
-by (stac lemma_even_div 1);
-by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex]));
-qed "lemma_even_div2";
-Addsimps [lemma_even_div2];
-
-Goal "~even n ==> (n + 1) div 2 = Suc (n div 2)";
-by (rtac (CLAIM "2 * x = 2 * y ==> x = (y::nat)") 1);
-by (stac lemma_not_even_div 1);
-by (auto_tac (claset(),simpset() addsimps [even_not_odd,
- odd_Suc_mult_two_ex]));
-by (cut_inst_tac [("m","Suc(2*m)"),("n","2")] mod_div_equality 1);
-by Auto_tac;
-qed "lemma_not_even_div2";
-Addsimps [lemma_not_even_div2];
-
-Goal "(Suc n) div 2 = 0 ==> even n";
-by (rtac ccontr 1);
-by (dtac lemma_not_even_div2 1 THEN Auto_tac);
-qed "Suc_n_div_two_zero_even";
-
-Goal "0 < n ==> even n = (~ even(n - 1))";
-by (case_tac "n" 1);
-by Auto_tac;
-qed "even_num_iff";
-
-Goal "0 < n ==> odd n = (~ odd(n - 1))";
-by (case_tac "n" 1);
-by Auto_tac;
-qed "odd_num_iff";
-
-(* Some mod and div stuff *)
-
-Goal "n ~= (0::nat) ==> (m = m div n * n + m mod n) & m mod n < n";
-by (auto_tac (claset() addIs [mod_less_divisor],simpset()));
-qed "mod_div_eq_less";
-
-Goal "(k*n + m) mod n = m mod (n::nat)";
-by (simp_tac (simpset() addsimps mult_ac @ add_ac) 1);
-qed "mod_mult_self3";
-Addsimps [mod_mult_self3];
-
-Goal "Suc (k*n + m) mod n = Suc m mod n";
-by (rtac (CLAIM "Suc (m + n) = (m + Suc n)" RS ssubst) 1);
-by (rtac mod_mult_self3 1);
-qed "mod_mult_self4";
-Addsimps [mod_mult_self4];
-
-Goal "Suc m mod n = Suc (m mod n) mod n";
-by (cut_inst_tac [("d'","Suc (m mod n) mod n")] (CLAIM "EX d. d' = d") 1);
-by (etac exE 1);
-by (Asm_simp_tac 1);
-by (res_inst_tac [("t","m"),("n1","n")] (mod_div_equality RS subst) 1);
-by (auto_tac (claset(),simpset() delsimprocs [cancel_div_mod_proc]));
-qed "mod_Suc_eq_Suc_mod";
-
-Goal "even n = (even (n mod 4))";
-by (cut_inst_tac [("d'","(even (n mod 4))")] (CLAIM "EX d. d' = d") 1);
-by (etac exE 1);
-by (Asm_simp_tac 1);
-by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
-by (auto_tac (claset(),simpset() addsimps [even_mult,even_num_iff] delsimprocs [cancel_div_mod_proc]));
-qed "even_even_mod_4_iff";
-
-Goal "odd n = (odd (n mod 4))";
-by (auto_tac (claset(),simpset() addsimps [odd_not_even,
- even_even_mod_4_iff RS sym]));
-qed "odd_odd_mod_4_iff";
-
-Goal "odd n ==> ((-1) ^ n) = (-1::real)";
-by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
-qed "odd_realpow_minus_one";
-Addsimps [odd_realpow_minus_one];
-
-Goal "even(4*n)";
-by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex]));
-qed "even_4n";
-Addsimps [even_4n];
-
-Goal "n mod 4 = 0 ==> even(n div 2)";
-by Auto_tac;
-qed "lemma_even_div_2";
-
-Goal "n mod 4 = 0 ==> even(n)";
-by Auto_tac;
-qed "lemma_mod_4_even_n";
-
-Goal "n mod 4 = 1 ==> odd(n)";
-by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
-by (auto_tac (claset(),simpset() addsimps [odd_num_iff] delsimprocs [cancel_div_mod_proc]));
-qed "lemma_mod_4_odd_n";
-
-Goal "n mod 4 = 2 ==> even(n)";
-by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
-by (auto_tac (claset(),simpset() addsimps [even_num_iff] delsimprocs [cancel_div_mod_proc]));
-qed "lemma_mod_4_even_n2";
-
-Goal "n mod 4 = 3 ==> odd(n)";
-by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
-by (auto_tac (claset(),simpset() addsimps [odd_num_iff] delsimprocs [cancel_div_mod_proc]));
-qed "lemma_mod_4_odd_n2";
-
-Goal "even n ==> ((-1) ^ n) = (1::real)";
-by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex]));
-qed "even_realpow_minus_one";
-Addsimps [even_realpow_minus_one];
-
-Goal "((4 * n) + 2) div 2 = (2::nat) * n + 1";
-by (arith_tac 1);
-qed "lemma_4n_add_2_div_2_eq";
-Addsimps [lemma_4n_add_2_div_2_eq];
-
-Goal "(Suc(Suc(4 * n))) div 2 = (2::nat) * n + 1";
-by (arith_tac 1);
-qed "lemma_Suc_Suc_4n_div_2_eq";
-Addsimps [lemma_Suc_Suc_4n_div_2_eq];
-
-Goal "(Suc(Suc(n * 4))) div 2 = (2::nat) * n + 1";
-by (arith_tac 1);
-qed "lemma_Suc_Suc_4n_div_2_eq2";
-Addsimps [lemma_Suc_Suc_4n_div_2_eq2];
-
-Goal "n mod 4 = 3 ==> odd((n - 1) div 2)";
-by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
-by (asm_full_simp_tac (simpset() addsimps [odd_num_iff] delsimprocs [cancel_div_mod_proc]) 1);
-val lemma_odd_mod_4_div_2 = result();
-
-Goal "(4 * n) div 2 = (2::nat) * n";
-by (arith_tac 1);
-qed "lemma_4n_div_2_eq";
-Addsimps [lemma_4n_div_2_eq];
-
-Goal "(n * 4) div 2 = (2::nat) * n";
-by (arith_tac 1);
-qed "lemma_4n_div_2_eq2";
-Addsimps [lemma_4n_div_2_eq2];
-
-Goal "n mod 4 = 1 ==> even ((n - 1) div 2)";
-by (res_inst_tac [("t","n"),("n1","4")] (mod_div_equality RS subst) 1);
-by (dtac ssubst 1 THEN assume_tac 2);
-by (rtac ((CLAIM "(n::nat) + 1 - 1 = n") RS ssubst) 1);
-by Auto_tac;
-val lemma_even_mod_4_div_2 = result();
-
-
--- a/src/HOL/Hyperreal/EvenOdd.thy Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Hyperreal/EvenOdd.thy Thu Mar 04 12:06:07 2004 +0100
@@ -4,17 +4,163 @@
Description : Even and odd numbers defined
*)
-EvenOdd = NthRoot +
+header{*Compatibility file from Parity*}
+
+theory EvenOdd = NthRoot:
+
+subsection{*General Lemmas About Division*}
+
+lemma div_add_self_two_is_m: "(m + m) div 2 = (m::nat)"
+by arith
+declare div_add_self_two_is_m [simp]
+
+lemma div_mult_self_Suc_Suc: "Suc(Suc(m*2)) div 2 = Suc m"
+by arith
+declare div_mult_self_Suc_Suc [simp]
+
+lemma div_mult_self_Suc_Suc2: "Suc(Suc(2*m)) div 2 = Suc m"
+by arith
+declare div_mult_self_Suc_Suc2 [simp]
+
+lemma div_add_self_Suc_Suc: "Suc(Suc(m + m)) div 2 = Suc m"
+by arith
+declare div_add_self_Suc_Suc [simp]
+
+lemma mod_two_Suc_2m: "Suc (2 * m) mod 2 = 1"
+apply (induct_tac "m")
+apply (auto simp add: mod_Suc)
+done
+declare mod_two_Suc_2m [simp]
+
+lemma Suc_n_le_Suc_Suc_n_div_2: "Suc n div 2 \<le> Suc (Suc n) div 2"
+by arith
+declare Suc_n_le_Suc_Suc_n_div_2 [simp]
+
+lemma Suc_n_div_2_gt_zero: "(0::nat) < n ==> 0 < (n + 1) div 2"
+by arith
+declare Suc_n_div_2_gt_zero [simp]
+
+lemma le_Suc_n_div_2: "n div 2 \<le> (Suc n) div 2"
+by arith
+declare le_Suc_n_div_2 [simp]
+
+lemma div_2_gt_zero: "(1::nat) < n ==> 0 < n div 2"
+by arith
+declare div_2_gt_zero [simp]
+
+lemma mod_mult_self3: "(k*n + m) mod n = m mod (n::nat)"
+by (simp add: mult_ac add_ac)
+declare mod_mult_self3 [simp]
+
+lemma mod_mult_self4: "Suc (k*n + m) mod n = Suc m mod n"
+proof -
+ have "Suc (k * n + m) mod n = (k * n + Suc m) mod n" by simp
+ also have "... = Suc m mod n" by (rule mod_mult_self3)
+ finally show ?thesis .
+qed
+declare mod_mult_self4 [simp]
+
+lemma nat_mod_idem [simp]: "m mod n mod n = (m mod n :: nat)"
+by (case_tac "n=0", auto)
+
+lemma mod_Suc_eq_Suc_mod: "Suc m mod n = Suc (m mod n) mod n"
+apply (subst mod_Suc [of m])
+apply (subst mod_Suc [of "m mod n"], simp)
+done
+
+lemma lemma_4n_add_2_div_2_eq: "((4 * n) + 2) div 2 = (2::nat) * n + 1"
+by arith
+declare lemma_4n_add_2_div_2_eq [simp]
+
+lemma lemma_Suc_Suc_4n_div_2_eq: "(Suc(Suc(4 * n))) div 2 = (2::nat) * n + 1"
+by arith
+declare lemma_Suc_Suc_4n_div_2_eq [simp]
+
+lemma lemma_Suc_Suc_4n_div_2_eq2: "(Suc(Suc(n * 4))) div 2 = (2::nat) * n + 1"
+by arith
+declare lemma_Suc_Suc_4n_div_2_eq2 [simp]
+
-consts even :: "nat => bool"
-primrec
- even_0 "even 0 = True"
- even_Suc "even (Suc n) = (~ (even n))"
+subsection{*More Even/Odd Results*}
+
+lemma even_mult_two_ex: "even(n) = (EX m::nat. n = 2*m)"
+by (simp add: even_nat_equiv_def2 numeral_2_eq_2)
+
+lemma odd_Suc_mult_two_ex: "odd(n) = (EX m. n = Suc (2*m))"
+by (simp add: odd_nat_equiv_def2 numeral_2_eq_2)
+
+lemma even_add: "even(m + n::nat) = (even m = even n)"
+by auto
+declare even_add [iff]
+
+lemma odd_add: "odd(m + n::nat) = (odd m ~= odd n)"
+by auto
+declare odd_add [iff]
+
+lemma lemma_even_div2: "even (n::nat) ==> (n + 1) div 2 = n div 2"
+apply (simp add: numeral_2_eq_2)
+apply (subst div_Suc)
+apply (simp add: even_nat_mod_two_eq_zero)
+done
+declare lemma_even_div2 [simp]
+
+lemma lemma_not_even_div2: "~even n ==> (n + 1) div 2 = Suc (n div 2)"
+apply (simp add: numeral_2_eq_2)
+apply (subst div_Suc)
+apply (simp add: odd_nat_mod_two_eq_one)
+done
+declare lemma_not_even_div2 [simp]
+
+lemma even_num_iff: "0 < n ==> even n = (~ even(n - 1 :: nat))"
+by (case_tac "n", auto)
+
+lemma even_even_mod_4_iff: "even (n::nat) = even (n mod 4)"
+apply (induct n, simp)
+apply (subst mod_Suc, simp)
+done
-consts odd :: "nat => bool"
-primrec
- odd_0 "odd 0 = False"
- odd_Suc "odd (Suc n) = (~ (odd n))"
+declare neg_one_odd_power [simp]
+declare neg_one_even_power [simp]
+
+lemma lemma_odd_mod_4_div_2: "n mod 4 = (3::nat) ==> odd((n - 1) div 2)"
+apply (rule_tac t = n and n1 = 4 in mod_div_equality [THEN subst])
+apply (simp add: even_num_iff)
+done
+
+lemma lemma_even_mod_4_div_2: "n mod 4 = (1::nat) ==> even ((n - 1) div 2)"
+by (rule_tac t = n and n1 = 4 in mod_div_equality [THEN subst], simp)
+
+ML
+{*
+val even_Suc = thm"Parity.even_nat_suc";
+
+val even_mult_two_ex = thm "even_mult_two_ex";
+val odd_Suc_mult_two_ex = thm "odd_Suc_mult_two_ex";
+val div_add_self_two_is_m = thm "div_add_self_two_is_m";
+val div_mult_self_Suc_Suc = thm "div_mult_self_Suc_Suc";
+val div_mult_self_Suc_Suc2 = thm "div_mult_self_Suc_Suc2";
+val div_add_self_Suc_Suc = thm "div_add_self_Suc_Suc";
+val even_add = thm "even_add";
+val odd_add = thm "odd_add";
+val mod_two_Suc_2m = thm "mod_two_Suc_2m";
+val Suc_n_le_Suc_Suc_n_div_2 = thm "Suc_n_le_Suc_Suc_n_div_2";
+val Suc_n_div_2_gt_zero = thm "Suc_n_div_2_gt_zero";
+val le_Suc_n_div_2 = thm "le_Suc_n_div_2";
+val div_2_gt_zero = thm "div_2_gt_zero";
+val lemma_even_div2 = thm "lemma_even_div2";
+val lemma_not_even_div2 = thm "lemma_not_even_div2";
+val even_num_iff = thm "even_num_iff";
+val mod_mult_self3 = thm "mod_mult_self3";
+val mod_mult_self4 = thm "mod_mult_self4";
+val nat_mod_idem = thm "nat_mod_idem";
+val mod_Suc_eq_Suc_mod = thm "mod_Suc_eq_Suc_mod";
+val even_even_mod_4_iff = thm "even_even_mod_4_iff";
+val lemma_4n_add_2_div_2_eq = thm "lemma_4n_add_2_div_2_eq";
+val lemma_Suc_Suc_4n_div_2_eq = thm "lemma_Suc_Suc_4n_div_2_eq";
+val lemma_Suc_Suc_4n_div_2_eq2 = thm "lemma_Suc_Suc_4n_div_2_eq2";
+val lemma_odd_mod_4_div_2 = thm "lemma_odd_mod_4_div_2";
+val lemma_even_mod_4_div_2 = thm "lemma_even_mod_4_div_2";
+*}
end
--- a/src/HOL/Hyperreal/HLog.thy Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Hyperreal/HLog.thy Thu Mar 04 12:06:07 2004 +0100
@@ -57,7 +57,7 @@
lemma hypreal_divide:
"(Abs_hypreal(hyprel `` {X}))/(Abs_hypreal(hyprel `` {Y})) =
(Abs_hypreal(hyprel `` {%n. (X n)/(Y n)}))"
-by (simp add: divide_inverse_zero hypreal_zero_num hypreal_inverse hypreal_mult)
+by (simp add: divide_inverse hypreal_zero_num hypreal_inverse hypreal_mult)
lemma powhr_divide:
"[| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)"
@@ -96,7 +96,7 @@
done
lemma powhr_minus_divide: "x powhr (-a) = 1/(x powhr a)"
-by (simp add: divide_inverse_zero powhr_minus)
+by (simp add: divide_inverse powhr_minus)
lemma powhr_less_mono: "[| a < b; 1 < x |] ==> x powhr a < x powhr b"
apply (rule eq_Abs_hypreal [of x])
@@ -194,7 +194,7 @@
apply (auto intro!: starfun_ln_HFinite_not_Infinitesimal
HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2
simp add: starfun_ln_HInfinite not_Infinitesimal_not_zero
- hlog_as_starfun hypreal_not_refl2 [THEN not_sym] divide_inverse_zero)
+ hlog_as_starfun hypreal_not_refl2 [THEN not_sym] divide_inverse)
done
lemma hlog_HInfinite_as_starfun:
@@ -220,7 +220,7 @@
lemma hlog_divide:
"[| 0 < a; a \<noteq> 1; 0 < x; 0 < y|] ==> hlog a (x/y) = hlog a x - hlog a y"
-by (simp add: hlog_mult hlog_inverse divide_inverse_zero)
+by (simp add: hlog_mult hlog_inverse divide_inverse)
lemma hlog_less_cancel_iff [simp]:
"[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x < hlog a y) = (x < y)"
--- a/src/HOL/Hyperreal/HTranscendental.thy Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Hyperreal/HTranscendental.thy Thu Mar 04 12:06:07 2004 +0100
@@ -555,13 +555,13 @@
"n \<in> HNatInfinite
==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n @= 1"
apply (frule lemma_sin_pi)
-apply (simp add: divide_inverse_zero)
+apply (simp add: divide_inverse)
done
lemma Infinitesimal_pi_divide_HNatInfinite:
"N \<in> HNatInfinite
==> hypreal_of_real pi/(hypreal_of_hypnat N) \<in> Infinitesimal"
-apply (simp add: divide_inverse_zero)
+apply (simp add: divide_inverse)
apply (auto intro: Infinitesimal_HFinite_mult2)
done
@@ -578,7 +578,7 @@
pi_divide_HNatInfinite_not_zero])
apply (auto simp add: hypreal_inverse_distrib)
apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"])
-apply (auto intro: SReal_inverse simp add: divide_inverse_zero mult_ac)
+apply (auto intro: SReal_inverse simp add: divide_inverse mult_ac)
done
lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2:
@@ -593,7 +593,7 @@
lemma starfunNat_pi_divide_n_Infinitesimal:
"N \<in> HNatInfinite ==> ( *fNat* (%x. pi / real x)) N \<in> Infinitesimal"
by (auto intro!: Infinitesimal_HFinite_mult2
- simp add: starfunNat_mult [symmetric] divide_inverse_zero
+ simp add: starfunNat_mult [symmetric] divide_inverse
starfunNat_inverse [symmetric] starfunNat_real_of_nat)
lemma STAR_sin_pi_divide_n_approx:
@@ -601,16 +601,16 @@
( *f* sin) (( *fNat* (%x. pi / real x)) N) @=
hypreal_of_real pi/(hypreal_of_hypnat N)"
by (auto intro!: STAR_sin_Infinitesimal Infinitesimal_HFinite_mult2
- simp add: starfunNat_mult [symmetric] divide_inverse_zero
+ simp add: starfunNat_mult [symmetric] divide_inverse
starfunNat_inverse_real_of_nat_eq)
lemma NSLIMSEQ_sin_pi: "(%n. real n * sin (pi / real n)) ----NS> pi"
apply (auto simp add: NSLIMSEQ_def starfunNat_mult [symmetric] starfunNat_real_of_nat)
apply (rule_tac f1 = sin in starfun_stafunNat_o2 [THEN subst])
-apply (auto simp add: starfunNat_mult [symmetric] starfunNat_real_of_nat divide_inverse_zero)
+apply (auto simp add: starfunNat_mult [symmetric] starfunNat_real_of_nat divide_inverse)
apply (rule_tac f1 = inverse in starfun_stafunNat_o2 [THEN subst])
apply (auto dest: STAR_sin_pi_divide_HNatInfinite_approx_pi
- simp add: starfunNat_real_of_nat mult_commute divide_inverse_zero)
+ simp add: starfunNat_real_of_nat mult_commute divide_inverse)
done
lemma NSLIMSEQ_cos_one: "(%n. cos (pi / real n))----NS> 1"
@@ -618,7 +618,7 @@
apply (rule_tac f1 = cos in starfun_stafunNat_o2 [THEN subst])
apply (rule STAR_cos_Infinitesimal)
apply (auto intro!: Infinitesimal_HFinite_mult2
- simp add: starfunNat_mult [symmetric] divide_inverse_zero
+ simp add: starfunNat_mult [symmetric] divide_inverse
starfunNat_inverse [symmetric] starfunNat_real_of_nat)
done
--- a/src/HOL/Hyperreal/HyperDef.thy Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy Thu Mar 04 12:06:07 2004 +0100
@@ -476,17 +476,14 @@
show "(x + y) * z = x * z + y * z" by (simp add: hypreal_add_mult_distrib)
show "0 \<noteq> (1::hypreal)" by (rule hypreal_zero_not_eq_one)
show "x \<noteq> 0 ==> inverse x * x = 1" by (simp add: hypreal_mult_inverse_left)
- show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: hypreal_divide_def)
+ show "x / y = x * inverse y" by (simp add: hypreal_divide_def)
qed
instance hypreal :: division_by_zero
proof
- fix x :: hypreal
- show inv: "inverse 0 = (0::hypreal)"
+ show "inverse 0 = (0::hypreal)"
by (simp add: hypreal_inverse hypreal_zero_def)
- show "x/0 = 0"
- by (simp add: hypreal_divide_def inv hypreal_mult_commute [of a])
qed
--- a/src/HOL/Hyperreal/Log.thy Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Hyperreal/Log.thy Thu Mar 04 12:06:07 2004 +0100
@@ -41,7 +41,7 @@
lemma powr_divide:
"[| 0 < x; 0 < y |] ==> (x / y) powr a = (x powr a)/(y powr a)"
-apply (simp add: divide_inverse_zero positive_imp_inverse_positive powr_mult)
+apply (simp add: divide_inverse positive_imp_inverse_positive powr_mult)
apply (simp add: powr_def exp_minus [symmetric] exp_add [symmetric] ln_inverse)
done
@@ -58,7 +58,7 @@
by (simp add: powr_def exp_minus [symmetric])
lemma powr_minus_divide: "x powr (-a) = 1/(x powr a)"
-by (simp add: divide_inverse_zero powr_minus)
+by (simp add: divide_inverse powr_minus)
lemma powr_less_mono: "[| a < b; 1 < x |] ==> x powr a < x powr b"
by (simp add: powr_def)
@@ -85,12 +85,12 @@
lemma log_mult:
"[| 0 < a; a \<noteq> 1; 0 < x; 0 < y |]
==> log a (x * y) = log a x + log a y"
-by (simp add: log_def ln_mult divide_inverse_zero left_distrib)
+by (simp add: log_def ln_mult divide_inverse left_distrib)
lemma log_eq_div_ln_mult_log:
"[| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |]
==> log a x = (ln b/ln a) * log b x"
-by (simp add: log_def divide_inverse_zero)
+by (simp add: log_def divide_inverse)
text{*Base 10 logarithms*}
lemma log_base_10_eq1: "0 < x ==> log 10 x = (ln (exp 1) / ln 10) * ln x"
@@ -113,7 +113,7 @@
lemma log_divide:
"[|0 < a; a \<noteq> 1; 0 < x; 0 < y|] ==> log a (x/y) = log a x - log a y"
-by (simp add: log_mult divide_inverse_zero log_inverse)
+by (simp add: log_mult divide_inverse log_inverse)
lemma log_less_cancel_iff [simp]:
"[| 1 < a; 0 < x; 0 < y |] ==> (log a x < log a y) = (x < y)"
--- a/src/HOL/Hyperreal/MacLaurin.ML Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Hyperreal/MacLaurin.ML Thu Mar 04 12:06:07 2004 +0100
@@ -535,9 +535,9 @@
by (res_inst_tac [("x","t")] exI 1);
by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
by (rtac sumr_fun_eq 1);
-by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
-by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
- even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
+by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
+by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
+(*Could sin_zero_iff help?*)
qed "Maclaurin_sin_expansion";
Goal "EX t. abs t <= abs x & \
@@ -566,9 +566,8 @@
by (arith_tac 1);
by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
by (rtac sumr_fun_eq 1);
-by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
-by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
- even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
+by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
+by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
qed "Maclaurin_sin_expansion2";
Goal "[| 0 < n; 0 < x |] ==> \
@@ -590,9 +589,8 @@
by (assume_tac 1 THEN assume_tac 1);
by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
by (rtac sumr_fun_eq 1);
-by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
-by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
- even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
+by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
+by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
qed "Maclaurin_sin_expansion3";
Goal "0 < x ==> \
@@ -614,9 +612,8 @@
by (assume_tac 1 THEN assume_tac 1);
by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
by (rtac sumr_fun_eq 1);
-by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
-by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
- even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
+by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
+by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex] delsimps [fact_Suc,realpow_Suc]));
qed "Maclaurin_sin_expansion4";
(*-----------------------------------------------------------------------------*)
@@ -658,9 +655,8 @@
by (arith_tac 1);
by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
by (rtac sumr_fun_eq 1);
-by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
-by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
- even_mult_two_ex,left_distrib,cos_add] delsimps
+by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
+by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex,left_distrib,cos_add] delsimps
[fact_Suc,realpow_Suc]));
by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));
qed "Maclaurin_cos_expansion";
@@ -685,10 +681,8 @@
by (assume_tac 1 THEN assume_tac 1);
by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
by (rtac sumr_fun_eq 1);
-by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
-by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
- even_mult_two_ex,left_distrib,cos_add] delsimps
- [fact_Suc,realpow_Suc]));
+by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
+by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex,left_distrib,cos_add] delsimps [fact_Suc,realpow_Suc]));
by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));
qed "Maclaurin_cos_expansion2";
@@ -712,10 +706,8 @@
by (assume_tac 1 THEN assume_tac 1);
by (rtac (CLAIM "[|x = y; x' = y'|] ==> x + x' = y + (y'::real)") 1);
by (rtac sumr_fun_eq 1);
-by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym]));
-by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex,
- even_mult_two_ex,left_distrib,cos_add] delsimps
- [fact_Suc,realpow_Suc]));
+by (auto_tac (claset(),simpset() addsimps [odd_Suc_mult_two_ex]));
+by (auto_tac (claset(),simpset() addsimps [even_mult_two_ex,left_distrib,cos_add] delsimps [fact_Suc,realpow_Suc]));
by (auto_tac (claset(),simpset() addsimps [real_mult_commute]));
qed "Maclaurin_minus_cos_expansion";
--- a/src/HOL/Hyperreal/NSA.thy Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Hyperreal/NSA.thy Thu Mar 04 12:06:07 2004 +0100
@@ -914,7 +914,7 @@
lemma Infinitesimal_SReal_divide:
"[| x \<in> Infinitesimal; y \<in> Reals |] ==> x/y \<in> Infinitesimal"
-apply (simp add: divide_inverse_zero)
+apply (simp add: divide_inverse)
apply (auto intro!: Infinitesimal_HFinite_mult
dest!: SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
done
--- a/src/HOL/Hyperreal/Transcendental.ML Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Hyperreal/Transcendental.ML Thu Mar 04 12:06:07 2004 +0100
@@ -830,7 +830,6 @@
by Auto_tac;
qed "sin_fdiffs2";
-(* thms in EvenOdd needed *)
Goalw [diffs_def,real_divide_def]
"diffs(%n. if even n then \
\ (- 1) ^ (n div 2)/(real (fact n)) else 0) \
@@ -841,11 +840,11 @@
by (stac real_of_nat_mult 1);
by (stac even_Suc 1);
by (stac inverse_mult_distrib 1);
-by (res_inst_tac [("z1","real (Suc n)")] (real_mult_commute RS ssubst) 1);
-by (res_inst_tac [("z1","inverse(real (Suc n))")]
- (real_mult_commute RS ssubst) 1);
+by (res_inst_tac [("a1","real (Suc n)")] (mult_commute RS ssubst) 1);
+by (res_inst_tac [("a1","inverse(real (Suc n))")]
+ (mult_commute RS ssubst) 1);
by (auto_tac (claset(),simpset() addsimps [real_mult_assoc,
- odd_not_even RS sym,odd_Suc_mult_two_ex]));
+ odd_Suc_mult_two_ex]));
qed "cos_fdiffs";
@@ -862,7 +861,7 @@
by (res_inst_tac [("z1","inverse (real (Suc n))")]
(real_mult_commute RS ssubst) 1);
by (auto_tac (claset(),simpset() addsimps [real_mult_assoc,
- odd_not_even RS sym,odd_Suc_mult_two_ex]));
+ odd_Suc_mult_two_ex]));
qed "cos_fdiffs2";
(* ------------------------------------------------------------------------ *)
@@ -1949,7 +1948,7 @@
(* Pre Isabelle99-2 proof was simpler- numerals arithmetic
now causes some unwanted re-arrangements of literals! *)
Goal "[| 0 <= x; cos x = 0 |] ==> \
-\ EX n. ~even n & x = real n * (pi/2)";
+\ EX n::nat. ~even n & x = real n * (pi/2)";
by (dtac (pi_gt_zero RS reals_Archimedean4) 1);
by (Step_tac 1);
by (subgoal_tac
@@ -1973,7 +1972,7 @@
qed "cos_zero_lemma";
Goal "[| 0 <= x; sin x = 0 |] ==> \
-\ EX n. even n & x = real n * (pi/2)";
+\ EX n::nat. even n & x = real n * (pi/2)";
by (subgoal_tac
"EX n. ~ even n & x + pi/2 = real n * (pi/2)" 1);
by (rtac cos_zero_lemma 2);
@@ -1981,15 +1980,15 @@
by (res_inst_tac [("x","n - 1")] exI 1);
by (rtac (CLAIM "-y <= x ==> -x <= (y::real)") 2);
by (rtac real_le_trans 2 THEN assume_tac 3);
-by (auto_tac (claset(),simpset() addsimps [odd_not_even RS sym,
+by (auto_tac (claset(),simpset() addsimps [
odd_Suc_mult_two_ex,real_of_nat_Suc,
left_distrib,real_mult_assoc RS sym]));
qed "sin_zero_lemma";
(* also spoilt by numeral arithmetic *)
Goal "(cos x = 0) = \
-\ ((EX n. ~even n & (x = real n * (pi/2))) | \
-\ (EX n. ~even n & (x = -(real n * (pi/2)))))";
+\ ((EX n::nat. ~even n & (x = real n * (pi/2))) | \
+\ (EX n::nat. ~even n & (x = -(real n * (pi/2)))))";
by (rtac iffI 1);
by (cut_inst_tac [("x","x")] (CLAIM "0 <= (x::real) | x <= 0") 1);
by (Step_tac 1);
@@ -1998,15 +1997,15 @@
by (dtac cos_zero_lemma 3);
by (Step_tac 1);
by (dtac (CLAIM "-x = y ==> x = -(y::real)") 2);
-by (auto_tac (claset(),HOL_ss addsimps [odd_not_even RS sym,
+by (auto_tac (claset(),HOL_ss addsimps [
odd_Suc_mult_two_ex,real_of_nat_Suc,left_distrib]));
by (auto_tac (claset(),simpset() addsimps [cos_add]));
qed "cos_zero_iff";
(* ditto: but to a lesser extent *)
Goal "(sin x = 0) = \
-\ ((EX n. even n & (x = real n * (pi/2))) | \
-\ (EX n. even n & (x = -(real n * (pi/2)))))";
+\ ((EX n::nat. even n & (x = real n * (pi/2))) | \
+\ (EX n::nat. even n & (x = -(real n * (pi/2)))))";
by (rtac iffI 1);
by (cut_inst_tac [("x","x")] (CLAIM "0 <= (x::real) | x <= 0") 1);
by (Step_tac 1);
--- a/src/HOL/Integ/IntDef.thy Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Integ/IntDef.thy Thu Mar 04 12:06:07 2004 +0100
@@ -369,9 +369,6 @@
apply (simp add: zle linorder_linear)
done
-instance int :: plus_ac0
-proof qed (rule zadd_commute zadd_assoc zadd_0)+
-
instance int :: linorder
proof qed (rule zle_linear)
@@ -909,6 +906,63 @@
declare le_iff_diff_le_0 [symmetric, simp]
+subsection{*More Properties of @{term setsum} and @{term setprod}*}
+
+text{*By Jeremy Avigad*}
+
+
+lemma setsum_of_nat: "of_nat (setsum f A) = setsum (of_nat \<circ> f) A"
+ apply (case_tac "finite A")
+ apply (erule finite_induct, auto)
+ apply (simp add: setsum_def)
+ done
+
+lemma setsum_of_int: "of_int (setsum f A) = setsum (of_int \<circ> f) A"
+ apply (case_tac "finite A")
+ apply (erule finite_induct, auto)
+ apply (simp add: setsum_def)
+ done
+
+lemma int_setsum: "int (setsum f A) = setsum (int \<circ> f) A"
+ by (subst int_eq_of_nat, rule setsum_of_nat)
+
+lemma setprod_of_nat: "of_nat (setprod f A) = setprod (of_nat \<circ> f) A"
+ apply (case_tac "finite A")
+ apply (erule finite_induct, auto)
+ apply (simp add: setprod_def)
+ done
+
+lemma setprod_of_int: "of_int (setprod f A) = setprod (of_int \<circ> f) A"
+ apply (case_tac "finite A")
+ apply (erule finite_induct, auto)
+ apply (simp add: setprod_def)
+ done
+
+lemma int_setprod: "int (setprod f A) = setprod (int \<circ> f) A"
+ by (subst int_eq_of_nat, rule setprod_of_nat)
+
+lemma setsum_constant: "finite A ==> (\<Sum>x \<in> A. y) = of_nat(card A) * y"
+ apply (erule finite_induct)
+ apply (auto simp add: ring_distrib add_ac)
+ done
+
+lemma setprod_nonzero_nat:
+ "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
+ by (rule setprod_nonzero, auto)
+
+lemma setprod_zero_eq_nat:
+ "finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)"
+ by (rule setprod_zero_eq, auto)
+
+lemma setprod_nonzero_int:
+ "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::int)) ==> setprod f A \<noteq> 0"
+ by (rule setprod_nonzero, auto)
+
+lemma setprod_zero_eq_int:
+ "finite A ==> (setprod f A = (0::int)) = (\<exists>x \<in> A. f x = 0)"
+ by (rule setprod_zero_eq, auto)
+
+
(*Legacy ML bindings, but no longer the structure Int.*)
ML
{*
--- a/src/HOL/Integ/NatBin.thy Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Integ/NatBin.thy Thu Mar 04 12:06:07 2004 +0100
@@ -648,6 +648,12 @@
else number_of (bin_add v v') + k)"
by simp
+lemma nat_number_of_mult_left:
+ "number_of v * (number_of v' * (k::nat)) =
+ (if neg (number_of v :: int) then 0
+ else number_of (bin_mult v v') * k)"
+by simp
+
subsubsection{*For @{text combine_numerals}*}
@@ -776,6 +782,7 @@
val nat_number = thms"nat_number";
val nat_number_of_add_left = thm"nat_number_of_add_left";
+val nat_number_of_mult_left = thm"nat_number_of_mult_left";
val left_add_mult_distrib = thm"left_add_mult_distrib";
val nat_diff_add_eq1 = thm"nat_diff_add_eq1";
val nat_diff_add_eq2 = thm"nat_diff_add_eq2";
--- a/src/HOL/Integ/NatSimprocs.thy Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Integ/NatSimprocs.thy Thu Mar 04 12:06:07 2004 +0100
@@ -204,7 +204,7 @@
lemma minus1_divide [simp]:
"-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)"
-by (simp add: divide_inverse_zero inverse_minus_eq)
+by (simp add: divide_inverse inverse_minus_eq)
ML
{*
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/Parity.thy Thu Mar 04 12:06:07 2004 +0100
@@ -0,0 +1,279 @@
+(* Title: Parity.thy
+ Author: Jeremy Avigad
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
+
+ Last modified 2 March 2004
+*)
+
+header {* Parity: Even and Odd for ints and nats*}
+
+theory Parity = Divides + IntDiv + NatSimprocs:
+
+axclass even_odd < type
+
+instance int :: even_odd ..
+instance nat :: even_odd ..
+
+consts
+ even :: "'a::even_odd => bool"
+
+syntax
+ odd :: "'a::even_odd => bool"
+
+translations
+ "odd x" == "~even x"
+
+defs (overloaded)
+ even_def: "even (x::int) == x mod 2 = 0"
+ even_nat_def: "even (x::nat) == even (int x)"
+
+
+subsection {* Casting a nat power to an integer *}
+
+lemma zpow_int: "int (x^y) = (int x)^y"
+ apply (induct_tac y)
+ apply (simp, simp add: zmult_int [THEN sym])
+ done
+
+subsection {* Even and odd are mutually exclusive *}
+
+lemma int_pos_lt_two_imp_zero_or_one:
+ "0 <= x ==> (x::int) < 2 ==> x = 0 | x = 1"
+ by auto
+
+lemma neq_one_mod_two [simp]: "((x::int) mod 2 ~= 0) = (x mod 2 = 1)"
+ apply (subgoal_tac "x mod 2 = 0 | x mod 2 = 1", force)
+ apply (rule int_pos_lt_two_imp_zero_or_one, auto)
+ done
+
+subsection {* Behavior under integer arithmetic operations *}
+
+lemma even_times_anything: "even (x::int) ==> even (x * y)"
+ by (simp add: even_def zmod_zmult1_eq')
+
+lemma anything_times_even: "even (y::int) ==> even (x * y)"
+ by (simp add: even_def zmod_zmult1_eq)
+
+lemma odd_times_odd: "odd (x::int) ==> odd y ==> odd (x * y)"
+ by (simp add: even_def zmod_zmult1_eq)
+
+lemma even_product: "even((x::int) * y) = (even x | even y)"
+ apply (auto simp add: even_times_anything anything_times_even)
+ apply (rule ccontr)
+ apply (auto simp add: odd_times_odd)
+ done
+
+lemma even_plus_even: "even (x::int) ==> even y ==> even (x + y)"
+ by (simp add: even_def zmod_zadd1_eq)
+
+lemma even_plus_odd: "even (x::int) ==> odd y ==> odd (x + y)"
+ by (simp add: even_def zmod_zadd1_eq)
+
+lemma odd_plus_even: "odd (x::int) ==> even y ==> odd (x + y)"
+ by (simp add: even_def zmod_zadd1_eq)
+
+lemma odd_plus_odd: "odd (x::int) ==> odd y ==> even (x + y)"
+ by (simp add: even_def zmod_zadd1_eq)
+
+lemma even_sum: "even ((x::int) + y) = ((even x & even y) | (odd x & odd y))"
+ apply (auto intro: even_plus_even odd_plus_odd)
+ apply (rule ccontr, simp add: even_plus_odd)
+ apply (rule ccontr, simp add: odd_plus_even)
+ done
+
+lemma even_neg: "even (-(x::int)) = even x"
+ by (auto simp add: even_def zmod_zminus1_eq_if)
+
+lemma even_difference:
+ "even ((x::int) - y) = ((even x & even y) | (odd x & odd y))"
+ by (simp only: diff_minus even_sum even_neg)
+
+lemma even_pow_gt_zero [rule_format]:
+ "even (x::int) ==> 0 < n --> even (x^n)"
+ apply (induct_tac n)
+ apply (auto simp add: even_product)
+ done
+
+lemma odd_pow: "odd x ==> odd((x::int)^n)"
+ apply (induct_tac n)
+ apply (simp add: even_def)
+ apply (simp add: even_product)
+ done
+
+lemma even_power: "even ((x::int)^n) = (even x & 0 < n)"
+ apply (auto simp add: even_pow_gt_zero)
+ apply (erule contrapos_pp, erule odd_pow)
+ apply (erule contrapos_pp, simp add: even_def)
+ done
+
+lemma even_zero: "even (0::int)"
+ by (simp add: even_def)
+
+lemma odd_one: "odd (1::int)"
+ by (simp add: even_def)
+
+lemmas even_odd_simps [simp] = even_def[of "number_of v",standard] even_zero
+ odd_one even_product even_sum even_neg even_difference even_power
+
+
+subsection {* Equivalent definitions *}
+
+lemma two_times_even_div_two: "even (x::int) ==> 2 * (x div 2) = x"
+ by (auto simp add: even_def)
+
+lemma two_times_odd_div_two_plus_one: "odd (x::int) ==>
+ 2 * (x div 2) + 1 = x"
+ apply (insert zmod_zdiv_equality [of x 2, THEN sym])
+ by (simp add: even_def)
+
+lemma even_equiv_def: "even (x::int) = (EX y. x = 2 * y)"
+ apply auto
+ apply (rule exI)
+ by (erule two_times_even_div_two [THEN sym])
+
+lemma odd_equiv_def: "odd (x::int) = (EX y. x = 2 * y + 1)"
+ apply auto
+ apply (rule exI)
+ by (erule two_times_odd_div_two_plus_one [THEN sym])
+
+
+subsection {* even and odd for nats *}
+
+lemma pos_int_even_equiv_nat_even: "0 \<le> x ==> even x = even (nat x)"
+ by (simp add: even_nat_def)
+
+lemma even_nat_product: "even((x::nat) * y) = (even x | even y)"
+ by (simp add: even_nat_def zmult_int [THEN sym])
+
+lemma even_nat_sum: "even ((x::nat) + y) =
+ ((even x & even y) | (odd x & odd y))"
+ by (unfold even_nat_def, simp)
+
+lemma even_nat_difference:
+ "even ((x::nat) - y) = (x < y | (even x & even y) | (odd x & odd y))"
+ apply (auto simp add: even_nat_def zdiff_int [THEN sym])
+ apply (case_tac "x < y", auto simp add: zdiff_int [THEN sym])
+ apply (case_tac "x < y", auto simp add: zdiff_int [THEN sym])
+ done
+
+lemma even_nat_suc: "even (Suc x) = odd x"
+ by (simp add: even_nat_def)
+
+lemma even_nat_power: "even ((x::nat)^y) = (even x & 0 < y)"
+ by (simp add: even_nat_def zpow_int)
+
+lemma even_nat_zero: "even (0::nat)"
+ by (simp add: even_nat_def)
+
+lemmas even_odd_nat_simps [simp] = even_nat_def[of "number_of v",standard]
+ even_nat_zero even_nat_suc even_nat_product even_nat_sum even_nat_power
+
+
+subsection {* Equivalent definitions *}
+
+lemma nat_lt_two_imp_zero_or_one: "(x::nat) < Suc (Suc 0) ==>
+ x = 0 | x = Suc 0"
+ by auto
+
+lemma even_nat_mod_two_eq_zero: "even (x::nat) ==> x mod (Suc (Suc 0)) = 0"
+ apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym])
+ apply (drule subst, assumption)
+ apply (subgoal_tac "x mod Suc (Suc 0) = 0 | x mod Suc (Suc 0) = Suc 0")
+ apply force
+ apply (subgoal_tac "0 < Suc (Suc 0)")
+ apply (frule mod_less_divisor [of "Suc (Suc 0)" x])
+ apply (erule nat_lt_two_imp_zero_or_one, auto)
+ done
+
+lemma odd_nat_mod_two_eq_one: "odd (x::nat) ==> x mod (Suc (Suc 0)) = Suc 0"
+ apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym])
+ apply (drule subst, assumption)
+ apply (subgoal_tac "x mod Suc (Suc 0) = 0 | x mod Suc (Suc 0) = Suc 0")
+ apply force
+ apply (subgoal_tac "0 < Suc (Suc 0)")
+ apply (frule mod_less_divisor [of "Suc (Suc 0)" x])
+ apply (erule nat_lt_two_imp_zero_or_one, auto)
+ done
+
+lemma even_nat_equiv_def: "even (x::nat) = (x mod Suc (Suc 0) = 0)"
+ apply (rule iffI)
+ apply (erule even_nat_mod_two_eq_zero)
+ apply (insert odd_nat_mod_two_eq_one [of x], auto)
+ done
+
+lemma odd_nat_equiv_def: "odd (x::nat) = (x mod Suc (Suc 0) = Suc 0)"
+ apply (auto simp add: even_nat_equiv_def)
+ apply (subgoal_tac "x mod (Suc (Suc 0)) < Suc (Suc 0)")
+ apply (frule nat_lt_two_imp_zero_or_one, auto)
+ done
+
+lemma even_nat_div_two_times_two: "even (x::nat) ==>
+ Suc (Suc 0) * (x div Suc (Suc 0)) = x"
+ apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym])
+ apply (drule even_nat_mod_two_eq_zero, simp)
+ done
+
+lemma odd_nat_div_two_times_two_plus_one: "odd (x::nat) ==>
+ Suc( Suc (Suc 0) * (x div Suc (Suc 0))) = x"
+ apply (insert mod_div_equality [of x "Suc (Suc 0)", THEN sym])
+ apply (drule odd_nat_mod_two_eq_one, simp)
+ done
+
+lemma even_nat_equiv_def2: "even (x::nat) = (EX y. x = Suc (Suc 0) * y)"
+ apply (rule iffI, rule exI)
+ apply (erule even_nat_div_two_times_two [THEN sym], auto)
+ done
+
+lemma odd_nat_equiv_def2: "odd (x::nat) = (EX y. x = Suc(Suc (Suc 0) * y))"
+ apply (rule iffI, rule exI)
+ apply (erule odd_nat_div_two_times_two_plus_one [THEN sym], auto)
+ done
+
+subsection {* Powers of negative one *}
+
+lemma neg_one_even_odd_power:
+ "(even x --> (-1::'a::{number_ring,ringpower})^x = 1) &
+ (odd x --> (-1::'a)^x = -1)"
+ apply (induct_tac x)
+ apply (simp, simp add: power_Suc)
+ done
+
+lemma neg_one_even_power: "even x ==> (-1::'a::{number_ring,ringpower})^x = 1"
+ by (rule neg_one_even_odd_power [THEN conjunct1, THEN mp], assumption)
+
+lemma neg_one_odd_power: "odd x ==> (-1::'a::{number_ring,ringpower})^x = -1"
+ by (rule neg_one_even_odd_power [THEN conjunct2, THEN mp], assumption)
+
+
+subsection {* Miscellaneous *}
+
+lemma even_plus_one_div_two: "even (x::int) ==> (x + 1) div 2 = x div 2"
+ apply (subst zdiv_zadd1_eq)
+ apply (simp add: even_def)
+ done
+
+lemma odd_plus_one_div_two: "odd (x::int) ==> (x + 1) div 2 = x div 2 + 1"
+ apply (subst zdiv_zadd1_eq)
+ apply (simp add: even_def)
+ done
+
+lemma div_Suc: "Suc a div c = a div c + Suc 0 div c +
+ (a mod c + Suc 0 mod c) div c"
+ apply (subgoal_tac "Suc a = a + Suc 0")
+ apply (erule ssubst)
+ apply (rule div_add1_eq, simp)
+ done
+
+lemma even_nat_plus_one_div_two: "even (x::nat) ==>
+ (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)"
+ apply (subst div_Suc)
+ apply (simp add: even_nat_equiv_def)
+ done
+
+lemma odd_nat_plus_one_div_two: "odd (x::nat) ==>
+ (Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))"
+ apply (subst div_Suc)
+ apply (simp add: odd_nat_equiv_def)
+ done
+
+end
--- a/src/HOL/Integ/nat_simprocs.ML Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Integ/nat_simprocs.ML Thu Mar 04 12:06:07 2004 +0100
@@ -6,6 +6,10 @@
Simprocs for nat numerals.
*)
+val Let_number_of = thm"Let_number_of";
+val Let_0 = thm"Let_0";
+val Let_1 = thm"Let_1";
+
structure Nat_Numeral_Simprocs =
struct
@@ -65,12 +69,14 @@
val trans_tac = Int_Numeral_Simprocs.trans_tac;
-val bin_simps = [nat_numeral_0_eq_0 RS sym, nat_numeral_1_eq_1 RS sym,
- add_nat_number_of, nat_number_of_add_left,
- diff_nat_number_of, le_number_of_eq_not_less,
- less_nat_number_of, mult_nat_number_of,
- thm "Let_number_of", nat_number_of] @
- bin_arith_simps @ bin_rel_simps;
+val bin_simps =
+ [nat_numeral_0_eq_0 RS sym, nat_numeral_1_eq_1 RS sym,
+ add_nat_number_of, nat_number_of_add_left,
+ diff_nat_number_of, le_number_of_eq_not_less,
+ mult_nat_number_of, nat_number_of_mult_left,
+ less_nat_number_of,
+ Let_number_of, nat_number_of] @
+ bin_arith_simps @ bin_rel_simps;
fun prep_simproc (name, pats, proc) =
Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc;
@@ -268,7 +274,8 @@
val trans_tac = trans_tac
val norm_tac = ALLGOALS
(simp_tac (HOL_ss addsimps [Suc_eq_add_numeral_1]@mult_1s))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@mult_ac))
+ THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
+ THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac))
val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
val simplify_meta_eq = simplify_meta_eq
end
@@ -504,7 +511,7 @@
(* reduce contradictory <= to False *)
val add_rules =
- [thm "Let_number_of", thm "Let_0", thm "Let_1", nat_0, nat_1,
+ [thm "Let_number_of", Let_0, Let_1, nat_0, nat_1,
add_nat_number_of, diff_nat_number_of, mult_nat_number_of,
eq_nat_number_of, less_nat_number_of, le_number_of_eq_not_less,
le_Suc_number_of,le_number_of_Suc,
--- a/src/HOL/IsaMakefile Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/IsaMakefile Thu Mar 04 12:06:07 2004 +0100
@@ -87,9 +87,8 @@
HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.thy \
Integ/cooper_dec.ML Integ/cooper_proof.ML \
Integ/Equiv.thy Integ/IntArith.thy Integ/IntDef.thy \
- Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy \
- Integ/int_arith1.ML \
- Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
+ Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Parity.thy \
+ Integ/int_arith1.ML Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy Nat.ML \
Nat.thy NatArith.ML NatArith.thy Numeral.thy \
@@ -143,7 +142,7 @@
Real/Rational.thy Real/PReal.thy Real/RComplete.thy \
Real/ROOT.ML Real/Real.thy Real/real_arith.ML Real/RealDef.thy \
Real/RealPow.thy Real/document/root.tex Real/real_arith.ML\
- Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy \
+ Hyperreal/EvenOdd.thy\
Hyperreal/Fact.ML Hyperreal/Fact.thy Hyperreal/HLog.thy\
Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HSeries.thy\
Hyperreal/HTranscendental.thy Hyperreal/HyperArith.thy\
--- a/src/HOL/NumberTheory/Finite2.thy Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/NumberTheory/Finite2.thy Thu Mar 04 12:06:07 2004 +0100
@@ -253,12 +253,7 @@
lemma cartesian_product_card [simp]: "[| finite A; finite B |] ==>
card (A <*> B) = card(A) * card(B)";
apply (rule_tac F = A in finite_induct, auto)
- apply (case_tac "F = {}", force)
- apply (subgoal_tac "card({x} <*> B \<union> F <*> B) = card({x} <*> B) +
- card(F <*> B)");
- apply simp
- apply (rule card_Un_disjoint)
- by auto
+ done
(******************************************************************)
(* *)
--- a/src/HOL/PreList.thy Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/PreList.thy Thu Mar 04 12:06:07 2004 +0100
@@ -9,7 +9,8 @@
(*Is defined separately to serve as a basis for theory ToyList in the
documentation.*)
-theory PreList = Wellfounded_Relations + Presburger + Recdef + Relation_Power:
+theory PreList =
+ Wellfounded_Relations + Presburger + Recdef + Relation_Power + Parity:
(*belongs to theory Wellfounded_Recursion*)
lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]
--- a/src/HOL/Real/PReal.thy Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Real/PReal.thy Thu Mar 04 12:06:07 2004 +0100
@@ -296,13 +296,13 @@
show "\<exists>y' \<in> B. z = x*?f + y'"
proof
show "z = x*?f + y*?f"
- by (simp add: left_distrib [symmetric] divide_inverse_zero mult_ac
+ by (simp add: left_distrib [symmetric] divide_inverse mult_ac
order_less_imp_not_eq2)
next
show "y * ?f \<in> B"
proof (rule preal_downwards_closed [OF B y])
show "0 < y * ?f"
- by (simp add: divide_inverse_zero zero_less_mult_iff)
+ by (simp add: divide_inverse zero_less_mult_iff)
next
show "y * ?f < y"
by (insert mult_strict_left_mono [OF fless ypos], simp)
@@ -312,7 +312,7 @@
show "x * ?f \<in> A"
proof (rule preal_downwards_closed [OF A x])
show "0 < x * ?f"
- by (simp add: divide_inverse_zero zero_less_mult_iff)
+ by (simp add: divide_inverse zero_less_mult_iff)
next
show "x * ?f < x"
by (insert mult_strict_left_mono [OF fless xpos], simp)
@@ -435,7 +435,7 @@
show "\<exists>y'\<in>B. z = (z/y) * y'"
proof
show "z = (z/y)*y"
- by (simp add: divide_inverse_zero mult_commute [of y] mult_assoc
+ by (simp add: divide_inverse mult_commute [of y] mult_assoc
order_less_imp_not_eq2)
show "y \<in> B" .
qed
@@ -522,7 +522,7 @@
show "\<exists>v'\<in>A. x = (x / v) * v'"
proof
show "x = (x/v)*v"
- by (simp add: divide_inverse_zero mult_assoc vpos
+ by (simp add: divide_inverse mult_assoc vpos
order_less_imp_not_eq2)
show "v \<in> A" .
qed
@@ -579,7 +579,7 @@
have cpos: "0 < ?c"
by (simp add: zero_less_divide_iff zero_less_mult_iff pos_add_strict)
show "a * d + b * e = ?c * (d + e)"
- by (simp add: divide_inverse_zero mult_assoc order_less_imp_not_eq2)
+ by (simp add: divide_inverse mult_assoc order_less_imp_not_eq2)
show "?c \<in> Rep_preal w"
proof (cases rule: linorder_le_cases)
assume "a \<le> b"
@@ -808,7 +808,7 @@
proof -
have "r + ?d < r + (r * ?d)/y" by (simp add: dless)
also with ypos have "... = (r/y) * (y + ?d)"
- by (simp only: right_distrib divide_inverse_zero mult_ac, simp)
+ by (simp only: right_distrib divide_inverse mult_ac, simp)
also have "... = r*x" using ypos
by simp
finally show "r + ?d < r*x" .
@@ -849,12 +849,12 @@
show "0 < x/u" using xpos upos
by (simp add: zero_less_divide_iff)
show "x/u < x/r" using xpos upos rpos
- by (simp add: divide_inverse_zero mult_less_cancel_left rless)
+ by (simp add: divide_inverse mult_less_cancel_left rless)
show "inverse (x / r) \<notin> Rep_preal R" using notin
- by (simp add: divide_inverse_zero mult_commute)
+ by (simp add: divide_inverse mult_commute)
show "u \<in> Rep_preal R" by (rule u)
show "x = x / u * u" using upos
- by (simp add: divide_inverse_zero mult_commute)
+ by (simp add: divide_inverse mult_commute)
qed
qed
@@ -875,7 +875,7 @@
have "q < inverse y" using rpos rless
by (simp add: not_in_preal_ub [OF Rep_preal notin] q)
hence "r * q < r/y" using rpos
- by (simp add: divide_inverse_zero mult_less_cancel_left)
+ by (simp add: divide_inverse mult_less_cancel_left)
also have "... \<le> 1" using rpos rless
by (simp add: pos_divide_le_eq)
finally show ?thesis .
@@ -1272,7 +1272,7 @@
have "x * z * inverse y * inverse z = x * inverse y * (z * inverse z)"
by (simp add: mult_ac)
also have "... = x/y" using zpos
- by (simp add: divide_inverse_zero)
+ by (simp add: divide_inverse)
also have "... < z"
by (simp add: pos_divide_less_eq [OF ypos] mult_commute)
finally show ?thesis .
--- a/src/HOL/Real/Rational.thy Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Real/Rational.thy Thu Mar 04 12:06:07 2004 +0100
@@ -511,9 +511,8 @@
(simp add: add_rat mult_rat eq_rat int_distrib)
show "q \<noteq> 0 ==> inverse q * q = 1"
by (induct q) (simp add: inverse_rat mult_rat one_rat zero_rat eq_rat)
- show "r \<noteq> 0 ==> q / r = q * inverse r"
- by (induct q, induct r)
- (simp add: mult_rat divide_rat inverse_rat zero_rat eq_rat)
+ show "q / r = q * inverse r"
+ by (simp add: divide_rat_def)
show "0 \<noteq> (1::rat)"
by (simp add: zero_rat one_rat eq_rat)
qed
@@ -632,9 +631,7 @@
instance rat :: division_by_zero
proof
- fix x :: rat
show "inverse 0 = (0::rat)" by (simp add: inverse_rat_def)
- show "x/0 = 0" by (simp add: divide_rat_def inverse_rat_def)
qed
--- a/src/HOL/Real/RealDef.thy Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Real/RealDef.thy Thu Mar 04 12:06:07 2004 +0100
@@ -351,7 +351,7 @@
show "(x + y) * z = x * z + y * z" by (simp add: real_add_mult_distrib)
show "0 \<noteq> (1::real)" by (rule real_zero_not_eq_one)
show "x \<noteq> 0 ==> inverse x * x = 1" by (rule real_mult_inverse_left)
- show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: real_divide_def)
+ show "x / y = x * inverse y" by (simp add: real_divide_def)
qed
@@ -365,9 +365,7 @@
instance real :: division_by_zero
proof
- fix x :: real
show "inverse 0 = (0::real)" by (rule INVERSE_ZERO)
- show "x/0 = 0" by (simp add: real_divide_def INVERSE_ZERO)
qed
--- a/src/HOL/Ring_and_Field.thy Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/Ring_and_Field.thy Thu Mar 04 12:06:07 2004 +0100
@@ -59,13 +59,12 @@
axclass field \<subseteq> ring, inverse
left_inverse [simp]: "a \<noteq> 0 ==> inverse a * a = 1"
- divide_inverse: "b \<noteq> 0 ==> a / b = a * inverse b"
+ divide_inverse: "a / b = a * inverse b"
axclass ordered_field \<subseteq> ordered_ring, field
axclass division_by_zero \<subseteq> zero, inverse
inverse_zero [simp]: "inverse 0 = 0"
- divide_zero [simp]: "a / 0 = 0"
subsection {* Derived Rules for Addition *}
@@ -595,7 +594,7 @@
instance ordered_ring \<subseteq> ordered_semiring
proof
have "(0::'a) \<le> 1*1" by (rule zero_le_square)
- thus "(0::'a) < 1" by (simp add: order_le_less )
+ thus "(0::'a) < 1" by (simp add: order_le_less)
qed
text{*All three types of comparision involving 0 and 1 are covered.*}
@@ -650,7 +649,7 @@
lemma less_1_mult: "[| 1 < m; 1 < n |] ==> 1 < m*(n::'a::ordered_semiring)"
apply (insert mult_strict_mono [of 1 m 1 n])
-apply (simp add: order_less_trans [OF zero_less_one]);
+apply (simp add: order_less_trans [OF zero_less_one])
done
@@ -743,24 +742,18 @@
lemma divide_self [simp]: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
by (simp add: divide_inverse)
-lemma divide_inverse_zero: "a/b = a * inverse(b::'a::{field,division_by_zero})"
-apply (case_tac "b = 0")
-apply (simp_all add: divide_inverse)
-done
+lemma divide_zero [simp]: "a / 0 = (0::'a::{field,division_by_zero})"
+by (simp add: divide_inverse)
-lemma divide_zero_left [simp]: "0/a = (0::'a::{field,division_by_zero})"
-by (simp add: divide_inverse_zero)
+lemma divide_zero_left [simp]: "0/a = (0::'a::field)"
+by (simp add: divide_inverse)
-lemma inverse_eq_divide: "inverse (a::'a::{field,division_by_zero}) = 1/a"
-by (simp add: divide_inverse_zero)
+lemma inverse_eq_divide: "inverse (a::'a::field) = 1/a"
+by (simp add: divide_inverse)
-lemma nonzero_add_divide_distrib: "c \<noteq> 0 ==> (a+b)/(c::'a::field) = a/c + b/c"
+lemma add_divide_distrib: "(a+b)/(c::'a::field) = a/c + b/c"
by (simp add: divide_inverse left_distrib)
-lemma add_divide_distrib: "(a+b)/(c::'a::{field,division_by_zero}) = a/c + b/c"
-apply (case_tac "c=0", simp)
-apply (simp add: nonzero_add_divide_distrib)
-done
text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement
of an ordering.*}
@@ -935,7 +928,7 @@
lemma inverse_divide [simp]:
"inverse (a/b) = b / (a::'a::{field,division_by_zero})"
- by (simp add: divide_inverse_zero mult_commute)
+ by (simp add: divide_inverse mult_commute)
lemma nonzero_mult_divide_cancel_left:
assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0"
@@ -975,23 +968,21 @@
by (simp add: mult_divide_cancel_left)
lemma divide_1 [simp]: "a/1 = (a::'a::field)"
- by (simp add: divide_inverse [OF not_sym])
+ by (simp add: divide_inverse)
-lemma times_divide_eq_right [simp]:
- "a * (b/c) = (a*b) / (c::'a::{field,division_by_zero})"
-by (simp add: divide_inverse_zero mult_assoc)
+lemma times_divide_eq_right [simp]: "a * (b/c) = (a*b) / (c::'a::field)"
+by (simp add: divide_inverse mult_assoc)
-lemma times_divide_eq_left [simp]:
- "(b/c) * a = (b*a) / (c::'a::{field,division_by_zero})"
-by (simp add: divide_inverse_zero mult_ac)
+lemma times_divide_eq_left: "(b/c) * a = (b*a) / (c::'a::field)"
+by (simp add: divide_inverse mult_ac)
lemma divide_divide_eq_right [simp]:
"a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
-by (simp add: divide_inverse_zero mult_ac)
+by (simp add: divide_inverse mult_ac)
lemma divide_divide_eq_left [simp]:
"(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
-by (simp add: divide_inverse_zero mult_assoc)
+by (simp add: divide_inverse mult_assoc)
subsection {* Division and Unary Minus *}
@@ -1005,14 +996,12 @@
lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a)/(-b) = a / (b::'a::field)"
by (simp add: divide_inverse nonzero_inverse_minus_eq)
-lemma minus_divide_left: "- (a/b) = (-a) / (b::'a::{field,division_by_zero})"
-apply (case_tac "b=0", simp)
-apply (simp add: nonzero_minus_divide_left)
-done
+lemma minus_divide_left: "- (a/b) = (-a) / (b::'a::field)"
+by (simp add: divide_inverse minus_mult_left [symmetric])
lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
-apply (case_tac "b=0", simp)
-by (rule nonzero_minus_divide_right)
+by (simp add: divide_inverse minus_mult_right [symmetric])
+
text{*The effect is to extract signs from divisions*}
declare minus_divide_left [symmetric, simp]
@@ -1028,8 +1017,7 @@
apply (simp add: nonzero_minus_divide_divide)
done
-lemma diff_divide_distrib:
- "(a-b)/(c::'a::{field,division_by_zero}) = a/c - b/c"
+lemma diff_divide_distrib: "(a-b)/(c::'a::field) = a/c - b/c"
by (simp add: diff_minus add_divide_distrib)
@@ -1236,26 +1224,26 @@
lemma zero_less_divide_iff:
"((0::'a::{ordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
-by (simp add: divide_inverse_zero zero_less_mult_iff)
+by (simp add: divide_inverse zero_less_mult_iff)
lemma divide_less_0_iff:
"(a/b < (0::'a::{ordered_field,division_by_zero})) =
(0 < a & b < 0 | a < 0 & 0 < b)"
-by (simp add: divide_inverse_zero mult_less_0_iff)
+by (simp add: divide_inverse mult_less_0_iff)
lemma zero_le_divide_iff:
"((0::'a::{ordered_field,division_by_zero}) \<le> a/b) =
(0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
-by (simp add: divide_inverse_zero zero_le_mult_iff)
+by (simp add: divide_inverse zero_le_mult_iff)
lemma divide_le_0_iff:
"(a/b \<le> (0::'a::{ordered_field,division_by_zero})) =
(0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
-by (simp add: divide_inverse_zero mult_le_0_iff)
+by (simp add: divide_inverse mult_le_0_iff)
lemma divide_eq_0_iff [simp]:
"(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
-by (simp add: divide_inverse_zero field_mult_eq_0_iff)
+by (simp add: divide_inverse field_mult_eq_0_iff)
subsection{*Simplification of Inequalities Involving Literal Divisors*}
@@ -1415,13 +1403,13 @@
lemma divide_cancel_right [simp]:
"(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
apply (case_tac "c=0", simp)
-apply (simp add: divide_inverse_zero field_mult_cancel_right)
+apply (simp add: divide_inverse field_mult_cancel_right)
done
lemma divide_cancel_left [simp]:
"(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
apply (case_tac "c=0", simp)
-apply (simp add: divide_inverse_zero field_mult_cancel_left)
+apply (simp add: divide_inverse field_mult_cancel_left)
done
subsection {* Division and the Number One *}
@@ -1669,6 +1657,9 @@
thus ?thesis by (simp add: ac cpos mult_strict_mono)
qed
+text{*Moving this up spoils many proofs using @{text mult_le_cancel_right}*}
+declare times_divide_eq_left [simp]
+
ML
{*
val add_assoc = thm"add_assoc";
@@ -1809,11 +1800,9 @@
val right_inverse_eq = thm"right_inverse_eq";
val nonzero_inverse_eq_divide = thm"nonzero_inverse_eq_divide";
val divide_self = thm"divide_self";
-val divide_inverse_zero = thm"divide_inverse_zero";
val inverse_divide = thm"inverse_divide";
val divide_zero_left = thm"divide_zero_left";
val inverse_eq_divide = thm"inverse_eq_divide";
-val nonzero_add_divide_distrib = thm"nonzero_add_divide_distrib";
val add_divide_distrib = thm"add_divide_distrib";
val field_mult_eq_0_iff = thm"field_mult_eq_0_iff";
val field_mult_cancel_right = thm"field_mult_cancel_right";
--- a/src/HOL/simpdata.ML Thu Mar 04 10:06:13 2004 +0100
+++ b/src/HOL/simpdata.ML Thu Mar 04 12:06:07 2004 +0100
@@ -246,7 +246,7 @@
imp_disjL, conj_assoc, disj_assoc,
de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
disj_not1, not_all, not_ex, cases_simp,
- thm "the_eq_trivial", the_sym_eq_trivial, thm "plus_ac0.zero", thm "plus_ac0_zero_right"]
+ thm "the_eq_trivial", the_sym_eq_trivial]
@ ex_simps @ all_simps @ simp_thms)
addsimprocs [defALL_regroup,defEX_regroup]
addcongs [imp_cong]