Theory Isomorphisms

section ‹Isomorphisms of Free Groups›

theory "Isomorphisms"
imports
   UnitGroup
   "HOL-Algebra.IntRing"
   FreeGroups
   C2
   "HOL-Cardinals.Cardinal_Order_Relation"
begin

subsection ‹The Free Group over the empty set›

text ‹The Free Group over an empty set of generators is isomorphic to the trivial
group.›

lemma free_group_over_empty_set: "∃h. h ∈ iso ℱ⇘{}⇙ unit_group"
proof(rule group.unit_group_unique)
  show "group ℱ⇘{}⇙" by (rule free_group_is_group)
next
  have "carrier ℱ⇘{}::'a set⇙ = {[]}"
    by (auto simp add:free_group_def)
  thus "card (carrier ℱ⇘{}::'a set⇙) = 1"
    by simp
qed

subsection ‹The Free Group over one generator›

text ‹The Free Group over one generator is isomorphic to the free abelian group
over one element, also known as the integers.›

abbreviation "int_group"
  where "int_group ≡ ⦇ carrier = carrier 𝒵, monoid.mult = (+), one = 0::int ⦈"

lemma replicate_set_eq[simp]: "∀x ∈ set xs. x = y ⟹ xs = replicate (length xs) y"
  by(induct xs)auto

lemma int_group_gen_by_one: "⟨{1}⟩⇘int_group⇙ = carrier int_group"
proof
  show "⟨{1}⟩⇘int_group⇙ ⊆ carrier int_group"
    by auto
  show "carrier int_group ⊆ ⟨{1}⟩⇘int_group⇙"
  proof
    interpret int: group int_group
      using int.a_group by auto
    fix x
    have plus1: "1 ∈ ⟨{1}⟩⇘int_group⇙"
      by (auto intro:gen_span.gen_gens)
    hence "inv⇘int_group⇙ 1 ∈ ⟨{1}⟩⇘int_group⇙"
      by (auto intro:gen_span.gen_inv)
    moreover
    have "-1 = inv⇘int_group⇙ 1" 
      by (rule sym, rule int.inv_equality) simp_all
    ultimately
    have minus1: "-1 ∈ ⟨{1}⟩⇘int_group⇙"
      by (simp)

    show "x ∈ ⟨{1::int}⟩⇘int_group⇙" (*
    It does not work directly, unfortunately:
    apply(induct x rule:int_induct[of _ "0::int"])
    apply (auto simp add: int_arith_rules intro:gen_span.intros[of int_group])
    *)
    proof(induct x rule:int_induct[of _ "0::int"])
    case base
      have "𝟭⇘int_group⇙ ∈ ⟨{1::int}⟩⇘int_group⇙"
        by (rule gen_span.gen_one)
      thus"0 ∈ ⟨{1}⟩⇘int_group⇙"
        by simp
    next
    case (step1 i)
      from ‹i ∈ ⟨{1}⟩⇘int_group⇙› and plus1
      have "i ⊗⇘int_group⇙ 1 ∈ ⟨{1}⟩⇘int_group⇙" 
        by (rule gen_span.gen_mult)
      thus "i + 1 ∈ ⟨{1}⟩⇘int_group⇙" by simp
    next
    case (step2 i)
      from ‹i ∈ ⟨{1}⟩⇘int_group⇙› and minus1
      have "i ⊗⇘int_group⇙ -1 ∈ ⟨{1}⟩⇘int_group⇙" 
        by (rule gen_span.gen_mult)
      thus "i - 1 ∈ ⟨{1}⟩⇘int_group⇙"
        by simp
    qed
  qed
qed

lemma free_group_over_one_gen: "∃h. h ∈ iso ℱ⇘{()}⇙ int_group"
proof-
  interpret int: group int_group 
    using int.a_group by auto
  define f :: "unit ⇒ int" where "f x = 1" for x
  have "f ∈ {()} → carrier int_group"
    by auto
  hence "int.lift f ∈ hom ℱ⇘{()}⇙ int_group"
    by (rule int.lift_is_hom)
  then
  interpret hom: group_hom "ℱ⇘{()}⇙" int_group "int.lift f"
    unfolding group_hom_def group_hom_axioms_def
    using int.a_group by(auto intro: free_group_is_group)
    
  { (* This shows injectiveness of the given map *)
    fix x
    assume "x ∈ carrier ℱ⇘{()}⇙"
    hence "canceled x" by (auto simp add:free_group_def)
    assume "int.lift f x = (0::int)"
    have "x = []" 
    proof(rule ccontr)
      assume "x ≠ []"
      then obtain a and xs where "x = a # xs" by (cases x, auto)
      hence "length (takeWhile (λy. y = a) x) > 0" by auto
      then obtain i where i: "length (takeWhile (λy. y = a) x) = Suc i" 
        by (cases "length (takeWhile (λy. y = a) x)", auto)
      have "Suc i ≥ length x"
      proof(rule ccontr)
        assume "¬ length x ≤ Suc i"
        hence "length (takeWhile (λy. y = a) x) < length x" using i by simp
        hence "¬ (λy. y = a) (x ! length (takeWhile (λy. y = a) x))"
          by (rule nth_length_takeWhile)
        hence "¬ (λy. y = a) (x ! Suc i)" using i by simp
        hence "fst (x ! Suc i) ≠ fst a" by (cases "x ! Suc i", cases "a", auto)
        moreover
        {
          have "takeWhile (λy. y = a) x ! i = x ! i"
            using i by (auto intro: takeWhile_nth)
          moreover
          have "(takeWhile (λy. y = a) x) ! i ∈ set (takeWhile (λy. y = a) x)"
            using i by auto
          ultimately
          have "(λy. y = a) (x ! i)"
            by (auto dest:set_takeWhileD)
        }
        hence "fst (x ! i) = fst a" by auto
        moreover
        have "snd (x ! i) = snd (x ! Suc i)" by simp
        ultimately
        have "canceling (x ! i) (x ! Suc i)" unfolding canceling_def by auto
        hence "cancels_to_1_at i x (cancel_at i x)"
          using ‹¬ length x ≤ Suc i› unfolding cancels_to_1_at_def 
          by (auto simp add:length_takeWhile_le)
        hence "cancels_to_1 x (cancel_at i x)" unfolding cancels_to_1_def by auto
        hence "¬ canceled x" unfolding canceled_def by auto
        thus False using ‹canceled x› by contradiction
      qed
      hence "length (takeWhile (λy. y = a) x) = length x"
        using i[THEN sym] by (auto dest:le_antisym simp add:length_takeWhile_le)
      hence "takeWhile (λy. y = a) x = x"
        by (subst takeWhile_eq_take, simp)
      moreover
      have "∀y ∈ set (takeWhile (λy. y = a) x). y = a"
        by (auto dest: set_takeWhileD)
      ultimately
      have "∀y ∈ set x. y = a" by auto
      hence "x = replicate (length x) a" by simp
      hence "int.lift f x = int.lift f (replicate (length x) a)" by simp
      also have "... = pow int_group (int.lift_gi f a) (length x)"
        apply (induct x)
        using local.int.nat_pow_Suc local.int.nat_pow_0
         apply (auto simp: int.lift_def [simplified])
        done
      also have "... = (int.lift_gi f a) * int (length x)"
        apply (induct x)
        using local.int.nat_pow_Suc local.int.nat_pow_0
        by (auto simp: int_distrib)
      finally have "… = 0" using ‹int.lift f x = 0› by simp
      hence "nat (abs (group.lift_gi int_group f a * int (length x))) = 0" by simp
      hence "nat (abs (group.lift_gi int_group f a)) * length x = 0" by simp
      hence "nat (abs (group.lift_gi int_group f a)) = 0"
        using ‹x ≠ []› by auto
      moreover
      have "inv⇘int_group⇙ 1 = -1" 
        using int.inv_equality by auto
      hence "abs (group.lift_gi int_group f a) = 1"
      using int.is_group
        by(auto simp add: group.lift_gi_def f_def)
      ultimately
      show False by simp
    qed
  }
  hence "∀x∈carrier ℱ⇘{()}⇙. int.lift f x = 𝟭⇘int_group⇙ ⟶ x = 𝟭⇘ℱ⇘{()}⇙⇙"
    by (auto simp add:free_group_def)
  moreover
  {
    have "carrier ℱ⇘{()}⇙ = ⟨insert`{()}⟩⇘ℱ⇘{()}⇙⇙"
      by (rule gens_span_free_group[THEN sym])
    moreover
    have "carrier int_group = ⟨{1}⟩⇘int_group⇙"
      by (rule int_group_gen_by_one[THEN sym])
    moreover
    have "int.lift f ` insert ` {()} = {1}"
      by (auto simp add: int.lift_def [simplified] insert_def f_def int.lift_gi_def [simplified])
    moreover
    have  "int.lift f ` ⟨insert`{()}⟩⇘ℱ⇘{()}⇙⇙ = ⟨int.lift f ` (insert `{()})⟩⇘int_group⇙"
      by (rule hom.hom_span, auto intro:insert_closed)
    ultimately
    have "int.lift f ` carrier ℱ⇘{()}⇙ = carrier int_group"
      by simp
  }
  ultimately
  have "int.lift f ∈ iso ℱ⇘{()}⇙ int_group"
    using ‹int.lift f ∈ hom ℱ⇘{()}⇙ int_group›
    using hom.hom_mult int.is_group
    by (auto intro:group_isoI simp add: free_group_is_group)
  thus ?thesis by auto
qed

subsection ‹Free Groups over isomorphic sets of generators›

text ‹Free Groups are isomorphic if their set of generators are isomorphic.›

definition lift_generator_function :: "('a ⇒ 'b) ⇒ (bool × 'a) list ⇒ (bool × 'b) list"
where "lift_generator_function f = map (map_prod id f)"

theorem isomorphic_free_groups:
  assumes "bij_betw f gens1 gens2"
  shows "lift_generator_function f ∈ iso ℱ⇘gens1⇙ ℱ⇘gens2⇙"
unfolding lift_generator_function_def
proof(rule group_isoI)
  show "∀x∈carrier ℱ⇘gens1⇙.
       map (map_prod id f) x = 𝟭⇘ℱ⇘gens2⇙⇙ ⟶ x = 𝟭⇘ℱ⇘gens1⇙⇙"
    by(auto simp add:free_group_def)
next
  from ‹bij_betw f gens1 gens2› have "inj_on f gens1" by (auto simp:bij_betw_def)
  show "map (map_prod id f) ` carrier ℱ⇘gens1⇙ = carrier ℱ⇘gens2⇙"
  proof(rule Set.set_eqI,rule iffI)
    from ‹bij_betw f gens1 gens2› have "f ` gens1 = gens2" by (auto simp:bij_betw_def)
    fix x :: "(bool × 'b) list"
    assume "x ∈ image (map (map_prod id f)) (carrier ℱ⇘gens1⇙)"
    then obtain y :: "(bool × 'a) list" where "x = map (map_prod id f) y"
                    and "y ∈ carrier ℱ⇘gens1⇙" by auto
    from ‹y ∈ carrier ℱ⇘gens1⇙›
    have "canceled y" and "y ∈ lists(UNIV×gens1)" by (auto simp add:free_group_def)

    from ‹y ∈ lists (UNIV×gens1)›
      and ‹x = map (map_prod id f) y›
      and ‹image f gens1 = gens2›
    have "x ∈ lists (UNIV×gens2)"
      by (auto iff:lists_eq_set)
    moreover

    from ‹x = map (map_prod id f) y›
     and ‹y ∈ lists (UNIV×gens1)›
     and ‹canceled y›
     and ‹inj_on f gens1›
    have "canceled x"
      by (auto intro!:rename_gens_canceled subset_inj_on[OF ‹inj_on f gens1›] iff:lists_eq_set)
    ultimately
    show "x ∈ carrier ℱ⇘gens2⇙" by (simp add:free_group_def)
  next
    fix x
    assume "x ∈ carrier ℱ⇘gens2⇙"
    hence "canceled x" and "x ∈ lists (UNIV×gens2)"
      unfolding free_group_def by auto
    define y where "y = map (map_prod id (the_inv_into gens1 f)) x"
    have "map (map_prod id f) y =
          map (map_prod id f) (map (map_prod id (the_inv_into gens1 f)) x)"
      by (simp add:y_def)
    also have "… = map (map_prod id f ∘ map_prod id (the_inv_into gens1 f)) x"
      by simp
    also have "… = map (map_prod id (f ∘ the_inv_into gens1 f)) x"
      by auto
    also have "… = map id x"
    proof(rule map_ext, rule impI)
      fix xa :: "bool × 'b"
      assume "xa ∈ set x"
      from ‹x ∈ lists (UNIV×gens2)›
      have "set (map snd x) ⊆ gens2"  by auto
      hence "snd ` set x ⊆ gens2" by (simp add: set_map)
      with ‹xa ∈ set x› have "snd xa ∈ gens2" by auto
      with ‹bij_betw f gens1 gens2› have "snd xa ∈ f`gens1"
        by (auto simp add: bij_betw_def)

      have "map_prod id (f ∘ the_inv_into gens1 f) xa
            = map_prod id (f ∘ the_inv_into gens1 f) (fst xa, snd xa)" by simp
      also have "… = (fst xa, f (the_inv_into gens1 f (snd xa)))"
        by (auto simp del:prod.collapse)
      also
      from ‹snd xa ∈ image f gens1› and ‹inj_on f gens1›
      have "… = (fst xa, snd xa)"
        by (auto elim:f_the_inv_into_f simp del:prod.collapse)
      also have "… = id xa" by simp
      finally show "map_prod id (f ∘ the_inv_into gens1 f) xa = id xa".
    qed
    also have "… = x" unfolding id_def by auto
    finally have "map (map_prod id f) y = x".
    moreover
    {
      from ‹bij_betw f gens1 gens2›
      have "bij_betw (the_inv_into gens1 f) gens2 gens1" by (rule bij_betw_the_inv_into)
      hence "inj_on (the_inv_into gens1 f) gens2" by (rule bij_betw_imp_inj_on)

      with ‹canceled x›      
       and ‹x ∈ lists (UNIV×gens2)›
      have "canceled y"
        by (auto intro!:rename_gens_canceled[OF subset_inj_on] simp add:y_def)
      moreover
      {
        from ‹bij_betw (the_inv_into gens1 f) gens2 gens1›
         and ‹x∈lists(UNIV×gens2)›
        have "y ∈ lists(UNIV×gens1)"
          unfolding y_def and bij_betw_def
          by (auto iff:lists_eq_set dest!:subsetD)
      }
      ultimately
      have "y ∈ carrier ℱ⇘gens1⇙" by (simp add:free_group_def)
    }
    ultimately
    show "x ∈ map (map_prod id f) ` carrier ℱ⇘gens1⇙" by auto
  qed
next
  from ‹bij_betw f gens1 gens2› have "inj_on f gens1" by (auto simp:bij_betw_def)
  {
  fix x
  assume "x ∈ carrier ℱ⇘gens1⇙"
  fix y
  assume "y ∈ carrier ℱ⇘gens1⇙"

  from ‹x ∈ carrier ℱ⇘gens1⇙› and ‹y ∈ carrier ℱ⇘gens1⇙›
  have "x ∈ lists(UNIV×gens1)" and "y ∈ lists(UNIV×gens1)"
    by (auto simp add:occuring_gens_in_element)
(*  hence "occuring_generators (x@y) ⊆ gens1"
    by(auto simp add:occuring_generators_def)
  with `inj_on f gens1` have "inj_on f (occuring_generators (x@y))"
    by (rule subset_inj_on) *)

  have "map (map_prod id f) (x ⊗⇘ℱ⇘gens1⇙⇙ y)
       = map (map_prod id f) (normalize (x@y))" by (simp add:free_group_def)
  also (* from `inj_on f (occuring_generators (x@y))` *)
       from ‹x ∈ lists(UNIV×gens1)› and ‹y ∈ lists(UNIV×gens1)›
        and ‹inj_on f gens1›
       have "… = normalize (map (map_prod id f) (x@y))"
         by -(rule rename_gens_normalize[THEN sym],
              auto intro!: subset_inj_on[OF ‹inj_on f gens1›] iff:lists_eq_set)
  also have "… = normalize (map (map_prod id f) x @ map (map_prod id f) y)"
       by (auto)
  also have "… = map (map_prod id f) x ⊗⇘ℱ⇘gens2⇙⇙ map (map_prod id f) y"
       by (simp add:free_group_def)
  finally have "map (map_prod id f) (x ⊗⇘ℱ⇘gens1⇙⇙ y) =
                map (map_prod id f) x ⊗⇘ℱ⇘gens2⇙⇙ map (map_prod id f) y".
  }
  thus "∀x∈carrier ℱ⇘gens1⇙.
       ∀y∈carrier ℱ⇘gens1⇙.
          map (map_prod id f) (x ⊗⇘ℱ⇘gens1⇙⇙ y) =
          map (map_prod id f) x ⊗⇘ℱ⇘gens2⇙⇙ map (map_prod id f) y"
   by auto
qed (auto intro: free_group_is_group)

subsection ‹Bases of isomorphic free groups›

text ‹
Isomorphic free groups have bases of same cardinality. The proof is very different
for infinite bases and for finite bases.

The proof for the finite case uses the set of of homomorphisms from the free
group to the group with two elements, as suggested by Christian Sievers. The
definition of @{term hom} is not suitable for proofs about the cardinality of that
set, as its definition does not require extensionality. This is amended by the
following definition:
›

definition homr
  where "homr G H = {h. h ∈ hom G H ∧ h ∈ extensional (carrier G)}"

lemma (in group_hom) restrict_hom[intro!]:
  shows "restrict h (carrier G) ∈ homr G H"
  unfolding homr_def and hom_def
  by (auto)

lemma hom_F_C2_Powerset:
  "∃ f. bij_betw f (Pow X) (homr (ℱ⇘X⇙) C2)"
proof
  interpret F: group "ℱ⇘X⇙" by (rule free_group_is_group)
  interpret C2: group C2 by (rule C2_is_group)
  let ?f = "λS . restrict (C2.lift (λx. x ∈ S)) (carrier ℱ⇘X⇙)"
  let ?f' = "λh . X ∩ Collect(h ∘ insert)"
  show "bij_betw ?f (Pow X) (homr (ℱ⇘X⇙) C2)"
  proof(induct rule: bij_betwI[of ?f _ _ ?f'])
  case 1 show ?case
    proof
      fix S assume "S ∈ Pow X"
      interpret h: group_hom "ℱ⇘X⇙" C2 "C2.lift (λx. x ∈ S)"
        by unfold_locales (auto intro: C2.lift_is_hom)
      show "?f S ∈ homr ℱ⇘X⇙ C2"
        by (rule h.restrict_hom)
     qed
  next
  case 2 show ?case by auto next
  case (3 S) show ?case
    proof (induct rule: Set.set_eqI)
      case (1 x) show ?case
      proof(cases "x ∈ X")
      case True thus ?thesis using insert_closed[of x X]
         by (auto simp add:insert_def C2.lift_def C2.lift_gi_def)
      next case False thus ?thesis using 3 by auto
    qed
  qed
  next
  case (4 h)
    hence hom: "h ∈ hom ℱ⇘X⇙ C2"
      and extn: "h ∈ extensional (carrier ℱ⇘X⇙)"
      unfolding homr_def by auto
    have "∀x ∈ carrier ℱ⇘X⇙ . h x = group.lift C2 (λz. z ∈ X & (h ∘ FreeGroups.insert) z) x"
     by (rule C2.lift_is_unique[OF C2_is_group _ hom, of "(λz. z ∈ X & (h ∘ FreeGroups.insert) z)"],
             auto)
    thus ?case
    by -(rule extensionalityI[OF restrict_extensional extn], auto)
  qed
qed

lemma group_iso_betw_hom:
  assumes "group G1" and "group G2"
      and iso: "i ∈ iso G1 G2"
  shows   "∃ f . bij_betw f (homr G2 H) (homr G1 H)"
proof-
  interpret G2: group G2 by (rule ‹group G2›)
  let ?i' = "restrict (inv_into (carrier G1) i) (carrier G2)"
  have "inv_into (carrier G1) i ∈ iso G2 G1"
    by (simp add: ‹group G1› group.iso_set_sym iso)    
  hence iso': "?i' ∈ iso G2 G1"
    by (auto simp add:Group.iso_def hom_def G2.m_closed)
  show ?thesis
  proof(rule, induct rule: bij_betwI[of "(λh. compose (carrier G1) h i)" _ _ "(λh. compose (carrier G2) h ?i')"])
  case 1
    show ?case
    proof
      fix h assume "h ∈ homr G2 H"
      hence "compose (carrier G1) h i ∈ hom G1 H"
        using iso
        by (auto intro: group.hom_compose[OF ‹group G1›, of _ G2] simp add:Group.iso_def homr_def)
      thus "compose (carrier G1) h i ∈ homr G1 H"
        unfolding homr_def by simp
     qed
  next
  case 2
    show ?case
    proof
      fix h assume "h ∈ homr G1 H"
      hence "compose (carrier G2) h ?i' ∈ hom G2 H"
        using iso'
        by (auto intro: group.hom_compose[OF ‹group G2›, of _ G1] simp add:Group.iso_def homr_def)
      thus "compose (carrier G2) h ?i' ∈ homr G2 H"
        unfolding homr_def by simp
     qed
  next
  case (3 x)
    hence "compose (carrier G2) (compose (carrier G1) x i) ?i'
          = compose (carrier G2) x (compose (carrier G2) i ?i')"
      using iso iso'
      by (auto intro: compose_assoc[THEN sym]   simp add:Group.iso_def hom_def homr_def)
    also have "… = compose (carrier G2) x (λy∈carrier G2. y)"
      using iso
      by (subst compose_id_inv_into, auto simp add:Group.iso_def hom_def bij_betw_def)
    also have "… = x"
      using 3
      by (auto intro:compose_Id simp add:homr_def)
    finally
    show ?case .
  next
  case (4 y)
    hence "compose (carrier G1) (compose (carrier G2) y ?i') i
          = compose (carrier G1) y (compose (carrier G1) ?i' i)"
      using iso iso'
      by (auto intro: compose_assoc[THEN sym] simp add:Group.iso_def hom_def homr_def)
    also have "… = compose (carrier G1) y (λx∈carrier G1. x)"
      using iso
      by (subst compose_inv_into_id, auto simp add:Group.iso_def hom_def bij_betw_def)
    also have "… = y"
      using 4
      by (auto intro:compose_Id simp add:homr_def)
    finally
    show ?case .
  qed
qed

lemma isomorphic_free_groups_bases_finite:
  assumes iso: "i ∈ iso ℱ⇘X⇙ ℱ⇘Y⇙"
      and finite: "finite X"
  shows "∃f. bij_betw f X Y"
proof-
  obtain f
    where "bij_betw f (homr ℱ⇘Y⇙ C2) (homr ℱ⇘X⇙ C2)"
    using group_iso_betw_hom[OF free_group_is_group free_group_is_group iso]
    by auto
  moreover
  obtain g'
    where "bij_betw g' (Pow X) (homr (ℱ⇘X⇙) C2)"
    using hom_F_C2_Powerset by auto
  then obtain g
    where "bij_betw g (homr (ℱ⇘X⇙) C2) (Pow X)"
    by (auto intro: bij_betw_inv_into)
  moreover
  obtain h
    where "bij_betw h (Pow Y) (homr (ℱ⇘Y⇙) C2)"
    using hom_F_C2_Powerset by auto
  ultimately
  have "bij_betw (g ∘ f ∘ h) (Pow Y) (Pow X)"
    by (auto intro: bij_betw_trans)
  hence eq_card: "card (Pow Y) = card (Pow X)"
    by (rule bij_betw_same_card)
  with finite
  have "finite (Pow Y)"
   by -(rule card_ge_0_finite, auto simp add:card_Pow)
  hence finite': "finite Y" by simp

  with eq_card finite
  have "card X = card Y"
   by (auto simp add:card_Pow)
  with finite finite'
  show ?thesis
   by (rule finite_same_card_bij)
qed

text ‹
The proof for the infinite case is trivial once the fact that the free group
over an infinite set has the same cardinality is established.
›

lemma free_group_card_infinite:
  assumes "¬ finite X"
  shows "|X| =o |carrier ℱ⇘X⇙|"
proof-
  have "inj_on insert X"
    by (rule inj_onI) (auto simp add: insert_def)
  moreover have "insert ` X ⊆ carrier ℱ⇘X⇙"
    by (auto intro: insert_closed)
  ultimately have "∃f. inj_on f X ∧ f ` X ⊆ carrier ℱ⇘X⇙"
    by auto
  then have "|X| ≤o |carrier ℱ⇘X⇙|"
    by (simp add: card_of_ordLeq)
  moreover
  have "|carrier ℱ⇘X⇙| ≤o |lists ((UNIV::bool set)×X)|"
    by (auto intro!:card_of_mono1 simp add:free_group_def)
  moreover
  have "|lists ((UNIV::bool set)×X)| =o |(UNIV::bool set)×X|"
    using ‹¬ finite X›
    by (auto intro:card_of_lists_infinite dest!:finite_cartesian_productD2)
  moreover
  have  "|(UNIV::bool set)×X| =o |X|"
    using ‹¬ finite X›
    by (auto intro: card_of_Times_infinite[OF _ _ ordLess_imp_ordLeq[OF finite_ordLess_infinite2], THEN conjunct2])
  ultimately
  show "|X| =o |carrier ℱ⇘X⇙|"
    by (subst ordIso_iff_ordLeq, auto intro: ord_trans)
qed

theorem isomorphic_free_groups_bases:
  assumes iso: "i ∈ iso ℱ⇘X⇙ ℱ⇘Y⇙"
  shows "∃f. bij_betw f X Y"
proof(cases "finite X")
case True
  thus ?thesis using iso by -(rule isomorphic_free_groups_bases_finite)
next
case False show ?thesis
  proof(cases "finite Y")
  case True
  from iso obtain i' where "i' ∈ iso ℱ⇘Y⇙ ℱ⇘X⇙"
    using free_group_is_group group.iso_set_sym by blast
  with ‹finite Y›
  have "∃f. bij_betw f Y X" by -(rule isomorphic_free_groups_bases_finite)
  thus "∃f. bij_betw f X Y" by (auto intro: bij_betw_the_inv_into) next
case False
  from ‹¬ finite X› have "|X| =o |carrier ℱ⇘X⇙|" 
    by (rule free_group_card_infinite)
  moreover
  from ‹¬ finite Y› have "|Y| =o |carrier ℱ⇘Y⇙|" 
    by (rule free_group_card_infinite)
  moreover
  from iso have "|carrier ℱ⇘X⇙| =o |carrier ℱ⇘Y⇙|"
    by (auto simp add:Group.iso_def iff:card_of_ordIso[THEN sym])
  ultimately
  have "|X| =o |Y|" by (auto intro: ordIso_equivalence)
  thus ?thesis by (subst card_of_ordIso)
qed
qed

end