(*  Title:       An Example of a Cofinitary Group in Isabelle/HOL
    Author:      Bart.Kastermans at colorado.edu, 2009
    Maintainer:  Bart.Kastermans at colorado.edu
*)

theory CofGroups
imports Main "HOL-Library.Nat_Bijection"
begin

section ‹Introduction›

text ‹Cofinitary groups have received a lot of attention in Set
 . I will start by giving some references, that together give a
  view of the area. See also Kastermans \cite {Kques} for my view
  where the study of these groups (other than formalization) is
 . 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
  also work on cardinal invariants related to these groups and other
  disjoint families, see e.g. Brendle, Spinas, and Zhang \cite
 MR1783921}, Hru{\v{s}}{\'a}k, Steprans, and Zhang \cite {MR1856740},
  Kastermans and Zhang \cite {KZ}. Then there is also work on
  and descriptive complexity of these groups, see
 .g. Zhang \cite {MR1974545}, Gao and Zhang \cite {MR2370282}, and
  \cite {BK1} and \cite {BK2}.

  this note we work through formalizing a basic example of a
  group. We want to achieve two things by working through
  example. First how to formalize some proofs from basic
 -theoretic algebra, and secondly, to do some first steps in the
  of formalization of this area of set theory. This is related to
  work of Paulson andGr{\polhk{a}}bczewski \cite {PG} on formalizing
  theory, our preference however is towards using Isar resulting in
  development more readable for ``normal'' mathematicians.

  \emph{cofinitary group} is a subgroup $G$ of the symmetric group on
 \mathbb{N}$ (in Isabelle @{term nat}) such that all non-identity
  $g \in G$ have finitely many fixed points. A simple example
  a cofinitary group is obtained by considering the group $G'$ a
  of the symmetric group on $\mathbb {Z}$ (in Isabelle @{term
 } generated by the function @{term upOne} $:\mathbb {Z}
 rightarrow \mathbb {Z}$ defined by $k \mapsto k + 1$. No element in
  group other than the identity has a fixed point. Conjugating
  group by any bijection $\mathbb {Z} \rightarrow \N$ gives a
  group.

  will develop a workable definition of a cofinitary group (Section
 ref {sect:mainnotions}) and show that the group as described in the
  paragraph is indeed cofinitary (this takes the whole paper,
  is all pulled together in Section \ref {sect:concl}). Note:
  the previous paragraph is all that is completed in this
 .

  this note is also written to be read by the proverbial
 `normal'' mathematician we will sometimes remark on notations as used
  Isabelle as they related to common notation. We do expect this
  mathematician to be somewhat flexible though. He or she
  need to be flexible in reading, this is just like reading any
  article; part of reading is reconstructing.›

text ‹We end this introduction with a quick overview of the paper.
  Section \ref {sect:mainnotions} we define the notion of cofinitary
 . 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
  of the group generated by @{term upOne}, there we also derive a
  form theorem for the elements of this set. In Section \ref
 sect:Ex1CofBij} we show all elements in @{term Ex1} are cofinitary
  (cofinitary here is used in the general meaning of having
  many fixed points). In Section \ref {sect:Ex1Closed} we show
  set is closed under composition and inverse, in effect showing
  it is a ``cofinitary group'' (cofinitary group here is in quotes,
  we only define it for sets of permutations on the natural
 ). In Section \ref {sect:moveNN} we show the general theorem that
  a permutation by a bijection does the expected thing to
  set of fixed points. In Section \ref {sect:bijN} we define the
  @{term CONJ} that is conjugation by @{term ni_bij}
 a bijection from @{typ nat} to @{typ int}), show that
  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
 , and show the basic properties of @{term Ex2}. Finally
  Section \ref {sect:concl} we quickly show that all the work in the
  before it combines to show that @{term Ex2} is a cofinitary
 .›



section ‹The Main Notions›

text ‹\label {sect:mainnotions} First we define the two main notions.

  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
  applied to an object. Related to this @{term inj} @{term f}
  @{term f} is injective, and @{term surj} @{term f} means @{term
 } is surjective.

  same notation is used for functionn application. Next we define a
  @{term Fix}, applying it to an object is also written by
 .›

text ‹Given any function @{term f} we define @{term Fix} @{term f}
  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
  the notion of a cofinitary group. An interpretation is
  by giving a set of functions $nat \rightarrow nat$ and showing
  it satisfies the identities the locale assumes. A locale is a
  to collect together some information that can then later be used
  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
 }, translation up by 1 and proof some of its basic properties.
 ›

definition upOne :: "int → int"
where
"upOne n = n + 1"

declare upOne_def [simp] ― ‹automated tools can use the definition›

text ‹First we show that this function is a bijection. This is done
  the usual two parts; we show it is injective by showing from the
  that outputs on two numbers are equal that these two
  are equal. Then we show it is surjective by finding the
  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}
  empty. We show this in two steps, first we show that no number
  a fixed point, and then derive from this that the set of fixed
  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
 }. The rule we use references ‹Hilbert_Choice› since the @{term
 } operator, the operator that gives an inverse of a function, is
  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
  instantiated : @{thm Hilbert_Choice.inv_f_eq[of upOne "n - 1"
 , 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
  of @{term upOne} and study some of its properties, note that
  is the group generated by @{term upOne} (in Section \ref
 sect:Ex1Closed} we prove it closed under composition and inverse).
  Section \ref {sect:Ex1CofBij} we show that all its elements are
  and bijections (bijections with finitely many fixed
 ). Note that this is not a cofinitary group, since our
  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
 .›

lemma Ex1_Normal_form_part1: "f ∈ Ex1 ==> ∃k. ∀ n. f(n) = n + k"
proof (rule Ex1.induct [of "f"], blast) 
    ― ‹blast takes care of the first goal which is formal noise›
  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
  for $k = 1$, then showing that if true for $k = i$ it is also
  for $k = i+1$ and finally showing that if true for $k = i$ then
  is also true for $k = i - 1$.

  proofs are fairly straightforward and use extensionality for
 . In the base case we are just dealing with @{term upOne}.
  the other cases we define the function ‹?h› which satisfies
  induction hypothesis. Then @{term f} is obtained from this by
  or subtracting one pointwise.

  this proof we use some pattern matching to save on writing. In the
  of the theorem, we match the theorem against ‹?P k› thereby
  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 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
 } are bijections, Theorem @{term all_bij}, and have no fixed
 , 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 -
    ― ‹we start by proving an easy general fact›
  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
  under composition. These facts can later be conjugated to
  obtain the corresponding results for the group on the natural
 .›

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
  by an induction on the definition of @{term Ex1} only using
  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"
    {
      ― ‹first we get an expression for @{term ?ci}›
      {
        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
      ― ‹then we check that this implies @{term ?ci} is›
      ― ‹a member of @{term Ex1}›
      {
        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
  numbers to the integers defined in the library. This will be
  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
  we are interested in is cofinitary. It states that when you
  a function with a bijection the fixed points get mapped
 .›

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
 } of @{term S_inf} that is the conjugate of @{term Ex1} bij @{term
 }, 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] ― ‹automated tools can use the definition›

text ‹We quickly check that this function is of the right type, and
  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
      ― ‹a simple computation using only associativity›
      ― ‹completes the proof›
  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
  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
  shown @{term Ex2} to be a cofinitary group. The formalization
  shows this, we just have to refer to the correct theorems proved
 .›

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