Email Gateway (Oct 07 2022 at 17:39): Email Gateway (Oct 07 2022 at 17:39):From: Jeremy Sylvestre <jsylvest@ualberta.ca>
In src/HOL/Fun.thy:
lemma (in group_add) inj_uminus[simp, intro]: "inj_on uminus A"
by (auto intro!: inj_onI)
lemma bij_uminus: "bij (uminus :: 'a \<Rightarrow> 'a::group_add)"
by (intro bijI, rule inj_uminus, intro surjI, rule minus_minus)
context group_add
begin
lemma surj_plus: "surj ((+) a)"
proof (standard, simp, standard, simp)
fix x
have "x = a + (-a + x)" by (simp add: add.assoc)
thus "x \<in> range ((+) a)" by blast
qed
lemma inj_diff_right [simp]: "inj (\<lambda>b. b - a)"
by (auto intro: injI simp add: algebra_simps)
lemma surj_diff_right [simp]: "surj (\<lambda>x. x - a)"
proof (standard, simp, standard, simp)
fix x
have "x = x + a - a" by simp
thus "x \<in> range (\<lambda>x. x - a)" by fast
qed
end
context semigroup_add
begin
lemma comp_plus: "(+) a \<circ> (+) b = (+) (a + b)"
using add.assoc[of a b] by fastforce
lemma comp_plus_right:
"(\<lambda>x. x + a) \<circ> (\<lambda>x. x + b) = (\<lambda>x. x + (b +
a))"
using add.assoc[of _ b a] by fastforce
end
lemma the_inv_eqI: "the_inv f = g" if "bij f" and "\<And>x. f (g x) = x"
using that the_inv_f_f[of f "g _"] bij_is_inj[of f] by presburger
context group_add
begin
lemma bij_plus : "bij ((+) a)"
using surj_plus bij_betw_add by presburger
lemma the_inv_plus: "the_inv ((+) t) = (\<lambda>x. -t + x)"
using bij_plus by (auto intro: the_inv_eqI)
lemma bij_diff_right: "bij (\<lambda>x. x - a)"
unfolding bij_def by force
lemma the_inv_diff_right: "the_inv (\<lambda>x. x - a) = (\<lambda>x. x +
a)"
using bij_diff_right by (auto intro: the_inv_eqI)
lemma bij_plus_right: "bij (\<lambda>x. x + a)"
using bij_betw_the_inv_into bij_diff_right the_inv_diff_right by metis
lemma the_inv_plus_right: "the_inv (\<lambda>x. x + a) = (\<lambda>x. x -
a)"
using bij_plus_right by (auto intro: the_inv_eqI)
lemma plus_diff_commutes: "(\<lambda>x. x - b) \<circ> (+) a = (+) a
\<circ> (\<lambda>x. x - b)"
using add.assoc[of a _ "-b"] by fastforce
lemma conjugation_eq_plus_diff_comp: "(\<lambda>x. a + x - a) =
(\<lambda>x. x - a) \<circ> (+) a"
by fastforce
lemma conjugation_eq_diff_plus_comp: "(\<lambda>x. a + x - a) = (+) a
\<circ> (\<lambda>x. x - a)"
by (simp add: conjugation_eq_plus_diff_comp plus_diff_commutes)
lemma conjugation_bij: "bij (\<lambda>x. a + x - a)"
using conjugation_eq_plus_diff_comp bij_comp bij_plus bij_diff_right by
metis
lemma the_inv_conjugation:
"the_inv (\<lambda>x. a + x - a) = (\<lambda>x. -a + x + a)"
using conjugation_bij by (auto intro: the_inv_eqI simp add: algebra_simps)
end
Email Gateway (Oct 09 2022 at 05:35):From: Tobias Nipkow <nipkow@in.tum.de>
Jeremy, thanks for the generalisations of the type classes which I have
committed here
https://isabelle.in.tum.de/repos/isabelle/rev/d123d9f67514
I did not add any of your additional lemmas (see 3 below) to Fun.thy because I
wonder whether Fun.thy is the best place for them: they are purely algebraic,
but on a functional level. Originally Fun.thy was meant to hold very generic
lemmas about functions, eg intjectivity, surjectivity etc. Then monotonicity
reasoning. Then more algebraic lemmas crept in, eg "surj ((+) a)", which
prompted you to suggest further algebraic lemmas.
The reason for this is that at the point where all the order and algebra type
classes are defined, Fun.thy (with o, inj, surj etc) is not known yet. The
reason is that Fun builds on Set which uses boolean_algebra which uses Lattices
which uses Groups.
General question: should we continue to put material that morally belongs into
algebra into Fun (and improve its section structure) or should we start a new
theory?
Tobias
smime.p7s
Email Gateway (Oct 10 2022 at 20:02):From: Jeremy Sylvestre <jsylvest@ualberta.ca>
Dear Tobias, thanks for incorporating those generalizations.
The extra lemmas are things that came up as part of a larger project that I
hope might be included into HOL/Computational_Algebra, perhaps that is a
better place for them if they are accepted.
Cheers,
Jeremy S.
Email Gateway (Oct 12 2022 at 05:54):From: Tobias Nipkow <nipkow@in.tum.de>
Jeremy,
I have actually included the most elementary lemmas and have cleaned up that
whole group of lemmas: surj/inj/bij of both (%x. x+/-a) and (%x. a+/-x) are
present now. https://isabelle.in.tum.de/repos/isabelle/rev/26524d0b4395
Tobias
smime.p7s
Last updated: Apr 23 2024 at 16:19 UTC