[STATEMENT]
lemma obs_split_det:
  assumes "xs@x#xs' = ys@y#ys'"
  and "obs_intra x S \<noteq> {}"
  and "\<forall>x' \<in> set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S"
  and "\<forall>zs z zs'. xs = zs@z#zs' \<and> obs_intra z S \<noteq> {}
  \<longrightarrow> (\<exists>z'' \<in> set (zs'@[x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S)"
  and "obs_intra y S \<noteq> {}"
  and "\<forall>y' \<in> set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S"
  and "\<forall>zs z zs'. ys = zs@z#zs' \<and> obs_intra z S \<noteq> {}
  \<longrightarrow> (\<exists>z'' \<in> set (zs'@[y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)"
  shows "xs = ys \<and> x = y \<and> xs' = ys'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs @ x # xs' = ys @ y # ys'
obs_intra x S \<noteq> {}
\<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S
\<forall>zs z zs'. xs = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S)
obs_intra y S \<noteq> {}
\<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S
\<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)

goal (1 subgoal):
 1. xs = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
proof(induct xs arbitrary:ys)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ys. \<lbrakk>[] @ x # xs' = ys @ y # ys'; obs_intra x S \<noteq> {}; \<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S; \<forall>zs z zs'. [] = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S); obs_intra y S \<noteq> {}; \<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S; \<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)\<rbrakk> \<Longrightarrow> [] = ys \<and> x = y \<and> xs' = ys'
 2. \<And>a xs ys. \<lbrakk>\<And>ys. \<lbrakk>xs @ x # xs' = ys @ y # ys'; obs_intra x S \<noteq> {}; \<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S; \<forall>zs z zs'. xs = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S); obs_intra y S \<noteq> {}; \<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S; \<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)\<rbrakk> \<Longrightarrow> xs = ys \<and> x = y \<and> xs' = ys'; (a # xs) @ x # xs' = ys @ y # ys'; obs_intra x S \<noteq> {}; \<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S; \<forall>zs z zs'. a # xs = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S); obs_intra y S \<noteq> {}; \<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S; \<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)\<rbrakk> \<Longrightarrow> a # xs = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
[] @ x # xs' = ys @ y # ys'
obs_intra x S \<noteq> {}
\<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S
\<forall>zs z zs'. [] = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S)
obs_intra y S \<noteq> {}
\<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S
\<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)

goal (2 subgoals):
 1. \<And>ys. \<lbrakk>[] @ x # xs' = ys @ y # ys'; obs_intra x S \<noteq> {}; \<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S; \<forall>zs z zs'. [] = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S); obs_intra y S \<noteq> {}; \<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S; \<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)\<rbrakk> \<Longrightarrow> [] = ys \<and> x = y \<and> xs' = ys'
 2. \<And>a xs ys. \<lbrakk>\<And>ys. \<lbrakk>xs @ x # xs' = ys @ y # ys'; obs_intra x S \<noteq> {}; \<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S; \<forall>zs z zs'. xs = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S); obs_intra y S \<noteq> {}; \<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S; \<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)\<rbrakk> \<Longrightarrow> xs = ys \<and> x = y \<and> xs' = ys'; (a # xs) @ x # xs' = ys @ y # ys'; obs_intra x S \<noteq> {}; \<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S; \<forall>zs z zs'. a # xs = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S); obs_intra y S \<noteq> {}; \<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S; \<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)\<rbrakk> \<Longrightarrow> a # xs = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
note impy = \<open>\<forall>zs z zs'. ys = zs@z#zs' \<and> obs_intra z S \<noteq> {}
    \<longrightarrow> (\<exists>z'' \<in> set (zs'@[y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)\<close>
[PROOF STATE]
proof (state)
this:
\<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)

goal (2 subgoals):
 1. \<And>ys. \<lbrakk>[] @ x # xs' = ys @ y # ys'; obs_intra x S \<noteq> {}; \<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S; \<forall>zs z zs'. [] = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S); obs_intra y S \<noteq> {}; \<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S; \<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)\<rbrakk> \<Longrightarrow> [] = ys \<and> x = y \<and> xs' = ys'
 2. \<And>a xs ys. \<lbrakk>\<And>ys. \<lbrakk>xs @ x # xs' = ys @ y # ys'; obs_intra x S \<noteq> {}; \<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S; \<forall>zs z zs'. xs = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S); obs_intra y S \<noteq> {}; \<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S; \<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)\<rbrakk> \<Longrightarrow> xs = ys \<and> x = y \<and> xs' = ys'; (a # xs) @ x # xs' = ys @ y # ys'; obs_intra x S \<noteq> {}; \<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S; \<forall>zs z zs'. a # xs = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S); obs_intra y S \<noteq> {}; \<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S; \<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)\<rbrakk> \<Longrightarrow> a # xs = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
proof(cases "ys = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ys = [] \<Longrightarrow> [] = ys \<and> x = y \<and> xs' = ys'
 2. ys \<noteq> [] \<Longrightarrow> [] = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
ys = []

goal (2 subgoals):
 1. ys = [] \<Longrightarrow> [] = ys \<and> x = y \<and> xs' = ys'
 2. ys \<noteq> [] \<Longrightarrow> [] = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
with Nil \<open>[]@x#xs' = ys@y#ys'\<close>
[PROOF STATE]
proof (chain)
picking this:
[] @ x # xs' = ys @ y # ys'
obs_intra x S \<noteq> {}
\<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S
\<forall>zs z zs'. [] = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S)
obs_intra y S \<noteq> {}
\<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S
\<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)
[] @ x # xs' = ys @ y # ys'
ys = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[] @ x # xs' = ys @ y # ys'
obs_intra x S \<noteq> {}
\<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S
\<forall>zs z zs'. [] = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S)
obs_intra y S \<noteq> {}
\<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S
\<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)
[] @ x # xs' = ys @ y # ys'
ys = []

goal (1 subgoal):
 1. [] = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[] = ys \<and> x = y \<and> xs' = ys'

goal (1 subgoal):
 1. ys \<noteq> [] \<Longrightarrow> [] = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ys \<noteq> [] \<Longrightarrow> [] = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
ys \<noteq> []

goal (1 subgoal):
 1. ys \<noteq> [] \<Longrightarrow> [] = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
with \<open>[] @ x # xs' = ys @ y # ys'\<close>
[PROOF STATE]
proof (chain)
picking this:
[] @ x # xs' = ys @ y # ys'
ys \<noteq> []
[PROOF STEP]
obtain zs where "x#zs = ys" and "xs' = zs@y#ys'"
[PROOF STATE]
proof (prove)
using this:
[] @ x # xs' = ys @ y # ys'
ys \<noteq> []

goal (1 subgoal):
 1. (\<And>zs. \<lbrakk>x # zs = ys; xs' = zs @ y # ys'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp:Cons_eq_append_conv)
[PROOF STATE]
proof (state)
this:
x # zs = ys
xs' = zs @ y # ys'

goal (1 subgoal):
 1. ys \<noteq> [] \<Longrightarrow> [] = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
from \<open>x#zs = ys\<close> \<open>obs_intra x S \<noteq> {}\<close> impy
[PROOF STATE]
proof (chain)
picking this:
x # zs = ys
obs_intra x S \<noteq> {}
\<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)
[PROOF STEP]
have "\<exists>z'' \<in> set (zs@[y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S"
[PROOF STATE]
proof (prove)
using this:
x # zs = ys
obs_intra x S \<noteq> {}
\<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)

goal (1 subgoal):
 1. \<exists>z''\<in>set (zs @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>z''\<in>set (zs @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S

goal (1 subgoal):
 1. ys \<noteq> [] \<Longrightarrow> [] = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
with \<open>xs' = zs@y#ys'\<close> \<open>\<forall>x' \<in> set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
xs' = zs @ y # ys'
\<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S
\<exists>z''\<in>set (zs @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
xs' = zs @ y # ys'
\<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S
\<exists>z''\<in>set (zs @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S

goal (1 subgoal):
 1. False
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. ys \<noteq> [] \<Longrightarrow> [] = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. [] = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[] = ys \<and> x = y \<and> xs' = ys'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[] = ys \<and> x = y \<and> xs' = ys'

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. \<lbrakk>xs @ x # xs' = ys @ y # ys'; obs_intra x S \<noteq> {}; \<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S; \<forall>zs z zs'. xs = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S); obs_intra y S \<noteq> {}; \<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S; \<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)\<rbrakk> \<Longrightarrow> xs = ys \<and> x = y \<and> xs' = ys'; (a # xs) @ x # xs' = ys @ y # ys'; obs_intra x S \<noteq> {}; \<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S; \<forall>zs z zs'. a # xs = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S); obs_intra y S \<noteq> {}; \<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S; \<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)\<rbrakk> \<Longrightarrow> a # xs = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. \<lbrakk>xs @ x # xs' = ys @ y # ys'; obs_intra x S \<noteq> {}; \<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S; \<forall>zs z zs'. xs = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S); obs_intra y S \<noteq> {}; \<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S; \<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)\<rbrakk> \<Longrightarrow> xs = ys \<and> x = y \<and> xs' = ys'; (a # xs) @ x # xs' = ys @ y # ys'; obs_intra x S \<noteq> {}; \<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S; \<forall>zs z zs'. a # xs = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S); obs_intra y S \<noteq> {}; \<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S; \<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)\<rbrakk> \<Longrightarrow> a # xs = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
case (Cons w ws)
[PROOF STATE]
proof (state)
this:
\<lbrakk>ws @ x # xs' = ?ys @ y # ys'; obs_intra x S \<noteq> {}; \<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S; \<forall>zs z zs'. ws = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S); obs_intra y S \<noteq> {}; \<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S; \<forall>zs z zs'. ?ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)\<rbrakk> \<Longrightarrow> ws = ?ys \<and> x = y \<and> xs' = ys'
(w # ws) @ x # xs' = ys @ y # ys'
obs_intra x S \<noteq> {}
\<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S
\<forall>zs z zs'. w # ws = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S)
obs_intra y S \<noteq> {}
\<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S
\<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. \<lbrakk>xs @ x # xs' = ys @ y # ys'; obs_intra x S \<noteq> {}; \<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S; \<forall>zs z zs'. xs = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S); obs_intra y S \<noteq> {}; \<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S; \<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)\<rbrakk> \<Longrightarrow> xs = ys \<and> x = y \<and> xs' = ys'; (a # xs) @ x # xs' = ys @ y # ys'; obs_intra x S \<noteq> {}; \<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S; \<forall>zs z zs'. a # xs = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S); obs_intra y S \<noteq> {}; \<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S; \<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)\<rbrakk> \<Longrightarrow> a # xs = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
note IH = \<open>\<And>ys. \<lbrakk>ws @ x # xs' = ys @ y # ys'; obs_intra x S \<noteq> {};
    \<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S;
    \<forall>zs z zs'. ws = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow>
      (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S);
    obs_intra y S \<noteq> {}; \<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S;
    \<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow>
      (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)\<rbrakk>
    \<Longrightarrow> ws = ys \<and> x = y \<and> xs' = ys'\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>ws @ x # xs' = ?ys @ y # ys'; obs_intra x S \<noteq> {}; \<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S; \<forall>zs z zs'. ws = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S); obs_intra y S \<noteq> {}; \<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S; \<forall>zs z zs'. ?ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)\<rbrakk> \<Longrightarrow> ws = ?ys \<and> x = y \<and> xs' = ys'

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. \<lbrakk>xs @ x # xs' = ys @ y # ys'; obs_intra x S \<noteq> {}; \<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S; \<forall>zs z zs'. xs = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S); obs_intra y S \<noteq> {}; \<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S; \<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)\<rbrakk> \<Longrightarrow> xs = ys \<and> x = y \<and> xs' = ys'; (a # xs) @ x # xs' = ys @ y # ys'; obs_intra x S \<noteq> {}; \<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S; \<forall>zs z zs'. a # xs = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S); obs_intra y S \<noteq> {}; \<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S; \<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)\<rbrakk> \<Longrightarrow> a # xs = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
note impw = \<open>\<forall>zs z zs'. w # ws = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow>
    (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S)\<close>
[PROOF STATE]
proof (state)
this:
\<forall>zs z zs'. w # ws = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S)

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. \<lbrakk>xs @ x # xs' = ys @ y # ys'; obs_intra x S \<noteq> {}; \<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S; \<forall>zs z zs'. xs = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S); obs_intra y S \<noteq> {}; \<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S; \<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)\<rbrakk> \<Longrightarrow> xs = ys \<and> x = y \<and> xs' = ys'; (a # xs) @ x # xs' = ys @ y # ys'; obs_intra x S \<noteq> {}; \<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S; \<forall>zs z zs'. a # xs = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S); obs_intra y S \<noteq> {}; \<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S; \<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)\<rbrakk> \<Longrightarrow> a # xs = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
note impy = \<open>\<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow>
    (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)\<close>
[PROOF STATE]
proof (state)
this:
\<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)

goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. \<lbrakk>xs @ x # xs' = ys @ y # ys'; obs_intra x S \<noteq> {}; \<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S; \<forall>zs z zs'. xs = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S); obs_intra y S \<noteq> {}; \<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S; \<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)\<rbrakk> \<Longrightarrow> xs = ys \<and> x = y \<and> xs' = ys'; (a # xs) @ x # xs' = ys @ y # ys'; obs_intra x S \<noteq> {}; \<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S; \<forall>zs z zs'. a # xs = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S); obs_intra y S \<noteq> {}; \<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S; \<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)\<rbrakk> \<Longrightarrow> a # xs = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w # ws = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
proof(cases ys)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ys = [] \<Longrightarrow> w # ws = ys \<and> x = y \<and> xs' = ys'
 2. \<And>a list. ys = a # list \<Longrightarrow> w # ws = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
ys = []

goal (2 subgoals):
 1. ys = [] \<Longrightarrow> w # ws = ys \<and> x = y \<and> xs' = ys'
 2. \<And>a list. ys = a # list \<Longrightarrow> w # ws = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
with \<open>(w#ws) @ x # xs' = ys @ y # ys'\<close>
[PROOF STATE]
proof (chain)
picking this:
(w # ws) @ x # xs' = ys @ y # ys'
ys = []
[PROOF STEP]
have "y = w" and "ys' = ws @ x # xs'"
[PROOF STATE]
proof (prove)
using this:
(w # ws) @ x # xs' = ys @ y # ys'
ys = []

goal (1 subgoal):
 1. y = w &&& ys' = ws @ x # xs'
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
y = w
ys' = ws @ x # xs'

goal (2 subgoals):
 1. ys = [] \<Longrightarrow> w # ws = ys \<and> x = y \<and> xs' = ys'
 2. \<And>a list. ys = a # list \<Longrightarrow> w # ws = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
from \<open>y = w\<close> \<open>obs_intra y S \<noteq> {}\<close> impw
[PROOF STATE]
proof (chain)
picking this:
y = w
obs_intra y S \<noteq> {}
\<forall>zs z zs'. w # ws = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S)
[PROOF STEP]
have "\<exists>z''\<in>set (ws @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S"
[PROOF STATE]
proof (prove)
using this:
y = w
obs_intra y S \<noteq> {}
\<forall>zs z zs'. w # ws = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S)

goal (1 subgoal):
 1. \<exists>z''\<in>set (ws @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>z''\<in>set (ws @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S

goal (2 subgoals):
 1. ys = [] \<Longrightarrow> w # ws = ys \<and> x = y \<and> xs' = ys'
 2. \<And>a list. ys = a # list \<Longrightarrow> w # ws = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
with \<open>ys' = ws @ x # xs'\<close>
      \<open>\<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
ys' = ws @ x # xs'
\<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S
\<exists>z''\<in>set (ws @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
ys' = ws @ x # xs'
\<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S
\<exists>z''\<in>set (ws @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S

goal (1 subgoal):
 1. False
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. ys = [] \<Longrightarrow> w # ws = ys \<and> x = y \<and> xs' = ys'
 2. \<And>a list. ys = a # list \<Longrightarrow> w # ws = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. w # ws = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
w # ws = ys \<and> x = y \<and> xs' = ys'

goal (1 subgoal):
 1. \<And>a list. ys = a # list \<Longrightarrow> w # ws = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. ys = a # list \<Longrightarrow> w # ws = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
case (Cons w' ws')
[PROOF STATE]
proof (state)
this:
ys = w' # ws'

goal (1 subgoal):
 1. \<And>a list. ys = a # list \<Longrightarrow> w # ws = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
with \<open>(w # ws) @ x # xs' = ys @ y # ys'\<close>
[PROOF STATE]
proof (chain)
picking this:
(w # ws) @ x # xs' = ys @ y # ys'
ys = w' # ws'
[PROOF STEP]
have "w = w'"
      and "ws @ x # xs' = ws' @ y # ys'"
[PROOF STATE]
proof (prove)
using this:
(w # ws) @ x # xs' = ys @ y # ys'
ys = w' # ws'

goal (1 subgoal):
 1. w = w' &&& ws @ x # xs' = ws' @ y # ys'
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
w = w'
ws @ x # xs' = ws' @ y # ys'

goal (1 subgoal):
 1. \<And>a list. ys = a # list \<Longrightarrow> w # ws = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
from impw
[PROOF STATE]
proof (chain)
picking this:
\<forall>zs z zs'. w # ws = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S)
[PROOF STEP]
have imp1:"\<forall>zs z zs'. ws = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow>
      (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S)"
[PROOF STATE]
proof (prove)
using this:
\<forall>zs z zs'. w # ws = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S)

goal (1 subgoal):
 1. \<forall>zs z zs'. ws = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S)
[PROOF STEP]
by clarsimp(erule_tac x="w#zs" in allE,clarsimp)
[PROOF STATE]
proof (state)
this:
\<forall>zs z zs'. ws = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [x]). \<exists>nx. call_of_return_node z'' nx \<and> nx \<notin> S)

goal (1 subgoal):
 1. \<And>a list. ys = a # list \<Longrightarrow> w # ws = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
from Cons impy
[PROOF STATE]
proof (chain)
picking this:
ys = w' # ws'
\<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)
[PROOF STEP]
have imp2:"\<forall>zs z zs'. ws' = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow>
      (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)"
[PROOF STATE]
proof (prove)
using this:
ys = w' # ws'
\<forall>zs z zs'. ys = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)

goal (1 subgoal):
 1. \<forall>zs z zs'. ws' = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)
[PROOF STEP]
by clarsimp(erule_tac x="w'#zs" in allE,clarsimp)
[PROOF STATE]
proof (state)
this:
\<forall>zs z zs'. ws' = zs @ z # zs' \<and> obs_intra z S \<noteq> {} \<longrightarrow> (\<exists>z''\<in>set (zs' @ [y]). \<exists>ny. call_of_return_node z'' ny \<and> ny \<notin> S)

goal (1 subgoal):
 1. \<And>a list. ys = a # list \<Longrightarrow> w # ws = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
from IH[OF \<open>ws @ x # xs' = ws' @ y # ys'\<close> \<open>obs_intra x S \<noteq> {}\<close>
      \<open>\<forall>x'\<in>set xs'. \<exists>x''. call_of_return_node x' x'' \<and> x'' \<in> S\<close> imp1
      \<open>obs_intra y S \<noteq> {}\<close> \<open>\<forall>y'\<in>set ys'. \<exists>y''. call_of_return_node y' y'' \<and> y'' \<in> S\<close>
      imp2]
[PROOF STATE]
proof (chain)
picking this:
ws = ws' \<and> x = y \<and> xs' = ys'
[PROOF STEP]
have "ws = ws' \<and> x = y \<and> xs' = ys'"
[PROOF STATE]
proof (prove)
using this:
ws = ws' \<and> x = y \<and> xs' = ys'

goal (1 subgoal):
 1. ws = ws' \<and> x = y \<and> xs' = ys'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ws = ws' \<and> x = y \<and> xs' = ys'

goal (1 subgoal):
 1. \<And>a list. ys = a # list \<Longrightarrow> w # ws = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
with \<open>w = w'\<close> Cons
[PROOF STATE]
proof (chain)
picking this:
w = w'
ys = w' # ws'
ws = ws' \<and> x = y \<and> xs' = ys'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
w = w'
ys = w' # ws'
ws = ws' \<and> x = y \<and> xs' = ys'

goal (1 subgoal):
 1. w # ws = ys \<and> x = y \<and> xs' = ys'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
w # ws = ys \<and> x = y \<and> xs' = ys'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
w # ws = ys \<and> x = y \<and> xs' = ys'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma in_obs_valid:
  assumes "ns' \<in> obs ns S" and "\<forall>n \<in> set ns. valid_node n"
  shows "\<forall>n \<in> set ns'. valid_node n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ball (set ns') valid_node
[PROOF STEP]
using \<open>ns' \<in> obs ns S\<close> \<open>\<forall>n \<in> set ns. valid_node n\<close>
[PROOF STATE]
proof (prove)
using this:
ns' \<in> obs ns S
Ball (set ns) valid_node

goal (1 subgoal):
 1. Ball (set ns') valid_node
[PROOF STEP]
by(induct ns)(auto intro:in_obs_intra_valid simp:Let_def split:if_split_asm)


[STATEMENT]
lemma cmod_cis [simp]:
  assumes "a \<noteq> 0"
  shows "of_real (cmod a) * cis (Arg a) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cor (cmod a) * cis (Arg a) = a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<noteq> 0

goal (1 subgoal):
 1. cor (cmod a) * cis (Arg a) = a
[PROOF STEP]
by (metis rcis_cmod_Arg rcis_def)


[STATEMENT]
lemma cis_cmod [simp]:
  assumes "a \<noteq> 0"
  shows "cis (Arg a) * of_real (cmod a) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cis (Arg a) * cor (cmod a) = a
[PROOF STEP]
by (metis assms cmod_cis mult.commute)


[STATEMENT]
lemma cor_squared:
  shows "(cor x)\<^sup>2 = cor (x\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cor x)\<^sup>2 = cor (x\<^sup>2)
[PROOF STEP]
by (simp add: power2_eq_square)


[STATEMENT]
lemma cor_sqrt_mult_cor_sqrt [simp]:
  shows "cor (sqrt A) * cor (sqrt A) = cor \<bar>A\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cor (sqrt A) * cor (sqrt A) = cor \<bar>A\<bar>
[PROOF STEP]
by (metis of_real_mult real_sqrt_mult_self)


[STATEMENT]
lemma cor_eq_0: "cor x + \<i> * cor y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cor x + \<i> * cor y = 0) = (x = 0 \<and> y = 0)
[PROOF STEP]
by (metis Complex_eq Im_complex_of_real Im_i_times Re_complex_of_real add_cancel_left_left of_real_eq_0_iff plus_complex.sel(2) zero_complex.code)


[STATEMENT]
lemma one_plus_square_neq_zero [simp]:
  shows "1 + (cor x)\<^sup>2 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + (cor x)\<^sup>2 \<noteq> 0
[PROOF STEP]
by (metis (opaque_lifting, no_types) of_real_1 of_real_add of_real_eq_0_iff of_real_power power_one sum_power2_eq_zero_iff zero_neq_one)


[STATEMENT]
lemma complex_real_two [simp]:
  shows "Complex 2 0 = 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complex 2 0 = 2
[PROOF STEP]
by (simp add: Complex_eq)


[STATEMENT]
lemma complex_double [simp]:
  shows "(Complex a b) * 2 = Complex (2*a) (2*b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complex a b * 2 = Complex (2 * a) (2 * b)
[PROOF STEP]
by (simp add: Complex_eq)


[STATEMENT]
lemma complex_half [simp]:
  shows "(Complex a b) / 2 = Complex (a/2) (b/2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complex a b / 2 = Complex (a / 2) (b / 2)
[PROOF STEP]
by (subst complex_eq_iff) auto


[STATEMENT]
lemma Complex_scale1:
  shows "Complex (a * b) (a * c) = cor a * Complex b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complex (a * b) (a * c) = cor a * Complex b c
[PROOF STEP]
unfolding complex_of_real_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complex (a * b) (a * c) = Complex a 0 * Complex b c
[PROOF STEP]
unfolding Complex_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cor (a * b) + \<i> * cor (a * c) = (cor a + \<i> * cor 0) * (cor b + \<i> * cor c)
[PROOF STEP]
by (auto simp add: field_simps)


[STATEMENT]
lemma Complex_scale2:
  shows "Complex (a * c) (b * c) = Complex a b * cor c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complex (a * c) (b * c) = Complex a b * cor c
[PROOF STEP]
unfolding complex_of_real_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complex (a * c) (b * c) = Complex a b * Complex c 0
[PROOF STEP]
unfolding Complex_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cor (a * c) + \<i> * cor (b * c) = (cor a + \<i> * cor b) * (cor c + \<i> * cor 0)
[PROOF STEP]
by (auto simp add: field_simps)


[STATEMENT]
lemma Complex_scale3:
  shows "Complex (a / b) (a / c) = cor a * Complex (1 / b) (1 / c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complex (a / b) (a / c) = cor a * Complex (1 / b) (1 / c)
[PROOF STEP]
unfolding complex_of_real_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complex (a / b) (a / c) = Complex a 0 * Complex (1 / b) (1 / c)
[PROOF STEP]
unfolding Complex_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cor (a / b) + \<i> * cor (a / c) = (cor a + \<i> * cor 0) * (cor (1 / b) + \<i> * cor (1 / c))
[PROOF STEP]
by (auto simp add: field_simps)


[STATEMENT]
lemma Complex_scale4:
  shows "c \<noteq> 0 \<Longrightarrow> Complex (a / c) (b / c) = Complex a b / cor c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> Complex (a / c) (b / c) = Complex a b / cor c
[PROOF STEP]
unfolding complex_of_real_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> Complex (a / c) (b / c) = Complex a b / Complex c 0
[PROOF STEP]
unfolding Complex_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> cor (a / c) + \<i> * cor (b / c) = (cor a + \<i> * cor b) / (cor c + \<i> * cor 0)
[PROOF STEP]
by (auto simp add: field_simps power2_eq_square)


[STATEMENT]
lemma Complex_Re_express_cnj:
  shows "Complex (Re z) 0 = (z + cnj z) / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complex (Re z) 0 = (z + cnj z) / 2
[PROOF STEP]
by (cases z) (simp add: Complex_eq)


[STATEMENT]
lemma Complex_Im_express_cnj:
  shows "Complex 0 (Im z) = (z - cnj z)/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complex 0 (Im z) = (z - cnj z) / 2
[PROOF STEP]
by (cases z) (simp add: Complex_eq)


[STATEMENT]
lemma complex_mult_cnj_cmod:
  shows "z * cnj z = cor ((cmod z)\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z * cnj z = cor ((cmod z)\<^sup>2)
[PROOF STEP]
using complex_norm_square
[PROOF STATE]
proof (prove)
using this:
cor ((cmod ?z)\<^sup>2) = ?z * cnj ?z

goal (1 subgoal):
 1. z * cnj z = cor ((cmod z)\<^sup>2)
[PROOF STEP]
by auto


[STATEMENT]
lemma cmod_square:
  shows "(cmod z)\<^sup>2 = Re (z * cnj z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod z)\<^sup>2 = Re (z * cnj z)
[PROOF STEP]
using complex_mult_cnj_cmod[of z]
[PROOF STATE]
proof (prove)
using this:
z * cnj z = cor ((cmod z)\<^sup>2)

goal (1 subgoal):
 1. (cmod z)\<^sup>2 = Re (z * cnj z)
[PROOF STEP]
by (simp add: power2_eq_square)


[STATEMENT]
lemma cnjE:
  assumes "x \<noteq> 0"
  shows "cnj x = cor ((cmod x)\<^sup>2) / x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj x = cor ((cmod x)\<^sup>2) / x
[PROOF STEP]
using complex_mult_cnj_cmod[of x] assms
[PROOF STATE]
proof (prove)
using this:
x * cnj x = cor ((cmod x)\<^sup>2)
x \<noteq> 0

goal (1 subgoal):
 1. cnj x = cor ((cmod x)\<^sup>2) / x
[PROOF STEP]
by (auto simp add: field_simps)


[STATEMENT]
lemma cmod_cor_divide [simp]:
  shows "cmod (z / cor k) = cmod z / \<bar>k\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (z / cor k) = cmod z / \<bar>k\<bar>
[PROOF STEP]
by (simp add: norm_divide)


[STATEMENT]
lemma cmod_mult_minus_left_distrib [simp]:
  shows "cmod (z*z1 - z*z2) = cmod z * cmod(z1 - z2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (z * z1 - z * z2) = cmod z * cmod (z1 - z2)
[PROOF STEP]
by (metis norm_mult right_diff_distrib)


[STATEMENT]
lemma cmod_eqI:
  assumes "z1 * cnj z1 = z2 * cnj z2"
  shows "cmod z1 = cmod z2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod z1 = cmod z2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
z1 * cnj z1 = z2 * cnj z2

goal (1 subgoal):
 1. cmod z1 = cmod z2
[PROOF STEP]
by (subst complex_mod_sqrt_Re_mult_cnj)+ auto


[STATEMENT]
lemma cmod_eqE:
  assumes "cmod z1 = cmod z2"
  shows "z1 * cnj z1 = z2 * cnj z2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z1 * cnj z1 = z2 * cnj z2
[PROOF STEP]
by (simp add: assms complex_mult_cnj_cmod)


[STATEMENT]
lemma cmod_eq_one [simp]:
  shows "cmod a = 1 \<longleftrightarrow> a*cnj a = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod a = 1) = (a * cnj a = 1)
[PROOF STEP]
by (metis cmod_eqE cmod_eqI complex_cnj_one monoid_mult_class.mult.left_neutral norm_one)


[STATEMENT]
lemma real_imag_0:
  assumes "is_real a" "is_imag a"
  shows "a = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_real a
is_imag a

goal (1 subgoal):
 1. a = 0
[PROOF STEP]
by (simp add: complex.expand)


[STATEMENT]
lemma complex_eq_if_Re_eq:
  assumes "is_real z1" and "is_real z2"
  shows "z1 = z2 \<longleftrightarrow> Re z1 = Re z2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (z1 = z2) = (Re z1 = Re z2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_real z1
is_real z2

goal (1 subgoal):
 1. (z1 = z2) = (Re z1 = Re z2)
[PROOF STEP]
by (cases z1, cases z2) auto


[STATEMENT]
lemma mult_reals [simp]:
  assumes "is_real a" and "is_real b"
  shows "is_real (a * b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_real (a * b)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_real a
is_real b

goal (1 subgoal):
 1. is_real (a * b)
[PROOF STEP]
by auto


[STATEMENT]
lemma div_reals [simp]:
  assumes "is_real a" and "is_real b"
  shows "is_real (a / b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_real (a / b)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_real a
is_real b

goal (1 subgoal):
 1. is_real (a / b)
[PROOF STEP]
by (simp add: complex_is_Real_iff)


[STATEMENT]
lemma complex_of_real_Re [simp]:
  assumes "is_real k"
  shows "cor (Re k) = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cor (Re k) = k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_real k

goal (1 subgoal):
 1. cor (Re k) = k
[PROOF STEP]
by (cases k) (auto simp add: complex_of_real_def)


[STATEMENT]
lemma cor_cmod_real:
  assumes "is_real a"
  shows "cor (cmod a) = a \<or> cor (cmod a) = -a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cor (cmod a) = a \<or> cor (cmod a) = - a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_real a

goal (1 subgoal):
 1. cor (cmod a) = a \<or> cor (cmod a) = - a
[PROOF STEP]
unfolding cmod_def
[PROOF STATE]
proof (prove)
using this:
is_real a

goal (1 subgoal):
 1. cor (sqrt ((Re a)\<^sup>2 + (Im a)\<^sup>2)) = a \<or> cor (sqrt ((Re a)\<^sup>2 + (Im a)\<^sup>2)) = - a
[PROOF STEP]
by (cases "Re a > 0") auto


[STATEMENT]
lemma eq_cnj_iff_real:
  shows "cnj z = z \<longleftrightarrow> is_real z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cnj z = z) = is_real z
[PROOF STEP]
by (cases z) (simp add: Complex_eq)


[STATEMENT]
lemma eq_minus_cnj_iff_imag:
  shows "cnj z = -z \<longleftrightarrow> is_imag z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cnj z = - z) = is_imag z
[PROOF STEP]
by (cases z) (simp add: Complex_eq)


[STATEMENT]
lemma Re_divide_real:
  assumes "is_real b" and "b \<noteq> 0"
  shows "Re (a / b) = (Re a) / (Re b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re (a / b) = Re a / Re b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_real b
b \<noteq> 0

goal (1 subgoal):
 1. Re (a / b) = Re a / Re b
[PROOF STEP]
by (simp add: complex_is_Real_iff)


[STATEMENT]
lemma Re_mult_real:
  assumes "is_real a"
  shows "Re (a * b) = (Re a) * (Re b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re (a * b) = Re a * Re b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_real a

goal (1 subgoal):
 1. Re (a * b) = Re a * Re b
[PROOF STEP]
by simp


[STATEMENT]
lemma Im_mult_real:
  assumes "is_real a"
  shows "Im (a * b) = (Re a) * (Im b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Im (a * b) = Re a * Im b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_real a

goal (1 subgoal):
 1. Im (a * b) = Re a * Im b
[PROOF STEP]
by simp


[STATEMENT]
lemma Im_divide_real:
  assumes "is_real b" and "b \<noteq> 0"
  shows "Im (a / b) = (Im a) / (Re b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Im (a / b) = Im a / Re b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_real b
b \<noteq> 0

goal (1 subgoal):
 1. Im (a / b) = Im a / Re b
[PROOF STEP]
by (simp add: complex_is_Real_iff)


[STATEMENT]
lemma Re_sgn:
  assumes "is_real R"
  shows "Re (sgn R) = sgn (Re R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re (sgn R) = sgn (Re R)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_real R

goal (1 subgoal):
 1. Re (sgn R) = sgn (Re R)
[PROOF STEP]
by (metis Re_sgn complex_of_real_Re norm_of_real real_sgn_eq)


[STATEMENT]
lemma is_real_div:
  assumes "b \<noteq> 0"
  shows "is_real (a / b) \<longleftrightarrow> a*cnj b = b*cnj a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_real (a / b) = (a * cnj b = b * cnj a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
b \<noteq> 0

goal (1 subgoal):
 1. is_real (a / b) = (a * cnj b = b * cnj a)
[PROOF STEP]
by (metis complex_cnj_divide complex_cnj_zero_iff eq_cnj_iff_real frac_eq_eq mult.commute)


[STATEMENT]
lemma is_real_mult_real:
  assumes "is_real a" and "a \<noteq> 0"
  shows "is_real b \<longleftrightarrow> is_real (a * b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_real b = is_real (a * b)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_real a
a \<noteq> 0

goal (1 subgoal):
 1. is_real b = is_real (a * b)
[PROOF STEP]
by (cases a, auto simp add: Complex_eq)


[STATEMENT]
lemma Im_express_cnj:
  shows "Im z = (z - cnj z) / (2 * \<i>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cor (Im z) = (z - cnj z) / (2 * \<i>)
[PROOF STEP]
by (simp add: complex_diff_cnj field_simps)


[STATEMENT]
lemma Re_express_cnj:
  shows "Re z = (z + cnj z) / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cor (Re z) = (z + cnj z) / 2
[PROOF STEP]
by (simp add: complex_add_cnj)


[STATEMENT]
lemma rot90_ii:
  shows "rot90 z = z * \<i>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rot90 z = z * \<i>
[PROOF STEP]
by (metis Complex_mult_i complex_surj)


[STATEMENT]
lemma cnj_mix_minus:
  shows "cnj z1*z2 - z1*cnj z2 = \<i> * cnj_mix (rot90 z1) z2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj z1 * z2 - z1 * cnj z2 = \<i> * cnj_mix (rot90 z1) z2
[PROOF STEP]
by (cases z1, cases z2) (simp add: Complex_eq field_simps)


[STATEMENT]
lemma cnj_mix_minus':
  shows "cnj z1*z2 - z1*cnj z2 = rot90 (cnj_mix (rot90 z1) z2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj z1 * z2 - z1 * cnj z2 = rot90 (cnj_mix (rot90 z1) z2)
[PROOF STEP]
by (cases z1, cases z2) (simp add: Complex_eq field_simps)


[STATEMENT]
lemma cnj_mix_real [simp]:
  shows "is_real (cnj_mix z1 z2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_real (cnj_mix z1 z2)
[PROOF STEP]
by (cases z1, cases z2) simp


[STATEMENT]
lemma scalprod_real [simp]:
  shows "is_real (scalprod z1 z2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_real (scalprod z1 z2)
[PROOF STEP]
using cnj_mix_real
[PROOF STATE]
proof (prove)
using this:
is_real (cnj_mix ?z1.0 ?z2.0)

goal (1 subgoal):
 1. is_real (scalprod z1 z2)
[PROOF STEP]
by simp


[STATEMENT]
lemma cis_minus_pi2 [simp]:
  shows "cis (-pi/2) = -\<i>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cis (- pi / 2) = - \<i>
[PROOF STEP]
by (simp add: cis_inverse[symmetric])


[STATEMENT]
lemma cis_pi2_minus_x [simp]:
  shows "cis (pi/2 - x) = \<i> * cis(-x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cis (pi / 2 - x) = \<i> * cis (- x)
[PROOF STEP]
using cis_divide[of "pi/2" x, symmetric]
[PROOF STATE]
proof (prove)
using this:
cis (pi / 2 - x) = cis (pi / 2) / cis x

goal (1 subgoal):
 1. cis (pi / 2 - x) = \<i> * cis (- x)
[PROOF STEP]
using cis_divide[of 0 x, symmetric]
[PROOF STATE]
proof (prove)
using this:
cis (pi / 2 - x) = cis (pi / 2) / cis x
cis (0 - x) = cis 0 / cis x

goal (1 subgoal):
 1. cis (pi / 2 - x) = \<i> * cis (- x)
[PROOF STEP]
by simp


[STATEMENT]
lemma cis_pm_pi [simp]:
  shows "cis (x - pi) = - cis x" and  "cis (x + pi) = - cis x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cis (x - pi) = - cis x &&& cis (x + pi) = - cis x
[PROOF STEP]
by (simp add: cis.ctr complex_minus)+


[STATEMENT]
lemma cis_times_cis_opposite [simp]:
  shows "cis \<phi> * cis (- \<phi>) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cis \<phi> * cis (- \<phi>) = 1
[PROOF STEP]
by (simp add: cis_mult)


[STATEMENT]
lemma cis_eq:
  assumes "cis a = cis b"
  shows "\<exists> k::int. a - b = 2 * k * pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. a - b = 2 * real_of_int x * pi
[PROOF STEP]
using assms sin_cos_eq[of a b]
[PROOF STATE]
proof (prove)
using this:
cis a = cis b
\<lbrakk>cos a = cos b; sin a = sin b\<rbrakk> \<Longrightarrow> \<exists>x. a - b = 2 * real_of_int x * pi

goal (1 subgoal):
 1. \<exists>x. a - b = 2 * real_of_int x * pi
[PROOF STEP]
using cis.sel[of a] cis.sel[of b]
[PROOF STATE]
proof (prove)
using this:
cis a = cis b
\<lbrakk>cos a = cos b; sin a = sin b\<rbrakk> \<Longrightarrow> \<exists>x. a - b = 2 * real_of_int x * pi
Re (cis a) = cos a
Im (cis a) = sin a
Re (cis b) = cos b
Im (cis b) = sin b

goal (1 subgoal):
 1. \<exists>x. a - b = 2 * real_of_int x * pi
[PROOF STEP]
by (cases "cis a", cases "cis b") auto


[STATEMENT]
lemma cis_inj:
  assumes "-pi < \<alpha>" and "\<alpha> \<le> pi" and "-pi < \<alpha>'" and "\<alpha>' \<le> pi"
  assumes "cis \<alpha> = cis \<alpha>'"
  shows "\<alpha> = \<alpha>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> = \<alpha>'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
- pi < \<alpha>
\<alpha> \<le> pi
- pi < \<alpha>'
\<alpha>' \<le> pi
cis \<alpha> = cis \<alpha>'

goal (1 subgoal):
 1. \<alpha> = \<alpha>'
[PROOF STEP]
by (metis cis_Arg_unique sgn_cis)


[STATEMENT]
lemma cis_diff_cis_opposite [simp]:
  shows "cis \<phi> - cis (- \<phi>) = 2 * \<i> * sin \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cis \<phi> - cis (- \<phi>) = 2 * \<i> * cor (sin \<phi>)
[PROOF STEP]
using Im_express_cnj[of "cis \<phi>"]
[PROOF STATE]
proof (prove)
using this:
cor (Im (cis \<phi>)) = (cis \<phi> - cnj (cis \<phi>)) / (2 * \<i>)

goal (1 subgoal):
 1. cis \<phi> - cis (- \<phi>) = 2 * \<i> * cor (sin \<phi>)
[PROOF STEP]
by simp


[STATEMENT]
lemma cis_opposite_diff_cis [simp]:
  shows "cis (-\<phi>) - cis (\<phi>) = - 2 * \<i> * sin \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cis (- \<phi>) - cis \<phi> = - 2 * \<i> * cor (sin \<phi>)
[PROOF STEP]
using cis_diff_cis_opposite[of "-\<phi>"]
[PROOF STATE]
proof (prove)
using this:
cis (- \<phi>) - cis (- (- \<phi>)) = 2 * \<i> * cor (sin (- \<phi>))

goal (1 subgoal):
 1. cis (- \<phi>) - cis \<phi> = - 2 * \<i> * cor (sin \<phi>)
[PROOF STEP]
by simp


[STATEMENT]
lemma cis_add_cis_opposite [simp]:
  shows "cis \<phi> + cis (-\<phi>) = 2 * cos \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cis \<phi> + cis (- \<phi>) = cor (2 * cos \<phi>)
[PROOF STEP]
by (metis cis.sel(1) cis_cnj complex_add_cnj)


[STATEMENT]
lemma cis_one [simp]:
  assumes "sin \<phi> = 0" and "cos \<phi> = 1"
  shows "cis \<phi> = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cis \<phi> = 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sin \<phi> = 0
cos \<phi> = 1

goal (1 subgoal):
 1. cis \<phi> = 1
[PROOF STEP]
by (auto simp add: cis.ctr one_complex.code)


[STATEMENT]
lemma cis_minus_one [simp]:
  assumes "sin \<phi> = 0" and "cos \<phi> = -1"
  shows "cis \<phi> = -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cis \<phi> = - 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sin \<phi> = 0
cos \<phi> = - 1

goal (1 subgoal):
 1. cis \<phi> = - 1
[PROOF STEP]
by (auto simp add: cis.ctr Complex_eq_neg_1)


[STATEMENT]
lemma is_real_arg1:
  assumes "Arg z = 0 \<or> Arg z = pi"
  shows "is_real z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_real z
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Arg z = 0 \<or> Arg z = pi

goal (1 subgoal):
 1. is_real z
[PROOF STEP]
using rcis_cmod_Arg[of z] Im_rcis[of "cmod z" "Arg z"]
[PROOF STATE]
proof (prove)
using this:
Arg z = 0 \<or> Arg z = pi
rcis (cmod z) (Arg z) = z
Im (rcis (cmod z) (Arg z)) = cmod z * sin (Arg z)

goal (1 subgoal):
 1. is_real z
[PROOF STEP]
by auto


[STATEMENT]
lemma is_real_arg2:
  assumes "is_real z"
  shows "Arg z = 0 \<or> Arg z = pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arg z = 0 \<or> Arg z = pi
[PROOF STEP]
proof (cases "z = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z = 0 \<Longrightarrow> Arg z = 0 \<or> Arg z = pi
 2. z \<noteq> 0 \<Longrightarrow> Arg z = 0 \<or> Arg z = pi
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
z \<noteq> 0

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> Arg z = 0 \<or> Arg z = pi
 2. z \<noteq> 0 \<Longrightarrow> Arg z = 0 \<or> Arg z = pi
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0

goal (1 subgoal):
 1. Arg z = 0 \<or> Arg z = pi
[PROOF STEP]
using Arg_bounded[of z]
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0
- pi < Arg z \<and> Arg z \<le> pi

goal (1 subgoal):
 1. Arg z = 0 \<or> Arg z = pi
[PROOF STEP]
by (smt (verit, best) Im_sgn assms cis.simps(2) cis_Arg div_0 sin_zero_pi_iff)
[PROOF STATE]
proof (state)
this:
Arg z = 0 \<or> Arg z = pi

goal (1 subgoal):
 1. z = 0 \<Longrightarrow> Arg z = 0 \<or> Arg z = pi
[PROOF STEP]
qed (auto simp add: Arg_zero)


[STATEMENT]
lemma arg_complex_of_real_positive [simp]:
  assumes "k > 0"
  shows "Arg (cor k) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arg (cor k) = 0
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Arg (cor k) = 0
[PROOF STEP]
have "cos (Arg (Complex k 0)) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < cos (Arg (Complex k 0))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < k

goal (1 subgoal):
 1. 0 < cos (Arg (Complex k 0))
[PROOF STEP]
using rcis_cmod_Arg[of "Complex k 0"] Re_rcis[of "cmod (Complex k 0)" "Arg (Complex k 0)"]
[PROOF STATE]
proof (prove)
using this:
0 < k
rcis (cmod (Complex k 0)) (Arg (Complex k 0)) = Complex k 0
Re (rcis (cmod (Complex k 0)) (Arg (Complex k 0))) = cmod (Complex k 0) * cos (Arg (Complex k 0))

goal (1 subgoal):
 1. 0 < cos (Arg (Complex k 0))
[PROOF STEP]
using cmod_eq_Re
[PROOF STATE]
proof (prove)
using this:
0 < k
rcis (cmod (Complex k 0)) (Arg (Complex k 0)) = Complex k 0
Re (rcis (cmod (Complex k 0)) (Arg (Complex k 0))) = cmod (Complex k 0) * cos (Arg (Complex k 0))
is_real ?z \<Longrightarrow> cmod ?z = \<bar>Re ?z\<bar>

goal (1 subgoal):
 1. 0 < cos (Arg (Complex k 0))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
0 < cos (Arg (Complex k 0))

goal (1 subgoal):
 1. Arg (cor k) = 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < cos (Arg (Complex k 0))

goal (1 subgoal):
 1. Arg (cor k) = 0
[PROOF STEP]
using assms is_real_arg2[of "cor k"]
[PROOF STATE]
proof (prove)
using this:
0 < cos (Arg (Complex k 0))
0 < k
is_real (cor k) \<Longrightarrow> Arg (cor k) = 0 \<or> Arg (cor k) = pi

goal (1 subgoal):
 1. Arg (cor k) = 0
[PROOF STEP]
unfolding complex_of_real_def
[PROOF STATE]
proof (prove)
using this:
0 < cos (Arg (Complex k 0))
0 < k
is_real (Complex k 0) \<Longrightarrow> Arg (Complex k 0) = 0 \<or> Arg (Complex k 0) = pi

goal (1 subgoal):
 1. Arg (Complex k 0) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Arg (cor k) = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arg_complex_of_real_negative [simp]:
  assumes "k < 0"
  shows "Arg (cor k) = pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arg (cor k) = pi
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Arg (cor k) = pi
[PROOF STEP]
have "cos (Arg (Complex k 0)) < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cos (Arg (Complex k 0)) < 0
[PROOF STEP]
using \<open>k < 0\<close> rcis_cmod_Arg[of "Complex k 0"] Re_rcis[of "cmod (Complex k 0)" "Arg (Complex k 0)"]
[PROOF STATE]
proof (prove)
using this:
k < 0
rcis (cmod (Complex k 0)) (Arg (Complex k 0)) = Complex k 0
Re (rcis (cmod (Complex k 0)) (Arg (Complex k 0))) = cmod (Complex k 0) * cos (Arg (Complex k 0))

goal (1 subgoal):
 1. cos (Arg (Complex k 0)) < 0
[PROOF STEP]
by (metis complex.sel(1) mult_less_0_iff norm_not_less_zero)
[PROOF STATE]
proof (state)
this:
cos (Arg (Complex k 0)) < 0

goal (1 subgoal):
 1. Arg (cor k) = pi
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
cos (Arg (Complex k 0)) < 0

goal (1 subgoal):
 1. Arg (cor k) = pi
[PROOF STEP]
using assms is_real_arg2[of "cor k"]
[PROOF STATE]
proof (prove)
using this:
cos (Arg (Complex k 0)) < 0
k < 0
is_real (cor k) \<Longrightarrow> Arg (cor k) = 0 \<or> Arg (cor k) = pi

goal (1 subgoal):
 1. Arg (cor k) = pi
[PROOF STEP]
unfolding complex_of_real_def
[PROOF STATE]
proof (prove)
using this:
cos (Arg (Complex k 0)) < 0
k < 0
is_real (Complex k 0) \<Longrightarrow> Arg (Complex k 0) = 0 \<or> Arg (Complex k 0) = pi

goal (1 subgoal):
 1. Arg (Complex k 0) = pi
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Arg (cor k) = pi

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arg_0_iff:
  shows "z \<noteq> 0 \<and> Arg z = 0 \<longleftrightarrow> is_real z \<and> Re z > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (z \<noteq> 0 \<and> Arg z = 0) = (is_real z \<and> 0 < Re z)
[PROOF STEP]
by (smt arg_complex_of_real_negative arg_complex_of_real_positive Arg_zero complex_of_real_Re is_real_arg1 pi_gt_zero zero_complex.simps)


[STATEMENT]
lemma arg_pi_iff:
  shows "Arg z = pi \<longleftrightarrow> is_real z \<and> Re z < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Arg z = pi) = (is_real z \<and> Re z < 0)
[PROOF STEP]
by (smt arg_complex_of_real_negative arg_complex_of_real_positive Arg_zero complex_of_real_Re is_real_arg1 pi_gt_zero zero_complex.simps)


[STATEMENT]
lemma is_imag_arg1:
  assumes "Arg z = pi/2 \<or> Arg z = -pi/2"
  shows "is_imag z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_imag z
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Arg z = pi / 2 \<or> Arg z = - pi / 2

goal (1 subgoal):
 1. is_imag z
[PROOF STEP]
using rcis_cmod_Arg[of z] Re_rcis[of "cmod z" "Arg z"]
[PROOF STATE]
proof (prove)
using this:
Arg z = pi / 2 \<or> Arg z = - pi / 2
rcis (cmod z) (Arg z) = z
Re (rcis (cmod z) (Arg z)) = cmod z * cos (Arg z)

goal (1 subgoal):
 1. is_imag z
[PROOF STEP]
by (metis cos_minus cos_pi_half minus_divide_left mult_eq_0_iff)


[STATEMENT]
lemma is_imag_arg2:
  assumes "is_imag z" and "z \<noteq> 0"
  shows "Arg z = pi/2 \<or> Arg z = -pi/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arg z = pi / 2 \<or> Arg z = - pi / 2
[PROOF STEP]
using Arg_bounded assms cos_0_iff_canon cos_Arg_i_mult_zero
[PROOF STATE]
proof (prove)
using this:
- pi < Arg ?z \<and> Arg ?z \<le> pi
is_imag z
z \<noteq> 0
\<lbrakk>cos ?\<phi> = 0; - pi < ?\<phi>; ?\<phi> \<le> pi\<rbrakk> \<Longrightarrow> ?\<phi> = pi / 2 \<or> ?\<phi> = - pi / 2
\<lbrakk>?y \<noteq> 0; is_imag ?y\<rbrakk> \<Longrightarrow> cos (Arg ?y) = 0

goal (1 subgoal):
 1. Arg z = pi / 2 \<or> Arg z = - pi / 2
[PROOF STEP]
by presburger


[STATEMENT]
lemma arg_complex_of_real_times_i_positive [simp]:
  assumes "k > 0"
  shows "Arg (cor k * \<i>) = pi / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arg (cor k * \<i>) = pi / 2
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Arg (cor k * \<i>) = pi / 2
[PROOF STEP]
have "sin (Arg (Complex 0 k)) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < sin (Arg (Complex 0 k))
[PROOF STEP]
using \<open>k > 0\<close> rcis_cmod_Arg[of "Complex 0 k"] Im_rcis[of "cmod (Complex 0 k)" "Arg (Complex 0 k)"]
[PROOF STATE]
proof (prove)
using this:
0 < k
rcis (cmod (Complex 0 k)) (Arg (Complex 0 k)) = Complex 0 k
Im (rcis (cmod (Complex 0 k)) (Arg (Complex 0 k))) = cmod (Complex 0 k) * sin (Arg (Complex 0 k))

goal (1 subgoal):
 1. 0 < sin (Arg (Complex 0 k))
[PROOF STEP]
by (smt complex.sel(2) mult_nonneg_nonpos norm_ge_zero)
[PROOF STATE]
proof (state)
this:
0 < sin (Arg (Complex 0 k))

goal (1 subgoal):
 1. Arg (cor k * \<i>) = pi / 2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < sin (Arg (Complex 0 k))

goal (1 subgoal):
 1. Arg (cor k * \<i>) = pi / 2
[PROOF STEP]
using assms is_imag_arg2[of "cor k * \<i>"]
[PROOF STATE]
proof (prove)
using this:
0 < sin (Arg (Complex 0 k))
0 < k
\<lbrakk>is_imag (cor k * \<i>); cor k * \<i> \<noteq> 0\<rbrakk> \<Longrightarrow> Arg (cor k * \<i>) = pi / 2 \<or> Arg (cor k * \<i>) = - pi / 2

goal (1 subgoal):
 1. Arg (cor k * \<i>) = pi / 2
[PROOF STEP]
using Arg_zero complex_of_real_i
[PROOF STATE]
proof (prove)
using this:
0 < sin (Arg (Complex 0 k))
0 < k
\<lbrakk>is_imag (cor k * \<i>); cor k * \<i> \<noteq> 0\<rbrakk> \<Longrightarrow> Arg (cor k * \<i>) = pi / 2 \<or> Arg (cor k * \<i>) = - pi / 2
Arg 0 = 0
cor ?r * \<i> = Complex 0 ?r

goal (1 subgoal):
 1. Arg (cor k * \<i>) = pi / 2
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Arg (cor k * \<i>) = pi / 2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arg_complex_of_real_times_i_negative [simp]:
  assumes "k < 0"
  shows "Arg (cor k * \<i>) = - pi / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arg (cor k * \<i>) = - pi / 2
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Arg (cor k * \<i>) = - pi / 2
[PROOF STEP]
have "sin (Arg (Complex 0 k)) < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sin (Arg (Complex 0 k)) < 0
[PROOF STEP]
using \<open>k < 0\<close> rcis_cmod_Arg[of "Complex 0 k"] Im_rcis[of "cmod (Complex 0 k)" "Arg (Complex 0 k)"]
[PROOF STATE]
proof (prove)
using this:
k < 0
rcis (cmod (Complex 0 k)) (Arg (Complex 0 k)) = Complex 0 k
Im (rcis (cmod (Complex 0 k)) (Arg (Complex 0 k))) = cmod (Complex 0 k) * sin (Arg (Complex 0 k))

goal (1 subgoal):
 1. sin (Arg (Complex 0 k)) < 0
[PROOF STEP]
by (metis complex.sel(2) mult_less_0_iff norm_not_less_zero)
[PROOF STATE]
proof (state)
this:
sin (Arg (Complex 0 k)) < 0

goal (1 subgoal):
 1. Arg (cor k * \<i>) = - pi / 2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
sin (Arg (Complex 0 k)) < 0

goal (1 subgoal):
 1. Arg (cor k * \<i>) = - pi / 2
[PROOF STEP]
using assms is_imag_arg2[of "cor k * \<i>"]
[PROOF STATE]
proof (prove)
using this:
sin (Arg (Complex 0 k)) < 0
k < 0
\<lbrakk>is_imag (cor k * \<i>); cor k * \<i> \<noteq> 0\<rbrakk> \<Longrightarrow> Arg (cor k * \<i>) = pi / 2 \<or> Arg (cor k * \<i>) = - pi / 2

goal (1 subgoal):
 1. Arg (cor k * \<i>) = - pi / 2
[PROOF STEP]
using Arg_zero complex_of_real_i[of k]
[PROOF STATE]
proof (prove)
using this:
sin (Arg (Complex 0 k)) < 0
k < 0
\<lbrakk>is_imag (cor k * \<i>); cor k * \<i> \<noteq> 0\<rbrakk> \<Longrightarrow> Arg (cor k * \<i>) = pi / 2 \<or> Arg (cor k * \<i>) = - pi / 2
Arg 0 = 0
cor k * \<i> = Complex 0 k

goal (1 subgoal):
 1. Arg (cor k * \<i>) = - pi / 2
[PROOF STEP]
by (smt complex.sel(1) sin_pi_half sin_zero)
[PROOF STATE]
proof (state)
this:
Arg (cor k * \<i>) = - pi / 2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arg_pi2_iff:
  shows "z \<noteq> 0 \<and> Arg z = pi / 2 \<longleftrightarrow> is_imag z \<and> Im z > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (z \<noteq> 0 \<and> Arg z = pi / 2) = (is_imag z \<and> 0 < Im z)
[PROOF STEP]
by (smt Im_rcis Re_i_times Re_rcis arcsin_minus_1 cos_pi_half divide_minus_left mult.commute mult_cancel_right1 rcis_cmod_Arg is_imag_arg2 sin_arcsin sin_pi_half zero_less_mult_pos zero_less_norm_iff)


[STATEMENT]
lemma arg_minus_pi2_iff:
  shows "z \<noteq> 0 \<and> Arg z = - pi / 2 \<longleftrightarrow> is_imag z \<and> Im z < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (z \<noteq> 0 \<and> Arg z = - pi / 2) = (is_imag z \<and> Im z < 0)
[PROOF STEP]
by (smt arg_pi2_iff complex.expand divide_cancel_right pi_neq_zero is_imag_arg1 is_imag_arg2 zero_complex.simps(1) zero_complex.simps(2))


[STATEMENT]
lemma canon_ang_arg:
  shows "\<downharpoonright>Arg z\<downharpoonleft> = Arg z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<downharpoonright>Arg z\<downharpoonleft> = Arg z
[PROOF STEP]
using canon_ang_id[of "Arg z"] Arg_bounded
[PROOF STATE]
proof (prove)
using this:
- pi < Arg z \<and> Arg z \<le> pi \<Longrightarrow> \<downharpoonright>Arg z\<downharpoonleft> = Arg z
- pi < Arg ?z \<and> Arg ?z \<le> pi

goal (1 subgoal):
 1. \<downharpoonright>Arg z\<downharpoonleft> = Arg z
[PROOF STEP]
by simp


[STATEMENT]
lemma arg_cis:
  shows "Arg (cis \<phi>) = \<downharpoonright>\<phi>\<downharpoonleft>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arg (cis \<phi>) = \<downharpoonright>\<phi>\<downharpoonleft>
[PROOF STEP]
using cis_Arg_unique canon_ang canon_ang_cos canon_ang_sin cis.ctr sgn_cis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>sgn ?z = cis ?x; - pi < ?x; ?x \<le> pi\<rbrakk> \<Longrightarrow> Arg ?z = ?x
- pi < \<downharpoonright>?\<alpha>\<downharpoonleft>
\<downharpoonright>?\<alpha>\<downharpoonleft> \<le> pi
\<exists>x. ?\<alpha> - \<downharpoonright>?\<alpha>\<downharpoonleft> = 2 * real_of_int x * pi
cos \<downharpoonright>?\<alpha>\<downharpoonleft> = cos ?\<alpha>
sin \<downharpoonright>?\<alpha>\<downharpoonleft> = sin ?\<alpha>
cis ?a = Complex (cos ?a) (sin ?a)
sgn (cis ?a) = cis ?a

goal (1 subgoal):
 1. Arg (cis \<phi>) = \<downharpoonright>\<phi>\<downharpoonleft>
[PROOF STEP]
by presburger


[STATEMENT]
lemma cos_arg:
  assumes "z \<noteq> 0"
  shows "cos (Arg z) = Re z / cmod z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cos (Arg z) = Re z / cmod z
[PROOF STEP]
by (metis Complex.Re_sgn cis.simps(1) assms cis_Arg)


[STATEMENT]
lemma sin_arg:
  assumes "z \<noteq> 0"
  shows "sin (Arg z) = Im z / cmod z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sin (Arg z) = Im z / cmod z
[PROOF STEP]
by (metis Complex.Im_sgn cis.simps(2) assms cis_Arg)


[STATEMENT]
lemma cis_arg_mult:
  assumes "z1 * z2 \<noteq> 0"
  shows "cis (Arg (z1 * z2)) = cis (Arg z1 + Arg z2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cis (Arg (z1 * z2)) = cis (Arg z1 + Arg z2)
[PROOF STEP]
by (metis assms cis_Arg cis_mult mult_eq_0_iff sgn_mult)


[STATEMENT]
lemma arg_mult_2kpi:
  assumes "z1 * z2 \<noteq> 0"
  shows "\<exists> k::int. Arg (z1 * z2) = Arg z1 + Arg z2 + 2*k*pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. Arg (z1 * z2) = Arg z1 + Arg z2 + 2 * real_of_int x * pi
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. Arg (z1 * z2) = Arg z1 + Arg z2 + 2 * real_of_int x * pi
[PROOF STEP]
have "cis (Arg (z1*z2)) = cis (Arg z1 + Arg z2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cis (Arg (z1 * z2)) = cis (Arg z1 + Arg z2)
[PROOF STEP]
by (rule cis_arg_mult[OF assms])
[PROOF STATE]
proof (state)
this:
cis (Arg (z1 * z2)) = cis (Arg z1 + Arg z2)

goal (1 subgoal):
 1. \<exists>x. Arg (z1 * z2) = Arg z1 + Arg z2 + 2 * real_of_int x * pi
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
cis (Arg (z1 * z2)) = cis (Arg z1 + Arg z2)

goal (1 subgoal):
 1. \<exists>x. Arg (z1 * z2) = Arg z1 + Arg z2 + 2 * real_of_int x * pi
[PROOF STEP]
using cis_eq[of "Arg (z1*z2)" "Arg z1 + Arg z2"]
[PROOF STATE]
proof (prove)
using this:
cis (Arg (z1 * z2)) = cis (Arg z1 + Arg z2)
cis (Arg (z1 * z2)) = cis (Arg z1 + Arg z2) \<Longrightarrow> \<exists>x. Arg (z1 * z2) - (Arg z1 + Arg z2) = 2 * real_of_int x * pi

goal (1 subgoal):
 1. \<exists>x. Arg (z1 * z2) = Arg z1 + Arg z2 + 2 * real_of_int x * pi
[PROOF STEP]
by (auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
\<exists>x. Arg (z1 * z2) = Arg z1 + Arg z2 + 2 * real_of_int x * pi

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arg_mult:
  assumes "z1 * z2 \<noteq> 0"
  shows "Arg(z1 * z2) = \<downharpoonright>Arg z1 + Arg z2\<downharpoonleft>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arg (z1 * z2) = \<downharpoonright>Arg z1 + Arg z2\<downharpoonleft>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Arg (z1 * z2) = \<downharpoonright>Arg z1 + Arg z2\<downharpoonleft>
[PROOF STEP]
obtain k::int where "Arg(z1 * z2) = Arg z1 + Arg z2 + 2*k*pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. Arg (z1 * z2) = Arg z1 + Arg z2 + real_of_int (2 * k) * pi \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using arg_mult_2kpi[of z1 z2]
[PROOF STATE]
proof (prove)
using this:
z1 * z2 \<noteq> 0 \<Longrightarrow> \<exists>x. Arg (z1 * z2) = Arg z1 + Arg z2 + 2 * real_of_int x * pi

goal (1 subgoal):
 1. (\<And>k. Arg (z1 * z2) = Arg z1 + Arg z2 + real_of_int (2 * k) * pi \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
z1 * z2 \<noteq> 0 \<Longrightarrow> \<exists>x. Arg (z1 * z2) = Arg z1 + Arg z2 + 2 * real_of_int x * pi
z1 * z2 \<noteq> 0

goal (1 subgoal):
 1. (\<And>k. Arg (z1 * z2) = Arg z1 + Arg z2 + real_of_int (2 * k) * pi \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Arg (z1 * z2) = Arg z1 + Arg z2 + real_of_int (2 * k) * pi

goal (1 subgoal):
 1. Arg (z1 * z2) = \<downharpoonright>Arg z1 + Arg z2\<downharpoonleft>
[PROOF STEP]
hence "\<downharpoonright>Arg(z1 * z2)\<downharpoonleft> = \<downharpoonright>Arg z1 + Arg z2\<downharpoonleft>"
[PROOF STATE]
proof (prove)
using this:
Arg (z1 * z2) = Arg z1 + Arg z2 + real_of_int (2 * k) * pi

goal (1 subgoal):
 1. \<downharpoonright>Arg (z1 * z2)\<downharpoonleft> = \<downharpoonright>Arg z1 + Arg z2\<downharpoonleft>
[PROOF STEP]
using canon_ang_eq
[PROOF STATE]
proof (prove)
using this:
Arg (z1 * z2) = Arg z1 + Arg z2 + real_of_int (2 * k) * pi
\<exists>x. ?\<alpha>\<^sub>1 - ?\<alpha>\<^sub>2 = 2 * real_of_int x * pi \<Longrightarrow> \<downharpoonright>?\<alpha>\<^sub>1\<downharpoonleft> = \<downharpoonright>?\<alpha>\<^sub>2\<downharpoonleft>

goal (1 subgoal):
 1. \<downharpoonright>Arg (z1 * z2)\<downharpoonleft> = \<downharpoonright>Arg z1 + Arg z2\<downharpoonleft>
[PROOF STEP]
by(simp add:field_simps)
[PROOF STATE]
proof (state)
this:
\<downharpoonright>Arg (z1 * z2)\<downharpoonleft> = \<downharpoonright>Arg z1 + Arg z2\<downharpoonleft>

goal (1 subgoal):
 1. Arg (z1 * z2) = \<downharpoonright>Arg z1 + Arg z2\<downharpoonleft>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<downharpoonright>Arg (z1 * z2)\<downharpoonleft> = \<downharpoonright>Arg z1 + Arg z2\<downharpoonleft>

goal (1 subgoal):
 1. Arg (z1 * z2) = \<downharpoonright>Arg z1 + Arg z2\<downharpoonleft>
[PROOF STEP]
using canon_ang_arg[of "z1*z2"]
[PROOF STATE]
proof (prove)
using this:
\<downharpoonright>Arg (z1 * z2)\<downharpoonleft> = \<downharpoonright>Arg z1 + Arg z2\<downharpoonleft>
\<downharpoonright>Arg (z1 * z2)\<downharpoonleft> = Arg (z1 * z2)

goal (1 subgoal):
 1. Arg (z1 * z2) = \<downharpoonright>Arg z1 + Arg z2\<downharpoonleft>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Arg (z1 * z2) = \<downharpoonright>Arg z1 + Arg z2\<downharpoonleft>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arg_mult_real_positive [simp]:
  assumes "k > 0"
  shows "Arg (cor k * z) = Arg z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arg (cor k * z) = Arg z
[PROOF STEP]
proof (cases "z = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z = 0 \<Longrightarrow> Arg (cor k * z) = Arg z
 2. z \<noteq> 0 \<Longrightarrow> Arg (cor k * z) = Arg z
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
z \<noteq> 0

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> Arg (cor k * z) = Arg z
 2. z \<noteq> 0 \<Longrightarrow> Arg (cor k * z) = Arg z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0

goal (1 subgoal):
 1. Arg (cor k * z) = Arg z
[PROOF STEP]
using arg_mult assms canon_ang_arg
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0
?z1.0 * ?z2.0 \<noteq> 0 \<Longrightarrow> Arg (?z1.0 * ?z2.0) = \<downharpoonright>Arg ?z1.0 + Arg ?z2.0\<downharpoonleft>
0 < k
\<downharpoonright>Arg ?z\<downharpoonleft> = Arg ?z

goal (1 subgoal):
 1. Arg (cor k * z) = Arg z
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Arg (cor k * z) = Arg z

goal (1 subgoal):
 1. z = 0 \<Longrightarrow> Arg (cor k * z) = Arg z
[PROOF STEP]
qed (auto simp: Arg_zero)


[STATEMENT]
lemma arg_mult_real_negative [simp]:
  assumes "k < 0"
  shows "Arg (cor k * z) = Arg (-z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arg (cor k * z) = Arg (- z)
[PROOF STEP]
proof (cases "z = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z = 0 \<Longrightarrow> Arg (cor k * z) = Arg (- z)
 2. z \<noteq> 0 \<Longrightarrow> Arg (cor k * z) = Arg (- z)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
z \<noteq> 0

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> Arg (cor k * z) = Arg (- z)
 2. z \<noteq> 0 \<Longrightarrow> Arg (cor k * z) = Arg (- z)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0

goal (1 subgoal):
 1. Arg (cor k * z) = Arg (- z)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0
k < 0

goal (1 subgoal):
 1. Arg (cor k * z) = Arg (- z)
[PROOF STEP]
by (metis arg_mult_real_positive minus_mult_commute neg_0_less_iff_less of_real_minus minus_minus)
[PROOF STATE]
proof (state)
this:
Arg (cor k * z) = Arg (- z)

goal (1 subgoal):
 1. z = 0 \<Longrightarrow> Arg (cor k * z) = Arg (- z)
[PROOF STEP]
qed (auto simp: Arg_zero)


[STATEMENT]
lemma arg_div_real_positive [simp]:
  assumes "k > 0"
  shows "Arg (z / cor k) = Arg z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arg (z / cor k) = Arg z
[PROOF STEP]
proof(cases "z = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z = 0 \<Longrightarrow> Arg (z / cor k) = Arg z
 2. z \<noteq> 0 \<Longrightarrow> Arg (z / cor k) = Arg z
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
z = 0

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> Arg (z / cor k) = Arg z
 2. z \<noteq> 0 \<Longrightarrow> Arg (z / cor k) = Arg z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
z = 0

goal (1 subgoal):
 1. Arg (z / cor k) = Arg z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Arg (z / cor k) = Arg z

goal (1 subgoal):
 1. z \<noteq> 0 \<Longrightarrow> Arg (z / cor k) = Arg z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z \<noteq> 0 \<Longrightarrow> Arg (z / cor k) = Arg z
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
z \<noteq> 0

goal (1 subgoal):
 1. z \<noteq> 0 \<Longrightarrow> Arg (z / cor k) = Arg z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0

goal (1 subgoal):
 1. Arg (z / cor k) = Arg z
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0
0 < k

goal (1 subgoal):
 1. Arg (z / cor k) = Arg z
[PROOF STEP]
using arg_mult_real_positive[of "1/k" z]
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0
0 < k
0 < 1 / k \<Longrightarrow> Arg (cor (1 / k) * z) = Arg z

goal (1 subgoal):
 1. Arg (z / cor k) = Arg z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Arg (z / cor k) = Arg z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arg_div_real_negative [simp]:
  assumes "k < 0"
  shows "Arg (z / cor k) = Arg (-z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arg (z / cor k) = Arg (- z)
[PROOF STEP]
proof(cases "z = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z = 0 \<Longrightarrow> Arg (z / cor k) = Arg (- z)
 2. z \<noteq> 0 \<Longrightarrow> Arg (z / cor k) = Arg (- z)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
z = 0

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> Arg (z / cor k) = Arg (- z)
 2. z \<noteq> 0 \<Longrightarrow> Arg (z / cor k) = Arg (- z)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
z = 0

goal (1 subgoal):
 1. Arg (z / cor k) = Arg (- z)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Arg (z / cor k) = Arg (- z)

goal (1 subgoal):
 1. z \<noteq> 0 \<Longrightarrow> Arg (z / cor k) = Arg (- z)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z \<noteq> 0 \<Longrightarrow> Arg (z / cor k) = Arg (- z)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
z \<noteq> 0

goal (1 subgoal):
 1. z \<noteq> 0 \<Longrightarrow> Arg (z / cor k) = Arg (- z)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0

goal (1 subgoal):
 1. Arg (z / cor k) = Arg (- z)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0
k < 0

goal (1 subgoal):
 1. Arg (z / cor k) = Arg (- z)
[PROOF STEP]
using arg_mult_real_negative[of "1/k" z]
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0
k < 0
1 / k < 0 \<Longrightarrow> Arg (cor (1 / k) * z) = Arg (- z)

goal (1 subgoal):
 1. Arg (z / cor k) = Arg (- z)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Arg (z / cor k) = Arg (- z)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arg_mult_eq:
  assumes "z * z1 \<noteq> 0" and "z * z2 \<noteq> 0"
  assumes "Arg (z * z1) = Arg (z * z2)"
  shows "Arg z1 = Arg z2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arg z1 = Arg z2
[PROOF STEP]
by (metis (no_types, lifting) arg_cis assms canon_ang_arg cis_Arg mult_eq_0_iff nonzero_mult_div_cancel_left sgn_divide)


[STATEMENT]
lemma arg_cnj_pi:
  assumes "Arg z = pi"
  shows "Arg (cnj z) = pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arg (cnj z) = pi
[PROOF STEP]
using arg_pi_iff assms
[PROOF STATE]
proof (prove)
using this:
(Arg ?z = pi) = (is_real ?z \<and> Re ?z < 0)
Arg z = pi

goal (1 subgoal):
 1. Arg (cnj z) = pi
[PROOF STEP]
by auto


[STATEMENT]
lemma arg_cnj_not_pi:
  assumes "Arg z \<noteq> pi"
  shows "Arg (cnj z) = -Arg z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arg (cnj z) = - Arg z
[PROOF STEP]
proof(cases "Arg z = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Arg z = 0 \<Longrightarrow> Arg (cnj z) = - Arg z
 2. Arg z \<noteq> 0 \<Longrightarrow> Arg (cnj z) = - Arg z
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Arg z = 0

goal (2 subgoals):
 1. Arg z = 0 \<Longrightarrow> Arg (cnj z) = - Arg z
 2. Arg z \<noteq> 0 \<Longrightarrow> Arg (cnj z) = - Arg z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Arg z = 0

goal (1 subgoal):
 1. Arg (cnj z) = - Arg z
[PROOF STEP]
using eq_cnj_iff_real[of z] is_real_arg1[of z]
[PROOF STATE]
proof (prove)
using this:
Arg z = 0
(cnj z = z) = is_real z
Arg z = 0 \<or> Arg z = pi \<Longrightarrow> is_real z

goal (1 subgoal):
 1. Arg (cnj z) = - Arg z
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Arg (cnj z) = - Arg z

goal (1 subgoal):
 1. Arg z \<noteq> 0 \<Longrightarrow> Arg (cnj z) = - Arg z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Arg z \<noteq> 0 \<Longrightarrow> Arg (cnj z) = - Arg z
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Arg z \<noteq> 0

goal (1 subgoal):
 1. Arg z \<noteq> 0 \<Longrightarrow> Arg (cnj z) = - Arg z
[PROOF STEP]
have "Arg (cnj z) = Arg z \<or> Arg(cnj z) = -Arg z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arg (cnj z) = Arg z \<or> Arg (cnj z) = - Arg z
[PROOF STEP]
using Arg_bounded[of z] Arg_bounded[of "cnj z"]
[PROOF STATE]
proof (prove)
using this:
- pi < Arg z \<and> Arg z \<le> pi
- pi < Arg (cnj z) \<and> Arg (cnj z) \<le> pi

goal (1 subgoal):
 1. Arg (cnj z) = Arg z \<or> Arg (cnj z) = - Arg z
[PROOF STEP]
by (smt (verit, best) arccos_cos arccos_cos2 cnj.sel(1) complex_cnj_zero_iff complex_mod_cnj cos_arg)
[PROOF STATE]
proof (state)
this:
Arg (cnj z) = Arg z \<or> Arg (cnj z) = - Arg z

goal (1 subgoal):
 1. Arg z \<noteq> 0 \<Longrightarrow> Arg (cnj z) = - Arg z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Arg (cnj z) = Arg z \<or> Arg (cnj z) = - Arg z

goal (1 subgoal):
 1. Arg z \<noteq> 0 \<Longrightarrow> Arg (cnj z) = - Arg z
[PROOF STEP]
have "Arg (cnj z) \<noteq> Arg z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arg (cnj z) \<noteq> Arg z
[PROOF STEP]
using sin_0_iff_canon[of "Arg (cnj z)"] Arg_bounded False assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>sin (Arg (cnj z)) = 0; - pi < Arg (cnj z); Arg (cnj z) \<le> pi\<rbrakk> \<Longrightarrow> Arg (cnj z) = 0 \<or> Arg (cnj z) = pi
- pi < Arg ?z \<and> Arg ?z \<le> pi
Arg z \<noteq> 0
Arg z \<noteq> pi

goal (1 subgoal):
 1. Arg (cnj z) \<noteq> Arg z
[PROOF STEP]
by (metis complex_mod_cnj eq_cnj_iff_real is_real_arg2 rcis_cmod_Arg)
[PROOF STATE]
proof (state)
this:
Arg (cnj z) \<noteq> Arg z

goal (1 subgoal):
 1. Arg z \<noteq> 0 \<Longrightarrow> Arg (cnj z) = - Arg z
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Arg (cnj z) = Arg z \<or> Arg (cnj z) = - Arg z
Arg (cnj z) \<noteq> Arg z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Arg (cnj z) = Arg z \<or> Arg (cnj z) = - Arg z
Arg (cnj z) \<noteq> Arg z

goal (1 subgoal):
 1. Arg (cnj z) = - Arg z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Arg (cnj z) = - Arg z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arg_inv_not_pi:
  assumes "z \<noteq> 0" and "Arg z \<noteq> pi"
  shows "Arg (1 / z) = - Arg z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arg (1 / z) = - Arg z
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Arg (1 / z) = - Arg z
[PROOF STEP]
have "1/z = cnj z / cor ((cmod z)\<^sup>2 )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / z = cnj z / cor ((cmod z)\<^sup>2)
[PROOF STEP]
using \<open>z \<noteq> 0\<close> complex_mult_cnj_cmod[of z]
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0
z * cnj z = cor ((cmod z)\<^sup>2)

goal (1 subgoal):
 1. 1 / z = cnj z / cor ((cmod z)\<^sup>2)
[PROOF STEP]
by (auto simp add:field_simps)
[PROOF STATE]
proof (state)
this:
1 / z = cnj z / cor ((cmod z)\<^sup>2)

goal (1 subgoal):
 1. Arg (1 / z) = - Arg z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
1 / z = cnj z / cor ((cmod z)\<^sup>2)

goal (1 subgoal):
 1. Arg (1 / z) = - Arg z
[PROOF STEP]
using arg_div_real_positive[of "(cmod z)\<^sup>2" "cnj z"] \<open>z \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
1 / z = cnj z / cor ((cmod z)\<^sup>2)
0 < (cmod z)\<^sup>2 \<Longrightarrow> Arg (cnj z / cor ((cmod z)\<^sup>2)) = Arg (cnj z)
z \<noteq> 0

goal (1 subgoal):
 1. Arg (1 / z) = - Arg z
[PROOF STEP]
using arg_cnj_not_pi[of z] \<open>Arg z \<noteq> pi\<close>
[PROOF STATE]
proof (prove)
using this:
1 / z = cnj z / cor ((cmod z)\<^sup>2)
0 < (cmod z)\<^sup>2 \<Longrightarrow> Arg (cnj z / cor ((cmod z)\<^sup>2)) = Arg (cnj z)
z \<noteq> 0
Arg z \<noteq> pi \<Longrightarrow> Arg (cnj z) = - Arg z
Arg z \<noteq> pi

goal (1 subgoal):
 1. Arg (1 / z) = - Arg z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Arg (1 / z) = - Arg z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arg_inv_pi:
  assumes "z \<noteq> 0" and "Arg z = pi"
  shows "Arg (1 / z) = pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arg (1 / z) = pi
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Arg (1 / z) = pi
[PROOF STEP]
have "1/z = cnj z / cor ((cmod z)\<^sup>2 )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / z = cnj z / cor ((cmod z)\<^sup>2)
[PROOF STEP]
using \<open>z \<noteq> 0\<close> complex_mult_cnj_cmod[of z]
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0
z * cnj z = cor ((cmod z)\<^sup>2)

goal (1 subgoal):
 1. 1 / z = cnj z / cor ((cmod z)\<^sup>2)
[PROOF STEP]
by (auto simp add:field_simps)
[PROOF STATE]
proof (state)
this:
1 / z = cnj z / cor ((cmod z)\<^sup>2)

goal (1 subgoal):
 1. Arg (1 / z) = pi
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
1 / z = cnj z / cor ((cmod z)\<^sup>2)

goal (1 subgoal):
 1. Arg (1 / z) = pi
[PROOF STEP]
using arg_div_real_positive[of "(cmod z)\<^sup>2" "cnj z"] \<open>z \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
1 / z = cnj z / cor ((cmod z)\<^sup>2)
0 < (cmod z)\<^sup>2 \<Longrightarrow> Arg (cnj z / cor ((cmod z)\<^sup>2)) = Arg (cnj z)
z \<noteq> 0

goal (1 subgoal):
 1. Arg (1 / z) = pi
[PROOF STEP]
using arg_cnj_pi[of z] \<open>Arg z = pi\<close>
[PROOF STATE]
proof (prove)
using this:
1 / z = cnj z / cor ((cmod z)\<^sup>2)
0 < (cmod z)\<^sup>2 \<Longrightarrow> Arg (cnj z / cor ((cmod z)\<^sup>2)) = Arg (cnj z)
z \<noteq> 0
Arg z = pi \<Longrightarrow> Arg (cnj z) = pi
Arg z = pi

goal (1 subgoal):
 1. Arg (1 / z) = pi
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Arg (1 / z) = pi

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arg_inv_2kpi:
  assumes "z \<noteq> 0"
  shows "\<exists> k::int. Arg (1 / z) = - Arg z + 2*k*pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. Arg (1 / z) = - Arg z + 2 * real_of_int x * pi
[PROOF STEP]
using arg_inv_pi[OF assms]
[PROOF STATE]
proof (prove)
using this:
Arg z = pi \<Longrightarrow> Arg (1 / z) = pi

goal (1 subgoal):
 1. \<exists>x. Arg (1 / z) = - Arg z + 2 * real_of_int x * pi
[PROOF STEP]
using arg_inv_not_pi[OF assms]
[PROOF STATE]
proof (prove)
using this:
Arg z = pi \<Longrightarrow> Arg (1 / z) = pi
Arg z \<noteq> pi \<Longrightarrow> Arg (1 / z) = - Arg z

goal (1 subgoal):
 1. \<exists>x. Arg (1 / z) = - Arg z + 2 * real_of_int x * pi
[PROOF STEP]
by (cases "Arg z = pi") (rule_tac x="1" in exI, simp, rule_tac x="0" in exI, simp)


[STATEMENT]
lemma arg_inv:
  assumes "z \<noteq> 0"
  shows "Arg (1 / z) = \<downharpoonright>- Arg z\<downharpoonleft>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arg (1 / z) = \<downharpoonright>- Arg z\<downharpoonleft>
[PROOF STEP]
by (metis arg_inv_not_pi arg_inv_pi assms canon_ang_arg canon_ang_uminus_pi)


[STATEMENT]
lemma arg_div_2kpi:
  assumes "z1 \<noteq> 0" and "z2 \<noteq> 0"
  shows "\<exists> k::int. Arg (z1 / z2) = Arg z1 - Arg z2 + 2*k*pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. Arg (z1 / z2) = Arg z1 - Arg z2 + 2 * real_of_int x * pi
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. Arg (z1 / z2) = Arg z1 - Arg z2 + 2 * real_of_int x * pi
[PROOF STEP]
obtain x1 where "Arg (z1 * (1 / z2)) = Arg z1 + Arg (1 / z2) + 2 * real_of_int x1 * pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x1. Arg (z1 * (1 / z2)) = Arg z1 + Arg (1 / z2) + 2 * real_of_int x1 * pi \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms arg_mult_2kpi[of z1 "1/z2"]
[PROOF STATE]
proof (prove)
using this:
z1 \<noteq> 0
z2 \<noteq> 0
z1 * (1 / z2) \<noteq> 0 \<Longrightarrow> \<exists>x. Arg (z1 * (1 / z2)) = Arg z1 + Arg (1 / z2) + 2 * real_of_int x * pi

goal (1 subgoal):
 1. (\<And>x1. Arg (z1 * (1 / z2)) = Arg z1 + Arg (1 / z2) + 2 * real_of_int x1 * pi \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Arg (z1 * (1 / z2)) = Arg z1 + Arg (1 / z2) + 2 * real_of_int x1 * pi

goal (1 subgoal):
 1. \<exists>x. Arg (z1 / z2) = Arg z1 - Arg z2 + 2 * real_of_int x * pi
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Arg (z1 * (1 / z2)) = Arg z1 + Arg (1 / z2) + 2 * real_of_int x1 * pi

goal (1 subgoal):
 1. \<exists>x. Arg (z1 / z2) = Arg z1 - Arg z2 + 2 * real_of_int x * pi
[PROOF STEP]
obtain x2 where "Arg (1 / z2) = - Arg z2 + 2 * real_of_int x2 * pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x2. Arg (1 / z2) = - Arg z2 + 2 * real_of_int x2 * pi \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms arg_inv_2kpi[of z2]
[PROOF STATE]
proof (prove)
using this:
z1 \<noteq> 0
z2 \<noteq> 0
z2 \<noteq> 0 \<Longrightarrow> \<exists>x. Arg (1 / z2) = - Arg z2 + 2 * real_of_int x * pi

goal (1 subgoal):
 1. (\<And>x2. Arg (1 / z2) = - Arg z2 + 2 * real_of_int x2 * pi \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Arg (1 / z2) = - Arg z2 + 2 * real_of_int x2 * pi

goal (1 subgoal):
 1. \<exists>x. Arg (z1 / z2) = Arg z1 - Arg z2 + 2 * real_of_int x * pi
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Arg (z1 * (1 / z2)) = Arg z1 + Arg (1 / z2) + 2 * real_of_int x1 * pi
Arg (1 / z2) = - Arg z2 + 2 * real_of_int x2 * pi
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Arg (z1 * (1 / z2)) = Arg z1 + Arg (1 / z2) + 2 * real_of_int x1 * pi
Arg (1 / z2) = - Arg z2 + 2 * real_of_int x2 * pi

goal (1 subgoal):
 1. \<exists>x. Arg (z1 / z2) = Arg z1 - Arg z2 + 2 * real_of_int x * pi
[PROOF STEP]
by (rule_tac x="x1 + x2" in exI, simp add: field_simps)
[PROOF STATE]
proof (state)
this:
\<exists>x. Arg (z1 / z2) = Arg z1 - Arg z2 + 2 * real_of_int x * pi

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arg_div:
  assumes "z1 \<noteq> 0" and "z2 \<noteq> 0"
  shows "Arg(z1 / z2) = \<downharpoonright>Arg z1 - Arg z2\<downharpoonleft>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arg (z1 / z2) = \<downharpoonright>Arg z1 - Arg z2\<downharpoonleft>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Arg (z1 / z2) = \<downharpoonright>Arg z1 - Arg z2\<downharpoonleft>
[PROOF STEP]
obtain k::int where "Arg(z1 / z2) = Arg z1 - Arg z2 + 2*k*pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. Arg (z1 / z2) = Arg z1 - Arg z2 + real_of_int (2 * k) * pi \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using arg_div_2kpi[of z1 z2]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>z1 \<noteq> 0; z2 \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>x. Arg (z1 / z2) = Arg z1 - Arg z2 + 2 * real_of_int x * pi

goal (1 subgoal):
 1. (\<And>k. Arg (z1 / z2) = Arg z1 - Arg z2 + real_of_int (2 * k) * pi \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>z1 \<noteq> 0; z2 \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>x. Arg (z1 / z2) = Arg z1 - Arg z2 + 2 * real_of_int x * pi
z1 \<noteq> 0
z2 \<noteq> 0

goal (1 subgoal):
 1. (\<And>k. Arg (z1 / z2) = Arg z1 - Arg z2 + real_of_int (2 * k) * pi \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Arg (z1 / z2) = Arg z1 - Arg z2 + real_of_int (2 * k) * pi

goal (1 subgoal):
 1. Arg (z1 / z2) = \<downharpoonright>Arg z1 - Arg z2\<downharpoonleft>
[PROOF STEP]
hence "canon_ang(Arg(z1 / z2)) = canon_ang(Arg z1 - Arg z2)"
[PROOF STATE]
proof (prove)
using this:
Arg (z1 / z2) = Arg z1 - Arg z2 + real_of_int (2 * k) * pi

goal (1 subgoal):
 1. \<downharpoonright>Arg (z1 / z2)\<downharpoonleft> = \<downharpoonright>Arg z1 - Arg z2\<downharpoonleft>
[PROOF STEP]
using canon_ang_eq
[PROOF STATE]
proof (prove)
using this:
Arg (z1 / z2) = Arg z1 - Arg z2 + real_of_int (2 * k) * pi
\<exists>x. ?\<alpha>\<^sub>1 - ?\<alpha>\<^sub>2 = 2 * real_of_int x * pi \<Longrightarrow> \<downharpoonright>?\<alpha>\<^sub>1\<downharpoonleft> = \<downharpoonright>?\<alpha>\<^sub>2\<downharpoonleft>

goal (1 subgoal):
 1. \<downharpoonright>Arg (z1 / z2)\<downharpoonleft> = \<downharpoonright>Arg z1 - Arg z2\<downharpoonleft>
[PROOF STEP]
by(simp add:field_simps)
[PROOF STATE]
proof (state)
this:
\<downharpoonright>Arg (z1 / z2)\<downharpoonleft> = \<downharpoonright>Arg z1 - Arg z2\<downharpoonleft>

goal (1 subgoal):
 1. Arg (z1 / z2) = \<downharpoonright>Arg z1 - Arg z2\<downharpoonleft>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<downharpoonright>Arg (z1 / z2)\<downharpoonleft> = \<downharpoonright>Arg z1 - Arg z2\<downharpoonleft>

goal (1 subgoal):
 1. Arg (z1 / z2) = \<downharpoonright>Arg z1 - Arg z2\<downharpoonleft>
[PROOF STEP]
using canon_ang_arg[of "z1/z2"]
[PROOF STATE]
proof (prove)
using this:
\<downharpoonright>Arg (z1 / z2)\<downharpoonleft> = \<downharpoonright>Arg z1 - Arg z2\<downharpoonleft>
\<downharpoonright>Arg (z1 / z2)\<downharpoonleft> = Arg (z1 / z2)

goal (1 subgoal):
 1. Arg (z1 / z2) = \<downharpoonright>Arg z1 - Arg z2\<downharpoonleft>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Arg (z1 / z2) = \<downharpoonright>Arg z1 - Arg z2\<downharpoonleft>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arg_uminus:
  assumes "z \<noteq> 0"
  shows "Arg (-z) = \<downharpoonright>Arg z + pi\<downharpoonleft>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Arg (- z) = \<downharpoonright>Arg z + pi\<downharpoonleft>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0

goal (1 subgoal):
 1. Arg (- z) = \<downharpoonright>Arg z + pi\<downharpoonleft>
[PROOF STEP]
using arg_mult[of "-1" z]
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0
- 1 * z \<noteq> 0 \<Longrightarrow> Arg (- 1 * z) = \<downharpoonright>Arg (- 1) + Arg z\<downharpoonleft>

goal (1 subgoal):
 1. Arg (- z) = \<downharpoonright>Arg z + pi\<downharpoonleft>
[PROOF STEP]
using arg_complex_of_real_negative[of "-1"]
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0
- 1 * z \<noteq> 0 \<Longrightarrow> Arg (- 1 * z) = \<downharpoonright>Arg (- 1) + Arg z\<downharpoonleft>
- 1 < 0 \<Longrightarrow> Arg (cor (- 1)) = pi

goal (1 subgoal):
 1. Arg (- z) = \<downharpoonright>Arg z + pi\<downharpoonleft>
[PROOF STEP]
by (auto simp add: field_simps)