Commit fe5e5b37 authored by haftmann's avatar haftmann
Browse files

collected lemmas on permutations

parent 30f9c323e6d0
......@@ -877,7 +877,7 @@ proof -
define f where "f = (\<lambda> \<sigma>. signof \<sigma> * (\<Prod>i=0..<m+n. M $$ (i, \<sigma> i)))"
have "degree (f \<pi>) = degree (\<Prod>i=0..<m + n. M $$ (i, \<pi> i))"
using nz by (auto simp: f_def degree_mult_eq signof_def)
using nz by (auto simp: f_def degree_mult_eq sign_def)
also have "\<dots> = (\<Sum>i=0..<m+n. degree (M $$ (i, \<pi> i)))"
using nz by (subst degree_prod_eq_sum_degree) auto
also have "\<dots> = (\<Sum>i<n. degree (M $$ (i, \<pi> i))) + (\<Sum>i<m. degree (M $$ (n + i, \<pi> (n + i))))"
......@@ -902,7 +902,7 @@ proof -
from that have \<sigma>_less: "\<sigma> i < m + n" if "i < m + n" for i
using permutes_in_image[OF \<open>\<sigma> permutes _\<close>] that by auto
have "degree (f \<sigma>) = degree (\<Prod>i=0..<m + n. M $$ (i, \<sigma> i))"
using nz by (auto simp: f_def degree_mult_eq signof_def)
using nz by (auto simp: f_def degree_mult_eq sign_def)
also have "\<dots> = (\<Sum>i=0..<m+n. degree (M $$ (i, \<sigma> i)))"
using nz by (subst degree_prod_eq_sum_degree) auto
also have "\<dots> = (\<Sum>i<n. degree (M $$ (i, \<sigma> i))) + (\<Sum>i<m. degree (M $$ (n + i, \<sigma> (n + i))))"
......@@ -1019,7 +1019,7 @@ proof -
have "lead_coeff (f \<pi>) = poly_add_sign m n"
proof -
have "lead_coeff (f \<pi>) = signof \<pi> * (\<Prod>i=0..<m + n. lead_coeff (M $$ (i, \<pi> i)))"
by (simp add: f_def signof_def lead_coeff_prod)
by (simp add: f_def sign_def lead_coeff_prod)
also have "(\<Prod>i=0..<m + n. lead_coeff (M $$ (i, \<pi> i))) =
(\<Prod>i<n. lead_coeff (M $$ (i, \<pi> i))) * (\<Prod>i<m. lead_coeff (M $$ (n + i, \<pi> (n + i))))"
by (subst indices_eq, subst prod.union_disjoint) (auto simp: prod.reindex)
......@@ -1075,7 +1075,7 @@ proof -
define f where "f = (\<lambda> \<sigma>. signof \<sigma> * (\<Prod>i=0..<m+n. M $$ (i, \<sigma> i)))"
have "degree (f id) = degree (\<Prod>i=0..<m + n. M $$ (i, i))"
using nz by (auto simp: f_def degree_mult_eq signof_def)
using nz by (auto simp: f_def degree_mult_eq sign_def)
also have "\<dots> = (\<Sum>i=0..<m+n. degree (M $$ (i, i)))"
using nz by (subst degree_prod_eq_sum_degree) auto
also have "\<dots> = (\<Sum>i<n. degree (M $$ (i, i))) + (\<Sum>i<m. degree (M $$ (n + i, n + i)))"
......@@ -1101,7 +1101,7 @@ proof -
from that have \<sigma>_less: "\<sigma> i < m + n" if "i < m + n" for i
using permutes_in_image[OF \<open>\<sigma> permutes _\<close>] that by auto
have "degree (f \<sigma>) = degree (\<Prod>i=0..<m + n. M $$ (i, \<sigma> i))"
using nz by (auto simp: f_def degree_mult_eq signof_def)
using nz by (auto simp: f_def degree_mult_eq sign_def)
also have "\<dots> = (\<Sum>i=0..<m+n. degree (M $$ (i, \<sigma> i)))"
using nz by (subst degree_prod_eq_sum_degree) auto
also have "\<dots> = (\<Sum>i<n. degree (M $$ (i, \<sigma> i))) + (\<Sum>i<m. degree (M $$ (n + i, \<sigma> (n + i))))"
......@@ -1175,7 +1175,7 @@ proof -
have "lead_coeff (f id) = 1"
proof -
have "lead_coeff (f id) = (\<Prod>i=0..<m + n. lead_coeff (M $$ (i, i)))"
by (simp add: f_def signof_def lead_coeff_prod sign_id)
by (simp add: f_def lead_coeff_prod)
also have "(\<Prod>i=0..<m + n. lead_coeff (M $$ (i, i))) =
(\<Prod>i<n. lead_coeff (M $$ (i, i))) * (\<Prod>i<m. lead_coeff (M $$ (n + i, n + i)))"
by (subst indices_eq, subst prod.union_disjoint) (auto simp: prod.reindex)
......@@ -1221,7 +1221,7 @@ proof -
define r where "r = poly_add_sign (degree p) (degree q) * poly_add p q"
have "lead_coeff r = 1" using p q deg_pos
by (simp add: r_def lead_coeff_mult poly_add_sign_def signof_def lead_coeff_poly_add)
by (simp add: r_def lead_coeff_mult poly_add_sign_def sign_def lead_coeff_poly_add)
moreover have "ipoly r (x + y) = 0"
using p q by (simp add: ipoly_poly_add r_def of_int_poly_hom.hom_mult)
ultimately show ?thesis
......
......@@ -236,7 +236,8 @@ proof -
let ?r = "\<Prod>i = 0..<n. A $$ (i, x i)"
have id: "?l = ?r"
by (rule prod.cong[OF refl poly], insert x, auto)
show "poly (signof x) k * ?l = signof x * ?r" unfolding id signof_def by auto
show "poly (signof x) k * ?l = signof x * ?r"
by (cases x rule: sign_cases) (simp_all add: id)
qed
qed
......@@ -362,7 +363,7 @@ proof -
qed
lemma degree_signof_mult[simp]: "degree (signof p * q) = degree q"
by (cases "sign p = 1", auto simp: signof_def)
by (cases p rule: sign_cases) simp_all
lemma degree_monic_char_poly: assumes A: "A \<in> carrier_mat n n"
shows "degree (char_poly A) = n \<and> coeff (char_poly A) n = 1"
......@@ -456,7 +457,8 @@ proof -
{
fix p
assume p: "p permutes {0 ..< n}"
have "pderiv (signof p :: 'a poly) = 0" unfolding signof_def by (simp add: pderiv_minus)
have "pderiv (signof p :: 'a poly) = 0"
by (cases p rule: sign_cases) (simp_all add: pderiv_minus)
hence "pderiv (signof p * ?e p) = signof p * pderiv (\<Prod>i = 0..<n. Sum $$ (i, p i))"
unfolding pderiv_mult by auto
also have "signof p * pderiv (\<Prod>i = 0..<n. Sum $$ (i, p i)) =
......
......@@ -15,7 +15,7 @@ is non-empty is available for integral domains, not just for fields.\<close>
theory Determinant
imports
Missing_Permutations
Missing_Misc
Column_Operations
"HOL-Computational_Algebra.Polynomial_Factorial" (* Only for to_fract. Probably not the right place. *)
Polynomial_Interpolation.Ring_Hom
......@@ -27,7 +27,7 @@ definition det:: "'a mat \<Rightarrow> 'a :: comm_ring_1" where
signof p * (\<Prod> i = 0 ..< dim_row A. A $$ (i, p i))) else 0)"
lemma(in ring_hom) hom_signof[simp]: "hom (signof p) = signof p"
unfolding signof_def by (auto simp: hom_distribs)
by (simp add: hom_uminus sign_def)
lemma(in comm_ring_hom) hom_det[simp]: "det (map_mat hom A) = hom (det A)"
unfolding det_def by (auto simp: hom_distribs)
......@@ -177,8 +177,7 @@ proof -
qed
lemma det_dim_zero[simp]: "A \<in> carrier_mat 0 0 \<Longrightarrow> det A = 1"
unfolding det_def carrier_mat_def signof_def sign_def by auto
unfolding det_def carrier_mat_def sign_def by auto
lemma det_lower_triangular:
assumes ld: "\<And>i j. i < j \<Longrightarrow> j < n \<Longrightarrow> A $$ (i,j) = 0"
......@@ -250,7 +249,7 @@ proof -
by (rule permutes_swap_id, insert k l, auto)
show ?thesis
by (rule trans[OF trans[OF _ det_permute_rows[OF one_carrier_mat[of n] p]]],
subst swap_rows_mat_eq_permute[OF k l], auto simp: signof_def sign_swap_id kl)
subst swap_rows_mat_eq_permute[OF k l], auto simp: sign_swap_id kl)
qed
lemma det_addrow_mat:
......@@ -283,12 +282,12 @@ lemma det_identical_rows:
proof-
let ?p = "Fun.swap i j id"
let ?n = "{0 ..< n}"
have sp: "signof ?p = - 1" "sign ?p = -1" unfolding signof_def using ij
have sp: "signof ?p = - 1" "sign ?p = (- 1 :: int)" using ij
by (auto simp add: sign_swap_id)
let ?f = "\<lambda> p. signof p * (\<Prod>i\<in>?n. A $$ (p i, i))"
let ?all = "{p. p permutes ?n}"
let ?one = "{p. p permutes ?n \<and> sign p = 1}"
let ?none = "{p. p permutes ?n \<and> sign p \<noteq> 1}"
let ?one = "{p. p permutes ?n \<and> sign p = (1 :: int)}"
let ?none = "{p. p permutes ?n \<and> sign p \<noteq> (1 :: int)}"
let ?pone = "(\<lambda> p. ?p o p) ` ?one"
have split: "?one \<union> ?none = ?all" by auto
have p: "?p permutes ?n" by (rule permutes_swap_id, insert i j, auto)
......@@ -317,7 +316,7 @@ proof-
{
fix q
assume "q \<in> ?none"
hence q: "q permutes ?n" and sq: "sign q = -1" unfolding sign_def by auto
hence q: "q permutes ?n" and sq: "sign q = (- 1 :: int)" unfolding sign_def by auto
from permutes_compose[OF q p] sign_compose[OF pp[OF p] pp[OF q], unfolded sp sq]
have "?p o q \<in> ?one" by auto
hence "?p o (?p o q) \<in> ?pone" by auto
......@@ -330,8 +329,9 @@ proof-
fix pq
assume "pq \<in> ?pone"
then obtain q where q: "q \<in> ?one" and pq: "pq = ?p o q" by auto
from q have q: "q permutes ?n" and sq: "sign q = 1" by auto
from sign_compose[OF pp[OF p] pp[OF q], unfolded sq sp] have spq: "sign pq = -1" unfolding pq by auto
from q have q: "q permutes ?n" and sq: "sign q = (1 :: int)" by auto
from sign_compose[OF pp[OF p] pp[OF q], unfolded sq sp]
have spq: "sign pq = (- 1 :: int)" unfolding pq by auto
from permutes_compose[OF q p] have pq: "pq permutes ?n" unfolding pq by auto
from pq spq have "pq \<in> ?none" by auto
}
......@@ -348,7 +348,7 @@ proof-
by (rule sum.distrib[symmetric])
also have "\<dots> = 0"
by (rule sum.neutral, insert A, auto simp:
sp sign_compose[OF pp[OF p] pp] ij signof_def finite_permutations *)
sp sign_compose[OF pp[OF p] pp] ij finite_permutations *)
finally show ?thesis .
qed
......@@ -643,7 +643,7 @@ proof -
?s p * (\<Prod>i\<in>{0..<n}. A $$ (i, p i)) * (?s (q \<circ> ?inv p) * (\<Prod>ia\<in>{0..<n}. B $$ (ia, q (?inv p ia))))"
unfolding sign thp
unfolding AA_def[symmetric] BB_def[symmetric]
by (simp add: ac_simps signof_def)
by (simp add: ac_simps flip: of_int_mult)
thus "?s q * (\<Prod>i = 0..<n. mat\<^sub>r n n (\<lambda>i. A $$ (i, p i) \<cdot>\<^sub>v row B (p i)) $$ (i, q i)) =
?s p * (\<Prod>i = 0..<n. A $$ (i, p i)) *
(?s (q \<circ> ?inv p) * (\<Prod>i = 0..<n. B $$ (i, (q \<circ> ?inv p) i)))" by simp
......@@ -1020,7 +1020,7 @@ proof -
also have "\<dots> = det A1"
unfolding mat_det_left_def[OF A1] dim by auto
also have "A4 $$ (0,0) = det A4"
using A4 unfolding det_def[of A4] by (auto simp: signof_def sign_def)
using A4 unfolding det_def[of A4] by (auto simp: sign_def)
finally show ?thesis by simp
qed
......@@ -2046,7 +2046,7 @@ proof -
also have "signof ?swap = -1"
proof-
have "n - Suc j < n - j" using Sjn by simp
thus ?thesis unfolding signof_def sign_swap_id by simp
thus ?thesis unfolding sign_swap_id by simp
qed
also have "signof ?prev = (-1::'a) ^ (n + (n - j)) * signof p" using Suc(1) j by auto
also have "(-1) * ... = (-1) ^ (1 + n + (n - j)) * signof p" by simp
......@@ -2081,7 +2081,7 @@ proof -
also have "signof ?swap = (-1)"
proof-
have "n - Suc i < n - i" using Sin by simp
thus ?thesis unfolding signof_def sign_swap_id by simp
thus ?thesis unfolding sign_swap_id by simp
qed
also have "signof ?prev = (-1::'a) ^ (n - i + j) * signof p"
using Suc(1)[OF i].
......@@ -2292,14 +2292,20 @@ proof -
{
fix p
assume p: "p permutes {0..<n}"
have "(\<Sum>x = 0..<n. degree (A $$ (x, p x))) \<le> (\<Sum>x = 0..<n. k)"
have "(\<Sum>x = 0..<n. degree (A $$ (x, p x))) \<le> (\<Sum>x = 0..<n. k)"
by (rule sum_mono[OF assms(1)], insert p, auto)
also have "\<dots> = k * n" unfolding sum_constant by simp
also note calculation
} note * = this
show ?thesis unfolding det_def'[OF A]
by (rule degree_sum_le, insert *, auto simp: finite_permutations signof_def
intro!: order.trans[OF degree_prod_sum_le])
apply (rule degree_sum_le)
apply (simp_all add: finite_permutations)
apply (drule *)
apply (rule order.trans [OF degree_mult_le])
apply simp
apply (rule order.trans [OF degree_prod_sum_le])
apply simp_all
done
qed
lemma upper_triangular_imp_det_eq_0_iff:
......
......@@ -19,10 +19,10 @@ etc. We connect these operations to HOL-Algebra with its explicit carrier sets.\
theory Matrix
imports
Missing_Ring
"HOL-Algebra.Module"
Polynomial_Interpolation.Ring_Hom
Missing_Ring
Conjugate
"HOL-Algebra.Module"
begin
subsection\<open>Vectors\<close>
......
......@@ -3,140 +3,22 @@
Akihisa Yamada
License: BSD
*)
section \<open>Missing Permutations\<close>
section \<open>Material missing in the distribution\<close>
text \<open>This theory provides some definitions and lemmas on permutations which we did not find in the
text \<open>This theory provides some definitions and lemmas which we did not find in the
Isabelle distribution.\<close>
theory Missing_Permutations
imports
Missing_Ring
"HOL-Combinatorics.Permutations"
theory Missing_Misc
imports
"HOL-Library.FuncSet"
"HOL-Combinatorics.Permutations"
begin
definition signof :: "(nat \<Rightarrow> nat) \<Rightarrow> 'a :: ring_1" where
"signof p = (if sign p = 1 then 1 else - 1)"
declare finite_image_iff [simp]
lemma signof_id[simp]: "signof id = 1" "signof (\<lambda> x. x) = 1"
unfolding signof_def sign_id id_def[symmetric] by auto
lemma signof_inv: "finite S \<Longrightarrow> p permutes S \<Longrightarrow> signof (Hilbert_Choice.inv p) = signof p"
unfolding signof_def using sign_inverse permutation_permutes by metis
lemma signof_pm_one: "signof p \<in> {1, - 1}"
unfolding signof_def by auto
lemma signof_compose: assumes "p permutes {0..<(n :: nat)}"
and "q permutes {0 ..<(m :: nat)}"
shows "signof (p o q) = signof p * signof q"
proof -
from assms have pp: "permutation p" "permutation q"
by (auto simp: permutation_permutes)
show "signof (p o q) = signof p * signof q"
unfolding signof_def sign_compose[OF pp]
by (auto simp: sign_def split: if_splits)
qed
lemma permutes_funcset: "p permutes A \<Longrightarrow> (p ` A \<rightarrow> B) = (A \<rightarrow> B)"
by (simp add: permutes_image)
context comm_monoid
begin
lemma finprod_permute:
assumes p: "p permutes S"
and f: "f \<in> S \<rightarrow> carrier G"
shows "finprod G f S = finprod G (f \<circ> p) S"
proof -
from \<open>p permutes S\<close> have "inj p"
by (rule permutes_inj)
then have "inj_on p S"
by (auto intro: subset_inj_on)
from finprod_reindex[OF _ this, unfolded permutes_image[OF p], OF f]
show ?thesis unfolding o_def .
qed
lemma finprod_singleton_set[simp]: assumes "f a \<in> carrier G"
shows "finprod G f {a} = f a"
proof -
have "finprod G f {a} = f a \<otimes> finprod G f {}"
by (rule finprod_insert, insert assms, auto)
also have "\<dots> = f a" using assms by auto
finally show ?thesis .
qed
end
lemmas (in semiring) finsum_permute = add.finprod_permute
lemmas (in semiring) finsum_singleton_set = add.finprod_singleton_set
lemma permutes_less[simp]: assumes p: "p permutes {0..<(n :: nat)}"
shows "i < n \<Longrightarrow> p i < n" "i < n \<Longrightarrow> Hilbert_Choice.inv p i < n"
"p (Hilbert_Choice.inv p i) = i"
"Hilbert_Choice.inv p (p i) = i"
proof -
assume i: "i < n"
show "p i < n" using permutes_in_image[OF p] i by auto
let ?inv = "Hilbert_Choice.inv p"
have "\<And>n. ?inv (p n) = n"
using permutes_inverses[OF p] by simp
thus "?inv i < n"
by (metis (no_types) atLeastLessThan_iff f_inv_into_f inv_into_into le0 permutes_image[OF p] i)
qed (insert permutes_inverses[OF p], auto)
context cring
begin
lemma finsum_permutations_inverse:
assumes f: "f \<in> {p. p permutes S} \<rightarrow> carrier R"
shows "finsum R f {p. p permutes S} = finsum R (\<lambda>p. f(Hilbert_Choice.inv p)) {p. p permutes S}"
(is "?lhs = ?rhs")
proof -
let ?inv = "Hilbert_Choice.inv"
let ?S = "{p . p permutes S}"
have th0: "inj_on ?inv ?S"
proof (auto simp add: inj_on_def)
fix q r
assume q: "q permutes S"
and r: "r permutes S"
and qr: "?inv q = ?inv r"
then have "?inv (?inv q) = ?inv (?inv r)"
by simp
with permutes_inv_inv[OF q] permutes_inv_inv[OF r] show "q = r"
by metis
qed
have th1: "?inv ` ?S = ?S"
using image_inverse_permutations by blast
have th2: "?rhs = finsum R (f \<circ> ?inv) ?S"
by (simp add: o_def)
from finsum_reindex[OF _ th0, of f] show ?thesis unfolding th1 th2 using f .
qed
lemma finsum_permutations_compose_right: assumes q: "q permutes S"
and *: "f \<in> {p. p permutes S} \<rightarrow> carrier R"
shows "finsum R f {p. p permutes S} = finsum R (\<lambda>p. f(p \<circ> q)) {p. p permutes S}"
(is "?lhs = ?rhs")
proof -
let ?S = "{p. p permutes S}"
let ?inv = "Hilbert_Choice.inv"
have th0: "?rhs = finsum R (f \<circ> (\<lambda>p. p \<circ> q)) ?S"
by (simp add: o_def)
have th1: "inj_on (\<lambda>p. p \<circ> q) ?S"
proof (auto simp add: inj_on_def)
fix p r
assume "p permutes S"
and r: "r permutes S"
and rp: "p \<circ> q = r \<circ> q"
then have "p \<circ> (q \<circ> ?inv q) = r \<circ> (q \<circ> ?inv q)"
by (simp add: o_assoc)
with permutes_surj[OF q, unfolded surj_iff] show "p = r"
by simp
qed
have th3: "(\<lambda>p. p \<circ> q) ` ?S = ?S"
using image_compose_permutations_right[OF q] by auto
from finsum_reindex[OF _ th1, of f]
show ?thesis unfolding th0 th1 th3 using * .
qed
end
lemma inj_on_finite:
\<open>finite (f ` A) \<longleftrightarrow> finite A\<close> if \<open>inj_on f A\<close>
using that by (fact finite_image_iff)
text \<open>The following lemma is slightly generalized from Determinants.thy in HMA.\<close>
......@@ -188,6 +70,28 @@ next
by metis
qed
lemma permutes_less [simp]:
assumes p: "p permutes {0..<(n :: nat)}"
shows
"i < n \<Longrightarrow> p i < n"
"i < n \<Longrightarrow> inv p i < n"
"p (inv p i) = i"
"inv p (p i) = i"
using assms
by (simp_all add: permutes_inverses permutes_nat_less permutes_nat_inv_less)
lemma permutes_prod:
assumes p: "p permutes S"
shows "(\<Prod>s\<in>S. f (p s) s) = (\<Prod>s\<in>S. f s (inv p s))"
(is "?l = ?r")
using assms by (fact prod.permutes_inv)
lemma permutes_sum:
assumes p: "p permutes S"
shows "(\<Sum>s\<in>S. f (p s) s) = (\<Sum>s\<in>S. f s (inv p s))"
(is "?l = ?r")
using assms by (fact sum.permutes_inv)
context
fixes A :: "'a set"
and B :: "'b set"
......@@ -288,9 +192,10 @@ proof
qed
qed
qed
end
lemma permutes_bij': assumes ab: "\<And> a. a \<in> A \<Longrightarrow> a_to_b a \<in> B"
lemma permutes_bij': assumes ab: "\<And> a. a \<in> A \<Longrightarrow> a_to_b a \<in> B"
and ba: "\<And> b. b \<in> B \<Longrightarrow> b_to_a b \<in> A"
and ab_ba: "\<And> a. a \<in> A \<Longrightarrow> b_to_a (a_to_b a) = a"
and ba_ab: "\<And> b. b \<in> B \<Longrightarrow> a_to_b (b_to_a b) = b"
......@@ -332,6 +237,10 @@ proof -
ultimately show ?thesis by blast
qed
lemma permutes_others:
assumes p: "p permutes S" and x: "x \<notin> S" shows "p x = x"
using p x by (rule permutes_not_in)
lemma inj_on_nat_permutes: assumes i: "inj_on f (S :: nat set)"
and fS: "f \<in> S \<rightarrow> S"
and fin: "finite S"
......@@ -359,105 +268,29 @@ proof (intro conjI allI impI, rule f)
qed
qed
abbreviation (input) signof :: \<open>(nat \<Rightarrow> nat) \<Rightarrow> 'a :: ring_1\<close>
where \<open>signof p \<equiv> of_int (sign p)\<close>
lemma permutes_pair_eq:
assumes p: "p permutes S"
shows "{ (p s, s) | s. s \<in> S } = { (s, Hilbert_Choice.inv p s) | s. s \<in> S }"
(is "?L = ?R")
proof
show "?L \<subseteq> ?R"
proof
fix x assume "x \<in> ?L"
then obtain s where x: "x = (p s, s)" and s: "s \<in> S" by auto
note x
also have "(p s, s) = (p s, Hilbert_Choice.inv p (p s))"
using permutes_inj[OF p] inv_f_f by auto
also have "... \<in> ?R" using s permutes_in_image[OF p] by auto
finally show "x \<in> ?R".
qed
show "?R \<subseteq> ?L"
proof
fix x assume "x \<in> ?R"
then obtain s
where x: "x = (s, Hilbert_Choice.inv p s)" (is "_ = (s, ?ips)")
and s: "s \<in> S" by auto
note x
also have "(s, ?ips) = (p ?ips, ?ips)"
using inv_f_f[OF permutes_inj[OF permutes_inv[OF p]]]
using inv_inv_eq[OF permutes_bij[OF p]] by auto
also have "... \<in> ?L"
using s permutes_in_image[OF permutes_inv[OF p]] by auto
finally show "x \<in> ?L".
qed
qed
lemma inj_on_finite[simp]:
assumes inj: "inj_on f A" shows "finite (f ` A) = finite A"
proof
assume fin: "finite (f ` A)"
show "finite A"
proof (cases "card (f ` A) = 0")
case True thus ?thesis using fin by auto
next case False
hence "card A > 0" unfolding card_image[OF inj] by auto
thus ?thesis using card.infinite by force
qed
qed auto
lemma permutes_prod:
assumes p: "p permutes S"
shows "(\<Prod>s\<in>S. f (p s) s) = (\<Prod>s\<in>S. f s (Hilbert_Choice.inv p s))"
(is "?l = ?r")
proof -
let ?f = "\<lambda>(x,y). f x y"
let ?ps = "\<lambda>s. (p s, s)"
let ?ips = "\<lambda>s. (s, Hilbert_Choice.inv p s)"
have inj1: "inj_on ?ps S" by (rule inj_onI;auto)
have inj2: "inj_on ?ips S" by (rule inj_onI;auto)
have "?l = prod ?f (?ps ` S)"
using prod.reindex[OF inj1, of ?f] by simp
also have "?ps ` S = {(p s, s) |s. s \<in> S}" by auto
also have "... = {(s, Hilbert_Choice.inv p s) | s. s \<in> S}"
unfolding permutes_pair_eq[OF p] by simp
also have "... = ?ips ` S" by auto
also have "prod ?f ... = ?r"
using prod.reindex[OF inj2, of ?f] by simp
finally show ?thesis.
qed
lemma signof_id:
"signof id = 1"
"signof (\<lambda>x. x) = 1"
by simp_all
lemma permutes_sum:
assumes p: "p permutes S"
shows "(\<Sum>s\<in>S. f (p s) s) = (\<Sum>s\<in>S. f s (Hilbert_Choice.inv p s))"
(is "?l = ?r")
lemma signof_inv: "finite S \<Longrightarrow> p permutes S \<Longrightarrow> signof (inv p) = signof p"
by (simp add: permutes_imp_permutation sign_inverse)
lemma signof_pm_one: "signof p \<in> {1, - 1}"
by (simp add: sign_def)
lemma signof_compose:
assumes "p permutes {0..<(n :: nat)}"
and "q permutes {0 ..<(m :: nat)}"
shows "signof (p o q) = signof p * signof q"
proof -
let ?f = "\<lambda>(x,y). f x y"
let ?ps = "\<lambda>s. (p s, s)"
let ?ips = "\<lambda>s. (s, Hilbert_Choice.inv p s)"
have inj1: "inj_on ?ps S" by (rule inj_onI;auto)
have inj2: "inj_on ?ips S" by (rule inj_onI;auto)
have "?l = sum ?f (?ps ` S)"
using sum.reindex[OF inj1, of ?f] by simp
also have "?ps ` S = {(p s, s) |s. s \<in> S}" by auto
also have "... = {(s, Hilbert_Choice.inv p s) | s. s \<in> S}"
unfolding permutes_pair_eq[OF p] by simp
also have "... = ?ips ` S" by auto
also have "sum ?f ... = ?r"
using sum.reindex[OF inj2, of ?f] by simp
finally show ?thesis.
qed
lemma inv_inj_on_permutes: "inj_on Hilbert_Choice.inv { p. p permutes S }"
proof (intro inj_onI, unfold mem_Collect_eq)
let ?i = "Hilbert_Choice.inv"
fix p q
assume p: "p permutes S" and q: "q permutes S" and eq: "?i p = ?i q"
have "?i (?i p) = ?i (?i q)" using eq by simp
thus "p = q"
using inv_inv_eq[OF permutes_bij] p q by metis
qed
lemma permutes_others:
assumes p: "p permutes S" and x: "x \<notin> S" shows "p x = x"
using p unfolding permutes_def using x by simp
from assms have pp: "permutation p" "permutation q"
by (auto simp: permutation_permutes)
then show "signof (p o q) = signof p * signof q"
by (simp add: sign_compose)
qed
end
\ No newline at end of file
end
......@@ -8,10 +8,152 @@ section \<open>Missing Ring\<close>
text \<open>This theory contains several lemmas which might be of interest to the Isabelle distribution.\<close>
theory Missing_Ring
imports
imports
"Missing_Misc"
"HOL-Algebra.Ring"
begin
context ordered_cancel_semiring
begin
subclass ordered_cancel_ab_semigroup_add ..
end
text \<open>partially ordered variant\<close>
class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +
assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
begin
subclass semiring_0_cancel ..
subclass ordered_semiring
proof
fix a b c :: 'a
assume A: "a \<le> b" "0 \<le> c"
from A show "c * a \<le> c * b"
unfolding le_less
using mult_strict_left_mono by (cases "c = 0") auto
from A show "a * c \<le> b * c"
unfolding le_less
using mult_strict_right_mono by (cases "c = 0") auto
qed
lemma mult_pos_pos[simp]: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
using mult_strict_left_mono [of 0 b a] by simp
lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
using mult_strict_left_mono [of b 0 a] by simp
lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"
using mult_strict_right_mono [of a 0 b] by simp
text \<open>Legacy - use \<open>mult_neg_pos\<close>\<close>
lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0"
by (drule mult_strict_right_mono [of b 0], auto)
text\<open>Strict monotonicity in both arguments\<close>
lemma mult_strict_mono:
assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"
shows "a * c < b * d"
using assms apply (cases "c=0")
apply (simp)
apply (erule mult_strict_right_mono [THEN less_trans])
apply (force simp add: le_less)
apply (erule mult_strict_left_mono, assumption)
done
text\<open>This weaker variant has more natural premises\<close>
lemma mult_strict_mono':
assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c"
shows "a * c < b * d"
by (rule mult_strict_mono) (insert assms, auto)
lemma mult_less_le_imp_less: