[STATEMENT]
theorem closed_inv: "f \<in> Ex1 \<Longrightarrow> inv f \<in> Ex1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> CofGroups.Ex1 \<Longrightarrow> inv f \<in> CofGroups.Ex1
[PROOF STEP]
proof (rule Ex1.induct [of "f"], blast)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. f \<in> CofGroups.Ex1 \<Longrightarrow> inv upOne \<in> CofGroups.Ex1
 2. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; inv fa \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv (upOne \<circ> fa) \<in> CofGroups.Ex1
 3. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; inv fa \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv (inv upOne \<circ> fa) \<in> CofGroups.Ex1
[PROOF STEP]
assume "f \<in> Ex1"
[PROOF STATE]
proof (state)
this:
f \<in> CofGroups.Ex1

goal (3 subgoals):
 1. f \<in> CofGroups.Ex1 \<Longrightarrow> inv upOne \<in> CofGroups.Ex1
 2. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; inv fa \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv (upOne \<circ> fa) \<in> CofGroups.Ex1
 3. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; inv fa \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv (inv upOne \<circ> fa) \<in> CofGroups.Ex1
[PROOF STEP]
show "inv upOne \<in> Ex1" (is "?right \<in> Ex1")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv upOne \<in> CofGroups.Ex1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv upOne \<in> CofGroups.Ex1
[PROOF STEP]
let ?left  = "inv upOne \<circ> (inv upOne \<circ> upOne)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv upOne \<in> CofGroups.Ex1
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv upOne \<in> CofGroups.Ex1
[PROOF STEP]
from Ex1.comp_inv and Ex1.base_func
[PROOF STATE]
proof (chain)
picking this:
?f \<in> CofGroups.Ex1 \<Longrightarrow> inv upOne \<circ> ?f \<in> CofGroups.Ex1
upOne \<in> CofGroups.Ex1
[PROOF STEP]
have "?left \<in> Ex1"
[PROOF STATE]
proof (prove)
using this:
?f \<in> CofGroups.Ex1 \<Longrightarrow> inv upOne \<circ> ?f \<in> CofGroups.Ex1
upOne \<in> CofGroups.Ex1

goal (1 subgoal):
 1. inv upOne \<circ> (inv upOne \<circ> upOne) \<in> CofGroups.Ex1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv upOne \<circ> (inv upOne \<circ> upOne) \<in> CofGroups.Ex1

goal (1 subgoal):
 1. inv upOne \<in> CofGroups.Ex1
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
inv upOne \<circ> (inv upOne \<circ> upOne) \<in> CofGroups.Ex1

goal (1 subgoal):
 1. inv upOne \<in> CofGroups.Ex1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inv upOne \<circ> (inv upOne \<circ> upOne) \<in> CofGroups.Ex1

goal (1 subgoal):
 1. inv upOne \<in> CofGroups.Ex1
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
inv upOne \<circ> (inv upOne \<circ> upOne) \<in> CofGroups.Ex1

goal (1 subgoal):
 1. inv upOne \<in> CofGroups.Ex1
[PROOF STEP]
from bij_upOne and bij_is_inj
[PROOF STATE]
proof (chain)
picking this:
bij upOne
bij ?f \<Longrightarrow> inj ?f
[PROOF STEP]
have "inj upOne"
[PROOF STATE]
proof (prove)
using this:
bij upOne
bij ?f \<Longrightarrow> inj ?f

goal (1 subgoal):
 1. inj upOne
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inj upOne

goal (1 subgoal):
 1. inv upOne \<in> CofGroups.Ex1
[PROOF STEP]
hence "inv upOne \<circ> upOne = id"
[PROOF STATE]
proof (prove)
using this:
inj upOne

goal (1 subgoal):
 1. inv upOne \<circ> upOne = id
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv upOne \<circ> upOne = id

goal (1 subgoal):
 1. inv upOne \<in> CofGroups.Ex1
[PROOF STEP]
hence "?left = ?right"
[PROOF STATE]
proof (prove)
using this:
inv upOne \<circ> upOne = id

goal (1 subgoal):
 1. inv upOne \<circ> (inv upOne \<circ> upOne) = inv upOne
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv upOne \<circ> (inv upOne \<circ> upOne) = inv upOne

goal (1 subgoal):
 1. inv upOne \<in> CofGroups.Ex1
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
inv upOne \<circ> (inv upOne \<circ> upOne) = inv upOne

goal (1 subgoal):
 1. inv upOne \<in> CofGroups.Ex1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
inv upOne \<circ> (inv upOne \<circ> upOne) \<in> CofGroups.Ex1
inv upOne \<circ> (inv upOne \<circ> upOne) = inv upOne
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inv upOne \<circ> (inv upOne \<circ> upOne) \<in> CofGroups.Ex1
inv upOne \<circ> (inv upOne \<circ> upOne) = inv upOne

goal (1 subgoal):
 1. inv upOne \<in> CofGroups.Ex1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv upOne \<in> CofGroups.Ex1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inv upOne \<in> CofGroups.Ex1

goal (2 subgoals):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; inv fa \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv (upOne \<circ> fa) \<in> CofGroups.Ex1
 2. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; inv fa \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv (inv upOne \<circ> fa) \<in> CofGroups.Ex1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; inv fa \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv (upOne \<circ> fa) \<in> CofGroups.Ex1
 2. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; inv fa \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv (inv upOne \<circ> fa) \<in> CofGroups.Ex1
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; inv fa \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv (upOne \<circ> fa) \<in> CofGroups.Ex1
 2. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; inv fa \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv (inv upOne \<circ> fa) \<in> CofGroups.Ex1
[PROOF STEP]
assume f_Ex1: "f \<in> Ex1"
[PROOF STATE]
proof (state)
this:
f \<in> CofGroups.Ex1

goal (2 subgoals):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; inv fa \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv (upOne \<circ> fa) \<in> CofGroups.Ex1
 2. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; inv fa \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv (inv upOne \<circ> fa) \<in> CofGroups.Ex1
[PROOF STEP]
from f_Ex1 and Ex1_Normal_form
[PROOF STATE]
proof (chain)
picking this:
f \<in> CofGroups.Ex1
(?f \<in> CofGroups.Ex1) = (\<exists>k. \<forall>n. ?f n = n + k)
[PROOF STEP]
obtain k where f_eq: "\<forall>n. f n = n + k"
[PROOF STATE]
proof (prove)
using this:
f \<in> CofGroups.Ex1
(?f \<in> CofGroups.Ex1) = (\<exists>k. \<forall>n. ?f n = n + k)

goal (1 subgoal):
 1. (\<And>k. \<forall>n. f n = n + k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. f n = n + k

goal (2 subgoals):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; inv fa \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv (upOne \<circ> fa) \<in> CofGroups.Ex1
 2. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; inv fa \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv (inv upOne \<circ> fa) \<in> CofGroups.Ex1
[PROOF STEP]
show "inv (upOne \<circ> f) \<in> Ex1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv (upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv (upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
let ?ic = "inv (upOne \<circ> f)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv (upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
let ?ci = "inv f \<circ> inv upOne"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv (upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
{
      \<comment> \<open>first we get an expression for @{term ?ci}\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv (upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv (upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
from all_bij and f_Ex1
[PROOF STATE]
proof (chain)
picking this:
?f \<in> CofGroups.Ex1 \<Longrightarrow> bij ?f
f \<in> CofGroups.Ex1
[PROOF STEP]
have "bij f"
[PROOF STATE]
proof (prove)
using this:
?f \<in> CofGroups.Ex1 \<Longrightarrow> bij ?f
f \<in> CofGroups.Ex1

goal (1 subgoal):
 1. bij f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bij f

goal (1 subgoal):
 1. inv (upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
with bij_is_inj
[PROOF STATE]
proof (chain)
picking this:
bij ?f \<Longrightarrow> inj ?f
bij f
[PROOF STEP]
have inj_f: "inj f"
[PROOF STATE]
proof (prove)
using this:
bij ?f \<Longrightarrow> inj ?f
bij f

goal (1 subgoal):
 1. inj f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inj f

goal (1 subgoal):
 1. inv (upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
have "\<forall>n. inv f n = n - k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. inv f n = n - k
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. inv f n = n - k
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. inv f n = n - k
[PROOF STEP]
from f_eq
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. f n = n + k
[PROOF STEP]
have "f (n - k) = n"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. f n = n + k

goal (1 subgoal):
 1. f (n - k) = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (n - k) = n

goal (1 subgoal):
 1. \<And>n. inv f n = n - k
[PROOF STEP]
with inv_f_eq[of f "n-k" "n"] and inj_f
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>inj f; f (n - k) = n\<rbrakk> \<Longrightarrow> inv f n = n - k
inj f
f (n - k) = n
[PROOF STEP]
show "inv f n = n-k"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>inj f; f (n - k) = n\<rbrakk> \<Longrightarrow> inv f n = n - k
inj f
f (n - k) = n

goal (1 subgoal):
 1. inv f n = n - k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv f n = n - k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n. inv f n = n - k

goal (1 subgoal):
 1. inv (upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
with inv_upOne_eq
[PROOF STATE]
proof (chain)
picking this:
inv upOne ?n = ?n - 1
\<forall>n. inv f n = n - k
[PROOF STEP]
have "\<forall>n. ?ci n = n - k - 1"
[PROOF STATE]
proof (prove)
using this:
inv upOne ?n = ?n - 1
\<forall>n. inv f n = n - k

goal (1 subgoal):
 1. \<forall>n. (inv f \<circ> inv upOne) n = n - k - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. (inv f \<circ> inv upOne) n = n - k - 1

goal (1 subgoal):
 1. inv (upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
hence "\<forall>n. ?ci n = n + (-1 - k)"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. (inv f \<circ> inv upOne) n = n - k - 1

goal (1 subgoal):
 1. \<forall>n. (inv f \<circ> inv upOne) n = n + (- 1 - k)
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
\<forall>n. (inv f \<circ> inv upOne) n = n + (- 1 - k)

goal (1 subgoal):
 1. inv (upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<forall>n. (inv f \<circ> inv upOne) n = n + (- 1 - k)

goal (1 subgoal):
 1. inv (upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
moreover
      \<comment> \<open>then we check that this implies @{term ?ci} is\<close>
      \<comment> \<open>a member of @{term Ex1}\<close>
[PROOF STATE]
proof (state)
this:
\<forall>n. (inv f \<circ> inv upOne) n = n + (- 1 - k)

goal (1 subgoal):
 1. inv (upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>n. (inv f \<circ> inv upOne) n = n + (- 1 - k)

goal (1 subgoal):
 1. inv (upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
from Ex1_Normal_form_part2[of "-1 - k"]
[PROOF STATE]
proof (chain)
picking this:
\<forall>f. (\<forall>n. f n = n + (- 1 - k)) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
have "(\<forall>f. ((\<forall>n. f n = n + (-1 - k)) \<longrightarrow> f \<in> Ex1))"
[PROOF STATE]
proof (prove)
using this:
\<forall>f. (\<forall>n. f n = n + (- 1 - k)) \<longrightarrow> f \<in> CofGroups.Ex1

goal (1 subgoal):
 1. \<forall>f. (\<forall>n. f n = n + (- 1 - k)) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>f. (\<forall>n. f n = n + (- 1 - k)) \<longrightarrow> f \<in> CofGroups.Ex1

goal (1 subgoal):
 1. inv (upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<forall>f. (\<forall>n. f n = n + (- 1 - k)) \<longrightarrow> f \<in> CofGroups.Ex1

goal (1 subgoal):
 1. inv (upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. (inv f \<circ> inv upOne) n = n + (- 1 - k)
\<forall>f. (\<forall>n. f n = n + (- 1 - k)) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
have "?ci \<in> Ex1"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. (inv f \<circ> inv upOne) n = n + (- 1 - k)
\<forall>f. (\<forall>n. f n = n + (- 1 - k)) \<longrightarrow> f \<in> CofGroups.Ex1

goal (1 subgoal):
 1. inv f \<circ> inv upOne \<in> CofGroups.Ex1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv f \<circ> inv upOne \<in> CofGroups.Ex1

goal (1 subgoal):
 1. inv (upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
inv f \<circ> inv upOne \<in> CofGroups.Ex1

goal (1 subgoal):
 1. inv (upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inv f \<circ> inv upOne \<in> CofGroups.Ex1

goal (1 subgoal):
 1. inv (upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
inv f \<circ> inv upOne \<in> CofGroups.Ex1

goal (1 subgoal):
 1. inv (upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
from f_Ex1 all_bij
[PROOF STATE]
proof (chain)
picking this:
f \<in> CofGroups.Ex1
?f \<in> CofGroups.Ex1 \<Longrightarrow> bij ?f
[PROOF STEP]
have "bij f"
[PROOF STATE]
proof (prove)
using this:
f \<in> CofGroups.Ex1
?f \<in> CofGroups.Ex1 \<Longrightarrow> bij ?f

goal (1 subgoal):
 1. bij f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bij f

goal (1 subgoal):
 1. inv (upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
with bij_upOne and o_inv_distrib[THEN sym]
[PROOF STATE]
proof (chain)
picking this:
bij upOne
\<lbrakk>bij ?f1; bij ?g1\<rbrakk> \<Longrightarrow> inv ?g1 \<circ> inv ?f1 = inv (?f1 \<circ> ?g1)
bij f
[PROOF STEP]
have "?ci = ?ic"
[PROOF STATE]
proof (prove)
using this:
bij upOne
\<lbrakk>bij ?f1; bij ?g1\<rbrakk> \<Longrightarrow> inv ?g1 \<circ> inv ?f1 = inv (?f1 \<circ> ?g1)
bij f

goal (1 subgoal):
 1. inv f \<circ> inv upOne = inv (upOne \<circ> f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv f \<circ> inv upOne = inv (upOne \<circ> f)

goal (1 subgoal):
 1. inv (upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
inv f \<circ> inv upOne = inv (upOne \<circ> f)

goal (1 subgoal):
 1. inv (upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
inv f \<circ> inv upOne \<in> CofGroups.Ex1
inv f \<circ> inv upOne = inv (upOne \<circ> f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inv f \<circ> inv upOne \<in> CofGroups.Ex1
inv f \<circ> inv upOne = inv (upOne \<circ> f)

goal (1 subgoal):
 1. inv (upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv (upOne \<circ> f) \<in> CofGroups.Ex1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inv (upOne \<circ> f) \<in> CofGroups.Ex1

goal (1 subgoal):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; inv fa \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv (inv upOne \<circ> fa) \<in> CofGroups.Ex1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; inv fa \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv (inv upOne \<circ> fa) \<in> CofGroups.Ex1
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; inv fa \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv (inv upOne \<circ> fa) \<in> CofGroups.Ex1
[PROOF STEP]
assume f_Ex1: "f \<in> Ex1"
[PROOF STATE]
proof (state)
this:
f \<in> CofGroups.Ex1

goal (1 subgoal):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; inv fa \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv (inv upOne \<circ> fa) \<in> CofGroups.Ex1
[PROOF STEP]
with Ex1_Normal_form
[PROOF STATE]
proof (chain)
picking this:
(?f \<in> CofGroups.Ex1) = (\<exists>k. \<forall>n. ?f n = n + k)
f \<in> CofGroups.Ex1
[PROOF STEP]
obtain k where f_eq: "\<forall>n. f n = n + k"
[PROOF STATE]
proof (prove)
using this:
(?f \<in> CofGroups.Ex1) = (\<exists>k. \<forall>n. ?f n = n + k)
f \<in> CofGroups.Ex1

goal (1 subgoal):
 1. (\<And>k. \<forall>n. f n = n + k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. f n = n + k

goal (1 subgoal):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; inv fa \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv (inv upOne \<circ> fa) \<in> CofGroups.Ex1
[PROOF STEP]
show "inv (inv upOne \<circ> f) \<in> Ex1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
let ?ic = "inv (inv upOne \<circ> f)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
let ?c = "inv f \<circ> upOne"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
from all_bij and f_Ex1
[PROOF STATE]
proof (chain)
picking this:
?f \<in> CofGroups.Ex1 \<Longrightarrow> bij ?f
f \<in> CofGroups.Ex1
[PROOF STEP]
have "bij f"
[PROOF STATE]
proof (prove)
using this:
?f \<in> CofGroups.Ex1 \<Longrightarrow> bij ?f
f \<in> CofGroups.Ex1

goal (1 subgoal):
 1. bij f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bij f

goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
with bij_is_inj
[PROOF STATE]
proof (chain)
picking this:
bij ?f \<Longrightarrow> inj ?f
bij f
[PROOF STEP]
have inj_f: "inj f"
[PROOF STATE]
proof (prove)
using this:
bij ?f \<Longrightarrow> inj ?f
bij f

goal (1 subgoal):
 1. inj f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inj f

goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
have "\<forall>n. inv f n = n - k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. inv f n = n - k
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. inv f n = n - k
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. inv f n = n - k
[PROOF STEP]
from f_eq
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. f n = n + k
[PROOF STEP]
have "f (n - k) = n"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. f n = n + k

goal (1 subgoal):
 1. f (n - k) = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (n - k) = n

goal (1 subgoal):
 1. \<And>n. inv f n = n - k
[PROOF STEP]
with inv_f_eq[of f "n-k" "n"] and inj_f
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>inj f; f (n - k) = n\<rbrakk> \<Longrightarrow> inv f n = n - k
inj f
f (n - k) = n
[PROOF STEP]
show "inv f n = n-k"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>inj f; f (n - k) = n\<rbrakk> \<Longrightarrow> inv f n = n - k
inj f
f (n - k) = n

goal (1 subgoal):
 1. inv f n = n - k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv f n = n - k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n. inv f n = n - k

goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
with upOne_def
[PROOF STATE]
proof (chain)
picking this:
upOne ?n = ?n + 1
\<forall>n. inv f n = n - k
[PROOF STEP]
have "\<forall>n. (inv f \<circ> upOne) n = n - k + 1"
[PROOF STATE]
proof (prove)
using this:
upOne ?n = ?n + 1
\<forall>n. inv f n = n - k

goal (1 subgoal):
 1. \<forall>n. (inv f \<circ> upOne) n = n - k + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. (inv f \<circ> upOne) n = n - k + 1

goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
hence "\<forall>n. (inv f \<circ> upOne) n = n + (1 - k)"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. (inv f \<circ> upOne) n = n - k + 1

goal (1 subgoal):
 1. \<forall>n. (inv f \<circ> upOne) n = n + (1 - k)
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
\<forall>n. (inv f \<circ> upOne) n = n + (1 - k)

goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n. (inv f \<circ> upOne) n = n + (1 - k)

goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
from Ex1_Normal_form_part2[of "1 - k"]
[PROOF STATE]
proof (chain)
picking this:
\<forall>f. (\<forall>n. f n = n + (1 - k)) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
have "(\<forall>f. ((\<forall>n. f n = n + (1 - k)) \<longrightarrow> f \<in> Ex1))"
[PROOF STATE]
proof (prove)
using this:
\<forall>f. (\<forall>n. f n = n + (1 - k)) \<longrightarrow> f \<in> CofGroups.Ex1

goal (1 subgoal):
 1. \<forall>f. (\<forall>n. f n = n + (1 - k)) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>f. (\<forall>n. f n = n + (1 - k)) \<longrightarrow> f \<in> CofGroups.Ex1

goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. (inv f \<circ> upOne) n = n + (1 - k)
\<forall>f. (\<forall>n. f n = n + (1 - k)) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
have "?c \<in> Ex1"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. (inv f \<circ> upOne) n = n + (1 - k)
\<forall>f. (\<forall>n. f n = n + (1 - k)) \<longrightarrow> f \<in> CofGroups.Ex1

goal (1 subgoal):
 1. inv f \<circ> upOne \<in> CofGroups.Ex1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv f \<circ> upOne \<in> CofGroups.Ex1

goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
inv f \<circ> upOne \<in> CofGroups.Ex1

goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inv f \<circ> upOne \<in> CofGroups.Ex1

goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
inv f \<circ> upOne \<in> CofGroups.Ex1

goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
from f_Ex1 all_bij and bij_is_inj
[PROOF STATE]
proof (chain)
picking this:
f \<in> CofGroups.Ex1
?f \<in> CofGroups.Ex1 \<Longrightarrow> bij ?f
bij ?f \<Longrightarrow> inj ?f
[PROOF STEP]
have "bij f"
[PROOF STATE]
proof (prove)
using this:
f \<in> CofGroups.Ex1
?f \<in> CofGroups.Ex1 \<Longrightarrow> bij ?f
bij ?f \<Longrightarrow> inj ?f

goal (1 subgoal):
 1. bij f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bij f

goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bij f

goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
from bij_upOne and bij_imp_bij_inv
[PROOF STATE]
proof (chain)
picking this:
bij upOne
bij ?f \<Longrightarrow> bij (inv ?f)
[PROOF STEP]
have "bij (inv upOne)"
[PROOF STATE]
proof (prove)
using this:
bij upOne
bij ?f \<Longrightarrow> bij (inv ?f)

goal (1 subgoal):
 1. bij (inv upOne)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bij (inv upOne)

goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bij (inv upOne)

goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
note o_inv_distrib[THEN sym]
[PROOF STATE]
proof (state)
this:
\<lbrakk>bij ?f1; bij ?g1\<rbrakk> \<Longrightarrow> inv ?g1 \<circ> inv ?f1 = inv (?f1 \<circ> ?g1)

goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bij f
bij (inv upOne)
\<lbrakk>bij ?f1; bij ?g1\<rbrakk> \<Longrightarrow> inv ?g1 \<circ> inv ?f1 = inv (?f1 \<circ> ?g1)
[PROOF STEP]
have "inv f \<circ> inv (inv upOne) = inv (inv upOne \<circ> f)"
[PROOF STATE]
proof (prove)
using this:
bij f
bij (inv upOne)
\<lbrakk>bij ?f1; bij ?g1\<rbrakk> \<Longrightarrow> inv ?g1 \<circ> inv ?f1 = inv (?f1 \<circ> ?g1)

goal (1 subgoal):
 1. inv f \<circ> inv (inv upOne) = inv (inv upOne \<circ> f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv f \<circ> inv (inv upOne) = inv (inv upOne \<circ> f)

goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inv f \<circ> inv (inv upOne) = inv (inv upOne \<circ> f)

goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
from bij_upOne and inv_inv_eq
[PROOF STATE]
proof (chain)
picking this:
bij upOne
bij ?f \<Longrightarrow> inv (inv ?f) = ?f
[PROOF STEP]
have "inv (inv upOne) = upOne"
[PROOF STATE]
proof (prove)
using this:
bij upOne
bij ?f \<Longrightarrow> inv (inv ?f) = ?f

goal (1 subgoal):
 1. inv (inv upOne) = upOne
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv (inv upOne) = upOne

goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
inv f \<circ> inv (inv upOne) = inv (inv upOne \<circ> f)
inv (inv upOne) = upOne
[PROOF STEP]
have "?c = ?ic"
[PROOF STATE]
proof (prove)
using this:
inv f \<circ> inv (inv upOne) = inv (inv upOne \<circ> f)
inv (inv upOne) = upOne

goal (1 subgoal):
 1. inv f \<circ> upOne = inv (inv upOne \<circ> f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv f \<circ> upOne = inv (inv upOne \<circ> f)

goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
inv f \<circ> upOne = inv (inv upOne \<circ> f)

goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
inv f \<circ> upOne \<in> CofGroups.Ex1
inv f \<circ> upOne = inv (inv upOne \<circ> f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inv f \<circ> upOne \<in> CofGroups.Ex1
inv f \<circ> upOne = inv (inv upOne \<circ> f)

goal (1 subgoal):
 1. inv (inv upOne \<circ> f) \<in> CofGroups.Ex1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv (inv upOne \<circ> f) \<in> CofGroups.Ex1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inv (inv upOne \<circ> f) \<in> CofGroups.Ex1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_f_o_inf_f: "bij f \<Longrightarrow> f \<circ> inv f = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij f \<Longrightarrow> f \<circ> inv f = id
[PROOF STEP]
unfolding bij_def surj_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj f \<and> f \<circ> inv f = id \<Longrightarrow> f \<circ> inv f = id
[PROOF STEP]
by simp


[STATEMENT]
theorem conj_fix_pt: "\<And>f::('a \<Rightarrow> 'b). \<And>g::('b \<Rightarrow> 'b). (bij f)
  \<Longrightarrow> ((inv f)`(Fix g)) = Fix ((inv f) \<circ> g \<circ> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f g. bij f \<Longrightarrow> inv f ` Fix g = Fix (inv f \<circ> g \<circ> f)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f g. bij f \<Longrightarrow> inv f ` Fix g = Fix (inv f \<circ> g \<circ> f)
[PROOF STEP]
fix f::"'a \<Rightarrow> 'b"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f g. bij f \<Longrightarrow> inv f ` Fix g = Fix (inv f \<circ> g \<circ> f)
[PROOF STEP]
assume bij_f: "bij f"
[PROOF STATE]
proof (state)
this:
bij f

goal (1 subgoal):
 1. \<And>f g. bij f \<Longrightarrow> inv f ` Fix g = Fix (inv f \<circ> g \<circ> f)
[PROOF STEP]
with bij_def
[PROOF STATE]
proof (chain)
picking this:
bij ?f = (inj ?f \<and> surj ?f)
bij f
[PROOF STEP]
have inj_f: "inj f"
[PROOF STATE]
proof (prove)
using this:
bij ?f = (inj ?f \<and> surj ?f)
bij f

goal (1 subgoal):
 1. inj f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inj f

goal (1 subgoal):
 1. \<And>f g. bij f \<Longrightarrow> inv f ` Fix g = Fix (inv f \<circ> g \<circ> f)
[PROOF STEP]
fix g::"'b\<Rightarrow>'b"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f g. bij f \<Longrightarrow> inv f ` Fix g = Fix (inv f \<circ> g \<circ> f)
[PROOF STEP]
show "((inv f)`(Fix g)) = Fix ((inv f) \<circ> g \<circ> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv f ` Fix g = Fix (inv f \<circ> g \<circ> f)
[PROOF STEP]
thm set_eq_subset[of "(inv f)`(Fix g)" "Fix((inv f) \<circ> g \<circ> f)"]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv f ` Fix g = Fix (inv f \<circ> g \<circ> f)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inv f ` Fix g \<subseteq> Fix (inv f \<circ> g \<circ> f)
 2. Fix (inv f \<circ> g \<circ> f) \<subseteq> inv f ` Fix g
[PROOF STEP]
show "(inv f)`(Fix g) \<subseteq> Fix ((inv f) \<circ> g \<circ> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv f ` Fix g \<subseteq> Fix (inv f \<circ> g \<circ> f)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> inv f ` Fix g \<Longrightarrow> x \<in> Fix (inv f \<circ> g \<circ> f)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> inv f ` Fix g \<Longrightarrow> x \<in> Fix (inv f \<circ> g \<circ> f)
[PROOF STEP]
assume "x \<in> (inv f)`(Fix g)"
[PROOF STATE]
proof (state)
this:
x \<in> inv f ` Fix g

goal (1 subgoal):
 1. \<And>x. x \<in> inv f ` Fix g \<Longrightarrow> x \<in> Fix (inv f \<circ> g \<circ> f)
[PROOF STEP]
with image_def
[PROOF STATE]
proof (chain)
picking this:
?f ` ?A = {y. \<exists>x\<in>?A. y = ?f x}
x \<in> inv f ` Fix g
[PROOF STEP]
have "\<exists>y \<in> Fix g. x = (inv f) y"
[PROOF STATE]
proof (prove)
using this:
?f ` ?A = {y. \<exists>x\<in>?A. y = ?f x}
x \<in> inv f ` Fix g

goal (1 subgoal):
 1. \<exists>y\<in>Fix g. x = inv f y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>Fix g. x = inv f y

goal (1 subgoal):
 1. \<And>x. x \<in> inv f ` Fix g \<Longrightarrow> x \<in> Fix (inv f \<circ> g \<circ> f)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>y\<in>Fix g. x = inv f y
[PROOF STEP]
obtain y where y_prop: "y \<in> Fix g \<and> x = (inv f) y"
[PROOF STATE]
proof (prove)
using this:
\<exists>y\<in>Fix g. x = inv f y

goal (1 subgoal):
 1. (\<And>y. y \<in> Fix g \<and> x = inv f y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> Fix g \<and> x = inv f y

goal (1 subgoal):
 1. \<And>x. x \<in> inv f ` Fix g \<Longrightarrow> x \<in> Fix (inv f \<circ> g \<circ> f)
[PROOF STEP]
hence "x = (inv f) y"
[PROOF STATE]
proof (prove)
using this:
y \<in> Fix g \<and> x = inv f y

goal (1 subgoal):
 1. x = inv f y
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
x = inv f y

goal (1 subgoal):
 1. \<And>x. x \<in> inv f ` Fix g \<Longrightarrow> x \<in> Fix (inv f \<circ> g \<circ> f)
[PROOF STEP]
hence "f x = (f \<circ> inv f) y"
[PROOF STATE]
proof (prove)
using this:
x = inv f y

goal (1 subgoal):
 1. f x = (f \<circ> inv f) y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f x = (f \<circ> inv f) y

goal (1 subgoal):
 1. \<And>x. x \<in> inv f ` Fix g \<Longrightarrow> x \<in> Fix (inv f \<circ> g \<circ> f)
[PROOF STEP]
with bij_f and bij_f_o_inf_f[of f]
[PROOF STATE]
proof (chain)
picking this:
bij f
bij f \<Longrightarrow> f \<circ> inv f = id
f x = (f \<circ> inv f) y
[PROOF STEP]
have f_x_y: "f x = y"
[PROOF STATE]
proof (prove)
using this:
bij f
bij f \<Longrightarrow> f \<circ> inv f = id
f x = (f \<circ> inv f) y

goal (1 subgoal):
 1. f x = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f x = y

goal (1 subgoal):
 1. \<And>x. x \<in> inv f ` Fix g \<Longrightarrow> x \<in> Fix (inv f \<circ> g \<circ> f)
[PROOF STEP]
from y_prop
[PROOF STATE]
proof (chain)
picking this:
y \<in> Fix g \<and> x = inv f y
[PROOF STEP]
have "y \<in> Fix g"
[PROOF STATE]
proof (prove)
using this:
y \<in> Fix g \<and> x = inv f y

goal (1 subgoal):
 1. y \<in> Fix g
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
y \<in> Fix g

goal (1 subgoal):
 1. \<And>x. x \<in> inv f ` Fix g \<Longrightarrow> x \<in> Fix (inv f \<circ> g \<circ> f)
[PROOF STEP]
with Fix_def[of g]
[PROOF STATE]
proof (chain)
picking this:
Fix g = {n. g n = n}
y \<in> Fix g
[PROOF STEP]
have "g y = y"
[PROOF STATE]
proof (prove)
using this:
Fix g = {n. g n = n}
y \<in> Fix g

goal (1 subgoal):
 1. g y = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g y = y

goal (1 subgoal):
 1. \<And>x. x \<in> inv f ` Fix g \<Longrightarrow> x \<in> Fix (inv f \<circ> g \<circ> f)
[PROOF STEP]
with f_x_y
[PROOF STATE]
proof (chain)
picking this:
f x = y
g y = y
[PROOF STEP]
have "g (f x) = f x"
[PROOF STATE]
proof (prove)
using this:
f x = y
g y = y

goal (1 subgoal):
 1. g (f x) = f x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g (f x) = f x

goal (1 subgoal):
 1. \<And>x. x \<in> inv f ` Fix g \<Longrightarrow> x \<in> Fix (inv f \<circ> g \<circ> f)
[PROOF STEP]
hence "(inv f) (g (f x)) = inv f (f x)"
[PROOF STATE]
proof (prove)
using this:
g (f x) = f x

goal (1 subgoal):
 1. inv f (g (f x)) = inv f (f x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv f (g (f x)) = inv f (f x)

goal (1 subgoal):
 1. \<And>x. x \<in> inv f ` Fix g \<Longrightarrow> x \<in> Fix (inv f \<circ> g \<circ> f)
[PROOF STEP]
with inv_f_f and inj_f
[PROOF STATE]
proof (chain)
picking this:
inj ?f \<Longrightarrow> inv ?f (?f ?x) = ?x
inj f
inv f (g (f x)) = inv f (f x)
[PROOF STEP]
have "(inv f) (g (f x)) = x"
[PROOF STATE]
proof (prove)
using this:
inj ?f \<Longrightarrow> inv ?f (?f ?x) = ?x
inj f
inv f (g (f x)) = inv f (f x)

goal (1 subgoal):
 1. inv f (g (f x)) = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv f (g (f x)) = x

goal (1 subgoal):
 1. \<And>x. x \<in> inv f ` Fix g \<Longrightarrow> x \<in> Fix (inv f \<circ> g \<circ> f)
[PROOF STEP]
hence "((inv f) \<circ> g \<circ> f) x = x"
[PROOF STATE]
proof (prove)
using this:
inv f (g (f x)) = x

goal (1 subgoal):
 1. (inv f \<circ> g \<circ> f) x = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(inv f \<circ> g \<circ> f) x = x

goal (1 subgoal):
 1. \<And>x. x \<in> inv f ` Fix g \<Longrightarrow> x \<in> Fix (inv f \<circ> g \<circ> f)
[PROOF STEP]
with Fix_def[of "inv f \<circ> g \<circ> f"]
[PROOF STATE]
proof (chain)
picking this:
Fix (inv f \<circ> g \<circ> f) = {n. (inv f \<circ> g \<circ> f) n = n}
(inv f \<circ> g \<circ> f) x = x
[PROOF STEP]
show "x \<in> Fix ((inv f) \<circ> g \<circ> f)"
[PROOF STATE]
proof (prove)
using this:
Fix (inv f \<circ> g \<circ> f) = {n. (inv f \<circ> g \<circ> f) n = n}
(inv f \<circ> g \<circ> f) x = x

goal (1 subgoal):
 1. x \<in> Fix (inv f \<circ> g \<circ> f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> Fix (inv f \<circ> g \<circ> f)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inv f ` Fix g \<subseteq> Fix (inv f \<circ> g \<circ> f)

goal (1 subgoal):
 1. Fix (inv f \<circ> g \<circ> f) \<subseteq> inv f ` Fix g
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Fix (inv f \<circ> g \<circ> f) \<subseteq> inv f ` Fix g
[PROOF STEP]
show "Fix (inv f \<circ> g \<circ> f) \<subseteq> (inv f)`(Fix g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fix (inv f \<circ> g \<circ> f) \<subseteq> inv f ` Fix g
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Fix (inv f \<circ> g \<circ> f) \<Longrightarrow> x \<in> inv f ` Fix g
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Fix (inv f \<circ> g \<circ> f) \<Longrightarrow> x \<in> inv f ` Fix g
[PROOF STEP]
assume "x \<in> Fix (inv f \<circ> g \<circ> f)"
[PROOF STATE]
proof (state)
this:
x \<in> Fix (inv f \<circ> g \<circ> f)

goal (1 subgoal):
 1. \<And>x. x \<in> Fix (inv f \<circ> g \<circ> f) \<Longrightarrow> x \<in> inv f ` Fix g
[PROOF STEP]
with Fix_def[of "inv f \<circ> g \<circ> f"]
[PROOF STATE]
proof (chain)
picking this:
Fix (inv f \<circ> g \<circ> f) = {n. (inv f \<circ> g \<circ> f) n = n}
x \<in> Fix (inv f \<circ> g \<circ> f)
[PROOF STEP]
have x_fix: "(inv f \<circ> g \<circ> f) x = x"
[PROOF STATE]
proof (prove)
using this:
Fix (inv f \<circ> g \<circ> f) = {n. (inv f \<circ> g \<circ> f) n = n}
x \<in> Fix (inv f \<circ> g \<circ> f)

goal (1 subgoal):
 1. (inv f \<circ> g \<circ> f) x = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(inv f \<circ> g \<circ> f) x = x

goal (1 subgoal):
 1. \<And>x. x \<in> Fix (inv f \<circ> g \<circ> f) \<Longrightarrow> x \<in> inv f ` Fix g
[PROOF STEP]
hence "(inv f) (g(f(x))) = x"
[PROOF STATE]
proof (prove)
using this:
(inv f \<circ> g \<circ> f) x = x

goal (1 subgoal):
 1. inv f (g (f x)) = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv f (g (f x)) = x

goal (1 subgoal):
 1. \<And>x. x \<in> Fix (inv f \<circ> g \<circ> f) \<Longrightarrow> x \<in> inv f ` Fix g
[PROOF STEP]
hence "\<exists>y. (inv f) y = x"
[PROOF STATE]
proof (prove)
using this:
inv f (g (f x)) = x

goal (1 subgoal):
 1. \<exists>y. inv f y = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>y. inv f y = x

goal (1 subgoal):
 1. \<And>x. x \<in> Fix (inv f \<circ> g \<circ> f) \<Longrightarrow> x \<in> inv f ` Fix g
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>y. inv f y = x
[PROOF STEP]
obtain y where x_inf_f_y: "x = (inv f) y"
[PROOF STATE]
proof (prove)
using this:
\<exists>y. inv f y = x

goal (1 subgoal):
 1. (\<And>y. x = inv f y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = inv f y

goal (1 subgoal):
 1. \<And>x. x \<in> Fix (inv f \<circ> g \<circ> f) \<Longrightarrow> x \<in> inv f ` Fix g
[PROOF STEP]
with x_fix
[PROOF STATE]
proof (chain)
picking this:
(inv f \<circ> g \<circ> f) x = x
x = inv f y
[PROOF STEP]
have "(inv f \<circ> g \<circ> f)((inv f) y) = (inv f) y"
[PROOF STATE]
proof (prove)
using this:
(inv f \<circ> g \<circ> f) x = x
x = inv f y

goal (1 subgoal):
 1. (inv f \<circ> g \<circ> f) (inv f y) = inv f y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(inv f \<circ> g \<circ> f) (inv f y) = inv f y

goal (1 subgoal):
 1. \<And>x. x \<in> Fix (inv f \<circ> g \<circ> f) \<Longrightarrow> x \<in> inv f ` Fix g
[PROOF STEP]
hence "(f \<circ> inv f \<circ> g \<circ> f \<circ> inv f) (y) = (f \<circ> inv f)(y)"
[PROOF STATE]
proof (prove)
using this:
(inv f \<circ> g \<circ> f) (inv f y) = inv f y

goal (1 subgoal):
 1. (f \<circ> inv f \<circ> g \<circ> f \<circ> inv f) y = (f \<circ> inv f) y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(f \<circ> inv f \<circ> g \<circ> f \<circ> inv f) y = (f \<circ> inv f) y

goal (1 subgoal):
 1. \<And>x. x \<in> Fix (inv f \<circ> g \<circ> f) \<Longrightarrow> x \<in> inv f ` Fix g
[PROOF STEP]
with o_assoc
[PROOF STATE]
proof (chain)
picking this:
?f \<circ> (?g \<circ> ?h) = ?f \<circ> ?g \<circ> ?h
(f \<circ> inv f \<circ> g \<circ> f \<circ> inv f) y = (f \<circ> inv f) y
[PROOF STEP]
have "((f \<circ> inv f) \<circ> g \<circ> (f \<circ> inv f)) y = (f \<circ> inv f)y"
[PROOF STATE]
proof (prove)
using this:
?f \<circ> (?g \<circ> ?h) = ?f \<circ> ?g \<circ> ?h
(f \<circ> inv f \<circ> g \<circ> f \<circ> inv f) y = (f \<circ> inv f) y

goal (1 subgoal):
 1. (f \<circ> inv f \<circ> g \<circ> (f \<circ> inv f)) y = (f \<circ> inv f) y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(f \<circ> inv f \<circ> g \<circ> (f \<circ> inv f)) y = (f \<circ> inv f) y

goal (1 subgoal):
 1. \<And>x. x \<in> Fix (inv f \<circ> g \<circ> f) \<Longrightarrow> x \<in> inv f ` Fix g
[PROOF STEP]
with bij_f and bij_f_o_inf_f[of f]
[PROOF STATE]
proof (chain)
picking this:
bij f
bij f \<Longrightarrow> f \<circ> inv f = id
(f \<circ> inv f \<circ> g \<circ> (f \<circ> inv f)) y = (f \<circ> inv f) y
[PROOF STEP]
have "g y = y"
[PROOF STATE]
proof (prove)
using this:
bij f
bij f \<Longrightarrow> f \<circ> inv f = id
(f \<circ> inv f \<circ> g \<circ> (f \<circ> inv f)) y = (f \<circ> inv f) y

goal (1 subgoal):
 1. g y = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g y = y

goal (1 subgoal):
 1. \<And>x. x \<in> Fix (inv f \<circ> g \<circ> f) \<Longrightarrow> x \<in> inv f ` Fix g
[PROOF STEP]
with Fix_def[of g]
[PROOF STATE]
proof (chain)
picking this:
Fix g = {n. g n = n}
g y = y
[PROOF STEP]
have "y \<in> Fix g"
[PROOF STATE]
proof (prove)
using this:
Fix g = {n. g n = n}
g y = y

goal (1 subgoal):
 1. y \<in> Fix g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> Fix g

goal (1 subgoal):
 1. \<And>x. x \<in> Fix (inv f \<circ> g \<circ> f) \<Longrightarrow> x \<in> inv f ` Fix g
[PROOF STEP]
with x_inf_f_y
[PROOF STATE]
proof (chain)
picking this:
x = inv f y
y \<in> Fix g
[PROOF STEP]
show "x \<in> (inv f)`(Fix g)"
[PROOF STATE]
proof (prove)
using this:
x = inv f y
y \<in> Fix g

goal (1 subgoal):
 1. x \<in> inv f ` Fix g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> inv f ` Fix g

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Fix (inv f \<circ> g \<circ> f) \<subseteq> inv f ` Fix g

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inv f ` Fix g = Fix (inv f \<circ> g \<circ> f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma type_CONJ: "f \<in> Ex1 \<Longrightarrow> (inv ni_bij) \<circ> f \<circ> ni_bij \<in> S_inf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> CofGroups.Ex1 \<Longrightarrow> inv ni_bij \<circ> f \<circ> ni_bij \<in> S_inf
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<in> CofGroups.Ex1 \<Longrightarrow> inv ni_bij \<circ> f \<circ> ni_bij \<in> S_inf
[PROOF STEP]
assume f_Ex1: "f \<in> Ex1"
[PROOF STATE]
proof (state)
this:
f \<in> CofGroups.Ex1

goal (1 subgoal):
 1. f \<in> CofGroups.Ex1 \<Longrightarrow> inv ni_bij \<circ> f \<circ> ni_bij \<in> S_inf
[PROOF STEP]
with all_bij
[PROOF STATE]
proof (chain)
picking this:
?f \<in> CofGroups.Ex1 \<Longrightarrow> bij ?f
f \<in> CofGroups.Ex1
[PROOF STEP]
have "bij f"
[PROOF STATE]
proof (prove)
using this:
?f \<in> CofGroups.Ex1 \<Longrightarrow> bij ?f
f \<in> CofGroups.Ex1

goal (1 subgoal):
 1. bij f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bij f

goal (1 subgoal):
 1. f \<in> CofGroups.Ex1 \<Longrightarrow> inv ni_bij \<circ> f \<circ> ni_bij \<in> S_inf
[PROOF STEP]
with bij_int_decode and bij_comp
[PROOF STATE]
proof (chain)
picking this:
bij ni_bij
\<lbrakk>bij ?f; bij ?g\<rbrakk> \<Longrightarrow> bij (?g \<circ> ?f)
bij f
[PROOF STEP]
have bij_f_nibij: "bij (f \<circ> ni_bij)"
[PROOF STATE]
proof (prove)
using this:
bij ni_bij
\<lbrakk>bij ?f; bij ?g\<rbrakk> \<Longrightarrow> bij (?g \<circ> ?f)
bij f

goal (1 subgoal):
 1. bij (f \<circ> ni_bij)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bij (f \<circ> ni_bij)

goal (1 subgoal):
 1. f \<in> CofGroups.Ex1 \<Longrightarrow> inv ni_bij \<circ> f \<circ> ni_bij \<in> S_inf
[PROOF STEP]
with bij_int_decode and bij_imp_bij_inv
[PROOF STATE]
proof (chain)
picking this:
bij ni_bij
bij ?f \<Longrightarrow> bij (inv ?f)
bij (f \<circ> ni_bij)
[PROOF STEP]
have "bij (inv ni_bij)"
[PROOF STATE]
proof (prove)
using this:
bij ni_bij
bij ?f \<Longrightarrow> bij (inv ?f)
bij (f \<circ> ni_bij)

goal (1 subgoal):
 1. bij (inv ni_bij)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bij (inv ni_bij)

goal (1 subgoal):
 1. f \<in> CofGroups.Ex1 \<Longrightarrow> inv ni_bij \<circ> f \<circ> ni_bij \<in> S_inf
[PROOF STEP]
with bij_f_nibij and bij_comp[of  "f \<circ> ni_bij" "inv ni_bij"]
    and o_assoc[of "inv ni_bij" "f" "ni_bij"]
[PROOF STATE]
proof (chain)
picking this:
bij (f \<circ> ni_bij)
\<lbrakk>bij (f \<circ> ni_bij); bij (inv ni_bij)\<rbrakk> \<Longrightarrow> bij (inv ni_bij \<circ> (f \<circ> ni_bij))
inv ni_bij \<circ> (f \<circ> ni_bij) = inv ni_bij \<circ> f \<circ> ni_bij
bij (inv ni_bij)
[PROOF STEP]
have "bij ((inv ni_bij) \<circ> f \<circ> ni_bij)"
[PROOF STATE]
proof (prove)
using this:
bij (f \<circ> ni_bij)
\<lbrakk>bij (f \<circ> ni_bij); bij (inv ni_bij)\<rbrakk> \<Longrightarrow> bij (inv ni_bij \<circ> (f \<circ> ni_bij))
inv ni_bij \<circ> (f \<circ> ni_bij) = inv ni_bij \<circ> f \<circ> ni_bij
bij (inv ni_bij)

goal (1 subgoal):
 1. bij (inv ni_bij \<circ> f \<circ> ni_bij)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bij (inv ni_bij \<circ> f \<circ> ni_bij)

goal (1 subgoal):
 1. f \<in> CofGroups.Ex1 \<Longrightarrow> inv ni_bij \<circ> f \<circ> ni_bij \<in> S_inf
[PROOF STEP]
with S_inf_def
[PROOF STATE]
proof (chain)
picking this:
S_inf = {f. bij f}
bij (inv ni_bij \<circ> f \<circ> ni_bij)
[PROOF STEP]
show "((inv ni_bij) \<circ> f \<circ> ni_bij) \<in> S_inf"
[PROOF STATE]
proof (prove)
using this:
S_inf = {f. bij f}
bij (inv ni_bij \<circ> f \<circ> ni_bij)

goal (1 subgoal):
 1. inv ni_bij \<circ> f \<circ> ni_bij \<in> S_inf
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv ni_bij \<circ> f \<circ> ni_bij \<in> S_inf

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inv_CONJ:
  assumes bij_f: "bij f"
  shows "inv (CONJ f) = CONJ (inv f)" (is "?left = ?right")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv (CONJ f) = CONJ (inv f)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv (CONJ f) = CONJ (inv f)
[PROOF STEP]
have st1: "?left = inv ((inv ni_bij) \<circ> f \<circ> ni_bij)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv (CONJ f) = inv (inv ni_bij \<circ> f \<circ> ni_bij)
[PROOF STEP]
using CONJ_def
[PROOF STATE]
proof (prove)
using this:
CONJ ?f = inv ni_bij \<circ> ?f \<circ> ni_bij

goal (1 subgoal):
 1. inv (CONJ f) = inv (inv ni_bij \<circ> f \<circ> ni_bij)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv (CONJ f) = inv (inv ni_bij \<circ> f \<circ> ni_bij)

goal (1 subgoal):
 1. inv (CONJ f) = CONJ (inv f)
[PROOF STEP]
from bij_int_decode and bij_imp_bij_inv
[PROOF STATE]
proof (chain)
picking this:
bij ni_bij
bij ?f \<Longrightarrow> bij (inv ?f)
[PROOF STEP]
have inv_ni_bij_bij: "bij (inv ni_bij)"
[PROOF STATE]
proof (prove)
using this:
bij ni_bij
bij ?f \<Longrightarrow> bij (inv ?f)

goal (1 subgoal):
 1. bij (inv ni_bij)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bij (inv ni_bij)

goal (1 subgoal):
 1. inv (CONJ f) = CONJ (inv f)
[PROOF STEP]
with bij_f and bij_comp
[PROOF STATE]
proof (chain)
picking this:
bij f
\<lbrakk>bij ?f; bij ?g\<rbrakk> \<Longrightarrow> bij (?g \<circ> ?f)
bij (inv ni_bij)
[PROOF STEP]
have "bij (inv ni_bij \<circ> f)"
[PROOF STATE]
proof (prove)
using this:
bij f
\<lbrakk>bij ?f; bij ?g\<rbrakk> \<Longrightarrow> bij (?g \<circ> ?f)
bij (inv ni_bij)

goal (1 subgoal):
 1. bij (inv ni_bij \<circ> f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bij (inv ni_bij \<circ> f)

goal (1 subgoal):
 1. inv (CONJ f) = CONJ (inv f)
[PROOF STEP]
with o_inv_distrib[of "inv ni_bij \<circ> f" ni_bij] and bij_int_decode
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>bij (inv ni_bij \<circ> f); bij ni_bij\<rbrakk> \<Longrightarrow> inv (inv ni_bij \<circ> f \<circ> ni_bij) = inv ni_bij \<circ> inv (inv ni_bij \<circ> f)
bij ni_bij
bij (inv ni_bij \<circ> f)
[PROOF STEP]
have "inv ((inv ni_bij) \<circ> f \<circ>  ni_bij) =
    (inv ni_bij) \<circ> (inv ((inv ni_bij) \<circ> f))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>bij (inv ni_bij \<circ> f); bij ni_bij\<rbrakk> \<Longrightarrow> inv (inv ni_bij \<circ> f \<circ> ni_bij) = inv ni_bij \<circ> inv (inv ni_bij \<circ> f)
bij ni_bij
bij (inv ni_bij \<circ> f)

goal (1 subgoal):
 1. inv (inv ni_bij \<circ> f \<circ> ni_bij) = inv ni_bij \<circ> inv (inv ni_bij \<circ> f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv (inv ni_bij \<circ> f \<circ> ni_bij) = inv ni_bij \<circ> inv (inv ni_bij \<circ> f)

goal (1 subgoal):
 1. inv (CONJ f) = CONJ (inv f)
[PROOF STEP]
with st1
[PROOF STATE]
proof (chain)
picking this:
inv (CONJ f) = inv (inv ni_bij \<circ> f \<circ> ni_bij)
inv (inv ni_bij \<circ> f \<circ> ni_bij) = inv ni_bij \<circ> inv (inv ni_bij \<circ> f)
[PROOF STEP]
have st2: "?left =
    (inv ni_bij) \<circ> (inv ((inv ni_bij) \<circ> f))"
[PROOF STATE]
proof (prove)
using this:
inv (CONJ f) = inv (inv ni_bij \<circ> f \<circ> ni_bij)
inv (inv ni_bij \<circ> f \<circ> ni_bij) = inv ni_bij \<circ> inv (inv ni_bij \<circ> f)

goal (1 subgoal):
 1. inv (CONJ f) = inv ni_bij \<circ> inv (inv ni_bij \<circ> f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv (CONJ f) = inv ni_bij \<circ> inv (inv ni_bij \<circ> f)

goal (1 subgoal):
 1. inv (CONJ f) = CONJ (inv f)
[PROOF STEP]
from inv_ni_bij_bij and \<open>bij f\<close> and o_inv_distrib
[PROOF STATE]
proof (chain)
picking this:
bij (inv ni_bij)
bij f
\<lbrakk>bij ?f; bij ?g\<rbrakk> \<Longrightarrow> inv (?f \<circ> ?g) = inv ?g \<circ> inv ?f
[PROOF STEP]
have h1: "inv (inv ni_bij \<circ> f) = inv f \<circ> inv (inv (ni_bij))"
[PROOF STATE]
proof (prove)
using this:
bij (inv ni_bij)
bij f
\<lbrakk>bij ?f; bij ?g\<rbrakk> \<Longrightarrow> inv (?f \<circ> ?g) = inv ?g \<circ> inv ?f

goal (1 subgoal):
 1. inv (inv ni_bij \<circ> f) = inv f \<circ> inv (inv ni_bij)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv (inv ni_bij \<circ> f) = inv f \<circ> inv (inv ni_bij)

goal (1 subgoal):
 1. inv (CONJ f) = CONJ (inv f)
[PROOF STEP]
from bij_int_decode and inv_inv_eq[of ni_bij]
[PROOF STATE]
proof (chain)
picking this:
bij ni_bij
bij ni_bij \<Longrightarrow> inv (inv ni_bij) = ni_bij
[PROOF STEP]
have "inv (inv ni_bij) = ni_bij"
[PROOF STATE]
proof (prove)
using this:
bij ni_bij
bij ni_bij \<Longrightarrow> inv (inv ni_bij) = ni_bij

goal (1 subgoal):
 1. inv (inv ni_bij) = ni_bij
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv (inv ni_bij) = ni_bij

goal (1 subgoal):
 1. inv (CONJ f) = CONJ (inv f)
[PROOF STEP]
with st2 and h1
[PROOF STATE]
proof (chain)
picking this:
inv (CONJ f) = inv ni_bij \<circ> inv (inv ni_bij \<circ> f)
inv (inv ni_bij \<circ> f) = inv f \<circ> inv (inv ni_bij)
inv (inv ni_bij) = ni_bij
[PROOF STEP]
have "?left = (inv ni_bij \<circ> (inv f \<circ> ( ni_bij)))"
[PROOF STATE]
proof (prove)
using this:
inv (CONJ f) = inv ni_bij \<circ> inv (inv ni_bij \<circ> f)
inv (inv ni_bij \<circ> f) = inv f \<circ> inv (inv ni_bij)
inv (inv ni_bij) = ni_bij

goal (1 subgoal):
 1. inv (CONJ f) = inv ni_bij \<circ> (inv f \<circ> ni_bij)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv (CONJ f) = inv ni_bij \<circ> (inv f \<circ> ni_bij)

goal (1 subgoal):
 1. inv (CONJ f) = CONJ (inv f)
[PROOF STEP]
with o_assoc
[PROOF STATE]
proof (chain)
picking this:
?f \<circ> (?g \<circ> ?h) = ?f \<circ> ?g \<circ> ?h
inv (CONJ f) = inv ni_bij \<circ> (inv f \<circ> ni_bij)
[PROOF STEP]
have "?left = inv ni_bij \<circ> inv f \<circ> ni_bij"
[PROOF STATE]
proof (prove)
using this:
?f \<circ> (?g \<circ> ?h) = ?f \<circ> ?g \<circ> ?h
inv (CONJ f) = inv ni_bij \<circ> (inv f \<circ> ni_bij)

goal (1 subgoal):
 1. inv (CONJ f) = inv ni_bij \<circ> inv f \<circ> ni_bij
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv (CONJ f) = inv ni_bij \<circ> inv f \<circ> ni_bij

goal (1 subgoal):
 1. inv (CONJ f) = CONJ (inv f)
[PROOF STEP]
with CONJ_def[of "inv f"]
[PROOF STATE]
proof (chain)
picking this:
CONJ (inv f) = inv ni_bij \<circ> inv f \<circ> ni_bij
inv (CONJ f) = inv ni_bij \<circ> inv f \<circ> ni_bij
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
CONJ (inv f) = inv ni_bij \<circ> inv f \<circ> ni_bij
inv (CONJ f) = inv ni_bij \<circ> inv f \<circ> ni_bij

goal (1 subgoal):
 1. inv (CONJ f) = CONJ (inv f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv (CONJ f) = CONJ (inv f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma comp_CONJ:
  "CONJ (f \<circ> g) = (CONJ f) \<circ> (CONJ g)" (is "?left = ?right")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CONJ (f \<circ> g) = CONJ f \<circ> CONJ g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. CONJ (f \<circ> g) = CONJ f \<circ> CONJ g
[PROOF STEP]
from bij_int_decode
[PROOF STATE]
proof (chain)
picking this:
bij ni_bij
[PROOF STEP]
have "surj ni_bij"
[PROOF STATE]
proof (prove)
using this:
bij ni_bij

goal (1 subgoal):
 1. surj ni_bij
[PROOF STEP]
unfolding bij_def
[PROOF STATE]
proof (prove)
using this:
inj ni_bij \<and> surj ni_bij

goal (1 subgoal):
 1. surj ni_bij
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
surj ni_bij

goal (1 subgoal):
 1. CONJ (f \<circ> g) = CONJ f \<circ> CONJ g
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
surj ni_bij
[PROOF STEP]
have "ni_bij \<circ> (inv ni_bij) = id"
[PROOF STATE]
proof (prove)
using this:
surj ni_bij

goal (1 subgoal):
 1. ni_bij \<circ> inv ni_bij = id
[PROOF STEP]
unfolding surj_iff
[PROOF STATE]
proof (prove)
using this:
ni_bij \<circ> inv ni_bij = id

goal (1 subgoal):
 1. ni_bij \<circ> inv ni_bij = id
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ni_bij \<circ> inv ni_bij = id

goal (1 subgoal):
 1. CONJ (f \<circ> g) = CONJ f \<circ> CONJ g
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ni_bij \<circ> inv ni_bij = id

goal (1 subgoal):
 1. CONJ (f \<circ> g) = CONJ f \<circ> CONJ g
[PROOF STEP]
have "?left = (inv ni_bij) \<circ> (f \<circ> g) \<circ> ni_bij"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CONJ (f \<circ> g) = inv ni_bij \<circ> (f \<circ> g) \<circ> ni_bij
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
CONJ (f \<circ> g) = inv ni_bij \<circ> (f \<circ> g) \<circ> ni_bij

goal (1 subgoal):
 1. CONJ (f \<circ> g) = CONJ f \<circ> CONJ g
[PROOF STEP]
hence "?left = (inv ni_bij) \<circ> ((f \<circ> id) \<circ> g) \<circ> ni_bij"
[PROOF STATE]
proof (prove)
using this:
CONJ (f \<circ> g) = inv ni_bij \<circ> (f \<circ> g) \<circ> ni_bij

goal (1 subgoal):
 1. CONJ (f \<circ> g) = inv ni_bij \<circ> (f \<circ> id \<circ> g) \<circ> ni_bij
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
CONJ (f \<circ> g) = inv ni_bij \<circ> (f \<circ> id \<circ> g) \<circ> ni_bij

goal (1 subgoal):
 1. CONJ (f \<circ> g) = CONJ f \<circ> CONJ g
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ni_bij \<circ> inv ni_bij = id
CONJ (f \<circ> g) = inv ni_bij \<circ> (f \<circ> id \<circ> g) \<circ> ni_bij
[PROOF STEP]
have "?left =
    (inv ni_bij) \<circ> ((f \<circ> (ni_bij \<circ> (inv ni_bij))) \<circ> g) \<circ> ni_bij"
[PROOF STATE]
proof (prove)
using this:
ni_bij \<circ> inv ni_bij = id
CONJ (f \<circ> g) = inv ni_bij \<circ> (f \<circ> id \<circ> g) \<circ> ni_bij

goal (1 subgoal):
 1. CONJ (f \<circ> g) = inv ni_bij \<circ> (f \<circ> (ni_bij \<circ> inv ni_bij) \<circ> g) \<circ> ni_bij
[PROOF STEP]
by auto
      \<comment> \<open>a simple computation using only associativity\<close>
      \<comment> \<open>completes the proof\<close>
[PROOF STATE]
proof (state)
this:
CONJ (f \<circ> g) = inv ni_bij \<circ> (f \<circ> (ni_bij \<circ> inv ni_bij) \<circ> g) \<circ> ni_bij

goal (1 subgoal):
 1. CONJ (f \<circ> g) = CONJ f \<circ> CONJ g
[PROOF STEP]
thus "?left = ?right"
[PROOF STATE]
proof (prove)
using this:
CONJ (f \<circ> g) = inv ni_bij \<circ> (f \<circ> (ni_bij \<circ> inv ni_bij) \<circ> g) \<circ> ni_bij

goal (1 subgoal):
 1. CONJ (f \<circ> g) = CONJ f \<circ> CONJ g
[PROOF STEP]
by (auto simp add: o_assoc)
[PROOF STATE]
proof (state)
this:
CONJ (f \<circ> g) = CONJ f \<circ> CONJ g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma id_CONJ: "CONJ id = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CONJ id = id
[PROOF STEP]
proof (unfold CONJ_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv ni_bij \<circ> id \<circ> ni_bij = id
[PROOF STEP]
from bij_int_decode
[PROOF STATE]
proof (chain)
picking this:
bij ni_bij
[PROOF STEP]
have "inj ni_bij"
[PROOF STATE]
proof (prove)
using this:
bij ni_bij

goal (1 subgoal):
 1. inj ni_bij
[PROOF STEP]
using bij_def
[PROOF STATE]
proof (prove)
using this:
bij ni_bij
bij ?f = (inj ?f \<and> surj ?f)

goal (1 subgoal):
 1. inj ni_bij
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inj ni_bij

goal (1 subgoal):
 1. inv ni_bij \<circ> id \<circ> ni_bij = id
[PROOF STEP]
hence "inv ni_bij \<circ> ni_bij = id"
[PROOF STATE]
proof (prove)
using this:
inj ni_bij

goal (1 subgoal):
 1. inv ni_bij \<circ> ni_bij = id
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv ni_bij \<circ> ni_bij = id

goal (1 subgoal):
 1. inv ni_bij \<circ> id \<circ> ni_bij = id
[PROOF STEP]
thus "(inv ni_bij \<circ> id) \<circ> ni_bij = id"
[PROOF STATE]
proof (prove)
using this:
inv ni_bij \<circ> ni_bij = id

goal (1 subgoal):
 1. inv ni_bij \<circ> id \<circ> ni_bij = id
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv ni_bij \<circ> id \<circ> ni_bij = id

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem mem_Ex2_rule: "f \<in> Ex2 = (\<exists>g. (g \<in> Ex1 \<and> f = CONJ g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<in> Ex2) = (\<exists>g. g \<in> CofGroups.Ex1 \<and> f = CONJ g)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f \<in> Ex2 \<Longrightarrow> \<exists>g. g \<in> CofGroups.Ex1 \<and> f = CONJ g
 2. \<exists>g. g \<in> CofGroups.Ex1 \<and> f = CONJ g \<Longrightarrow> f \<in> Ex2
[PROOF STEP]
assume "f \<in> Ex2"
[PROOF STATE]
proof (state)
this:
f \<in> Ex2

goal (2 subgoals):
 1. f \<in> Ex2 \<Longrightarrow> \<exists>g. g \<in> CofGroups.Ex1 \<and> f = CONJ g
 2. \<exists>g. g \<in> CofGroups.Ex1 \<and> f = CONJ g \<Longrightarrow> f \<in> Ex2
[PROOF STEP]
hence "f \<in> CONJ`Ex1"
[PROOF STATE]
proof (prove)
using this:
f \<in> Ex2

goal (1 subgoal):
 1. f \<in> CONJ ` CofGroups.Ex1
[PROOF STEP]
using Ex2_def
[PROOF STATE]
proof (prove)
using this:
f \<in> Ex2
Ex2 = CONJ ` CofGroups.Ex1

goal (1 subgoal):
 1. f \<in> CONJ ` CofGroups.Ex1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> CONJ ` CofGroups.Ex1

goal (2 subgoals):
 1. f \<in> Ex2 \<Longrightarrow> \<exists>g. g \<in> CofGroups.Ex1 \<and> f = CONJ g
 2. \<exists>g. g \<in> CofGroups.Ex1 \<and> f = CONJ g \<Longrightarrow> f \<in> Ex2
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
f \<in> CONJ ` CofGroups.Ex1
[PROOF STEP]
obtain "g" where "g \<in> Ex1 \<and> f = CONJ g"
[PROOF STATE]
proof (prove)
using this:
f \<in> CONJ ` CofGroups.Ex1

goal (1 subgoal):
 1. (\<And>g. g \<in> CofGroups.Ex1 \<and> f = CONJ g \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
g \<in> CofGroups.Ex1 \<and> f = CONJ g

goal (2 subgoals):
 1. f \<in> Ex2 \<Longrightarrow> \<exists>g. g \<in> CofGroups.Ex1 \<and> f = CONJ g
 2. \<exists>g. g \<in> CofGroups.Ex1 \<and> f = CONJ g \<Longrightarrow> f \<in> Ex2
[PROOF STEP]
thus "\<exists>g. (g \<in> Ex1 \<and> f = CONJ g)"
[PROOF STATE]
proof (prove)
using this:
g \<in> CofGroups.Ex1 \<and> f = CONJ g

goal (1 subgoal):
 1. \<exists>g. g \<in> CofGroups.Ex1 \<and> f = CONJ g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>g. g \<in> CofGroups.Ex1 \<and> f = CONJ g

goal (1 subgoal):
 1. \<exists>g. g \<in> CofGroups.Ex1 \<and> f = CONJ g \<Longrightarrow> f \<in> Ex2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>g. g \<in> CofGroups.Ex1 \<and> f = CONJ g \<Longrightarrow> f \<in> Ex2
[PROOF STEP]
assume "\<exists>g. (g \<in> Ex1 \<and> f = CONJ g)"
[PROOF STATE]
proof (state)
this:
\<exists>g. g \<in> CofGroups.Ex1 \<and> f = CONJ g

goal (1 subgoal):
 1. \<exists>g. g \<in> CofGroups.Ex1 \<and> f = CONJ g \<Longrightarrow> f \<in> Ex2
[PROOF STEP]
with Ex2_def
[PROOF STATE]
proof (chain)
picking this:
Ex2 = CONJ ` CofGroups.Ex1
\<exists>g. g \<in> CofGroups.Ex1 \<and> f = CONJ g
[PROOF STEP]
show "f \<in> Ex2"
[PROOF STATE]
proof (prove)
using this:
Ex2 = CONJ ` CofGroups.Ex1
\<exists>g. g \<in> CofGroups.Ex1 \<and> f = CONJ g

goal (1 subgoal):
 1. f \<in> Ex2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> Ex2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem Ex2_cofinitary:
  assumes f_Ex2: "f \<in> Ex2"
  and f_nid: "f \<noteq> id"
  shows "Fix f = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fix f = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Fix f = {}
[PROOF STEP]
from f_Ex2 and mem_Ex2_rule
[PROOF STATE]
proof (chain)
picking this:
f \<in> Ex2
(?f \<in> Ex2) = (\<exists>g. g \<in> CofGroups.Ex1 \<and> ?f = CONJ g)
[PROOF STEP]
obtain g where g_Ex1: "g \<in> Ex1" and f_cg: "f = CONJ g"
[PROOF STATE]
proof (prove)
using this:
f \<in> Ex2
(?f \<in> Ex2) = (\<exists>g. g \<in> CofGroups.Ex1 \<and> ?f = CONJ g)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> CofGroups.Ex1; f = CONJ g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g \<in> CofGroups.Ex1
f = CONJ g

goal (1 subgoal):
 1. Fix f = {}
[PROOF STEP]
with id_CONJ and f_nid
[PROOF STATE]
proof (chain)
picking this:
CONJ id = id
f \<noteq> id
g \<in> CofGroups.Ex1
f = CONJ g
[PROOF STEP]
have "g \<noteq> id"
[PROOF STATE]
proof (prove)
using this:
CONJ id = id
f \<noteq> id
g \<in> CofGroups.Ex1
f = CONJ g

goal (1 subgoal):
 1. g \<noteq> id
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g \<noteq> id

goal (1 subgoal):
 1. Fix f = {}
[PROOF STEP]
with g_Ex1 and no_fixed_pt[of g]
[PROOF STATE]
proof (chain)
picking this:
g \<in> CofGroups.Ex1
\<lbrakk>g \<in> CofGroups.Ex1; g \<noteq> id\<rbrakk> \<Longrightarrow> Fix g = {}
g \<noteq> id
[PROOF STEP]
have fg_empty: "Fix g = {}"
[PROOF STATE]
proof (prove)
using this:
g \<in> CofGroups.Ex1
\<lbrakk>g \<in> CofGroups.Ex1; g \<noteq> id\<rbrakk> \<Longrightarrow> Fix g = {}
g \<noteq> id

goal (1 subgoal):
 1. Fix g = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Fix g = {}

goal (1 subgoal):
 1. Fix f = {}
[PROOF STEP]
from conj_fix_pt[of ni_bij g] and bij_int_decode
[PROOF STATE]
proof (chain)
picking this:
bij ni_bij \<Longrightarrow> inv ni_bij ` Fix g = Fix (inv ni_bij \<circ> g \<circ> ni_bij)
bij ni_bij
[PROOF STEP]
have "(inv ni_bij)`(Fix g) = Fix(CONJ g)"
[PROOF STATE]
proof (prove)
using this:
bij ni_bij \<Longrightarrow> inv ni_bij ` Fix g = Fix (inv ni_bij \<circ> g \<circ> ni_bij)
bij ni_bij

goal (1 subgoal):
 1. inv ni_bij ` Fix g = Fix (CONJ g)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv ni_bij ` Fix g = Fix (CONJ g)

goal (1 subgoal):
 1. Fix f = {}
[PROOF STEP]
with fg_empty
[PROOF STATE]
proof (chain)
picking this:
Fix g = {}
inv ni_bij ` Fix g = Fix (CONJ g)
[PROOF STEP]
have "{} = Fix (CONJ g)"
[PROOF STATE]
proof (prove)
using this:
Fix g = {}
inv ni_bij ` Fix g = Fix (CONJ g)

goal (1 subgoal):
 1. {} = Fix (CONJ g)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{} = Fix (CONJ g)

goal (1 subgoal):
 1. Fix f = {}
[PROOF STEP]
with f_cg
[PROOF STATE]
proof (chain)
picking this:
f = CONJ g
{} = Fix (CONJ g)
[PROOF STEP]
show "Fix f = {}"
[PROOF STATE]
proof (prove)
using this:
f = CONJ g
{} = Fix (CONJ g)

goal (1 subgoal):
 1. Fix f = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Fix f = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma id_Ex2: "id \<in> Ex2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. id \<in> Ex2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. id \<in> Ex2
[PROOF STEP]
from Ex1_Normal_form_part2[of "0"]
[PROOF STATE]
proof (chain)
picking this:
\<forall>f. (\<forall>n. f n = n + 0) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
have "id \<in> Ex1"
[PROOF STATE]
proof (prove)
using this:
\<forall>f. (\<forall>n. f n = n + 0) \<longrightarrow> f \<in> CofGroups.Ex1

goal (1 subgoal):
 1. id \<in> CofGroups.Ex1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
id \<in> CofGroups.Ex1

goal (1 subgoal):
 1. id \<in> Ex2
[PROOF STEP]
with id_CONJ and Ex2_def and mem_Ex2_rule
[PROOF STATE]
proof (chain)
picking this:
CONJ id = id
Ex2 = CONJ ` CofGroups.Ex1
(?f \<in> Ex2) = (\<exists>g. g \<in> CofGroups.Ex1 \<and> ?f = CONJ g)
id \<in> CofGroups.Ex1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
CONJ id = id
Ex2 = CONJ ` CofGroups.Ex1
(?f \<in> Ex2) = (\<exists>g. g \<in> CofGroups.Ex1 \<and> ?f = CONJ g)
id \<in> CofGroups.Ex1

goal (1 subgoal):
 1. id \<in> Ex2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
id \<in> Ex2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inv_Ex2: "f \<in> Ex2 \<Longrightarrow> (inv f) \<in> Ex2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> Ex2 \<Longrightarrow> inv f \<in> Ex2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<in> Ex2 \<Longrightarrow> inv f \<in> Ex2
[PROOF STEP]
assume "f \<in> Ex2"
[PROOF STATE]
proof (state)
this:
f \<in> Ex2

goal (1 subgoal):
 1. f \<in> Ex2 \<Longrightarrow> inv f \<in> Ex2
[PROOF STEP]
with mem_Ex2_rule
[PROOF STATE]
proof (chain)
picking this:
(?f \<in> Ex2) = (\<exists>g. g \<in> CofGroups.Ex1 \<and> ?f = CONJ g)
f \<in> Ex2
[PROOF STEP]
obtain "g" where "g \<in> Ex1" and "f = CONJ g"
[PROOF STATE]
proof (prove)
using this:
(?f \<in> Ex2) = (\<exists>g. g \<in> CofGroups.Ex1 \<and> ?f = CONJ g)
f \<in> Ex2

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> CofGroups.Ex1; f = CONJ g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g \<in> CofGroups.Ex1
f = CONJ g

goal (1 subgoal):
 1. f \<in> Ex2 \<Longrightarrow> inv f \<in> Ex2
[PROOF STEP]
with closed_inv
[PROOF STATE]
proof (chain)
picking this:
?f \<in> CofGroups.Ex1 \<Longrightarrow> inv ?f \<in> CofGroups.Ex1
g \<in> CofGroups.Ex1
f = CONJ g
[PROOF STEP]
have "inv g \<in> Ex1"
[PROOF STATE]
proof (prove)
using this:
?f \<in> CofGroups.Ex1 \<Longrightarrow> inv ?f \<in> CofGroups.Ex1
g \<in> CofGroups.Ex1
f = CONJ g

goal (1 subgoal):
 1. inv g \<in> CofGroups.Ex1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv g \<in> CofGroups.Ex1

goal (1 subgoal):
 1. f \<in> Ex2 \<Longrightarrow> inv f \<in> Ex2
[PROOF STEP]
from \<open>f = CONJ g\<close>
[PROOF STATE]
proof (chain)
picking this:
f = CONJ g
[PROOF STEP]
have if_iCg: "inv f = inv (CONJ g)"
[PROOF STATE]
proof (prove)
using this:
f = CONJ g

goal (1 subgoal):
 1. inv f = inv (CONJ g)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv f = inv (CONJ g)

goal (1 subgoal):
 1. f \<in> Ex2 \<Longrightarrow> inv f \<in> Ex2
[PROOF STEP]
from all_bij and \<open>g \<in> Ex1\<close>
[PROOF STATE]
proof (chain)
picking this:
?f \<in> CofGroups.Ex1 \<Longrightarrow> bij ?f
g \<in> CofGroups.Ex1
[PROOF STEP]
have "bij g"
[PROOF STATE]
proof (prove)
using this:
?f \<in> CofGroups.Ex1 \<Longrightarrow> bij ?f
g \<in> CofGroups.Ex1

goal (1 subgoal):
 1. bij g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bij g

goal (1 subgoal):
 1. f \<in> Ex2 \<Longrightarrow> inv f \<in> Ex2
[PROOF STEP]
with if_iCg and inv_CONJ
[PROOF STATE]
proof (chain)
picking this:
inv f = inv (CONJ g)
bij ?f \<Longrightarrow> inv (CONJ ?f) = CONJ (inv ?f)
bij g
[PROOF STEP]
have "inv f = CONJ (inv g)"
[PROOF STATE]
proof (prove)
using this:
inv f = inv (CONJ g)
bij ?f \<Longrightarrow> inv (CONJ ?f) = CONJ (inv ?f)
bij g

goal (1 subgoal):
 1. inv f = CONJ (inv g)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv f = CONJ (inv g)

goal (1 subgoal):
 1. f \<in> Ex2 \<Longrightarrow> inv f \<in> Ex2
[PROOF STEP]
from \<open>g \<in> Ex1\<close> and "closed_inv"
[PROOF STATE]
proof (chain)
picking this:
g \<in> CofGroups.Ex1
?f \<in> CofGroups.Ex1 \<Longrightarrow> inv ?f \<in> CofGroups.Ex1
[PROOF STEP]
have "inv g \<in> Ex1"
[PROOF STATE]
proof (prove)
using this:
g \<in> CofGroups.Ex1
?f \<in> CofGroups.Ex1 \<Longrightarrow> inv ?f \<in> CofGroups.Ex1

goal (1 subgoal):
 1. inv g \<in> CofGroups.Ex1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv g \<in> CofGroups.Ex1

goal (1 subgoal):
 1. f \<in> Ex2 \<Longrightarrow> inv f \<in> Ex2
[PROOF STEP]
with \<open>inv f = CONJ (inv g)\<close> and mem_Ex2_rule
[PROOF STATE]
proof (chain)
picking this:
inv f = CONJ (inv g)
(?f \<in> Ex2) = (\<exists>g. g \<in> CofGroups.Ex1 \<and> ?f = CONJ g)
inv g \<in> CofGroups.Ex1
[PROOF STEP]
show "inv f \<in> Ex2"
[PROOF STATE]
proof (prove)
using this:
inv f = CONJ (inv g)
(?f \<in> Ex2) = (\<exists>g. g \<in> CofGroups.Ex1 \<and> ?f = CONJ g)
inv g \<in> CofGroups.Ex1

goal (1 subgoal):
 1. inv f \<in> Ex2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv f \<in> Ex2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma comp_Ex2:
  assumes f_Ex2: "f \<in> Ex2" and
  g_Ex2: "g \<in> Ex2"
  shows "f \<circ> g \<in> Ex2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<circ> g \<in> Ex2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<circ> g \<in> Ex2
[PROOF STEP]
from f_Ex2
[PROOF STATE]
proof (chain)
picking this:
f \<in> Ex2
[PROOF STEP]
obtain f_1
    where f_1_Ex1: "f_1 \<in> Ex1" and "f = CONJ f_1"
[PROOF STATE]
proof (prove)
using this:
f \<in> Ex2

goal (1 subgoal):
 1. (\<And>f_1. \<lbrakk>f_1 \<in> CofGroups.Ex1; f = CONJ f_1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using mem_Ex2_rule
[PROOF STATE]
proof (prove)
using this:
f \<in> Ex2
(?f \<in> Ex2) = (\<exists>g. g \<in> CofGroups.Ex1 \<and> ?f = CONJ g)

goal (1 subgoal):
 1. (\<And>f_1. \<lbrakk>f_1 \<in> CofGroups.Ex1; f = CONJ f_1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f_1 \<in> CofGroups.Ex1
f = CONJ f_1

goal (1 subgoal):
 1. f \<circ> g \<in> Ex2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f_1 \<in> CofGroups.Ex1
f = CONJ f_1

goal (1 subgoal):
 1. f \<circ> g \<in> Ex2
[PROOF STEP]
from g_Ex2
[PROOF STATE]
proof (chain)
picking this:
g \<in> Ex2
[PROOF STEP]
obtain g_1
    where g_1_Ex1: "g_1 \<in> Ex1" and "g = CONJ g_1"
[PROOF STATE]
proof (prove)
using this:
g \<in> Ex2

goal (1 subgoal):
 1. (\<And>g_1. \<lbrakk>g_1 \<in> CofGroups.Ex1; g = CONJ g_1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using mem_Ex2_rule
[PROOF STATE]
proof (prove)
using this:
g \<in> Ex2
(?f \<in> Ex2) = (\<exists>g. g \<in> CofGroups.Ex1 \<and> ?f = CONJ g)

goal (1 subgoal):
 1. (\<And>g_1. \<lbrakk>g_1 \<in> CofGroups.Ex1; g = CONJ g_1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g_1 \<in> CofGroups.Ex1
g = CONJ g_1

goal (1 subgoal):
 1. f \<circ> g \<in> Ex2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f_1 \<in> CofGroups.Ex1
f = CONJ f_1
g_1 \<in> CofGroups.Ex1
g = CONJ g_1
[PROOF STEP]
have "f \<circ> g = (CONJ f_1) \<circ> (CONJ g_1)"
[PROOF STATE]
proof (prove)
using this:
f_1 \<in> CofGroups.Ex1
f = CONJ f_1
g_1 \<in> CofGroups.Ex1
g = CONJ g_1

goal (1 subgoal):
 1. f \<circ> g = CONJ f_1 \<circ> CONJ g_1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<circ> g = CONJ f_1 \<circ> CONJ g_1

goal (1 subgoal):
 1. f \<circ> g \<in> Ex2
[PROOF STEP]
hence "f \<circ> g = CONJ (f_1 \<circ> g_1)"
[PROOF STATE]
proof (prove)
using this:
f \<circ> g = CONJ f_1 \<circ> CONJ g_1

goal (1 subgoal):
 1. f \<circ> g = CONJ (f_1 \<circ> g_1)
[PROOF STEP]
using comp_CONJ
[PROOF STATE]
proof (prove)
using this:
f \<circ> g = CONJ f_1 \<circ> CONJ g_1
CONJ (?f \<circ> ?g) = CONJ ?f \<circ> CONJ ?g

goal (1 subgoal):
 1. f \<circ> g = CONJ (f_1 \<circ> g_1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<circ> g = CONJ (f_1 \<circ> g_1)

goal (1 subgoal):
 1. f \<circ> g \<in> Ex2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f \<circ> g = CONJ (f_1 \<circ> g_1)

goal (1 subgoal):
 1. f \<circ> g \<in> Ex2
[PROOF STEP]
have "f_1 \<circ> g_1 \<in> Ex1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_1 \<circ> g_1 \<in> CofGroups.Ex1
[PROOF STEP]
using closed_comp and f_1_Ex1 and g_1_Ex1
[PROOF STATE]
proof (prove)
using this:
?f \<in> CofGroups.Ex1 \<and> ?g \<in> CofGroups.Ex1 \<Longrightarrow> ?f \<circ> ?g \<in> CofGroups.Ex1
f_1 \<in> CofGroups.Ex1
g_1 \<in> CofGroups.Ex1

goal (1 subgoal):
 1. f_1 \<circ> g_1 \<in> CofGroups.Ex1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f_1 \<circ> g_1 \<in> CofGroups.Ex1

goal (1 subgoal):
 1. f \<circ> g \<in> Ex2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f \<circ> g = CONJ (f_1 \<circ> g_1)
f_1 \<circ> g_1 \<in> CofGroups.Ex1
[PROOF STEP]
show "f \<circ> g \<in> Ex2"
[PROOF STATE]
proof (prove)
using this:
f \<circ> g = CONJ (f_1 \<circ> g_1)
f_1 \<circ> g_1 \<in> CofGroups.Ex1

goal (1 subgoal):
 1. f \<circ> g \<in> Ex2
[PROOF STEP]
using mem_Ex2_rule
[PROOF STATE]
proof (prove)
using this:
f \<circ> g = CONJ (f_1 \<circ> g_1)
f_1 \<circ> g_1 \<in> CofGroups.Ex1
(?f \<in> Ex2) = (\<exists>g. g \<in> CofGroups.Ex1 \<and> ?f = CONJ g)

goal (1 subgoal):
 1. f \<circ> g \<in> Ex2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<circ> g \<in> Ex2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj_tuple_replicate: "(\<And>i. i \<in> set bs \<Longrightarrow> \<not>i) \<Longrightarrow> length bs = length as \<Longrightarrow>
  proj_tuple bs as = replicate (length bs) None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. i \<in> set bs \<Longrightarrow> \<not> i; length bs = length as\<rbrakk> \<Longrightarrow> proj_tuple bs as = replicate (length bs) None
[PROOF STEP]
by (induction bs as rule: proj_tuple.induct) fastforce+


[STATEMENT]
lemma proj_tuple_join_mask_empty: "length as = n \<Longrightarrow>
  proj_tuple (join_mask n {}) as = replicate n None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length as = n \<Longrightarrow> proj_tuple (join_mask n {}) as = replicate n None
[PROOF STEP]
using proj_tuple_replicate[of "join_mask n {}"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>i. i \<in> set (join_mask n {}) \<Longrightarrow> \<not> i; length (join_mask n {}) = length ?as\<rbrakk> \<Longrightarrow> proj_tuple (join_mask n {}) ?as = replicate (length (join_mask n {})) None

goal (1 subgoal):
 1. length as = n \<Longrightarrow> proj_tuple (join_mask n {}) as = replicate n None
[PROOF STEP]
by (auto simp add: join_mask_def)


[STATEMENT]
lemma proj_tuple_alt: "proj_tuple bs as = map2 (\<lambda>b a. if b then a else None) bs as"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj_tuple bs as = map2 (\<lambda>x y. if x then y else None) bs as
[PROOF STEP]
by (induction bs as rule: proj_tuple.induct) auto


[STATEMENT]
lemma map2_map: "map2 f (map g [0..<length as]) as = map (\<lambda>i. f (g i) (as ! i)) [0..<length as]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map2 f (map g [0..<length as]) as = map (\<lambda>i. f (g i) (as ! i)) [0..<length as]
[PROOF STEP]
by (rule nth_equalityI) auto


[STATEMENT]
lemma proj_tuple_join_mask_restrict: "length as = n \<Longrightarrow>
  proj_tuple (join_mask n X) as = restrict X as"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length as = n \<Longrightarrow> proj_tuple (join_mask n X) as = restrict X as
[PROOF STEP]
by (auto simp add: restrict_def proj_tuple_alt join_mask_def map2_map)


[STATEMENT]
lemma wf_tuple_proj_idle:
  assumes wf: "wf_tuple n X as"
  shows "proj_tuple (join_mask n X) as = as"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj_tuple (join_mask n X) as = as
[PROOF STEP]
using proj_tuple_join_mask_restrict[of as n X, unfolded restrict_idle[OF wf]] wf
[PROOF STATE]
proof (prove)
using this:
length as = n \<Longrightarrow> proj_tuple (join_mask n X) as = as
wf_tuple n X as

goal (1 subgoal):
 1. proj_tuple (join_mask n X) as = as
[PROOF STEP]
by (auto simp add: wf_tuple_def)


[STATEMENT]
lemma wf_tuple_change_base:
  assumes wf: "wf_tuple n X as"
  and mask: "join_mask n X = join_mask n Y"
  shows "wf_tuple n Y as"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_tuple n Y as
[PROOF STEP]
using wf mask
[PROOF STATE]
proof (prove)
using this:
wf_tuple n X as
join_mask n X = join_mask n Y

goal (1 subgoal):
 1. wf_tuple n Y as
[PROOF STEP]
by (auto simp add: wf_tuple_def join_mask_def)


[STATEMENT]
lemma proj_tuple_in_join_mask_idle:
  assumes wf: "wf_tuple n X as"
  shows "proj_tuple_in_join pos (join_mask n X) as t \<longleftrightarrow> join_cond pos t as"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj_tuple_in_join pos (join_mask n X) as t = join_cond pos t as
[PROOF STEP]
using wf_tuple_proj_idle[OF wf]
[PROOF STATE]
proof (prove)
using this:
proj_tuple (join_mask n X) as = as

goal (1 subgoal):
 1. proj_tuple_in_join pos (join_mask n X) as t = join_cond pos t as
[PROOF STEP]
by (auto simp add: proj_tuple_in_join_def)


[STATEMENT]
lemma join_sub:
  assumes "L \<subseteq> R" "table n L t1" "table n R t2"
  shows "join t2 pos t1 = {as \<in> t2. proj_tuple_in_join pos (join_mask n L) as t1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. join t2 pos t1 = {as \<in> t2. proj_tuple_in_join pos (join_mask n L) as t1}
[PROOF STEP]
using assms proj_tuple_join_mask_restrict[of _ n L] join_restrict[of t2 n R t1 L pos]
    wf_tuple_length restrict_idle
[PROOF STATE]
proof (prove)
using this:
L \<subseteq> R
table n L t1
table n R t2
length ?as = n \<Longrightarrow> proj_tuple (join_mask n L) ?as = restrict L ?as
\<lbrakk>\<And>v. v \<in> t2 \<Longrightarrow> wf_tuple n R v; \<And>v. v \<in> t1 \<Longrightarrow> wf_tuple n L v; \<not> pos \<Longrightarrow> L \<subseteq> R\<rbrakk> \<Longrightarrow> (?v \<in> join t2 pos t1) = (wf_tuple n (R \<union> L) ?v \<and> restrict R ?v \<in> t2 \<and> join_cond pos t1 (restrict L ?v))
wf_tuple ?n ?V ?x \<Longrightarrow> length ?x = ?n
wf_tuple ?n ?A ?v \<Longrightarrow> restrict ?A ?v = ?v

goal (1 subgoal):
 1. join t2 pos t1 = {as \<in> t2. proj_tuple_in_join pos (join_mask n L) as t1}
[PROOF STEP]
by (auto simp add: table_def proj_tuple_in_join_def sup.absorb1) fastforce+


[STATEMENT]
lemma join_sub':
  assumes "R \<subseteq> L" "table n L t1" "table n R t2"
  shows "join t2 True t1 = {as \<in> t1. proj_tuple_in_join True (join_mask n R) as t2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. join t2 True t1 = {as \<in> t1. proj_tuple_in_join True (join_mask n R) as t2}
[PROOF STEP]
using assms proj_tuple_join_mask_restrict[of _ n R] join_restrict[of t2 n R t1 L True]
    wf_tuple_length restrict_idle
[PROOF STATE]
proof (prove)
using this:
R \<subseteq> L
table n L t1
table n R t2
length ?as = n \<Longrightarrow> proj_tuple (join_mask n R) ?as = restrict R ?as
\<lbrakk>\<And>v. v \<in> t2 \<Longrightarrow> wf_tuple n R v; \<And>v. v \<in> t1 \<Longrightarrow> wf_tuple n L v; \<not> True \<Longrightarrow> L \<subseteq> R\<rbrakk> \<Longrightarrow> (?v \<in> join t2 True t1) = (wf_tuple n (R \<union> L) ?v \<and> restrict R ?v \<in> t2 \<and> join_cond True t1 (restrict L ?v))
wf_tuple ?n ?V ?x \<Longrightarrow> length ?x = ?n
wf_tuple ?n ?A ?v \<Longrightarrow> restrict ?A ?v = ?v

goal (1 subgoal):
 1. join t2 True t1 = {as \<in> t1. proj_tuple_in_join True (join_mask n R) as t2}
[PROOF STEP]
by (auto simp add: table_def proj_tuple_in_join_def sup.absorb1 Un_absorb1) fastforce+


[STATEMENT]
lemma join_eq:
  assumes tab: "table n R t1" "table n R t2"
  shows "join t2 pos t1 = (if pos then t2 \<inter> t1 else t2 - t1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. join t2 pos t1 = (if pos then t2 \<inter> t1 else t2 - t1)
[PROOF STEP]
using join_sub[OF _ tab, of pos] tab(2) proj_tuple_in_join_mask_idle[of n R _ pos t1]
[PROOF STATE]
proof (prove)
using this:
R \<subseteq> R \<Longrightarrow> join t2 pos t1 = {as \<in> t2. proj_tuple_in_join pos (join_mask n R) as t1}
table n R t2
wf_tuple n R ?as \<Longrightarrow> proj_tuple_in_join pos (join_mask n R) ?as t1 = join_cond pos t1 ?as

goal (1 subgoal):
 1. join t2 pos t1 = (if pos then t2 \<inter> t1 else t2 - t1)
[PROOF STEP]
by (auto simp add: table_def)


[STATEMENT]
lemma join_no_cols:
  assumes tab: "table n {} t1" "table n R t2"
  shows "join t2 pos t1 = (if (pos \<longleftrightarrow> replicate n None \<in> t1) then t2 else {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. join t2 pos t1 = (if pos = (replicate n None \<in> t1) then t2 else {})
[PROOF STEP]
using join_sub[OF _ tab, of pos] tab(2)
[PROOF STATE]
proof (prove)
using this:
{} \<subseteq> R \<Longrightarrow> join t2 pos t1 = {as \<in> t2. proj_tuple_in_join pos (join_mask n {}) as t1}
table n R t2

goal (1 subgoal):
 1. join t2 pos t1 = (if pos = (replicate n None \<in> t1) then t2 else {})
[PROOF STEP]
by (auto simp add: table_def proj_tuple_in_join_def wf_tuple_length proj_tuple_join_mask_empty)


[STATEMENT]
lemma join_empty_left: "join {} pos t = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. join {} pos t = {}
[PROOF STEP]
by (auto simp add: join_def)


[STATEMENT]
lemma join_empty_right: "join t pos {} = (if pos then {} else t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. join t pos {} = (if pos then {} else t)
[PROOF STEP]
by (auto simp add: join_def)


[STATEMENT]
lemma bin_join_table:
  assumes tab: "table n A t" "table n A' t'"
  shows "bin_join n A t pos A' t' = join t pos t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_join n A t pos A' t' = join t pos t'
[PROOF STEP]
using assms join_empty_left[of pos t'] join_empty_right[of t pos]
    join_no_cols[OF _ assms(1), of t' pos] join_eq[of n A t' t pos] join_sub[OF _ assms(2,1)]
    join_sub'[OF _ assms(2,1)]
[PROOF STATE]
proof (prove)
using this:
table n A t
table n A' t'
join {} pos t' = {}
join t pos {} = (if pos then {} else t)
table n {} t' \<Longrightarrow> join t pos t' = (if pos = (replicate n None \<in> t') then t else {})
\<lbrakk>table n A t'; table n A t\<rbrakk> \<Longrightarrow> join t pos t' = (if pos then t \<inter> t' else t - t')
A' \<subseteq> A \<Longrightarrow> join t ?pos t' = {as \<in> t. proj_tuple_in_join ?pos (join_mask n A') as t'}
A \<subseteq> A' \<Longrightarrow> join t True t' = {as \<in> t'. proj_tuple_in_join True (join_mask n A) as t}

goal (1 subgoal):
 1. bin_join n A t pos A' t' = join t pos t'
[PROOF STEP]
by auto+