section ‹Cancelation of words of generators and their inverses› theory Cancelation imports "HOL-Proofs-Lambda.Commutation" begin text ‹ This theory defines cancelation via relations. The one-step relation @{term "cancels_to_1 a b"} describes that @{term b} is obtained from @{term a} by removing exactly one pair of generators, while @{term cancels_to} is the reflexive transitive hull of that relation. Due to confluence, this relation has a normal form, allowing for the definition of @{term normalize}. › subsection ‹Auxiliary results› text ‹Some lemmas that would be useful in a more general setting are collected beforehand.› subsubsection ‹Auxiliary results about relations› text ‹ These were helpfully provided by Andreas Lochbihler. › theorem lconfluent_confluent: "⟦ wfP (R^--1); ⋀a b c. R a b ⟹ R a c ⟹ ∃d. R^** b d ∧ R^** c d ⟧ ⟹ confluent R" by(auto simp add: diamond_def commute_def square_def intro: newman) lemma confluentD: "⟦ confluent R; R^** a b; R^** a c ⟧ ⟹ ∃d. R^** b d ∧ R^** c d" by(auto simp add: commute_def diamond_def square_def) lemma tranclp_DomainP: "R^++ a b ⟹ Domainp R a" by(auto elim: converse_tranclpE) lemma confluent_unique_normal_form: "⟦ confluent R; R^** a b; R^** a c; ¬ Domainp R b; ¬ Domainp R c ⟧ ⟹ b = c" by(fastforce dest!: confluentD[of R a b c] dest: tranclp_DomainP rtranclpD[where a=b] rtranclpD[where a=c]) subsection ‹Definition of the @{term "canceling"} relation› type_synonym 'a "g_i" = "(bool × 'a)" (* A generator or its inverse *) type_synonym 'a "word_g_i" = "'a g_i list" (* A word in the generators or their inverses *) text ‹ These type aliases encode the notion of a ``generator or its inverse'' (@{typ "'a g_i"}) and the notion of a ``word in generators and their inverses'' (@{typ "'a word_g_i"}), which form the building blocks of Free Groups. › definition canceling :: "'a g_i ⇒ 'a g_i ⇒ bool" where "canceling a b = ((snd a = snd b) ∧ (fst a ≠ fst b))" subsubsection ‹Simple results about canceling› text ‹ A generators cancels with its inverse, either way. The relation is symmetic. › lemma cancel_cancel: "⟦ canceling a b; canceling b c ⟧ ⟹ a = c" by (auto intro: prod_eqI simp add:canceling_def) lemma cancel_sym: "canceling a b ⟹ canceling b a" by (simp add:canceling_def) lemma cancel_sym_neg: "¬canceling a b ⟹ ¬canceling b a" by (rule classical, simp add:canceling_def) subsection ‹Definition of the @{term "cancels_to"} relation› text ‹ First, we define the function that removes the @{term i}th and ‹(i+1)›st element from a word of generators, together with basic properties. › definition cancel_at :: "nat ⇒ 'a word_g_i ⇒ 'a word_g_i" where "cancel_at i l = take i l @ drop (2+i) l" lemma cancel_at_length[simp]: "1+i < length l ⟹ length (cancel_at i l) = length l - 2" by(auto simp add: cancel_at_def) lemma cancel_at_nth1[simp]: "⟦ n < i; 1+i < length l ⟧ ⟹ (cancel_at i l) ! n = l ! n" by(auto simp add: cancel_at_def nth_append) lemma cancel_at_nth2[simp]: assumes "n ≥ i" and "n < length l - 2" shows "(cancel_at i l) ! n = l ! (n + 2)" proof- from ‹n ≥ i› and ‹n < length l - 2› have "i = min (length l) i" by auto with ‹n ≥ i› and ‹n < length l - 2› show "(cancel_at i l) ! n = l ! (n + 2)" by(auto simp add: cancel_at_def nth_append nth_via_drop) qed text ‹ Then we can define the relation @{term "cancels_to_1_at i a b"} which specifies that @{term b} can be obtained by @{term a} by canceling the @{term i}th and ‹(i+1)›st position. Based on that, we existentially quantify over the position ‹i› to obtain the relation ‹cancels_to_1›, of which ‹cancels_to› is the reflexive and transitive closure. A word is ‹canceled› if it can not be canceled any futher. › definition cancels_to_1_at :: "nat ⇒ 'a word_g_i ⇒ 'a word_g_i ⇒ bool" where "cancels_to_1_at i l1 l2 = (0≤i ∧ (1+i) < length l1 ∧ canceling (l1 ! i) (l1 ! (1+i)) ∧ (l2 = cancel_at i l1))" definition cancels_to_1 :: "'a word_g_i ⇒ 'a word_g_i ⇒ bool" where "cancels_to_1 l1 l2 = (∃i. cancels_to_1_at i l1 l2)" definition cancels_to :: "'a word_g_i ⇒ 'a word_g_i ⇒ bool" where "cancels_to = cancels_to_1^**" lemma cancels_to_trans [trans]: "⟦ cancels_to a b; cancels_to b c ⟧ ⟹ cancels_to a c" by (auto simp add:cancels_to_def) definition canceled :: "'a word_g_i ⇒ bool" where "canceled l = (¬ Domainp cancels_to_1 l)" (* Alternative view on cancelation, sometimes easier to work with *) lemma cancels_to_1_unfold: assumes "cancels_to_1 x y" obtains xs1 x1 x2 xs2 where "x = xs1 @ x1 # x2 # xs2" and "y = xs1 @ xs2" and "canceling x1 x2" proof- assume a: "(⋀xs1 x1 x2 xs2. ⟦x = xs1 @ x1 # x2 # xs2; y = xs1 @ xs2; canceling x1 x2⟧ ⟹ thesis)" from ‹cancels_to_1 x y› obtain i where "cancels_to_1_at i x y" unfolding cancels_to_1_def by auto hence "canceling (x ! i) (x ! Suc i)" and "y = (take i x) @ (drop (Suc (Suc i)) x)" and "x = (take i x) @ x ! i # x ! Suc i # (drop (Suc (Suc i)) x)" unfolding cancel_at_def and cancels_to_1_at_def by (auto simp add: Cons_nth_drop_Suc) with a show thesis by blast qed (* And the reverse direction *) lemma cancels_to_1_fold: "canceling x1 x2 ⟹ cancels_to_1 (xs1 @ x1 # x2 # xs2) (xs1 @ xs2)" unfolding cancels_to_1_def and cancels_to_1_at_def and cancel_at_def by (rule_tac x="length xs1" in exI, auto simp add:nth_append) subsubsection ‹Existence of the normal form› text ‹ One of two steps to show that we have a normal form is the following lemma, guaranteeing that by canceling, we always end up at a fully canceled word. › lemma canceling_terminates: "wfP (cancels_to_1^--1)" proof- have "wf (measure length)" by auto moreover have "{(x, y). cancels_to_1 y x} ⊆ measure length" by (auto simp add: cancels_to_1_def cancel_at_def cancels_to_1_at_def) ultimately have "wf {(x, y). cancels_to_1 y x}" by(rule wf_subset) thus ?thesis by (simp add:wfP_def) qed text ‹ The next two lemmas prepare for the proof of confluence. It does not matter in which order we cancel, we can obtain the same result. › lemma canceling_neighbor: assumes "cancels_to_1_at i l a" and "cancels_to_1_at (Suc i) l b" shows "a = b" proof- from ‹cancels_to_1_at i l a› have "canceling (l ! i) (l ! Suc i)" and "i < length l" by (auto simp add: cancels_to_1_at_def) from ‹cancels_to_1_at (Suc i) l b› have "canceling (l ! Suc i) (l ! Suc (Suc i))" and "Suc (Suc i) < length l" by (auto simp add: cancels_to_1_at_def) from ‹canceling (l ! i) (l ! Suc i)› and ‹canceling (l ! Suc i) (l ! Suc (Suc i))› have "l ! i = l ! Suc (Suc i)" by (rule cancel_cancel) from ‹cancels_to_1_at (Suc i) l b› have "b = take (Suc i) l @ drop (Suc (Suc (Suc i))) l" by (simp add: cancels_to_1_at_def cancel_at_def) also from ‹i < length l› have "… = take i l @ [l ! i] @ drop (Suc (Suc (Suc i))) l" by(auto simp add: take_Suc_conv_app_nth) also from ‹l ! i = l ! Suc (Suc i)› have "… = take i l @ [l ! Suc (Suc i)] @ drop (Suc (Suc (Suc i))) l" by simp also from ‹Suc (Suc i) < length l› have "… = take i l @ drop (Suc (Suc i)) l" by (simp add: Cons_nth_drop_Suc) also from ‹cancels_to_1_at i l a› have "… = a" by (simp add: cancels_to_1_at_def cancel_at_def) finally show "a = b" by(rule sym) qed lemma canceling_indep: assumes "cancels_to_1_at i l a" and "cancels_to_1_at j l b" and "j > Suc i" obtains c where "cancels_to_1_at (j - 2) a c" and "cancels_to_1_at i b c" proof(atomize_elim) from ‹cancels_to_1_at i l a› have "Suc i < length l" and "canceling (l ! i) (l ! Suc i)" and "a = cancel_at i l" and "length a = length l - 2" and "min (length l) i = i" by (auto simp add:cancels_to_1_at_def) from ‹cancels_to_1_at j l b› have "Suc j < length l" and "canceling (l ! j) (l ! Suc j)" and "b = cancel_at j l" and "length b = length l - 2" by (auto simp add:cancels_to_1_at_def) let ?c = "cancel_at (j - 2) a" from ‹j > Suc i› have "Suc (Suc (j - 2)) = j" and "Suc (Suc (Suc j - 2)) = Suc j" by auto with ‹min (length l) i = i› and ‹j > Suc i› and ‹Suc j < length l› have "(l ! j) = (cancel_at i l ! (j - 2))" and "(l ! (Suc j)) = (cancel_at i l ! Suc (j - 2))" by(auto simp add:cancel_at_def simp add:nth_append) with ‹cancels_to_1_at i l a› and ‹cancels_to_1_at j l b› have "canceling (a ! (j - 2)) (a ! Suc (j - 2))" by(auto simp add:cancels_to_1_at_def) with ‹j > Suc i› and ‹Suc j < length l› and ‹length a = length l - 2› have "cancels_to_1_at (j - 2) a ?c" by (auto simp add: cancels_to_1_at_def) from ‹length b = length l - 2› and ‹j > Suc i› and ‹Suc j < length l› have "Suc i < length b" by auto moreover from ‹b = cancel_at j l› and ‹j > Suc i› and ‹Suc i < length l› have "(b ! i) = (l ! i)" and "(b ! Suc i) = (l ! Suc i)" by (auto simp add:cancel_at_def nth_append) with ‹canceling (l ! i) (l ! Suc i)› have "canceling (b ! i) (b ! Suc i)" by simp moreover from ‹j > Suc i› and ‹Suc j < length l› have "min i j = i" and "min (j - 2) i = i" and "min (length l) j = j" and "min (length l) i = i" and "Suc (Suc (j - 2)) = j" by auto with ‹a = cancel_at i l› and ‹b = cancel_at j l› and ‹Suc (Suc (j - 2)) = j› have "cancel_at (j - 2) a = cancel_at i b" by (auto simp add:cancel_at_def take_drop) ultimately have "cancels_to_1_at i b (cancel_at (j - 2) a)" by (auto simp add:cancels_to_1_at_def) with ‹cancels_to_1_at (j - 2) a ?c› show "∃c. cancels_to_1_at (j - 2) a c ∧ cancels_to_1_at i b c" by blast qed text ‹This is the confluence lemma› lemma confluent_cancels_to_1: "confluent cancels_to_1" proof(rule lconfluent_confluent) show "wfP cancels_to_1¯¯" by (rule canceling_terminates) next fix a b c assume "cancels_to_1 a b" then obtain i where "cancels_to_1_at i a b" by(simp add: cancels_to_1_def)(erule exE) assume "cancels_to_1 a c" then obtain j where "cancels_to_1_at j a c" by(simp add: cancels_to_1_def)(erule exE) show "∃d. cancels_to_1⇧^{*}⇧^{*}b d ∧ cancels_to_1⇧^{*}⇧^{*}c d" proof (cases "i=j") assume "i=j" from ‹cancels_to_1_at i a b› have "b = cancel_at i a" by (simp add:cancels_to_1_at_def) moreover from ‹i=j› have "… = cancel_at j a" by (clarify) moreover from ‹cancels_to_1_at j a c› have "… = c" by (simp add:cancels_to_1_at_def) ultimately have "b = c" by (simp) hence "cancels_to_1⇧^{*}⇧^{*}b b" and "cancels_to_1⇧^{*}⇧^{*}c b" by auto thus "∃d. cancels_to_1⇧^{*}⇧^{*}b d ∧ cancels_to_1⇧^{*}⇧^{*}c d" by blast next assume "i ≠ j" show ?thesis proof (cases "j = Suc i") assume "j = Suc i" with ‹cancels_to_1_at i a b› and ‹cancels_to_1_at j a c› have "b = c" by (auto elim: canceling_neighbor) hence "cancels_to_1⇧^{*}⇧^{*}b b" and "cancels_to_1⇧^{*}⇧^{*}c b" by auto thus "∃d. cancels_to_1⇧^{*}⇧^{*}b d ∧ cancels_to_1⇧^{*}⇧^{*}c d" by blast next assume "j ≠ Suc i" show ?thesis proof (cases "i = Suc j") assume "i = Suc j" with ‹cancels_to_1_at i a b› and ‹cancels_to_1_at j a c› have "c = b" by (auto elim: canceling_neighbor) hence "cancels_to_1⇧^{*}⇧^{*}b b" and "cancels_to_1⇧^{*}⇧^{*}c b" by auto thus "∃d. cancels_to_1⇧^{*}⇧^{*}b d ∧ cancels_to_1⇧^{*}⇧^{*}c d" by blast next assume "i ≠ Suc j" show ?thesis proof (cases "i < j") assume "i < j" with ‹j ≠ Suc i› have "Suc i < j" by auto with ‹cancels_to_1_at i a b› and ‹cancels_to_1_at j a c› obtain d where "cancels_to_1_at (j - 2) b d" and "cancels_to_1_at i c d" by(erule canceling_indep) hence "cancels_to_1 b d" and "cancels_to_1 c d" by (auto simp add:cancels_to_1_def) thus "∃d. cancels_to_1⇧^{*}⇧^{*}b d ∧ cancels_to_1⇧^{*}⇧^{*}c d" by (auto) next assume "¬ i < j" with ‹j ≠ Suc i› and ‹i ≠ j› and ‹i ≠ Suc j› have "Suc j < i" by auto with ‹cancels_to_1_at i a b› and ‹cancels_to_1_at j a c› obtain d where "cancels_to_1_at (i - 2) c d" and "cancels_to_1_at j b d" by -(erule canceling_indep) hence "cancels_to_1 b d" and "cancels_to_1 c d" by (auto simp add:cancels_to_1_def) thus "∃d. cancels_to_1⇧^{*}⇧^{*}b d ∧ cancels_to_1⇧^{*}⇧^{*}c d" by (auto) qed qed qed qed qed text ‹ And finally, we show that there exists a unique normal form for each word. › (* lemma inv_rtrcl: "R^**^--1 = R^--1^**" (* Did I overlook this in the standard libs? *) by (auto simp add:fun_eq_iff intro: dest:rtranclp_converseD intro:rtranclp_converseI) *) lemma norm_form_uniq: assumes "cancels_to a b" and "cancels_to a c" and "canceled b" and "canceled c" shows "b = c" proof- have "confluent cancels_to_1" by (rule confluent_cancels_to_1) moreover from ‹cancels_to a b› have "cancels_to_1^** a b" by (simp add: cancels_to_def) moreover from ‹cancels_to a c› have "cancels_to_1^** a c" by (simp add: cancels_to_def) moreover from ‹canceled b› have "¬ Domainp cancels_to_1 b" by (simp add: canceled_def) moreover from ‹canceled c› have "¬ Domainp cancels_to_1 c" by (simp add: canceled_def) ultimately show "b = c" by (rule confluent_unique_normal_form) qed subsubsection ‹Some properties of cancelation› text ‹ Distributivity rules of cancelation and ‹append›. › lemma cancel_to_1_append: assumes "cancels_to_1 a b" shows "cancels_to_1 (l@a@l') (l@b@l')" proof- from ‹cancels_to_1 a b› obtain i where "cancels_to_1_at i a b" by(simp add: cancels_to_1_def)(erule exE) hence "cancels_to_1_at (length l + i) (l@a@l') (l@b@l')" by (auto simp add:cancels_to_1_at_def nth_append cancel_at_def) thus "cancels_to_1 (l@a@l') (l@b@l')" by (auto simp add: cancels_to_1_def) qed lemma cancel_to_append: assumes "cancels_to a b" shows "cancels_to (l@a@l') (l@b@l')" using assms unfolding cancels_to_def proof(induct) case base show ?case by (simp add:cancels_to_def) next case (step b c) from ‹cancels_to_1 b c› have "cancels_to_1 (l @ b @ l') (l @ c @ l')" by (rule cancel_to_1_append) with ‹cancels_to_1^** (l @ a @ l') (l @ b @ l')› show ?case by (auto simp add:cancels_to_def) qed lemma cancels_to_append2: assumes "cancels_to a a'" and "cancels_to b b'" shows "cancels_to (a@b) (a'@b')" using ‹cancels_to a a'› unfolding cancels_to_def proof(induct) case base from ‹cancels_to b b'› have "cancels_to (a@b@[]) (a@b'@[])" by (rule cancel_to_append) thus ?case unfolding cancels_to_def by simp next case (step ba c) from ‹cancels_to_1 ba c› have "cancels_to_1 ([]@ba@b') ([]@c@b')" by(rule cancel_to_1_append) with ‹cancels_to_1^** (a @ b) (ba @ b')› show ?case unfolding cancels_to_def by simp qed text ‹ The empty list is canceled, a one letter word is canceled and a word is trivially cancled from itself. › lemma empty_canceled[simp]: "canceled []" by(auto simp add: canceled_def cancels_to_1_def cancels_to_1_at_def) lemma singleton_canceled[simp]: "canceled [a]" by(auto simp add: canceled_def cancels_to_1_def cancels_to_1_at_def) lemma cons_canceled: assumes "canceled (a#x)" shows "canceled x" proof(rule ccontr) assume "¬ canceled x" hence "Domainp cancels_to_1 x" by (simp add:canceled_def) then obtain x' where "cancels_to_1 x x'" by auto then obtain xs1 x1 x2 xs2 where x: "x = xs1 @ x1 # x2 # xs2" and "canceling x1 x2" by (rule cancels_to_1_unfold) hence "cancels_to_1 ((a#xs1) @ x1 # x2 # xs2) ( (a#xs1) @ xs2)" by (auto intro:cancels_to_1_fold simp del:append_Cons) with x have "cancels_to_1 (a#x) (a#xs1 @ xs2)" by simp hence "¬ canceled (a#x)" by (auto simp add:canceled_def) thus False using ‹canceled (a#x)› by contradiction qed lemma cancels_to_self[simp]: "cancels_to l l" by (simp add:cancels_to_def) subsection ‹Definition of normalization› text ‹ Using the THE construct, we can define the normalization function ‹normalize› as the unique fully cancled word that the argument cancels to. › definition normalize :: "'a word_g_i ⇒ 'a word_g_i" where "normalize l = (THE l'. cancels_to l l' ∧ canceled l')" text ‹ Some obvious properties of the normalize function, and other useful lemmas. › lemma shows normalized_canceled[simp]: "canceled (normalize l)" and normalized_cancels_to[simp]: "cancels_to l (normalize l)" proof- let ?Q = "{l'. cancels_to_1^** l l'}" have "l ∈ ?Q" by (auto) hence "∃x. x ∈ ?Q" by (rule exI) have "wfP cancels_to_1^--1" by (rule canceling_terminates) hence "∀Q. (∃x. x ∈ Q) ⟶ (∃z∈Q. ∀y. cancels_to_1 z y ⟶ y ∉ Q)" by (simp add:wfP_eq_minimal) hence "(∃x. x ∈ ?Q) ⟶ (∃z∈?Q. ∀y. cancels_to_1 z y ⟶ y ∉ ?Q)" by (erule_tac x="?Q" in allE) then obtain l' where "l' ∈ ?Q" and minimal: "⋀y. cancels_to_1 l' y ⟹ y ∉ ?Q" by auto from ‹l' ∈ ?Q› have "cancels_to l l'" by (auto simp add: cancels_to_def) have "canceled l'" proof(rule ccontr) assume "¬ canceled l'" hence "Domainp cancels_to_1 l'" by (simp add: canceled_def) then obtain y where "cancels_to_1 l' y" by auto with ‹cancels_to l l'› have "cancels_to l y" by (auto simp add: cancels_to_def) from ‹cancels_to_1 l' y› have "y ∉ ?Q" by(rule minimal) hence "¬ cancels_to_1^** l y" by auto hence "¬ cancels_to l y" by (simp add: cancels_to_def) with ‹cancels_to l y› show False by contradiction qed from ‹cancels_to l l'› and ‹canceled l'› have "cancels_to l l' ∧ canceled l'" by simp hence "cancels_to l (normalize l) ∧ canceled (normalize l)" unfolding normalize_def proof (rule theI) fix l'a assume "cancels_to l l'a ∧ canceled l'a" thus "l'a = l'" using ‹cancels_to l l' ∧ canceled l'› by (auto elim:norm_form_uniq) qed thus "canceled (normalize l)" and "cancels_to l (normalize l)" by auto qed lemma normalize_discover: assumes "canceled l'" and "cancels_to l l'" shows "normalize l = l'" proof- from ‹canceled l'› and ‹cancels_to l l'› have "cancels_to l l' ∧ canceled l'" by auto thus ?thesis unfolding normalize_def by (auto elim:norm_form_uniq) qed text ‹Words, related by cancelation, have the same normal form.› lemma normalize_canceled[simp]: assumes "cancels_to l l'" shows "normalize l = normalize l'" proof(rule normalize_discover) show "canceled (normalize l')" by (rule normalized_canceled) next have "cancels_to l' (normalize l')" by (rule normalized_cancels_to) with ‹cancels_to l l'› show "cancels_to l (normalize l')" by (rule cancels_to_trans) qed text ‹Normalization is idempotent.› lemma normalize_idemp[simp]: assumes "canceled l" shows "normalize l = l" using assms by(rule normalize_discover)(rule cancels_to_self) text ‹ This lemma lifts the distributivity results from above to the normalize function. › lemma normalize_append_cancel_to: assumes "cancels_to l1 l1'" and "cancels_to l2 l2'" shows "normalize (l1 @ l2) = normalize (l1' @ l2')" proof(rule normalize_discover) show "canceled (normalize (l1' @ l2'))" by (rule normalized_canceled) next from ‹cancels_to l1 l1'› and ‹cancels_to l2 l2'› have "cancels_to (l1 @ l2) (l1' @ l2')" by (rule cancels_to_append2) also have "cancels_to (l1' @ l2') (normalize (l1' @ l2'))" by (rule normalized_cancels_to) finally show "cancels_to (l1 @ l2) (normalize (l1' @ l2'))". qed subsection ‹Normalization preserves generators› text ‹ Somewhat obvious, but still required to formalize Free Groups, is the fact that canceling a word of generators of a specific set (and their inverses) results in a word in generators from that set. › lemma cancels_to_1_preserves_generators: assumes "cancels_to_1 l l'" and "l ∈ lists (UNIV × gens)" shows "l' ∈ lists (UNIV × gens)" proof- from assms obtain i where "l' = cancel_at i l" unfolding cancels_to_1_def and cancels_to_1_at_def by auto hence "l' = take i l @ drop (2 + i) l" unfolding cancel_at_def . hence "set l' = set (take i l @ drop (2 + i) l)" by simp moreover have "… = set (take i l @ drop (2 + i) l)" by auto moreover have "… ⊆ set (take i l) ∪ set (drop (2 + i) l)" by auto moreover have "… ⊆ set l" by (auto dest: in_set_takeD in_set_dropD) ultimately have "set l' ⊆ set l" by simp thus ?thesis using assms(2) by auto qed lemma cancels_to_preserves_generators: assumes "cancels_to l l'" and "l ∈ lists (UNIV × gens)" shows "l' ∈ lists (UNIV × gens)" using assms unfolding cancels_to_def by (induct, auto dest:cancels_to_1_preserves_generators) lemma normalize_preserves_generators: assumes "l ∈ lists (UNIV × gens)" shows "normalize l ∈ lists (UNIV × gens)" proof- have "cancels_to l (normalize l)" by simp thus ?thesis using assms by(rule cancels_to_preserves_generators) qed text ‹ Two simplification lemmas about lists. › lemma empty_in_lists[simp]: "[] ∈ lists A" by auto lemma lists_empty[simp]: "lists {} = {[]}" by auto subsection ‹Normalization and renaming generators› text ‹ Renaming the generators, i.e. mapping them through an injective function, commutes with normalization. Similarly, replacing generators by their inverses and vica-versa commutes with normalization. Both operations are similar enough to be handled at once here. › lemma rename_gens_cancel_at: "cancel_at i (map f l) = map f (cancel_at i l)" unfolding "cancel_at_def" by (auto simp add:take_map drop_map) lemma rename_gens_cancels_to_1: assumes "inj f" and "cancels_to_1 l l'" shows "cancels_to_1 (map (map_prod f g) l) (map (map_prod f g) l')" proof- from ‹cancels_to_1 l l'› obtain ls1 l1 l2 ls2 where "l = ls1 @ l1 # l2 # ls2" and "l' = ls1 @ ls2" and "canceling l1 l2" by (rule cancels_to_1_unfold) from ‹canceling l1 l2› have "fst l1 ≠ fst l2" and "snd l1 = snd l2" unfolding canceling_def by auto from ‹fst l1 ≠ fst l2› and ‹inj f› have "f (fst l1) ≠ f (fst l2)" by(auto dest!:inj_on_contraD) hence "fst (map_prod f g l1) ≠ fst (map_prod f g l2)" by auto moreover from ‹snd l1 = snd l2› have "snd (map_prod f g l1) = snd (map_prod f g l2)" by auto ultimately have "canceling (map_prod f g (l1)) (map_prod f g (l2))" unfolding canceling_def by auto hence "cancels_to_1 (map (map_prod f g) ls1 @ map_prod f g l1 # map_prod f g l2 # map (map_prod f g) ls2) (map (map_prod f g) ls1 @ map (map_prod f g) ls2)" by(rule cancels_to_1_fold) with ‹l = ls1 @ l1 # l2 # ls2› and ‹l' = ls1 @ ls2› show "cancels_to_1 (map (map_prod f g) l) (map (map_prod f g) l')" by simp qed lemma rename_gens_cancels_to: assumes "inj f" and "cancels_to l l'" shows "cancels_to (map (map_prod f g) l) (map (map_prod f g) l')" using ‹cancels_to l l'› unfolding cancels_to_def proof(induct rule:rtranclp_induct) case (step x z) from ‹cancels_to_1 x z› and ‹inj f› have "cancels_to_1 (map (map_prod f g) x) (map (map_prod f g) z)" by -(rule rename_gens_cancels_to_1) with ‹cancels_to_1^** (map (map_prod f g) l) (map (map_prod f g) x)› show "cancels_to_1^** (map (map_prod f g) l) (map (map_prod f g) z)" by auto qed(auto) lemma rename_gens_canceled: assumes "inj_on g (snd`set l)" and "canceled l" shows "canceled (map (map_prod f g) l)" unfolding canceled_def proof (* This statement is needed explicitly later in this proof *) have different_images: "⋀ f a b. f a ≠ f b ⟹ a ≠ b" by auto assume "Domainp cancels_to_1 (map (map_prod f g) l)" then obtain l' where "cancels_to_1 (map (map_prod f g) l) l'" by auto then obtain i where "Suc i < length l" and "canceling (map (map_prod f g) l ! i) (map (map_prod f g) l ! Suc i)" by(auto simp add:cancels_to_1_def cancels_to_1_at_def) hence "f (fst (l ! i)) ≠ f (fst (l ! Suc i))" and "g (snd (l ! i)) = g (snd (l ! Suc i))" by(auto simp add:canceling_def) from ‹f (fst (l ! i)) ≠ f (fst (l ! Suc i))› have "fst (l ! i) ≠ fst (l ! Suc i)" by -(erule different_images) moreover from ‹Suc i < length l› have "snd (l ! i) ∈ snd ` set l" and "snd (l ! Suc i) ∈ snd ` set l" by auto with ‹g (snd (l ! i)) = g (snd (l ! Suc i))› have "snd (l ! i) = snd (l ! Suc i)" using ‹inj_on g (image snd (set l))› by (auto dest: inj_onD) ultimately have "canceling (l ! i) (l ! Suc i)" unfolding canceling_def by simp with ‹Suc i < length l› have "cancels_to_1_at i l (cancel_at i l)" unfolding cancels_to_1_at_def by auto hence "cancels_to_1 l (cancel_at i l)" unfolding cancels_to_1_def by auto hence "¬canceled l" unfolding canceled_def by auto with ‹canceled l› show False by contradiction qed lemma rename_gens_normalize: assumes "inj f" and "inj_on g (snd ` set l)" shows "normalize (map (map_prod f g) l) = map (map_prod f g) (normalize l)" proof(rule normalize_discover) from ‹inj_on g (image snd (set l))› have "inj_on g (image snd (set (normalize l)))" proof (rule subset_inj_on) have UNIV_snd: "⋀A. A ⊆ UNIV × snd ` A" proof fix A and x::"'c×'d" assume "x∈A" hence "(fst x,snd x)∈ (UNIV × snd ` A)" by -(rule, auto) thus "x∈ (UNIV × snd ` A)" by simp qed have "l ∈ lists (set l)" by auto hence "l ∈ lists (UNIV × snd ` set l)" by (rule subsetD[OF lists_mono[OF UNIV_snd], of l "set l"]) hence "normalize l ∈ lists (UNIV × snd ` set l)" by (rule normalize_preserves_generators[of _ "snd ` set l"]) thus "snd ` set (normalize l) ⊆ snd ` set l" by (auto simp add: lists_eq_set) qed thus "canceled (map (map_prod f g) (normalize l))" by(rule rename_gens_canceled,simp) next from ‹inj f› show "cancels_to (map (map_prod f g) l) (map (map_prod f g) (normalize l))" by (rule rename_gens_cancels_to, simp) qed end