Theory CofGroups
theory CofGroups
imports Main "HOL-Library.Nat_Bijection"
begin
section ‹Introduction›
text ‹Cofinitary groups have received a lot of attention in Set
Theory. I will start by giving some references, that together give a
nice view of the area. See also Kastermans \cite {Kques} for my view
of where the study of these groups (other than formalization) is
headed. Starting work was done by Adeleke \cite {MR989749}, Truss
\cite {MR896533} and \cite {MR1683516}, and Koppelberg \cite
{MR709997}. Cameron \cite {MR1367160} is a very nice survey. There
is also work on cardinal invariants related to these groups and other
almost disjoint families, see e.g. Brendle, Spinas, and Zhang \cite
{MR1783921}, Hru{\v{s}}{\'a}k, Steprans, and Zhang \cite {MR1856740},
and Kastermans and Zhang \cite {KZ}. Then there is also work on
constructions and descriptive complexity of these groups, see
e.g. Zhang \cite {MR1974545}, Gao and Zhang \cite {MR2370282}, and
Kastermans \cite {BK1} and \cite {BK2}.
In this note we work through formalizing a basic example of a
cofinitary group. We want to achieve two things by working through
this example. First how to formalize some proofs from basic
set-theoretic algebra, and secondly, to do some first steps in the
study of formalization of this area of set theory. This is related to
the work of Paulson andGr{\polhk{a}}bczewski \cite {PG} on formalizing
set theory, our preference however is towards using Isar resulting in
a development more readable for ``normal'' mathematicians.
A \emph{cofinitary group} is a subgroup $G$ of the symmetric group on
$\mathbb{N}$ (in Isabelle @{term nat}) such that all non-identity
elements $g \in G$ have finitely many fixed points. A simple example
of a cofinitary group is obtained by considering the group $G'$ a
subgroup of the symmetric group on $\mathbb {Z}$ (in Isabelle @{term
int} generated by the function @{term upOne} $:\mathbb {Z}
\rightarrow \mathbb {Z}$ defined by $k \mapsto k + 1$. No element in
this group other than the identity has a fixed point. Conjugating
this group by any bijection $\mathbb {Z} \rightarrow \N$ gives a
cofinitary group.
We will develop a workable definition of a cofinitary group (Section
\ref {sect:mainnotions}) and show that the group as described in the
previous paragraph is indeed cofinitary (this takes the whole paper,
but is all pulled together in Section \ref {sect:concl}). Note:
formalizing the previous paragraph is all that is completed in this
note.
Since this note is also written to be read by the proverbial
``normal'' mathematician we will sometimes remark on notations as used
in Isabelle as they related to common notation. We do expect this
proverbial mathematician to be somewhat flexible though. He or she
will need to be flexible in reading, this is just like reading any
other article; part of reading is reconstructing.›
text ‹We end this introduction with a quick overview of the paper.
In Section \ref {sect:mainnotions} we define the notion of cofinitary
group. In Section \ref {sect:theFunction} we define the function
@{term upOne} and give some of its basic properties. In Section \ref
{sect:setOFunc} we define the set @{term Ex1} which is the underlying
set of the group generated by @{term upOne}, there we also derive a
normal form theorem for the elements of this set. In Section \ref
{sect:Ex1CofBij} we show all elements in @{term Ex1} are cofinitary
bijections (cofinitary here is used in the general meaning of having
finitely many fixed points). In Section \ref {sect:Ex1Closed} we show
this set is closed under composition and inverse, in effect showing
that it is a ``cofinitary group'' (cofinitary group here is in quotes,
since we only define it for sets of permutations on the natural
numbers). In Section \ref {sect:moveNN} we show the general theorem that
conjugating a permutation by a bijection does the expected thing to
the set of fixed points. In Section \ref {sect:bijN} we define the
function @{term CONJ} that is conjugation by @{term ni_bij}
(a bijection from @{typ nat} to @{typ int}), show that
is acts well with respect to the group operations, use it to define
@{term Ex2} which is the underlying set of the cofinitary group we are
construction, and show the basic properties of @{term Ex2}. Finally
in Section \ref {sect:concl} we quickly show that all the work in the
section before it combines to show that @{term Ex2} is a cofinitary
group.›
section ‹The Main Notions›
text ‹\label {sect:mainnotions} First we define the two main notions.
We write @{term S_inf} for the symmetric group on the natural numbers
(we do not define this as a group, only as the set of bijections).›
definition S_inf :: "(nat ⇒ nat) set"
where
"S_inf = {f::(nat ⇒ nat). bij f}"
text ‹Note here that @{term bij} @{term f} is the predicate that
@{term f} is a bijection. This is common notation in Isabelle, a
predicate applied to an object. Related to this @{term inj} @{term f}
means @{term f} is injective, and @{term surj} @{term f} means @{term
f} is surjective.
The same notation is used for functionn application. Next we define a
function @{term Fix}, applying it to an object is also written by
juxtaposition.›
text ‹Given any function @{term f} we define @{term Fix} @{term f}
to be the set of fixed points for this function.›
definition Fix :: "('a ⇒ 'a) ⇒ ('a set)"
where
"Fix f = { n . f(n) = n }"
text ‹We then define a locale @{term CofinitaryGroup} that
represents the notion of a cofinitary group. An interpretation is
given by giving a set of functions $nat \rightarrow nat$ and showing
that it satisfies the identities the locale assumes. A locale is a
way to collect together some information that can then later be used
in a flexible way (we will not make a lot of use of that here).›
locale CofinitaryGroup =
fixes
dom :: "(nat ⇒ nat) set"
assumes
type_dom : "dom ⊆ S_inf" and
id_com : "id ∈ dom" and
mult_closed : "f ∈ dom ∧ g ∈ dom ⟹ f ∘ g ∈ dom" and
inv_closed : "f ∈ dom ⟹ inv f ∈ dom" and
cofinitary : "f ∈ dom ∧ f ≠ id ⟹ finite (Fix f)"
section ‹The Function @{term upOne}›
text ‹\label{sect:theFunction} Here we define the function, @{term
upOne}, translation up by 1 and proof some of its basic properties.
›
definition upOne :: "int ⇒ int"
where
"upOne n = n + 1"
declare upOne_def [simp]
text ‹First we show that this function is a bijection. This is done
in the usual two parts; we show it is injective by showing from the
assumption that outputs on two numbers are equal that these two
numbers are equal. Then we show it is surjective by finding the
number that maps to a given number.›
lemma inj_upOne: "inj upOne"
by (rule Fun.injI, simp)
lemma surj_upOne: "surj upOne"
proof (unfold Fun.surj_def, rule)
fix k::int
show "∃m. k = upOne m"
by (rule exI[of "λl. k = upOne l" "k - 1"], simp)
qed
theorem bij_upOne: "bij upOne"
by (unfold bij_def, rule conjI [OF inj_upOne surj_upOne])
text ‹Now we show that the set of fixed points of @{term upOne}
is empty. We show this in two steps, first we show that no number
is a fixed point, and then derive from this that the set of fixed
points is empty.›
lemma no_fix_upOne: "upOne n ≠ n"
proof (rule notI)
assume "upOne n = n"
with upOne_def have "n+1 = n" by simp
thus False by auto
qed
theorem "Fix upOne = {}"
proof -
from Fix_def[of upOne]
have "Fix upOne = {n . upOne n = n}" by auto
with no_fix_upOne have "Fix upOne = {n . False}" by auto
with Set.empty_def show "Fix upOne = {}" by auto
qed
text ‹Finally we derive the equation for the inverse of @{term
upOne}. The rule we use references ‹Hilbert_Choice› since the @{term
inv} operator, the operator that gives an inverse of a function, is
defined using Hilbert's choice operator.›
lemma inv_upOne_eq: "(inv upOne) (n::int) = n - 1"
proof -
fix "n" :: int
have "((inv upOne) ∘ upOne) (n - 1) = (inv upOne) n" by simp
with inj_upOne and Hilbert_Choice.inv_o_cancel
show "(inv upOne) n = n - 1" by auto
qed
text ‹We can also show this quickly using Hilbert\_Choice.inv\_f\_eq
properly instantiated : @{thm Hilbert_Choice.inv_f_eq[of upOne "n - 1"
n, OF inj_upOne]}.›
lemma "(inv upOne) n = n - 1"
by (rule Hilbert_Choice.inv_f_eq[of upOne "n - 1" n, OF inj_upOne], simp)
section ‹The Set of Functions and Normal Forms›
text ‹\label {sect:setOFunc} We define the set @{term Ex1} of all
powers of @{term upOne} and study some of its properties, note that
this is the group generated by @{term upOne} (in Section \ref
{sect:Ex1Closed} we prove it closed under composition and inverse).
In Section \ref {sect:Ex1CofBij} we show that all its elements are
cofinitary and bijections (bijections with finitely many fixed
points). Note that this is not a cofinitary group, since our
definition requires the group to be a subset of @{term S_inf}›
inductive_set Ex1 :: "(int ⇒ int) set" where
base_func: "upOne ∈ Ex1" |
comp_func: "f ∈ Ex1 ⟹ (upOne ∘ f) ∈ Ex1" |
comp_inv : "f ∈ Ex1 ⟹ ((inv upOne) ∘ f) ∈ Ex1"
text ‹We start by showing a \emph{normal form} for elements in this
set.›
lemma Ex1_Normal_form_part1: "f ∈ Ex1 ⟹ ∃k. ∀ n. f(n) = n + k"
proof (rule Ex1.induct [of "f"], blast)
assume "f ∈ Ex1"
have "∀n. upOne n = n + 1" by simp
with HOL.exI show "∃k. ∀n. upOne n = n + k" by auto
next
fix fa:: "int => int"
assume fa_k: "∃k. ∀n. fa n = n + k"
thus "∃k. ∀n. (upOne ∘ fa) n = n + k" by auto
next
fix fa :: "int ⇒ int"
assume fa_k: "∃k. ∀n. fa n = n + k"
from inv_upOne_eq have "∀n. (inv upOne) n = n - 1" by auto
with fa_k show "∃k. ∀n. (inv upOne ∘ fa) n = n + k" by auto
qed
text ‹Now we'll show the other direction. Then we apply rule ‹int_induct› which allows us to do the induction by first showing it
true for $k = 1$, then showing that if true for $k = i$ it is also
true for $k = i+1$ and finally showing that if true for $k = i$ then
it is also true for $k = i - 1$.
All proofs are fairly straightforward and use extensionality for
functions. In the base case we are just dealing with @{term upOne}.
In the other cases we define the function ‹?h› which satisfies
the induction hypothesis. Then @{term f} is obtained from this by
adding or subtracting one pointwise.
In this proof we use some pattern matching to save on writing. In the
statement of the theorem, we match the theorem against ‹?P k› thereby
defining the predicate ‹?P›.›
lemma Ex1_Normal_form_part2:
"(∀f. ((∀n. f n = n + k) ⟶ f ∈ Ex1))" (is "?P k")
proof (rule int_induct [of "?P" 1])
show "∀f. (∀n. f n = n + 1) ⟶ f ∈ Ex1"
proof
fix f:: "int ⇒ int"
show "(∀n. f n = n + 1) ⟶ f ∈ Ex1"
proof
assume "∀n. f n = n + 1"
hence "∀n. f n = upOne n" by auto
with fun_eq_iff[of f upOne,THEN sym]
have "f = upOne" by auto
with Ex1.base_func show "f ∈ Ex1" by auto
qed
qed
next
fix i::int
assume "1 ≤ i"
assume induct_hyp: "∀f. (∀n. f n = n + i) ⟶ f ∈ Ex1"
show "∀f. (∀n. f n = n + (i + 1)) ⟶ f ∈ Ex1"
proof
fix f:: "int ⇒ int"
show "(∀n. f n = n + (i + 1)) ⟶ f ∈ Ex1"
proof
assume f_eq: "∀n. f n = n + (i + 1)"
let ?h = "λn. n + i"
from induct_hyp have h_Ex1: "?h ∈ Ex1" by auto
from f_eq have "∀n. f n = upOne (?h n)" by (unfold upOne_def,auto)
hence "∀n. f n = (upOne ∘ ?h) n" by auto
with fun_eq_iff[THEN sym, of f "upOne ∘ ?h"]
have "f = upOne ∘ ?h" by auto
with h_Ex1 and Ex1.comp_func[of ?h] show "f ∈ Ex1" by auto
qed
qed
next
fix i::int
assume "i ≤ 1"
assume induct_hyp: "∀f. (∀n. f n = n + i) ⟶ f ∈ Ex1"
show "∀f. (∀n. f n = n + (i - 1)) ⟶ f ∈ Ex1"
proof
fix f:: "int ⇒ int"
show "(∀n. f n = n + (i - 1)) ⟶ f ∈ Ex1"
proof
assume f_eq: "∀n. f n = n + (i - 1)"
let ?h = "λn. n + i"
from induct_hyp have h_Ex1: "?h ∈ Ex1" by auto
from inv_upOne_eq and f_eq
have "∀n. f n = (inv upOne) (?h n)" by auto
hence "∀n. f n = (inv upOne ∘ ?h) n" by auto
with fun_eq_iff[THEN sym, of f "inv upOne ∘ ?h"]
have "f = inv upOne ∘ ?h" by auto
with h_Ex1 and Ex1.comp_inv[of ?h] show "f ∈ Ex1" by auto
qed
qed
qed
text ‹Combining the two directions we get the normal form
theorem.›
theorem Ex1_Normal_form: "(f ∈ Ex1) = (∃k. ∀n. f(n) = n + k)"
proof
assume "f ∈ Ex1"
with Ex1_Normal_form_part1 [of f]
show "(∃k. ∀n. f(n) = n + k)" by auto
next
assume "∃k. ∀n. f(n) = n + k"
with Ex1_Normal_form_part2
show "f ∈ Ex1" by auto
qed
section ‹All Elements Cofinitary Bijections.›
text ‹\label {sect:Ex1CofBij} We now show all elements in @{term
Ex1} are bijections, Theorem @{term all_bij}, and have no fixed
points, Theorem @{term no_fixed_pt}.›
theorem all_bij: "f ∈ Ex1 ⟹ bij f"
proof (unfold bij_def)
assume "f ∈ Ex1"
with Ex1_Normal_form
obtain k where f_eq:"∀n. f n = n + k" by auto
show "inj f ∧ surj f"
proof (rule conjI)
show INJ: "inj f"
proof (rule injI)
fix n m
assume "f n = f m"
with f_eq have "n + k = m + k" by auto
thus "n = m" by auto
qed
next
show SURJ: "surj f"
proof (unfold Fun.surj_def, rule allI)
fix n
from f_eq have "n = f (n - k)" by auto
thus "∃m. n = f m" by (rule exI)
qed
qed
qed
theorem no_fixed_pt:
assumes f_Ex1: "f ∈ Ex1"
and f_not_id: "f ≠ id"
shows "Fix f = {}"
proof -
have f_eq_then_id: "(∀n. f(n) = n) ⟹ f = id"
proof -
assume f_prop : "∀n. f(n) = n"
have "(f x = id x) = (f x = x)" by simp
hence "(∀x. (f x = id x)) = (∀x. (f x = x))" by simp
with fun_eq_iff[THEN sym, of f id] and f_prop show "f = id" by auto
qed
from f_Ex1 and Ex1_Normal_form have "∃k. ∀n. f(n) = n + k" by auto
then obtain k where k_prop: "∀n. f(n) = n + k" ..
hence "k = 0 ⟹ ∀n. f(n) = n" by auto
with f_eq_then_id and f_not_id have "k ≠ 0" by auto
with k_prop have "∀n. f(n) ≠ n" by auto
moreover
from Fix_def[of f] have "Fix f = {n . f(n) = n}" by auto
ultimately have "Fix f = {n. False}" by auto
with Set.empty_def show "Fix f = {}" by auto
qed
section ‹Closed under Composition and Inverse›
text ‹\label {sect:Ex1Closed} We start by showing that this set is
closed under composition. These facts can later be conjugated to
easily obtain the corresponding results for the group on the natural
numbers.›
theorem closed_comp: "f ∈ Ex1 ∧ g ∈ Ex1 ⟹ f ∘ g ∈ Ex1"
proof (rule Ex1.induct [of f], blast)
assume "f ∈ Ex1 ∧ g ∈ Ex1"
with Ex1.comp_func[of g] show "upOne ∘ g ∈ Ex1" by auto
next
fix fa
assume "fa ∘ g ∈ Ex1"
with Ex1.comp_func [of "fa ∘ g"]
and Fun.o_assoc [of "upOne" "fa" "g"]
show "upOne ∘ fa ∘ g ∈ Ex1" by auto
next
fix fa
assume "fa ∘ g ∈ Ex1"
with Ex1.comp_inv [of "fa ∘ g"]
and Fun.o_assoc [of "inv upOne" "fa" "g"]
show "(inv upOne) ∘ fa ∘ g ∈ Ex1" by auto
qed
text ‹Now we show the set is closed under inverses. This is
done by an induction on the definition of @{term Ex1} only using
the normal form theorem and rewriting of expressions.›
theorem closed_inv: "f ∈ Ex1 ⟹ inv f ∈ Ex1"
proof (rule Ex1.induct [of "f"], blast)
assume "f ∈ Ex1"
show "inv upOne ∈ Ex1" (is "?right ∈ Ex1")
proof -
let ?left = "inv upOne ∘ (inv upOne ∘ upOne)"
{
from Ex1.comp_inv and Ex1.base_func have "?left ∈ Ex1" by auto
}
moreover
{
from bij_upOne and bij_is_inj have "inj upOne" by auto
hence "inv upOne ∘ upOne = id" by auto
hence "?left = ?right" by auto
}
ultimately
show ?thesis by auto
qed
next
fix f
assume f_Ex1: "f ∈ Ex1"
from f_Ex1 and Ex1_Normal_form
obtain k where f_eq: "∀n. f n = n + k" by auto
show "inv (upOne ∘ f) ∈ Ex1"
proof -
let ?ic = "inv (upOne ∘ f)"
let ?ci = "inv f ∘ inv upOne"
{
{
from all_bij and f_Ex1 have "bij f" by auto
with bij_is_inj have inj_f: "inj f" by auto
have "∀n. inv f n = n - k"
proof
fix n
from f_eq have "f (n - k) = n" by auto
with inv_f_eq[of f "n-k" "n"] and inj_f
show "inv f n = n-k" by auto
qed
with inv_upOne_eq
have "∀n. ?ci n = n - k - 1" by auto
hence "∀n. ?ci n = n + (-1 - k)" by arith
}
moreover
{
from Ex1_Normal_form_part2[of "-1 - k"]
have "(∀f. ((∀n. f n = n + (-1 - k)) ⟶ f ∈ Ex1))" by auto
}
ultimately
have "?ci ∈ Ex1" by auto
}
moreover
{
from f_Ex1 all_bij have "bij f" by auto
with bij_upOne and o_inv_distrib[THEN sym]
have "?ci = ?ic" by auto
}
ultimately show ?thesis by auto
qed
next
fix f
assume f_Ex1: "f ∈ Ex1"
with Ex1_Normal_form
obtain k where f_eq: "∀n. f n = n + k" by auto
show "inv (inv upOne ∘ f) ∈ Ex1"
proof -
let ?ic = "inv (inv upOne ∘ f)"
let ?c = "inv f ∘ upOne"
{
from all_bij and f_Ex1 have "bij f" by auto
with bij_is_inj have inj_f: "inj f" by auto
have "∀n. inv f n = n - k"
proof
fix n
from f_eq have "f (n - k) = n" by auto
with inv_f_eq[of f "n-k" "n"] and inj_f
show "inv f n = n-k" by auto
qed
with upOne_def
have "∀n. (inv f ∘ upOne) n = n - k + 1" by auto
hence "∀n. (inv f ∘ upOne) n = n + (1 - k)" by arith
moreover
from Ex1_Normal_form_part2[of "1 - k"]
have "(∀f. ((∀n. f n = n + (1 - k)) ⟶ f ∈ Ex1))" by auto
ultimately
have "?c ∈ Ex1" by auto
}
moreover
{
from f_Ex1 all_bij and bij_is_inj have "bij f" by auto
moreover
from bij_upOne and bij_imp_bij_inv have "bij (inv upOne)" by auto
moreover
note o_inv_distrib[THEN sym]
ultimately
have "inv f ∘ inv (inv upOne) = inv (inv upOne ∘ f)" by auto
moreover
from bij_upOne and inv_inv_eq
have "inv (inv upOne) = upOne" by auto
ultimately
have "?c = ?ic" by auto
}
ultimately
show ?thesis by auto
qed
qed
section ‹Conjugation with a Bijection›
text ‹\label {sect:moveNN} An abbreviation of the bijection from the
natural numbers to the integers defined in the library. This will be
used to coerce the functions above to be on the natural numbers.›
abbreviation "ni_bij == int_decode"
lemma bij_f_o_inf_f: "bij f ⟹ f ∘ inv f = id"
unfolding bij_def surj_iff by simp
text ‹The following theorem is a key theorem in showing that the
group we are interested in is cofinitary. It states that when you
conjugate a function with a bijection the fixed points get mapped
over.›
theorem conj_fix_pt: "⋀f::('a ⇒ 'b). ⋀g::('b ⇒ 'b). (bij f)
⟹ ((inv f)`(Fix g)) = Fix ((inv f) ∘ g ∘ f)"
proof -
fix f::"'a ⇒ 'b"
assume bij_f: "bij f"
with bij_def have inj_f: "inj f" by auto
fix g::"'b⇒'b"
show "((inv f)`(Fix g)) = Fix ((inv f) ∘ g ∘ f)"
thm set_eq_subset[of "(inv f)`(Fix g)" "Fix((inv f) ∘ g ∘ f)"]
proof
show "(inv f)`(Fix g) ⊆ Fix ((inv f) ∘ g ∘ f)"
proof
fix x
assume "x ∈ (inv f)`(Fix g)"
with image_def have "∃y ∈ Fix g. x = (inv f) y" by auto
from this obtain y where y_prop: "y ∈ Fix g ∧ x = (inv f) y" by auto
hence "x = (inv f) y" ..
hence "f x = (f ∘ inv f) y" by auto
with bij_f and bij_f_o_inf_f[of f] have f_x_y: "f x = y" by auto
from y_prop have "y ∈ Fix g" ..
with Fix_def[of g] have "g y = y" by auto
with f_x_y have "g (f x) = f x" by auto
hence "(inv f) (g (f x)) = inv f (f x)" by auto
with inv_f_f and inj_f have "(inv f) (g (f x)) = x" by auto
hence "((inv f) ∘ g ∘ f) x = x" by auto
with Fix_def[of "inv f ∘ g ∘ f"]
show "x ∈ Fix ((inv f) ∘ g ∘ f)" by auto
qed
next
show "Fix (inv f ∘ g ∘ f) ⊆ (inv f)`(Fix g)"
proof
fix x
assume "x ∈ Fix (inv f ∘ g ∘ f)"
with Fix_def[of "inv f ∘ g ∘ f"]
have x_fix: "(inv f ∘ g ∘ f) x = x" by auto
hence "(inv f) (g(f(x))) = x" by auto
hence "∃y. (inv f) y = x" by auto
from this obtain y where x_inf_f_y: "x = (inv f) y" by auto
with x_fix have "(inv f ∘ g ∘ f)((inv f) y) = (inv f) y" by auto
hence "(f ∘ inv f ∘ g ∘ f ∘ inv f) (y) = (f ∘ inv f)(y)" by auto
with o_assoc
have "((f ∘ inv f) ∘ g ∘ (f ∘ inv f)) y = (f ∘ inv f)y" by auto
with bij_f and bij_f_o_inf_f[of f]
have "g y = y" by auto
with Fix_def[of g] have "y ∈ Fix g" by auto
with x_inf_f_y show "x ∈ (inv f)`(Fix g)" by auto
qed
qed
qed
section ‹Bijections on $\mathbb{N}$›
text ‹\label {sect:bijN} In this section we define the subset @{term
Ex2} of @{term S_inf} that is the conjugate of @{term Ex1} bij @{term
ni_bij}, and show its basic properties.
@{term CONJ} is the function that will conjugate @{term Ex1} to @{term Ex2}.›
definition CONJ :: "(int ⇒ int) ⇒ (nat ⇒ nat)"
where
"CONJ f = (inv ni_bij) ∘ f ∘ ni_bij"
declare CONJ_def [simp]
text ‹We quickly check that this function is of the right type, and
then show three of its properties that are very useful in showing
@{term Ex2} is a group.›
lemma type_CONJ: "f ∈ Ex1 ⟹ (inv ni_bij) ∘ f ∘ ni_bij ∈ S_inf"
proof -
assume f_Ex1: "f ∈ Ex1"
with all_bij have "bij f" by auto
with bij_int_decode and bij_comp
have bij_f_nibij: "bij (f ∘ ni_bij)" by auto
with bij_int_decode and bij_imp_bij_inv have "bij (inv ni_bij)" by auto
with bij_f_nibij and bij_comp[of "f ∘ ni_bij" "inv ni_bij"]
and o_assoc[of "inv ni_bij" "f" "ni_bij"]
have "bij ((inv ni_bij) ∘ f ∘ ni_bij)" by auto
with S_inf_def show "((inv ni_bij) ∘ f ∘ ni_bij) ∈ S_inf" by auto
qed
lemma inv_CONJ:
assumes bij_f: "bij f"
shows "inv (CONJ f) = CONJ (inv f)" (is "?left = ?right")
proof -
have st1: "?left = inv ((inv ni_bij) ∘ f ∘ ni_bij)"
using CONJ_def by auto
from bij_int_decode and bij_imp_bij_inv
have inv_ni_bij_bij: "bij (inv ni_bij)" by auto
with bij_f and bij_comp have "bij (inv ni_bij ∘ f)" by auto
with o_inv_distrib[of "inv ni_bij ∘ f" ni_bij] and bij_int_decode
have "inv ((inv ni_bij) ∘ f ∘ ni_bij) =
(inv ni_bij) ∘ (inv ((inv ni_bij) ∘ f))" by auto
with st1 have st2: "?left =
(inv ni_bij) ∘ (inv ((inv ni_bij) ∘ f))" by auto
from inv_ni_bij_bij and ‹bij f› and o_inv_distrib
have h1: "inv (inv ni_bij ∘ f) = inv f ∘ inv (inv (ni_bij))" by auto
from bij_int_decode and inv_inv_eq[of ni_bij]
have "inv (inv ni_bij) = ni_bij" by auto
with st2 and h1 have "?left = (inv ni_bij ∘ (inv f ∘ ( ni_bij)))" by auto
with o_assoc have "?left = inv ni_bij ∘ inv f ∘ ni_bij" by auto
with CONJ_def[of "inv f"] show ?thesis by auto
qed
lemma comp_CONJ:
"CONJ (f ∘ g) = (CONJ f) ∘ (CONJ g)" (is "?left = ?right")
proof -
from bij_int_decode have "surj ni_bij" unfolding bij_def by auto
then have "ni_bij ∘ (inv ni_bij) = id" unfolding surj_iff by auto
moreover
have "?left = (inv ni_bij) ∘ (f ∘ g) ∘ ni_bij" by simp
hence "?left = (inv ni_bij) ∘ ((f ∘ id) ∘ g) ∘ ni_bij" by simp
ultimately
have "?left =
(inv ni_bij) ∘ ((f ∘ (ni_bij ∘ (inv ni_bij))) ∘ g) ∘ ni_bij"
by auto
thus "?left = ?right" by (auto simp add: o_assoc)
qed
lemma id_CONJ: "CONJ id = id"
proof (unfold CONJ_def)
from bij_int_decode have "inj ni_bij" using bij_def by auto
hence "inv ni_bij ∘ ni_bij = id" by auto
thus "(inv ni_bij ∘ id) ∘ ni_bij = id" by auto
qed
text ‹We now define the group we are interested in, and show the
basic facts that together will show this is a cofinitary group.›
definition Ex2 :: "(nat ⇒ nat) set"
where
"Ex2 = CONJ`Ex1"
theorem mem_Ex2_rule: "f ∈ Ex2 = (∃g. (g ∈ Ex1 ∧ f = CONJ g))"
proof
assume "f ∈ Ex2"
hence "f ∈ CONJ`Ex1" using Ex2_def by auto
from this obtain "g" where "g ∈ Ex1 ∧ f = CONJ g" by blast
thus "∃g. (g ∈ Ex1 ∧ f = CONJ g)" by auto
next
assume "∃g. (g ∈ Ex1 ∧ f = CONJ g)"
with Ex2_def show "f ∈ Ex2" by auto
qed
theorem Ex2_cofinitary:
assumes f_Ex2: "f ∈ Ex2"
and f_nid: "f ≠ id"
shows "Fix f = {}"
proof -
from f_Ex2 and mem_Ex2_rule
obtain g where g_Ex1: "g ∈ Ex1" and f_cg: "f = CONJ g" by auto
with id_CONJ and f_nid have "g ≠ id" by auto
with g_Ex1 and no_fixed_pt[of g] have fg_empty: "Fix g = {}" by auto
from conj_fix_pt[of ni_bij g] and bij_int_decode
have "(inv ni_bij)`(Fix g) = Fix(CONJ g)" by auto
with fg_empty have "{} = Fix (CONJ g)" by auto
with f_cg show "Fix f = {}" by auto
qed
lemma id_Ex2: "id ∈ Ex2"
proof -
from Ex1_Normal_form_part2[of "0"] have "id ∈ Ex1" by auto
with id_CONJ and Ex2_def and mem_Ex2_rule show ?thesis by auto
qed
lemma inv_Ex2: "f ∈ Ex2 ⟹ (inv f) ∈ Ex2"
proof -
assume "f ∈ Ex2"
with mem_Ex2_rule obtain "g" where "g ∈ Ex1" and "f = CONJ g" by auto
with closed_inv have "inv g ∈ Ex1" by auto
from ‹f = CONJ g› have if_iCg: "inv f = inv (CONJ g)" by auto
from all_bij and ‹g ∈ Ex1› have "bij g" by auto
with if_iCg and inv_CONJ have "inv f = CONJ (inv g)" by auto
from ‹g ∈ Ex1› and "closed_inv" have "inv g ∈ Ex1" by auto
with ‹inv f = CONJ (inv g)› and mem_Ex2_rule show "inv f ∈ Ex2" by auto
qed
lemma comp_Ex2:
assumes f_Ex2: "f ∈ Ex2" and
g_Ex2: "g ∈ Ex2"
shows "f ∘ g ∈ Ex2"
proof -
from f_Ex2 obtain f_1
where f_1_Ex1: "f_1 ∈ Ex1" and "f = CONJ f_1"
using mem_Ex2_rule by auto
moreover
from g_Ex2 obtain g_1
where g_1_Ex1: "g_1 ∈ Ex1" and "g = CONJ g_1"
using mem_Ex2_rule by auto
ultimately
have "f ∘ g = (CONJ f_1) ∘ (CONJ g_1)" by auto
hence "f ∘ g = CONJ (f_1 ∘ g_1)" using comp_CONJ by auto
moreover
have "f_1 ∘ g_1 ∈ Ex1" using closed_comp and f_1_Ex1 and g_1_Ex1 by auto
ultimately
show "f ∘ g ∈ Ex2" using mem_Ex2_rule by auto
qed
section ‹The Conclusion›
text ‹\label{sect:concl} With all that we have shown we have already
clearly shown @{term Ex2} to be a cofinitary group. The formalization
also shows this, we just have to refer to the correct theorems proved
above.›
interpretation CofinitaryGroup Ex2
proof
show "Ex2 ⊆ S_inf"
proof
fix f
assume "f ∈ Ex2"
with mem_Ex2_rule obtain g where "g ∈ Ex1" and "f = CONJ g" by auto
with type_CONJ show "f ∈ S_inf" by auto
qed
next
from id_Ex2 show "id ∈ Ex2" .
next
fix f g
assume "f ∈ Ex2 ∧ g ∈ Ex2"
with comp_Ex2 show "f ∘ g ∈ Ex2" by auto
next
fix f
assume "f ∈ Ex2"
with inv_Ex2 show "inv f ∈ Ex2" by auto
next
fix f
assume "f ∈ Ex2 ∧ f ≠ id"
with Ex2_cofinitary have "Fix f = {}" by auto
thus "finite (Fix f)" using finite_def by auto
qed
end