Theory Cancelation

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 = (0i  (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)  (zQ. 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 "xA"
        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