# HG changeset patch # User wenzelm # Date 1380050865 -7200 # Node ID 11debf826dd6e964e11789cbdd7fb687ba722891 # Parent 65c775430caa83e601d5ed27d9212a9f084c8597# Parent 78afb4c4e6838d56fd5dfbde399a5643f6590d64 merged diff -r 65c775430caa -r 11debf826dd6 Admin/isatest/settings/mac-poly-M4 --- a/Admin/isatest/settings/mac-poly-M4 Tue Sep 24 20:58:27 2013 +0200 +++ b/Admin/isatest/settings/mac-poly-M4 Tue Sep 24 21:27:45 2013 +0200 @@ -6,7 +6,7 @@ ML_SYSTEM="polyml-5.5.1" ML_PLATFORM="x86-darwin" ML_HOME="$POLYML_HOME/$ML_PLATFORM" - ML_OPTIONS="-H 1000 --gcthreads 4" + ML_OPTIONS="-H 500 --gcthreads 4" ISABELLE_HOME_USER=~/isabelle-mac-poly-M4 diff -r 65c775430caa -r 11debf826dd6 Admin/isatest/settings/mac-poly-M8 --- a/Admin/isatest/settings/mac-poly-M8 Tue Sep 24 20:58:27 2013 +0200 +++ b/Admin/isatest/settings/mac-poly-M8 Tue Sep 24 21:27:45 2013 +0200 @@ -6,7 +6,7 @@ ML_SYSTEM="polyml-5.5.1" ML_PLATFORM="x86-darwin" ML_HOME="$POLYML_HOME/$ML_PLATFORM" - ML_OPTIONS="-H 1000 --gcthreads 8" + ML_OPTIONS="-H 500 --gcthreads 8" ISABELLE_HOME_USER=~/isabelle-mac-poly-M8 diff -r 65c775430caa -r 11debf826dd6 NEWS --- a/NEWS Tue Sep 24 20:58:27 2013 +0200 +++ b/NEWS Tue Sep 24 21:27:45 2013 +0200 @@ -57,6 +57,9 @@ *** Prover IDE -- Isabelle/Scala/jEdit *** +* Separate manual "jedit" for Isabelle/jEdit, see isabelle doc or +Documentation panel. + * Improved "Theories" panel: Continuous checking of proof document (visible and required parts) may be controlled explicitly, using check box or shortcut "C+e ENTER". Individual theory nodes may be marked diff -r 65c775430caa -r 11debf826dd6 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Sep 24 20:58:27 2013 +0200 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Sep 24 21:27:45 2013 +0200 @@ -24,9 +24,10 @@ (** move this **) lemma divide_nonneg_nonneg: + fixes a b :: real assumes "a \ 0" and "b \ 0" - shows "0 \ a / (b::real)" + shows "0 \ a / b" proof (cases "b = 0") case True then show ?thesis by auto @@ -1390,7 +1391,8 @@ fix x xa xb xc y assume as: "x = (\(b, g) x. if x = a then b else g x) xa" - "xb \ UNIV - insert a s0" "xa = (xc, y)" + "xb \ UNIV - insert a s0" + "xa = (xc, y)" "xc \ t" "\x\s0. y x \ t" "\x\UNIV - s0. y x = d" @@ -2220,7 +2222,7 @@ ultimately have *: "?A = {s, insert a3 (s - {a0})}" by blast have "s \ insert a3 (s - {a0})" - using `a3\s` by auto + using `a3 \ s` by auto then have ?thesis unfolding * by auto } @@ -3344,7 +3346,9 @@ moreover guess s using as(1)[unfolded simplex_top_face[OF assms(1) allp,symmetric]] .. then guess a .. ultimately show "\s a. ksimplex p (n + 1) s \ - a \ s \ f = s - {a} \ reduced lab (n + 1) ` f = {0..n} \ ((\j\{1..n + 1}. \x\f. x j = 0) \ (\j\{1..n + 1}. \x\f. x j = p))" (is ?ex) + a \ s \ f = s - {a} \ + reduced lab (n + 1) ` f = {0..n} \ + ((\j\{1..n + 1}. \x\f. x j = 0) \ (\j\{1..n + 1}. \x\f. x j = p))" apply (rule_tac x = s in exI) apply (rule_tac x = a in exI) unfolding complete_face_top[OF *] @@ -3354,7 +3358,8 @@ next fix f assume as: "\s a. ksimplex p (n + 1) s \ - a \ s \ f = s - {a} \ reduced lab (n + 1) ` f = {0..n} \ ((\j\{1..n + 1}. \x\f. x j = 0) \ (\j\{1..n + 1}. \x\f. x j = p))" (is ?ex) + a \ s \ f = s - {a} \ reduced lab (n + 1) ` f = {0..n} \ + ((\j\{1..n + 1}. \x\f. x j = 0) \ (\j\{1..n + 1}. \x\f. x j = p))" then guess s .. then guess a by (elim exE conjE) note sa = this { @@ -3447,7 +3452,7 @@ and "\x. \j\{1..Suc n}. (\j. x j \ p) \ x j = 0 \ lab x j = 0" and "\x. \j\{1..Suc n}. (\j. x j \ p) \ x j = p \ lab x j = 1" and "odd (card {f. ksimplex p n f \ reduced lab n ` f = {0..n}})" - shows "odd (card {s. ksimplex p (Suc n) s \ reduced lab (Suc n) ` s = {0..Suc n}})" + shows "odd (card {s. ksimplex p (Suc n) s \ reduced lab (Suc n) ` s = {0..Suc n}})" using assms unfolding Suc_eq_plus1 by (rule kuhn_induction) @@ -4255,7 +4260,7 @@ lemma interval_bij_bij: "\(i::'a::ordered_euclidean_space)\Basis. a\i < b\i \ u\i < v\i \ - interval_bij (a,b) (u,v) (interval_bij (u,v) (a,b) x) = x" + interval_bij (a, b) (u, v) (interval_bij (u, v) (a, b) x) = x" by (auto simp: interval_bij_def euclidean_eq_iff[where 'a='a]) end diff -r 65c775430caa -r 11debf826dd6 src/HOL/Multivariate_Analysis/Determinants.thy --- a/src/HOL/Multivariate_Analysis/Determinants.thy Tue Sep 24 20:58:27 2013 +0200 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy Tue Sep 24 21:27:45 2013 +0200 @@ -20,20 +20,26 @@ done lemma setprod_add_split: - assumes mn: "(m::nat) <= n + 1" - shows "setprod f {m.. n+p} = setprod f {m .. n} * setprod f {n+1..n+p}" + fixes m n :: nat + assumes mn: "m \ n + 1" + shows "setprod f {m..n+p} = setprod f {m .. n} * setprod f {n+1..n+p}" proof - - let ?A = "{m .. n+p}" - let ?B = "{m .. n}" + let ?A = "{m..n+p}" + let ?B = "{m..n}" let ?C = "{n+1..n+p}" - from mn have un: "?B \ ?C = ?A" by auto - from mn have dj: "?B \ ?C = {}" by auto - have f: "finite ?B" "finite ?C" by simp_all + from mn have un: "?B \ ?C = ?A" + by auto + from mn have dj: "?B \ ?C = {}" + by auto + have f: "finite ?B" "finite ?C" + by simp_all from setprod_Un_disjoint[OF f dj, of f, unfolded un] show ?thesis . qed -lemma setprod_offset: "setprod f {(m::nat) + p .. n + p} = setprod (\i. f (i + p)) {m..n}" +lemma setprod_offset: + fixes m n :: nat + shows "setprod f {m + p .. n + p} = setprod (\i. f (i + p)) {m..n}" apply (rule setprod_reindex_cong[where f="op + p"]) apply (auto simp add: image_iff Bex_def inj_on_def) apply presburger @@ -44,7 +50,9 @@ lemma setprod_singleton: "setprod f {x} = f x" by simp -lemma setprod_singleton_nat_seg: "setprod f {n..n} = f (n::'a::order)" +lemma setprod_singleton_nat_seg: + fixes n :: "'a::order" + shows "setprod f {n..n} = f n" by simp lemma setprod_numseg: @@ -54,8 +62,9 @@ by (auto simp add: atLeastAtMostSuc_conv) lemma setprod_le: + fixes f g :: "'b \ 'a::linordered_idom" assumes fS: "finite S" - and fg: "\x\S. f x \ 0 \ f x \ (g x :: 'a::linordered_idom)" + and fg: "\x\S. f x \ 0 \ f x \ g x" shows "setprod f S \ setprod g S" using fS fg apply (induct S) @@ -65,7 +74,7 @@ apply (auto intro: setprod_nonneg) done - (* FIXME: In Finite_Set there is a useless further assumption *) +(* FIXME: In Finite_Set there is a useless further assumption *) lemma setprod_inversef: "finite A \ setprod (inverse \ f) A = (inverse (setprod f A) :: 'a:: field_inverse_zero)" apply (erule finite_induct) @@ -74,8 +83,9 @@ done lemma setprod_le_1: + fixes f :: "'b \ 'a::linordered_idom" assumes fS: "finite S" - and f: "\x\S. f x \ 0 \ f x \ (1::'a::linordered_idom)" + and f: "\x\S. f x \ 0 \ f x \ 1" shows "setprod f S \ 1" using setprod_le[OF fS f] unfolding setprod_1 . @@ -85,10 +95,10 @@ definition trace :: "'a::semiring_1^'n^'n \ 'a" where "trace A = setsum (\i. ((A$i)$i)) (UNIV::'n set)" -lemma trace_0: "trace(mat 0) = 0" +lemma trace_0: "trace (mat 0) = 0" by (simp add: trace_def mat_def) -lemma trace_I: "trace(mat 1 :: 'a::semiring_1^'n^'n) = of_nat(CARD('n))" +lemma trace_I: "trace (mat 1 :: 'a::semiring_1^'n^'n) = of_nat(CARD('n))" by (simp add: trace_def mat_def) lemma trace_add: "trace ((A::'a::comm_semiring_1^'n^'n) + B) = trace A + trace B" @@ -97,37 +107,32 @@ lemma trace_sub: "trace ((A::'a::comm_ring_1^'n^'n) - B) = trace A - trace B" by (simp add: trace_def setsum_subtractf) -lemma trace_mul_sym:"trace ((A::'a::comm_semiring_1^'n^'m) ** B) = trace (B**A)" +lemma trace_mul_sym: "trace ((A::'a::comm_semiring_1^'n^'m) ** B) = trace (B**A)" apply (simp add: trace_def matrix_matrix_mult_def) apply (subst setsum_commute) apply (simp add: mult_commute) done -(* ------------------------------------------------------------------------- *) -(* Definition of determinant. *) -(* ------------------------------------------------------------------------- *) +text {* Definition of determinant. *} definition det:: "'a::comm_ring_1^'n^'n \ 'a" where "det A = setsum (\p. of_int (sign p) * setprod (\i. A$i$p i) (UNIV :: 'n set)) {p. p permutes (UNIV :: 'n set)}" -(* ------------------------------------------------------------------------- *) -(* A few general lemmas we need below. *) -(* ------------------------------------------------------------------------- *) +text {* A few general lemmas we need below. *} lemma setprod_permute: assumes p: "p permutes S" - shows "setprod f S = setprod (f o p) S" + shows "setprod f S = setprod (f \ p) S" using assms by (fact setprod.permute) lemma setproduct_permute_nat_interval: - "p permutes {m::nat .. n} ==> setprod f {m..n} = setprod (f o p) {m..n}" + fixes m n :: nat + shows "p permutes {m..n} \ setprod f {m..n} = setprod (f \ p) {m..n}" by (blast intro!: setprod_permute) -(* ------------------------------------------------------------------------- *) -(* Basic determinant properties. *) -(* ------------------------------------------------------------------------- *) +text {* Basic determinant properties. *} lemma det_transpose: "det (transpose A) = det (A::'a::comm_ring_1 ^'n^'n)" proof - @@ -137,15 +142,18 @@ { fix p assume p: "p \ {p. p permutes ?U}" - from p have pU: "p permutes ?U" by blast + from p have pU: "p permutes ?U" + by blast have sth: "sign (inv p) = sign p" by (metis sign_inverse fU p mem_Collect_eq permutation_permutes) from permutes_inj[OF pU] - have pi: "inj_on p ?U" by (blast intro: subset_inj_on) + have pi: "inj_on p ?U" + by (blast intro: subset_inj_on) from permutes_image[OF pU] have "setprod (\i. ?di (transpose A) i (inv p i)) ?U = - setprod (\i. ?di (transpose A) i (inv p i)) (p ` ?U)" by simp - also have "\ = setprod ((\i. ?di (transpose A) i (inv p i)) o p) ?U" + setprod (\i. ?di (transpose A) i (inv p i)) (p ` ?U)" + by simp + also have "\ = setprod ((\i. ?di (transpose A) i (inv p i)) \ p) ?U" unfolding setprod_reindex[OF pi] .. also have "\ = setprod (\i. ?di A i (p i)) ?U" proof - @@ -153,14 +161,16 @@ fix i assume i: "i \ ?U" from i permutes_inv_o[OF pU] permutes_in_image[OF pU] - have "((\i. ?di (transpose A) i (inv p i)) o p) i = ?di A i (p i)" + have "((\i. ?di (transpose A) i (inv p i)) \ p) i = ?di A i (p i)" unfolding transpose_def by (simp add: fun_eq_iff) } - then show "setprod ((\i. ?di (transpose A) i (inv p i)) o p) ?U = - setprod (\i. ?di A i (p i)) ?U" by (auto intro: setprod_cong) + then show "setprod ((\i. ?di (transpose A) i (inv p i)) \ p) ?U = + setprod (\i. ?di A i (p i)) ?U" + by (auto intro: setprod_cong) qed finally have "of_int (sign (inv p)) * (setprod (\i. ?di (transpose A) i (inv p i)) ?U) = - of_int (sign p) * (setprod (\i. ?di A i (p i)) ?U)" using sth by simp + of_int (sign p) * (setprod (\i. ?di A i (p i)) ?U)" + using sth by simp } then show ?thesis unfolding det_def @@ -178,12 +188,14 @@ let ?U = "UNIV:: 'n set" let ?PU = "{p. p permutes ?U}" let ?pp = "\p. of_int (sign p) * setprod (\i. A$i$p i) (UNIV :: 'n set)" - have fU: "finite ?U" by simp + have fU: "finite ?U" + by simp from finite_permutations[OF fU] have fPU: "finite ?PU" . - have id0: "{id} \ ?PU" by (auto simp add: permutes_id) + have id0: "{id} \ ?PU" + by (auto simp add: permutes_id) { fix p - assume p: "p \ ?PU -{id}" + assume p: "p \ ?PU - {id}" from p have pU: "p permutes ?U" and pid: "p \ id" by blast+ from permutes_natset_le[OF pU] pid obtain i where i: "p i > i" @@ -193,7 +205,7 @@ from setprod_zero[OF fU ex] have "?pp p = 0" by simp } - then have p0: "\p \ ?PU -{id}. ?pp p = 0" + then have p0: "\p \ ?PU - {id}. ?pp p = 0" by blast from setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis unfolding det_def by (simp add: sign_id) @@ -207,18 +219,22 @@ let ?U = "UNIV:: 'n set" let ?PU = "{p. p permutes ?U}" let ?pp = "(\p. of_int (sign p) * setprod (\i. A$i$p i) (UNIV :: 'n set))" - have fU: "finite ?U" by simp + have fU: "finite ?U" + by simp from finite_permutations[OF fU] have fPU: "finite ?PU" . - have id0: "{id} \ ?PU" by (auto simp add: permutes_id) + have id0: "{id} \ ?PU" + by (auto simp add: permutes_id) { fix p - assume p: "p \ ?PU -{id}" + assume p: "p \ ?PU - {id}" from p have pU: "p permutes ?U" and pid: "p \ id" by blast+ from permutes_natset_ge[OF pU] pid obtain i where i: "p i < i" by (metis not_le) - from ld[OF i] have ex:"\i \ ?U. A$i$p i = 0" by blast - from setprod_zero[OF fU ex] have "?pp p = 0" by simp + from ld[OF i] have ex:"\i \ ?U. A$i$p i = 0" + by blast + from setprod_zero[OF fU ex] have "?pp p = 0" + by simp } then have p0: "\p \ ?PU -{id}. ?pp p = 0" by blast @@ -236,15 +252,22 @@ let ?pp = "\p. of_int (sign p) * setprod (\i. A$i$p i) (UNIV :: 'n set)" have fU: "finite ?U" by simp from finite_permutations[OF fU] have fPU: "finite ?PU" . - have id0: "{id} \ ?PU" by (auto simp add: permutes_id) + have id0: "{id} \ ?PU" + by (auto simp add: permutes_id) { fix p assume p: "p \ ?PU - {id}" - then have "p \ id" by simp - then obtain i where i: "p i \ i" unfolding fun_eq_iff by auto - from ld [OF i [symmetric]] have ex:"\i \ ?U. A$i$p i = 0" by blast - from setprod_zero [OF fU ex] have "?pp p = 0" by simp} - then have p0: "\p \ ?PU - {id}. ?pp p = 0" by blast + then have "p \ id" + by simp + then obtain i where i: "p i \ i" + unfolding fun_eq_iff by auto + from ld [OF i [symmetric]] have ex:"\i \ ?U. A$i$p i = 0" + by blast + from setprod_zero [OF fU ex] have "?pp p = 0" + by simp + } + then have p0: "\p \ ?PU - {id}. ?pp p = 0" + by blast from setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis unfolding det_def by (simp add: sign_id) qed @@ -257,18 +280,21 @@ { fix i assume i: "i \ ?U" - have "?f i i = 1" using i by (vector mat_def) + have "?f i i = 1" + using i by (vector mat_def) } then have th: "setprod (\i. ?f i i) ?U = setprod (\x. 1) ?U" by (auto intro: setprod_cong) { fix i j assume i: "i \ ?U" and j: "j \ ?U" and ij: "i \ j" - have "?f i j = 0" using i j ij by (vector mat_def) + have "?f i j = 0" using i j ij + by (vector mat_def) } - then have "det ?A = setprod (\i. ?f i i) ?U" using det_diagonal - by blast - also have "\ = 1" unfolding th setprod_1 .. + then have "det ?A = setprod (\i. ?f i i) ?U" + using det_diagonal by blast + also have "\ = 1" + unfolding th setprod_1 .. finally show ?thesis . qed @@ -278,7 +304,7 @@ lemma det_permute_rows: fixes A :: "'a::comm_ring_1^'n^'n" assumes p: "p permutes (UNIV :: 'n::finite set)" - shows "det(\ i. A$p i :: 'a^'n^'n) = of_int (sign p) * det A" + shows "det (\ i. A$p i :: 'a^'n^'n) = of_int (sign p) * det A" apply (simp add: det_def setsum_right_distrib mult_assoc[symmetric]) apply (subst sum_permutations_compose_right[OF p]) proof (rule setsum_cong2) @@ -286,21 +312,22 @@ let ?PU = "{p. p permutes ?U}" fix q assume qPU: "q \ ?PU" - have fU: "finite ?U" by simp + have fU: "finite ?U" + by simp from qPU have q: "q permutes ?U" by blast from p q have pp: "permutation p" and qp: "permutation q" by (metis fU permutation_permutes)+ from permutes_inv[OF p] have ip: "inv p permutes ?U" . - have "setprod (\i. A$p i$ (q o p) i) ?U = setprod ((\i. A$p i$(q o p) i) o inv p) ?U" + have "setprod (\i. A$p i$ (q \ p) i) ?U = setprod ((\i. A$p i$(q \ p) i) \ inv p) ?U" by (simp only: setprod_permute[OF ip, symmetric]) - also have "\ = setprod (\i. A $ (p o inv p) i $ (q o (p o inv p)) i) ?U" + also have "\ = setprod (\i. A $ (p \ inv p) i $ (q \ (p \ inv p)) i) ?U" by (simp only: o_def) also have "\ = setprod (\i. A$i$q i) ?U" by (simp only: o_def permutes_inverses[OF p]) - finally have thp: "setprod (\i. A$p i$ (q o p) i) ?U = setprod (\i. A$i$q i) ?U" + finally have thp: "setprod (\i. A$p i$ (q \ p) i) ?U = setprod (\i. A$i$q i) ?U" by blast - show "of_int (sign (q o p)) * setprod (\i. A$ p i$ (q o p) i) ?U = + show "of_int (sign (q \ p)) * setprod (\i. A$ p i$ (q \ p) i) ?U = of_int (sign p) * of_int (sign q) * setprod (\i. A$i$q i) ?U" by (simp only: thp sign_compose[OF qp pp] mult_commute of_int_mult) qed @@ -317,7 +344,8 @@ moreover have "?Ap = transpose (\ i. transpose A $ p i)" by (simp add: transpose_def vec_eq_iff) - ultimately show ?thesis by simp + ultimately show ?thesis + by simp qed lemma det_identical_rows: @@ -372,7 +400,7 @@ shows "det((\ i. if i = k then a i + b i else c i)::'a::comm_ring_1^'n^'n) = det((\ i. if i = k then a i else c i)::'a::comm_ring_1^'n^'n) + det((\ i. if i = k then b i else c i)::'a::comm_ring_1^'n^'n)" - unfolding det_def vec_lambda_beta setsum_addf[symmetric] + unfolding det_def vec_lambda_beta setsum_addf[symmetric] proof (rule setsum_cong2) let ?U = "UNIV :: 'n set" let ?pU = "{p. p permutes ?U}" @@ -382,8 +410,10 @@ fix p assume p: "p \ ?pU" let ?Uk = "?U - {k}" - from p have pU: "p permutes ?U" by blast - have kU: "?U = insert k ?Uk" by blast + from p have pU: "p permutes ?U" + by blast + have kU: "?U = insert k ?Uk" + by blast { fix j assume j: "j \ ?Uk" @@ -395,10 +425,11 @@ apply - apply (rule setprod_cong, simp_all)+ done - have th3: "finite ?Uk" "k \ ?Uk" by auto + have th3: "finite ?Uk" "k \ ?Uk" + by auto have "setprod (\i. ?f i $ p i) ?U = setprod (\i. ?f i $ p i) (insert k ?Uk)" unfolding kU[symmetric] .. - also have "\ = ?f k $ p k * setprod (\i. ?f i $ p i) ?Uk" + also have "\ = ?f k $ p k * setprod (\i. ?f i $ p i) ?Uk" apply (rule setprod_insert) apply simp apply blast @@ -409,8 +440,8 @@ by (metis th1 th2) also have "\ = setprod (\i. ?g i $ p i) (insert k ?Uk) + setprod (\i. ?h i $ p i) (insert k ?Uk)" unfolding setprod_insert[OF th3] by simp - finally have "setprod (\i. ?f i $ p i) ?U = - setprod (\i. ?g i $ p i) ?U + setprod (\i. ?h i $ p i) ?U" unfolding kU[symmetric] . + finally have "setprod (\i. ?f i $ p i) ?U = setprod (\i. ?g i $ p i) ?U + setprod (\i. ?h i $ p i) ?U" + unfolding kU[symmetric] . then show "of_int (sign p) * setprod (\i. ?f i $ p i) ?U = of_int (sign p) * setprod (\i. ?g i $ p i) ?U + of_int (sign p) * setprod (\i. ?h i $ p i) ?U" by (simp add: field_simps) @@ -429,19 +460,23 @@ fix p assume p: "p \ ?pU" let ?Uk = "?U - {k}" - from p have pU: "p permutes ?U" by blast - have kU: "?U = insert k ?Uk" by blast + from p have pU: "p permutes ?U" + by blast + have kU: "?U = insert k ?Uk" + by blast { fix j assume j: "j \ ?Uk" - from j have "?f j $ p j = ?g j $ p j" by simp + from j have "?f j $ p j = ?g j $ p j" + by simp } then have th1: "setprod (\i. ?f i $ p i) ?Uk = setprod (\i. ?g i $ p i) ?Uk" apply - apply (rule setprod_cong) apply simp_all done - have th3: "finite ?Uk" "k \ ?Uk" by auto + have th3: "finite ?Uk" "k \ ?Uk" + by auto have "setprod (\i. ?f i $ p i) ?U = setprod (\i. ?f i $ p i) (insert k ?Uk)" unfolding kU[symmetric] .. also have "\ = ?f k $ p k * setprod (\i. ?f i $ p i) ?Uk" @@ -495,7 +530,8 @@ let ?P = "\x. ?d (row i A + x) = det A" { fix k - have "(if k = i then row i A + 0 else row k A) = row k A" by simp + have "(if k = i then row i A + 0 else row k A) = row k A" + by simp } then have P0: "?P 0" apply - @@ -506,9 +542,11 @@ { fix c z y assume zS: "z \ ?S" and Py: "?P y" - from zS obtain j where j: "z = row j A" "i \ j" by blast + from zS obtain j where j: "z = row j A" "i \ j" + by blast let ?w = "row i A + y" - have th0: "row i A + (c*s z + y) = ?w + c*s z" by vector + have th0: "row i A + (c*s z + y) = ?w + c*s z" + by vector have thz: "?d z = 0" apply (rule det_identical_rows[OF j(2)]) using j @@ -528,10 +566,10 @@ done qed -(* ------------------------------------------------------------------------- *) -(* May as well do this, though it's a bit unsatisfactory since it ignores *) -(* exact duplicates by considering the rows/columns as a set. *) -(* ------------------------------------------------------------------------- *) +text {* + May as well do this, though it's a bit unsatisfactory since it ignores + exact duplicates by considering the rows/columns as a set. +*} lemma det_dependent_rows: fixes A:: "real^'n^'n" @@ -571,9 +609,7 @@ shows "det A = 0" by (metis d det_dependent_rows rows_transpose det_transpose) -(* ------------------------------------------------------------------------- *) -(* Multilinearity and the multiplication formula. *) -(* ------------------------------------------------------------------------- *) +text {* Multilinearity and the multiplication formula. *} lemma Cart_lambda_cong: "(\x. f x = g x) \ (vec_lambda f::'a^'n) = (vec_lambda g :: 'a^'n)" by (rule iffD1[OF vec_lambda_unique]) vector @@ -600,8 +636,10 @@ shows "finite {f. (\i \ {1.. (k::nat)}. f i \ S) \ (\i. i \ {1 .. k} \ f i = i)}" proof (induct k) case 0 - have th: "{f. \i. f i = i} = {id}" by auto - show ?case by (auto simp add: th) + have th: "{f. \i. f i = i} = {id}" + by auto + show ?case + by (auto simp add: th) next case (Suc k) let ?f = "\(y::nat,g) i. if i = Suc k then y else g i" @@ -613,15 +651,18 @@ apply auto done with finite_imageI[OF finite_cartesian_product[OF fS Suc.hyps(1)], of ?f] - show ?case by metis + show ?case + by metis qed -lemma eq_id_iff[simp]: "(\x. f x = x) = (f = id)" by auto +lemma eq_id_iff[simp]: "(\x. f x = x) \ f = id" + by auto lemma det_linear_rows_setsum_lemma: - assumes fS: "finite S" and fT: "finite T" - shows "det((\ i. if i \ T then setsum (a i) S else c i):: 'a::comm_ring_1^'n^'n) = + assumes fS: "finite S" + and fT: "finite T" + shows "det ((\ i. if i \ T then setsum (a i) S else c i):: 'a::comm_ring_1^'n^'n) = setsum (\f. det((\ i. if i \ T then a i (f i) else c i)::'a^'n^'n)) {f. (\i \ T. f i \ S) \ (\i. i \ T \ f i = i)}" using fT @@ -629,7 +670,8 @@ case empty have th0: "\x y. (\ i. if i \ {} then x i else y i) = (\ i. y i)" by vector - from empty.prems show ?case unfolding th0 by simp + from empty.prems show ?case + unfolding th0 by simp next case (insert z T a c) let ?F = "\T. {f. (\i \ T. f i \ S) \ (\i. i \ T \ f i = i)}" @@ -671,7 +713,8 @@ qed lemma det_linear_rows_setsum: - assumes fS: "finite (S::'n::finite set)" + fixes S :: "'n::finite set" + assumes fS: "finite S" shows "det (\ i. setsum (a i) S) = setsum (\f. det (\ i. a i (f i) :: 'a::comm_ring_1 ^ 'n^'n)) {f. \i. f i \ S}" proof - @@ -700,7 +743,8 @@ have "setprod (\i. c i * a i $ p i) ?U = setprod c ?U * setprod (\i. a i $ p i) ?U" unfolding setprod_timesf .. then show "?s * (\xa\?U. c xa * a xa $ p xa) = - setprod c ?U * (?s* (\xa\?U. a xa $ p xa))" by (simp add: field_simps) + setprod c ?U * (?s* (\xa\?U. a xa $ p xa))" + by (simp add: field_simps) qed lemma det_mul: @@ -710,19 +754,22 @@ let ?U = "UNIV :: 'n set" let ?F = "{f. (\i\ ?U. f i \ ?U) \ (\i. i \ ?U \ f i = i)}" let ?PU = "{p. p permutes ?U}" - have fU: "finite ?U" by simp - have fF: "finite ?F" by (rule finite) + have fU: "finite ?U" + by simp + have fF: "finite ?F" + by (rule finite) { fix p assume p: "p permutes ?U" have "p \ ?F" unfolding mem_Collect_eq permutes_in_image[OF p] using p[unfolded permutes_def] by simp } - then have PUF: "?PU \ ?F" by blast + then have PUF: "?PU \ ?F" by blast { fix f assume fPU: "f \ ?F - ?PU" - have fUU: "f ` ?U \ ?U" using fPU by auto + have fUU: "f ` ?U \ ?U" + using fPU by auto from fPU have f: "\i \ ?U. f i \ ?U" "\i. i \ ?U \ f i = i" "\(\y. \!x. f x = y)" unfolding permutes_def by auto @@ -733,7 +780,8 @@ then obtain i j where ij: "f i = f j" "i \ j" unfolding inj_on_def by blast from ij - have rth: "row i ?B = row j ?B" by (vector row_def) + have rth: "row i ?B = row j ?B" + by (vector row_def) from det_identical_rows[OF ij(2) rth] have "det (\ i. A$i$f i *s B$f i) = 0" unfolding det_rows_mul by simp @@ -744,48 +792,56 @@ from f fi have fith: "\i j. f i = f j \ i = j" unfolding inj_on_def by metis note fs = fi[unfolded surjective_iff_injective_gen[OF fU fU refl fUU, symmetric]] - { fix y - from fs f have "\x. f x = y" by blast - then obtain x where x: "f x = y" by blast + from fs f have "\x. f x = y" + by blast + then obtain x where x: "f x = y" + by blast { fix z assume z: "f z = y" - from fith x z have "z = x" by metis + from fith x z have "z = x" + by metis } - with x have "\!x. f x = y" by blast + with x have "\!x. f x = y" + by blast } - with f(3) have "det (\ i. A$i$f i *s B$f i) = 0" by blast + with f(3) have "det (\ i. A$i$f i *s B$f i) = 0" + by blast } - ultimately have "det (\ i. A$i$f i *s B$f i) = 0" by blast + ultimately have "det (\ i. A$i$f i *s B$f i) = 0" + by blast } - hence zth: "\ f\ ?F - ?PU. det (\ i. A$i$f i *s B$f i) = 0" + then have zth: "\ f\ ?F - ?PU. det (\ i. A$i$f i *s B$f i) = 0" by simp { fix p assume pU: "p \ ?PU" - from pU have p: "p permutes ?U" by blast + from pU have p: "p permutes ?U" + by blast let ?s = "\p. of_int (sign p)" let ?f = "\q. ?s p * (\i\ ?U. A $ i $ p i) * (?s q * (\i\ ?U. B $ i $ q i))" have "(setsum (\q. ?s q * (\i\ ?U. (\ i. A $ i $ p i *s B $ p i :: 'a^'n^'n) $ i $ q i)) ?PU) = (setsum (\q. ?s p * (\i\ ?U. A $ i $ p i) * (?s q * (\i\ ?U. B $ i $ q i))) ?PU)" unfolding sum_permutations_compose_right[OF permutes_inv[OF p], of ?f] - proof(rule setsum_cong2) + proof (rule setsum_cong2) fix q assume qU: "q \ ?PU" - hence q: "q permutes ?U" by blast + then have q: "q permutes ?U" + by blast from p q have pp: "permutation p" and pq: "permutation q" unfolding permutation_permutes by auto have th00: "of_int (sign p) * of_int (sign p) = (1::'a)" "\a. of_int (sign p) * (of_int (sign p) * a) = a" - unfolding mult_assoc[symmetric] unfolding of_int_mult[symmetric] + unfolding mult_assoc[symmetric] + unfolding of_int_mult[symmetric] by (simp_all add: sign_idempotent) - have ths: "?s q = ?s p * ?s (q o inv p)" + have ths: "?s q = ?s p * ?s (q \ inv p)" using pp pq permutation_inverse[OF pp] sign_inverse[OF pp] by (simp add: th00 mult_ac sign_idempotent sign_compose) - have th001: "setprod (\i. B$i$ q (inv p i)) ?U = setprod ((\i. B$i$ q (inv p i)) o p) ?U" + have th001: "setprod (\i. B$i$ q (inv p i)) ?U = setprod ((\i. B$i$ q (inv p i)) \ p) ?U" by (rule setprod_permute[OF p]) have thp: "setprod (\i. (\