# Theory PingPongLemma

Up to index of Isabelle/HOL/Free-Groups

theory PingPongLemma
imports Bij FreeGroups
`header {* The Ping Pong lemma *}theory "PingPongLemma"imports   "~~/src/HOL/Algebra/Bij"   "FreeGroups"begintext {*The Ping Pong Lemma is a way to recognice a Free Group by its action ona set (often a topological space or a graph). The name stems from the way thatelements of the set are passed forth and back between the subsets given there.*}text {*We start with two auxillary lemmas, one about the identity of the group ofbijections, and one about sets of cardinality larger than one.*}lemma Bij_one[simp]:  assumes "x ∈ X"  shows "\<one>⇘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 autonext  case False  hence "I - {i} ≠ {}" by (metis Diff_empty finite.emptyI finite_Diff_insert)  thus ?thesis using that by autoqedtext {*And now we can attempt the lemma. The gencount condition is a weaker variantof ``x has to lie outside all subsets'' that is only required if the set ofgenerators is one. Otherwise, we will be able to find a suitable x to startwith 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 (\<F>⇘I⇙) G"proof-  interpret F: group "\<F>⇘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 "\<F>⇘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 \<F>⇘I⇙. G.lift g x = \<one>⇘G⇙ --> x = \<one>⇘\<F>⇘I⇙⇙"       proof(rule+)         txt {* We lift the Xout and Xin sets to generators and their inveres, and         create variants of the disj-conditions: *}         def Xout' ≡ "λ(b,i::'d). if b then Xin i else Xout i"         def 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 \<F>⇘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 \<F>⇘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 \<F>⇘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 = \<one>⇘G⇙"         ultimately show "w = \<one>⇘\<F>⇘I⇙⇙"           using `x∈X` Cons(1) x2 `w ∈ carrier \<F>⇘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 \<F>⇘I⇙ =          G.lift g ` ⟨ι ` I⟩⇘\<F>⇘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)         hence "G.lift g ` (ι ` I) = g ` I "           by (auto intro!: image_cong simp add: image_compose[THEN sym])         thus ?thesis by simp       qed     also have "… = carrier G" using assms by simp     finally show "G.lift g ` carrier \<F>⇘I⇙ = carrier G".  qedqedend`