Theory Jordan_Normal_Form.Missing_Misc
section ‹Material missing in the distribution›
text ‹This theory provides some definitions and lemmas which we did not find in the
Isabelle distribution.›
theory Missing_Misc
imports
"HOL-Library.FuncSet"
"HOL-Combinatorics.Permutations"
begin
declare finite_image_iff [simp]
lemma inj_on_finite:
‹finite (f ` A) ⟷ finite A› if ‹inj_on f A›
using that by (fact finite_image_iff)
text ‹The following lemma is slightly generalized from Determinants.thy in HMA.›
lemma finite_bounded_functions:
assumes fS: "finite S"
shows "finite T ⟹ finite {f. (∀i ∈ T. f i ∈ S) ∧ (∀i. i ∉ T ⟶ f i = i)}"
proof (induct T rule: finite_induct)
case empty
have th: "{f. ∀i. f i = i} = {id}"
by auto
show ?case
by (auto simp add: th)
next
case (insert a T)
let ?f = "λ(y,g) i. if i = a then y else g i"
let ?S = "?f ` (S × {f. (∀i∈T. f i ∈ S) ∧ (∀i. i ∉ T ⟶ f i = i)})"
have "?S = {f. (∀i∈ insert a T. f i ∈ S) ∧ (∀i. i ∉ insert a T ⟶ f i = i)}"
apply (auto simp add: image_iff)
apply (rule_tac x="x a" in bexI)
apply (rule_tac x = "λi. if i = a then i else x i" in exI)
apply (insert insert, auto)
done
with finite_imageI[OF finite_cartesian_product[OF fS insert.hyps(3)], of ?f]
show ?case
by metis
qed
lemma finite_bounded_functions':
assumes fS: "finite S"
shows "finite T ⟹ finite {f. (∀i ∈ T. f i ∈ S) ∧ (∀i. i ∉ T ⟶ f i = j)}"
proof (induct T rule: finite_induct)
case empty
have th: "{f. ∀i. f i = j} = {(λ x. j)}"
by auto
show ?case
by (auto simp add: th)
next
case (insert a T)
let ?f = "λ(y,g) i. if i = a then y else g i"
let ?S = "?f ` (S × {f. (∀i∈T. f i ∈ S) ∧ (∀i. i ∉ T ⟶ f i = j)})"
have "?S = {f. (∀i∈ insert a T. f i ∈ S) ∧ (∀i. i ∉ insert a T ⟶ f i = j)}"
apply (auto simp add: image_iff)
apply (rule_tac x="x a" in bexI)
apply (rule_tac x = "λi. if i = a then j else x i" in exI)
apply (insert insert, auto)
done
with finite_imageI[OF finite_cartesian_product[OF fS insert.hyps(3)], of ?f]
show ?case
by metis
qed
lemma permutes_less [simp]:
assumes p: "p permutes {0..<(n :: nat)}"
shows
"i < n ⟹ p i < n"
"i < n ⟹ 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 "(∏s∈S. f (p s) s) = (∏s∈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 "(∑s∈S. f (p s) s) = (∑s∈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"
and a_to_b :: "'a ⇒ 'b"
and b_to_a :: "'b ⇒ 'a"
assumes ab: "⋀ a. a ∈ A ⟹ a_to_b a ∈ B"
and ba: "⋀ b. b ∈ B ⟹ b_to_a b ∈ A"
and ab_ba: "⋀ a. a ∈ A ⟹ b_to_a (a_to_b a) = a"
and ba_ab: "⋀ b. b ∈ B ⟹ a_to_b (b_to_a b) = b"
begin
qualified lemma permutes_memb: fixes p :: "'b ⇒ 'b"
assumes p: "p permutes B"
and a: "a ∈ A"
defines "ip ≡ Hilbert_Choice.inv p"
shows "a ∈ A" "a_to_b a ∈ B" "ip (a_to_b a) ∈ B" "p (a_to_b a) ∈ B"
"b_to_a (p (a_to_b a)) ∈ A" "b_to_a (ip (a_to_b a)) ∈ A"
proof -
let ?b = "a_to_b a"
from p have ip: "ip permutes B" unfolding ip_def by (rule permutes_inv)
note in_ip = permutes_in_image[OF ip]
note in_p = permutes_in_image[OF p]
show a: "a ∈ A" by fact
show b: "?b ∈ B" by (rule ab[OF a])
show pb: "p ?b ∈ B" unfolding in_p by (rule b)
show ipb: "ip ?b ∈ B" unfolding in_ip by (rule b)
show "b_to_a (p ?b) ∈ A" by (rule ba[OF pb])
show "b_to_a (ip ?b) ∈ A" by (rule ba[OF ipb])
qed
lemma permutes_bij_main:
"{p . p permutes A} ⊇ (λ p a. if a ∈ A then b_to_a (p (a_to_b a)) else a) ` {p . p permutes B}"
(is "?A ⊇ ?f ` ?B")
proof
note d = permutes_def
let ?g = "λ q b. if b ∈ B then a_to_b (q (b_to_a b)) else b"
let ?inv = "Hilbert_Choice.inv"
fix p
assume p: "p ∈ ?f ` ?B"
then obtain q where q: "q permutes B" and p: "p = ?f q" by auto
let ?iq = "?inv q"
from q have iq: "?iq permutes B" by (rule permutes_inv)
note in_iq = permutes_in_image[OF iq]
note in_q = permutes_in_image[OF q]
have qiB: "⋀ b. b ∈ B ⟹ q (?iq b) = b" using q by (rule permutes_inverses)
have iqB: "⋀ b. b ∈ B ⟹ ?iq (q b) = b" using q by (rule permutes_inverses)
from q[unfolded d]
have q1: "⋀ b. b ∉ B ⟹ q b = b"
and q2: "⋀ b. ∃!b'. q b' = b" by auto
note memb = permutes_memb[OF q]
show "p ∈ ?A" unfolding p d
proof (rule, intro conjI impI allI, force)
fix a
show "∃!a'. ?f q a' = a"
proof (cases "a ∈ A")
case True
note a = memb[OF True]
let ?a = "b_to_a (?iq (a_to_b a))"
show ?thesis
proof
show "?f q ?a = a" using a by (simp add: ba_ab qiB ab_ba)
next
fix a'
assume id: "?f q a' = a"
show "a' = ?a"
proof (cases "a' ∈ A")
case False
thus ?thesis using id a by auto
next
case True
note a' = memb[OF this]
from id True have "b_to_a (q (a_to_b a')) = a" by simp
from arg_cong[OF this, of "a_to_b"] a' a
have "q (a_to_b a') = a_to_b a" by (simp add: ba_ab)
from arg_cong[OF this, of ?iq]
have "a_to_b a' = ?iq (a_to_b a)" unfolding iqB[OF a'(2)] .
from arg_cong[OF this, of b_to_a] show ?thesis unfolding ab_ba[OF True] .
qed
qed
next
case False note a = this
show ?thesis
proof
show "?f q a = a" using a by simp
next
fix a'
assume id: "?f q a' = a"
show "a' = a"
proof (cases "a' ∈ A")
case False
with id show ?thesis by simp
next
case True
note a' = memb[OF True]
with id False show ?thesis by auto
qed
qed
qed
qed
qed
end
lemma permutes_bij': assumes ab: "⋀ a. a ∈ A ⟹ a_to_b a ∈ B"
and ba: "⋀ b. b ∈ B ⟹ b_to_a b ∈ A"
and ab_ba: "⋀ a. a ∈ A ⟹ b_to_a (a_to_b a) = a"
and ba_ab: "⋀ b. b ∈ B ⟹ a_to_b (b_to_a b) = b"
shows "{p . p permutes A} = (λ p a. if a ∈ A then b_to_a (p (a_to_b a)) else a) ` {p . p permutes B}"
(is "?A = ?f ` ?B")
proof -
note one_dir = ab ba ab_ba ba_ab
note other_dir = ba ab ba_ab ab_ba
let ?g = "(λ p b. if b ∈ B then a_to_b (p (b_to_a b)) else b)"
define PA where "PA = ?A"
define f where "f = ?f"
define g where "g = ?g"
{
fix p
assume "p ∈ PA"
hence p: "p permutes A" unfolding PA_def by simp
from p[unfolded permutes_def] have pnA: "⋀ a. a ∉ A ⟹ p a = a" by auto
have "?f (?g p) = p"
proof (rule ext)
fix a
show "?f (?g p) a = p a"
proof (cases "a ∈ A")
case False
thus ?thesis by (simp add: pnA)
next
case True note a = this
hence "p a ∈ A" unfolding permutes_in_image[OF p] .
thus ?thesis using a by (simp add: ab_ba ba_ab ab)
qed
qed
hence "f (g p) = p" unfolding f_def g_def .
}
hence "f ` g ` PA = PA" by force
hence id: "?f ` ?g ` ?A = ?A" unfolding PA_def f_def g_def .
have "?f ` ?B ⊆ ?A" by (rule permutes_bij_main[OF one_dir])
moreover have "?g ` ?A ⊆ ?B" by (rule permutes_bij_main[OF ba ab ba_ab ab_ba])
hence "?f ` ?g ` ?A ⊆ ?f ` ?B" by auto
hence "?A ⊆ ?f ` ?B" unfolding id .
ultimately show ?thesis by blast
qed
lemma permutes_others:
assumes p: "p permutes S" and x: "x ∉ 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 ∈ S → S"
and fin: "finite S"
and f: "⋀ i. i ∉ S ⟹ f i = i"
shows "f permutes S"
unfolding permutes_def
proof (intro conjI allI impI, rule f)
fix y
from endo_inj_surj[OF fin _ i] fS have fs: "f ` S = S" by auto
show "∃!x. f x = y"
proof (cases "y ∈ S")
case False
thus ?thesis by (intro ex1I[of _ y], insert fS f, auto)
next
case True
with fs obtain x where x: "x ∈ S" and fx: "f x = y" by force
show ?thesis
proof (rule ex1I, rule fx)
fix x'
assume fx': "f x' = y"
with True f[of x'] have "x' ∈ S" by metis
from inj_onD[OF i fx[folded fx'] x this]
show "x' = x" by simp
qed
qed
qed
abbreviation (input) signof :: ‹(nat ⇒ nat) ⇒ 'a :: ring_1›
where ‹signof p ≡ of_int (sign p)›
lemma signof_id:
"signof id = 1"
"signof (λx. x) = 1"
by simp_all
lemma signof_inv: "finite S ⟹ p permutes S ⟹ signof (inv p) = signof p"
by (simp add: permutes_imp_permutation sign_inverse)
lemma signof_pm_one: "signof p ∈ {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 -
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