[STATEMENT]
lemma stereographic_inv_stereographic [simp]:
  shows "stereographic (inv_stereographic w) = w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stereographic (inv_stereographic w) = w
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stereographic (inv_stereographic w) = w
[PROOF STEP]
have "w = stereographic (inv_stereographic w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w = stereographic (inv_stereographic w)
[PROOF STEP]
proof (transfer, transfer)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. w \<noteq> vec_zero \<Longrightarrow> w \<approx>\<^sub>v stereographic_r3_cvec (inv_stereographic_cvec_r3 w)
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. w \<noteq> vec_zero \<Longrightarrow> w \<approx>\<^sub>v stereographic_r3_cvec (inv_stereographic_cvec_r3 w)
[PROOF STEP]
assume "w \<noteq> vec_zero"
[PROOF STATE]
proof (state)
this:
w \<noteq> vec_zero

goal (1 subgoal):
 1. \<And>w. w \<noteq> vec_zero \<Longrightarrow> w \<approx>\<^sub>v stereographic_r3_cvec (inv_stereographic_cvec_r3 w)
[PROOF STEP]
obtain w1 w2 where *: "w = (w1, w2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>w1 w2. w = (w1, w2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases w, auto)
[PROOF STATE]
proof (state)
this:
w = (w1, w2)

goal (1 subgoal):
 1. \<And>w. w \<noteq> vec_zero \<Longrightarrow> w \<approx>\<^sub>v stereographic_r3_cvec (inv_stereographic_cvec_r3 w)
[PROOF STEP]
obtain x y z where **: "inv_stereographic_cvec_r3 w = (x, y, z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y z. inv_stereographic_cvec_r3 w = (x, y, z) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "inv_stereographic_cvec_r3 w", blast)
[PROOF STATE]
proof (state)
this:
inv_stereographic_cvec_r3 w = (x, y, z)

goal (1 subgoal):
 1. \<And>w. w \<noteq> vec_zero \<Longrightarrow> w \<approx>\<^sub>v stereographic_r3_cvec (inv_stereographic_cvec_r3 w)
[PROOF STEP]
show "w \<approx>\<^sub>v stereographic_r3_cvec (inv_stereographic_cvec_r3 w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<approx>\<^sub>v stereographic_r3_cvec (inv_stereographic_cvec_r3 w)
[PROOF STEP]
using \<open>w \<noteq> vec_zero\<close> stereographic_inv_stereographic'[of "w1/w2" w1 w2 x y z] * **
[PROOF STATE]
proof (prove)
using this:
w \<noteq> vec_zero
\<lbrakk>w1 / w2 = w1 / w2; w2 \<noteq> 0; x = Re (2 * (w1 / w2) / (1 + w1 / w2 * cnj (w1 / w2))); y = Im (2 * (w1 / w2) / (1 + w1 / w2 * cnj (w1 / w2))); z = ((cmod (w1 / w2))\<^sup>2 - 1) / (1 + (cmod (w1 / w2))\<^sup>2)\<rbrakk> \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> (cor x + \<i> * cor y, cor (1 - z)) = k *\<^sub>s\<^sub>v (w1, w2)
w = (w1, w2)
inv_stereographic_cvec_r3 w = (x, y, z)

goal (1 subgoal):
 1. w \<approx>\<^sub>v stereographic_r3_cvec (inv_stereographic_cvec_r3 w)
[PROOF STEP]
by (auto simp add: split_def Let_def split: if_split_asm)
[PROOF STATE]
proof (state)
this:
w \<approx>\<^sub>v stereographic_r3_cvec (inv_stereographic_cvec_r3 w)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
w = stereographic (inv_stereographic w)

goal (1 subgoal):
 1. stereographic (inv_stereographic w) = w
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
w = stereographic (inv_stereographic w)

goal (1 subgoal):
 1. stereographic (inv_stereographic w) = w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
stereographic (inv_stereographic w) = w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_stereographic:
  shows "bij stereographic"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij stereographic
[PROOF STEP]
unfolding bij_def inj_on_def surj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>UNIV. \<forall>y\<in>UNIV. stereographic x = stereographic y \<longrightarrow> x = y) \<and> (\<forall>y. \<exists>x. y = stereographic x)
[PROOF STEP]
proof (safe)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; stereographic x = stereographic y\<rbrakk> \<Longrightarrow> x = y
 2. \<And>y. \<exists>x. y = stereographic x
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; stereographic x = stereographic y\<rbrakk> \<Longrightarrow> x = y
 2. \<And>y. \<exists>x. y = stereographic x
[PROOF STEP]
assume "stereographic a = stereographic b"
[PROOF STATE]
proof (state)
this:
stereographic a = stereographic b

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV; stereographic x = stereographic y\<rbrakk> \<Longrightarrow> x = y
 2. \<And>y. \<exists>x. y = stereographic x
[PROOF STEP]
thus "a = b"
[PROOF STATE]
proof (prove)
using this:
stereographic a = stereographic b

goal (1 subgoal):
 1. a = b
[PROOF STEP]
proof (transfer, transfer)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>a \<in> unit_sphere; b \<in> unit_sphere; stereographic_r3_cvec a \<approx>\<^sub>v stereographic_r3_cvec b; aa \<in> unit_sphere; ba \<in> unit_sphere; stereographic_r3_hcoords aa \<approx> stereographic_r3_hcoords ba\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
fix a b :: R3
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>a \<in> unit_sphere; b \<in> unit_sphere; stereographic_r3_cvec a \<approx>\<^sub>v stereographic_r3_cvec b; aa \<in> unit_sphere; ba \<in> unit_sphere; stereographic_r3_hcoords aa \<approx> stereographic_r3_hcoords ba\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
obtain xa ya za xb yb zb where
      *: "a = (xa, ya, za)" "b = (xb, yb, zb)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xa ya za xb yb zb. \<lbrakk>a = (xa, ya, za); b = (xb, yb, zb)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases a, cases b, auto)
[PROOF STATE]
proof (state)
this:
a = (xa, ya, za)
b = (xb, yb, zb)

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>a \<in> unit_sphere; b \<in> unit_sphere; stereographic_r3_cvec a \<approx>\<^sub>v stereographic_r3_cvec b; aa \<in> unit_sphere; ba \<in> unit_sphere; stereographic_r3_hcoords aa \<approx> stereographic_r3_hcoords ba\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
assume **: "a \<in> unit_sphere" "b \<in> unit_sphere" "stereographic_r3_cvec a \<approx>\<^sub>v stereographic_r3_cvec b"
[PROOF STATE]
proof (state)
this:
a \<in> unit_sphere
b \<in> unit_sphere
stereographic_r3_cvec a \<approx>\<^sub>v stereographic_r3_cvec b

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>a \<in> unit_sphere; b \<in> unit_sphere; stereographic_r3_cvec a \<approx>\<^sub>v stereographic_r3_cvec b; aa \<in> unit_sphere; ba \<in> unit_sphere; stereographic_r3_hcoords aa \<approx> stereographic_r3_hcoords ba\<rbrakk> \<Longrightarrow> a = b
[PROOF STEP]
show "a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = b
[PROOF STEP]
proof (cases "a = (0, 0, 1) \<or> b = (0, 0, 1)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = (0, 0, 1) \<or> b = (0, 0, 1) \<Longrightarrow> a = b
 2. \<not> (a = (0, 0, 1) \<or> b = (0, 0, 1)) \<Longrightarrow> a = b
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a = (0, 0, 1) \<or> b = (0, 0, 1)

goal (2 subgoals):
 1. a = (0, 0, 1) \<or> b = (0, 0, 1) \<Longrightarrow> a = b
 2. \<not> (a = (0, 0, 1) \<or> b = (0, 0, 1)) \<Longrightarrow> a = b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a = (0, 0, 1) \<or> b = (0, 0, 1)

goal (1 subgoal):
 1. a = b
[PROOF STEP]
using * **
[PROOF STATE]
proof (prove)
using this:
a = (0, 0, 1) \<or> b = (0, 0, 1)
a = (xa, ya, za)
b = (xb, yb, zb)
a \<in> unit_sphere
b \<in> unit_sphere
stereographic_r3_cvec a \<approx>\<^sub>v stereographic_r3_cvec b

goal (1 subgoal):
 1. a = b
[PROOF STEP]
by (simp split: if_split_asm) force+
[PROOF STATE]
proof (state)
this:
a = b

goal (1 subgoal):
 1. \<not> (a = (0, 0, 1) \<or> b = (0, 0, 1)) \<Longrightarrow> a = b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (a = (0, 0, 1) \<or> b = (0, 0, 1)) \<Longrightarrow> a = b
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (a = (0, 0, 1) \<or> b = (0, 0, 1))

goal (1 subgoal):
 1. \<not> (a = (0, 0, 1) \<or> b = (0, 0, 1)) \<Longrightarrow> a = b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (a = (0, 0, 1) \<or> b = (0, 0, 1))
[PROOF STEP]
obtain k where ++: "k \<noteq> 0" "cor xb + \<i> * cor yb = k * (cor xa + \<i> * cor ya)" "1 - cor zb = k * (1 - cor za)"
[PROOF STATE]
proof (prove)
using this:
\<not> (a = (0, 0, 1) \<or> b = (0, 0, 1))

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k \<noteq> 0; cor xb + \<i> * cor yb = k * (cor xa + \<i> * cor ya); 1 - cor zb = k * (1 - cor za)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using * **
[PROOF STATE]
proof (prove)
using this:
\<not> (a = (0, 0, 1) \<or> b = (0, 0, 1))
a = (xa, ya, za)
b = (xb, yb, zb)
a \<in> unit_sphere
b \<in> unit_sphere
stereographic_r3_cvec a \<approx>\<^sub>v stereographic_r3_cvec b

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k \<noteq> 0; cor xb + \<i> * cor yb = k * (cor xa + \<i> * cor ya); 1 - cor zb = k * (1 - cor za)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto split: if_split_asm)
[PROOF STATE]
proof (state)
this:
k \<noteq> 0
cor xb + \<i> * cor yb = k * (cor xa + \<i> * cor ya)
1 - cor zb = k * (1 - cor za)

goal (1 subgoal):
 1. \<not> (a = (0, 0, 1) \<or> b = (0, 0, 1)) \<Longrightarrow> a = b
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
k \<noteq> 0
cor xb + \<i> * cor yb = k * (cor xa + \<i> * cor ya)
1 - cor zb = k * (1 - cor za)

goal (1 subgoal):
 1. \<not> (a = (0, 0, 1) \<or> b = (0, 0, 1)) \<Longrightarrow> a = b
[PROOF STEP]
assume "xb + xa*zb = xa + xb*za"
                 "yb + ya*zb = ya + yb*za"
                 "xa*xa + ya*ya + za*za = 1" "xb*xb + yb*yb + zb*zb = 1"
                 "za \<noteq> 1" "zb \<noteq> 1"
[PROOF STATE]
proof (state)
this:
xb + xa * zb = xa + xb * za
yb + ya * zb = ya + yb * za
xa * xa + ya * ya + za * za = 1
xb * xb + yb * yb + zb * zb = 1
za \<noteq> 1
zb \<noteq> 1

goal (1 subgoal):
 1. \<not> (a = (0, 0, 1) \<or> b = (0, 0, 1)) \<Longrightarrow> a = b
[PROOF STEP]
hence "xa = xb \<and> ya = yb \<and> za = zb"
[PROOF STATE]
proof (prove)
using this:
xb + xa * zb = xa + xb * za
yb + ya * zb = ya + yb * za
xa * xa + ya * ya + za * za = 1
xb * xb + yb * yb + zb * zb = 1
za \<noteq> 1
zb \<noteq> 1

goal (1 subgoal):
 1. xa = xb \<and> ya = yb \<and> za = zb
[PROOF STEP]
by algebra
[PROOF STATE]
proof (state)
this:
xa = xb \<and> ya = yb \<and> za = zb

goal (1 subgoal):
 1. \<not> (a = (0, 0, 1) \<or> b = (0, 0, 1)) \<Longrightarrow> a = b
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>xb + xa * zb = xa + xb * za; yb + ya * zb = ya + yb * za; xa * xa + ya * ya + za * za = 1; xb * xb + yb * yb + zb * zb = 1; za \<noteq> 1; zb \<noteq> 1\<rbrakk> \<Longrightarrow> xa = xb \<and> ya = yb \<and> za = zb

goal (1 subgoal):
 1. \<not> (a = (0, 0, 1) \<or> b = (0, 0, 1)) \<Longrightarrow> a = b
[PROOF STEP]
note *** = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>xb + xa * zb = xa + xb * za; yb + ya * zb = ya + yb * za; xa * xa + ya * ya + za * za = 1; xb * xb + yb * yb + zb * zb = 1; za \<noteq> 1; zb \<noteq> 1\<rbrakk> \<Longrightarrow> xa = xb \<and> ya = yb \<and> za = zb

goal (1 subgoal):
 1. \<not> (a = (0, 0, 1) \<or> b = (0, 0, 1)) \<Longrightarrow> a = b
[PROOF STEP]
have "za \<noteq> 1" "zb \<noteq> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. za \<noteq> 1 &&& zb \<noteq> 1
[PROOF STEP]
using False * **
[PROOF STATE]
proof (prove)
using this:
\<not> (a = (0, 0, 1) \<or> b = (0, 0, 1))
a = (xa, ya, za)
b = (xb, yb, zb)
a \<in> unit_sphere
b \<in> unit_sphere
stereographic_r3_cvec a \<approx>\<^sub>v stereographic_r3_cvec b

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

goal (1 subgoal):
 1. \<not> (a = (0, 0, 1) \<or> b = (0, 0, 1)) \<Longrightarrow> a = b
[PROOF STEP]
have "k = (1 - cor zb) / (1 - cor za)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k = (1 - cor zb) / (1 - cor za)
[PROOF STEP]
using \<open>1 - cor zb = k * (1 - cor za)\<close> \<open>za \<noteq> 1\<close>
[PROOF STATE]
proof (prove)
using this:
1 - cor zb = k * (1 - cor za)
za \<noteq> 1

goal (1 subgoal):
 1. k = (1 - cor zb) / (1 - cor za)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k = (1 - cor zb) / (1 - cor za)

goal (1 subgoal):
 1. \<not> (a = (0, 0, 1) \<or> b = (0, 0, 1)) \<Longrightarrow> a = b
[PROOF STEP]
hence "(1 - cor za) * (cor xb + \<i> * cor yb) = (1 - cor zb) * (cor xa + \<i> * cor ya)"
[PROOF STATE]
proof (prove)
using this:
k = (1 - cor zb) / (1 - cor za)

goal (1 subgoal):
 1. (1 - cor za) * (cor xb + \<i> * cor yb) = (1 - cor zb) * (cor xa + \<i> * cor ya)
[PROOF STEP]
using \<open>za \<noteq> 1\<close> ++(2)
[PROOF STATE]
proof (prove)
using this:
k = (1 - cor zb) / (1 - cor za)
za \<noteq> 1
cor xb + \<i> * cor yb = k * (cor xa + \<i> * cor ya)

goal (1 subgoal):
 1. (1 - cor za) * (cor xb + \<i> * cor yb) = (1 - cor zb) * (cor xa + \<i> * cor ya)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(1 - cor za) * (cor xb + \<i> * cor yb) = (1 - cor zb) * (cor xa + \<i> * cor ya)

goal (1 subgoal):
 1. \<not> (a = (0, 0, 1) \<or> b = (0, 0, 1)) \<Longrightarrow> a = b
[PROOF STEP]
hence "xb + xa*zb = xa + xb*za"
            "yb + ya*zb = ya + yb*za"
            "xa*xa + ya*ya + za*za = 1" "xb*xb + yb*yb + zb*zb = 1"
[PROOF STATE]
proof (prove)
using this:
(1 - cor za) * (cor xb + \<i> * cor yb) = (1 - cor zb) * (cor xa + \<i> * cor ya)

goal (1 subgoal):
 1. (xb + xa * zb = xa + xb * za &&& yb + ya * zb = ya + yb * za) &&& xa * xa + ya * ya + za * za = 1 &&& xb * xb + yb * yb + zb * zb = 1
[PROOF STEP]
using * ** \<open>za \<noteq> 1\<close>
[PROOF STATE]
proof (prove)
using this:
(1 - cor za) * (cor xb + \<i> * cor yb) = (1 - cor zb) * (cor xa + \<i> * cor ya)
a = (xa, ya, za)
b = (xb, yb, zb)
a \<in> unit_sphere
b \<in> unit_sphere
stereographic_r3_cvec a \<approx>\<^sub>v stereographic_r3_cvec b
za \<noteq> 1

goal (1 subgoal):
 1. (xb + xa * zb = xa + xb * za &&& yb + ya * zb = ya + yb * za) &&& xa * xa + ya * ya + za * za = 1 &&& xb * xb + yb * yb + zb * zb = 1
[PROOF STEP]
apply (simp_all add: field_simps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cor xb + (\<i> * cor yb + (cor xa * cor zb + \<i> * (cor ya * cor zb))) = cor xa + (\<i> * cor ya + (cor xb * cor za + \<i> * (cor yb * cor za))); a = (xa, ya, za); b = (xb, yb, zb); xa * xa + (ya * ya + za * za) = 1; xb * xb + (yb * yb + zb * zb) = 1; \<exists>k. k \<noteq> 0 \<and> (if yb = 0 \<longrightarrow> xb = 0 \<longrightarrow> zb \<noteq> 1 then (cor xb + \<i> * cor yb, cor (1 - zb)) else (1, 0)) = (k * cor xa + k * (\<i> * cor ya), k - k * cor za); za \<noteq> 1\<rbrakk> \<Longrightarrow> xb + xa * zb = xa + xb * za
 2. \<lbrakk>cor xb + (\<i> * cor yb + (cor xa * cor zb + \<i> * (cor ya * cor zb))) = cor xa + (\<i> * cor ya + (cor xb * cor za + \<i> * (cor yb * cor za))); a = (xa, ya, za); b = (xb, yb, zb); xa * xa + (ya * ya + za * za) = 1; xb * xb + (yb * yb + zb * zb) = 1; \<exists>k. k \<noteq> 0 \<and> (if yb = 0 \<longrightarrow> xb = 0 \<longrightarrow> zb \<noteq> 1 then (cor xb + \<i> * cor yb, cor (1 - zb)) else (1, 0)) = (k * cor xa + k * (\<i> * cor ya), k - k * cor za); za \<noteq> 1\<rbrakk> \<Longrightarrow> yb + ya * zb = ya + yb * za
[PROOF STEP]
unfolding complex_of_real_def imaginary_unit.ctr
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Complex xb 0 + (Complex 0 1 * Complex yb 0 + (Complex xa 0 * Complex zb 0 + Complex 0 1 * (Complex ya 0 * Complex zb 0))) = Complex xa 0 + (Complex 0 1 * Complex ya 0 + (Complex xb 0 * Complex za 0 + Complex 0 1 * (Complex yb 0 * Complex za 0))); a = (xa, ya, za); b = (xb, yb, zb); xa * xa + (ya * ya + za * za) = 1; xb * xb + (yb * yb + zb * zb) = 1; \<exists>k. k \<noteq> 0 \<and> (if yb = 0 \<longrightarrow> xb = 0 \<longrightarrow> zb \<noteq> 1 then (Complex xb 0 + Complex 0 1 * Complex yb 0, Complex (1 - zb) 0) else (1, 0)) = (k * Complex xa 0 + k * (Complex 0 1 * Complex ya 0), k - k * Complex za 0); za \<noteq> 1\<rbrakk> \<Longrightarrow> xb + xa * zb = xa + xb * za
 2. \<lbrakk>Complex xb 0 + (Complex 0 1 * Complex yb 0 + (Complex xa 0 * Complex zb 0 + Complex 0 1 * (Complex ya 0 * Complex zb 0))) = Complex xa 0 + (Complex 0 1 * Complex ya 0 + (Complex xb 0 * Complex za 0 + Complex 0 1 * (Complex yb 0 * Complex za 0))); a = (xa, ya, za); b = (xb, yb, zb); xa * xa + (ya * ya + za * za) = 1; xb * xb + (yb * yb + zb * zb) = 1; \<exists>k. k \<noteq> 0 \<and> (if yb = 0 \<longrightarrow> xb = 0 \<longrightarrow> zb \<noteq> 1 then (Complex xb 0 + Complex 0 1 * Complex yb 0, Complex (1 - zb) 0) else (1, 0)) = (k * Complex xa 0 + k * (Complex 0 1 * Complex ya 0), k - k * Complex za 0); za \<noteq> 1\<rbrakk> \<Longrightarrow> yb + ya * zb = ya + yb * za
[PROOF STEP]
by (simp_all add: legacy_Complex_simps)
[PROOF STATE]
proof (state)
this:
xb + xa * zb = xa + xb * za
yb + ya * zb = ya + yb * za
xa * xa + ya * ya + za * za = 1
xb * xb + yb * yb + zb * zb = 1

goal (1 subgoal):
 1. \<not> (a = (0, 0, 1) \<or> b = (0, 0, 1)) \<Longrightarrow> a = b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
xb + xa * zb = xa + xb * za
yb + ya * zb = ya + yb * za
xa * xa + ya * ya + za * za = 1
xb * xb + yb * yb + zb * zb = 1

goal (1 subgoal):
 1. a = b
[PROOF STEP]
using * ** *** \<open>za \<noteq> 1\<close> \<open>zb \<noteq> 1\<close>
[PROOF STATE]
proof (prove)
using this:
xb + xa * zb = xa + xb * za
yb + ya * zb = ya + yb * za
xa * xa + ya * ya + za * za = 1
xb * xb + yb * yb + zb * zb = 1
a = (xa, ya, za)
b = (xb, yb, zb)
a \<in> unit_sphere
b \<in> unit_sphere
stereographic_r3_cvec a \<approx>\<^sub>v stereographic_r3_cvec b
\<lbrakk>xb + xa * zb = xa + xb * za; yb + ya * zb = ya + yb * za; xa * xa + ya * ya + za * za = 1; xb * xb + yb * yb + zb * zb = 1; za \<noteq> 1; zb \<noteq> 1\<rbrakk> \<Longrightarrow> xa = xb \<and> ya = yb \<and> za = zb
za \<noteq> 1
zb \<noteq> 1

goal (1 subgoal):
 1. a = b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a = b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
a = b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
a = b

goal (1 subgoal):
 1. \<And>y. \<exists>x. y = stereographic x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. \<exists>x. y = stereographic x
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. \<exists>x. y = stereographic x
[PROOF STEP]
show "\<exists> x. y = stereographic x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. y = stereographic x
[PROOF STEP]
by (rule_tac x="inv_stereographic y" in exI, simp)
[PROOF STATE]
proof (state)
this:
\<exists>x. y = stereographic x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inv_stereographic_stereographic [simp]:
  shows "inv_stereographic (stereographic x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_stereographic (stereographic x) = x
[PROOF STEP]
using stereographic_inv_stereographic[of "stereographic x"]
[PROOF STATE]
proof (prove)
using this:
stereographic (inv_stereographic (stereographic x)) = stereographic x

goal (1 subgoal):
 1. inv_stereographic (stereographic x) = x
[PROOF STEP]
using bij_stereographic
[PROOF STATE]
proof (prove)
using this:
stereographic (inv_stereographic (stereographic x)) = stereographic x
bij stereographic

goal (1 subgoal):
 1. inv_stereographic (stereographic x) = x
[PROOF STEP]
unfolding bij_def inj_on_def
[PROOF STATE]
proof (prove)
using this:
stereographic (inv_stereographic (stereographic x)) = stereographic x
(\<forall>x\<in>UNIV. \<forall>y\<in>UNIV. stereographic x = stereographic y \<longrightarrow> x = y) \<and> surj stereographic

goal (1 subgoal):
 1. inv_stereographic (stereographic x) = x
[PROOF STEP]
by simp


[STATEMENT]
lemma inv_stereographic_is_inv:
  shows "inv_stereographic = inv stereographic"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_stereographic = inv stereographic
[PROOF STEP]
by (rule inv_equality[symmetric], simp_all)


[STATEMENT]
lemma mult_sv_one [simp]:
  shows "1 *\<^sub>s\<^sub>v\<^sub>4 x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 *\<^sub>s\<^sub>v\<^sub>4 x = x
[PROOF STEP]
by (cases x) simp


[STATEMENT]
lemma mult_sv_distb [simp]:
  shows "x *\<^sub>s\<^sub>v\<^sub>4 (y *\<^sub>s\<^sub>v\<^sub>4 v) = (x*y) *\<^sub>s\<^sub>v\<^sub>4 v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x *\<^sub>s\<^sub>v\<^sub>4 (y *\<^sub>s\<^sub>v\<^sub>4 v) = (x * y) *\<^sub>s\<^sub>v\<^sub>4 v
[PROOF STEP]
by (cases v) simp


[STATEMENT]
lemma stereographic_circline_inv_stereographic_circline:
  shows "stereographic_circline \<circ> inv_stereographic_circline = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stereographic_circline \<circ> inv_stereographic_circline = id
[PROOF STEP]
proof (rule ext, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. stereographic_circline (inv_stereographic_circline x) = x
[PROOF STEP]
fix H
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. stereographic_circline (inv_stereographic_circline x) = x
[PROOF STEP]
show "stereographic_circline (inv_stereographic_circline H) = H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stereographic_circline (inv_stereographic_circline H) = H
[PROOF STEP]
proof (transfer, transfer)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>H. hermitean H \<and> H \<noteq> mat_zero \<Longrightarrow> circline_eq_cmat (stereographic_circline_r4_cmat (inv_stereographic_circline_cmat_r4 H)) H
[PROOF STEP]
fix H
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>H. hermitean H \<and> H \<noteq> mat_zero \<Longrightarrow> circline_eq_cmat (stereographic_circline_r4_cmat (inv_stereographic_circline_cmat_r4 H)) H
[PROOF STEP]
assume hh: "hermitean H \<and> H \<noteq> mat_zero"
[PROOF STATE]
proof (state)
this:
hermitean H \<and> H \<noteq> mat_zero

goal (1 subgoal):
 1. \<And>H. hermitean H \<and> H \<noteq> mat_zero \<Longrightarrow> circline_eq_cmat (stereographic_circline_r4_cmat (inv_stereographic_circline_cmat_r4 H)) H
[PROOF STEP]
obtain A B C D where HH: "H = (A, B, C, D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A B C D. H = (A, B, C, D) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "H") auto
[PROOF STATE]
proof (state)
this:
H = (A, B, C, D)

goal (1 subgoal):
 1. \<And>H. hermitean H \<and> H \<noteq> mat_zero \<Longrightarrow> circline_eq_cmat (stereographic_circline_r4_cmat (inv_stereographic_circline_cmat_r4 H)) H
[PROOF STEP]
have "is_real A" "is_real D" "C = cnj B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_real A &&& is_real D &&& C = cnj B
[PROOF STEP]
using HH hh hermitean_elems[of A B C D]
[PROOF STATE]
proof (prove)
using this:
H = (A, B, C, D)
hermitean H \<and> H \<noteq> mat_zero
hermitean (A, B, C, D) \<Longrightarrow> is_real A
hermitean (A, B, C, D) \<Longrightarrow> is_real D
hermitean (A, B, C, D) \<Longrightarrow> B = cnj C
hermitean (A, B, C, D) \<Longrightarrow> cnj B = C

goal (1 subgoal):
 1. is_real A &&& is_real D &&& C = cnj B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_real A
is_real D
C = cnj B

goal (1 subgoal):
 1. \<And>H. hermitean H \<and> H \<noteq> mat_zero \<Longrightarrow> circline_eq_cmat (stereographic_circline_r4_cmat (inv_stereographic_circline_cmat_r4 H)) H
[PROOF STEP]
thus "circline_eq_cmat (stereographic_circline_r4_cmat (inv_stereographic_circline_cmat_r4 H)) H"
[PROOF STATE]
proof (prove)
using this:
is_real A
is_real D
C = cnj B

goal (1 subgoal):
 1. circline_eq_cmat (stereographic_circline_r4_cmat (inv_stereographic_circline_cmat_r4 H)) H
[PROOF STEP]
using HH
[PROOF STATE]
proof (prove)
using this:
is_real A
is_real D
C = cnj B
H = (A, B, C, D)

goal (1 subgoal):
 1. circline_eq_cmat (stereographic_circline_r4_cmat (inv_stereographic_circline_cmat_r4 H)) H
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_real A; is_real D; C = cnj B; H = (A, B, cnj B, D)\<rbrakk> \<Longrightarrow> \<exists>k. k \<noteq> 0 \<and> (A = 0 \<or> k = 1) \<and> B * 2 = cor k * (2 * cor (Re B) + \<i> * (2 * cor (Im B))) \<and> cnj B * 2 = cor k * (2 * cor (Re B) - \<i> * (2 * cor (Im B))) \<and> (D = 0 \<or> k = 1)
[PROOF STEP]
apply (rule_tac x=1 in exI, cases B)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>is_real A; is_real D; C = cnj B; H = (A, B, cnj B, D); B = Complex x1 x2\<rbrakk> \<Longrightarrow> 1 \<noteq> 0 \<and> (A = 0 \<or> 1 = 1) \<and> B * 2 = cor 1 * (2 * cor (Re B) + \<i> * (2 * cor (Im B))) \<and> cnj B * 2 = cor 1 * (2 * cor (Re B) - \<i> * (2 * cor (Im B))) \<and> (D = 0 \<or> 1 = 1)
[PROOF STEP]
by (smt add_uminus_conv_diff complex_cnj_add complex_cnj_complex_of_real complex_cnj_i complex_cnj_mult complex_cnj_one complex_eq distrib_left_numeral mult.commute mult.left_commute mult.left_neutral mult_cancel_right2 mult_minus_left of_real_1 one_add_one)
[PROOF STATE]
proof (state)
this:
circline_eq_cmat (stereographic_circline_r4_cmat (inv_stereographic_circline_cmat_r4 H)) H

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
stereographic_circline (inv_stereographic_circline H) = H

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inv_stereographic_circline_stereographic_circline:
  "inv_stereographic_circline \<circ> stereographic_circline = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_stereographic_circline \<circ> stereographic_circline = id
[PROOF STEP]
proof (rule ext, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. inv_stereographic_circline (stereographic_circline x) = x
[PROOF STEP]
fix \<alpha>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. inv_stereographic_circline (stereographic_circline x) = x
[PROOF STEP]
show "inv_stereographic_circline (stereographic_circline \<alpha>) = \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_stereographic_circline (stereographic_circline \<alpha>) = \<alpha>
[PROOF STEP]
proof (transfer, transfer)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<alpha>. \<alpha> \<in> plane_vectors \<Longrightarrow> plane_vec_eq_r4 (inv_stereographic_circline_cmat_r4 (stereographic_circline_r4_cmat \<alpha>)) \<alpha>
[PROOF STEP]
fix \<alpha>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<alpha>. \<alpha> \<in> plane_vectors \<Longrightarrow> plane_vec_eq_r4 (inv_stereographic_circline_cmat_r4 (stereographic_circline_r4_cmat \<alpha>)) \<alpha>
[PROOF STEP]
assume aa: "\<alpha> \<in> plane_vectors"
[PROOF STATE]
proof (state)
this:
\<alpha> \<in> plane_vectors

goal (1 subgoal):
 1. \<And>\<alpha>. \<alpha> \<in> plane_vectors \<Longrightarrow> plane_vec_eq_r4 (inv_stereographic_circline_cmat_r4 (stereographic_circline_r4_cmat \<alpha>)) \<alpha>
[PROOF STEP]
obtain a b c d where AA: "\<alpha> = (a, b, c, d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b c d. \<alpha> = (a, b, c, d) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "\<alpha>") auto
[PROOF STATE]
proof (state)
this:
\<alpha> = (a, b, c, d)

goal (1 subgoal):
 1. \<And>\<alpha>. \<alpha> \<in> plane_vectors \<Longrightarrow> plane_vec_eq_r4 (inv_stereographic_circline_cmat_r4 (stereographic_circline_r4_cmat \<alpha>)) \<alpha>
[PROOF STEP]
thus "plane_vec_eq_r4 (inv_stereographic_circline_cmat_r4 (stereographic_circline_r4_cmat \<alpha>)) \<alpha>"
[PROOF STATE]
proof (prove)
using this:
\<alpha> = (a, b, c, d)

goal (1 subgoal):
 1. plane_vec_eq_r4 (inv_stereographic_circline_cmat_r4 (stereographic_circline_r4_cmat \<alpha>)) \<alpha>
[PROOF STEP]
using AA
[PROOF STATE]
proof (prove)
using this:
\<alpha> = (a, b, c, d)
\<alpha> = (a, b, c, d)

goal (1 subgoal):
 1. plane_vec_eq_r4 (inv_stereographic_circline_cmat_r4 (stereographic_circline_r4_cmat \<alpha>)) \<alpha>
[PROOF STEP]
by simp (rule_tac x=1 in exI, auto simp add: field_simps complex_of_real_def)
[PROOF STATE]
proof (state)
this:
plane_vec_eq_r4 (inv_stereographic_circline_cmat_r4 (stereographic_circline_r4_cmat \<alpha>)) \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inv_stereographic_circline (stereographic_circline \<alpha>) = \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stereographic_sphere_circle_set'':
  shows "on_sphere_circle (inv_stereographic_circline H) z \<longleftrightarrow>
         on_circline H (stereographic z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. on_sphere_circle (inv_stereographic_circline H) z = on_circline H (stereographic z)
[PROOF STEP]
proof (transfer, transfer)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>H z. \<lbrakk>hermitean H \<and> H \<noteq> mat_zero; z \<in> unit_sphere\<rbrakk> \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) z = on_circline_cmat_cvec H (stereographic_r3_cvec z)
[PROOF STEP]
fix M :: R3 and H :: complex_mat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>H z. \<lbrakk>hermitean H \<and> H \<noteq> mat_zero; z \<in> unit_sphere\<rbrakk> \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) z = on_circline_cmat_cvec H (stereographic_r3_cvec z)
[PROOF STEP]
assume hh: "hermitean H \<and> H \<noteq> mat_zero" "M \<in> unit_sphere"
[PROOF STATE]
proof (state)
this:
hermitean H \<and> H \<noteq> mat_zero
M \<in> unit_sphere

goal (1 subgoal):
 1. \<And>H z. \<lbrakk>hermitean H \<and> H \<noteq> mat_zero; z \<in> unit_sphere\<rbrakk> \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) z = on_circline_cmat_cvec H (stereographic_r3_cvec z)
[PROOF STEP]
obtain A B C D where HH: "H = (A, B, C, D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A B C D. H = (A, B, C, D) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "H") auto
[PROOF STATE]
proof (state)
this:
H = (A, B, C, D)

goal (1 subgoal):
 1. \<And>H z. \<lbrakk>hermitean H \<and> H \<noteq> mat_zero; z \<in> unit_sphere\<rbrakk> \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) z = on_circline_cmat_cvec H (stereographic_r3_cvec z)
[PROOF STEP]
have *: "is_real A" "is_real D" "C = cnj B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_real A &&& is_real D &&& C = cnj B
[PROOF STEP]
using hh HH hermitean_elems[of A B C D]
[PROOF STATE]
proof (prove)
using this:
hermitean H \<and> H \<noteq> mat_zero
M \<in> unit_sphere
H = (A, B, C, D)
hermitean (A, B, C, D) \<Longrightarrow> is_real A
hermitean (A, B, C, D) \<Longrightarrow> is_real D
hermitean (A, B, C, D) \<Longrightarrow> B = cnj C
hermitean (A, B, C, D) \<Longrightarrow> cnj B = C

goal (1 subgoal):
 1. is_real A &&& is_real D &&& C = cnj B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_real A
is_real D
C = cnj B

goal (1 subgoal):
 1. \<And>H z. \<lbrakk>hermitean H \<and> H \<noteq> mat_zero; z \<in> unit_sphere\<rbrakk> \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) z = on_circline_cmat_cvec H (stereographic_r3_cvec z)
[PROOF STEP]
obtain x y z where MM: "M = (x, y, z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y z. M = (x, y, z) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "M") auto
[PROOF STATE]
proof (state)
this:
M = (x, y, z)

goal (1 subgoal):
 1. \<And>H z. \<lbrakk>hermitean H \<and> H \<noteq> mat_zero; z \<in> unit_sphere\<rbrakk> \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) z = on_circline_cmat_cvec H (stereographic_r3_cvec z)
[PROOF STEP]
show "on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M \<longleftrightarrow>
        on_circline_cmat_cvec H (stereographic_r3_cvec M)" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M = on_circline_cmat_cvec H (stereographic_r3_cvec M)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M \<Longrightarrow> on_circline_cmat_cvec H (stereographic_r3_cvec M)
 2. on_circline_cmat_cvec H (stereographic_r3_cvec M) \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M

goal (2 subgoals):
 1. on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M \<Longrightarrow> on_circline_cmat_cvec H (stereographic_r3_cvec M)
 2. on_circline_cmat_cvec H (stereographic_r3_cvec M) \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. on_circline_cmat_cvec H (stereographic_r3_cvec M)
[PROOF STEP]
proof (cases "z=1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z = 1 \<Longrightarrow> on_circline_cmat_cvec H (stereographic_r3_cvec M)
 2. z \<noteq> 1 \<Longrightarrow> on_circline_cmat_cvec H (stereographic_r3_cvec M)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
z = 1

goal (2 subgoals):
 1. z = 1 \<Longrightarrow> on_circline_cmat_cvec H (stereographic_r3_cvec M)
 2. z \<noteq> 1 \<Longrightarrow> on_circline_cmat_cvec H (stereographic_r3_cvec M)
[PROOF STEP]
hence "x = 0" "y = 0"
[PROOF STATE]
proof (prove)
using this:
z = 1

goal (1 subgoal):
 1. x = 0 &&& y = 0
[PROOF STEP]
using MM hh
[PROOF STATE]
proof (prove)
using this:
z = 1
M = (x, y, z)
hermitean H \<and> H \<noteq> mat_zero
M \<in> unit_sphere

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

goal (2 subgoals):
 1. z = 1 \<Longrightarrow> on_circline_cmat_cvec H (stereographic_r3_cvec M)
 2. z \<noteq> 1 \<Longrightarrow> on_circline_cmat_cvec H (stereographic_r3_cvec M)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x = 0
y = 0

goal (1 subgoal):
 1. on_circline_cmat_cvec H (stereographic_r3_cvec M)
[PROOF STEP]
using * \<open>?lhs\<close> HH MM \<open>z=1\<close>
[PROOF STATE]
proof (prove)
using this:
x = 0
y = 0
is_real A
is_real D
C = cnj B
on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
H = (A, B, C, D)
M = (x, y, z)
z = 1

goal (1 subgoal):
 1. on_circline_cmat_cvec H (stereographic_r3_cvec M)
[PROOF STEP]
by (cases A, simp add: vec_cnj_def Complex_eq Let_def)
[PROOF STATE]
proof (state)
this:
on_circline_cmat_cvec H (stereographic_r3_cvec M)

goal (1 subgoal):
 1. z \<noteq> 1 \<Longrightarrow> on_circline_cmat_cvec H (stereographic_r3_cvec M)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z \<noteq> 1 \<Longrightarrow> on_circline_cmat_cvec H (stereographic_r3_cvec M)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
z \<noteq> 1

goal (1 subgoal):
 1. z \<noteq> 1 \<Longrightarrow> on_circline_cmat_cvec H (stereographic_r3_cvec M)
[PROOF STEP]
hence "Re A*(1+z) + 2*Re B*x + 2*Im B*y + Re D*(1-z) = 0"
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 1

goal (1 subgoal):
 1. Re A * (1 + z) + 2 * Re B * x + 2 * Im B * y + Re D * (1 - z) = 0
[PROOF STEP]
using * \<open>?lhs\<close> HH MM
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 1
is_real A
is_real D
C = cnj B
on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
H = (A, B, C, D)
M = (x, y, z)

goal (1 subgoal):
 1. Re A * (1 + z) + 2 * Re B * x + 2 * Im B * y + Re D * (1 - z) = 0
[PROOF STEP]
by (simp add: Let_def field_simps)
[PROOF STATE]
proof (state)
this:
Re A * (1 + z) + 2 * Re B * x + 2 * Im B * y + Re D * (1 - z) = 0

goal (1 subgoal):
 1. z \<noteq> 1 \<Longrightarrow> on_circline_cmat_cvec H (stereographic_r3_cvec M)
[PROOF STEP]
hence "(Re A*(1+z) + 2*Re B*x + 2*Im B*y + Re D*(1-z))*(1-z) = 0"
[PROOF STATE]
proof (prove)
using this:
Re A * (1 + z) + 2 * Re B * x + 2 * Im B * y + Re D * (1 - z) = 0

goal (1 subgoal):
 1. (Re A * (1 + z) + 2 * Re B * x + 2 * Im B * y + Re D * (1 - z)) * (1 - z) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(Re A * (1 + z) + 2 * Re B * x + 2 * Im B * y + Re D * (1 - z)) * (1 - z) = 0

goal (1 subgoal):
 1. z \<noteq> 1 \<Longrightarrow> on_circline_cmat_cvec H (stereographic_r3_cvec M)
[PROOF STEP]
hence "Re A*(1+z)*(1-z) + 2*Re B*x*(1-z) + 2*Im B*y*(1-z) + Re D*(1-z)*(1-z) = 0"
[PROOF STATE]
proof (prove)
using this:
(Re A * (1 + z) + 2 * Re B * x + 2 * Im B * y + Re D * (1 - z)) * (1 - z) = 0

goal (1 subgoal):
 1. Re A * (1 + z) * (1 - z) + 2 * Re B * x * (1 - z) + 2 * Im B * y * (1 - z) + Re D * (1 - z) * (1 - z) = 0
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
Re A * (1 + z) * (1 - z) + 2 * Re B * x * (1 - z) + 2 * Im B * y * (1 - z) + Re D * (1 - z) * (1 - z) = 0

goal (1 subgoal):
 1. z \<noteq> 1 \<Longrightarrow> on_circline_cmat_cvec H (stereographic_r3_cvec M)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Re A * (1 + z) * (1 - z) + 2 * Re B * x * (1 - z) + 2 * Im B * y * (1 - z) + Re D * (1 - z) * (1 - z) = 0

goal (1 subgoal):
 1. z \<noteq> 1 \<Longrightarrow> on_circline_cmat_cvec H (stereographic_r3_cvec M)
[PROOF STEP]
have "x*x+y*y = (1+z)*(1-z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * x + y * y = (1 + z) * (1 - z)
[PROOF STEP]
using MM hh
[PROOF STATE]
proof (prove)
using this:
M = (x, y, z)
hermitean H \<and> H \<noteq> mat_zero
M \<in> unit_sphere

goal (1 subgoal):
 1. x * x + y * y = (1 + z) * (1 - z)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
x * x + y * y = (1 + z) * (1 - z)

goal (1 subgoal):
 1. z \<noteq> 1 \<Longrightarrow> on_circline_cmat_cvec H (stereographic_r3_cvec M)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Re A * (1 + z) * (1 - z) + 2 * Re B * x * (1 - z) + 2 * Im B * y * (1 - z) + Re D * (1 - z) * (1 - z) = 0
x * x + y * y = (1 + z) * (1 - z)
[PROOF STEP]
have "Re A*(x*x+y*y) + 2*Re B*x*(1-z) + 2*Im B*y*(1-z) + Re D*(1-z)*(1-z) = 0"
[PROOF STATE]
proof (prove)
using this:
Re A * (1 + z) * (1 - z) + 2 * Re B * x * (1 - z) + 2 * Im B * y * (1 - z) + Re D * (1 - z) * (1 - z) = 0
x * x + y * y = (1 + z) * (1 - z)

goal (1 subgoal):
 1. Re A * (x * x + y * y) + 2 * Re B * x * (1 - z) + 2 * Im B * y * (1 - z) + Re D * (1 - z) * (1 - z) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Re A * (x * x + y * y) + 2 * Re B * x * (1 - z) + 2 * Im B * y * (1 - z) + Re D * (1 - z) * (1 - z) = 0

goal (1 subgoal):
 1. z \<noteq> 1 \<Longrightarrow> on_circline_cmat_cvec H (stereographic_r3_cvec M)
[PROOF STEP]
hence "(x * Re A + (1 - z) * Re B) * x - (- (y * Re A) + - ((1 - z) * Im B)) * y + (x * Re B + y * Im B + (1 - z) * Re D) * (1 - z) = 0"
[PROOF STATE]
proof (prove)
using this:
Re A * (x * x + y * y) + 2 * Re B * x * (1 - z) + 2 * Im B * y * (1 - z) + Re D * (1 - z) * (1 - z) = 0

goal (1 subgoal):
 1. (x * Re A + (1 - z) * Re B) * x - (- (y * Re A) + - ((1 - z) * Im B)) * y + (x * Re B + y * Im B + (1 - z) * Re D) * (1 - z) = 0
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
(x * Re A + (1 - z) * Re B) * x - (- (y * Re A) + - ((1 - z) * Im B)) * y + (x * Re B + y * Im B + (1 - z) * Re D) * (1 - z) = 0

goal (1 subgoal):
 1. z \<noteq> 1 \<Longrightarrow> on_circline_cmat_cvec H (stereographic_r3_cvec M)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(x * Re A + (1 - z) * Re B) * x - (- (y * Re A) + - ((1 - z) * Im B)) * y + (x * Re B + y * Im B + (1 - z) * Re D) * (1 - z) = 0

goal (1 subgoal):
 1. on_circline_cmat_cvec H (stereographic_r3_cvec M)
[PROOF STEP]
using \<open>z \<noteq> 1\<close> HH MM * \<open>Re A*(1+z) + 2*Re B*x + 2*Im B*y + Re D*(1-z) = 0\<close>
[PROOF STATE]
proof (prove)
using this:
(x * Re A + (1 - z) * Re B) * x - (- (y * Re A) + - ((1 - z) * Im B)) * y + (x * Re B + y * Im B + (1 - z) * Re D) * (1 - z) = 0
z \<noteq> 1
H = (A, B, C, D)
M = (x, y, z)
is_real A
is_real D
C = cnj B
Re A * (1 + z) + 2 * Re B * x + 2 * Im B * y + Re D * (1 - z) = 0

goal (1 subgoal):
 1. on_circline_cmat_cvec H (stereographic_r3_cvec M)
[PROOF STEP]
apply (simp add: Let_def vec_cnj_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x * Re A + (1 - z) * Re B) * x - (- (y * Re A) - (1 - z) * Im B) * y + (x * Re B + y * Im B + (1 - z) * Re D) * (1 - z) = 0; z \<noteq> 1; H = (A, B, cnj B, D); M = (x, y, z); is_real A; is_real D; C = cnj B; Re A * (1 + z) + 2 * Re B * x + 2 * Im B * y + Re D * (1 - z) = 0\<rbrakk> \<Longrightarrow> ((cor x - \<i> * cor y) * A + (1 - cor z) * cnj B) * (cor x + \<i> * cor y) + ((cor x - \<i> * cor y) * B + (1 - cor z) * D) * (1 - cor z) = 0
[PROOF STEP]
apply (subst complex_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x * Re A + (1 - z) * Re B) * x - (- (y * Re A) - (1 - z) * Im B) * y + (x * Re B + y * Im B + (1 - z) * Re D) * (1 - z) = 0; z \<noteq> 1; H = (A, B, cnj B, D); M = (x, y, z); is_real A; is_real D; C = cnj B; Re A * (1 + z) + 2 * Re B * x + 2 * Im B * y + Re D * (1 - z) = 0\<rbrakk> \<Longrightarrow> Re (((cor x - \<i> * cor y) * A + (1 - cor z) * cnj B) * (cor x + \<i> * cor y) + ((cor x - \<i> * cor y) * B + (1 - cor z) * D) * (1 - cor z)) = Re 0 \<and> Im (((cor x - \<i> * cor y) * A + (1 - cor z) * cnj B) * (cor x + \<i> * cor y) + ((cor x - \<i> * cor y) * B + (1 - cor z) * D) * (1 - cor z)) = Im 0
[PROOF STEP]
apply (simp add: field_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
on_circline_cmat_cvec H (stereographic_r3_cvec M)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
on_circline_cmat_cvec H (stereographic_r3_cvec M)

goal (1 subgoal):
 1. on_circline_cmat_cvec H (stereographic_r3_cvec M) \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. on_circline_cmat_cvec H (stereographic_r3_cvec M) \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
on_circline_cmat_cvec H (stereographic_r3_cvec M)

goal (1 subgoal):
 1. on_circline_cmat_cvec H (stereographic_r3_cvec M) \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
[PROOF STEP]
proof (cases "z=1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z = 1 \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
 2. z \<noteq> 1 \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
z = 1

goal (2 subgoals):
 1. z = 1 \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
 2. z \<noteq> 1 \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
[PROOF STEP]
hence "x = 0" "y = 0"
[PROOF STATE]
proof (prove)
using this:
z = 1

goal (1 subgoal):
 1. x = 0 &&& y = 0
[PROOF STEP]
using MM hh
[PROOF STATE]
proof (prove)
using this:
z = 1
M = (x, y, z)
hermitean H \<and> H \<noteq> mat_zero
M \<in> unit_sphere

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

goal (2 subgoals):
 1. z = 1 \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
 2. z \<noteq> 1 \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x = 0
y = 0

goal (1 subgoal):
 1. on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
[PROOF STEP]
using HH MM \<open>?rhs\<close> \<open>z = 1\<close>
[PROOF STATE]
proof (prove)
using this:
x = 0
y = 0
H = (A, B, C, D)
M = (x, y, z)
on_circline_cmat_cvec H (stereographic_r3_cvec M)
z = 1

goal (1 subgoal):
 1. on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
[PROOF STEP]
by (simp add: Let_def vec_cnj_def)
[PROOF STATE]
proof (state)
this:
on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M

goal (1 subgoal):
 1. z \<noteq> 1 \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z \<noteq> 1 \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
z \<noteq> 1

goal (1 subgoal):
 1. z \<noteq> 1 \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
[PROOF STEP]
hence "(x * Re A + (1 - z) * Re B) * x - (- (y * Re A) + - ((1 - z) * Im B)) * y + (x * Re B + y * Im B + (1 - z) * Re D) * (1 - z) = 0"
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 1

goal (1 subgoal):
 1. (x * Re A + (1 - z) * Re B) * x - (- (y * Re A) + - ((1 - z) * Im B)) * y + (x * Re B + y * Im B + (1 - z) * Re D) * (1 - z) = 0
[PROOF STEP]
using HH MM * \<open>?rhs\<close>
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 1
H = (A, B, C, D)
M = (x, y, z)
is_real A
is_real D
C = cnj B
on_circline_cmat_cvec H (stereographic_r3_cvec M)

goal (1 subgoal):
 1. (x * Re A + (1 - z) * Re B) * x - (- (y * Re A) + - ((1 - z) * Im B)) * y + (x * Re B + y * Im B + (1 - z) * Re D) * (1 - z) = 0
[PROOF STEP]
by (simp add: Let_def vec_cnj_def complex_eq_iff)
[PROOF STATE]
proof (state)
this:
(x * Re A + (1 - z) * Re B) * x - (- (y * Re A) + - ((1 - z) * Im B)) * y + (x * Re B + y * Im B + (1 - z) * Re D) * (1 - z) = 0

goal (1 subgoal):
 1. z \<noteq> 1 \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
[PROOF STEP]
hence "Re A*(x*x+y*y) + 2*Re B*x*(1-z) + 2*Im B*y*(1-z) + Re D*(1-z)*(1-z) = 0"
[PROOF STATE]
proof (prove)
using this:
(x * Re A + (1 - z) * Re B) * x - (- (y * Re A) + - ((1 - z) * Im B)) * y + (x * Re B + y * Im B + (1 - z) * Re D) * (1 - z) = 0

goal (1 subgoal):
 1. Re A * (x * x + y * y) + 2 * Re B * x * (1 - z) + 2 * Im B * y * (1 - z) + Re D * (1 - z) * (1 - z) = 0
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
Re A * (x * x + y * y) + 2 * Re B * x * (1 - z) + 2 * Im B * y * (1 - z) + Re D * (1 - z) * (1 - z) = 0

goal (1 subgoal):
 1. z \<noteq> 1 \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Re A * (x * x + y * y) + 2 * Re B * x * (1 - z) + 2 * Im B * y * (1 - z) + Re D * (1 - z) * (1 - z) = 0

goal (1 subgoal):
 1. z \<noteq> 1 \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
[PROOF STEP]
have "x*x + y*y = (1+z)*(1-z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * x + y * y = (1 + z) * (1 - z)
[PROOF STEP]
using MM hh
[PROOF STATE]
proof (prove)
using this:
M = (x, y, z)
hermitean H \<and> H \<noteq> mat_zero
M \<in> unit_sphere

goal (1 subgoal):
 1. x * x + y * y = (1 + z) * (1 - z)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
x * x + y * y = (1 + z) * (1 - z)

goal (1 subgoal):
 1. z \<noteq> 1 \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Re A * (x * x + y * y) + 2 * Re B * x * (1 - z) + 2 * Im B * y * (1 - z) + Re D * (1 - z) * (1 - z) = 0
x * x + y * y = (1 + z) * (1 - z)
[PROOF STEP]
have "Re A*(1+z)*(1-z) + 2*Re B*x*(1-z) + 2*Im B*y*(1-z) + Re D*(1-z)*(1-z) = 0"
[PROOF STATE]
proof (prove)
using this:
Re A * (x * x + y * y) + 2 * Re B * x * (1 - z) + 2 * Im B * y * (1 - z) + Re D * (1 - z) * (1 - z) = 0
x * x + y * y = (1 + z) * (1 - z)

goal (1 subgoal):
 1. Re A * (1 + z) * (1 - z) + 2 * Re B * x * (1 - z) + 2 * Im B * y * (1 - z) + Re D * (1 - z) * (1 - z) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Re A * (1 + z) * (1 - z) + 2 * Re B * x * (1 - z) + 2 * Im B * y * (1 - z) + Re D * (1 - z) * (1 - z) = 0

goal (1 subgoal):
 1. z \<noteq> 1 \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
[PROOF STEP]
hence "(Re A*(1+z) + 2*Re B*x + 2*Im B*y + Re D*(1-z))*(1-z) = 0"
[PROOF STATE]
proof (prove)
using this:
Re A * (1 + z) * (1 - z) + 2 * Re B * x * (1 - z) + 2 * Im B * y * (1 - z) + Re D * (1 - z) * (1 - z) = 0

goal (1 subgoal):
 1. (Re A * (1 + z) + 2 * Re B * x + 2 * Im B * y + Re D * (1 - z)) * (1 - z) = 0
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
(Re A * (1 + z) + 2 * Re B * x + 2 * Im B * y + Re D * (1 - z)) * (1 - z) = 0

goal (1 subgoal):
 1. z \<noteq> 1 \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
[PROOF STEP]
hence "Re A*(1+z) + 2*Re B*x + 2*Im B*y + Re D*(1-z) = 0"
[PROOF STATE]
proof (prove)
using this:
(Re A * (1 + z) + 2 * Re B * x + 2 * Im B * y + Re D * (1 - z)) * (1 - z) = 0

goal (1 subgoal):
 1. Re A * (1 + z) + 2 * Re B * x + 2 * Im B * y + Re D * (1 - z) = 0
[PROOF STEP]
using \<open>z \<noteq> 1\<close>
[PROOF STATE]
proof (prove)
using this:
(Re A * (1 + z) + 2 * Re B * x + 2 * Im B * y + Re D * (1 - z)) * (1 - z) = 0
z \<noteq> 1

goal (1 subgoal):
 1. Re A * (1 + z) + 2 * Re B * x + 2 * Im B * y + Re D * (1 - z) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Re A * (1 + z) + 2 * Re B * x + 2 * Im B * y + Re D * (1 - z) = 0

goal (1 subgoal):
 1. z \<noteq> 1 \<Longrightarrow> on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Re A * (1 + z) + 2 * Re B * x + 2 * Im B * y + Re D * (1 - z) = 0

goal (1 subgoal):
 1. on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
[PROOF STEP]
using MM HH *
[PROOF STATE]
proof (prove)
using this:
Re A * (1 + z) + 2 * Re B * x + 2 * Im B * y + Re D * (1 - z) = 0
M = (x, y, z)
H = (A, B, C, D)
is_real A
is_real D
C = cnj B

goal (1 subgoal):
 1. on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
on_sphere_circle_r4_r3 (inv_stereographic_circline_cmat_r4 H) M = on_circline_cmat_cvec H (stereographic_r3_cvec M)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stereographic_sphere_circle_set' [simp]:
  shows "stereographic ` sphere_circle_set (inv_stereographic_circline H) =
         circline_set H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stereographic ` sphere_circle_set (inv_stereographic_circline H) = circline_set H
[PROOF STEP]
unfolding sphere_circle_set_def circline_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stereographic ` Collect (on_sphere_circle (inv_stereographic_circline H)) = Collect (on_circline H)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. on_sphere_circle (inv_stereographic_circline H) xa \<Longrightarrow> on_circline H (stereographic xa)
 2. \<And>x. on_circline H x \<Longrightarrow> x \<in> stereographic ` Collect (on_sphere_circle (inv_stereographic_circline H))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa. on_sphere_circle (inv_stereographic_circline H) xa \<Longrightarrow> on_circline H (stereographic xa)
 2. \<And>x. on_circline H x \<Longrightarrow> x \<in> stereographic ` Collect (on_sphere_circle (inv_stereographic_circline H))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa. on_sphere_circle (inv_stereographic_circline H) xa \<Longrightarrow> on_circline H (stereographic xa)
 2. \<And>x. on_circline H x \<Longrightarrow> x \<in> stereographic ` Collect (on_sphere_circle (inv_stereographic_circline H))
[PROOF STEP]
assume "on_sphere_circle (inv_stereographic_circline H) x"
[PROOF STATE]
proof (state)
this:
on_sphere_circle (inv_stereographic_circline H) x

goal (2 subgoals):
 1. \<And>x xa. on_sphere_circle (inv_stereographic_circline H) xa \<Longrightarrow> on_circline H (stereographic xa)
 2. \<And>x. on_circline H x \<Longrightarrow> x \<in> stereographic ` Collect (on_sphere_circle (inv_stereographic_circline H))
[PROOF STEP]
thus "on_circline H (stereographic x)"
[PROOF STATE]
proof (prove)
using this:
on_sphere_circle (inv_stereographic_circline H) x

goal (1 subgoal):
 1. on_circline H (stereographic x)
[PROOF STEP]
using stereographic_sphere_circle_set''
[PROOF STATE]
proof (prove)
using this:
on_sphere_circle (inv_stereographic_circline H) x
on_sphere_circle (inv_stereographic_circline ?H) ?z = on_circline ?H (stereographic ?z)

goal (1 subgoal):
 1. on_circline H (stereographic x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
on_circline H (stereographic x)

goal (1 subgoal):
 1. \<And>x. on_circline H x \<Longrightarrow> x \<in> stereographic ` Collect (on_sphere_circle (inv_stereographic_circline H))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. on_circline H x \<Longrightarrow> x \<in> stereographic ` Collect (on_sphere_circle (inv_stereographic_circline H))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. on_circline H x \<Longrightarrow> x \<in> stereographic ` Collect (on_sphere_circle (inv_stereographic_circline H))
[PROOF STEP]
assume "on_circline H x"
[PROOF STATE]
proof (state)
this:
on_circline H x

goal (1 subgoal):
 1. \<And>x. on_circline H x \<Longrightarrow> x \<in> stereographic ` Collect (on_sphere_circle (inv_stereographic_circline H))
[PROOF STEP]
show "x \<in> stereographic ` {z. on_sphere_circle (inv_stereographic_circline H) z}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> stereographic ` {z. on_sphere_circle (inv_stereographic_circline H) z}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = stereographic ?x
 2. ?x \<in> {z. on_sphere_circle (inv_stereographic_circline H) z}
[PROOF STEP]
show "x = stereographic (inv_stereographic x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = stereographic (inv_stereographic x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = stereographic (inv_stereographic x)

goal (1 subgoal):
 1. inv_stereographic x \<in> {z. on_sphere_circle (inv_stereographic_circline H) z}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv_stereographic x \<in> {z. on_sphere_circle (inv_stereographic_circline H) z}
[PROOF STEP]
show "inv_stereographic x \<in> {z. on_sphere_circle (inv_stereographic_circline H) z}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_stereographic x \<in> {z. on_sphere_circle (inv_stereographic_circline H) z}
[PROOF STEP]
using stereographic_sphere_circle_set''[of H "inv_stereographic x"] \<open>on_circline H x\<close>
[PROOF STATE]
proof (prove)
using this:
on_sphere_circle (inv_stereographic_circline H) (inv_stereographic x) = on_circline H (stereographic (inv_stereographic x))
on_circline H x

goal (1 subgoal):
 1. inv_stereographic x \<in> {z. on_sphere_circle (inv_stereographic_circline H) z}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
inv_stereographic x \<in> {z. on_sphere_circle (inv_stereographic_circline H) z}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> stereographic ` {z. on_sphere_circle (inv_stereographic_circline H) z}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stereographic_sphere_circle_set:
  shows "stereographic ` sphere_circle_set H = circline_set (stereographic_circline H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stereographic ` sphere_circle_set H = circline_set (stereographic_circline H)
[PROOF STEP]
using stereographic_sphere_circle_set'[of "stereographic_circline H"]
[PROOF STATE]
proof (prove)
using this:
stereographic ` sphere_circle_set (inv_stereographic_circline (stereographic_circline H)) = circline_set (stereographic_circline H)

goal (1 subgoal):
 1. stereographic ` sphere_circle_set H = circline_set (stereographic_circline H)
[PROOF STEP]
using inv_stereographic_circline_stereographic_circline
[PROOF STATE]
proof (prove)
using this:
stereographic ` sphere_circle_set (inv_stereographic_circline (stereographic_circline H)) = circline_set (stereographic_circline H)
inv_stereographic_circline \<circ> stereographic_circline = id

goal (1 subgoal):
 1. stereographic ` sphere_circle_set H = circline_set (stereographic_circline H)
[PROOF STEP]
unfolding comp_def
[PROOF STATE]
proof (prove)
using this:
stereographic ` sphere_circle_set (inv_stereographic_circline (stereographic_circline H)) = circline_set (stereographic_circline H)
(\<lambda>x. inv_stereographic_circline (stereographic_circline x)) = id

goal (1 subgoal):
 1. stereographic ` sphere_circle_set H = circline_set (stereographic_circline H)
[PROOF STEP]
by (metis id_apply)


[STATEMENT]
lemma bij_stereographic_circline:
  shows "bij stereographic_circline"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij stereographic_circline
[PROOF STEP]
using stereographic_circline_inv_stereographic_circline inv_stereographic_circline_stereographic_circline
[PROOF STATE]
proof (prove)
using this:
stereographic_circline \<circ> inv_stereographic_circline = id
inv_stereographic_circline \<circ> stereographic_circline = id

goal (1 subgoal):
 1. bij stereographic_circline
[PROOF STEP]
using o_bij
[PROOF STATE]
proof (prove)
using this:
stereographic_circline \<circ> inv_stereographic_circline = id
inv_stereographic_circline \<circ> stereographic_circline = id
\<lbrakk>?g \<circ> ?f = id; ?f \<circ> ?g = id\<rbrakk> \<Longrightarrow> bij ?f

goal (1 subgoal):
 1. bij stereographic_circline
[PROOF STEP]
by blast


[STATEMENT]
lemma bij_inv_stereographic_circline:
  shows "bij inv_stereographic_circline"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij inv_stereographic_circline
[PROOF STEP]
using stereographic_circline_inv_stereographic_circline inv_stereographic_circline_stereographic_circline
[PROOF STATE]
proof (prove)
using this:
stereographic_circline \<circ> inv_stereographic_circline = id
inv_stereographic_circline \<circ> stereographic_circline = id

goal (1 subgoal):
 1. bij inv_stereographic_circline
[PROOF STEP]
using o_bij
[PROOF STATE]
proof (prove)
using this:
stereographic_circline \<circ> inv_stereographic_circline = id
inv_stereographic_circline \<circ> stereographic_circline = id
\<lbrakk>?g \<circ> ?f = id; ?f \<circ> ?g = id\<rbrakk> \<Longrightarrow> bij ?f

goal (1 subgoal):
 1. bij inv_stereographic_circline
[PROOF STEP]
by blast


[STATEMENT]
lemma deriv_to_deriv[simp]:
assumes "(C,n) \<in> derivable R"
shows "C \<in> derivable' R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<in> derivable' R
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(C, n) \<in> derivable R

goal (1 subgoal):
 1. C \<in> derivable' R
[PROOF STEP]
by (induct) auto


[STATEMENT]
lemma deriv_to_deriv2:
assumes "C \<in> derivable' R"
shows "\<exists> n. (C,n) \<in> derivable R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. (C, n) \<in> derivable R
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
C \<in> derivable' R

goal (1 subgoal):
 1. \<exists>n. (C, n) \<in> derivable R
[PROOF STEP]
proof (induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C. ([], C) \<in> R \<Longrightarrow> \<exists>n. (C, n) \<in> derivable R
 2. \<And>r. \<lbrakk>r \<in> R; fst r \<noteq> []; \<forall>p\<in>set (fst r). p \<in> derivable' R \<and> (\<exists>n. (p, n) \<in> derivable R)\<rbrakk> \<Longrightarrow> \<exists>n. (snd r, n) \<in> derivable R
[PROOF STEP]
case (base C)
[PROOF STATE]
proof (state)
this:
([], C) \<in> R

goal (2 subgoals):
 1. \<And>C. ([], C) \<in> R \<Longrightarrow> \<exists>n. (C, n) \<in> derivable R
 2. \<And>r. \<lbrakk>r \<in> R; fst r \<noteq> []; \<forall>p\<in>set (fst r). p \<in> derivable' R \<and> (\<exists>n. (p, n) \<in> derivable R)\<rbrakk> \<Longrightarrow> \<exists>n. (snd r, n) \<in> derivable R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
([], C) \<in> R
[PROOF STEP]
have "(C,0) \<in> derivable R"
[PROOF STATE]
proof (prove)
using this:
([], C) \<in> R

goal (1 subgoal):
 1. (C, 0) \<in> derivable R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(C, 0) \<in> derivable R

goal (2 subgoals):
 1. \<And>C. ([], C) \<in> R \<Longrightarrow> \<exists>n. (C, n) \<in> derivable R
 2. \<And>r. \<lbrakk>r \<in> R; fst r \<noteq> []; \<forall>p\<in>set (fst r). p \<in> derivable' R \<and> (\<exists>n. (p, n) \<in> derivable R)\<rbrakk> \<Longrightarrow> \<exists>n. (snd r, n) \<in> derivable R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(C, 0) \<in> derivable R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(C, 0) \<in> derivable R

goal (1 subgoal):
 1. \<exists>n. (C, n) \<in> derivable R
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>n. (C, n) \<in> derivable R

goal (1 subgoal):
 1. \<And>r. \<lbrakk>r \<in> R; fst r \<noteq> []; \<forall>p\<in>set (fst r). p \<in> derivable' R \<and> (\<exists>n. (p, n) \<in> derivable R)\<rbrakk> \<Longrightarrow> \<exists>n. (snd r, n) \<in> derivable R
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>r \<in> R; fst r \<noteq> []; \<forall>p\<in>set (fst r). p \<in> derivable' R \<and> (\<exists>n. (p, n) \<in> derivable R)\<rbrakk> \<Longrightarrow> \<exists>n. (snd r, n) \<in> derivable R
[PROOF STEP]
case (step r)
[PROOF STATE]
proof (state)
this:
r \<in> R
fst r \<noteq> []
\<forall>p\<in>set (fst r). p \<in> derivable' R \<and> (\<exists>n. (p, n) \<in> derivable R)

goal (1 subgoal):
 1. \<And>r. \<lbrakk>r \<in> R; fst r \<noteq> []; \<forall>p\<in>set (fst r). p \<in> derivable' R \<and> (\<exists>n. (p, n) \<in> derivable R)\<rbrakk> \<Longrightarrow> \<exists>n. (snd r, n) \<in> derivable R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> R
fst r \<noteq> []
\<forall>p\<in>set (fst r). p \<in> derivable' R \<and> (\<exists>n. (p, n) \<in> derivable R)
[PROOF STEP]
obtain ps c where "r = (ps,c)" and "ps \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
r \<in> R
fst r \<noteq> []
\<forall>p\<in>set (fst r). p \<in> derivable' R \<and> (\<exists>n. (p, n) \<in> derivable R)

goal (1 subgoal):
 1. (\<And>ps c. \<lbrakk>r = (ps, c); ps \<noteq> []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases r) auto
[PROOF STATE]
proof (state)
this:
r = (ps, c)
ps \<noteq> []

goal (1 subgoal):
 1. \<And>r. \<lbrakk>r \<in> R; fst r \<noteq> []; \<forall>p\<in>set (fst r). p \<in> derivable' R \<and> (\<exists>n. (p, n) \<in> derivable R)\<rbrakk> \<Longrightarrow> \<exists>n. (snd r, n) \<in> derivable R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r = (ps, c)
ps \<noteq> []
[PROOF STEP]
have aa: "\<forall> p \<in> set ps. \<exists> n. (p,n) \<in> derivable R"
[PROOF STATE]
proof (prove)
using this:
r = (ps, c)
ps \<noteq> []

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>n. (p, n) \<in> derivable R
[PROOF STEP]
using step(3)
[PROOF STATE]
proof (prove)
using this:
r = (ps, c)
ps \<noteq> []
\<forall>p\<in>set (fst r). p \<in> derivable' R \<and> (\<exists>n. (p, n) \<in> derivable R)

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>n. (p, n) \<in> derivable R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set ps. \<exists>n. (p, n) \<in> derivable R

goal (1 subgoal):
 1. \<And>r. \<lbrakk>r \<in> R; fst r \<noteq> []; \<forall>p\<in>set (fst r). p \<in> derivable' R \<and> (\<exists>n. (p, n) \<in> derivable R)\<rbrakk> \<Longrightarrow> \<exists>n. (snd r, n) \<in> derivable R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>p\<in>set ps. \<exists>n. (p, n) \<in> derivable R
[PROOF STEP]
have "\<exists> m. \<forall> p \<in> set ps. \<exists> n\<le>m. (p,n) \<in> derivable R"
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set ps. \<exists>n. (p, n) \<in> derivable R

goal (1 subgoal):
 1. \<exists>m. \<forall>p\<in>set ps. \<exists>n\<le>m. (p, n) \<in> derivable R
[PROOF STEP]
proof (induct ps)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>p\<in>set []. \<exists>n. (p, n) \<in> derivable R \<Longrightarrow> \<exists>m. \<forall>p\<in>set []. \<exists>n\<le>m. (p, n) \<in> derivable R
 2. \<And>a ps. \<lbrakk>\<forall>p\<in>set ps. \<exists>n. (p, n) \<in> derivable R \<Longrightarrow> \<exists>m. \<forall>p\<in>set ps. \<exists>n\<le>m. (p, n) \<in> derivable R; \<forall>p\<in>set (a # ps). \<exists>n. (p, n) \<in> derivable R\<rbrakk> \<Longrightarrow> \<exists>m. \<forall>p\<in>set (a # ps). \<exists>n\<le>m. (p, n) \<in> derivable R
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set []. \<exists>n. (p, n) \<in> derivable R

goal (2 subgoals):
 1. \<forall>p\<in>set []. \<exists>n. (p, n) \<in> derivable R \<Longrightarrow> \<exists>m. \<forall>p\<in>set []. \<exists>n\<le>m. (p, n) \<in> derivable R
 2. \<And>a ps. \<lbrakk>\<forall>p\<in>set ps. \<exists>n. (p, n) \<in> derivable R \<Longrightarrow> \<exists>m. \<forall>p\<in>set ps. \<exists>n\<le>m. (p, n) \<in> derivable R; \<forall>p\<in>set (a # ps). \<exists>n. (p, n) \<in> derivable R\<rbrakk> \<Longrightarrow> \<exists>m. \<forall>p\<in>set (a # ps). \<exists>n\<le>m. (p, n) \<in> derivable R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>p\<in>set []. \<exists>n. (p, n) \<in> derivable R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set []. \<exists>n. (p, n) \<in> derivable R

goal (1 subgoal):
 1. \<exists>m. \<forall>p\<in>set []. \<exists>n\<le>m. (p, n) \<in> derivable R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>m. \<forall>p\<in>set []. \<exists>n\<le>m. (p, n) \<in> derivable R

goal (1 subgoal):
 1. \<And>a ps. \<lbrakk>\<forall>p\<in>set ps. \<exists>n. (p, n) \<in> derivable R \<Longrightarrow> \<exists>m. \<forall>p\<in>set ps. \<exists>n\<le>m. (p, n) \<in> derivable R; \<forall>p\<in>set (a # ps). \<exists>n. (p, n) \<in> derivable R\<rbrakk> \<Longrightarrow> \<exists>m. \<forall>p\<in>set (a # ps). \<exists>n\<le>m. (p, n) \<in> derivable R
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ps. \<lbrakk>\<forall>p\<in>set ps. \<exists>n. (p, n) \<in> derivable R \<Longrightarrow> \<exists>m. \<forall>p\<in>set ps. \<exists>n\<le>m. (p, n) \<in> derivable R; \<forall>p\<in>set (a # ps). \<exists>n. (p, n) \<in> derivable R\<rbrakk> \<Longrightarrow> \<exists>m. \<forall>p\<in>set (a # ps). \<exists>n\<le>m. (p, n) \<in> derivable R
[PROOF STEP]
case (Cons a as)
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set as. \<exists>n. (p, n) \<in> derivable R \<Longrightarrow> \<exists>m. \<forall>p\<in>set as. \<exists>n\<le>m. (p, n) \<in> derivable R
\<forall>p\<in>set (a # as). \<exists>n. (p, n) \<in> derivable R

goal (1 subgoal):
 1. \<And>a ps. \<lbrakk>\<forall>p\<in>set ps. \<exists>n. (p, n) \<in> derivable R \<Longrightarrow> \<exists>m. \<forall>p\<in>set ps. \<exists>n\<le>m. (p, n) \<in> derivable R; \<forall>p\<in>set (a # ps). \<exists>n. (p, n) \<in> derivable R\<rbrakk> \<Longrightarrow> \<exists>m. \<forall>p\<in>set (a # ps). \<exists>n\<le>m. (p, n) \<in> derivable R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>p\<in>set as. \<exists>n. (p, n) \<in> derivable R \<Longrightarrow> \<exists>m. \<forall>p\<in>set as. \<exists>n\<le>m. (p, n) \<in> derivable R
\<forall>p\<in>set (a # as). \<exists>n. (p, n) \<in> derivable R
[PROOF STEP]
have "\<exists> m. \<forall> p \<in> set as. \<exists> n\<le>m. (p,n) \<in> derivable R"
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set as. \<exists>n. (p, n) \<in> derivable R \<Longrightarrow> \<exists>m. \<forall>p\<in>set as. \<exists>n\<le>m. (p, n) \<in> derivable R
\<forall>p\<in>set (a # as). \<exists>n. (p, n) \<in> derivable R

goal (1 subgoal):
 1. \<exists>m. \<forall>p\<in>set as. \<exists>n\<le>m. (p, n) \<in> derivable R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>m. \<forall>p\<in>set as. \<exists>n\<le>m. (p, n) \<in> derivable R

goal (1 subgoal):
 1. \<And>a ps. \<lbrakk>\<forall>p\<in>set ps. \<exists>n. (p, n) \<in> derivable R \<Longrightarrow> \<exists>m. \<forall>p\<in>set ps. \<exists>n\<le>m. (p, n) \<in> derivable R; \<forall>p\<in>set (a # ps). \<exists>n. (p, n) \<in> derivable R\<rbrakk> \<Longrightarrow> \<exists>m. \<forall>p\<in>set (a # ps). \<exists>n\<le>m. (p, n) \<in> derivable R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>m. \<forall>p\<in>set as. \<exists>n\<le>m. (p, n) \<in> derivable R
[PROOF STEP]
obtain m where "\<forall> p \<in> set as. \<exists> n\<le>m. (p,n) \<in> derivable R"
[PROOF STATE]
proof (prove)
using this:
\<exists>m. \<forall>p\<in>set as. \<exists>n\<le>m. (p, n) \<in> derivable R

goal (1 subgoal):
 1. (\<And>m. \<forall>p\<in>set as. \<exists>n\<le>m. (p, n) \<in> derivable R \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set as. \<exists>n\<le>m. (p, n) \<in> derivable R

goal (1 subgoal):
 1. \<And>a ps. \<lbrakk>\<forall>p\<in>set ps. \<exists>n. (p, n) \<in> derivable R \<Longrightarrow> \<exists>m. \<forall>p\<in>set ps. \<exists>n\<le>m. (p, n) \<in> derivable R; \<forall>p\<in>set (a # ps). \<exists>n. (p, n) \<in> derivable R\<rbrakk> \<Longrightarrow> \<exists>m. \<forall>p\<in>set (a # ps). \<exists>n\<le>m. (p, n) \<in> derivable R
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set as. \<exists>n\<le>m. (p, n) \<in> derivable R

goal (1 subgoal):
 1. \<And>a ps. \<lbrakk>\<forall>p\<in>set ps. \<exists>n. (p, n) \<in> derivable R \<Longrightarrow> \<exists>m. \<forall>p\<in>set ps. \<exists>n\<le>m. (p, n) \<in> derivable R; \<forall>p\<in>set (a # ps). \<exists>n. (p, n) \<in> derivable R\<rbrakk> \<Longrightarrow> \<exists>m. \<forall>p\<in>set (a # ps). \<exists>n\<le>m. (p, n) \<in> derivable R
[PROOF STEP]
from \<open>\<forall> p \<in> set (a # as). \<exists> n. (p,n) \<in> derivable R\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>p\<in>set (a # as). \<exists>n. (p, n) \<in> derivable R
[PROOF STEP]
have
      "\<exists> n. (a,n) \<in> derivable R"
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set (a # as). \<exists>n. (p, n) \<in> derivable R

goal (1 subgoal):
 1. \<exists>n. (a, n) \<in> derivable R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>n. (a, n) \<in> derivable R

goal (1 subgoal):
 1. \<And>a ps. \<lbrakk>\<forall>p\<in>set ps. \<exists>n. (p, n) \<in> derivable R \<Longrightarrow> \<exists>m. \<forall>p\<in>set ps. \<exists>n\<le>m. (p, n) \<in> derivable R; \<forall>p\<in>set (a # ps). \<exists>n. (p, n) \<in> derivable R\<rbrakk> \<Longrightarrow> \<exists>m. \<forall>p\<in>set (a # ps). \<exists>n\<le>m. (p, n) \<in> derivable R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. (a, n) \<in> derivable R
[PROOF STEP]
obtain m' where "(a,m') \<in> derivable R"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. (a, n) \<in> derivable R

goal (1 subgoal):
 1. (\<And>m'. (a, m') \<in> derivable R \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(a, m') \<in> derivable R

goal (1 subgoal):
 1. \<And>a ps. \<lbrakk>\<forall>p\<in>set ps. \<exists>n. (p, n) \<in> derivable R \<Longrightarrow> \<exists>m. \<forall>p\<in>set ps. \<exists>n\<le>m. (p, n) \<in> derivable R; \<forall>p\<in>set (a # ps). \<exists>n. (p, n) \<in> derivable R\<rbrakk> \<Longrightarrow> \<exists>m. \<forall>p\<in>set (a # ps). \<exists>n\<le>m. (p, n) \<in> derivable R
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>p\<in>set as. \<exists>n\<le>m. (p, n) \<in> derivable R
(a, m') \<in> derivable R
[PROOF STEP]
have "\<forall> p \<in> set (a # as). \<exists> n\<le>(max m m'). (p,n) \<in> derivable R"
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set as. \<exists>n\<le>m. (p, n) \<in> derivable R
(a, m') \<in> derivable R

goal (1 subgoal):
 1. \<forall>p\<in>set (a # as). \<exists>n\<le>max m m'. (p, n) \<in> derivable R
[PROOF STEP]
apply (auto simp add:Ball_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x. x \<in> set as \<longrightarrow> (\<exists>n\<le>m. (x, n) \<in> derivable R); (a, m') \<in> derivable R\<rbrakk> \<Longrightarrow> \<exists>n\<le>max m m'. (a, n) \<in> derivable R
 2. \<And>x. \<lbrakk>\<forall>x. x \<in> set as \<longrightarrow> (\<exists>n\<le>m. (x, n) \<in> derivable R); (a, m') \<in> derivable R; x \<in> set as\<rbrakk> \<Longrightarrow> \<exists>n\<le>max m m'. (x, n) \<in> derivable R
[PROOF STEP]
apply (rule_tac x=m' in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x. x \<in> set as \<longrightarrow> (\<exists>n\<le>m. (x, n) \<in> derivable R); (a, m') \<in> derivable R\<rbrakk> \<Longrightarrow> m' \<le> max m m' \<and> (a, m') \<in> derivable R
 2. \<And>x. \<lbrakk>\<forall>x. x \<in> set as \<longrightarrow> (\<exists>n\<le>m. (x, n) \<in> derivable R); (a, m') \<in> derivable R; x \<in> set as\<rbrakk> \<Longrightarrow> \<exists>n\<le>max m m'. (x, n) \<in> derivable R
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x. x \<in> set as \<longrightarrow> (\<exists>n\<le>m. (x, n) \<in> derivable R); (a, m') \<in> derivable R; x \<in> set as\<rbrakk> \<Longrightarrow> \<exists>n\<le>max m m'. (x, n) \<in> derivable R
[PROOF STEP]
apply (drule_tac x=x in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(a, m') \<in> derivable R; x \<in> set as; x \<in> set as \<longrightarrow> (\<exists>n\<le>m. (x, n) \<in> derivable R)\<rbrakk> \<Longrightarrow> \<exists>n\<le>max m m'. (x, n) \<in> derivable R
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x n. \<lbrakk>(a, m') \<in> derivable R; x \<in> set as; n \<le> m; (x, n) \<in> derivable R\<rbrakk> \<Longrightarrow> \<exists>n\<le>max m m'. (x, n) \<in> derivable R
[PROOF STEP]
by (rule_tac x=n in exI) auto
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set (a # as). \<exists>n\<le>max m m'. (p, n) \<in> derivable R

goal (1 subgoal):
 1. \<And>a ps. \<lbrakk>\<forall>p\<in>set ps. \<exists>n. (p, n) \<in> derivable R \<Longrightarrow> \<exists>m. \<forall>p\<in>set ps. \<exists>n\<le>m. (p, n) \<in> derivable R; \<forall>p\<in>set (a # ps). \<exists>n. (p, n) \<in> derivable R\<rbrakk> \<Longrightarrow> \<exists>m. \<forall>p\<in>set (a # ps). \<exists>n\<le>m. (p, n) \<in> derivable R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>p\<in>set (a # as). \<exists>n\<le>max m m'. (p, n) \<in> derivable R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set (a # as). \<exists>n\<le>max m m'. (p, n) \<in> derivable R

goal (1 subgoal):
 1. \<exists>m. \<forall>p\<in>set (a # as). \<exists>n\<le>m. (p, n) \<in> derivable R
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>m. \<forall>p\<in>set (a # as). \<exists>n\<le>m. (p, n) \<in> derivable R

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>m. \<forall>p\<in>set ps. \<exists>n\<le>m. (p, n) \<in> derivable R

goal (1 subgoal):
 1. \<And>r. \<lbrakk>r \<in> R; fst r \<noteq> []; \<forall>p\<in>set (fst r). p \<in> derivable' R \<and> (\<exists>n. (p, n) \<in> derivable R)\<rbrakk> \<Longrightarrow> \<exists>n. (snd r, n) \<in> derivable R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>m. \<forall>p\<in>set ps. \<exists>n\<le>m. (p, n) \<in> derivable R
[PROOF STEP]
obtain m where "\<forall> p \<in> set ps. \<exists> n\<le>m. (p,n) \<in> derivable R"
[PROOF STATE]
proof (prove)
using this:
\<exists>m. \<forall>p\<in>set ps. \<exists>n\<le>m. (p, n) \<in> derivable R

goal (1 subgoal):
 1. (\<And>m. \<forall>p\<in>set ps. \<exists>n\<le>m. (p, n) \<in> derivable R \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set ps. \<exists>n\<le>m. (p, n) \<in> derivable R

goal (1 subgoal):
 1. \<And>r. \<lbrakk>r \<in> R; fst r \<noteq> []; \<forall>p\<in>set (fst r). p \<in> derivable' R \<and> (\<exists>n. (p, n) \<in> derivable R)\<rbrakk> \<Longrightarrow> \<exists>n. (snd r, n) \<in> derivable R
[PROOF STEP]
with \<open>r = (ps,c)\<close> and \<open>r \<in> R\<close>
[PROOF STATE]
proof (chain)
picking this:
r = (ps, c)
r \<in> R
\<forall>p\<in>set ps. \<exists>n\<le>m. (p, n) \<in> derivable R
[PROOF STEP]
have "(c,m+1) \<in> derivable R"
[PROOF STATE]
proof (prove)
using this:
r = (ps, c)
r \<in> R
\<forall>p\<in>set ps. \<exists>n\<le>m. (p, n) \<in> derivable R

goal (1 subgoal):
 1. (c, m + 1) \<in> derivable R
[PROOF STEP]
using \<open>ps \<noteq> []\<close> and
    derivable.step[where r="(ps,c)" and R=R and m=m]
[PROOF STATE]
proof (prove)
using this:
r = (ps, c)
r \<in> R
\<forall>p\<in>set ps. \<exists>n\<le>m. (p, n) \<in> derivable R
ps \<noteq> []
\<lbrakk>(ps, c) \<in> R; fst (ps, c) \<noteq> []; \<forall>p\<in>set (fst (ps, c)). \<exists>n\<le>m. (p, n) \<in> derivable R\<rbrakk> \<Longrightarrow> (snd (ps, c), m + 1) \<in> derivable R

goal (1 subgoal):
 1. (c, m + 1) \<in> derivable R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(c, m + 1) \<in> derivable R

goal (1 subgoal):
 1. \<And>r. \<lbrakk>r \<in> R; fst r \<noteq> []; \<forall>p\<in>set (fst r). p \<in> derivable' R \<and> (\<exists>n. (p, n) \<in> derivable R)\<rbrakk> \<Longrightarrow> \<exists>n. (snd r, n) \<in> derivable R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(c, m + 1) \<in> derivable R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(c, m + 1) \<in> derivable R

goal (1 subgoal):
 1. \<exists>n. (snd r, n) \<in> derivable R
[PROOF STEP]
using \<open>r = (ps,c)\<close>
[PROOF STATE]
proof (prove)
using this:
(c, m + 1) \<in> derivable R
r = (ps, c)

goal (1 subgoal):
 1. \<exists>n. (snd r, n) \<in> derivable R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>n. (snd r, n) \<in> derivable R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma characteriseSeq:
shows "\<exists> A B. (C :: 'a sequent) = (A \<Rightarrow>* B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A B. C = ( A \<Rightarrow>* B)
[PROOF STEP]
apply (rule_tac x="antec C" in exI, rule_tac x="succ C" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C = ( antec C \<Rightarrow>* succ C)
[PROOF STEP]
by (cases C) (auto)


[STATEMENT]
lemma nonEmptySet:
shows "A \<noteq> [] \<longrightarrow> (\<exists> a. a \<in> set A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<noteq> [] \<longrightarrow> (\<exists>a. a \<in> set A)
[PROOF STEP]
by (auto simp add:neq_Nil_conv)


[STATEMENT]
lemma midMultiset:
  assumes "\<Gamma> \<oplus> A = \<Gamma>' \<oplus> B" and "A \<noteq> B"
  shows "\<exists> \<Gamma>''. \<Gamma> = \<Gamma>'' \<oplus> B \<and> \<Gamma>' = \<Gamma>'' \<oplus> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<Gamma>''. \<Gamma> = \<Gamma>'' \<oplus> B \<and> \<Gamma>' = \<Gamma>'' \<oplus> A
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<Gamma>''. \<Gamma> = \<Gamma>'' \<oplus> B \<and> \<Gamma>' = \<Gamma>'' \<oplus> A
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> \<oplus> A = \<Gamma>' \<oplus> B
A \<noteq> B
[PROOF STEP]
have "A \<in># \<Gamma>'"
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<oplus> A = \<Gamma>' \<oplus> B
A \<noteq> B

goal (1 subgoal):
 1. A \<in># \<Gamma>'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> \<oplus> A = \<Gamma>' \<oplus> B; A \<noteq> B\<rbrakk> \<Longrightarrow> A \<in># \<Gamma>'
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> \<oplus> A = \<Gamma>' \<oplus> B
A \<noteq> B
[PROOF STEP]
have "set_mset (\<Gamma> \<oplus> A) = set_mset (\<Gamma>' \<oplus> B)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<oplus> A = \<Gamma>' \<oplus> B
A \<noteq> B

goal (1 subgoal):
 1. set_mset (\<Gamma> \<oplus> A) = set_mset (\<Gamma>' \<oplus> B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set_mset (\<Gamma> \<oplus> A) = set_mset (\<Gamma>' \<oplus> B)

goal (1 subgoal):
 1. \<lbrakk>\<Gamma> \<oplus> A = \<Gamma>' \<oplus> B; A \<noteq> B\<rbrakk> \<Longrightarrow> A \<in># \<Gamma>'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set_mset (\<Gamma> \<oplus> A) = set_mset (\<Gamma>' \<oplus> B)
[PROOF STEP]
have "set_mset \<Gamma> \<union> {A} = set_mset \<Gamma>' \<union> {B}"
[PROOF STATE]
proof (prove)
using this:
set_mset (\<Gamma> \<oplus> A) = set_mset (\<Gamma>' \<oplus> B)

goal (1 subgoal):
 1. set_mset \<Gamma> \<union> {A} = set_mset \<Gamma>' \<union> {B}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set_mset \<Gamma> \<union> {A} = set_mset \<Gamma>' \<union> {B}

goal (1 subgoal):
 1. \<lbrakk>\<Gamma> \<oplus> A = \<Gamma>' \<oplus> B; A \<noteq> B\<rbrakk> \<Longrightarrow> A \<in># \<Gamma>'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set_mset \<Gamma> \<union> {A} = set_mset \<Gamma>' \<union> {B}
[PROOF STEP]
have "set_mset \<Gamma> \<union> {A} \<subseteq> set_mset \<Gamma>' \<union> {B}"
[PROOF STATE]
proof (prove)
using this:
set_mset \<Gamma> \<union> {A} = set_mset \<Gamma>' \<union> {B}

goal (1 subgoal):
 1. set_mset \<Gamma> \<union> {A} \<subseteq> set_mset \<Gamma>' \<union> {B}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set_mset \<Gamma> \<union> {A} \<subseteq> set_mset \<Gamma>' \<union> {B}

goal (1 subgoal):
 1. \<lbrakk>\<Gamma> \<oplus> A = \<Gamma>' \<oplus> B; A \<noteq> B\<rbrakk> \<Longrightarrow> A \<in># \<Gamma>'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set_mset \<Gamma> \<union> {A} \<subseteq> set_mset \<Gamma>' \<union> {B}
[PROOF STEP]
have "A \<in> set_mset \<Gamma>'"
[PROOF STATE]
proof (prove)
using this:
set_mset \<Gamma> \<union> {A} \<subseteq> set_mset \<Gamma>' \<union> {B}

goal (1 subgoal):
 1. A \<in># \<Gamma>'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set_mset \<Gamma> \<union> {A} \<subseteq> set_mset \<Gamma>' \<union> {B}
\<Gamma> \<oplus> A = \<Gamma>' \<oplus> B
A \<noteq> B

goal (1 subgoal):
 1. A \<in># \<Gamma>'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<in># \<Gamma>'

goal (1 subgoal):
 1. \<lbrakk>\<Gamma> \<oplus> A = \<Gamma>' \<oplus> B; A \<noteq> B\<rbrakk> \<Longrightarrow> A \<in># \<Gamma>'
[PROOF STEP]
thus "A \<in># \<Gamma>'"
[PROOF STATE]
proof (prove)
using this:
A \<in># \<Gamma>'

goal (1 subgoal):
 1. A \<in># \<Gamma>'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A \<in># \<Gamma>'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A \<in># \<Gamma>'

goal (1 subgoal):
 1. \<exists>\<Gamma>''. \<Gamma> = \<Gamma>'' \<oplus> B \<and> \<Gamma>' = \<Gamma>'' \<oplus> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<in># \<Gamma>'
[PROOF STEP]
have "\<Gamma>' \<ominus> A \<oplus> A = \<Gamma>'"
[PROOF STATE]
proof (prove)
using this:
A \<in># \<Gamma>'

goal (1 subgoal):
 1. \<Gamma>' \<ominus> A \<oplus> A = \<Gamma>'
[PROOF STEP]
by (auto simp add:multiset_eq_iff)
[PROOF STATE]
proof (state)
this:
\<Gamma>' \<ominus> A \<oplus> A = \<Gamma>'

goal (1 subgoal):
 1. \<exists>\<Gamma>''. \<Gamma> = \<Gamma>'' \<oplus> B \<and> \<Gamma>' = \<Gamma>'' \<oplus> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>' \<ominus> A \<oplus> A = \<Gamma>'
[PROOF STEP]
have "\<exists> \<Gamma>''. \<Gamma>' = \<Gamma>'' \<oplus> A"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>' \<ominus> A \<oplus> A = \<Gamma>'

goal (1 subgoal):
 1. \<exists>\<Gamma>''. \<Gamma>' = \<Gamma>'' \<oplus> A
[PROOF STEP]
apply (rule_tac x="\<Gamma>' \<ominus> A" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>' \<ominus> A \<oplus> A = \<Gamma>' \<Longrightarrow> \<Gamma>' = \<Gamma>' \<ominus> A \<oplus> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>\<Gamma>''. \<Gamma>' = \<Gamma>'' \<oplus> A

goal (1 subgoal):
 1. \<exists>\<Gamma>''. \<Gamma> = \<Gamma>'' \<oplus> B \<and> \<Gamma>' = \<Gamma>'' \<oplus> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<Gamma>''. \<Gamma>' = \<Gamma>'' \<oplus> A
[PROOF STEP]
obtain \<Gamma>'' where eq1:"\<Gamma>' = \<Gamma>'' \<oplus> A"
[PROOF STATE]
proof (prove)
using this:
\<exists>\<Gamma>''. \<Gamma>' = \<Gamma>'' \<oplus> A

goal (1 subgoal):
 1. (\<And>\<Gamma>''. \<Gamma>' = \<Gamma>'' \<oplus> A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<Gamma>' = \<Gamma>'' \<oplus> A

goal (1 subgoal):
 1. \<exists>\<Gamma>''. \<Gamma> = \<Gamma>'' \<oplus> B \<and> \<Gamma>' = \<Gamma>'' \<oplus> A
[PROOF STEP]
from \<open>\<Gamma> \<oplus> A = \<Gamma>' \<oplus> B\<close> eq1
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> \<oplus> A = \<Gamma>' \<oplus> B
\<Gamma>' = \<Gamma>'' \<oplus> A
[PROOF STEP]
have "\<Gamma> \<oplus> A = \<Gamma>'' \<oplus> A \<oplus> B"
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<oplus> A = \<Gamma>' \<oplus> B
\<Gamma>' = \<Gamma>'' \<oplus> A

goal (1 subgoal):
 1. \<Gamma> \<oplus> A = \<Gamma>'' \<oplus> A \<oplus> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Gamma> \<oplus> A = \<Gamma>'' \<oplus> A \<oplus> B

goal (1 subgoal):
 1. \<exists>\<Gamma>''. \<Gamma> = \<Gamma>'' \<oplus> B \<and> \<Gamma>' = \<Gamma>'' \<oplus> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> \<oplus> A = \<Gamma>'' \<oplus> A \<oplus> B
[PROOF STEP]
have "\<Gamma> = \<Gamma>'' \<oplus> B"
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<oplus> A = \<Gamma>'' \<oplus> A \<oplus> B

goal (1 subgoal):
 1. \<Gamma> = \<Gamma>'' \<oplus> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Gamma> = \<Gamma>'' \<oplus> B

goal (1 subgoal):
 1. \<exists>\<Gamma>''. \<Gamma> = \<Gamma>'' \<oplus> B \<and> \<Gamma>' = \<Gamma>'' \<oplus> A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma> = \<Gamma>'' \<oplus> B

goal (1 subgoal):
 1. \<exists>\<Gamma>''. \<Gamma> = \<Gamma>'' \<oplus> B \<and> \<Gamma>' = \<Gamma>'' \<oplus> A
[PROOF STEP]
using eq1
[PROOF STATE]
proof (prove)
using this:
\<Gamma> = \<Gamma>'' \<oplus> B
\<Gamma>' = \<Gamma>'' \<oplus> A

goal (1 subgoal):
 1. \<exists>\<Gamma>''. \<Gamma> = \<Gamma>'' \<oplus> B \<and> \<Gamma>' = \<Gamma>'' \<oplus> A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>\<Gamma>''. \<Gamma> = \<Gamma>'' \<oplus> B \<and> \<Gamma>' = \<Gamma>'' \<oplus> A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma extendID:
assumes "extend S (\<LM> At i \<RM> \<Rightarrow>* At i) = (\<Gamma> \<Rightarrow>* \<Delta>)"
shows "At i \<in># \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. At i \<in># \<Gamma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
extend S ( \<LM> At i  \<RM> \<Rightarrow>* At i) = ( \<Gamma> \<Rightarrow>* \<Delta>)

goal (1 subgoal):
 1. At i \<in># \<Gamma>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. extend S ( \<LM> At i  \<RM> \<Rightarrow>* At i) = ( \<Gamma> \<Rightarrow>* \<Delta>) \<Longrightarrow> At i \<in># \<Gamma>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
extend S ( \<LM> At i  \<RM> \<Rightarrow>* At i) = ( \<Gamma> \<Rightarrow>* \<Delta>)
[PROOF STEP]
have "\<exists> \<Gamma>'. \<Gamma> = \<Gamma>' \<oplus> At i"
[PROOF STATE]
proof (prove)
using this:
extend S ( \<LM> At i  \<RM> \<Rightarrow>* At i) = ( \<Gamma> \<Rightarrow>* \<Delta>)

goal (1 subgoal):
 1. \<exists>\<Gamma>'. \<Gamma> = \<Gamma>' \<oplus> At i
[PROOF STEP]
using extend_def[where forms=S and seq="\<LM> At i \<RM> \<Rightarrow>* At i"]
[PROOF STATE]
proof (prove)
using this:
extend S ( \<LM> At i  \<RM> \<Rightarrow>* At i) = ( \<Gamma> \<Rightarrow>* \<Delta>)
extend S ( \<LM> At i  \<RM> \<Rightarrow>* At i) \<equiv> if succ ( \<LM> At i  \<RM> \<Rightarrow>* At i) = Em then  antec S + antec ( \<LM> At i  \<RM> \<Rightarrow>* At i) \<Rightarrow>* succ S else ( antec S + antec ( \<LM> At i  \<RM> \<Rightarrow>* At i) \<Rightarrow>* succ ( \<LM> At i  \<RM> \<Rightarrow>* At i))

goal (1 subgoal):
 1. \<exists>\<Gamma>'. \<Gamma> = \<Gamma>' \<oplus> At i
[PROOF STEP]
by (rule_tac x="antec S" in exI) auto
[PROOF STATE]
proof (state)
this:
\<exists>\<Gamma>'. \<Gamma> = \<Gamma>' \<oplus> At i

goal (1 subgoal):
 1. extend S ( \<LM> At i  \<RM> \<Rightarrow>* At i) = ( \<Gamma> \<Rightarrow>* \<Delta>) \<Longrightarrow> At i \<in># \<Gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<Gamma>'. \<Gamma> = \<Gamma>' \<oplus> At i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>\<Gamma>'. \<Gamma> = \<Gamma>' \<oplus> At i

goal (1 subgoal):
 1. At i \<in># \<Gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
At i \<in># \<Gamma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma extendFalsum:
assumes "extend S (\<LM> ff \<RM> \<Rightarrow>* Em) = (\<Gamma> \<Rightarrow>* \<Delta>)"
shows "ff \<in># \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ff \<in># \<Gamma>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ff \<in># \<Gamma>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
extend S ( \<LM> ff  \<RM> \<Rightarrow>* Em) = ( \<Gamma> \<Rightarrow>* \<Delta>)
[PROOF STEP]
have "\<exists> \<Gamma>'. \<Gamma> = \<Gamma>' \<oplus> ff"
[PROOF STATE]
proof (prove)
using this:
extend S ( \<LM> ff  \<RM> \<Rightarrow>* Em) = ( \<Gamma> \<Rightarrow>* \<Delta>)

goal (1 subgoal):
 1. \<exists>\<Gamma>'. \<Gamma> = \<Gamma>' \<oplus> ff
[PROOF STEP]
using extend_def[where forms=S and seq="\<LM>ff \<RM> \<Rightarrow>* Em"]
[PROOF STATE]
proof (prove)
using this:
extend S ( \<LM> ff  \<RM> \<Rightarrow>* Em) = ( \<Gamma> \<Rightarrow>* \<Delta>)
extend S ( \<LM> ff  \<RM> \<Rightarrow>* Em) \<equiv> if succ ( \<LM> ff  \<RM> \<Rightarrow>* Em) = Em then  antec S + antec ( \<LM> ff  \<RM> \<Rightarrow>* Em) \<Rightarrow>* succ S else ( antec S + antec ( \<LM> ff  \<RM> \<Rightarrow>* Em) \<Rightarrow>* succ ( \<LM> ff  \<RM> \<Rightarrow>* Em))

goal (1 subgoal):
 1. \<exists>\<Gamma>'. \<Gamma> = \<Gamma>' \<oplus> ff
[PROOF STEP]
by (rule_tac x="antec S" in exI) auto
[PROOF STATE]
proof (state)
this:
\<exists>\<Gamma>'. \<Gamma> = \<Gamma>' \<oplus> ff

goal (1 subgoal):
 1. ff \<in># \<Gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<Gamma>'. \<Gamma> = \<Gamma>' \<oplus> ff
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>\<Gamma>'. \<Gamma> = \<Gamma>' \<oplus> ff

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma containID:
assumes a:"At i \<in># \<Gamma>"
    and b:"Ax \<subseteq> R"
shows "(\<Gamma> \<Rightarrow>* At i,0) \<in> derivable R*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* At i, 0) \<in> derivable R*
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* At i, 0) \<in> derivable R*
[PROOF STEP]
from a
[PROOF STATE]
proof (chain)
picking this:
At i \<in># \<Gamma>
[PROOF STEP]
have "\<Gamma> = \<Gamma> \<ominus> At i \<oplus> At i"
[PROOF STATE]
proof (prove)
using this:
At i \<in># \<Gamma>

goal (1 subgoal):
 1. \<Gamma> = \<Gamma> \<ominus> At i \<oplus> At i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Gamma> = \<Gamma> \<ominus> At i \<oplus> At i

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* At i, 0) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> = \<Gamma> \<ominus> At i \<oplus> At i
[PROOF STEP]
have "extend ((\<Gamma> \<ominus> At i) \<Rightarrow>* Em) (\<LM> At i \<RM> \<Rightarrow>* At i) = (\<Gamma> \<Rightarrow>* At i)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma> = \<Gamma> \<ominus> At i \<oplus> At i

goal (1 subgoal):
 1. extend ( \<Gamma> \<ominus> At i \<Rightarrow>* Em) ( \<LM> At i  \<RM> \<Rightarrow>* At i) = ( \<Gamma> \<Rightarrow>* At i)
[PROOF STEP]
using extend_def[where forms="\<Gamma> \<ominus> At i \<Rightarrow>* Em" and seq="\<LM>At i\<RM> \<Rightarrow>* At i"]
[PROOF STATE]
proof (prove)
using this:
\<Gamma> = \<Gamma> \<ominus> At i \<oplus> At i
extend ( \<Gamma> \<ominus> At i \<Rightarrow>* Em) ( \<LM> At i  \<RM> \<Rightarrow>* At i) \<equiv> if succ ( \<LM> At i  \<RM> \<Rightarrow>* At i) = Em then  antec ( \<Gamma> \<ominus> At i \<Rightarrow>* Em) + antec ( \<LM> At i  \<RM> \<Rightarrow>* At i) \<Rightarrow>* succ ( \<Gamma> \<ominus> At i \<Rightarrow>* Em) else ( antec ( \<Gamma> \<ominus> At i \<Rightarrow>* Em) + antec ( \<LM> At i  \<RM> \<Rightarrow>* At i) \<Rightarrow>* succ ( \<LM> At i  \<RM> \<Rightarrow>* At i))

goal (1 subgoal):
 1. extend ( \<Gamma> \<ominus> At i \<Rightarrow>* Em) ( \<LM> At i  \<RM> \<Rightarrow>* At i) = ( \<Gamma> \<Rightarrow>* At i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
extend ( \<Gamma> \<ominus> At i \<Rightarrow>* Em) ( \<LM> At i  \<RM> \<Rightarrow>* At i) = ( \<Gamma> \<Rightarrow>* At i)

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* At i, 0) \<in> derivable R*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
extend ( \<Gamma> \<ominus> At i \<Rightarrow>* Em) ( \<LM> At i  \<RM> \<Rightarrow>* At i) = ( \<Gamma> \<Rightarrow>* At i)

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* At i, 0) \<in> derivable R*
[PROOF STEP]
have "([],\<LM> At i \<RM> \<Rightarrow>* At i) \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([],  \<LM> At i  \<RM> \<Rightarrow>* At i) \<in> R
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
Ax \<subseteq> R

goal (1 subgoal):
 1. ([],  \<LM> At i  \<RM> \<Rightarrow>* At i) \<in> R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
([],  \<LM> At i  \<RM> \<Rightarrow>* At i) \<in> R

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* At i, 0) \<in> derivable R*
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
extend ( \<Gamma> \<ominus> At i \<Rightarrow>* Em) ( \<LM> At i  \<RM> \<Rightarrow>* At i) = ( \<Gamma> \<Rightarrow>* At i)
([],  \<LM> At i  \<RM> \<Rightarrow>* At i) \<in> R
[PROOF STEP]
have "([],\<Gamma> \<Rightarrow>* At i) \<in> R*"
[PROOF STATE]
proof (prove)
using this:
extend ( \<Gamma> \<ominus> At i \<Rightarrow>* Em) ( \<LM> At i  \<RM> \<Rightarrow>* At i) = ( \<Gamma> \<Rightarrow>* At i)
([],  \<LM> At i  \<RM> \<Rightarrow>* At i) \<in> R

goal (1 subgoal):
 1. ([],  \<Gamma> \<Rightarrow>* At i) \<in> R*
[PROOF STEP]
using extRules.I[where R=R and r="([],  \<LM>At i\<RM> \<Rightarrow>* At i)" and seq="\<Gamma> \<ominus> At i \<Rightarrow>* Em"]
       and extendRule_def[where forms="\<Gamma> \<ominus> At i \<Rightarrow>* Em" and R="([],  \<LM>At i\<RM> \<Rightarrow>* At i)"]
[PROOF STATE]
proof (prove)
using this:
extend ( \<Gamma> \<ominus> At i \<Rightarrow>* Em) ( \<LM> At i  \<RM> \<Rightarrow>* At i) = ( \<Gamma> \<Rightarrow>* At i)
([],  \<LM> At i  \<RM> \<Rightarrow>* At i) \<in> R
([],  \<LM> At i  \<RM> \<Rightarrow>* At i) \<in> R \<Longrightarrow> extendRule ( \<Gamma> \<ominus> At i \<Rightarrow>* Em) ([],  \<LM> At i  \<RM> \<Rightarrow>* At i) \<in> R*
extendRule ( \<Gamma> \<ominus> At i \<Rightarrow>* Em) ([],  \<LM> At i  \<RM> \<Rightarrow>* At i) \<equiv> (map (extend ( \<Gamma> \<ominus> At i \<Rightarrow>* Em)) (fst ([],  \<LM> At i  \<RM> \<Rightarrow>* At i)), extend ( \<Gamma> \<ominus> At i \<Rightarrow>* Em) (snd ([],  \<LM> At i  \<RM> \<Rightarrow>* At i)))

goal (1 subgoal):
 1. ([],  \<Gamma> \<Rightarrow>* At i) \<in> R*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
([],  \<Gamma> \<Rightarrow>* At i) \<in> R*

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* At i, 0) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
([],  \<Gamma> \<Rightarrow>* At i) \<in> R*
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
([],  \<Gamma> \<Rightarrow>* At i) \<in> R*

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* At i, 0) \<in> derivable R*
[PROOF STEP]
using derivable.base[where R="R*" and C="\<Gamma> \<Rightarrow>* At i"]
[PROOF STATE]
proof (prove)
using this:
([],  \<Gamma> \<Rightarrow>* At i) \<in> R*
([],  \<Gamma> \<Rightarrow>* At i) \<in> R* \<Longrightarrow> ( \<Gamma> \<Rightarrow>* At i, 0) \<in> derivable R*

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* At i, 0) \<in> derivable R*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
( \<Gamma> \<Rightarrow>* At i, 0) \<in> derivable R*

goal:
No subgoals!
[PROOF STEP]
qed