[STATEMENT]
lemma err_semilat_Product_esl:
  "\<And>L\<^sub>1 L\<^sub>2. \<lbrakk> err_semilat L\<^sub>1; err_semilat L\<^sub>2 \<rbrakk> \<Longrightarrow> err_semilat(Product.esl L\<^sub>1 L\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>L\<^sub>1 L\<^sub>2. \<lbrakk>err_semilat L\<^sub>1; err_semilat L\<^sub>2\<rbrakk> \<Longrightarrow> err_semilat (Product.esl L\<^sub>1 L\<^sub>2)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>L\<^sub>1 L\<^sub>2. \<lbrakk>err_semilat L\<^sub>1; err_semilat L\<^sub>2\<rbrakk> \<Longrightarrow> err_semilat (Product.esl L\<^sub>1 L\<^sub>2)
[PROOF STEP]
apply (unfold esl_def Err.sl_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>L\<^sub>1 L\<^sub>2. \<lbrakk>semilat (case L\<^sub>1 of (A, r, f) \<Rightarrow> (err A, Err.le r, lift2 f)); semilat (case L\<^sub>2 of (A, r, f) \<Rightarrow> (err A, Err.le r, lift2 f))\<rbrakk> \<Longrightarrow> semilat (case (case L\<^sub>1 of (A, r\<^sub>A, f\<^sub>A) \<Rightarrow> \<lambda>(B, r\<^sub>B, f\<^sub>B). (A \<times> B, Product.le r\<^sub>A r\<^sub>B, Product.sup f\<^sub>A f\<^sub>B)) L\<^sub>2 of (A, r, f) \<Rightarrow> (err A, Err.le r, lift2 f))
[PROOF STEP]
apply (simp (no_asm_simp) only: split_tupled_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ab ac ba. \<lbrakk>semilat (case (a, aa, b) of (A, r, f) \<Rightarrow> (err A, Err.le r, lift2 f)); semilat (case (ab, ac, ba) of (A, r, f) \<Rightarrow> (err A, Err.le r, lift2 f))\<rbrakk> \<Longrightarrow> semilat (case (case (a, aa, b) of (A, r\<^sub>A, f\<^sub>A) \<Rightarrow> \<lambda>(B, r\<^sub>B, f\<^sub>B). (A \<times> B, Product.le r\<^sub>A r\<^sub>B, Product.sup f\<^sub>A f\<^sub>B)) (ab, ac, ba) of (A, r, f) \<Rightarrow> (err A, Err.le r, lift2 f))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ab ac ba. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba)\<rbrakk> \<Longrightarrow> semilat (err (a \<times> ab), Err.le (Product.le aa ac), lift2 (Product.sup b ba))
[PROOF STEP]
apply (simp (no_asm) only: semilat_Def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ab ac ba. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba)\<rbrakk> \<Longrightarrow> order (Err.le (Product.le aa ac)) (err (a \<times> ab)) \<and> closed (err (a \<times> ab)) (lift2 (Product.sup b ba)) \<and> (\<forall>x\<in>err (a \<times> ab). \<forall>y\<in>err (a \<times> ab). x \<sqsubseteq>\<^bsub>Err.le (Product.le aa ac)\<^esub> x \<squnion>\<^bsub>lift2 (Product.sup b ba)\<^esub> y) \<and> (\<forall>x\<in>err (a \<times> ab). \<forall>y\<in>err (a \<times> ab). y \<sqsubseteq>\<^bsub>Err.le (Product.le aa ac)\<^esub> x \<squnion>\<^bsub>lift2 (Product.sup b ba)\<^esub> y) \<and> (\<forall>x\<in>err (a \<times> ab). \<forall>y\<in>err (a \<times> ab). \<forall>z\<in>err (a \<times> ab). x \<sqsubseteq>\<^bsub>Err.le (Product.le aa ac)\<^esub> z \<and> y \<sqsubseteq>\<^bsub>Err.le (Product.le aa ac)\<^esub> z \<longrightarrow> x \<squnion>\<^bsub>lift2 (Product.sup b ba)\<^esub> y \<sqsubseteq>\<^bsub>Err.le (Product.le aa ac)\<^esub> z)
[PROOF STEP]
apply (simp (no_asm_simp) only: Semilat.closedI [OF Semilat.intro] closed_lift2_sup)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ab ac ba. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba)\<rbrakk> \<Longrightarrow> order (Err.le (Product.le aa ac)) (err (a \<times> ab)) \<and> True \<and> (\<forall>x\<in>err (a \<times> ab). \<forall>y\<in>err (a \<times> ab). x \<sqsubseteq>\<^bsub>Err.le (Product.le aa ac)\<^esub> x \<squnion>\<^bsub>lift2 (Product.sup b ba)\<^esub> y) \<and> (\<forall>x\<in>err (a \<times> ab). \<forall>y\<in>err (a \<times> ab). y \<sqsubseteq>\<^bsub>Err.le (Product.le aa ac)\<^esub> x \<squnion>\<^bsub>lift2 (Product.sup b ba)\<^esub> y) \<and> (\<forall>x\<in>err (a \<times> ab). \<forall>y\<in>err (a \<times> ab). \<forall>z\<in>err (a \<times> ab). x \<sqsubseteq>\<^bsub>Err.le (Product.le aa ac)\<^esub> z \<and> y \<sqsubseteq>\<^bsub>Err.le (Product.le aa ac)\<^esub> z \<longrightarrow> x \<squnion>\<^bsub>lift2 (Product.sup b ba)\<^esub> y \<sqsubseteq>\<^bsub>Err.le (Product.le aa ac)\<^esub> z)
[PROOF STEP]
apply (simp (no_asm) only: unfold_lesub_err Err.le_def unfold_plussub_lift2 sup_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ab ac ba. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba)\<rbrakk> \<Longrightarrow> order (Err.le (Product.le aa ac)) (err (a \<times> ab)) \<and> True \<and> (\<forall>x\<in>err (a \<times> ab). \<forall>y\<in>err (a \<times> ab). case lift2 (\<lambda>(a\<^sub>1, b\<^sub>1) (a\<^sub>2, b\<^sub>2). Err.sup Pair (a\<^sub>1 \<squnion>\<^bsub>b\<^esub> a\<^sub>2) (b\<^sub>1 \<squnion>\<^bsub>ba\<^esub> b\<^sub>2)) x y of Err \<Rightarrow> True | OK y \<Rightarrow> case x of Err \<Rightarrow> False | OK x \<Rightarrow> x <=(aa,ac) y) \<and> (\<forall>x\<in>err (a \<times> ab). \<forall>y\<in>err (a \<times> ab). case lift2 (\<lambda>(a\<^sub>1, b\<^sub>1) (a\<^sub>2, b\<^sub>2). Err.sup Pair (a\<^sub>1 \<squnion>\<^bsub>b\<^esub> a\<^sub>2) (b\<^sub>1 \<squnion>\<^bsub>ba\<^esub> b\<^sub>2)) x y of Err \<Rightarrow> True | OK ya \<Rightarrow> case y of Err \<Rightarrow> False | OK x \<Rightarrow> x <=(aa,ac) ya) \<and> (\<forall>x\<in>err (a \<times> ab). \<forall>y\<in>err (a \<times> ab). \<forall>z\<in>err (a \<times> ab). (case z of Err \<Rightarrow> True | OK y \<Rightarrow> case x of Err \<Rightarrow> False | OK x \<Rightarrow> x <=(aa,ac) y) \<and> (case z of Err \<Rightarrow> True | OK ya \<Rightarrow> case y of Err \<Rightarrow> False | OK x \<Rightarrow> x <=(aa,ac) ya) \<longrightarrow> (case z of Err \<Rightarrow> True | OK ya \<Rightarrow> case lift2 (\<lambda>(a\<^sub>1, b\<^sub>1) (a\<^sub>2, b\<^sub>2). Err.sup Pair (a\<^sub>1 \<squnion>\<^bsub>b\<^esub> a\<^sub>2) (b\<^sub>1 \<squnion>\<^bsub>ba\<^esub> b\<^sub>2)) x y of Err \<Rightarrow> False | OK x \<Rightarrow> x <=(aa,ac) ya))
[PROOF STEP]
apply (auto elim: semilat_le_err_OK1 semilat_le_err_OK2
            simp add: lift2_def  split: err.split)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a aa b ab ac ba. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba)\<rbrakk> \<Longrightarrow> order (Product.le aa ac) (a \<times> ab)
 2. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> ag \<sqsubseteq>\<^bsub>aa\<^esub> af
 3. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> be \<sqsubseteq>\<^bsub>ac\<^esub> bd
[PROOF STEP]
apply(rule order_le_prodI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a aa b ab ac ba. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba)\<rbrakk> \<Longrightarrow> order aa a \<and> order ac ab
 2. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> ag \<sqsubseteq>\<^bsub>aa\<^esub> af
 3. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> be \<sqsubseteq>\<^bsub>ac\<^esub> bd
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a aa b ab ac ba. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba)\<rbrakk> \<Longrightarrow> order aa a
 2. \<And>a aa b ab ac ba. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba)\<rbrakk> \<Longrightarrow> order ac ab
 3. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> ag \<sqsubseteq>\<^bsub>aa\<^esub> af
 4. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> be \<sqsubseteq>\<^bsub>ac\<^esub> bd
[PROOF STEP]
apply (blast dest: Semilat.orderI [OF Semilat.intro])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a aa b ab ac ba. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba)\<rbrakk> \<Longrightarrow> order ac ab
 2. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> ag \<sqsubseteq>\<^bsub>aa\<^esub> af
 3. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> be \<sqsubseteq>\<^bsub>ac\<^esub> bd
[PROOF STEP]
apply (blast dest: Semilat.orderI [OF Semilat.intro])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> ag \<sqsubseteq>\<^bsub>aa\<^esub> af
 2. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> be \<sqsubseteq>\<^bsub>ac\<^esub> bd
[PROOF STEP]
apply (rule OK_le_err_OK [THEN iffD1])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK ag \<sqsubseteq>\<^bsub>Err.le aa\<^esub> OK af
 2. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> be \<sqsubseteq>\<^bsub>ac\<^esub> bd
[PROOF STEP]
apply (erule subst, subst OK_lift2_OK [symmetric], rule Semilat.lub [OF Semilat.intro])
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> semilat (?A310 a aa b ab ac ba ad bb ae bc af bd ag be, Err.le aa, lift2 b)
 2. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK ad \<sqsubseteq>\<^bsub>Err.le aa\<^esub> OK af
 3. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK ae \<sqsubseteq>\<^bsub>Err.le aa\<^esub> OK af
 4. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK ad \<in> ?A310 a aa b ab ac ba ad bb ae bc af bd ag be
 5. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK ae \<in> ?A310 a aa b ab ac ba ad bb ae bc af bd ag be
 6. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK af \<in> ?A310 a aa b ab ac ba ad bb ae bc af bd ag be
 7. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> be \<sqsubseteq>\<^bsub>ac\<^esub> bd
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK ad \<sqsubseteq>\<^bsub>Err.le aa\<^esub> OK af
 2. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK ae \<sqsubseteq>\<^bsub>Err.le aa\<^esub> OK af
 3. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK ad \<in> err a
 4. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK ae \<in> err a
 5. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK af \<in> err a
 6. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> be \<sqsubseteq>\<^bsub>ac\<^esub> bd
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK ae \<sqsubseteq>\<^bsub>Err.le aa\<^esub> OK af
 2. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK ad \<in> err a
 3. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK ae \<in> err a
 4. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK af \<in> err a
 5. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> be \<sqsubseteq>\<^bsub>ac\<^esub> bd
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK ad \<in> err a
 2. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK ae \<in> err a
 3. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK af \<in> err a
 4. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> be \<sqsubseteq>\<^bsub>ac\<^esub> bd
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK ae \<in> err a
 2. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK af \<in> err a
 3. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> be \<sqsubseteq>\<^bsub>ac\<^esub> bd
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK af \<in> err a
 2. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> be \<sqsubseteq>\<^bsub>ac\<^esub> bd
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> be \<sqsubseteq>\<^bsub>ac\<^esub> bd
[PROOF STEP]
apply (rule OK_le_err_OK [THEN iffD1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; bb \<squnion>\<^bsub>ba\<^esub> bc = OK be; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK be \<sqsubseteq>\<^bsub>Err.le ac\<^esub> OK bd
[PROOF STEP]
apply (erule subst, subst OK_lift2_OK [symmetric], rule Semilat.lub [OF Semilat.intro])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> semilat (?A325 a aa b ab ac ba ad bb ae bc af bd ag be, Err.le ac, lift2 ba)
 2. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK bb \<sqsubseteq>\<^bsub>Err.le ac\<^esub> OK bd
 3. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK bc \<sqsubseteq>\<^bsub>Err.le ac\<^esub> OK bd
 4. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK bb \<in> ?A325 a aa b ab ac ba ad bb ae bc af bd ag be
 5. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK bc \<in> ?A325 a aa b ab ac ba ad bb ae bc af bd ag be
 6. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK bd \<in> ?A325 a aa b ab ac ba ad bb ae bc af bd ag be
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK bb \<sqsubseteq>\<^bsub>Err.le ac\<^esub> OK bd
 2. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK bc \<sqsubseteq>\<^bsub>Err.le ac\<^esub> OK bd
 3. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK bb \<in> err ab
 4. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK bc \<in> err ab
 5. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK bd \<in> err ab
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK bc \<sqsubseteq>\<^bsub>Err.le ac\<^esub> OK bd
 2. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK bb \<in> err ab
 3. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK bc \<in> err ab
 4. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK bd \<in> err ab
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK bb \<in> err ab
 2. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK bc \<in> err ab
 3. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK bd \<in> err ab
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK bc \<in> err ab
 2. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK bd \<in> err ab
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ab ac ba ad bb ae bc af bd ag be. \<lbrakk>semilat (err a, Err.le aa, lift2 b); semilat (err ab, Err.le ac, lift2 ba); ae \<in> a; bc \<in> ab; ad \<in> a; bb \<in> ab; ad \<squnion>\<^bsub>b\<^esub> ae = OK ag; af \<in> a; bd \<in> ab; ad \<sqsubseteq>\<^bsub>aa\<^esub> af; bb \<sqsubseteq>\<^bsub>ac\<^esub> bd; ae \<sqsubseteq>\<^bsub>aa\<^esub> af; bc \<sqsubseteq>\<^bsub>ac\<^esub> bd\<rbrakk> \<Longrightarrow> OK bd \<in> err ab
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


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


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


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


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


[STATEMENT]
lemma mult_sv_ex_id1 [simp]:
  shows "\<exists> k::complex. k \<noteq> 0 \<and> k *\<^sub>s\<^sub>v v = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> k *\<^sub>s\<^sub>v v = v
[PROOF STEP]
by (rule_tac x=1 in exI, simp)


[STATEMENT]
lemma mult_sv_ex_id2 [simp]:
  shows "\<exists> k::complex. k \<noteq> 0 \<and> v = k *\<^sub>s\<^sub>v v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> v = k *\<^sub>s\<^sub>v v
[PROOF STEP]
by (rule_tac x=1 in exI, simp)


[STATEMENT]
lemma mult_vv_commute:
  shows "v1 *\<^sub>v\<^sub>v v2 = v2 *\<^sub>v\<^sub>v v1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v1 *\<^sub>v\<^sub>v v2 = v2 *\<^sub>v\<^sub>v v1
[PROOF STEP]
by (cases v1, cases v2) auto


[STATEMENT]
lemma mult_vv_scale_sv1:
  shows "(k *\<^sub>s\<^sub>v v1) *\<^sub>v\<^sub>v v2 = k * (v1 *\<^sub>v\<^sub>v v2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k *\<^sub>s\<^sub>v v1 *\<^sub>v\<^sub>v v2 = k * v1 *\<^sub>v\<^sub>v v2
[PROOF STEP]
by (cases v1, cases v2) (auto simp add: field_simps)


[STATEMENT]
lemma mult_vv_scale_sv2:
  shows "v1 *\<^sub>v\<^sub>v (k *\<^sub>s\<^sub>v v2) = k * (v1 *\<^sub>v\<^sub>v v2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v1 *\<^sub>v\<^sub>v (k *\<^sub>s\<^sub>v v2) = k * v1 *\<^sub>v\<^sub>v v2
[PROOF STEP]
by (cases v1, cases v2) (auto simp add: field_simps)


[STATEMENT]
lemma vec_cnj_vec_cnj [simp]:
  shows "vec_cnj (vec_cnj v) = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_cnj (vec_cnj v) = v
[PROOF STEP]
by (cases v) (simp add: vec_cnj_def)


[STATEMENT]
lemma cnj_mult_vv:
  shows "cnj (v1 *\<^sub>v\<^sub>v v2) = (vec_cnj v1) *\<^sub>v\<^sub>v (vec_cnj v2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj (v1 *\<^sub>v\<^sub>v v2) = vec_cnj v1 *\<^sub>v\<^sub>v vec_cnj v2
[PROOF STEP]
by (cases v1, cases v2) (simp add: vec_cnj_def)


[STATEMENT]
lemma vec_cnj_sv [simp]:
  shows "vec_cnj (k *\<^sub>s\<^sub>v A) = cnj k *\<^sub>s\<^sub>v vec_cnj A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_cnj (k *\<^sub>s\<^sub>v A) = cnj k *\<^sub>s\<^sub>v vec_cnj A
[PROOF STEP]
by (cases A) (auto simp add: vec_cnj_def)


[STATEMENT]
lemma scalsquare_vv_zero:
  shows "(vec_cnj v) *\<^sub>v\<^sub>v v = 0 \<longleftrightarrow> v = vec_zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (vec_cnj v *\<^sub>v\<^sub>v v = 0) = (v = vec_zero)
[PROOF STEP]
apply (cases v)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. v = (a, b) \<Longrightarrow> (vec_cnj v *\<^sub>v\<^sub>v v = 0) = (v = vec_zero)
[PROOF STEP]
apply (auto simp add: vec_cnj_def field_simps complex_mult_cnj_cmod power2_eq_square)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>v = (a, b); cor (cmod a) * cor (cmod a) + cor (cmod b) * cor (cmod b) = 0\<rbrakk> \<Longrightarrow> a = 0
 2. \<And>a b. \<lbrakk>v = (a, b); cor (cmod a) * cor (cmod a) + cor (cmod b) * cor (cmod b) = 0\<rbrakk> \<Longrightarrow> b = 0
[PROOF STEP]
apply (metis (no_types) norm_eq_zero of_real_0 of_real_add of_real_eq_iff of_real_mult sum_squares_eq_zero_iff)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mult_sm_distribution [simp]:
  shows "k1 *\<^sub>s\<^sub>m (k2 *\<^sub>s\<^sub>m A) = (k1*k2) *\<^sub>s\<^sub>m A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k1 *\<^sub>s\<^sub>m (k2 *\<^sub>s\<^sub>m A) = (k1 * k2) *\<^sub>s\<^sub>m A
[PROOF STEP]
by (cases A) auto


[STATEMENT]
lemma mult_sm_neutral [simp]:
  shows "1 *\<^sub>s\<^sub>m A = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 *\<^sub>s\<^sub>m A = A
[PROOF STEP]
by (cases A) auto


[STATEMENT]
lemma mult_sm_inv_l:
  assumes "k \<noteq> 0" and "k *\<^sub>s\<^sub>m A = B"
  shows "A = (1/k) *\<^sub>s\<^sub>m B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = (1 / k) *\<^sub>s\<^sub>m B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0
k *\<^sub>s\<^sub>m A = B

goal (1 subgoal):
 1. A = (1 / k) *\<^sub>s\<^sub>m B
[PROOF STEP]
by auto


[STATEMENT]
lemma mult_sm_ex_id1 [simp]:
  shows "\<exists> k::complex. k \<noteq> 0 \<and> k *\<^sub>s\<^sub>m M = M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> k *\<^sub>s\<^sub>m M = M
[PROOF STEP]
by (rule_tac x=1 in exI, simp)


[STATEMENT]
lemma mult_sm_ex_id2 [simp]:
  shows "\<exists> k::complex. k \<noteq> 0 \<and> M = k *\<^sub>s\<^sub>m M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. k \<noteq> 0 \<and> M = k *\<^sub>s\<^sub>m M
[PROOF STEP]
by (rule_tac x=1 in exI, simp)


[STATEMENT]
lemma nonzero_mult_real:
  assumes "A \<noteq> mat_zero" and "k \<noteq> 0"
  shows "k *\<^sub>s\<^sub>m A \<noteq> mat_zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k *\<^sub>s\<^sub>m A \<noteq> mat_zero
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<noteq> mat_zero
k \<noteq> 0

goal (1 subgoal):
 1. k *\<^sub>s\<^sub>m A \<noteq> mat_zero
[PROOF STEP]
by (cases A) simp


[STATEMENT]
lemma mult_mm_assoc:
  shows "A *\<^sub>m\<^sub>m (B *\<^sub>m\<^sub>m C) = (A *\<^sub>m\<^sub>m B) *\<^sub>m\<^sub>m C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>m\<^sub>m (B *\<^sub>m\<^sub>m C) = A *\<^sub>m\<^sub>m B *\<^sub>m\<^sub>m C
[PROOF STEP]
by (cases A, cases B, cases C) (auto simp add: field_simps)


[STATEMENT]
lemma mult_assoc_5:
  shows "A *\<^sub>m\<^sub>m (B *\<^sub>m\<^sub>m C *\<^sub>m\<^sub>m D) *\<^sub>m\<^sub>m E = (A *\<^sub>m\<^sub>m B) *\<^sub>m\<^sub>m C *\<^sub>m\<^sub>m (D *\<^sub>m\<^sub>m E)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>m\<^sub>m (B *\<^sub>m\<^sub>m C *\<^sub>m\<^sub>m D) *\<^sub>m\<^sub>m E = A *\<^sub>m\<^sub>m B *\<^sub>m\<^sub>m C *\<^sub>m\<^sub>m (D *\<^sub>m\<^sub>m E)
[PROOF STEP]
by (simp only: mult_mm_assoc)


[STATEMENT]
lemma mat_zero_r [simp]:
  shows "A *\<^sub>m\<^sub>m mat_zero = mat_zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>m\<^sub>m mat_zero = mat_zero
[PROOF STEP]
by (cases A) simp


[STATEMENT]
lemma mat_zero_l [simp]:
  shows "mat_zero *\<^sub>m\<^sub>m A = mat_zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_zero *\<^sub>m\<^sub>m A = mat_zero
[PROOF STEP]
by (cases A) simp


[STATEMENT]
lemma mat_eye_l:
  shows "eye *\<^sub>m\<^sub>m A = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eye *\<^sub>m\<^sub>m A = A
[PROOF STEP]
by (cases A) auto


[STATEMENT]
lemma mat_eye_r:
  shows "A *\<^sub>m\<^sub>m eye = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>m\<^sub>m eye = A
[PROOF STEP]
by (cases A) auto


[STATEMENT]
lemma mult_mm_sm [simp]:
  shows "A *\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m B) = k *\<^sub>s\<^sub>m (A *\<^sub>m\<^sub>m B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m B) = k *\<^sub>s\<^sub>m (A *\<^sub>m\<^sub>m B)
[PROOF STEP]
by (cases A, cases B) (simp add: field_simps)


[STATEMENT]
lemma mult_sm_mm [simp]:
  shows "(k *\<^sub>s\<^sub>m A) *\<^sub>m\<^sub>m B = k *\<^sub>s\<^sub>m (A *\<^sub>m\<^sub>m B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k *\<^sub>s\<^sub>m A *\<^sub>m\<^sub>m B = k *\<^sub>s\<^sub>m (A *\<^sub>m\<^sub>m B)
[PROOF STEP]
by (cases A, cases B) (simp add: field_simps)


[STATEMENT]
lemma mult_sm_eye_mm [simp]:
  shows "k *\<^sub>s\<^sub>m eye *\<^sub>m\<^sub>m A = k *\<^sub>s\<^sub>m A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k *\<^sub>s\<^sub>m eye *\<^sub>m\<^sub>m A = k *\<^sub>s\<^sub>m A
[PROOF STEP]
by (cases A) simp


[STATEMENT]
lemma mat_det_mult [simp]:
  shows "mat_det (A *\<^sub>m\<^sub>m B) = mat_det A * mat_det B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_det (A *\<^sub>m\<^sub>m B) = mat_det A * mat_det B
[PROOF STEP]
by (cases A, cases B) (auto simp add: field_simps)


[STATEMENT]
lemma mat_det_mult_sm [simp]:
  shows "mat_det (k *\<^sub>s\<^sub>m A) = (k*k) * mat_det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_det (k *\<^sub>s\<^sub>m A) = k * k * mat_det A
[PROOF STEP]
by (cases A) (auto simp add: field_simps)


[STATEMENT]
lemma mat_inv_r:
  assumes "mat_det A \<noteq> 0"
  shows "A *\<^sub>m\<^sub>m (mat_inv A) = eye"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>m\<^sub>m mat_inv A = eye
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mat_det A \<noteq> 0

goal (1 subgoal):
 1. A *\<^sub>m\<^sub>m mat_inv A = eye
[PROOF STEP]
proof (cases A, auto simp add: field_simps)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c d. \<lbrakk>a * d \<noteq> b * c; A = (a, b, c, d); a * (a * (d * d)) + b * (b * (c * c)) = a * (b * (c * (d * 2)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix a b c d :: complex
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c d. \<lbrakk>a * d \<noteq> b * c; A = (a, b, c, d); a * (a * (d * d)) + b * (b * (c * c)) = a * (b * (c * (d * 2)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "a * (a * (d * d)) + b * (b * (c * c)) = a * (b * (c * (d * 2)))"
[PROOF STATE]
proof (state)
this:
a * (a * (d * d)) + b * (b * (c * c)) = a * (b * (c * (d * 2)))

goal (1 subgoal):
 1. \<And>a b c d. \<lbrakk>a * d \<noteq> b * c; A = (a, b, c, d); a * (a * (d * d)) + b * (b * (c * c)) = a * (b * (c * (d * 2)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "(a*d - b*c)*(a*d - b*c) = 0"
[PROOF STATE]
proof (prove)
using this:
a * (a * (d * d)) + b * (b * (c * c)) = a * (b * (c * (d * 2)))

goal (1 subgoal):
 1. (a * d - b * c) * (a * d - b * c) = 0
[PROOF STEP]
by (auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
(a * d - b * c) * (a * d - b * c) = 0

goal (1 subgoal):
 1. \<And>a b c d. \<lbrakk>a * d \<noteq> b * c; A = (a, b, c, d); a * (a * (d * d)) + b * (b * (c * c)) = a * (b * (c * (d * 2)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence *: "a*d - b*c = 0"
[PROOF STATE]
proof (prove)
using this:
(a * d - b * c) * (a * d - b * c) = 0

goal (1 subgoal):
 1. a * d - b * c = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a * d - b * c = 0

goal (1 subgoal):
 1. \<And>a b c d. \<lbrakk>a * d \<noteq> b * c; A = (a, b, c, d); a * (a * (d * d)) + b * (b * (c * c)) = a * (b * (c * (d * 2)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "a*d \<noteq> b*c"
[PROOF STATE]
proof (state)
this:
a * d \<noteq> b * c

goal (1 subgoal):
 1. \<And>a b c d. \<lbrakk>a * d \<noteq> b * c; A = (a, b, c, d); a * (a * (d * d)) + b * (b * (c * c)) = a * (b * (c * (d * 2)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
a * d - b * c = 0
a * d \<noteq> b * c
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
a * d - b * c = 0
a * d \<noteq> b * c

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mat_inv_l:
  assumes "mat_det A \<noteq> 0"
  shows "(mat_inv A) *\<^sub>m\<^sub>m A  = eye"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_inv A *\<^sub>m\<^sub>m A = eye
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mat_det A \<noteq> 0

goal (1 subgoal):
 1. mat_inv A *\<^sub>m\<^sub>m A = eye
[PROOF STEP]
proof (cases A, auto simp add: field_simps)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c d. \<lbrakk>a * d \<noteq> b * c; A = (a, b, c, d); a * (a * (d * d)) + b * (b * (c * c)) = a * (b * (c * (d * 2)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix a b c d :: complex
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c d. \<lbrakk>a * d \<noteq> b * c; A = (a, b, c, d); a * (a * (d * d)) + b * (b * (c * c)) = a * (b * (c * (d * 2)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "a * (a * (d * d)) + b * (b * (c * c)) = a * (b * (c * (d * 2)))"
[PROOF STATE]
proof (state)
this:
a * (a * (d * d)) + b * (b * (c * c)) = a * (b * (c * (d * 2)))

goal (1 subgoal):
 1. \<And>a b c d. \<lbrakk>a * d \<noteq> b * c; A = (a, b, c, d); a * (a * (d * d)) + b * (b * (c * c)) = a * (b * (c * (d * 2)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "(a*d - b*c)*(a*d - b*c) = 0"
[PROOF STATE]
proof (prove)
using this:
a * (a * (d * d)) + b * (b * (c * c)) = a * (b * (c * (d * 2)))

goal (1 subgoal):
 1. (a * d - b * c) * (a * d - b * c) = 0
[PROOF STEP]
by (auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
(a * d - b * c) * (a * d - b * c) = 0

goal (1 subgoal):
 1. \<And>a b c d. \<lbrakk>a * d \<noteq> b * c; A = (a, b, c, d); a * (a * (d * d)) + b * (b * (c * c)) = a * (b * (c * (d * 2)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence *: "a*d - b*c = 0"
[PROOF STATE]
proof (prove)
using this:
(a * d - b * c) * (a * d - b * c) = 0

goal (1 subgoal):
 1. a * d - b * c = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a * d - b * c = 0

goal (1 subgoal):
 1. \<And>a b c d. \<lbrakk>a * d \<noteq> b * c; A = (a, b, c, d); a * (a * (d * d)) + b * (b * (c * c)) = a * (b * (c * (d * 2)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "a*d \<noteq> b*c"
[PROOF STATE]
proof (state)
this:
a * d \<noteq> b * c

goal (1 subgoal):
 1. \<And>a b c d. \<lbrakk>a * d \<noteq> b * c; A = (a, b, c, d); a * (a * (d * d)) + b * (b * (c * c)) = a * (b * (c * (d * 2)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
a * d - b * c = 0
a * d \<noteq> b * c
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
a * d - b * c = 0
a * d \<noteq> b * c

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mat_det_inv:
  assumes "mat_det A \<noteq> 0"
  shows "mat_det (mat_inv A) = 1 / mat_det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_det (mat_inv A) = 1 / mat_det A
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat_det (mat_inv A) = 1 / mat_det A
[PROOF STEP]
have "mat_det eye = mat_det A * mat_det (mat_inv A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_det eye = mat_det A * mat_det (mat_inv A)
[PROOF STEP]
using mat_inv_l[OF assms, symmetric]
[PROOF STATE]
proof (prove)
using this:
eye = mat_inv A *\<^sub>m\<^sub>m A

goal (1 subgoal):
 1. mat_det eye = mat_det A * mat_det (mat_inv A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mat_det eye = mat_det A * mat_det (mat_inv A)

goal (1 subgoal):
 1. mat_det (mat_inv A) = 1 / mat_det A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
mat_det eye = mat_det A * mat_det (mat_inv A)

goal (1 subgoal):
 1. mat_det (mat_inv A) = 1 / mat_det A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mat_det eye = mat_det A * mat_det (mat_inv A)
mat_det A \<noteq> 0

goal (1 subgoal):
 1. mat_det (mat_inv A) = 1 / mat_det A
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
mat_det (mat_inv A) = 1 / mat_det A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mult_mm_inv_l:
  assumes "mat_det A \<noteq> 0" and "A *\<^sub>m\<^sub>m B = C"
  shows "B = mat_inv A *\<^sub>m\<^sub>m C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B = mat_inv A *\<^sub>m\<^sub>m C
[PROOF STEP]
using assms mat_eye_l[of B]
[PROOF STATE]
proof (prove)
using this:
mat_det A \<noteq> 0
A *\<^sub>m\<^sub>m B = C
eye *\<^sub>m\<^sub>m B = B

goal (1 subgoal):
 1. B = mat_inv A *\<^sub>m\<^sub>m C
[PROOF STEP]
by (auto simp add: mult_mm_assoc mat_inv_l)


[STATEMENT]
lemma mult_mm_inv_r:
  assumes "mat_det B \<noteq> 0" and "A *\<^sub>m\<^sub>m B = C"
  shows "A = C *\<^sub>m\<^sub>m mat_inv B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = C *\<^sub>m\<^sub>m mat_inv B
[PROOF STEP]
using assms mat_eye_r[of A]
[PROOF STATE]
proof (prove)
using this:
mat_det B \<noteq> 0
A *\<^sub>m\<^sub>m B = C
A *\<^sub>m\<^sub>m eye = A

goal (1 subgoal):
 1. A = C *\<^sub>m\<^sub>m mat_inv B
[PROOF STEP]
by (auto simp add: mult_mm_assoc[symmetric] mat_inv_r)


[STATEMENT]
lemma mult_mm_non_zero_l:
  assumes "mat_det A \<noteq> 0" and "B \<noteq> mat_zero"
  shows "A *\<^sub>m\<^sub>m B \<noteq> mat_zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>m\<^sub>m B \<noteq> mat_zero
[PROOF STEP]
using assms mat_zero_r
[PROOF STATE]
proof (prove)
using this:
mat_det A \<noteq> 0
B \<noteq> mat_zero
?A *\<^sub>m\<^sub>m mat_zero = mat_zero

goal (1 subgoal):
 1. A *\<^sub>m\<^sub>m B \<noteq> mat_zero
[PROOF STEP]
using mult_mm_inv_l[OF assms(1), of B mat_zero]
[PROOF STATE]
proof (prove)
using this:
mat_det A \<noteq> 0
B \<noteq> mat_zero
?A *\<^sub>m\<^sub>m mat_zero = mat_zero
A *\<^sub>m\<^sub>m B = mat_zero \<Longrightarrow> B = mat_inv A *\<^sub>m\<^sub>m mat_zero

goal (1 subgoal):
 1. A *\<^sub>m\<^sub>m B \<noteq> mat_zero
[PROOF STEP]
by auto


[STATEMENT]
lemma mat_inv_mult_mm:
  assumes "mat_det A \<noteq> 0" and "mat_det B \<noteq> 0"
  shows "mat_inv (A *\<^sub>m\<^sub>m B) = mat_inv B *\<^sub>m\<^sub>m mat_inv A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_inv (A *\<^sub>m\<^sub>m B) = mat_inv B *\<^sub>m\<^sub>m mat_inv A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mat_det A \<noteq> 0
mat_det B \<noteq> 0

goal (1 subgoal):
 1. mat_inv (A *\<^sub>m\<^sub>m B) = mat_inv B *\<^sub>m\<^sub>m mat_inv A
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>mat_det A \<noteq> 0; mat_det B \<noteq> 0\<rbrakk> \<Longrightarrow> mat_inv (A *\<^sub>m\<^sub>m B) = mat_inv B *\<^sub>m\<^sub>m mat_inv A
[PROOF STEP]
have "(A *\<^sub>m\<^sub>m B) *\<^sub>m\<^sub>m (mat_inv B *\<^sub>m\<^sub>m mat_inv A) = eye"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>m\<^sub>m B *\<^sub>m\<^sub>m (mat_inv B *\<^sub>m\<^sub>m mat_inv A) = eye
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mat_det A \<noteq> 0
mat_det B \<noteq> 0

goal (1 subgoal):
 1. A *\<^sub>m\<^sub>m B *\<^sub>m\<^sub>m (mat_inv B *\<^sub>m\<^sub>m mat_inv A) = eye
[PROOF STEP]
by (metis mat_inv_r mult_mm_assoc mult_mm_inv_r)
[PROOF STATE]
proof (state)
this:
A *\<^sub>m\<^sub>m B *\<^sub>m\<^sub>m (mat_inv B *\<^sub>m\<^sub>m mat_inv A) = eye

goal (1 subgoal):
 1. \<lbrakk>mat_det A \<noteq> 0; mat_det B \<noteq> 0\<rbrakk> \<Longrightarrow> mat_inv (A *\<^sub>m\<^sub>m B) = mat_inv B *\<^sub>m\<^sub>m mat_inv A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A *\<^sub>m\<^sub>m B *\<^sub>m\<^sub>m (mat_inv B *\<^sub>m\<^sub>m mat_inv A) = eye

goal (1 subgoal):
 1. mat_inv (A *\<^sub>m\<^sub>m B) = mat_inv B *\<^sub>m\<^sub>m mat_inv A
[PROOF STEP]
using mult_mm_inv_l[of "A *\<^sub>m\<^sub>m B" "mat_inv B *\<^sub>m\<^sub>m mat_inv A" eye] assms mat_eye_r
[PROOF STATE]
proof (prove)
using this:
A *\<^sub>m\<^sub>m B *\<^sub>m\<^sub>m (mat_inv B *\<^sub>m\<^sub>m mat_inv A) = eye
\<lbrakk>mat_det (A *\<^sub>m\<^sub>m B) \<noteq> 0; A *\<^sub>m\<^sub>m B *\<^sub>m\<^sub>m (mat_inv B *\<^sub>m\<^sub>m mat_inv A) = eye\<rbrakk> \<Longrightarrow> mat_inv B *\<^sub>m\<^sub>m mat_inv A = mat_inv (A *\<^sub>m\<^sub>m B) *\<^sub>m\<^sub>m eye
mat_det A \<noteq> 0
mat_det B \<noteq> 0
?A *\<^sub>m\<^sub>m eye = ?A

goal (1 subgoal):
 1. mat_inv (A *\<^sub>m\<^sub>m B) = mat_inv B *\<^sub>m\<^sub>m mat_inv A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mat_inv (A *\<^sub>m\<^sub>m B) = mat_inv B *\<^sub>m\<^sub>m mat_inv A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mult_mm_cancel_l:
  assumes "mat_det M \<noteq> 0"  "M *\<^sub>m\<^sub>m A = M *\<^sub>m\<^sub>m B"
  shows "A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mat_det M \<noteq> 0
M *\<^sub>m\<^sub>m A = M *\<^sub>m\<^sub>m B

goal (1 subgoal):
 1. A = B
[PROOF STEP]
by (metis mult_mm_inv_l)


[STATEMENT]
lemma mult_mm_cancel_r:
  assumes "mat_det M \<noteq> 0"  "A *\<^sub>m\<^sub>m M = B *\<^sub>m\<^sub>m M"
  shows "A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mat_det M \<noteq> 0
A *\<^sub>m\<^sub>m M = B *\<^sub>m\<^sub>m M

goal (1 subgoal):
 1. A = B
[PROOF STEP]
by (metis mult_mm_inv_r)


[STATEMENT]
lemma mult_mm_non_zero_r:
  assumes "A \<noteq> mat_zero" and "mat_det B \<noteq> 0"
  shows "A *\<^sub>m\<^sub>m B \<noteq> mat_zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>m\<^sub>m B \<noteq> mat_zero
[PROOF STEP]
using assms mat_zero_l
[PROOF STATE]
proof (prove)
using this:
A \<noteq> mat_zero
mat_det B \<noteq> 0
mat_zero *\<^sub>m\<^sub>m ?A = mat_zero

goal (1 subgoal):
 1. A *\<^sub>m\<^sub>m B \<noteq> mat_zero
[PROOF STEP]
using mult_mm_inv_r[OF assms(2), of A mat_zero]
[PROOF STATE]
proof (prove)
using this:
A \<noteq> mat_zero
mat_det B \<noteq> 0
mat_zero *\<^sub>m\<^sub>m ?A = mat_zero
A *\<^sub>m\<^sub>m B = mat_zero \<Longrightarrow> A = mat_zero *\<^sub>m\<^sub>m mat_inv B

goal (1 subgoal):
 1. A *\<^sub>m\<^sub>m B \<noteq> mat_zero
[PROOF STEP]
by auto


[STATEMENT]
lemma mat_inv_mult_sm:
  assumes "k \<noteq> 0"
  shows "mat_inv (k *\<^sub>s\<^sub>m A) = (1 / k) *\<^sub>s\<^sub>m mat_inv A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_inv (k *\<^sub>s\<^sub>m A) = (1 / k) *\<^sub>s\<^sub>m mat_inv A
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat_inv (k *\<^sub>s\<^sub>m A) = (1 / k) *\<^sub>s\<^sub>m mat_inv A
[PROOF STEP]
obtain a b c d where "A = (a, b, c, d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b c d. A = (a, b, c, d) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases A) auto
[PROOF STATE]
proof (state)
this:
A = (a, b, c, d)

goal (1 subgoal):
 1. mat_inv (k *\<^sub>s\<^sub>m A) = (1 / k) *\<^sub>s\<^sub>m mat_inv A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A = (a, b, c, d)

goal (1 subgoal):
 1. mat_inv (k *\<^sub>s\<^sub>m A) = (1 / k) *\<^sub>s\<^sub>m mat_inv A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A = (a, b, c, d)
k \<noteq> 0

goal (1 subgoal):
 1. mat_inv (k *\<^sub>s\<^sub>m A) = (1 / k) *\<^sub>s\<^sub>m mat_inv A
[PROOF STEP]
by auto (subst mult.assoc[of k a "k*d"], subst mult.assoc[of k b "k*c"], subst right_diff_distrib[of k "a*(k*d)" "b*(k*c)", symmetric], simp, simp add: field_simps)+
[PROOF STATE]
proof (state)
this:
mat_inv (k *\<^sub>s\<^sub>m A) = (1 / k) *\<^sub>s\<^sub>m mat_inv A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mat_inv_inv [simp]:
  assumes "mat_det M \<noteq> 0"
  shows "mat_inv (mat_inv M) = M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_inv (mat_inv M) = M
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat_inv (mat_inv M) = M
[PROOF STEP]
have "mat_inv M *\<^sub>m\<^sub>m M = eye"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_inv M *\<^sub>m\<^sub>m M = eye
[PROOF STEP]
using mat_inv_l[OF assms]
[PROOF STATE]
proof (prove)
using this:
mat_inv M *\<^sub>m\<^sub>m M = eye

goal (1 subgoal):
 1. mat_inv M *\<^sub>m\<^sub>m M = eye
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mat_inv M *\<^sub>m\<^sub>m M = eye

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

goal (1 subgoal):
 1. mat_inv (mat_inv M) = M
[PROOF STEP]
using assms mat_det_inv[of M]
[PROOF STATE]
proof (prove)
using this:
mat_inv M *\<^sub>m\<^sub>m M = eye
mat_det M \<noteq> 0
mat_det M \<noteq> 0 \<Longrightarrow> mat_det (mat_inv M) = 1 / mat_det M

goal (1 subgoal):
 1. mat_inv (mat_inv M) = M
[PROOF STEP]
using mult_mm_inv_l[of "mat_inv M" M eye] mat_eye_r
[PROOF STATE]
proof (prove)
using this:
mat_inv M *\<^sub>m\<^sub>m M = eye
mat_det M \<noteq> 0
mat_det M \<noteq> 0 \<Longrightarrow> mat_det (mat_inv M) = 1 / mat_det M
\<lbrakk>mat_det (mat_inv M) \<noteq> 0; mat_inv M *\<^sub>m\<^sub>m M = eye\<rbrakk> \<Longrightarrow> M = mat_inv (mat_inv M) *\<^sub>m\<^sub>m eye
?A *\<^sub>m\<^sub>m eye = ?A

goal (1 subgoal):
 1. mat_inv (mat_inv M) = M
[PROOF STEP]
by (auto simp del: eye_def)
[PROOF STATE]
proof (state)
this:
mat_inv (mat_inv M) = M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mat_t_mat_t [simp]:
  shows "mat_transpose (mat_transpose A) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_transpose (mat_transpose A) = A
[PROOF STEP]
by (cases A) auto


[STATEMENT]
lemma mat_t_mult_sm [simp]:
  shows "mat_transpose (k *\<^sub>s\<^sub>m A) = k *\<^sub>s\<^sub>m (mat_transpose A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_transpose (k *\<^sub>s\<^sub>m A) = k *\<^sub>s\<^sub>m mat_transpose A
[PROOF STEP]
by (cases A) simp


[STATEMENT]
lemma mat_inv_transpose:
  shows "mat_transpose (mat_inv M) = mat_inv (mat_transpose M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_transpose (mat_inv M) = mat_inv (mat_transpose M)
[PROOF STEP]
by (cases M) auto


[STATEMENT]
lemma mat_det_transpose [simp]:
  fixes M :: "complex_mat"
  shows "mat_det (mat_transpose M) = mat_det M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_det (mat_transpose M) = mat_det M
[PROOF STEP]
by (cases M) auto


[STATEMENT]
lemma mat_cnj_cnj [simp]:
  shows "mat_cnj (mat_cnj A) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_cnj (mat_cnj A) = A
[PROOF STEP]
unfolding mat_cnj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_map cnj (mat_map cnj A) = A
[PROOF STEP]
by (cases A) auto


[STATEMENT]
lemma mat_cnj_sm [simp]:
  shows "mat_cnj (k *\<^sub>s\<^sub>m A) = cnj k *\<^sub>s\<^sub>m (mat_cnj A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_cnj (k *\<^sub>s\<^sub>m A) = cnj k *\<^sub>s\<^sub>m mat_cnj A
[PROOF STEP]
by (cases A) (simp add: mat_cnj_def)


[STATEMENT]
lemma mat_det_cnj [simp]:
  shows "mat_det (mat_cnj A) = cnj (mat_det A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_det (mat_cnj A) = cnj (mat_det A)
[PROOF STEP]
by (cases A) (simp add: mat_cnj_def)


[STATEMENT]
lemma nonzero_mat_cnj:
  shows "mat_cnj A = mat_zero \<longleftrightarrow> A = mat_zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mat_cnj A = mat_zero) = (A = mat_zero)
[PROOF STEP]
by (cases A) (auto simp add: mat_cnj_def)


[STATEMENT]
lemma mat_inv_cnj:
  shows "mat_cnj (mat_inv M) = mat_inv (mat_cnj M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_cnj (mat_inv M) = mat_inv (mat_cnj M)
[PROOF STEP]
unfolding mat_cnj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_map cnj (mat_inv M) = mat_inv (mat_map cnj M)
[PROOF STEP]
by (cases M) auto


[STATEMENT]
lemma mat_adj_mult_mm [simp]:
  shows "mat_adj (A *\<^sub>m\<^sub>m B) = mat_adj B *\<^sub>m\<^sub>m mat_adj A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_adj (A *\<^sub>m\<^sub>m B) = mat_adj B *\<^sub>m\<^sub>m mat_adj A
[PROOF STEP]
by (cases A, cases B) (auto simp add: mat_adj_def mat_cnj_def)


[STATEMENT]
lemma mat_adj_mult_sm [simp]:
  shows "mat_adj (k *\<^sub>s\<^sub>m A) = cnj k *\<^sub>s\<^sub>m mat_adj A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_adj (k *\<^sub>s\<^sub>m A) = cnj k *\<^sub>s\<^sub>m mat_adj A
[PROOF STEP]
by (cases A) (auto simp add: mat_adj_def mat_cnj_def)


[STATEMENT]
lemma mat_det_adj:
  shows "mat_det (mat_adj A) = cnj (mat_det A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_det (mat_adj A) = cnj (mat_det A)
[PROOF STEP]
by (cases A) (auto simp add: mat_adj_def mat_cnj_def)


[STATEMENT]
lemma mat_adj_inv:
  assumes "mat_det M \<noteq> 0"
  shows "mat_adj (mat_inv M) = mat_inv (mat_adj M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_adj (mat_inv M) = mat_inv (mat_adj M)
[PROOF STEP]
by (cases M) (auto simp add: mat_adj_def mat_cnj_def)


[STATEMENT]
lemma mat_transpose_mat_cnj:
  shows "mat_transpose (mat_cnj A) = mat_adj A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_transpose (mat_cnj A) = mat_adj A
[PROOF STEP]
by (cases A)  (auto simp add: mat_adj_def mat_cnj_def)


[STATEMENT]
lemma mat_adj_adj [simp]:
  shows "mat_adj (mat_adj A) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_adj (mat_adj A) = A
[PROOF STEP]
unfolding mat_adj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_cnj (mat_transpose (mat_cnj (mat_transpose A))) = A
[PROOF STEP]
by (subst mat_transpose_mat_cnj) (simp add: mat_adj_def)


[STATEMENT]
lemma mat_adj_eye [simp]:
  shows "mat_adj eye = eye"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_adj eye = eye
[PROOF STEP]
by (auto simp add: mat_adj_def mat_cnj_def)


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


[STATEMENT]
lemma mult_mv_mv [simp]:
  shows "B *\<^sub>m\<^sub>v (A *\<^sub>m\<^sub>v v) = (B *\<^sub>m\<^sub>m A) *\<^sub>m\<^sub>v v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B *\<^sub>m\<^sub>v (A *\<^sub>m\<^sub>v v) = B *\<^sub>m\<^sub>m A *\<^sub>m\<^sub>v v
[PROOF STEP]
by (cases v, cases A, cases B) (auto simp add: field_simps)


[STATEMENT]
lemma mult_mv_inv:
  assumes "x =  A *\<^sub>m\<^sub>v y" and "mat_det A \<noteq> 0"
  shows "y = (mat_inv A) *\<^sub>m\<^sub>v x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y = mat_inv A *\<^sub>m\<^sub>v x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x = A *\<^sub>m\<^sub>v y
mat_det A \<noteq> 0

goal (1 subgoal):
 1. y = mat_inv A *\<^sub>m\<^sub>v x
[PROOF STEP]
by (cases y) (simp add: mat_inv_l)


[STATEMENT]
lemma mult_vm_inv:
  assumes "x =  y *\<^sub>v\<^sub>m A" and "mat_det A \<noteq> 0"
  shows "y = x *\<^sub>v\<^sub>m (mat_inv A) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y = x *\<^sub>v\<^sub>m mat_inv A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x = y *\<^sub>v\<^sub>m A
mat_det A \<noteq> 0

goal (1 subgoal):
 1. y = x *\<^sub>v\<^sub>m mat_inv A
[PROOF STEP]
by (cases y) (simp add: mat_inv_r)


[STATEMENT]
lemma mult_mv_cancel_l:
  assumes "mat_det A \<noteq> 0" and "A *\<^sub>m\<^sub>v v = A *\<^sub>m\<^sub>v v'"
  shows "v = v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v = v'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mat_det A \<noteq> 0
A *\<^sub>m\<^sub>v v = A *\<^sub>m\<^sub>v v'

goal (1 subgoal):
 1. v = v'
[PROOF STEP]
using mult_mv_inv
[PROOF STATE]
proof (prove)
using this:
mat_det A \<noteq> 0
A *\<^sub>m\<^sub>v v = A *\<^sub>m\<^sub>v v'
\<lbrakk>?x = ?A *\<^sub>m\<^sub>v ?y; mat_det ?A \<noteq> 0\<rbrakk> \<Longrightarrow> ?y = mat_inv ?A *\<^sub>m\<^sub>v ?x

goal (1 subgoal):
 1. v = v'
[PROOF STEP]
by blast


[STATEMENT]
lemma mult_vm_cancel_r:
  assumes "mat_det A \<noteq> 0" and "v *\<^sub>v\<^sub>m A = v' *\<^sub>v\<^sub>m A"
  shows "v = v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v = v'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mat_det A \<noteq> 0
v *\<^sub>v\<^sub>m A = v' *\<^sub>v\<^sub>m A

goal (1 subgoal):
 1. v = v'
[PROOF STEP]
using mult_vm_inv
[PROOF STATE]
proof (prove)
using this:
mat_det A \<noteq> 0
v *\<^sub>v\<^sub>m A = v' *\<^sub>v\<^sub>m A
\<lbrakk>?x = ?y *\<^sub>v\<^sub>m ?A; mat_det ?A \<noteq> 0\<rbrakk> \<Longrightarrow> ?y = ?x *\<^sub>v\<^sub>m mat_inv ?A

goal (1 subgoal):
 1. v = v'
[PROOF STEP]
by blast


[STATEMENT]
lemma vec_zero_l [simp]:
  shows "A *\<^sub>m\<^sub>v vec_zero = vec_zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>m\<^sub>v vec_zero = vec_zero
[PROOF STEP]
by (cases A) simp


[STATEMENT]
lemma vec_zero_r [simp]:
  shows "vec_zero *\<^sub>v\<^sub>m A = vec_zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_zero *\<^sub>v\<^sub>m A = vec_zero
[PROOF STEP]
by (cases A) simp


[STATEMENT]
lemma mult_mv_nonzero:
  assumes "v \<noteq> vec_zero" and "mat_det A \<noteq> 0"
  shows "A *\<^sub>m\<^sub>v v \<noteq> vec_zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>m\<^sub>v v \<noteq> vec_zero
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> A *\<^sub>m\<^sub>v v \<noteq> vec_zero \<Longrightarrow> False
[PROOF STEP]
using assms mult_mv_inv[of vec_zero A v] mat_inv_l vec_zero_l
[PROOF STATE]
proof (prove)
using this:
v \<noteq> vec_zero
mat_det A \<noteq> 0
\<lbrakk>vec_zero = A *\<^sub>m\<^sub>v v; mat_det A \<noteq> 0\<rbrakk> \<Longrightarrow> v = mat_inv A *\<^sub>m\<^sub>v vec_zero
mat_det ?A \<noteq> 0 \<Longrightarrow> mat_inv ?A *\<^sub>m\<^sub>m ?A = eye
?A *\<^sub>m\<^sub>v vec_zero = vec_zero

goal (1 subgoal):
 1. \<not> A *\<^sub>m\<^sub>v v \<noteq> vec_zero \<Longrightarrow> False
[PROOF STEP]
by auto


[STATEMENT]
lemma mult_vm_nonzero:
  assumes "v \<noteq> vec_zero" and "mat_det A \<noteq> 0"
  shows "v *\<^sub>v\<^sub>m A \<noteq> vec_zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v *\<^sub>v\<^sub>m A \<noteq> vec_zero
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> v *\<^sub>v\<^sub>m A \<noteq> vec_zero \<Longrightarrow> False
[PROOF STEP]
using assms mult_vm_inv[of vec_zero v A] mat_inv_r vec_zero_r
[PROOF STATE]
proof (prove)
using this:
v \<noteq> vec_zero
mat_det A \<noteq> 0
\<lbrakk>vec_zero = v *\<^sub>v\<^sub>m A; mat_det A \<noteq> 0\<rbrakk> \<Longrightarrow> v = vec_zero *\<^sub>v\<^sub>m mat_inv A
mat_det ?A \<noteq> 0 \<Longrightarrow> ?A *\<^sub>m\<^sub>m mat_inv ?A = eye
vec_zero *\<^sub>v\<^sub>m ?A = vec_zero

goal (1 subgoal):
 1. \<not> v *\<^sub>v\<^sub>m A \<noteq> vec_zero \<Longrightarrow> False
[PROOF STEP]
by auto


[STATEMENT]
lemma mult_sv_mv:
  shows "k *\<^sub>s\<^sub>v (A *\<^sub>m\<^sub>v v) = (A *\<^sub>m\<^sub>v (k *\<^sub>s\<^sub>v v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k *\<^sub>s\<^sub>v (A *\<^sub>m\<^sub>v v) = A *\<^sub>m\<^sub>v (k *\<^sub>s\<^sub>v v)
[PROOF STEP]
by (cases A, cases v) (simp add: field_simps)


[STATEMENT]
lemma mult_mv_mult_vm:
  shows "A *\<^sub>m\<^sub>v x = x *\<^sub>v\<^sub>m (mat_transpose A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>m\<^sub>v x = x *\<^sub>v\<^sub>m mat_transpose A
[PROOF STEP]
by (cases A, cases x) auto


[STATEMENT]
lemma mult_mv_vv:
  shows "A *\<^sub>m\<^sub>v v1 *\<^sub>v\<^sub>v v2 = v1 *\<^sub>v\<^sub>v (mat_transpose A *\<^sub>m\<^sub>v v2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>m\<^sub>v v1 *\<^sub>v\<^sub>v v2 = v1 *\<^sub>v\<^sub>v (mat_transpose A *\<^sub>m\<^sub>v v2)
[PROOF STEP]
by (cases v1, cases v2, cases A) (auto simp add: field_simps)


[STATEMENT]
lemma mult_vv_mv:
  shows "x *\<^sub>v\<^sub>v (A *\<^sub>m\<^sub>v y)  = (x *\<^sub>v\<^sub>m A) *\<^sub>v\<^sub>v y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x *\<^sub>v\<^sub>v (A *\<^sub>m\<^sub>v y) = x *\<^sub>v\<^sub>m A *\<^sub>v\<^sub>v y
[PROOF STEP]
by (cases x, cases y, cases A) (auto simp add: field_simps)


[STATEMENT]
lemma vec_cnj_mult_mv:
  shows "vec_cnj (A *\<^sub>m\<^sub>v x) =  (mat_cnj A) *\<^sub>m\<^sub>v (vec_cnj x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_cnj (A *\<^sub>m\<^sub>v x) = mat_cnj A *\<^sub>m\<^sub>v vec_cnj x
[PROOF STEP]
by (cases A, cases x) (auto simp add: vec_cnj_def mat_cnj_def)


[STATEMENT]
lemma vec_cnj_mult_vm:
  shows "vec_cnj (v *\<^sub>v\<^sub>m A) = vec_cnj v *\<^sub>v\<^sub>m mat_cnj A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_cnj (v *\<^sub>v\<^sub>m A) = vec_cnj v *\<^sub>v\<^sub>m mat_cnj A
[PROOF STEP]
unfolding vec_cnj_def mat_cnj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_map cnj (v *\<^sub>v\<^sub>m A) = vec_map cnj v *\<^sub>v\<^sub>m mat_map cnj A
[PROOF STEP]
by (cases A, cases v, auto)


[STATEMENT]
lemma eigen_equation:
  shows "eigenval k H \<longleftrightarrow> k\<^sup>2 - mat_trace H * k + mat_det H = 0" (is "?lhs \<longleftrightarrow> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eigenval k H = (k\<^sup>2 - mat_trace H * k + mat_det H = 0)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eigenval k H = (k\<^sup>2 - mat_trace H * k + mat_det H = 0)
[PROOF STEP]
obtain A B C D where HH: "H = (A, B, C, D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A B C D. H = (A, B, C, D) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases H) auto
[PROOF STATE]
proof (state)
this:
H = (A, B, C, D)

goal (1 subgoal):
 1. eigenval k H = (k\<^sup>2 - mat_trace H * k + mat_det H = 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eigenval k H = (k\<^sup>2 - mat_trace H * k + mat_det H = 0)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. eigenval k H \<Longrightarrow> k\<^sup>2 - mat_trace H * k + mat_det H = 0
 2. k\<^sup>2 - mat_trace H * k + mat_det H = 0 \<Longrightarrow> eigenval k H
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
eigenval k H

goal (2 subgoals):
 1. eigenval k H \<Longrightarrow> k\<^sup>2 - mat_trace H * k + mat_det H = 0
 2. k\<^sup>2 - mat_trace H * k + mat_det H = 0 \<Longrightarrow> eigenval k H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eigenval k H
[PROOF STEP]
obtain v where "v \<noteq> vec_zero" "H *\<^sub>m\<^sub>v v = k *\<^sub>s\<^sub>v v"
[PROOF STATE]
proof (prove)
using this:
eigenval k H

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<noteq> vec_zero; H *\<^sub>m\<^sub>v v = k *\<^sub>s\<^sub>v v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding eigenval_def
[PROOF STATE]
proof (prove)
using this:
\<exists>v. v \<noteq> vec_zero \<and> H *\<^sub>m\<^sub>v v = k *\<^sub>s\<^sub>v v

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<noteq> vec_zero; H *\<^sub>m\<^sub>v v = k *\<^sub>s\<^sub>v v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v \<noteq> vec_zero
H *\<^sub>m\<^sub>v v = k *\<^sub>s\<^sub>v v

goal (2 subgoals):
 1. eigenval k H \<Longrightarrow> k\<^sup>2 - mat_trace H * k + mat_det H = 0
 2. k\<^sup>2 - mat_trace H * k + mat_det H = 0 \<Longrightarrow> eigenval k H
[PROOF STEP]
obtain v1 v2 where vv: "v = (v1, v2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v1 v2. v = (v1, v2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases v) auto
[PROOF STATE]
proof (state)
this:
v = (v1, v2)

goal (2 subgoals):
 1. eigenval k H \<Longrightarrow> k\<^sup>2 - mat_trace H * k + mat_det H = 0
 2. k\<^sup>2 - mat_trace H * k + mat_det H = 0 \<Longrightarrow> eigenval k H
[PROOF STEP]
from \<open>H *\<^sub>m\<^sub>v v = k *\<^sub>s\<^sub>v v\<close>
[PROOF STATE]
proof (chain)
picking this:
H *\<^sub>m\<^sub>v v = k *\<^sub>s\<^sub>v v
[PROOF STEP]
have "(H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye)) *\<^sub>m\<^sub>v v = vec_zero"
[PROOF STATE]
proof (prove)
using this:
H *\<^sub>m\<^sub>v v = k *\<^sub>s\<^sub>v v

goal (1 subgoal):
 1. H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v v = vec_zero
[PROOF STEP]
using HH vv
[PROOF STATE]
proof (prove)
using this:
H *\<^sub>m\<^sub>v v = k *\<^sub>s\<^sub>v v
H = (A, B, C, D)
v = (v1, v2)

goal (1 subgoal):
 1. H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v v = vec_zero
[PROOF STEP]
by (auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v v = vec_zero

goal (2 subgoals):
 1. eigenval k H \<Longrightarrow> k\<^sup>2 - mat_trace H * k + mat_det H = 0
 2. k\<^sup>2 - mat_trace H * k + mat_det H = 0 \<Longrightarrow> eigenval k H
[PROOF STEP]
hence "mat_det (H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye)) = 0"
[PROOF STATE]
proof (prove)
using this:
H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v v = vec_zero

goal (1 subgoal):
 1. mat_det (H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye)) = 0
[PROOF STEP]
using \<open>v \<noteq> vec_zero\<close> vv HH
[PROOF STATE]
proof (prove)
using this:
H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v v = vec_zero
v \<noteq> vec_zero
v = (v1, v2)
H = (A, B, C, D)

goal (1 subgoal):
 1. mat_det (H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye)) = 0
[PROOF STEP]
using regular_homogenous_system[of "A - k" B C "D - k" v1 v2]
[PROOF STATE]
proof (prove)
using this:
H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v v = vec_zero
v \<noteq> vec_zero
v = (v1, v2)
H = (A, B, C, D)
\<lbrakk>det2 (A - k) B C (D - k) \<noteq> 0; (A - k) * v1 + B * v2 = 0; C * v1 + (D - k) * v2 = 0\<rbrakk> \<Longrightarrow> v1 = 0 \<and> v2 = 0

goal (1 subgoal):
 1. mat_det (H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye)) = 0
[PROOF STEP]
unfolding det2_def
[PROOF STATE]
proof (prove)
using this:
H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v v = vec_zero
v \<noteq> vec_zero
v = (v1, v2)
H = (A, B, C, D)
\<lbrakk>(A - k) * (D - k) - B * C \<noteq> 0; (A - k) * v1 + B * v2 = 0; C * v1 + (D - k) * v2 = 0\<rbrakk> \<Longrightarrow> v1 = 0 \<and> v2 = 0

goal (1 subgoal):
 1. mat_det (H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye)) = 0
[PROOF STEP]
by (auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
mat_det (H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye)) = 0

goal (2 subgoals):
 1. eigenval k H \<Longrightarrow> k\<^sup>2 - mat_trace H * k + mat_det H = 0
 2. k\<^sup>2 - mat_trace H * k + mat_det H = 0 \<Longrightarrow> eigenval k H
[PROOF STEP]
thus ?rhs
[PROOF STATE]
proof (prove)
using this:
mat_det (H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye)) = 0

goal (1 subgoal):
 1. k\<^sup>2 - mat_trace H * k + mat_det H = 0
[PROOF STEP]
using HH
[PROOF STATE]
proof (prove)
using this:
mat_det (H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye)) = 0
H = (A, B, C, D)

goal (1 subgoal):
 1. k\<^sup>2 - mat_trace H * k + mat_det H = 0
[PROOF STEP]
by (auto simp add: power2_eq_square field_simps)
[PROOF STATE]
proof (state)
this:
k\<^sup>2 - mat_trace H * k + mat_det H = 0

goal (1 subgoal):
 1. k\<^sup>2 - mat_trace H * k + mat_det H = 0 \<Longrightarrow> eigenval k H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k\<^sup>2 - mat_trace H * k + mat_det H = 0 \<Longrightarrow> eigenval k H
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
k\<^sup>2 - mat_trace H * k + mat_det H = 0

goal (1 subgoal):
 1. k\<^sup>2 - mat_trace H * k + mat_det H = 0 \<Longrightarrow> eigenval k H
[PROOF STEP]
hence *: "mat_det (H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye)) = 0"
[PROOF STATE]
proof (prove)
using this:
k\<^sup>2 - mat_trace H * k + mat_det H = 0

goal (1 subgoal):
 1. mat_det (H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye)) = 0
[PROOF STEP]
using HH
[PROOF STATE]
proof (prove)
using this:
k\<^sup>2 - mat_trace H * k + mat_det H = 0
H = (A, B, C, D)

goal (1 subgoal):
 1. mat_det (H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye)) = 0
[PROOF STEP]
by (auto simp add: field_simps power2_eq_square)
[PROOF STATE]
proof (state)
this:
mat_det (H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye)) = 0

goal (1 subgoal):
 1. k\<^sup>2 - mat_trace H * k + mat_det H = 0 \<Longrightarrow> eigenval k H
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eigenval k H
[PROOF STEP]
proof (cases "H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) = mat_zero")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) = mat_zero \<Longrightarrow> eigenval k H
 2. H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) \<noteq> mat_zero \<Longrightarrow> eigenval k H
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) = mat_zero

goal (2 subgoals):
 1. H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) = mat_zero \<Longrightarrow> eigenval k H
 2. H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) \<noteq> mat_zero \<Longrightarrow> eigenval k H
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) = mat_zero

goal (1 subgoal):
 1. eigenval k H
[PROOF STEP]
using HH
[PROOF STATE]
proof (prove)
using this:
H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) = mat_zero
H = (A, B, C, D)

goal (1 subgoal):
 1. eigenval k H
[PROOF STEP]
by (auto) (rule_tac x=1 in exI, simp)
[PROOF STATE]
proof (state)
this:
eigenval k H

goal (1 subgoal):
 1. H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) \<noteq> mat_zero \<Longrightarrow> eigenval k H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) \<noteq> mat_zero \<Longrightarrow> eigenval k H
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) \<noteq> mat_zero

goal (1 subgoal):
 1. H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) \<noteq> mat_zero \<Longrightarrow> eigenval k H
[PROOF STEP]
hence "(A - k \<noteq> 0 \<or> B \<noteq> 0) \<or> (D - k \<noteq> 0 \<or> C \<noteq> 0)"
[PROOF STATE]
proof (prove)
using this:
H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) \<noteq> mat_zero

goal (1 subgoal):
 1. (A - k \<noteq> 0 \<or> B \<noteq> 0) \<or> D - k \<noteq> 0 \<or> C \<noteq> 0
[PROOF STEP]
using HH
[PROOF STATE]
proof (prove)
using this:
H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) \<noteq> mat_zero
H = (A, B, C, D)

goal (1 subgoal):
 1. (A - k \<noteq> 0 \<or> B \<noteq> 0) \<or> D - k \<noteq> 0 \<or> C \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(A - k \<noteq> 0 \<or> B \<noteq> 0) \<or> D - k \<noteq> 0 \<or> C \<noteq> 0

goal (1 subgoal):
 1. H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) \<noteq> mat_zero \<Longrightarrow> eigenval k H
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(A - k \<noteq> 0 \<or> B \<noteq> 0) \<or> D - k \<noteq> 0 \<or> C \<noteq> 0

goal (1 subgoal):
 1. eigenval k H
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A - k \<noteq> 0 \<or> B \<noteq> 0 \<Longrightarrow> eigenval k H
 2. D - k \<noteq> 0 \<or> C \<noteq> 0 \<Longrightarrow> eigenval k H
[PROOF STEP]
assume "A - k \<noteq> 0 \<or> B \<noteq> 0"
[PROOF STATE]
proof (state)
this:
A - k \<noteq> 0 \<or> B \<noteq> 0

goal (2 subgoals):
 1. A - k \<noteq> 0 \<or> B \<noteq> 0 \<Longrightarrow> eigenval k H
 2. D - k \<noteq> 0 \<or> C \<noteq> 0 \<Longrightarrow> eigenval k H
[PROOF STEP]
hence "C * B + (D - k) * (k - A) = 0"
[PROOF STATE]
proof (prove)
using this:
A - k \<noteq> 0 \<or> B \<noteq> 0

goal (1 subgoal):
 1. C * B + (D - k) * (k - A) = 0
[PROOF STEP]
using * singular_system[of "A-k" "D-k" B C "(0, 0)" 0 0  "(B, k-A)"] HH
[PROOF STATE]
proof (prove)
using this:
A - k \<noteq> 0 \<or> B \<noteq> 0
mat_det (H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye)) = 0
\<lbrakk>det2 (A - k) (D - k) B C = 0; A - k \<noteq> 0 \<or> D - k \<noteq> 0; (A - k) * fst (0, 0) + (D - k) * snd (0, 0) = 0; B * fst (0, 0) + C * snd (0, 0) = 0; (A - k) * fst (B, k - A) + (D - k) * snd (B, k - A) = 0\<rbrakk> \<Longrightarrow> B * fst (B, k - A) + C * snd (B, k - A) = 0
H = (A, B, C, D)

goal (1 subgoal):
 1. C * B + (D - k) * (k - A) = 0
[PROOF STEP]
by (auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
C * B + (D - k) * (k - A) = 0

goal (2 subgoals):
 1. A - k \<noteq> 0 \<or> B \<noteq> 0 \<Longrightarrow> eigenval k H
 2. D - k \<noteq> 0 \<or> C \<noteq> 0 \<Longrightarrow> eigenval k H
[PROOF STEP]
hence  "(B, k-A) \<noteq> vec_zero" "(H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye)) *\<^sub>m\<^sub>v (B, k-A) = vec_zero"
[PROOF STATE]
proof (prove)
using this:
C * B + (D - k) * (k - A) = 0

goal (1 subgoal):
 1. (B, k - A) \<noteq> vec_zero &&& H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v (B, k - A) = vec_zero
[PROOF STEP]
using HH \<open>A - k \<noteq> 0 \<or> B \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
C * B + (D - k) * (k - A) = 0
H = (A, B, C, D)
A - k \<noteq> 0 \<or> B \<noteq> 0

goal (1 subgoal):
 1. (B, k - A) \<noteq> vec_zero &&& H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v (B, k - A) = vec_zero
[PROOF STEP]
by (auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
(B, k - A) \<noteq> vec_zero
H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v (B, k - A) = vec_zero

goal (2 subgoals):
 1. A - k \<noteq> 0 \<or> B \<noteq> 0 \<Longrightarrow> eigenval k H
 2. D - k \<noteq> 0 \<or> C \<noteq> 0 \<Longrightarrow> eigenval k H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(B, k - A) \<noteq> vec_zero
H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v (B, k - A) = vec_zero
[PROOF STEP]
obtain v where "v \<noteq> vec_zero \<and> (H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye)) *\<^sub>m\<^sub>v v = vec_zero"
[PROOF STATE]
proof (prove)
using this:
(B, k - A) \<noteq> vec_zero
H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v (B, k - A) = vec_zero

goal (1 subgoal):
 1. (\<And>v. v \<noteq> vec_zero \<and> H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v v = vec_zero \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v \<noteq> vec_zero \<and> H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v v = vec_zero

goal (2 subgoals):
 1. A - k \<noteq> 0 \<or> B \<noteq> 0 \<Longrightarrow> eigenval k H
 2. D - k \<noteq> 0 \<or> C \<noteq> 0 \<Longrightarrow> eigenval k H
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
v \<noteq> vec_zero \<and> H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v v = vec_zero

goal (1 subgoal):
 1. eigenval k H
[PROOF STEP]
using HH
[PROOF STATE]
proof (prove)
using this:
v \<noteq> vec_zero \<and> H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v v = vec_zero
H = (A, B, C, D)

goal (1 subgoal):
 1. eigenval k H
[PROOF STEP]
unfolding eigenval_def
[PROOF STATE]
proof (prove)
using this:
v \<noteq> vec_zero \<and> H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v v = vec_zero
H = (A, B, C, D)

goal (1 subgoal):
 1. \<exists>v. v \<noteq> vec_zero \<and> H *\<^sub>m\<^sub>v v = k *\<^sub>s\<^sub>v v
[PROOF STEP]
by (rule_tac x="v" in exI) (case_tac v, simp add: field_simps)
[PROOF STATE]
proof (state)
this:
eigenval k H

goal (1 subgoal):
 1. D - k \<noteq> 0 \<or> C \<noteq> 0 \<Longrightarrow> eigenval k H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. D - k \<noteq> 0 \<or> C \<noteq> 0 \<Longrightarrow> eigenval k H
[PROOF STEP]
assume "D - k \<noteq> 0 \<or> C \<noteq> 0"
[PROOF STATE]
proof (state)
this:
D - k \<noteq> 0 \<or> C \<noteq> 0

goal (1 subgoal):
 1. D - k \<noteq> 0 \<or> C \<noteq> 0 \<Longrightarrow> eigenval k H
[PROOF STEP]
hence "C * B + (D - k) * (k - A) = 0"
[PROOF STATE]
proof (prove)
using this:
D - k \<noteq> 0 \<or> C \<noteq> 0

goal (1 subgoal):
 1. C * B + (D - k) * (k - A) = 0
[PROOF STEP]
using * singular_system[of "D-k" "A-k" C B "(0, 0)" 0 0  "(C, k-D)"] HH
[PROOF STATE]
proof (prove)
using this:
D - k \<noteq> 0 \<or> C \<noteq> 0
mat_det (H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye)) = 0
\<lbrakk>det2 (D - k) (A - k) C B = 0; D - k \<noteq> 0 \<or> A - k \<noteq> 0; (D - k) * fst (0, 0) + (A - k) * snd (0, 0) = 0; C * fst (0, 0) + B * snd (0, 0) = 0; (D - k) * fst (C, k - D) + (A - k) * snd (C, k - D) = 0\<rbrakk> \<Longrightarrow> C * fst (C, k - D) + B * snd (C, k - D) = 0
H = (A, B, C, D)

goal (1 subgoal):
 1. C * B + (D - k) * (k - A) = 0
[PROOF STEP]
by (auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
C * B + (D - k) * (k - A) = 0

goal (1 subgoal):
 1. D - k \<noteq> 0 \<or> C \<noteq> 0 \<Longrightarrow> eigenval k H
[PROOF STEP]
hence  "(k-D, C) \<noteq> vec_zero" "(H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye)) *\<^sub>m\<^sub>v (k-D, C) = vec_zero"
[PROOF STATE]
proof (prove)
using this:
C * B + (D - k) * (k - A) = 0

goal (1 subgoal):
 1. (k - D, C) \<noteq> vec_zero &&& H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v (k - D, C) = vec_zero
[PROOF STEP]
using HH \<open>D - k \<noteq> 0 \<or> C \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
C * B + (D - k) * (k - A) = 0
H = (A, B, C, D)
D - k \<noteq> 0 \<or> C \<noteq> 0

goal (1 subgoal):
 1. (k - D, C) \<noteq> vec_zero &&& H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v (k - D, C) = vec_zero
[PROOF STEP]
by (auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
(k - D, C) \<noteq> vec_zero
H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v (k - D, C) = vec_zero

goal (1 subgoal):
 1. D - k \<noteq> 0 \<or> C \<noteq> 0 \<Longrightarrow> eigenval k H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(k - D, C) \<noteq> vec_zero
H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v (k - D, C) = vec_zero
[PROOF STEP]
obtain v where "v \<noteq> vec_zero \<and> (H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye)) *\<^sub>m\<^sub>v v = vec_zero"
[PROOF STATE]
proof (prove)
using this:
(k - D, C) \<noteq> vec_zero
H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v (k - D, C) = vec_zero

goal (1 subgoal):
 1. (\<And>v. v \<noteq> vec_zero \<and> H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v v = vec_zero \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v \<noteq> vec_zero \<and> H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v v = vec_zero

goal (1 subgoal):
 1. D - k \<noteq> 0 \<or> C \<noteq> 0 \<Longrightarrow> eigenval k H
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
v \<noteq> vec_zero \<and> H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v v = vec_zero

goal (1 subgoal):
 1. eigenval k H
[PROOF STEP]
using HH
[PROOF STATE]
proof (prove)
using this:
v \<noteq> vec_zero \<and> H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v v = vec_zero
H = (A, B, C, D)

goal (1 subgoal):
 1. eigenval k H
[PROOF STEP]
unfolding eigenval_def
[PROOF STATE]
proof (prove)
using this:
v \<noteq> vec_zero \<and> H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) *\<^sub>m\<^sub>v v = vec_zero
H = (A, B, C, D)

goal (1 subgoal):
 1. \<exists>v. v \<noteq> vec_zero \<and> H *\<^sub>m\<^sub>v v = k *\<^sub>s\<^sub>v v
[PROOF STEP]
by (rule_tac x="v" in exI) (case_tac v, simp add: field_simps)
[PROOF STATE]
proof (state)
this:
eigenval k H

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eigenval k H

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eigenval k H

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eigenval k H = (k\<^sup>2 - mat_trace H * k + mat_det H = 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bilinear_form_scale_m:
  shows "bilinear_form v1 v2 (k *\<^sub>s\<^sub>m H) = k * bilinear_form v1 v2 H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bilinear_form v1 v2 (k *\<^sub>s\<^sub>m H) = k * bilinear_form v1 v2 H
[PROOF STEP]
by (cases v1, cases v2, cases H) (simp add: vec_cnj_def field_simps)


[STATEMENT]
lemma bilinear_form_scale_v1:
  shows "bilinear_form (k *\<^sub>s\<^sub>v v1) v2 H = cnj k * bilinear_form v1 v2 H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bilinear_form (k *\<^sub>s\<^sub>v v1) v2 H = cnj k * bilinear_form v1 v2 H
[PROOF STEP]
by (cases v1, cases v2, cases H) (simp add: vec_cnj_def field_simps)


[STATEMENT]
lemma bilinear_form_scale_v2:
  shows "bilinear_form  v1 (k *\<^sub>s\<^sub>v v2) H = k * bilinear_form v1 v2 H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bilinear_form v1 (k *\<^sub>s\<^sub>v v2) H = k * bilinear_form v1 v2 H
[PROOF STEP]
by (cases v1, cases v2, cases H) (simp add: vec_cnj_def field_simps)


[STATEMENT]
lemma quad_form_bilinear_form:
  shows "quad_form v H = bilinear_form v v H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quad_form v H = bilinear_form v v H
[PROOF STEP]
by simp


[STATEMENT]
lemma quad_form_scale_v:
  shows "quad_form (k *\<^sub>s\<^sub>v v) H = cor ((cmod k)\<^sup>2) * quad_form v H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quad_form (k *\<^sub>s\<^sub>v v) H = cor ((cmod k)\<^sup>2) * quad_form v H
[PROOF STEP]
using bilinear_form_scale_v1 bilinear_form_scale_v2
[PROOF STATE]
proof (prove)
using this:
bilinear_form (?k *\<^sub>s\<^sub>v ?v1.0) ?v2.0 ?H = cnj ?k * bilinear_form ?v1.0 ?v2.0 ?H
bilinear_form ?v1.0 (?k *\<^sub>s\<^sub>v ?v2.0) ?H = ?k * bilinear_form ?v1.0 ?v2.0 ?H

goal (1 subgoal):
 1. quad_form (k *\<^sub>s\<^sub>v v) H = cor ((cmod k)\<^sup>2) * quad_form v H
[PROOF STEP]
by (simp add: complex_mult_cnj_cmod field_simps)


[STATEMENT]
lemma quad_form_scale_m:
  shows "quad_form v (k *\<^sub>s\<^sub>m H) = k * quad_form v H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quad_form v (k *\<^sub>s\<^sub>m H) = k * quad_form v H
[PROOF STEP]
using bilinear_form_scale_m
[PROOF STATE]
proof (prove)
using this:
bilinear_form ?v1.0 ?v2.0 (?k *\<^sub>s\<^sub>m ?H) = ?k * bilinear_form ?v1.0 ?v2.0 ?H

goal (1 subgoal):
 1. quad_form v (k *\<^sub>s\<^sub>m H) = k * quad_form v H
[PROOF STEP]
by simp


[STATEMENT]
lemma cnj_quad_form [simp]:
  shows "cnj (quad_form z H) = quad_form z (mat_adj H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnj (quad_form z H) = quad_form z (mat_adj H)
[PROOF STEP]
by (cases H, cases z) (auto simp add: mat_adj_def mat_cnj_def vec_cnj_def field_simps)


[STATEMENT]
lemma congruence_nonzero:
  assumes "H \<noteq> mat_zero" and "mat_det M \<noteq> 0"
  shows "congruence M H \<noteq> mat_zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. congruence M H \<noteq> mat_zero
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
H \<noteq> mat_zero
mat_det M \<noteq> 0

goal (1 subgoal):
 1. congruence M H \<noteq> mat_zero
[PROOF STEP]
unfolding congruence_def
[PROOF STATE]
proof (prove)
using this:
H \<noteq> mat_zero
mat_det M \<noteq> 0

goal (1 subgoal):
 1. mat_adj M *\<^sub>m\<^sub>m H *\<^sub>m\<^sub>m M \<noteq> mat_zero
[PROOF STEP]
by (subst mult_mm_non_zero_r, subst mult_mm_non_zero_l) (auto simp add: mat_det_adj)


[STATEMENT]
lemma congruence_congruence:
  shows "congruence M1 (congruence M2 H) = congruence (M2 *\<^sub>m\<^sub>m M1) H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. congruence M1 (congruence M2 H) = congruence (M2 *\<^sub>m\<^sub>m M1) H
[PROOF STEP]
unfolding congruence_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_adj M1 *\<^sub>m\<^sub>m (mat_adj M2 *\<^sub>m\<^sub>m H *\<^sub>m\<^sub>m M2) *\<^sub>m\<^sub>m M1 = mat_adj (M2 *\<^sub>m\<^sub>m M1) *\<^sub>m\<^sub>m H *\<^sub>m\<^sub>m (M2 *\<^sub>m\<^sub>m M1)
[PROOF STEP]
apply (subst mult_mm_assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_adj M1 *\<^sub>m\<^sub>m (mat_adj M2 *\<^sub>m\<^sub>m H) *\<^sub>m\<^sub>m M2 *\<^sub>m\<^sub>m M1 = mat_adj (M2 *\<^sub>m\<^sub>m M1) *\<^sub>m\<^sub>m H *\<^sub>m\<^sub>m (M2 *\<^sub>m\<^sub>m M1)
[PROOF STEP]
apply (subst mult_mm_assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_adj M1 *\<^sub>m\<^sub>m mat_adj M2 *\<^sub>m\<^sub>m H *\<^sub>m\<^sub>m M2 *\<^sub>m\<^sub>m M1 = mat_adj (M2 *\<^sub>m\<^sub>m M1) *\<^sub>m\<^sub>m H *\<^sub>m\<^sub>m (M2 *\<^sub>m\<^sub>m M1)
[PROOF STEP]
apply (subst mat_adj_mult_mm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_adj M1 *\<^sub>m\<^sub>m mat_adj M2 *\<^sub>m\<^sub>m H *\<^sub>m\<^sub>m M2 *\<^sub>m\<^sub>m M1 = mat_adj M1 *\<^sub>m\<^sub>m mat_adj M2 *\<^sub>m\<^sub>m H *\<^sub>m\<^sub>m (M2 *\<^sub>m\<^sub>m M1)
[PROOF STEP]
apply (subst mult_mm_assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_adj M1 *\<^sub>m\<^sub>m mat_adj M2 *\<^sub>m\<^sub>m H *\<^sub>m\<^sub>m M2 *\<^sub>m\<^sub>m M1 = mat_adj M1 *\<^sub>m\<^sub>m mat_adj M2 *\<^sub>m\<^sub>m H *\<^sub>m\<^sub>m M2 *\<^sub>m\<^sub>m M1
[PROOF STEP]
by simp


[STATEMENT]
lemma congruence_eye [simp]:
  shows "congruence eye H = H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. congruence eye H = H
[PROOF STEP]
by (cases H) (simp add: mat_adj_def mat_cnj_def)