Theory PingPongLemma

section ‹The Ping Pong lemma›

theory "PingPongLemma"
imports
   "HOL-Algebra.Bij"
   FreeGroups
begin

text ‹
The Ping Pong Lemma is a way to recognice a Free Group by its action on
a set (often a topological space or a graph). The name stems from the way that
elements of the set are passed forth and back between the subsets given there.
›

text ‹
We start with two auxiliary lemmas, one about the identity of the group of
bijections, and one about sets of cardinality larger than one.
›

lemma Bij_one[simp]:
  assumes "x ∈ X"
  shows "𝟭⇘BijGroup X⇙ x = x"
using assms by (auto simp add: BijGroup_def)

lemma other_member:
   assumes "I ≠ {}" and "i ∈ I" and "card I ≠ 1"
   obtains j where "j∈I" and "j≠i"
proof(cases "finite I")
  case True
  hence "I - {i} ≠ {}" using ‹card I ≠ 1› and ‹i∈I› by (metis Suc_eq_plus1_left card_Diff_subset_Int card_Suc_Diff1 diff_add_inverse2 diff_self_eq_0 empty_Diff finite.emptyI inf_bot_left minus_nat.diff_0)
  thus ?thesis using that by auto
next
  case False
  hence "I - {i} ≠ {}" by (metis Diff_empty finite.emptyI finite_Diff_insert)
  thus ?thesis using that by auto
qed

text ‹
And now we can attempt the lemma. The gencount condition is a weaker variant
of ``x has to lie outside all subsets'' that is only required if the set of
generators is one. Otherwise, we will be able to find a suitable x to start
with in the proof.
›

lemma ping_pong_lemma:
  assumes "group G"
  and "act ∈ hom G (BijGroup X)"
  and "g ∈ (I → carrier G)"
  and "⟨g ` I⟩⇘G⇙ = carrier G"
  and sub1: "∀i∈I. Xout i ⊆ X"
  and sub2: "∀i∈I. Xin i ⊆ X"
  and disj1: "∀i∈I. ∀j∈I. i ≠ j ⟶ Xout i ∩ Xout j = {}"
  and disj2: "∀i∈I. ∀j∈I. i ≠ j ⟶ Xin i ∩ Xin j = {}"
  and disj3: "∀i∈I. ∀j∈I. Xin i ∩ Xout j = {}"
  and "x ∈ X"
  and gencount: "∀ i . I = {i} ⟶ (x ∉ Xout i ∧ x ∉ Xin i)"
  and ping: "∀i∈I. act (g i) ` (X - Xout i) ⊆ Xin i"
  and pong: "∀i∈I. act (inv⇘G⇙ (g i)) ` (X - Xin i) ⊆ Xout i"
  shows "group.lift G g ∈ iso (ℱ⇘I⇙) G"
proof-
  interpret F: group "ℱ⇘I⇙"
    using assms by (auto simp add: free_group_is_group)
  interpret G: group G by fact
  interpret B: group "BijGroup X" using group_BijGroup by auto
  interpret act: group_hom G "BijGroup X" act by (unfold_locales) fact
  interpret h: group_hom "ℱ⇘I⇙" G "G.lift g" 
    using F.is_group G.is_group G.lift_is_hom assms
    by (auto intro!: group_hom.intro group_hom_axioms.intro)

  show ?thesis
  proof(rule h.group_hom_isoI)
    txt ‹Injectivity is the hard part of the proof.›
    show "∀x∈carrier ℱ⇘I⇙. G.lift g x = 𝟭⇘G⇙ ⟶ x = 𝟭⇘ℱ⇘I⇙⇙"
       proof(rule+)

         txt ‹We lift the Xout and Xin sets to generators and their inveres, and
         create variants of the disj-conditions:›
         define Xout' where "Xout' = (λ(b,i::'d). if b then Xin i else Xout i)"
         define Xin' where "Xin' = (λ(b,i::'d). if b then Xout i else Xin i)"

         have disj1': "∀i∈(UNIV × I). ∀j∈(UNIV × I). i ≠ j ⟶ Xout' i ∩ Xout' j = {}"
           using disj1[rule_format] disj2[rule_format] disj3[rule_format]
           by (auto simp add:Xout'_def Xin'_def split:if_splits, blast+)
         have disj2': "∀i∈(UNIV × I). ∀j∈(UNIV × I). i ≠ j ⟶ Xin' i ∩ Xin' j = {}"
           using disj1[rule_format] disj2[rule_format] disj3[rule_format]
           by (auto simp add:Xout'_def Xin'_def split:if_splits, blast+)
         have disj3': "∀i∈(UNIV × I). ∀j∈(UNIV × I). ¬ canceling i j ⟶ Xin' i ∩ Xout' j = {}"
           using disj1[rule_format] disj2[rule_format] disj3[rule_format]
           by (auto simp add:canceling_def Xout'_def Xin'_def split:if_splits, blast)

         txt ‹We need to pick a suitable element of the set to play ping pong
         with. In particular, it needs to be outside of the Xout-set of the last
         generator in the list, and outside the in-set of the first element. This
         part of the proof is surprisingly tedious, because there are several
         cases, some similar but not the same.
›

         fix w
         assume w: "w ∈ carrier ℱ⇘I⇙"

         obtain x where "x ∈ X"
           and x1: "w = [] ∨ x ∉ Xout' (last w)" 
           and x2: "w = [] ∨ x ∉ Xin' (hd w)"
         proof-
           { assume "I = {}"
             hence "w = []" using w by (auto simp add:free_group_def)
             hence ?thesis using that ‹x∈X› by auto
           }
           moreover
           { assume "card I = 1"
             then obtain i where "I={i}" by (auto dest: card_eq_SucD)
             assume "w≠[]"
             hence "snd (hd w) = i" and "snd (last w) = i"
               using w ‹I={i}›
               apply (cases w, auto simp add:free_group_def)
               apply (cases w rule:rev_exhaust, auto simp add:free_group_def)
               done
             hence ?thesis using gencount[rule_format, OF ‹I={i}›] that[OF ‹x∈X›] ‹w≠[]›
             by (cases "last w", cases "hd w", auto simp add:Xout'_def Xin'_def split:if_splits)
           }
           moreover
           { assume "I ≠ {}" and "card I ≠ 1" and "w ≠ []"

             from ‹w ≠ []› and w
             obtain b i where hd: "hd w = (b,i)" and "i∈I"
               by (cases w, auto simp add:free_group_def)
             from ‹w ≠ []› and w
             obtain b' i' where last: "last w = (b',i')" and "i'∈I"
               by (cases w rule: rev_exhaust, auto simp add:free_group_def)

             txt ‹What follows are two very similar cases, but the correct
             choice of variables depends on where we find x.›
             {
             obtain b'' i'' where
               "(b'',i'') ≠ (b,i)" and
               "(b'',i'') ≠ (b',i')" and
               "¬ canceling (b'', i'') (b',i')" and
               "i''∈I"
             proof(cases "i=i'")
               case True
               obtain j where "j∈I" and "j≠i" using  ‹card I ≠ 1› and ‹i∈I›
                 by -(rule other_member, auto)
               with True show ?thesis using that by (auto simp add:canceling_def)
             next
               case False thus ?thesis using that ‹i∈I› ‹i' ∈ I›
               by (simp add:canceling_def, metis)
             qed
             let ?g = "(b'',i'')"

             assume "x ∈ Xout' (last w)"
             hence "x ∉ Xout' ?g"
               using disj1'[rule_format, OF _ _ ‹?g ≠ (b',i')›]
                   ‹i ∈ I› ‹i'∈I› ‹i''∈I› hd last
               by auto 
             hence "act (G.lift_gi g ?g) x ∈ Xin' ?g" (is "?x ∈ _") using ‹i'' ∈ I› ‹x ∈ X›
               ping[rule_format, OF ‹i'' ∈ I›, THEN subsetD]
               pong[rule_format, OF ‹i'' ∈ I›, THEN subsetD]
               by (auto simp add:G.lift_def G.lift_gi_def Xout'_def Xin'_def)
             hence "?x ∉ Xout' (last w) ∧ ?x ∉ Xin' (hd w)"
               using 
                 disj3'[rule_format, OF _ _ ‹¬ canceling (b'', i'') (b',i')›]
                 disj2'[rule_format, OF _ _  ‹?g ≠ (b,i)›]
                 ‹i ∈ I› ‹i'∈I› ‹i''∈I› hd last
               by (auto simp add: canceling_def) 
             moreover
             note ‹i'' ∈ I›
             hence "g i'' ∈ carrier G" using ‹g ∈ (I → carrier G)› by auto
             hence "G.lift_gi g ?g ∈ carrier G"
               by (auto simp add:G.lift_gi_def inv1_def)
             hence "act (G.lift_gi g ?g) ∈ carrier (BijGroup X)"
               using ‹act ∈ hom G (BijGroup X)› by auto
             hence "?x ∈ X" using ‹x∈X› 
               by (auto simp add:BijGroup_def Bij_def bij_betw_def)
             ultimately have ?thesis using that[of ?x] by auto
             }
             moreover
             {
             obtain b'' i'' where
               "¬ canceling (b'',i'') (b,i)" and
               "¬ canceling (b'',i'') (b',i')" and
               "(b,i) ≠ (b'',i'')" and
               "i''∈I"
             proof(cases "i=i'")
               case True
               obtain j where "j∈I" and "j≠i" using  ‹card I ≠ 1› and ‹i∈I›
                 by -(rule other_member, auto)
               with True show ?thesis using that by (auto simp add:canceling_def)
             next
               case False thus ?thesis using that ‹i∈I› ‹i' ∈ I›
               by (simp add:canceling_def, metis)
             qed
             let ?g = "(b'',i'')" 
             note cancel_sym_neg[OF ‹¬ canceling (b'',i'') (b,i)›]
             note cancel_sym_neg[OF ‹¬ canceling (b'',i'') (b',i')›]

             assume "x ∈ Xin' (hd w)"
             hence "x ∉ Xout' ?g"
               using disj3'[rule_format, OF _ _ ‹¬ canceling (b,i) ?g›]
                   ‹i ∈ I› ‹i'∈I› ‹i''∈I› hd last
               by auto 
             hence "act (G.lift_gi g ?g) x ∈ Xin' ?g" (is "?x ∈ _") using ‹i'' ∈ I› ‹x ∈ X›
               ping[rule_format, OF ‹i'' ∈ I›, THEN subsetD]
               pong[rule_format, OF ‹i'' ∈ I›, THEN subsetD]
               by (auto simp add:G.lift_def G.lift_gi_def Xout'_def Xin'_def)
             hence "?x ∉ Xout' (last w) ∧ ?x ∉ Xin' (hd w)"
               using 
                 disj3'[rule_format, OF _ _ ‹¬ canceling ?g (b',i')›]
                 disj2'[rule_format, OF _ _  ‹(b,i) ≠ ?g›]
                 ‹i ∈ I› ‹i'∈I› ‹i''∈I› hd last
               by (auto simp add: canceling_def) 
             moreover
             note ‹i'' ∈ I›
             hence "g i'' ∈ carrier G" using ‹g ∈ (I → carrier G)› by auto
             hence "G.lift_gi g ?g ∈ carrier G"
               by (auto simp add:G.lift_gi_def)
             hence "act (G.lift_gi g ?g) ∈ carrier (BijGroup X)"
               using ‹act ∈ hom G (BijGroup X)› by auto
             hence "?x ∈ X" using ‹x∈X› 
               by (auto simp add:BijGroup_def Bij_def bij_betw_def)
             ultimately have ?thesis using that[of ?x] by auto
             }
             moreover note calculation
           }
           ultimately show ?thesis using ‹x∈ X› that by auto
         qed
    
         txt ‹The proof works by induction over the length of the word. Each
         inductive step is one ping as in ping pong. At the end, we land in one
         of the subsets of X, so the word cannot be the identity.›
         from x1 and w
         have "w = [] ∨ act (G.lift g w) x ∈ Xin' (hd w)"
         proof(induct w)
           case Nil show ?case by simp
         next case (Cons w ws)
           note C = Cons

           txt ‹The following lemmas establish all ``obvious'' element relations that will be required during the proof.›
           note calculation = Cons(3)
           moreover have "x∈X" by fact
           moreover have "snd w ∈ I" using calculation by (auto simp add:free_group_def) 
           moreover have "g ∈ (I → carrier G)" by fact
           moreover have "g (snd w) ∈ carrier G" using calculation by auto
           moreover have "ws ∈ carrier ℱ⇘I⇙"
              using calculation by (auto intro:cons_canceled simp add:free_group_def)
           moreover have "G.lift g ws ∈ carrier G" and "G.lift g [w] ∈ carrier G"
              using calculation by (auto simp add: free_group_def)
           moreover have "act (G.lift g ws) ∈ carrier (BijGroup X)"
                     and "act (G.lift g [w]) ∈ carrier (BijGroup X)"
                     and "act (G.lift g (w#ws)) ∈ carrier (BijGroup X)"
                     and "act (g (snd w)) ∈ carrier (BijGroup X)"
              using calculation by auto
           moreover have "act (g (snd w)) ∈ Bij X"
              using calculation by (auto simp add:BijGroup_def)
           moreover have "act (G.lift g ws) x ∈ X" (is "?x2 ∈ X")
              using calculation by (auto simp add:BijGroup_def Bij_def bij_betw_def)
           moreover have "act (G.lift g [w]) ?x2 ∈ X"
              using calculation by (auto simp add:BijGroup_def Bij_def bij_betw_def)
           moreover have "act (G.lift g (w#ws)) x ∈ X"
              using calculation by (auto simp add:BijGroup_def Bij_def bij_betw_def)
           moreover note mems = calculation
          
           have "act (G.lift g ws) x ∉ Xout' w"
           proof(cases ws)
             case Nil             
               moreover have "x ∉ Xout' w" using Cons(2) Nil
                 unfolding Xout'_def using mems
                 by (auto split:if_splits)
               ultimately show "act (G.lift g ws) x ∉ Xout' w"
                 using mems by auto
           next case (Cons ww wws)
             hence "act (G.lift g ws) x ∈ Xin' (hd ws)"
               using C mems by simp
             moreover have "Xin' (hd ws) ∩ Xout' w = {}"
             proof-
               have "¬ canceling (hd ws) w"
               proof
                 assume "canceling (hd ws) w"
                 hence "cancels_to_1 (w#ws) wws" using Cons
                    by(auto simp add:cancel_sym cancels_to_1_def cancels_to_1_at_def cancel_at_def)
                 thus False using ‹w#ws ∈ carrier ℱ⇘I⇙›
                    by(auto simp add:free_group_def canceled_def)
               qed  

               have "w ∈ UNIV × I" "hd ws ∈ UNIV × I"
                 using ‹snd w ∈ I› mems Cons
                 by (cases w, auto, cases "hd ws", auto simp add:free_group_def)
               thus ?thesis
                 by- (rule disj3'[rule_format, OF _ _ ‹¬ canceling (hd ws) w›], auto)
             qed
             ultimately show "act (G.lift g ws) x ∉ Xout' w" using Cons by auto
           qed
           show ?case
           proof-
             have "act (G.lift g (w # ws)) x = act (G.lift g ([w] @ ws)) x" by simp
             also have "… = act (G.lift g [w] ⊗⇘G⇙ G.lift g ws) x" 
               using mems by (subst G.lift_append, auto simp add:free_group_def)
             also have "… = (act (G.lift g [w]) ⊗⇘BijGroup X⇙ act (G.lift g ws)) x"
               using mems by (auto simp add:act.hom_mult free_group_def intro!:G.lift_closed)
             also have "… = act (G.lift g [w]) (act (G.lift g ws) x)"
               using mems by (auto simp add:BijGroup_def compose_def)
             also have "… ∉ act (G.lift g [w]) ` Xout' w"
               apply(rule ccontr)
               apply simp
               apply (erule imageE)
               apply (subst (asm) inj_on_eq_iff[of "act (G.lift g [w])" "X"])
               using mems ‹act (G.lift g ws) x ∉ Xout' w› ‹∀i∈I. Xout i ⊆ X› ‹∀i∈I. Xin i ⊆ X› 
               apply (auto simp add:BijGroup_def Bij_def bij_betw_def free_group_def Xout'_def split:if_splits)
               apply blast+
               done
             finally            
             have "act (G.lift g (w # ws)) x ∈ Xin' w"
             proof-
               assume "act (G.lift g (w # ws)) x ∉ act (G.lift g [w]) ` Xout' w"
               hence "act (G.lift g (w # ws)) x ∈ (X - act (G.lift g [w]) ` Xout' w)"
                 using mems by auto
               also have "… ⊆ act (G.lift g [w]) ` X - act (G.lift g [w]) ` Xout' w"
                     using ‹act (G.lift g [w]) ∈ carrier (BijGroup X)›
                     by (auto simp add:BijGroup_def Bij_def bij_betw_def)
               also have "… ⊆ act (G.lift g [w]) ` (X - Xout' w)"
                      by (rule image_diff_subset)
               also have "... ⊆ Xin' w"
               proof(cases "fst w")
                 assume "¬ fst w"
                 thus ?thesis
                   using mems
                   by (auto intro!: ping[rule_format, THEN subsetD] simp add: Xout'_def Xin'_def G.lift_def G.lift_gi_def free_group_def) 
               next assume "fst w"
                 thus ?thesis
                   using mems
                   by (auto intro!: pong[rule_format, THEN subsetD] simp add: restrict_def inv_BijGroup Xout'_def Xin'_def G.lift_def G.lift_gi_def free_group_def) 
               qed
               finally show ?thesis .
             qed
             thus ?thesis by simp
           qed
         qed
           moreover assume "G.lift g w = 𝟭⇘G⇙"
         ultimately show "w = 𝟭⇘ℱ⇘I⇙⇙"
           using ‹x∈X› Cons(1) x2 ‹w ∈ carrier ℱ⇘I⇙›
         by (cases w, auto simp add:free_group_def Xin'_def split:if_splits)       
       qed
    next
    txt ‹Surjectivity is relatively simple, and often not even mentioned in
    human proofs.›
    have "G.lift g ` carrier ℱ⇘I⇙ =
          G.lift g ` ⟨ι ` I⟩⇘ℱ⇘I⇙⇙"
      by (metis gens_span_free_group)
    also have "... = ⟨G.lift g ` (ι ` I) ⟩⇘G⇙"
       by (auto intro!:h.hom_span simp add: insert_closed)
    also have "… = ⟨g ` I ⟩⇘G⇙"
       proof-
         have "∀ i ∈ I. G.lift g (ι i) = g i"
           using ‹g ∈ (I → carrier G)›         
           by (auto simp add:insert_def G.lift_def G.lift_gi_def intro:G.r_one)
         then have "G.lift g ` (ι ` I) = g ` I "
           by (auto intro!: image_cong simp add: image_comp [symmetric, THEN sym])
         thus ?thesis by simp
       qed
     also have "… = carrier G" using assms by simp
     finally show "G.lift g ` carrier ℱ⇘I⇙ = carrier G".
  qed
qed

end