# HG changeset patch # User huffman # Date 1234603441 28800 # Node ID b82ab2aebbbf3a041b7079552242e75bc51fec36 # Parent 6b9eea61057c253956a5f4ede6764aa349ef892a# Parent 2c0046b26f80811f19ecb239a560ed21be6c69e9 merged diff -r 2c0046b26f80 -r b82ab2aebbbf src/HOL/Auth/document/root.tex --- a/src/HOL/Auth/document/root.tex Sat Feb 14 08:45:16 2009 +0100 +++ b/src/HOL/Auth/document/root.tex Sat Feb 14 01:24:01 2009 -0800 @@ -1,5 +1,6 @@ \documentclass[10pt,a4paper,twoside]{article} \usepackage{graphicx} +\usepackage{amssymb} \usepackage[latin1]{inputenc} \usepackage{latexsym,theorem} \usepackage{isabelle,isabellesym} diff -r 2c0046b26f80 -r b82ab2aebbbf src/HOL/Library/Binomial.thy --- a/src/HOL/Library/Binomial.thy Sat Feb 14 08:45:16 2009 +0100 +++ b/src/HOL/Library/Binomial.thy Sat Feb 14 01:24:01 2009 -0800 @@ -182,7 +182,7 @@ finally show ?case by simp qed -section{* Pochhammer's symbol : generalized raising factorial*} +subsection{* Pochhammer's symbol : generalized raising factorial*} definition "pochhammer (a::'a::comm_semiring_1) n = (if n = 0 then 1 else setprod (\n. a + of_nat n) {0 .. n - 1})" @@ -285,7 +285,7 @@ pochhammer_of_nat_eq_0_lemma'[of k n, where ?'a = 'a] by (auto simp add: not_le[symmetric]) -section{* Generalized binomial coefficients *} +subsection{* Generalized binomial coefficients *} definition gbinomial :: "'a::{field, recpower,ring_char_0} \ nat \ 'a" (infixl "gchoose" 65) where "a gchoose n = (if n = 0 then 1 else (setprod (\i. a - of_nat i) {0 .. n - 1}) / of_nat (fact n))" diff -r 2c0046b26f80 -r b82ab2aebbbf src/HOL/Library/Euclidean_Space.thy --- a/src/HOL/Library/Euclidean_Space.thy Sat Feb 14 08:45:16 2009 +0100 +++ b/src/HOL/Library/Euclidean_Space.thy Sat Feb 14 01:24:01 2009 -0800 @@ -40,7 +40,7 @@ lemma setsum_3: "setsum f {1::nat..3} = f 1 + f 2 + f 3" by (simp add: nat_number atLeastAtMostSuc_conv add_commute) -section{* Basic componentwise operations on vectors. *} +subsection{* Basic componentwise operations on vectors. *} instantiation "^" :: (plus,type) plus begin @@ -106,7 +106,7 @@ lemma dot_3[simp]: "(x::'a::{comm_monoid_add, times}^3) \ y = (x$1) * (y$1) + (x$2) * (y$2) + (x$3) * (y$3)" by (simp add: dot_def dimindex_def nat_number) -section {* A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space. *} +subsection {* A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space. *} lemmas Cart_lambda_beta' = Cart_lambda_beta[rule_format] method_setup vector = {* @@ -236,6 +236,7 @@ apply (intro_classes) by (vector ring_simps)+ instance "^" :: (comm_semiring_0,type) comm_semiring_0 by (intro_classes) +instance "^" :: (cancel_comm_monoid_add, type) cancel_comm_monoid_add .. instance "^" :: (semiring_0_cancel,type) semiring_0_cancel by (intro_classes) instance "^" :: (comm_semiring_0_cancel,type) comm_semiring_0_cancel by (intro_classes) instance "^" :: (ring,type) ring by (intro_classes) diff -r 2c0046b26f80 -r b82ab2aebbbf src/HOL/Library/Finite_Cartesian_Product.thy --- a/src/HOL/Library/Finite_Cartesian_Product.thy Sat Feb 14 08:45:16 2009 +0100 +++ b/src/HOL/Library/Finite_Cartesian_Product.thy Sat Feb 14 01:24:01 2009 -0800 @@ -33,7 +33,7 @@ by (simp add: dimindex_def hassize_def) -section{* An indexing type parametrized by base type. *} +subsection{* An indexing type parametrized by base type. *} typedef 'a finite_image = "{1 .. DIM('a)}" using dimindex_ge_1 by auto diff -r 2c0046b26f80 -r b82ab2aebbbf src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Sat Feb 14 08:45:16 2009 +0100 +++ b/src/HOL/Library/Formal_Power_Series.thy Sat Feb 14 01:24:01 2009 -0800 @@ -9,7 +9,7 @@ imports Main Fact Parity begin -section {* The type of formal power series*} +subsection {* The type of formal power series*} typedef 'a fps = "{f :: nat \ 'a. True}" by simp @@ -94,7 +94,7 @@ lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)" by auto -section{* Formal power series form a commutative ring with unity, if the range of sequences +subsection{* Formal power series form a commutative ring with unity, if the range of sequences they represent is a commutative ring with unity*} instantiation fps :: (semigroup_add) semigroup_add @@ -293,7 +293,7 @@ qed end -section {* Selection of the nth power of the implicit variable in the infinite sum*} +subsection {* Selection of the nth power of the implicit variable in the infinite sum*} definition fps_nth:: "'a fps \ nat \ 'a" (infixl "$" 75) where "f $ n = Rep_fps f n" @@ -358,7 +358,7 @@ ultimately show ?thesis by blast qed -section{* Injection of the basic ring elements and multiplication by scalars *} +subsection{* Injection of the basic ring elements and multiplication by scalars *} definition "fps_const c = Abs_fps (\n. if n = 0 then c else 0)" lemma fps_const_0_eq_0[simp]: "fps_const 0 = 0" by (simp add: fps_const_def fps_eq_iff) @@ -391,7 +391,7 @@ lemma fps_mult_right_const_nth[simp]: "(f * fps_const (c::'a::semiring_1))$n = f$n * c" by (simp add: fps_mult_nth fps_const_nth cond_application_beta cond_value_iff setsum_delta' cong del: if_weak_cong) -section {* Formal power series form an integral domain*} +subsection {* Formal power series form an integral domain*} instantiation fps :: (ring_1) ring_1 begin @@ -442,7 +442,7 @@ instance .. end -section{* Inverses of formal power series *} +subsection{* Inverses of formal power series *} declare setsum_cong[fundef_cong] @@ -561,7 +561,7 @@ by(simp add: setsum_delta) qed -section{* Formal Derivatives, and the McLauren theorem around 0*} +subsection{* Formal Derivatives, and the McLauren theorem around 0*} definition "fps_deriv f = Abs_fps (\n. of_nat (n + 1) * f $ (n + 1))" @@ -730,7 +730,7 @@ lemma fps_deriv_maclauren_0: "(fps_nth_deriv k (f:: ('a::comm_semiring_1) fps)) $ 0 = of_nat (fact k) * f$(k)" by (induct k arbitrary: f) (auto simp add: ring_simps of_nat_mult) -section {* Powers*} +subsection {* Powers*} instantiation fps :: (semiring_1) power begin @@ -945,7 +945,7 @@ using fps_inverse_deriv[OF a0] by (simp add: fps_divide_def ring_simps power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0]) -section{* The eXtractor series X*} +subsection{* The eXtractor series X*} lemma minus_one_power_iff: "(- (1::'a :: {recpower, comm_ring_1})) ^ n = (if even n then 1 else - 1)" by (induct n, auto) @@ -1015,7 +1015,7 @@ qed -section{* Integration *} +subsection{* Integration *} definition "fps_integral a a0 = Abs_fps (\n. if n = 0 then a0 else (a$(n - 1) / of_nat n))" lemma fps_deriv_fps_integral: "fps_deriv (fps_integral a (a0 :: 'a :: {field, ring_char_0})) = a" @@ -1029,7 +1029,7 @@ unfolding fps_deriv_eq_iff by auto qed -section {* Composition of FPSs *} +subsection {* Composition of FPSs *} definition fps_compose :: "('a::semiring_1) fps \ 'a fps \ 'a fps" (infixl "oo" 55) where fps_compose_def: "a oo b = Abs_fps (\n. setsum (\i. a$i * (b^i$n)) {0..n})" @@ -1051,9 +1051,9 @@ by simp_all -section {* Rules from Herbert Wilf's Generatingfunctionology*} +subsection {* Rules from Herbert Wilf's Generatingfunctionology*} -subsection {* Rule 1 *} +subsubsection {* Rule 1 *} (* {a_{n+k}}_0^infty Corresponds to (f - setsum (\i. a_i * x^i))/x^h, for h>0*) lemma fps_power_mult_eq_shift: @@ -1083,7 +1083,7 @@ then show ?thesis by (simp add: fps_eq_iff) qed -subsection{* Rule 2*} +subsubsection{* Rule 2*} (* We can not reach the form of Wilf, but still near to it using rewrite rules*) (* If f reprents {a_n} and P is a polynomial, then @@ -1108,8 +1108,8 @@ lemma fps_mult_XD_shift: "(XD ^k) (a:: ('a::{comm_ring_1, recpower, ring_char_0}) fps) = Abs_fps (\n. (of_nat n ^ k) * a$n)" by (induct k arbitrary: a) (simp_all add: power_Suc XD_def fps_eq_iff ring_simps del: One_nat_def) -subsection{* Rule 3 is trivial and is given by @{text fps_times_def}*} -subsection{* Rule 5 --- summation and "division" by (1 - X)*} +subsubsection{* Rule 3 is trivial and is given by @{text fps_times_def}*} +subsubsection{* Rule 5 --- summation and "division" by (1 - X)*} lemma fps_divide_X_minus1_setsum_lemma: "a = ((1::('a::comm_ring_1) fps) - X) * Abs_fps (\n. setsum (\i. a $ i) {0..n})" @@ -1157,7 +1157,7 @@ finally show ?thesis by (simp add: inverse_mult_eq_1[OF th0]) qed -subsection{* Rule 4 in its more general form: generalizes Rule 3 for an arbitrary +subsubsection{* Rule 4 in its more general form: generalizes Rule 3 for an arbitrary finite product of FPS, also the relvant instance of powers of a FPS*} definition "natpermute n k = {l:: nat list. length l = k \ foldl op + 0 l = n}" @@ -1447,7 +1447,7 @@ qed -section {* Radicals *} +subsection {* Radicals *} declare setprod_cong[fundef_cong] function radical :: "(nat \ 'a \ 'a) \ nat \ ('a::{field, recpower}) fps \ nat \ 'a" where @@ -1832,7 +1832,7 @@ ultimately show ?thesis by blast qed -section{* Derivative of composition *} +subsection{* Derivative of composition *} lemma fps_compose_deriv: fixes a:: "('a::idom) fps" @@ -1898,7 +1898,7 @@ ultimately show ?thesis by (cases n, auto) qed -section{* Finite FPS (i.e. polynomials) and X *} +subsection{* Finite FPS (i.e. polynomials) and X *} lemma fps_poly_sum_X: assumes z: "\i > n. a$i = (0::'a::comm_ring_1)" shows "a = setsum (\i. fps_const (a$i) * X^i) {0..n}" (is "a = ?r") @@ -1911,7 +1911,7 @@ then show ?thesis unfolding fps_eq_iff by blast qed -section{* Compositional inverses *} +subsection{* Compositional inverses *} fun compinv :: "'a fps \ nat \ 'a::{recpower,field}" where @@ -2217,9 +2217,9 @@ show "?dia = inverse ?d" by simp qed -section{* Elementary series *} +subsection{* Elementary series *} -subsection{* Exponential series *} +subsubsection{* Exponential series *} definition "E x = Abs_fps (\n. x^n / of_nat (fact n))" lemma E_deriv[simp]: "fps_deriv (E a) = fps_const (a::'a::{field, recpower, ring_char_0}) * E a" (is "?l = ?r") @@ -2332,7 +2332,7 @@ lemma E_power_mult: "(E (c::'a::{field,recpower,ring_char_0}))^n = E (of_nat n * c)" by (induct n, auto simp add: ring_simps E_add_mult power_Suc) -subsection{* Logarithmic series *} +subsubsection{* Logarithmic series *} definition "(L::'a::{field, ring_char_0,recpower} fps) = Abs_fps (\n. (- 1) ^ Suc n / of_nat n)" @@ -2366,7 +2366,7 @@ by (simp add: L_nth fps_inv_def) qed -subsection{* Formal trigonometric functions *} +subsubsection{* Formal trigonometric functions *} definition "fps_sin (c::'a::{field, recpower, ring_char_0}) = Abs_fps (\n. if even n then 0 else (- 1) ^((n - 1) div 2) * c^n /(of_nat (fact n)))" diff -r 2c0046b26f80 -r b82ab2aebbbf src/HOL/NSA/StarDef.thy --- a/src/HOL/NSA/StarDef.thy Sat Feb 14 08:45:16 2009 +0100 +++ b/src/HOL/NSA/StarDef.thy Sat Feb 14 01:24:01 2009 -0800 @@ -844,6 +844,8 @@ instance star :: (cancel_ab_semigroup_add) cancel_ab_semigroup_add by (intro_classes, transfer, rule add_imp_eq) +instance star :: (cancel_comm_monoid_add) cancel_comm_monoid_add .. + instance star :: (ab_group_add) ab_group_add apply (intro_classes) apply (transfer, rule left_minus) diff -r 2c0046b26f80 -r b82ab2aebbbf src/HOL/OrderedGroup.thy --- a/src/HOL/OrderedGroup.thy Sat Feb 14 08:45:16 2009 +0100 +++ b/src/HOL/OrderedGroup.thy Sat Feb 14 01:24:01 2009 -0800 @@ -147,6 +147,9 @@ end +class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add + + subsection {* Groups *} class group_add = minus + uminus + monoid_add + @@ -261,7 +264,7 @@ subclass group_add proof qed (simp_all add: ab_left_minus ab_diff_minus) -subclass cancel_ab_semigroup_add +subclass cancel_comm_monoid_add proof fix a b c :: 'a assume "a + b = a + c" diff -r 2c0046b26f80 -r b82ab2aebbbf src/HOL/Polynomial.thy --- a/src/HOL/Polynomial.thy Sat Feb 14 08:45:16 2009 +0100 +++ b/src/HOL/Polynomial.thy Sat Feb 14 01:24:01 2009 -0800 @@ -293,8 +293,7 @@ end -instance poly :: - ("{cancel_ab_semigroup_add,comm_monoid_add}") cancel_ab_semigroup_add +instance poly :: (cancel_comm_monoid_add) cancel_comm_monoid_add proof fix p q r :: "'a poly" assume "p + q = p + r" thus "q = r" diff -r 2c0046b26f80 -r b82ab2aebbbf src/HOL/Ring_and_Field.thy --- a/src/HOL/Ring_and_Field.thy Sat Feb 14 08:45:16 2009 +0100 +++ b/src/HOL/Ring_and_Field.thy Sat Feb 14 01:24:01 2009 -0800 @@ -41,7 +41,7 @@ class semiring_0 = semiring + comm_monoid_add + mult_zero -class semiring_0_cancel = semiring + comm_monoid_add + cancel_ab_semigroup_add +class semiring_0_cancel = semiring + cancel_comm_monoid_add begin subclass semiring_0 @@ -80,7 +80,7 @@ end -class comm_semiring_0_cancel = comm_semiring + comm_monoid_add + cancel_ab_semigroup_add +class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add begin subclass semiring_0_cancel .. @@ -198,8 +198,8 @@ class no_zero_divisors = zero + times + assumes no_zero_divisors: "a \ 0 \ b \ 0 \ a * b \ 0" -class semiring_1_cancel = semiring + comm_monoid_add + zero_neq_one - + cancel_ab_semigroup_add + monoid_mult +class semiring_1_cancel = semiring + cancel_comm_monoid_add + + zero_neq_one + monoid_mult begin subclass semiring_0_cancel .. @@ -208,8 +208,8 @@ end -class comm_semiring_1_cancel = comm_semiring + comm_monoid_add + comm_monoid_mult - + zero_neq_one + cancel_ab_semigroup_add +class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add + + zero_neq_one + comm_monoid_mult begin subclass semiring_1_cancel .. @@ -543,7 +543,7 @@ end class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add - + semiring + comm_monoid_add + cancel_ab_semigroup_add + + semiring + cancel_comm_monoid_add begin subclass semiring_0_cancel ..