[STATEMENT]
lemma unitary_gen_inv:
  assumes "unitary_gen M"
  shows "unitary_gen (mat_inv M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unitary_gen (mat_inv M)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. unitary_gen (mat_inv M)
[PROOF STEP]
obtain k M' where "0 < k" "unitary M'" "M = cor k *\<^sub>s\<^sub>m eye *\<^sub>m\<^sub>m M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k M'. \<lbrakk>0 < k; unitary M'; M = cor k *\<^sub>s\<^sub>m eye *\<^sub>m\<^sub>m M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using unitary_gen_unitary[of M] assms
[PROOF STATE]
proof (prove)
using this:
unitary_gen M = (\<exists>k M'. 0 < k \<and> unitary M' \<and> M = cor k *\<^sub>s\<^sub>m eye *\<^sub>m\<^sub>m M')
unitary_gen M

goal (1 subgoal):
 1. (\<And>k M'. \<lbrakk>0 < k; unitary M'; M = cor k *\<^sub>s\<^sub>m eye *\<^sub>m\<^sub>m M'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 < k
unitary M'
M = cor k *\<^sub>s\<^sub>m eye *\<^sub>m\<^sub>m M'

goal (1 subgoal):
 1. unitary_gen (mat_inv M)
[PROOF STEP]
hence "mat_inv M = cor (1/k) *\<^sub>s\<^sub>m mat_inv M'"
[PROOF STATE]
proof (prove)
using this:
0 < k
unitary M'
M = cor k *\<^sub>s\<^sub>m eye *\<^sub>m\<^sub>m M'

goal (1 subgoal):
 1. mat_inv M = cor (1 / k) *\<^sub>s\<^sub>m mat_inv M'
[PROOF STEP]
by (metis mat_inv_mult_sm mult_sm_eye_mm norm_not_less_zero of_real_1 of_real_divide of_real_eq_0_iff sgn_1_neg sgn_greater sgn_if sgn_pos sgn_sgn)
[PROOF STATE]
proof (state)
this:
mat_inv M = cor (1 / k) *\<^sub>s\<^sub>m mat_inv M'

goal (1 subgoal):
 1. unitary_gen (mat_inv M)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
mat_inv M = cor (1 / k) *\<^sub>s\<^sub>m mat_inv M'

goal (1 subgoal):
 1. unitary_gen (mat_inv M)
[PROOF STEP]
using \<open>k > 0\<close> \<open>unitary M'\<close>
[PROOF STATE]
proof (prove)
using this:
mat_inv M = cor (1 / k) *\<^sub>s\<^sub>m mat_inv M'
0 < k
unitary M'

goal (1 subgoal):
 1. unitary_gen (mat_inv M)
[PROOF STEP]
by (subst unitary_gen_unitary[of "mat_inv M"]) (rule_tac x="1/k" in exI, rule_tac x="mat_inv M'" in exI, metis divide_pos_pos mult_sm_eye_mm unitary_inv zero_less_one)
[PROOF STATE]
proof (state)
this:
unitary_gen (mat_inv M)

goal:
No subgoals!
[PROOF STEP]
qed