[STATEMENT]
lemma radiant_of:
  "0 \<le> radiant_of p \<and> radiant_of p < 2 * pi \<and> of_radiant (radiant_of p) = normalize p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> radiant_of p \<and> radiant_of p < 2 * pi \<and> of_radiant (radiant_of p) = normalize p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 \<le> radiant_of p \<and> radiant_of p < 2 * pi \<and> of_radiant (radiant_of p) = normalize p
[PROOF STEP]
let ?a = "if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- (normalize p $ 1))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 \<le> radiant_of p \<and> radiant_of p < 2 * pi \<and> of_radiant (radiant_of p) = normalize p
[PROOF STEP]
have "0 \<le> ?a \<and> ?a < 2 * pi \<and> of_radiant ?a = normalize p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) \<and> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi \<and> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) = normalize p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 \<le> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) \<and> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi \<and> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) = normalize p
[PROOF STEP]
have "0 \<le> ?a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))

goal (1 subgoal):
 1. 0 \<le> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) \<and> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi \<and> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) = normalize p
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))

goal (1 subgoal):
 1. 0 \<le> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) \<and> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi \<and> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) = normalize p
[PROOF STEP]
have "?a < 2 * pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi
 2. \<not> ?P \<Longrightarrow> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi
[PROOF STEP]
assume "0 \<le> p $ 2"
[PROOF STATE]
proof (state)
this:
0 \<le> p $ 2

goal (2 subgoals):
 1. ?P \<Longrightarrow> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi
 2. \<not> ?P \<Longrightarrow> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
0 \<le> p $ 2
[PROOF STEP]
have "?a \<le> pi"
[PROOF STATE]
proof (prove)
using this:
0 \<le> p $ 2

goal (1 subgoal):
 1. (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) \<le> pi
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) \<le> pi

goal (2 subgoals):
 1. ?P \<Longrightarrow> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi
 2. \<not> ?P \<Longrightarrow> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) \<le> pi
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) \<le> pi

goal (1 subgoal):
 1. (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi
[PROOF STEP]
using pi_gt_zero
[PROOF STATE]
proof (prove)
using this:
(if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) \<le> pi
0 < pi

goal (1 subgoal):
 1. (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
(if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi

goal (1 subgoal):
 1. \<not> 0 \<le> p $ 2 \<Longrightarrow> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 \<le> p $ 2 \<Longrightarrow> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi
[PROOF STEP]
assume "\<not> 0 \<le> p $ 2"
[PROOF STATE]
proof (state)
this:
\<not> 0 \<le> p $ 2

goal (1 subgoal):
 1. \<not> 0 \<le> p $ 2 \<Longrightarrow> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi
[PROOF STEP]
have "arccos (- normalize p $ 1) < pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arccos (- normalize p $ 1) < pi
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. arccos (- normalize p $ 1) < pi
[PROOF STEP]
have "\<bar>normalize p $ 1\<bar> \<noteq> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>normalize p $ 1\<bar> \<noteq> 1
[PROOF STEP]
using \<open>\<not> 0 \<le> p $ 2\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> 0 \<le> p $ 2

goal (1 subgoal):
 1. \<bar>normalize p $ 1\<bar> \<noteq> 1
[PROOF STEP]
by (simp only: normalize_boundary_iff)
[PROOF STATE]
proof (state)
this:
\<bar>normalize p $ 1\<bar> \<noteq> 1

goal (1 subgoal):
 1. arccos (- normalize p $ 1) < pi
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<bar>normalize p $ 1\<bar> \<noteq> 1
[PROOF STEP]
have "arccos (- normalize p $ 1) \<noteq> pi"
[PROOF STATE]
proof (prove)
using this:
\<bar>normalize p $ 1\<bar> \<noteq> 1

goal (1 subgoal):
 1. arccos (- normalize p $ 1) \<noteq> pi
[PROOF STEP]
unfolding arccos_minus_1[symmetric]
[PROOF STATE]
proof (prove)
using this:
\<bar>normalize p $ 1\<bar> \<noteq> 1

goal (1 subgoal):
 1. arccos (- normalize p $ 1) \<noteq> arccos (- 1)
[PROOF STEP]
by (subst arccos_eq_iff) auto
[PROOF STATE]
proof (state)
this:
arccos (- normalize p $ 1) \<noteq> pi

goal (1 subgoal):
 1. arccos (- normalize p $ 1) < pi
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
arccos (- normalize p $ 1) \<noteq> pi

goal (1 subgoal):
 1. arccos (- normalize p $ 1) < pi
[PROOF STEP]
have "arccos (- normalize p $ 1) \<le> pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arccos (- normalize p $ 1) \<le> pi
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
arccos (- normalize p $ 1) \<le> pi

goal (1 subgoal):
 1. arccos (- normalize p $ 1) < pi
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
arccos (- normalize p $ 1) \<noteq> pi
arccos (- normalize p $ 1) \<le> pi
[PROOF STEP]
show "arccos (- normalize p $ 1) < pi"
[PROOF STATE]
proof (prove)
using this:
arccos (- normalize p $ 1) \<noteq> pi
arccos (- normalize p $ 1) \<le> pi

goal (1 subgoal):
 1. arccos (- normalize p $ 1) < pi
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
arccos (- normalize p $ 1) < pi

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
arccos (- normalize p $ 1) < pi

goal (1 subgoal):
 1. \<not> 0 \<le> p $ 2 \<Longrightarrow> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi
[PROOF STEP]
from this \<open>\<not> 0 \<le> p $ 2\<close>
[PROOF STATE]
proof (chain)
picking this:
arccos (- normalize p $ 1) < pi
\<not> 0 \<le> p $ 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
arccos (- normalize p $ 1) < pi
\<not> 0 \<le> p $ 2

goal (1 subgoal):
 1. (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi

goal (1 subgoal):
 1. 0 \<le> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) \<and> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi \<and> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) = normalize p
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi

goal (1 subgoal):
 1. 0 \<le> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) \<and> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi \<and> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) = normalize p
[PROOF STEP]
have "of_radiant ?a = normalize p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) = normalize p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) = normalize p
[PROOF STEP]
have "of_radiant ?a $ i = normalize p $ i" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ i = normalize p $ i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ i = normalize p $ i
[PROOF STEP]
have "of_radiant ?a $ 1 = normalize p $ 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 1 = normalize p $ 1
[PROOF STEP]
unfolding of_radiant_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (axis 1 (cos (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))) + axis 2 (sin (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)))) $ 1 = normalize p $ 1
[PROOF STEP]
by (simp add: cos_arccos_abs)
[PROOF STATE]
proof (state)
this:
of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 1 = normalize p $ 1

goal (1 subgoal):
 1. of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ i = normalize p $ i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 1 = normalize p $ 1

goal (1 subgoal):
 1. of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ i = normalize p $ i
[PROOF STEP]
have "of_radiant ?a $ 2 = normalize p $ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 2 = normalize p $ 2
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 2 = normalize p $ 2
 2. \<not> ?P \<Longrightarrow> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 2 = normalize p $ 2
[PROOF STEP]
assume "0 \<le> p $ 2"
[PROOF STATE]
proof (state)
this:
0 \<le> p $ 2

goal (2 subgoals):
 1. ?P \<Longrightarrow> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 2 = normalize p $ 2
 2. \<not> ?P \<Longrightarrow> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 2 = normalize p $ 2
[PROOF STEP]
have "sin (arccos (normalize p $ 1)) = sqrt (1 - (normalize p $ 1) ^ 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sin (arccos (normalize p $ 1)) = sqrt (1 - (normalize p $ 1)\<^sup>2)
[PROOF STEP]
by (simp add: sin_arccos_abs)
[PROOF STATE]
proof (state)
this:
sin (arccos (normalize p $ 1)) = sqrt (1 - (normalize p $ 1)\<^sup>2)

goal (2 subgoals):
 1. ?P \<Longrightarrow> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 2 = normalize p $ 2
 2. \<not> ?P \<Longrightarrow> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 2 = normalize p $ 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sin (arccos (normalize p $ 1)) = sqrt (1 - (normalize p $ 1)\<^sup>2)

goal (2 subgoals):
 1. ?P \<Longrightarrow> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 2 = normalize p $ 2
 2. \<not> ?P \<Longrightarrow> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 2 = normalize p $ 2
[PROOF STEP]
have "\<dots> = normalize p $ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt (1 - (normalize p $ 1)\<^sup>2) = normalize p $ 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sqrt (1 - (normalize p $ 1)\<^sup>2) = normalize p $ 2
[PROOF STEP]
have "1 - (normalize p $ 1)\<^sup>2 = (normalize p $ 2)\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 - (normalize p $ 1)\<^sup>2 = (normalize p $ 2)\<^sup>2
[PROOF STEP]
using normalize_square[of p]
[PROOF STATE]
proof (prove)
using this:
(normalize p $ 1)\<^sup>2 + (normalize p $ 2)\<^sup>2 = 1

goal (1 subgoal):
 1. 1 - (normalize p $ 1)\<^sup>2 = (normalize p $ 2)\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 - (normalize p $ 1)\<^sup>2 = (normalize p $ 2)\<^sup>2

goal (1 subgoal):
 1. sqrt (1 - (normalize p $ 1)\<^sup>2) = normalize p $ 2
[PROOF STEP]
from this \<open>0 \<le> p $ 2\<close>
[PROOF STATE]
proof (chain)
picking this:
1 - (normalize p $ 1)\<^sup>2 = (normalize p $ 2)\<^sup>2
0 \<le> p $ 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 - (normalize p $ 1)\<^sup>2 = (normalize p $ 2)\<^sup>2
0 \<le> p $ 2

goal (1 subgoal):
 1. sqrt (1 - (normalize p $ 1)\<^sup>2) = normalize p $ 2
[PROOF STEP]
by (simp add: nth_normalize_ge_zero_iff)
[PROOF STATE]
proof (state)
this:
sqrt (1 - (normalize p $ 1)\<^sup>2) = normalize p $ 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sqrt (1 - (normalize p $ 1)\<^sup>2) = normalize p $ 2

goal (2 subgoals):
 1. ?P \<Longrightarrow> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 2 = normalize p $ 2
 2. \<not> ?P \<Longrightarrow> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 2 = normalize p $ 2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sin (arccos (normalize p $ 1)) = normalize p $ 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sin (arccos (normalize p $ 1)) = normalize p $ 2

goal (1 subgoal):
 1. of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 2 = normalize p $ 2
[PROOF STEP]
using \<open>0 \<le> p $ 2\<close>
[PROOF STATE]
proof (prove)
using this:
sin (arccos (normalize p $ 1)) = normalize p $ 2
0 \<le> p $ 2

goal (1 subgoal):
 1. of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 2 = normalize p $ 2
[PROOF STEP]
unfolding of_radiant_def
[PROOF STATE]
proof (prove)
using this:
sin (arccos (normalize p $ 1)) = normalize p $ 2
0 \<le> p $ 2

goal (1 subgoal):
 1. (axis 1 (cos (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))) + axis 2 (sin (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)))) $ 2 = normalize p $ 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 2 = normalize p $ 2

goal (1 subgoal):
 1. \<not> 0 \<le> p $ 2 \<Longrightarrow> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 2 = normalize p $ 2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 \<le> p $ 2 \<Longrightarrow> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 2 = normalize p $ 2
[PROOF STEP]
assume "\<not> 0 \<le> p $ 2"
[PROOF STATE]
proof (state)
this:
\<not> 0 \<le> p $ 2

goal (1 subgoal):
 1. \<not> 0 \<le> p $ 2 \<Longrightarrow> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 2 = normalize p $ 2
[PROOF STEP]
have "- sin (arccos (- normalize p $ 1)) = - sqrt (1 - (normalize p $ 1)\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - sin (arccos (- normalize p $ 1)) = - sqrt (1 - (normalize p $ 1)\<^sup>2)
[PROOF STEP]
by (simp add: sin_arccos_abs)
[PROOF STATE]
proof (state)
this:
- sin (arccos (- normalize p $ 1)) = - sqrt (1 - (normalize p $ 1)\<^sup>2)

goal (1 subgoal):
 1. \<not> 0 \<le> p $ 2 \<Longrightarrow> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 2 = normalize p $ 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- sin (arccos (- normalize p $ 1)) = - sqrt (1 - (normalize p $ 1)\<^sup>2)

goal (1 subgoal):
 1. \<not> 0 \<le> p $ 2 \<Longrightarrow> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 2 = normalize p $ 2
[PROOF STEP]
have "\<dots> = normalize p $ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - sqrt (1 - (normalize p $ 1)\<^sup>2) = normalize p $ 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. - sqrt (1 - (normalize p $ 1)\<^sup>2) = normalize p $ 2
[PROOF STEP]
have "1 - (normalize p $ 1)\<^sup>2 = (normalize p $ 2)\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 - (normalize p $ 1)\<^sup>2 = (normalize p $ 2)\<^sup>2
[PROOF STEP]
using normalize_square[of p]
[PROOF STATE]
proof (prove)
using this:
(normalize p $ 1)\<^sup>2 + (normalize p $ 2)\<^sup>2 = 1

goal (1 subgoal):
 1. 1 - (normalize p $ 1)\<^sup>2 = (normalize p $ 2)\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 - (normalize p $ 1)\<^sup>2 = (normalize p $ 2)\<^sup>2

goal (1 subgoal):
 1. - sqrt (1 - (normalize p $ 1)\<^sup>2) = normalize p $ 2
[PROOF STEP]
from this \<open>\<not> 0 \<le> p $ 2\<close>
[PROOF STATE]
proof (chain)
picking this:
1 - (normalize p $ 1)\<^sup>2 = (normalize p $ 2)\<^sup>2
\<not> 0 \<le> p $ 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 - (normalize p $ 1)\<^sup>2 = (normalize p $ 2)\<^sup>2
\<not> 0 \<le> p $ 2

goal (1 subgoal):
 1. - sqrt (1 - (normalize p $ 1)\<^sup>2) = normalize p $ 2
[PROOF STEP]
using nth_normalize_ge_zero_iff
[PROOF STATE]
proof (prove)
using this:
1 - (normalize p $ 1)\<^sup>2 = (normalize p $ 2)\<^sup>2
\<not> 0 \<le> p $ 2
(0 \<le> normalize ?p $ ?i) = (0 \<le> ?p $ ?i)

goal (1 subgoal):
 1. - sqrt (1 - (normalize p $ 1)\<^sup>2) = normalize p $ 2
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
- sqrt (1 - (normalize p $ 1)\<^sup>2) = normalize p $ 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
- sqrt (1 - (normalize p $ 1)\<^sup>2) = normalize p $ 2

goal (1 subgoal):
 1. \<not> 0 \<le> p $ 2 \<Longrightarrow> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 2 = normalize p $ 2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
- sin (arccos (- normalize p $ 1)) = normalize p $ 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
- sin (arccos (- normalize p $ 1)) = normalize p $ 2

goal (1 subgoal):
 1. of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 2 = normalize p $ 2
[PROOF STEP]
using \<open>\<not> 0 \<le> p $ 2\<close>
[PROOF STATE]
proof (prove)
using this:
- sin (arccos (- normalize p $ 1)) = normalize p $ 2
\<not> 0 \<le> p $ 2

goal (1 subgoal):
 1. of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 2 = normalize p $ 2
[PROOF STEP]
unfolding of_radiant_def
[PROOF STATE]
proof (prove)
using this:
- sin (arccos (- normalize p $ 1)) = normalize p $ 2
\<not> 0 \<le> p $ 2

goal (1 subgoal):
 1. (axis 1 (cos (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))) + axis 2 (sin (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)))) $ 2 = normalize p $ 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 2 = normalize p $ 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 2 = normalize p $ 2

goal (1 subgoal):
 1. of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ i = normalize p $ i
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 1 = normalize p $ 1
of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 2 = normalize p $ 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 1 = normalize p $ 1
of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ 2 = normalize p $ 2

goal (1 subgoal):
 1. of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ i = normalize p $ i
[PROOF STEP]
by (metis exhaust_2[of i])
[PROOF STATE]
proof (state)
this:
of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ i = normalize p $ i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ ?i = normalize p $ ?i

goal (1 subgoal):
 1. of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) = normalize p
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ ?i = normalize p $ ?i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) $ ?i = normalize p $ ?i

goal (1 subgoal):
 1. of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) = normalize p
[PROOF STEP]
by (simp add: vec_eq_iff)
[PROOF STATE]
proof (state)
this:
of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) = normalize p

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) = normalize p

goal (1 subgoal):
 1. 0 \<le> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) \<and> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi \<and> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) = normalize p
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 \<le> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))
(if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi
of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) = normalize p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))
(if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi
of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) = normalize p

goal (1 subgoal):
 1. 0 \<le> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) \<and> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi \<and> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) = normalize p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 \<le> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) \<and> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi \<and> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) = normalize p

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 \<le> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) \<and> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi \<and> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) = normalize p

goal (1 subgoal):
 1. 0 \<le> radiant_of p \<and> radiant_of p < 2 * pi \<and> of_radiant (radiant_of p) = normalize p
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) \<and> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi \<and> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) = normalize p

goal (1 subgoal):
 1. 0 \<le> radiant_of p \<and> radiant_of p < 2 * pi \<and> of_radiant (radiant_of p) = normalize p
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
0 \<le> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) \<and> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi \<and> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) = normalize p

goal (1 subgoal):
 1. 0 \<le> radiant_of p \<and> radiant_of p < 2 * pi \<and> of_radiant (radiant_of p) = normalize p
[PROOF STEP]
fix \<omega>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 \<le> radiant_of p \<and> radiant_of p < 2 * pi \<and> of_radiant (radiant_of p) = normalize p
[PROOF STEP]
assume "0 \<le> \<omega> \<and> \<omega> < 2 * pi \<and> of_radiant \<omega> = normalize p"
[PROOF STATE]
proof (state)
this:
0 \<le> \<omega> \<and> \<omega> < 2 * pi \<and> of_radiant \<omega> = normalize p

goal (1 subgoal):
 1. 0 \<le> radiant_of p \<and> radiant_of p < 2 * pi \<and> of_radiant (radiant_of p) = normalize p
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
0 \<le> \<omega> \<and> \<omega> < 2 * pi \<and> of_radiant \<omega> = normalize p
[PROOF STEP]
have "0 \<le> \<omega>" "\<omega> < 2 * pi" "normalize p = of_radiant \<omega>"
[PROOF STATE]
proof (prove)
using this:
0 \<le> \<omega> \<and> \<omega> < 2 * pi \<and> of_radiant \<omega> = normalize p

goal (1 subgoal):
 1. 0 \<le> \<omega> &&& \<omega> < 2 * pi &&& normalize p = of_radiant \<omega>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> \<omega>
\<omega> < 2 * pi
normalize p = of_radiant \<omega>

goal (1 subgoal):
 1. 0 \<le> radiant_of p \<and> radiant_of p < 2 * pi \<and> of_radiant (radiant_of p) = normalize p
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
0 \<le> \<omega>
\<omega> < 2 * pi
normalize p = of_radiant \<omega>
[PROOF STEP]
have "cos \<omega> = normalize p $ 1" "sin \<omega> = normalize p $ 2"
[PROOF STATE]
proof (prove)
using this:
0 \<le> \<omega>
\<omega> < 2 * pi
normalize p = of_radiant \<omega>

goal (1 subgoal):
 1. cos \<omega> = normalize p $ 1 &&& sin \<omega> = normalize p $ 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cos \<omega> = normalize p $ 1
sin \<omega> = normalize p $ 2

goal (1 subgoal):
 1. 0 \<le> radiant_of p \<and> radiant_of p < 2 * pi \<and> of_radiant (radiant_of p) = normalize p
[PROOF STEP]
have "\<omega> = ?a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<omega> = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<omega> = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))
 2. \<not> ?P \<Longrightarrow> \<omega> = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))
[PROOF STEP]
assume "0 \<le> p $ 2"
[PROOF STATE]
proof (state)
this:
0 \<le> p $ 2

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<omega> = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))
 2. \<not> ?P \<Longrightarrow> \<omega> = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
0 \<le> p $ 2
[PROOF STEP]
have "\<omega> \<le> pi"
[PROOF STATE]
proof (prove)
using this:
0 \<le> p $ 2

goal (1 subgoal):
 1. \<omega> \<le> pi
[PROOF STEP]
using \<open>0 \<le> \<omega>\<close> \<open>\<omega> < 2 * pi\<close> \<open>sin \<omega> = normalize p $ 2\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> p $ 2
0 \<le> \<omega>
\<omega> < 2 * pi
sin \<omega> = normalize p $ 2

goal (1 subgoal):
 1. \<omega> \<le> pi
[PROOF STEP]
by (simp add: sin_ge_zero_iff[symmetric] nth_normalize_ge_zero_iff)
[PROOF STATE]
proof (state)
this:
\<omega> \<le> pi

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<omega> = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))
 2. \<not> ?P \<Longrightarrow> \<omega> = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))
[PROOF STEP]
from \<open>0 \<le> \<omega>\<close> this
[PROOF STATE]
proof (chain)
picking this:
0 \<le> \<omega>
\<omega> \<le> pi
[PROOF STEP]
have "\<omega> = arccos (cos \<omega>)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> \<omega>
\<omega> \<le> pi

goal (1 subgoal):
 1. \<omega> = arccos (cos \<omega>)
[PROOF STEP]
by (simp add: arccos_cos)
[PROOF STATE]
proof (state)
this:
\<omega> = arccos (cos \<omega>)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<omega> = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))
 2. \<not> ?P \<Longrightarrow> \<omega> = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))
[PROOF STEP]
from \<open>cos \<omega> = normalize p $ 1\<close> this
[PROOF STATE]
proof (chain)
picking this:
cos \<omega> = normalize p $ 1
\<omega> = arccos (cos \<omega>)
[PROOF STEP]
have "\<omega> = arccos (normalize p $ 1)"
[PROOF STATE]
proof (prove)
using this:
cos \<omega> = normalize p $ 1
\<omega> = arccos (cos \<omega>)

goal (1 subgoal):
 1. \<omega> = arccos (normalize p $ 1)
[PROOF STEP]
by (simp add: arccos_eq_iff)
[PROOF STATE]
proof (state)
this:
\<omega> = arccos (normalize p $ 1)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<omega> = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))
 2. \<not> ?P \<Longrightarrow> \<omega> = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<omega> = arccos (normalize p $ 1)
[PROOF STEP]
show "\<omega> = ?a"
[PROOF STATE]
proof (prove)
using this:
\<omega> = arccos (normalize p $ 1)

goal (1 subgoal):
 1. \<omega> = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))
[PROOF STEP]
using \<open>0 \<le> p $ 2\<close>
[PROOF STATE]
proof (prove)
using this:
\<omega> = arccos (normalize p $ 1)
0 \<le> p $ 2

goal (1 subgoal):
 1. \<omega> = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<omega> = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))

goal (1 subgoal):
 1. \<not> 0 \<le> p $ 2 \<Longrightarrow> \<omega> = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 \<le> p $ 2 \<Longrightarrow> \<omega> = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))
[PROOF STEP]
assume "\<not> 0 \<le> p $ 2"
[PROOF STATE]
proof (state)
this:
\<not> 0 \<le> p $ 2

goal (1 subgoal):
 1. \<not> 0 \<le> p $ 2 \<Longrightarrow> \<omega> = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> 0 \<le> p $ 2
[PROOF STEP]
have "\<omega> > pi"
[PROOF STATE]
proof (prove)
using this:
\<not> 0 \<le> p $ 2

goal (1 subgoal):
 1. pi < \<omega>
[PROOF STEP]
using \<open>0 \<le> \<omega>\<close> \<open>\<omega> < 2 * pi\<close> \<open>sin \<omega> = normalize p $ 2\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> 0 \<le> p $ 2
0 \<le> \<omega>
\<omega> < 2 * pi
sin \<omega> = normalize p $ 2

goal (1 subgoal):
 1. pi < \<omega>
[PROOF STEP]
by (simp add: sin_less_zero_iff[symmetric] nth_normalize_less_zero_iff)
[PROOF STATE]
proof (state)
this:
pi < \<omega>

goal (1 subgoal):
 1. \<not> 0 \<le> p $ 2 \<Longrightarrow> \<omega> = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))
[PROOF STEP]
from this \<open>\<omega> < 2 * pi\<close>
[PROOF STATE]
proof (chain)
picking this:
pi < \<omega>
\<omega> < 2 * pi
[PROOF STEP]
have "\<omega> - pi = arccos (cos (\<omega> - pi))"
[PROOF STATE]
proof (prove)
using this:
pi < \<omega>
\<omega> < 2 * pi

goal (1 subgoal):
 1. \<omega> - pi = arccos (cos (\<omega> - pi))
[PROOF STEP]
by (auto simp only: arccos_cos)
[PROOF STATE]
proof (state)
this:
\<omega> - pi = arccos (cos (\<omega> - pi))

goal (1 subgoal):
 1. \<not> 0 \<le> p $ 2 \<Longrightarrow> \<omega> = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))
[PROOF STEP]
from this \<open>cos \<omega> = normalize p $ 1\<close>
[PROOF STATE]
proof (chain)
picking this:
\<omega> - pi = arccos (cos (\<omega> - pi))
cos \<omega> = normalize p $ 1
[PROOF STEP]
have "\<omega> - pi = arccos (- normalize p $ 1)"
[PROOF STATE]
proof (prove)
using this:
\<omega> - pi = arccos (cos (\<omega> - pi))
cos \<omega> = normalize p $ 1

goal (1 subgoal):
 1. \<omega> - pi = arccos (- normalize p $ 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<omega> - pi = arccos (- normalize p $ 1)

goal (1 subgoal):
 1. \<not> 0 \<le> p $ 2 \<Longrightarrow> \<omega> = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<omega> - pi = arccos (- normalize p $ 1)
[PROOF STEP]
have "\<omega> = pi + arccos (- normalize p $ 1)"
[PROOF STATE]
proof (prove)
using this:
\<omega> - pi = arccos (- normalize p $ 1)

goal (1 subgoal):
 1. \<omega> = pi + arccos (- normalize p $ 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<omega> = pi + arccos (- normalize p $ 1)

goal (1 subgoal):
 1. \<not> 0 \<le> p $ 2 \<Longrightarrow> \<omega> = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<omega> = pi + arccos (- normalize p $ 1)
[PROOF STEP]
show "\<omega> = ?a"
[PROOF STATE]
proof (prove)
using this:
\<omega> = pi + arccos (- normalize p $ 1)

goal (1 subgoal):
 1. \<omega> = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))
[PROOF STEP]
using \<open>\<not> 0 \<le> p $ 2\<close>
[PROOF STATE]
proof (prove)
using this:
\<omega> = pi + arccos (- normalize p $ 1)
\<not> 0 \<le> p $ 2

goal (1 subgoal):
 1. \<omega> = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<omega> = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<omega> = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))

goal (1 subgoal):
 1. 0 \<le> radiant_of p \<and> radiant_of p < 2 * pi \<and> of_radiant (radiant_of p) = normalize p
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
0 \<le> ?\<omega>2 \<and> ?\<omega>2 < 2 * pi \<and> of_radiant ?\<omega>2 = normalize p \<Longrightarrow> ?\<omega>2 = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))

goal (1 subgoal):
 1. 0 \<le> radiant_of p \<and> radiant_of p < 2 * pi \<and> of_radiant (radiant_of p) = normalize p
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 \<le> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) \<and> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi \<and> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) = normalize p
0 \<le> ?\<omega>2 \<and> ?\<omega>2 < 2 * pi \<and> of_radiant ?\<omega>2 = normalize p \<Longrightarrow> ?\<omega>2 = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) \<and> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi \<and> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) = normalize p
0 \<le> ?\<omega>2 \<and> ?\<omega>2 < 2 * pi \<and> of_radiant ?\<omega>2 = normalize p \<Longrightarrow> ?\<omega>2 = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))

goal (1 subgoal):
 1. 0 \<le> radiant_of p \<and> radiant_of p < 2 * pi \<and> of_radiant (radiant_of p) = normalize p
[PROOF STEP]
unfolding radiant_of_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) \<and> (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) < 2 * pi \<and> of_radiant (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1)) = normalize p
0 \<le> ?\<omega>2 \<and> ?\<omega>2 < 2 * pi \<and> of_radiant ?\<omega>2 = normalize p \<Longrightarrow> ?\<omega>2 = (if 0 \<le> p $ 2 then arccos (normalize p $ 1) else pi + arccos (- normalize p $ 1))

goal (1 subgoal):
 1. 0 \<le> (THE \<omega>. 0 \<le> \<omega> \<and> \<omega> < 2 * pi \<and> of_radiant \<omega> = normalize p) \<and> (THE \<omega>. 0 \<le> \<omega> \<and> \<omega> < 2 * pi \<and> of_radiant \<omega> = normalize p) < 2 * pi \<and> of_radiant (THE \<omega>. 0 \<le> \<omega> \<and> \<omega> < 2 * pi \<and> of_radiant \<omega> = normalize p) = normalize p
[PROOF STEP]
by (rule theI)
[PROOF STATE]
proof (state)
this:
0 \<le> radiant_of p \<and> radiant_of p < 2 * pi \<and> of_radiant (radiant_of p) = normalize p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma radiant_of_bounds [simp]:
  "0 \<le> radiant_of p" "radiant_of p < 2 * pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> radiant_of p &&& radiant_of p < 2 * pi
[PROOF STEP]
using radiant_of
[PROOF STATE]
proof (prove)
using this:
0 \<le> radiant_of ?p \<and> radiant_of ?p < 2 * pi \<and> of_radiant (radiant_of ?p) = normalize ?p

goal (1 subgoal):
 1. 0 \<le> radiant_of p &&& radiant_of p < 2 * pi
[PROOF STEP]
by auto


[STATEMENT]
lemma radiant_of_weak_ubound [simp]:
  "radiant_of p \<le> 2 * pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. radiant_of p \<le> 2 * pi
[PROOF STEP]
using radiant_of_bounds(2)[of p]
[PROOF STATE]
proof (prove)
using this:
radiant_of p < 2 * pi

goal (1 subgoal):
 1. radiant_of p \<le> 2 * pi
[PROOF STEP]
by linarith


[STATEMENT]
lemma polar_form_eq:
  "norm p *\<^sub>R of_radiant (radiant_of p) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm p *\<^sub>R of_radiant (radiant_of p) = p
[PROOF STEP]
using radiant_of normalize_eq
[PROOF STATE]
proof (prove)
using this:
0 \<le> radiant_of ?p \<and> radiant_of ?p < 2 * pi \<and> of_radiant (radiant_of ?p) = normalize ?p
norm ?p *\<^sub>R normalize ?p = ?p

goal (1 subgoal):
 1. norm p *\<^sub>R of_radiant (radiant_of p) = p
[PROOF STEP]
by simp


[STATEMENT]
lemma relative_polar_form_eq:
  "Q + dist P Q *\<^sub>R of_radiant (radiant_of (P - Q)) = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q + dist P Q *\<^sub>R of_radiant (radiant_of (P - Q)) = P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Q + dist P Q *\<^sub>R of_radiant (radiant_of (P - Q)) = P
[PROOF STEP]
have "norm (P - Q) *\<^sub>R of_radiant (radiant_of (P - Q)) = P - Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (P - Q) *\<^sub>R of_radiant (radiant_of (P - Q)) = P - Q
[PROOF STEP]
unfolding polar_form_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P - Q = P - Q
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
norm (P - Q) *\<^sub>R of_radiant (radiant_of (P - Q)) = P - Q

goal (1 subgoal):
 1. Q + dist P Q *\<^sub>R of_radiant (radiant_of (P - Q)) = P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
norm (P - Q) *\<^sub>R of_radiant (radiant_of (P - Q)) = P - Q

goal (1 subgoal):
 1. Q + dist P Q *\<^sub>R of_radiant (radiant_of (P - Q)) = P
[PROOF STEP]
have "dist P Q = norm (P - Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist P Q = norm (P - Q)
[PROOF STEP]
by (simp add: dist_norm)
[PROOF STATE]
proof (state)
this:
dist P Q = norm (P - Q)

goal (1 subgoal):
 1. Q + dist P Q *\<^sub>R of_radiant (radiant_of (P - Q)) = P
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
norm (P - Q) *\<^sub>R of_radiant (radiant_of (P - Q)) = P - Q
dist P Q = norm (P - Q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
norm (P - Q) *\<^sub>R of_radiant (radiant_of (P - Q)) = P - Q
dist P Q = norm (P - Q)

goal (1 subgoal):
 1. Q + dist P Q *\<^sub>R of_radiant (radiant_of (P - Q)) = P
[PROOF STEP]
by (metis add.commute diff_add_cancel)
[PROOF STATE]
proof (state)
this:
Q + dist P Q *\<^sub>R of_radiant (radiant_of (P - Q)) = P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dist_circle_segment:
  assumes "0 \<le> radius" "0 \<le> \<alpha>" "\<alpha> \<le> \<beta>" "\<beta> \<le> 2 * pi"
  shows "dist (center + radius *\<^sub>R of_radiant \<alpha>) (center + radius *\<^sub>R of_radiant \<beta>) = 2 * radius * sin ((\<beta> - \<alpha>) / 2)"
    (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (center + radius *\<^sub>R of_radiant \<alpha>) (center + radius *\<^sub>R of_radiant \<beta>) = 2 * radius * sin ((\<beta> - \<alpha>) / 2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist (center + radius *\<^sub>R of_radiant \<alpha>) (center + radius *\<^sub>R of_radiant \<beta>) = 2 * radius * sin ((\<beta> - \<alpha>) / 2)
[PROOF STEP]
have trigonometry: "(cos \<alpha> - cos \<beta>)\<^sup>2 + (sin \<alpha> - sin \<beta>)\<^sup>2 = (2 *  sin ((\<beta> - \<alpha>) / 2))\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cos \<alpha> - cos \<beta>)\<^sup>2 + (sin \<alpha> - sin \<beta>)\<^sup>2 = (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (cos \<alpha> - cos \<beta>)\<^sup>2 + (sin \<alpha> - sin \<beta>)\<^sup>2 = (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2
[PROOF STEP]
have sin_diff_minus: "sin ((\<alpha> - \<beta>) / 2) = - sin ((\<beta> - \<alpha>) / 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sin ((\<alpha> - \<beta>) / 2) = - sin ((\<beta> - \<alpha>) / 2)
[PROOF STEP]
by (simp only: sin_minus[symmetric] minus_divide_left minus_diff_eq)
[PROOF STATE]
proof (state)
this:
sin ((\<alpha> - \<beta>) / 2) = - sin ((\<beta> - \<alpha>) / 2)

goal (1 subgoal):
 1. (cos \<alpha> - cos \<beta>)\<^sup>2 + (sin \<alpha> - sin \<beta>)\<^sup>2 = (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2
[PROOF STEP]
have "(cos \<alpha> - cos \<beta>)\<^sup>2 + (sin \<alpha> - sin \<beta>)\<^sup>2 =
      (2 * sin ((\<alpha> + \<beta>) / 2) * sin ((\<beta> - \<alpha>) / 2))\<^sup>2 + (2 * sin ((\<alpha> - \<beta>) / 2) * cos ((\<alpha> + \<beta>) / 2))\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cos \<alpha> - cos \<beta>)\<^sup>2 + (sin \<alpha> - sin \<beta>)\<^sup>2 = (2 * sin ((\<alpha> + \<beta>) / 2) * sin ((\<beta> - \<alpha>) / 2))\<^sup>2 + (2 * sin ((\<alpha> - \<beta>) / 2) * cos ((\<alpha> + \<beta>) / 2))\<^sup>2
[PROOF STEP]
by (simp only: cos_diff_cos sin_diff_sin)
[PROOF STATE]
proof (state)
this:
(cos \<alpha> - cos \<beta>)\<^sup>2 + (sin \<alpha> - sin \<beta>)\<^sup>2 = (2 * sin ((\<alpha> + \<beta>) / 2) * sin ((\<beta> - \<alpha>) / 2))\<^sup>2 + (2 * sin ((\<alpha> - \<beta>) / 2) * cos ((\<alpha> + \<beta>) / 2))\<^sup>2

goal (1 subgoal):
 1. (cos \<alpha> - cos \<beta>)\<^sup>2 + (sin \<alpha> - sin \<beta>)\<^sup>2 = (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(cos \<alpha> - cos \<beta>)\<^sup>2 + (sin \<alpha> - sin \<beta>)\<^sup>2 = (2 * sin ((\<alpha> + \<beta>) / 2) * sin ((\<beta> - \<alpha>) / 2))\<^sup>2 + (2 * sin ((\<alpha> - \<beta>) / 2) * cos ((\<alpha> + \<beta>) / 2))\<^sup>2

goal (1 subgoal):
 1. (cos \<alpha> - cos \<beta>)\<^sup>2 + (sin \<alpha> - sin \<beta>)\<^sup>2 = (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2
[PROOF STEP]
have "\<dots> = (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2 * ((sin ((\<alpha> + \<beta>) / 2))\<^sup>2 + (cos ((\<alpha> + \<beta>) / 2))\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (2 * sin ((\<alpha> + \<beta>) / 2) * sin ((\<beta> - \<alpha>) / 2))\<^sup>2 + (2 * sin ((\<alpha> - \<beta>) / 2) * cos ((\<alpha> + \<beta>) / 2))\<^sup>2 = (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2 * ((sin ((\<alpha> + \<beta>) / 2))\<^sup>2 + (cos ((\<alpha> + \<beta>) / 2))\<^sup>2)
[PROOF STEP]
unfolding sin_diff_minus
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (2 * sin ((\<alpha> + \<beta>) / 2) * sin ((\<beta> - \<alpha>) / 2))\<^sup>2 + (2 * - sin ((\<beta> - \<alpha>) / 2) * cos ((\<alpha> + \<beta>) / 2))\<^sup>2 = (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2 * ((sin ((\<alpha> + \<beta>) / 2))\<^sup>2 + (cos ((\<alpha> + \<beta>) / 2))\<^sup>2)
[PROOF STEP]
by algebra
[PROOF STATE]
proof (state)
this:
(2 * sin ((\<alpha> + \<beta>) / 2) * sin ((\<beta> - \<alpha>) / 2))\<^sup>2 + (2 * sin ((\<alpha> - \<beta>) / 2) * cos ((\<alpha> + \<beta>) / 2))\<^sup>2 = (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2 * ((sin ((\<alpha> + \<beta>) / 2))\<^sup>2 + (cos ((\<alpha> + \<beta>) / 2))\<^sup>2)

goal (1 subgoal):
 1. (cos \<alpha> - cos \<beta>)\<^sup>2 + (sin \<alpha> - sin \<beta>)\<^sup>2 = (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(2 * sin ((\<alpha> + \<beta>) / 2) * sin ((\<beta> - \<alpha>) / 2))\<^sup>2 + (2 * sin ((\<alpha> - \<beta>) / 2) * cos ((\<alpha> + \<beta>) / 2))\<^sup>2 = (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2 * ((sin ((\<alpha> + \<beta>) / 2))\<^sup>2 + (cos ((\<alpha> + \<beta>) / 2))\<^sup>2)

goal (1 subgoal):
 1. (cos \<alpha> - cos \<beta>)\<^sup>2 + (sin \<alpha> - sin \<beta>)\<^sup>2 = (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2
[PROOF STEP]
have "\<dots> = (2 *  sin ((\<beta> - \<alpha>) / 2))\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2 * ((sin ((\<alpha> + \<beta>) / 2))\<^sup>2 + (cos ((\<alpha> + \<beta>) / 2))\<^sup>2) = (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2 * ((sin ((\<alpha> + \<beta>) / 2))\<^sup>2 + (cos ((\<alpha> + \<beta>) / 2))\<^sup>2) = (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2

goal (1 subgoal):
 1. (cos \<alpha> - cos \<beta>)\<^sup>2 + (sin \<alpha> - sin \<beta>)\<^sup>2 = (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(cos \<alpha> - cos \<beta>)\<^sup>2 + (sin \<alpha> - sin \<beta>)\<^sup>2 = (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(cos \<alpha> - cos \<beta>)\<^sup>2 + (sin \<alpha> - sin \<beta>)\<^sup>2 = (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2

goal (1 subgoal):
 1. (cos \<alpha> - cos \<beta>)\<^sup>2 + (sin \<alpha> - sin \<beta>)\<^sup>2 = (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(cos \<alpha> - cos \<beta>)\<^sup>2 + (sin \<alpha> - sin \<beta>)\<^sup>2 = (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(cos \<alpha> - cos \<beta>)\<^sup>2 + (sin \<alpha> - sin \<beta>)\<^sup>2 = (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2

goal (1 subgoal):
 1. dist (center + radius *\<^sub>R of_radiant \<alpha>) (center + radius *\<^sub>R of_radiant \<beta>) = 2 * radius * sin ((\<beta> - \<alpha>) / 2)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 \<le> radius
0 \<le> \<alpha>
\<alpha> \<le> \<beta>
\<beta> \<le> 2 * pi
[PROOF STEP]
have "0 \<le> sin ((\<beta> - \<alpha>) / 2)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> radius
0 \<le> \<alpha>
\<alpha> \<le> \<beta>
\<beta> \<le> 2 * pi

goal (1 subgoal):
 1. 0 \<le> sin ((\<beta> - \<alpha>) / 2)
[PROOF STEP]
by (simp add: sin_ge_zero)
[PROOF STATE]
proof (state)
this:
0 \<le> sin ((\<beta> - \<alpha>) / 2)

goal (1 subgoal):
 1. dist (center + radius *\<^sub>R of_radiant \<alpha>) (center + radius *\<^sub>R of_radiant \<beta>) = 2 * radius * sin ((\<beta> - \<alpha>) / 2)
[PROOF STEP]
have "?lhs = sqrt (radius\<^sup>2 * ((cos \<alpha> - cos \<beta>)\<^sup>2 + (sin \<alpha> - sin \<beta>)\<^sup>2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (center + radius *\<^sub>R of_radiant \<alpha>) (center + radius *\<^sub>R of_radiant \<beta>) = sqrt (radius\<^sup>2 * ((cos \<alpha> - cos \<beta>)\<^sup>2 + (sin \<alpha> - sin \<beta>)\<^sup>2))
[PROOF STEP]
unfolding dist_eq_on_real_2_vec
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt (((center + radius *\<^sub>R of_radiant \<alpha>) $ 1 - (center + radius *\<^sub>R of_radiant \<beta>) $ 1)\<^sup>2 + ((center + radius *\<^sub>R of_radiant \<alpha>) $ 2 - (center + radius *\<^sub>R of_radiant \<beta>) $ 2)\<^sup>2) = sqrt (radius\<^sup>2 * ((cos \<alpha> - cos \<beta>)\<^sup>2 + (sin \<alpha> - sin \<beta>)\<^sup>2))
[PROOF STEP]
by simp algebra
[PROOF STATE]
proof (state)
this:
dist (center + radius *\<^sub>R of_radiant \<alpha>) (center + radius *\<^sub>R of_radiant \<beta>) = sqrt (radius\<^sup>2 * ((cos \<alpha> - cos \<beta>)\<^sup>2 + (sin \<alpha> - sin \<beta>)\<^sup>2))

goal (1 subgoal):
 1. dist (center + radius *\<^sub>R of_radiant \<alpha>) (center + radius *\<^sub>R of_radiant \<beta>) = 2 * radius * sin ((\<beta> - \<alpha>) / 2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (center + radius *\<^sub>R of_radiant \<alpha>) (center + radius *\<^sub>R of_radiant \<beta>) = sqrt (radius\<^sup>2 * ((cos \<alpha> - cos \<beta>)\<^sup>2 + (sin \<alpha> - sin \<beta>)\<^sup>2))

goal (1 subgoal):
 1. dist (center + radius *\<^sub>R of_radiant \<alpha>) (center + radius *\<^sub>R of_radiant \<beta>) = 2 * radius * sin ((\<beta> - \<alpha>) / 2)
[PROOF STEP]
have "\<dots> = sqrt (radius\<^sup>2 *  (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt (radius\<^sup>2 * ((cos \<alpha> - cos \<beta>)\<^sup>2 + (sin \<alpha> - sin \<beta>)\<^sup>2)) = sqrt (radius\<^sup>2 * (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2)
[PROOF STEP]
by (simp add: trigonometry)
[PROOF STATE]
proof (state)
this:
sqrt (radius\<^sup>2 * ((cos \<alpha> - cos \<beta>)\<^sup>2 + (sin \<alpha> - sin \<beta>)\<^sup>2)) = sqrt (radius\<^sup>2 * (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2)

goal (1 subgoal):
 1. dist (center + radius *\<^sub>R of_radiant \<alpha>) (center + radius *\<^sub>R of_radiant \<beta>) = 2 * radius * sin ((\<beta> - \<alpha>) / 2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sqrt (radius\<^sup>2 * ((cos \<alpha> - cos \<beta>)\<^sup>2 + (sin \<alpha> - sin \<beta>)\<^sup>2)) = sqrt (radius\<^sup>2 * (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2)

goal (1 subgoal):
 1. dist (center + radius *\<^sub>R of_radiant \<alpha>) (center + radius *\<^sub>R of_radiant \<beta>) = 2 * radius * sin ((\<beta> - \<alpha>) / 2)
[PROOF STEP]
have "\<dots> = ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt (radius\<^sup>2 * (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2) = 2 * radius * sin ((\<beta> - \<alpha>) / 2)
[PROOF STEP]
using \<open>0 \<le> radius\<close> \<open>0 \<le> sin ((\<beta> - \<alpha>) / 2)\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> radius
0 \<le> sin ((\<beta> - \<alpha>) / 2)

goal (1 subgoal):
 1. sqrt (radius\<^sup>2 * (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2) = 2 * radius * sin ((\<beta> - \<alpha>) / 2)
[PROOF STEP]
by (simp add: real_sqrt_mult)
[PROOF STATE]
proof (state)
this:
sqrt (radius\<^sup>2 * (2 * sin ((\<beta> - \<alpha>) / 2))\<^sup>2) = 2 * radius * sin ((\<beta> - \<alpha>) / 2)

goal (1 subgoal):
 1. dist (center + radius *\<^sub>R of_radiant \<alpha>) (center + radius *\<^sub>R of_radiant \<beta>) = 2 * radius * sin ((\<beta> - \<alpha>) / 2)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (center + radius *\<^sub>R of_radiant \<alpha>) (center + radius *\<^sub>R of_radiant \<beta>) = 2 * radius * sin ((\<beta> - \<alpha>) / 2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist (center + radius *\<^sub>R of_radiant \<alpha>) (center + radius *\<^sub>R of_radiant \<beta>) = 2 * radius * sin ((\<beta> - \<alpha>) / 2)

goal (1 subgoal):
 1. dist (center + radius *\<^sub>R of_radiant \<alpha>) (center + radius *\<^sub>R of_radiant \<beta>) = 2 * radius * sin ((\<beta> - \<alpha>) / 2)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
dist (center + radius *\<^sub>R of_radiant \<alpha>) (center + radius *\<^sub>R of_radiant \<beta>) = 2 * radius * sin ((\<beta> - \<alpha>) / 2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem ptolemy_trigonometric:
  fixes \<omega>\<^sub>1 \<omega>\<^sub>2 \<omega>\<^sub>3 :: real
  shows "sin (\<omega>\<^sub>1 + \<omega>\<^sub>2) * sin (\<omega>\<^sub>2 + \<omega>\<^sub>3) = sin \<omega>\<^sub>1 * sin \<omega>\<^sub>3 + sin \<omega>\<^sub>2 * sin (\<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sin (\<omega>\<^sub>1 + \<omega>\<^sub>2) * sin (\<omega>\<^sub>2 + \<omega>\<^sub>3) = sin \<omega>\<^sub>1 * sin \<omega>\<^sub>3 + sin \<omega>\<^sub>2 * sin (\<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sin (\<omega>\<^sub>1 + \<omega>\<^sub>2) * sin (\<omega>\<^sub>2 + \<omega>\<^sub>3) = sin \<omega>\<^sub>1 * sin \<omega>\<^sub>3 + sin \<omega>\<^sub>2 * sin (\<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3)
[PROOF STEP]
have "sin (\<omega>\<^sub>1 + \<omega>\<^sub>2) * sin (\<omega>\<^sub>2 + \<omega>\<^sub>3) = ((sin \<omega>\<^sub>2)\<^sup>2 + (cos \<omega>\<^sub>2)\<^sup>2) * sin \<omega>\<^sub>1 * sin \<omega>\<^sub>3 + sin \<omega>\<^sub>2 * sin (\<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sin (\<omega>\<^sub>1 + \<omega>\<^sub>2) * sin (\<omega>\<^sub>2 + \<omega>\<^sub>3) = ((sin \<omega>\<^sub>2)\<^sup>2 + (cos \<omega>\<^sub>2)\<^sup>2) * sin \<omega>\<^sub>1 * sin \<omega>\<^sub>3 + sin \<omega>\<^sub>2 * sin (\<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3)
[PROOF STEP]
by (simp only: sin_add cos_add) algebra
[PROOF STATE]
proof (state)
this:
sin (\<omega>\<^sub>1 + \<omega>\<^sub>2) * sin (\<omega>\<^sub>2 + \<omega>\<^sub>3) = ((sin \<omega>\<^sub>2)\<^sup>2 + (cos \<omega>\<^sub>2)\<^sup>2) * sin \<omega>\<^sub>1 * sin \<omega>\<^sub>3 + sin \<omega>\<^sub>2 * sin (\<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3)

goal (1 subgoal):
 1. sin (\<omega>\<^sub>1 + \<omega>\<^sub>2) * sin (\<omega>\<^sub>2 + \<omega>\<^sub>3) = sin \<omega>\<^sub>1 * sin \<omega>\<^sub>3 + sin \<omega>\<^sub>2 * sin (\<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sin (\<omega>\<^sub>1 + \<omega>\<^sub>2) * sin (\<omega>\<^sub>2 + \<omega>\<^sub>3) = ((sin \<omega>\<^sub>2)\<^sup>2 + (cos \<omega>\<^sub>2)\<^sup>2) * sin \<omega>\<^sub>1 * sin \<omega>\<^sub>3 + sin \<omega>\<^sub>2 * sin (\<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3)

goal (1 subgoal):
 1. sin (\<omega>\<^sub>1 + \<omega>\<^sub>2) * sin (\<omega>\<^sub>2 + \<omega>\<^sub>3) = sin \<omega>\<^sub>1 * sin \<omega>\<^sub>3 + sin \<omega>\<^sub>2 * sin (\<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3)
[PROOF STEP]
have "\<dots> = sin \<omega>\<^sub>1 * sin \<omega>\<^sub>3 + sin \<omega>\<^sub>2 * sin (\<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((sin \<omega>\<^sub>2)\<^sup>2 + (cos \<omega>\<^sub>2)\<^sup>2) * sin \<omega>\<^sub>1 * sin \<omega>\<^sub>3 + sin \<omega>\<^sub>2 * sin (\<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3) = sin \<omega>\<^sub>1 * sin \<omega>\<^sub>3 + sin \<omega>\<^sub>2 * sin (\<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((sin \<omega>\<^sub>2)\<^sup>2 + (cos \<omega>\<^sub>2)\<^sup>2) * sin \<omega>\<^sub>1 * sin \<omega>\<^sub>3 + sin \<omega>\<^sub>2 * sin (\<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3) = sin \<omega>\<^sub>1 * sin \<omega>\<^sub>3 + sin \<omega>\<^sub>2 * sin (\<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3)

goal (1 subgoal):
 1. sin (\<omega>\<^sub>1 + \<omega>\<^sub>2) * sin (\<omega>\<^sub>2 + \<omega>\<^sub>3) = sin \<omega>\<^sub>1 * sin \<omega>\<^sub>3 + sin \<omega>\<^sub>2 * sin (\<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sin (\<omega>\<^sub>1 + \<omega>\<^sub>2) * sin (\<omega>\<^sub>2 + \<omega>\<^sub>3) = sin \<omega>\<^sub>1 * sin \<omega>\<^sub>3 + sin \<omega>\<^sub>2 * sin (\<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sin (\<omega>\<^sub>1 + \<omega>\<^sub>2) * sin (\<omega>\<^sub>2 + \<omega>\<^sub>3) = sin \<omega>\<^sub>1 * sin \<omega>\<^sub>3 + sin \<omega>\<^sub>2 * sin (\<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3)

goal (1 subgoal):
 1. sin (\<omega>\<^sub>1 + \<omega>\<^sub>2) * sin (\<omega>\<^sub>2 + \<omega>\<^sub>3) = sin \<omega>\<^sub>1 * sin \<omega>\<^sub>3 + sin \<omega>\<^sub>2 * sin (\<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sin (\<omega>\<^sub>1 + \<omega>\<^sub>2) * sin (\<omega>\<^sub>2 + \<omega>\<^sub>3) = sin \<omega>\<^sub>1 * sin \<omega>\<^sub>3 + sin \<omega>\<^sub>2 * sin (\<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem ptolemy:
  fixes A B C D center :: "real ^ 2"
  assumes "dist center A = radius" and "dist center B = radius"
  assumes "dist center C = radius" and "dist center D = radius"
  assumes ordering_of_points:
    "radiant_of (A - center) \<le> radiant_of (B - center)"
    "radiant_of (B - center) \<le> radiant_of (C - center)"
    "radiant_of (C - center) \<le> radiant_of (D - center)"
  shows "dist A C * dist B D = dist A B * dist C D + dist A D * dist B C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist A C * dist B D = dist A B * dist C D + dist A D * dist B C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist A C * dist B D = dist A B * dist C D + dist A D * dist B C
[PROOF STEP]
from \<open>dist center A = radius\<close>
[PROOF STATE]
proof (chain)
picking this:
dist center A = radius
[PROOF STEP]
have "0 \<le> radius"
[PROOF STATE]
proof (prove)
using this:
dist center A = radius

goal (1 subgoal):
 1. 0 \<le> radius
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> radius

goal (1 subgoal):
 1. dist A C * dist B D = dist A B * dist C D + dist A D * dist B C
[PROOF STEP]
define \<alpha> \<beta> \<gamma> \<delta>
    where "\<alpha> = radiant_of (A - center)" and "\<beta> = radiant_of (B - center)"
    and "\<gamma> = radiant_of (C - center)" and "\<delta> = radiant_of (D - center)"
[PROOF STATE]
proof (state)
this:
\<alpha> = radiant_of (A - center)
\<beta> = radiant_of (B - center)
\<gamma> = radiant_of (C - center)
\<delta> = radiant_of (D - center)

goal (1 subgoal):
 1. dist A C * dist B D = dist A B * dist C D + dist A D * dist B C
[PROOF STEP]
from ordering_of_points
[PROOF STATE]
proof (chain)
picking this:
radiant_of (A - center) \<le> radiant_of (B - center)
radiant_of (B - center) \<le> radiant_of (C - center)
radiant_of (C - center) \<le> radiant_of (D - center)
[PROOF STEP]
have angle_basics:
    "\<alpha> \<le> \<beta>" "\<beta> \<le> \<gamma>" "\<gamma> \<le> \<delta>"
    "0 \<le> \<alpha>" "\<alpha> \<le> 2 * pi" "0 \<le> \<beta>" "\<beta> \<le> 2 * pi"
    "0 \<le> \<gamma>" "\<gamma> \<le> 2 * pi" "0 \<le> \<delta>" "\<delta> \<le> 2 * pi"
[PROOF STATE]
proof (prove)
using this:
radiant_of (A - center) \<le> radiant_of (B - center)
radiant_of (B - center) \<le> radiant_of (C - center)
radiant_of (C - center) \<le> radiant_of (D - center)

goal (1 subgoal):
 1. ((\<alpha> \<le> \<beta> &&& \<beta> \<le> \<gamma>) &&& \<gamma> \<le> \<delta> &&& 0 \<le> \<alpha> &&& \<alpha> \<le> 2 * pi) &&& (0 \<le> \<beta> &&& \<beta> \<le> 2 * pi &&& 0 \<le> \<gamma>) &&& \<gamma> \<le> 2 * pi &&& 0 \<le> \<delta> &&& \<delta> \<le> 2 * pi
[PROOF STEP]
unfolding \<alpha>_def \<beta>_def \<gamma>_def \<delta>_def
[PROOF STATE]
proof (prove)
using this:
radiant_of (A - center) \<le> radiant_of (B - center)
radiant_of (B - center) \<le> radiant_of (C - center)
radiant_of (C - center) \<le> radiant_of (D - center)

goal (1 subgoal):
 1. ((radiant_of (A - center) \<le> radiant_of (B - center) &&& radiant_of (B - center) \<le> radiant_of (C - center)) &&& radiant_of (C - center) \<le> radiant_of (D - center) &&& 0 \<le> radiant_of (A - center) &&& radiant_of (A - center) \<le> 2 * pi) &&& (0 \<le> radiant_of (B - center) &&& radiant_of (B - center) \<le> 2 * pi &&& 0 \<le> radiant_of (C - center)) &&& radiant_of (C - center) \<le> 2 * pi &&& 0 \<le> radiant_of (D - center) &&& radiant_of (D - center) \<le> 2 * pi
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<alpha> \<le> \<beta>
\<beta> \<le> \<gamma>
\<gamma> \<le> \<delta>
0 \<le> \<alpha>
\<alpha> \<le> 2 * pi
0 \<le> \<beta>
\<beta> \<le> 2 * pi
0 \<le> \<gamma>
\<gamma> \<le> 2 * pi
0 \<le> \<delta>
\<delta> \<le> 2 * pi

goal (1 subgoal):
 1. dist A C * dist B D = dist A B * dist C D + dist A D * dist B C
[PROOF STEP]
from assms(1-4)
[PROOF STATE]
proof (chain)
picking this:
dist center A = radius
dist center B = radius
dist center C = radius
dist center D = radius
[PROOF STEP]
have
    "A = center + radius *\<^sub>R of_radiant \<alpha>" "B = center + radius *\<^sub>R of_radiant \<beta>"
    "C = center + radius *\<^sub>R of_radiant \<gamma>" "D = center + radius *\<^sub>R of_radiant \<delta>"
[PROOF STATE]
proof (prove)
using this:
dist center A = radius
dist center B = radius
dist center C = radius
dist center D = radius

goal (1 subgoal):
 1. (A = center + radius *\<^sub>R of_radiant \<alpha> &&& B = center + radius *\<^sub>R of_radiant \<beta>) &&& C = center + radius *\<^sub>R of_radiant \<gamma> &&& D = center + radius *\<^sub>R of_radiant \<delta>
[PROOF STEP]
unfolding \<alpha>_def \<beta>_def \<gamma>_def \<delta>_def
[PROOF STATE]
proof (prove)
using this:
dist center A = radius
dist center B = radius
dist center C = radius
dist center D = radius

goal (1 subgoal):
 1. (A = center + radius *\<^sub>R of_radiant (radiant_of (A - center)) &&& B = center + radius *\<^sub>R of_radiant (radiant_of (B - center))) &&& C = center + radius *\<^sub>R of_radiant (radiant_of (C - center)) &&& D = center + radius *\<^sub>R of_radiant (radiant_of (D - center))
[PROOF STEP]
using relative_polar_form_eq dist_commute
[PROOF STATE]
proof (prove)
using this:
dist center A = radius
dist center B = radius
dist center C = radius
dist center D = radius
?Q + dist ?P ?Q *\<^sub>R of_radiant (radiant_of (?P - ?Q)) = ?P
dist ?x ?y = dist ?y ?x

goal (1 subgoal):
 1. (A = center + radius *\<^sub>R of_radiant (radiant_of (A - center)) &&& B = center + radius *\<^sub>R of_radiant (radiant_of (B - center))) &&& C = center + radius *\<^sub>R of_radiant (radiant_of (C - center)) &&& D = center + radius *\<^sub>R of_radiant (radiant_of (D - center))
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
A = center + radius *\<^sub>R of_radiant \<alpha>
B = center + radius *\<^sub>R of_radiant \<beta>
C = center + radius *\<^sub>R of_radiant \<gamma>
D = center + radius *\<^sub>R of_radiant \<delta>

goal (1 subgoal):
 1. dist A C * dist B D = dist A B * dist C D + dist A D * dist B C
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
A = center + radius *\<^sub>R of_radiant \<alpha>
B = center + radius *\<^sub>R of_radiant \<beta>
C = center + radius *\<^sub>R of_radiant \<gamma>
D = center + radius *\<^sub>R of_radiant \<delta>
[PROOF STEP]
have dist_eqs:
    "dist A C = 2 * radius * sin ((\<gamma> - \<alpha>) / 2)"
    "dist B D = 2 * radius * sin ((\<delta> - \<beta>) / 2)"
    "dist A B = 2 * radius * sin ((\<beta> - \<alpha>) / 2)"
    "dist C D = 2 * radius * sin ((\<delta> - \<gamma>) / 2)"
    "dist A D = 2 * radius * sin ((\<delta> - \<alpha>) / 2)"
    "dist B C = 2 * radius * sin ((\<gamma> - \<beta>) / 2)"
[PROOF STATE]
proof (prove)
using this:
A = center + radius *\<^sub>R of_radiant \<alpha>
B = center + radius *\<^sub>R of_radiant \<beta>
C = center + radius *\<^sub>R of_radiant \<gamma>
D = center + radius *\<^sub>R of_radiant \<delta>

goal (1 subgoal):
 1. (dist A C = 2 * radius * sin ((\<gamma> - \<alpha>) / 2) &&& dist B D = 2 * radius * sin ((\<delta> - \<beta>) / 2) &&& dist A B = 2 * radius * sin ((\<beta> - \<alpha>) / 2)) &&& dist C D = 2 * radius * sin ((\<delta> - \<gamma>) / 2) &&& dist A D = 2 * radius * sin ((\<delta> - \<alpha>) / 2) &&& dist B C = 2 * radius * sin ((\<gamma> - \<beta>) / 2)
[PROOF STEP]
using angle_basics \<open>radius \<ge> 0\<close> dist_circle_segment
[PROOF STATE]
proof (prove)
using this:
A = center + radius *\<^sub>R of_radiant \<alpha>
B = center + radius *\<^sub>R of_radiant \<beta>
C = center + radius *\<^sub>R of_radiant \<gamma>
D = center + radius *\<^sub>R of_radiant \<delta>
\<alpha> \<le> \<beta>
\<beta> \<le> \<gamma>
\<gamma> \<le> \<delta>
0 \<le> \<alpha>
\<alpha> \<le> 2 * pi
0 \<le> \<beta>
\<beta> \<le> 2 * pi
0 \<le> \<gamma>
\<gamma> \<le> 2 * pi
0 \<le> \<delta>
\<delta> \<le> 2 * pi
0 \<le> radius
\<lbrakk>0 \<le> ?radius; 0 \<le> ?\<alpha>; ?\<alpha> \<le> ?\<beta>; ?\<beta> \<le> 2 * pi\<rbrakk> \<Longrightarrow> dist (?center + ?radius *\<^sub>R of_radiant ?\<alpha>) (?center + ?radius *\<^sub>R of_radiant ?\<beta>) = 2 * ?radius * sin ((?\<beta> - ?\<alpha>) / 2)

goal (1 subgoal):
 1. (dist A C = 2 * radius * sin ((\<gamma> - \<alpha>) / 2) &&& dist B D = 2 * radius * sin ((\<delta> - \<beta>) / 2) &&& dist A B = 2 * radius * sin ((\<beta> - \<alpha>) / 2)) &&& dist C D = 2 * radius * sin ((\<delta> - \<gamma>) / 2) &&& dist A D = 2 * radius * sin ((\<delta> - \<alpha>) / 2) &&& dist B C = 2 * radius * sin ((\<gamma> - \<beta>) / 2)
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
dist A C = 2 * radius * sin ((\<gamma> - \<alpha>) / 2)
dist B D = 2 * radius * sin ((\<delta> - \<beta>) / 2)
dist A B = 2 * radius * sin ((\<beta> - \<alpha>) / 2)
dist C D = 2 * radius * sin ((\<delta> - \<gamma>) / 2)
dist A D = 2 * radius * sin ((\<delta> - \<alpha>) / 2)
dist B C = 2 * radius * sin ((\<gamma> - \<beta>) / 2)

goal (1 subgoal):
 1. dist A C * dist B D = dist A B * dist C D + dist A D * dist B C
[PROOF STEP]
have "dist A C * dist B D = 4 * radius ^ 2 * sin ((\<gamma> - \<alpha>) / 2) * sin ((\<delta> - \<beta>) / 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist A C * dist B D = 4 * radius\<^sup>2 * sin ((\<gamma> - \<alpha>) / 2) * sin ((\<delta> - \<beta>) / 2)
[PROOF STEP]
unfolding dist_eqs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * radius * sin ((\<gamma> - \<alpha>) / 2) * (2 * radius * sin ((\<delta> - \<beta>) / 2)) = 4 * radius\<^sup>2 * sin ((\<gamma> - \<alpha>) / 2) * sin ((\<delta> - \<beta>) / 2)
[PROOF STEP]
by (simp add: power2_eq_square)
[PROOF STATE]
proof (state)
this:
dist A C * dist B D = 4 * radius\<^sup>2 * sin ((\<gamma> - \<alpha>) / 2) * sin ((\<delta> - \<beta>) / 2)

goal (1 subgoal):
 1. dist A C * dist B D = dist A B * dist C D + dist A D * dist B C
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist A C * dist B D = 4 * radius\<^sup>2 * sin ((\<gamma> - \<alpha>) / 2) * sin ((\<delta> - \<beta>) / 2)

goal (1 subgoal):
 1. dist A C * dist B D = dist A B * dist C D + dist A D * dist B C
[PROOF STEP]
have "\<dots> = 4 * radius ^ 2 * (sin ((\<beta> - \<alpha>) / 2) * sin ((\<delta> - \<gamma>) / 2) + sin ((\<gamma> - \<beta>) / 2) * sin ((\<delta> - \<alpha>) / 2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 4 * radius\<^sup>2 * sin ((\<gamma> - \<alpha>) / 2) * sin ((\<delta> - \<beta>) / 2) = 4 * radius\<^sup>2 * (sin ((\<beta> - \<alpha>) / 2) * sin ((\<delta> - \<gamma>) / 2) + sin ((\<gamma> - \<beta>) / 2) * sin ((\<delta> - \<alpha>) / 2))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 4 * radius\<^sup>2 * sin ((\<gamma> - \<alpha>) / 2) * sin ((\<delta> - \<beta>) / 2) = 4 * radius\<^sup>2 * (sin ((\<beta> - \<alpha>) / 2) * sin ((\<delta> - \<gamma>) / 2) + sin ((\<gamma> - \<beta>) / 2) * sin ((\<delta> - \<alpha>) / 2))
[PROOF STEP]
define \<omega>\<^sub>1 \<omega>\<^sub>2 \<omega>\<^sub>3 where "\<omega>\<^sub>1 = (\<beta> - \<alpha>) / 2" and "\<omega>\<^sub>2 = (\<gamma> - \<beta>) / 2" and "\<omega>\<^sub>3 = (\<delta> - \<gamma>) / 2"
[PROOF STATE]
proof (state)
this:
\<omega>\<^sub>1 = (\<beta> - \<alpha>) / 2
\<omega>\<^sub>2 = (\<gamma> - \<beta>) / 2
\<omega>\<^sub>3 = (\<delta> - \<gamma>) / 2

goal (1 subgoal):
 1. 4 * radius\<^sup>2 * sin ((\<gamma> - \<alpha>) / 2) * sin ((\<delta> - \<beta>) / 2) = 4 * radius\<^sup>2 * (sin ((\<beta> - \<alpha>) / 2) * sin ((\<delta> - \<gamma>) / 2) + sin ((\<gamma> - \<beta>) / 2) * sin ((\<delta> - \<alpha>) / 2))
[PROOF STEP]
have "(\<gamma> - \<alpha>) / 2 = \<omega>\<^sub>1 + \<omega>\<^sub>2" and "(\<delta> - \<beta>) / 2 = \<omega>\<^sub>2 + \<omega>\<^sub>3" and "(\<delta> - \<alpha>) / 2 = \<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<gamma> - \<alpha>) / 2 = \<omega>\<^sub>1 + \<omega>\<^sub>2 &&& (\<delta> - \<beta>) / 2 = \<omega>\<^sub>2 + \<omega>\<^sub>3 &&& (\<delta> - \<alpha>) / 2 = \<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3
[PROOF STEP]
unfolding \<omega>\<^sub>1_def \<omega>\<^sub>2_def \<omega>\<^sub>3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<gamma> - \<alpha>) / 2 = (\<beta> - \<alpha>) / 2 + (\<gamma> - \<beta>) / 2 &&& (\<delta> - \<beta>) / 2 = (\<gamma> - \<beta>) / 2 + (\<delta> - \<gamma>) / 2 &&& (\<delta> - \<alpha>) / 2 = (\<beta> - \<alpha>) / 2 + (\<gamma> - \<beta>) / 2 + (\<delta> - \<gamma>) / 2
[PROOF STEP]
by (auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
(\<gamma> - \<alpha>) / 2 = \<omega>\<^sub>1 + \<omega>\<^sub>2
(\<delta> - \<beta>) / 2 = \<omega>\<^sub>2 + \<omega>\<^sub>3
(\<delta> - \<alpha>) / 2 = \<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3

goal (1 subgoal):
 1. 4 * radius\<^sup>2 * sin ((\<gamma> - \<alpha>) / 2) * sin ((\<delta> - \<beta>) / 2) = 4 * radius\<^sup>2 * (sin ((\<beta> - \<alpha>) / 2) * sin ((\<delta> - \<gamma>) / 2) + sin ((\<gamma> - \<beta>) / 2) * sin ((\<delta> - \<alpha>) / 2))
[PROOF STEP]
have "sin ((\<gamma> - \<alpha>) / 2) * sin ((\<delta> - \<beta>) / 2) = sin (\<omega>\<^sub>1 + \<omega>\<^sub>2) * sin (\<omega>\<^sub>2 + \<omega>\<^sub>3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sin ((\<gamma> - \<alpha>) / 2) * sin ((\<delta> - \<beta>) / 2) = sin (\<omega>\<^sub>1 + \<omega>\<^sub>2) * sin (\<omega>\<^sub>2 + \<omega>\<^sub>3)
[PROOF STEP]
using \<open>(\<gamma> - \<alpha>) / 2 = \<omega>\<^sub>1 + \<omega>\<^sub>2\<close> \<open>(\<delta> - \<beta>) / 2 = \<omega>\<^sub>2 + \<omega>\<^sub>3\<close>
[PROOF STATE]
proof (prove)
using this:
(\<gamma> - \<alpha>) / 2 = \<omega>\<^sub>1 + \<omega>\<^sub>2
(\<delta> - \<beta>) / 2 = \<omega>\<^sub>2 + \<omega>\<^sub>3

goal (1 subgoal):
 1. sin ((\<gamma> - \<alpha>) / 2) * sin ((\<delta> - \<beta>) / 2) = sin (\<omega>\<^sub>1 + \<omega>\<^sub>2) * sin (\<omega>\<^sub>2 + \<omega>\<^sub>3)
[PROOF STEP]
by (simp only:)
[PROOF STATE]
proof (state)
this:
sin ((\<gamma> - \<alpha>) / 2) * sin ((\<delta> - \<beta>) / 2) = sin (\<omega>\<^sub>1 + \<omega>\<^sub>2) * sin (\<omega>\<^sub>2 + \<omega>\<^sub>3)

goal (1 subgoal):
 1. 4 * radius\<^sup>2 * sin ((\<gamma> - \<alpha>) / 2) * sin ((\<delta> - \<beta>) / 2) = 4 * radius\<^sup>2 * (sin ((\<beta> - \<alpha>) / 2) * sin ((\<delta> - \<gamma>) / 2) + sin ((\<gamma> - \<beta>) / 2) * sin ((\<delta> - \<alpha>) / 2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sin ((\<gamma> - \<alpha>) / 2) * sin ((\<delta> - \<beta>) / 2) = sin (\<omega>\<^sub>1 + \<omega>\<^sub>2) * sin (\<omega>\<^sub>2 + \<omega>\<^sub>3)

goal (1 subgoal):
 1. 4 * radius\<^sup>2 * sin ((\<gamma> - \<alpha>) / 2) * sin ((\<delta> - \<beta>) / 2) = 4 * radius\<^sup>2 * (sin ((\<beta> - \<alpha>) / 2) * sin ((\<delta> - \<gamma>) / 2) + sin ((\<gamma> - \<beta>) / 2) * sin ((\<delta> - \<alpha>) / 2))
[PROOF STEP]
have "\<dots> = sin \<omega>\<^sub>1 * sin \<omega>\<^sub>3 + sin \<omega>\<^sub>2 * sin (\<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sin (\<omega>\<^sub>1 + \<omega>\<^sub>2) * sin (\<omega>\<^sub>2 + \<omega>\<^sub>3) = sin \<omega>\<^sub>1 * sin \<omega>\<^sub>3 + sin \<omega>\<^sub>2 * sin (\<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3)
[PROOF STEP]
by (rule ptolemy_trigonometric)
[PROOF STATE]
proof (state)
this:
sin (\<omega>\<^sub>1 + \<omega>\<^sub>2) * sin (\<omega>\<^sub>2 + \<omega>\<^sub>3) = sin \<omega>\<^sub>1 * sin \<omega>\<^sub>3 + sin \<omega>\<^sub>2 * sin (\<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3)

goal (1 subgoal):
 1. 4 * radius\<^sup>2 * sin ((\<gamma> - \<alpha>) / 2) * sin ((\<delta> - \<beta>) / 2) = 4 * radius\<^sup>2 * (sin ((\<beta> - \<alpha>) / 2) * sin ((\<delta> - \<gamma>) / 2) + sin ((\<gamma> - \<beta>) / 2) * sin ((\<delta> - \<alpha>) / 2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sin (\<omega>\<^sub>1 + \<omega>\<^sub>2) * sin (\<omega>\<^sub>2 + \<omega>\<^sub>3) = sin \<omega>\<^sub>1 * sin \<omega>\<^sub>3 + sin \<omega>\<^sub>2 * sin (\<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3)

goal (1 subgoal):
 1. 4 * radius\<^sup>2 * sin ((\<gamma> - \<alpha>) / 2) * sin ((\<delta> - \<beta>) / 2) = 4 * radius\<^sup>2 * (sin ((\<beta> - \<alpha>) / 2) * sin ((\<delta> - \<gamma>) / 2) + sin ((\<gamma> - \<beta>) / 2) * sin ((\<delta> - \<alpha>) / 2))
[PROOF STEP]
have "\<dots> = (sin ((\<beta> - \<alpha>) / 2) * sin ((\<delta> - \<gamma>) / 2) + sin ((\<gamma> - \<beta>) / 2) * sin ((\<delta> - \<alpha>) / 2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sin \<omega>\<^sub>1 * sin \<omega>\<^sub>3 + sin \<omega>\<^sub>2 * sin (\<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3) = sin ((\<beta> - \<alpha>) / 2) * sin ((\<delta> - \<gamma>) / 2) + sin ((\<gamma> - \<beta>) / 2) * sin ((\<delta> - \<alpha>) / 2)
[PROOF STEP]
using \<omega>\<^sub>1_def \<omega>\<^sub>2_def \<omega>\<^sub>3_def \<open>(\<delta> - \<alpha>) / 2 = \<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3\<close>
[PROOF STATE]
proof (prove)
using this:
\<omega>\<^sub>1 = (\<beta> - \<alpha>) / 2
\<omega>\<^sub>2 = (\<gamma> - \<beta>) / 2
\<omega>\<^sub>3 = (\<delta> - \<gamma>) / 2
(\<delta> - \<alpha>) / 2 = \<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3

goal (1 subgoal):
 1. sin \<omega>\<^sub>1 * sin \<omega>\<^sub>3 + sin \<omega>\<^sub>2 * sin (\<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3) = sin ((\<beta> - \<alpha>) / 2) * sin ((\<delta> - \<gamma>) / 2) + sin ((\<gamma> - \<beta>) / 2) * sin ((\<delta> - \<alpha>) / 2)
[PROOF STEP]
by (simp only:)
[PROOF STATE]
proof (state)
this:
sin \<omega>\<^sub>1 * sin \<omega>\<^sub>3 + sin \<omega>\<^sub>2 * sin (\<omega>\<^sub>1 + \<omega>\<^sub>2 + \<omega>\<^sub>3) = sin ((\<beta> - \<alpha>) / 2) * sin ((\<delta> - \<gamma>) / 2) + sin ((\<gamma> - \<beta>) / 2) * sin ((\<delta> - \<alpha>) / 2)

goal (1 subgoal):
 1. 4 * radius\<^sup>2 * sin ((\<gamma> - \<alpha>) / 2) * sin ((\<delta> - \<beta>) / 2) = 4 * radius\<^sup>2 * (sin ((\<beta> - \<alpha>) / 2) * sin ((\<delta> - \<gamma>) / 2) + sin ((\<gamma> - \<beta>) / 2) * sin ((\<delta> - \<alpha>) / 2))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sin ((\<gamma> - \<alpha>) / 2) * sin ((\<delta> - \<beta>) / 2) = sin ((\<beta> - \<alpha>) / 2) * sin ((\<delta> - \<gamma>) / 2) + sin ((\<gamma> - \<beta>) / 2) * sin ((\<delta> - \<alpha>) / 2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sin ((\<gamma> - \<alpha>) / 2) * sin ((\<delta> - \<beta>) / 2) = sin ((\<beta> - \<alpha>) / 2) * sin ((\<delta> - \<gamma>) / 2) + sin ((\<gamma> - \<beta>) / 2) * sin ((\<delta> - \<alpha>) / 2)

goal (1 subgoal):
 1. 4 * radius\<^sup>2 * sin ((\<gamma> - \<alpha>) / 2) * sin ((\<delta> - \<beta>) / 2) = 4 * radius\<^sup>2 * (sin ((\<beta> - \<alpha>) / 2) * sin ((\<delta> - \<gamma>) / 2) + sin ((\<gamma> - \<beta>) / 2) * sin ((\<delta> - \<alpha>) / 2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
4 * radius\<^sup>2 * sin ((\<gamma> - \<alpha>) / 2) * sin ((\<delta> - \<beta>) / 2) = 4 * radius\<^sup>2 * (sin ((\<beta> - \<alpha>) / 2) * sin ((\<delta> - \<gamma>) / 2) + sin ((\<gamma> - \<beta>) / 2) * sin ((\<delta> - \<alpha>) / 2))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
4 * radius\<^sup>2 * sin ((\<gamma> - \<alpha>) / 2) * sin ((\<delta> - \<beta>) / 2) = 4 * radius\<^sup>2 * (sin ((\<beta> - \<alpha>) / 2) * sin ((\<delta> - \<gamma>) / 2) + sin ((\<gamma> - \<beta>) / 2) * sin ((\<delta> - \<alpha>) / 2))

goal (1 subgoal):
 1. dist A C * dist B D = dist A B * dist C D + dist A D * dist B C
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
4 * radius\<^sup>2 * sin ((\<gamma> - \<alpha>) / 2) * sin ((\<delta> - \<beta>) / 2) = 4 * radius\<^sup>2 * (sin ((\<beta> - \<alpha>) / 2) * sin ((\<delta> - \<gamma>) / 2) + sin ((\<gamma> - \<beta>) / 2) * sin ((\<delta> - \<alpha>) / 2))

goal (1 subgoal):
 1. dist A C * dist B D = dist A B * dist C D + dist A D * dist B C
[PROOF STEP]
have "\<dots> = dist A B * dist C D + dist A D * dist B C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 4 * radius\<^sup>2 * (sin ((\<beta> - \<alpha>) / 2) * sin ((\<delta> - \<gamma>) / 2) + sin ((\<gamma> - \<beta>) / 2) * sin ((\<delta> - \<alpha>) / 2)) = dist A B * dist C D + dist A D * dist B C
[PROOF STEP]
unfolding dist_eqs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 4 * radius\<^sup>2 * (sin ((\<beta> - \<alpha>) / 2) * sin ((\<delta> - \<gamma>) / 2) + sin ((\<gamma> - \<beta>) / 2) * sin ((\<delta> - \<alpha>) / 2)) = 2 * radius * sin ((\<beta> - \<alpha>) / 2) * (2 * radius * sin ((\<delta> - \<gamma>) / 2)) + 2 * radius * sin ((\<delta> - \<alpha>) / 2) * (2 * radius * sin ((\<gamma> - \<beta>) / 2))
[PROOF STEP]
by (simp add: distrib_left power2_eq_square)
[PROOF STATE]
proof (state)
this:
4 * radius\<^sup>2 * (sin ((\<beta> - \<alpha>) / 2) * sin ((\<delta> - \<gamma>) / 2) + sin ((\<gamma> - \<beta>) / 2) * sin ((\<delta> - \<alpha>) / 2)) = dist A B * dist C D + dist A D * dist B C

goal (1 subgoal):
 1. dist A C * dist B D = dist A B * dist C D + dist A D * dist B C
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist A C * dist B D = dist A B * dist C D + dist A D * dist B C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist A C * dist B D = dist A B * dist C D + dist A D * dist B C

goal (1 subgoal):
 1. dist A C * dist B D = dist A B * dist C D + dist A D * dist B C
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
dist A C * dist B D = dist A B * dist C D + dist A D * dist B C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mem_ass_forms[simp]: "a |\<in>| ass_forms \<longleftrightarrow> a \<in> set assumptions"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a |\<in>| ass_forms) = (a \<in> set assumptions)
[PROOF STEP]
by (auto simp add: ass_forms_def)


[STATEMENT]
lemma mem_conc_forms[simp]: "a |\<in>| conc_forms \<longleftrightarrow> a \<in> set conclusions"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a |\<in>| conc_forms) = (a \<in> set conclusions)
[PROOF STEP]
by (auto simp add: conc_forms_def)


[STATEMENT]
lemma subst_freshen_assumptions[simp]:
    assumes "pf \<in> set assumptions"
    shows "subst s (freshen a pf) = pf "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst s (freshen a pf) = pf
[PROOF STEP]
using assms assumptions_closed
[PROOF STATE]
proof (prove)
using this:
pf \<in> set assumptions
?a \<in> set assumptions \<Longrightarrow> closed ?a

goal (1 subgoal):
 1. subst s (freshen a pf) = pf
[PROOF STEP]
by (simp add: closed_no_lconsts freshen_def rename_closed subst_closed)


[STATEMENT]
lemma subst_freshen_conclusions[simp]:
    assumes "pf \<in> set conclusions"
    shows "subst s (freshen a pf) = pf "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst s (freshen a pf) = pf
[PROOF STEP]
using assms conclusions_closed
[PROOF STATE]
proof (prove)
using this:
pf \<in> set conclusions
?c \<in> set conclusions \<Longrightarrow> closed ?c

goal (1 subgoal):
 1. subst s (freshen a pf) = pf
[PROOF STEP]
by (simp add: closed_no_lconsts freshen_def rename_closed subst_closed)


[STATEMENT]
lemma subst_freshen_in_ass_formsI:
    assumes "pf \<in> set assumptions"
    shows "subst s (freshen a pf) |\<in>| ass_forms"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst s (freshen a pf) |\<in>| ass_forms
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
pf \<in> set assumptions

goal (1 subgoal):
 1. subst s (freshen a pf) |\<in>| ass_forms
[PROOF STEP]
by simp


[STATEMENT]
lemma subst_freshen_in_conc_formsI:
    assumes "pf \<in> set conclusions"
    shows "subst s (freshen a pf) |\<in>| conc_forms"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst s (freshen a pf) |\<in>| conc_forms
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
pf \<in> set conclusions

goal (1 subgoal):
 1. subst s (freshen a pf) |\<in>| conc_forms
[PROOF STEP]
by simp


[STATEMENT]
lemma vars_clause_mono: "S \<subseteq># C \<Longrightarrow> vars_clause S \<subseteq> vars_clause C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<subseteq># C \<Longrightarrow> vars_clause S \<subseteq> vars_clause C
[PROOF STEP]
unfolding vars_clause_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<subseteq># C \<Longrightarrow> \<Union> (set_mset (image_mset vars_lit S)) \<subseteq> \<Union> (set_mset (image_mset vars_lit C))
[PROOF STEP]
by auto


[STATEMENT]
lemma is_ground_atm_is_ground_on_var:
  assumes "is_ground_atm (A \<cdot> \<sigma>)" and "v \<in> vars_term A"
  shows "is_ground_atm (\<sigma> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_ground_atm (\<sigma> v)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_ground_atm (A \<cdot> \<sigma>)
v \<in> vars_term A

goal (1 subgoal):
 1. is_ground_atm (\<sigma> v)
[PROOF STEP]
proof (induction A)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_ground_atm (Var x \<cdot> \<sigma>); v \<in> vars_term (Var x)\<rbrakk> \<Longrightarrow> is_ground_atm (\<sigma> v)
 2. \<And>x1a x2. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set x2; is_ground_atm (x2a \<cdot> \<sigma>); v \<in> vars_term x2a\<rbrakk> \<Longrightarrow> is_ground_atm (\<sigma> v); is_ground_atm (Fun x1a x2 \<cdot> \<sigma>); v \<in> vars_term (Fun x1a x2)\<rbrakk> \<Longrightarrow> is_ground_atm (\<sigma> v)
[PROOF STEP]
case (Var x)
[PROOF STATE]
proof (state)
this:
is_ground_atm (Var x \<cdot> \<sigma>)
v \<in> vars_term (Var x)

goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_ground_atm (Var x \<cdot> \<sigma>); v \<in> vars_term (Var x)\<rbrakk> \<Longrightarrow> is_ground_atm (\<sigma> v)
 2. \<And>x1a x2. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set x2; is_ground_atm (x2a \<cdot> \<sigma>); v \<in> vars_term x2a\<rbrakk> \<Longrightarrow> is_ground_atm (\<sigma> v); is_ground_atm (Fun x1a x2 \<cdot> \<sigma>); v \<in> vars_term (Fun x1a x2)\<rbrakk> \<Longrightarrow> is_ground_atm (\<sigma> v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_ground_atm (Var x \<cdot> \<sigma>)
v \<in> vars_term (Var x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
is_ground_atm (Var x \<cdot> \<sigma>)
v \<in> vars_term (Var x)

goal (1 subgoal):
 1. is_ground_atm (\<sigma> v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_ground_atm (\<sigma> v)

goal (1 subgoal):
 1. \<And>x1a x2. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set x2; is_ground_atm (x2a \<cdot> \<sigma>); v \<in> vars_term x2a\<rbrakk> \<Longrightarrow> is_ground_atm (\<sigma> v); is_ground_atm (Fun x1a x2 \<cdot> \<sigma>); v \<in> vars_term (Fun x1a x2)\<rbrakk> \<Longrightarrow> is_ground_atm (\<sigma> v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1a x2. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set x2; is_ground_atm (x2a \<cdot> \<sigma>); v \<in> vars_term x2a\<rbrakk> \<Longrightarrow> is_ground_atm (\<sigma> v); is_ground_atm (Fun x1a x2 \<cdot> \<sigma>); v \<in> vars_term (Fun x1a x2)\<rbrakk> \<Longrightarrow> is_ground_atm (\<sigma> v)
[PROOF STEP]
case (Fun f ts)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2a \<in> set ts; is_ground_atm (?x2a \<cdot> \<sigma>); v \<in> vars_term ?x2a\<rbrakk> \<Longrightarrow> is_ground_atm (\<sigma> v)
is_ground_atm (Fun f ts \<cdot> \<sigma>)
v \<in> vars_term (Fun f ts)

goal (1 subgoal):
 1. \<And>x1a x2. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set x2; is_ground_atm (x2a \<cdot> \<sigma>); v \<in> vars_term x2a\<rbrakk> \<Longrightarrow> is_ground_atm (\<sigma> v); is_ground_atm (Fun x1a x2 \<cdot> \<sigma>); v \<in> vars_term (Fun x1a x2)\<rbrakk> \<Longrightarrow> is_ground_atm (\<sigma> v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x2a \<in> set ts; is_ground_atm (?x2a \<cdot> \<sigma>); v \<in> vars_term ?x2a\<rbrakk> \<Longrightarrow> is_ground_atm (\<sigma> v)
is_ground_atm (Fun f ts \<cdot> \<sigma>)
v \<in> vars_term (Fun f ts)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2a \<in> set ts; is_ground_atm (?x2a \<cdot> \<sigma>); v \<in> vars_term ?x2a\<rbrakk> \<Longrightarrow> is_ground_atm (\<sigma> v)
is_ground_atm (Fun f ts \<cdot> \<sigma>)
v \<in> vars_term (Fun f ts)

goal (1 subgoal):
 1. is_ground_atm (\<sigma> v)
[PROOF STEP]
unfolding is_ground_atm_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2a \<in> set ts; \<forall>\<sigma>'. ?x2a \<cdot> \<sigma> = subst_atm_abbrev (?x2a \<cdot> \<sigma>) \<sigma>'; v \<in> vars_term ?x2a\<rbrakk> \<Longrightarrow> \<forall>\<sigma>'. \<sigma> v = subst_atm_abbrev (\<sigma> v) \<sigma>'
\<forall>\<sigma>'. Fun f ts \<cdot> \<sigma> = subst_atm_abbrev (Fun f ts \<cdot> \<sigma>) \<sigma>'
v \<in> vars_term (Fun f ts)

goal (1 subgoal):
 1. \<forall>\<sigma>'. \<sigma> v = subst_atm_abbrev (\<sigma> v) \<sigma>'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_ground_atm (\<sigma> v)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_ground_lit_is_ground_on_var:
  assumes ground_lit: "is_ground_lit (subst_lit L \<sigma>)" and v_in_L: "v \<in> vars_lit L"
  shows "is_ground_atm (\<sigma> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_ground_atm (\<sigma> v)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_ground_atm (\<sigma> v)
[PROOF STEP]
let ?A = "atm_of L"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_ground_atm (\<sigma> v)
[PROOF STEP]
from v_in_L
[PROOF STATE]
proof (chain)
picking this:
v \<in> vars_lit L
[PROOF STEP]
have A_p: "v \<in> vars_term ?A"
[PROOF STATE]
proof (prove)
using this:
v \<in> vars_lit L

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

goal (1 subgoal):
 1. is_ground_atm (\<sigma> v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> vars_lit L
[PROOF STEP]
have "is_ground_atm (?A \<cdot> \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
v \<in> vars_lit L

goal (1 subgoal):
 1. is_ground_atm (subst_atm_abbrev (atm_of L) \<sigma>)
[PROOF STEP]
using ground_lit
[PROOF STATE]
proof (prove)
using this:
v \<in> vars_lit L
is_ground_lit (subst_lit L \<sigma>)

goal (1 subgoal):
 1. is_ground_atm (subst_atm_abbrev (atm_of L) \<sigma>)
[PROOF STEP]
unfolding is_ground_lit_def
[PROOF STATE]
proof (prove)
using this:
v \<in> vars_lit L
is_ground_atm (atm_of (subst_lit L \<sigma>))

goal (1 subgoal):
 1. is_ground_atm (subst_atm_abbrev (atm_of L) \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_ground_atm (subst_atm_abbrev (atm_of L) \<sigma>)

goal (1 subgoal):
 1. is_ground_atm (\<sigma> v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_ground_atm (subst_atm_abbrev (atm_of L) \<sigma>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_ground_atm (subst_atm_abbrev (atm_of L) \<sigma>)

goal (1 subgoal):
 1. is_ground_atm (\<sigma> v)
[PROOF STEP]
using A_p is_ground_atm_is_ground_on_var
[PROOF STATE]
proof (prove)
using this:
is_ground_atm (subst_atm_abbrev (atm_of L) \<sigma>)
v \<in> vars_lit L
\<lbrakk>is_ground_atm (?A \<cdot> ?\<sigma>); ?v \<in> vars_term ?A\<rbrakk> \<Longrightarrow> is_ground_atm (?\<sigma> ?v)

goal (1 subgoal):
 1. is_ground_atm (\<sigma> v)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
is_ground_atm (\<sigma> v)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_ground_cls_is_ground_on_var:
  assumes
    ground_clause: "is_ground_cls (subst_cls C \<sigma>)" and
    v_in_C: "v \<in> vars_clause C"
  shows "is_ground_atm (\<sigma> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_ground_atm (\<sigma> v)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_ground_atm (\<sigma> v)
[PROOF STEP]
from v_in_C
[PROOF STATE]
proof (chain)
picking this:
v \<in> vars_clause C
[PROOF STEP]
obtain L where L_p: "L \<in># C" "v \<in> vars_lit L"
[PROOF STATE]
proof (prove)
using this:
v \<in> vars_clause C

goal (1 subgoal):
 1. (\<And>L. \<lbrakk>L \<in># C; v \<in> vars_lit L\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding vars_clause_def
[PROOF STATE]
proof (prove)
using this:
v \<in> \<Union> (set_mset (image_mset vars_lit C))

goal (1 subgoal):
 1. (\<And>L. \<lbrakk>L \<in># C; v \<in> vars_lit L\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L \<in># C
v \<in> vars_lit L

goal (1 subgoal):
 1. is_ground_atm (\<sigma> v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
L \<in># C
v \<in> vars_lit L
[PROOF STEP]
have "is_ground_lit (subst_lit L \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
L \<in># C
v \<in> vars_lit L

goal (1 subgoal):
 1. is_ground_lit (subst_lit L \<sigma>)
[PROOF STEP]
using ground_clause
[PROOF STATE]
proof (prove)
using this:
L \<in># C
v \<in> vars_lit L
is_ground_cls (subst_cls C \<sigma>)

goal (1 subgoal):
 1. is_ground_lit (subst_lit L \<sigma>)
[PROOF STEP]
unfolding is_ground_cls_def subst_cls_def
[PROOF STATE]
proof (prove)
using this:
L \<in># C
v \<in> vars_lit L
\<forall>L. L \<in># {#subst_lit A \<sigma>. A \<in># C#} \<longrightarrow> is_ground_lit L

goal (1 subgoal):
 1. is_ground_lit (subst_lit L \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_ground_lit (subst_lit L \<sigma>)

goal (1 subgoal):
 1. is_ground_atm (\<sigma> v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_ground_lit (subst_lit L \<sigma>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_ground_lit (subst_lit L \<sigma>)

goal (1 subgoal):
 1. is_ground_atm (\<sigma> v)
[PROOF STEP]
using L_p is_ground_lit_is_ground_on_var
[PROOF STATE]
proof (prove)
using this:
is_ground_lit (subst_lit L \<sigma>)
L \<in># C
v \<in> vars_lit L
\<lbrakk>is_ground_lit (subst_lit ?L ?\<sigma>); ?v \<in> vars_lit ?L\<rbrakk> \<Longrightarrow> is_ground_atm (?\<sigma> ?v)

goal (1 subgoal):
 1. is_ground_atm (\<sigma> v)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
is_ground_atm (\<sigma> v)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_ground_cls_list_is_ground_on_var:
  assumes ground_list: "is_ground_cls_list (subst_cls_list Cs \<sigma>)"
    and v_in_Cs: "v \<in> vars_clause_list Cs"
  shows "is_ground_atm (\<sigma> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_ground_atm (\<sigma> v)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_ground_atm (\<sigma> v)
[PROOF STEP]
from v_in_Cs
[PROOF STATE]
proof (chain)
picking this:
v \<in> vars_clause_list Cs
[PROOF STEP]
obtain C where C_p: "C \<in> set Cs" "v \<in> vars_clause C"
[PROOF STATE]
proof (prove)
using this:
v \<in> vars_clause_list Cs

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>C \<in> set Cs; v \<in> vars_clause C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding vars_clause_list_def
[PROOF STATE]
proof (prove)
using this:
v \<in> \<Union> (vars_clause ` set Cs)

goal (1 subgoal):
 1. (\<And>C. \<lbrakk>C \<in> set Cs; v \<in> vars_clause C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C \<in> set Cs
v \<in> vars_clause C

goal (1 subgoal):
 1. is_ground_atm (\<sigma> v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C \<in> set Cs
v \<in> vars_clause C
[PROOF STEP]
have "is_ground_cls (subst_cls C \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
C \<in> set Cs
v \<in> vars_clause C

goal (1 subgoal):
 1. is_ground_cls (subst_cls C \<sigma>)
[PROOF STEP]
using ground_list
[PROOF STATE]
proof (prove)
using this:
C \<in> set Cs
v \<in> vars_clause C
is_ground_cls_list (subst_cls_list Cs \<sigma>)

goal (1 subgoal):
 1. is_ground_cls (subst_cls C \<sigma>)
[PROOF STEP]
unfolding is_ground_cls_list_def subst_cls_list_def
[PROOF STATE]
proof (prove)
using this:
C \<in> set Cs
v \<in> vars_clause C
Ball (set (map (\<lambda>A. subst_cls A \<sigma>) Cs)) is_ground_cls

goal (1 subgoal):
 1. is_ground_cls (subst_cls C \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_ground_cls (subst_cls C \<sigma>)

goal (1 subgoal):
 1. is_ground_atm (\<sigma> v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_ground_cls (subst_cls C \<sigma>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_ground_cls (subst_cls C \<sigma>)

goal (1 subgoal):
 1. is_ground_atm (\<sigma> v)
[PROOF STEP]
using C_p is_ground_cls_is_ground_on_var
[PROOF STATE]
proof (prove)
using this:
is_ground_cls (subst_cls C \<sigma>)
C \<in> set Cs
v \<in> vars_clause C
\<lbrakk>is_ground_cls (subst_cls ?C ?\<sigma>); ?v \<in> vars_clause ?C\<rbrakk> \<Longrightarrow> is_ground_atm (?\<sigma> ?v)

goal (1 subgoal):
 1. is_ground_atm (\<sigma> v)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
is_ground_atm (\<sigma> v)

goal:
No subgoals!
[PROOF STEP]
qed