[STATEMENT]
lemma append_rows_mult_left_id:
  assumes A: "(A::'a::comm_semiring_1 mat) \<in> carrier_mat 1 n"
  and B: "B \<in> carrier_mat (m-1) n"
  and C: "C = four_block_mat (1\<^sub>m 1) (0\<^sub>m 1 (m - 1)) (0\<^sub>m (m - 1) 1) D"
  and D: "D \<in> carrier_mat (m-1) (m-1)"
shows "C * (A @\<^sub>r B) = A @\<^sub>r (D * B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C * (A @\<^sub>r B) = A @\<^sub>r D * B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. C * (A @\<^sub>r B) = A @\<^sub>r D * B
[PROOF STEP]
have "transpose_mat (C * (A @\<^sub>r B)) = (A @\<^sub>r B)\<^sup>T * C\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C * (A @\<^sub>r B))\<^sup>T = (A @\<^sub>r B)\<^sup>T * C\<^sup>T
[PROOF STEP]
by (metis (no_types, lifting) B C D Matrix.transpose_mult append_rows_def A carrier_matD
        carrier_mat_triv index_mat_four_block(2,3) index_zero_mat(2) one_carrier_mat)
[PROOF STATE]
proof (state)
this:
(C * (A @\<^sub>r B))\<^sup>T = (A @\<^sub>r B)\<^sup>T * C\<^sup>T

goal (1 subgoal):
 1. C * (A @\<^sub>r B) = A @\<^sub>r D * B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(C * (A @\<^sub>r B))\<^sup>T = (A @\<^sub>r B)\<^sup>T * C\<^sup>T

goal (1 subgoal):
 1. C * (A @\<^sub>r B) = A @\<^sub>r D * B
[PROOF STEP]
have "... = (A\<^sup>T @\<^sub>c B\<^sup>T) * C\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A @\<^sub>r B)\<^sup>T * C\<^sup>T = (A\<^sup>T @\<^sub>c B\<^sup>T) * C\<^sup>T
[PROOF STEP]
using transpose_mat_append_rows[OF A B]
[PROOF STATE]
proof (prove)
using this:
(A @\<^sub>r B)\<^sup>T = A\<^sup>T @\<^sub>c B\<^sup>T

goal (1 subgoal):
 1. (A @\<^sub>r B)\<^sup>T * C\<^sup>T = (A\<^sup>T @\<^sub>c B\<^sup>T) * C\<^sup>T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(A @\<^sub>r B)\<^sup>T * C\<^sup>T = (A\<^sup>T @\<^sub>c B\<^sup>T) * C\<^sup>T

goal (1 subgoal):
 1. C * (A @\<^sub>r B) = A @\<^sub>r D * B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(A @\<^sub>r B)\<^sup>T * C\<^sup>T = (A\<^sup>T @\<^sub>c B\<^sup>T) * C\<^sup>T

goal (1 subgoal):
 1. C * (A @\<^sub>r B) = A @\<^sub>r D * B
[PROOF STEP]
have "... = A\<^sup>T @\<^sub>c (B\<^sup>T * D\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A\<^sup>T @\<^sub>c B\<^sup>T) * C\<^sup>T = A\<^sup>T @\<^sub>c B\<^sup>T * D\<^sup>T
[PROOF STEP]
by (rule append_cols_mult_right_id, insert A B C D, auto)
[PROOF STATE]
proof (state)
this:
(A\<^sup>T @\<^sub>c B\<^sup>T) * C\<^sup>T = A\<^sup>T @\<^sub>c B\<^sup>T * D\<^sup>T

goal (1 subgoal):
 1. C * (A @\<^sub>r B) = A @\<^sub>r D * B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(A\<^sup>T @\<^sub>c B\<^sup>T) * C\<^sup>T = A\<^sup>T @\<^sub>c B\<^sup>T * D\<^sup>T

goal (1 subgoal):
 1. C * (A @\<^sub>r B) = A @\<^sub>r D * B
[PROOF STEP]
have "transpose_mat ... = A @\<^sub>r (D * B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A\<^sup>T @\<^sub>c B\<^sup>T * D\<^sup>T)\<^sup>T = A @\<^sub>r D * B
[PROOF STEP]
by (smt B D Matrix.transpose_mult Matrix.transpose_transpose append_cols_def append_rows_def A
        carrier_matD(2) carrier_mat_triv index_mult_mat(3) index_transpose_mat(3)
        transpose_four_block_mat zero_carrier_mat zero_transpose_mat)
[PROOF STATE]
proof (state)
this:
(A\<^sup>T @\<^sub>c B\<^sup>T * D\<^sup>T)\<^sup>T = A @\<^sub>r D * B

goal (1 subgoal):
 1. C * (A @\<^sub>r B) = A @\<^sub>r D * B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(C * (A @\<^sub>r B))\<^sup>T\<^sup>T = A @\<^sub>r D * B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(C * (A @\<^sub>r B))\<^sup>T\<^sup>T = A @\<^sub>r D * B

goal (1 subgoal):
 1. C * (A @\<^sub>r B) = A @\<^sub>r D * B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C * (A @\<^sub>r B) = A @\<^sub>r D * B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_eval_Throw:
assumes eval_e: "P \<turnstile> \<langle>throw x,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>"
shows "P \<turnstile> \<langle>map Val vs @ throw x # es',s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<langle>map Val vs @ throw x # es',s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<langle>map Val vs @ throw x # es',s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<turnstile> \<langle>map Val vs @ throw x # es',s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
from eval_e
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> \<langle>throw x,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>
[PROOF STEP]
obtain a where e': "e' = Throw a"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> \<langle>throw x,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>

goal (1 subgoal):
 1. (\<And>a. e' = Throw a \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases) (auto dest!: eval_final)
[PROOF STATE]
proof (state)
this:
e' = Throw a

goal (1 subgoal):
 1. P \<turnstile> \<langle>map Val vs @ throw x # es',s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
e' = Throw a

goal (1 subgoal):
 1. P \<turnstile> \<langle>map Val vs @ throw x # es',s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
fix es
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<turnstile> \<langle>map Val vs @ throw x # es',s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
have "\<And>vs. es = map Val vs @ throw x # es'
           \<Longrightarrow> P \<turnstile> \<langle>es,s\<rangle>[\<Rightarrow>]\<langle>map Val vs @ e' # es',s'\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>vs. es = map Val vs @ throw x # es' \<Longrightarrow> P \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
proof (induct es type: list)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>vs. [] = map Val vs @ throw x # es' \<Longrightarrow> P \<turnstile> \<langle>[],s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
 2. \<And>a list vs. \<lbrakk>\<And>vs. list = map Val vs @ throw x # es' \<Longrightarrow> P \<turnstile> \<langle>list,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>; a # list = map Val vs @ throw x # es'\<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>a # list,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
[] = map Val vs @ throw x # es'

goal (2 subgoals):
 1. \<And>vs. [] = map Val vs @ throw x # es' \<Longrightarrow> P \<turnstile> \<langle>[],s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
 2. \<And>a list vs. \<lbrakk>\<And>vs. list = map Val vs @ throw x # es' \<Longrightarrow> P \<turnstile> \<langle>list,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>; a # list = map Val vs @ throw x # es'\<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>a # list,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
[] = map Val vs @ throw x # es'

goal (1 subgoal):
 1. P \<turnstile> \<langle>[],s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<langle>[],s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>

goal (1 subgoal):
 1. \<And>a list vs. \<lbrakk>\<And>vs. list = map Val vs @ throw x # es' \<Longrightarrow> P \<turnstile> \<langle>list,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>; a # list = map Val vs @ throw x # es'\<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>a # list,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list vs. \<lbrakk>\<And>vs. list = map Val vs @ throw x # es' \<Longrightarrow> P \<turnstile> \<langle>list,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>; a # list = map Val vs @ throw x # es'\<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>a # list,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
case (Cons e es vs)
[PROOF STATE]
proof (state)
this:
es = map Val ?vs @ throw x # es' \<Longrightarrow> P \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>map Val ?vs @ e' # es',s'\<rangle>
e # es = map Val vs @ throw x # es'

goal (1 subgoal):
 1. \<And>a list vs. \<lbrakk>\<And>vs. list = map Val vs @ throw x # es' \<Longrightarrow> P \<turnstile> \<langle>list,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>; a # list = map Val vs @ throw x # es'\<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>a # list,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
have e_es: "e # es = map Val vs @ throw x # es'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e # es = map Val vs @ throw x # es'
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
e # es = map Val vs @ throw x # es'

goal (1 subgoal):
 1. \<And>a list vs. \<lbrakk>\<And>vs. list = map Val vs @ throw x # es' \<Longrightarrow> P \<turnstile> \<langle>list,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>; a # list = map Val vs @ throw x # es'\<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>a # list,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
show "P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
proof (cases vs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vs = [] \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
 2. \<And>a list. vs = a # list \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
vs = []

goal (2 subgoals):
 1. vs = [] \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
 2. \<And>a list. vs = a # list \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
with e_es
[PROOF STATE]
proof (chain)
picking this:
e # es = map Val vs @ throw x # es'
vs = []
[PROOF STEP]
obtain "e=throw x" "es=es'"
[PROOF STATE]
proof (prove)
using this:
e # es = map Val vs @ throw x # es'
vs = []

goal (1 subgoal):
 1. (\<lbrakk>e = throw x; es = es'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
e = throw x
es = es'

goal (2 subgoals):
 1. vs = [] \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
 2. \<And>a list. vs = a # list \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
e = throw x
es = es'

goal (2 subgoals):
 1. vs = [] \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
 2. \<And>a list. vs = a # list \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
from eval_e e'
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> \<langle>throw x,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>
e' = Throw a
[PROOF STEP]
have "P \<turnstile> \<langle>throw x # es,s\<rangle> [\<Rightarrow>] \<langle>Throw a # es,s'\<rangle>"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> \<langle>throw x,s\<rangle> \<Rightarrow> \<langle>e',s'\<rangle>
e' = Throw a

goal (1 subgoal):
 1. P \<turnstile> \<langle>throw x # es,s\<rangle> [\<Rightarrow>] \<langle>Throw a # es,s'\<rangle>
[PROOF STEP]
by (iprover intro: ConsThrow)
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<langle>throw x # es,s\<rangle> [\<Rightarrow>] \<langle>Throw a # es,s'\<rangle>

goal (2 subgoals):
 1. vs = [] \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
 2. \<And>a list. vs = a # list \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
e = throw x
es = es'
P \<turnstile> \<langle>throw x # es,s\<rangle> [\<Rightarrow>] \<langle>Throw a # es,s'\<rangle>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
e = throw x
es = es'
P \<turnstile> \<langle>throw x # es,s\<rangle> [\<Rightarrow>] \<langle>Throw a # es,s'\<rangle>

goal (1 subgoal):
 1. P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
using Nil e'
[PROOF STATE]
proof (prove)
using this:
e = throw x
es = es'
P \<turnstile> \<langle>throw x # es,s\<rangle> [\<Rightarrow>] \<langle>Throw a # es,s'\<rangle>
vs = []
e' = Throw a

goal (1 subgoal):
 1. P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>

goal (1 subgoal):
 1. \<And>a list. vs = a # list \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. vs = a # list \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
case (Cons v vs')
[PROOF STATE]
proof (state)
this:
vs = v # vs'

goal (1 subgoal):
 1. \<And>a list. vs = a # list \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
have vs: "vs = v # vs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vs = v # vs'
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
vs = v # vs'

goal (1 subgoal):
 1. \<And>a list. vs = a # list \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
with e_es
[PROOF STATE]
proof (chain)
picking this:
e # es = map Val vs @ throw x # es'
vs = v # vs'
[PROOF STEP]
obtain
          e: "e=Val v" and es:"es= map Val vs' @ throw x # es'"
[PROOF STATE]
proof (prove)
using this:
e # es = map Val vs @ throw x # es'
vs = v # vs'

goal (1 subgoal):
 1. (\<lbrakk>e = Val v; es = map Val vs' @ throw x # es'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
e = Val v
es = map Val vs' @ throw x # es'

goal (1 subgoal):
 1. \<And>a list. vs = a # list \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
from e
[PROOF STATE]
proof (chain)
picking this:
e = Val v
[PROOF STEP]
have "P \<turnstile> \<langle>e,s\<rangle> \<Rightarrow> \<langle>Val v,s\<rangle>"
[PROOF STATE]
proof (prove)
using this:
e = Val v

goal (1 subgoal):
 1. P \<turnstile> \<langle>e,s\<rangle> \<Rightarrow> \<langle>Val v,s\<rangle>
[PROOF STEP]
by (iprover intro: eval_evals.Val)
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<langle>e,s\<rangle> \<Rightarrow> \<langle>Val v,s\<rangle>

goal (1 subgoal):
 1. \<And>a list. vs = a # list \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<langle>e,s\<rangle> \<Rightarrow> \<langle>Val v,s\<rangle>

goal (1 subgoal):
 1. \<And>a list. vs = a # list \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
from es
[PROOF STATE]
proof (chain)
picking this:
es = map Val vs' @ throw x # es'
[PROOF STEP]
have "P \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs' @ e' # es',s'\<rangle>"
[PROOF STATE]
proof (prove)
using this:
es = map Val vs' @ throw x # es'

goal (1 subgoal):
 1. P \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs' @ e' # es',s'\<rangle>
[PROOF STEP]
by (rule Cons.hyps)
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs' @ e' # es',s'\<rangle>

goal (1 subgoal):
 1. \<And>a list. vs = a # list \<Longrightarrow> P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> \<langle>e,s\<rangle> \<Rightarrow> \<langle>Val v,s\<rangle>
P \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs' @ e' # es',s'\<rangle>
[PROOF STEP]
show
          "P \<turnstile> \<langle>e#es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> \<langle>e,s\<rangle> \<Rightarrow> \<langle>Val v,s\<rangle>
P \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs' @ e' # es',s'\<rangle>

goal (1 subgoal):
 1. P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
using vs
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> \<langle>e,s\<rangle> \<Rightarrow> \<langle>Val v,s\<rangle>
P \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs' @ e' # es',s'\<rangle>
vs = v # vs'

goal (1 subgoal):
 1. P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
by (auto intro: eval_evals.Cons)
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<langle>e # es,s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
es = map Val ?vs @ throw x # es' \<Longrightarrow> P \<turnstile> \<langle>es,s\<rangle> [\<Rightarrow>] \<langle>map Val ?vs @ e' # es',s'\<rangle>

goal (1 subgoal):
 1. P \<turnstile> \<langle>map Val vs @ throw x # es',s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?es3 = map Val ?vs @ throw x # es' \<Longrightarrow> P \<turnstile> \<langle>?es3,s\<rangle> [\<Rightarrow>] \<langle>map Val ?vs @ e' # es',s'\<rangle>

goal (1 subgoal):
 1. P \<turnstile> \<langle>map Val vs @ throw x # es',s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?es3 = map Val ?vs @ throw x # es' \<Longrightarrow> P \<turnstile> \<langle>?es3,s\<rangle> [\<Rightarrow>] \<langle>map Val ?vs @ e' # es',s'\<rangle>

goal (1 subgoal):
 1. P \<turnstile> \<langle>map Val vs @ throw x # es',s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<langle>map Val vs @ throw x # es',s\<rangle> [\<Rightarrow>] \<langle>map Val vs @ e' # es',s'\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed
(*>*)

\<comment> \<open> separate evaluation of first subexp of a sequence \<close>


[STATEMENT]
lemma bot_annirr'' [simp]: "x \<cdot> \<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<cdot> \<bottom> = \<bottom>
[PROOF STEP]
using Sup_distl[where Y="{}"]
[PROOF STATE]
proof (prove)
using this:
?x \<cdot> Sup {} = Sup {z. \<exists>y\<in>{}. z = ?x \<cdot> y}

goal (1 subgoal):
 1. x \<cdot> \<bottom> = \<bottom>
[PROOF STEP]
by auto


[STATEMENT]
lemma apply_guards_append:
  "apply_guards (a@a') s = (apply_guards a s \<and> apply_guards a' s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_guards (a @ a') s = (apply_guards a s \<and> apply_guards a' s)
[PROOF STEP]
using apply_guards_def
[PROOF STATE]
proof (prove)
using this:
apply_guards ?G ?s = (\<forall>g\<in>set (map (\<lambda>g. gval g ?s) ?G). g = true)

goal (1 subgoal):
 1. apply_guards (a @ a') s = (apply_guards a s \<and> apply_guards a' s)
[PROOF STEP]
by auto


[STATEMENT]
lemma lconf_empty[iff]: "P,h \<turnstile> Map.empty (:\<le>)\<^sub>w E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,h \<turnstile> Map.empty (:\<le>)\<^sub>w E
[PROOF STEP]
by(simp add:lconf_def)


[STATEMENT]
lemma flrestriction_vempty[simp]: "0 \<restriction>\<^sup>l\<^sub>\<bullet> A = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. []\<^sub>\<circ> \<restriction>\<^sup>l\<^sub>\<bullet> A = []\<^sub>\<circ>
[PROOF STEP]
by auto


[STATEMENT]
lemma fdomainI[intro]:
  assumes "[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> r"
  shows "a \<in>\<^sub>\<circ> \<D>\<^sub>\<bullet> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<D>\<^sub>\<bullet> r
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> r

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<D>\<^sub>\<bullet> r
[PROOF STEP]
unfolding fdomain_def
[PROOF STATE]
proof (prove)
using this:
[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> r

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> set {a. \<exists>b. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> r}
[PROOF STEP]
by auto


[STATEMENT]
lemma echelon_form_JNF_imp_upper_triangular:
  assumes eA: "echelon_form_JNF A"
  shows "upper_triangular' A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upper_triangular' A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < dim_col A; j < i; i < dim_row A\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < dim_col A; j < i; i < dim_row A\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
assume ji: "j<i" and i: "i<dim_row A" and j: "j<dim_col A"
[PROOF STATE]
proof (state)
this:
j < i
i < dim_row A
j < dim_col A

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < dim_col A; j < i; i < dim_row A\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
have A: "A \<in> carrier_mat (dim_row A) (dim_col A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in> carrier_mat (dim_row A) (dim_col A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<in> carrier_mat (dim_row A) (dim_col A)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < dim_col A; j < i; i < dim_row A\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
show "A $$ (i,j) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (i, j) = (0::'a)
[PROOF STEP]
proof (cases "is_zero_row_JNF i A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_zero_row_JNF i A \<Longrightarrow> A $$ (i, j) = (0::'a)
 2. \<not> is_zero_row_JNF i A \<Longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_JNF i A

goal (2 subgoals):
 1. is_zero_row_JNF i A \<Longrightarrow> A $$ (i, j) = (0::'a)
 2. \<not> is_zero_row_JNF i A \<Longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
have "i\<le> (LEAST n. A $$(i,n) \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> (LEAST n. A $$ (i, n) \<noteq> (0::'a))
[PROOF STEP]
by (rule echelon_form_JNF_least_position_ge_diagonal[OF eA A False i])
[PROOF STATE]
proof (state)
this:
i \<le> (LEAST n. A $$ (i, n) \<noteq> (0::'a))

goal (2 subgoals):
 1. is_zero_row_JNF i A \<Longrightarrow> A $$ (i, j) = (0::'a)
 2. \<not> is_zero_row_JNF i A \<Longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<le> (LEAST n. A $$ (i, n) \<noteq> (0::'a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<le> (LEAST n. A $$ (i, n) \<noteq> (0::'a))

goal (1 subgoal):
 1. A $$ (i, j) = (0::'a)
[PROOF STEP]
using ji not_less_Least order.strict_trans2
[PROOF STATE]
proof (prove)
using this:
i \<le> (LEAST n. A $$ (i, n) \<noteq> (0::'a))
j < i
?k < (LEAST x. ?P x) \<Longrightarrow> \<not> ?P ?k
\<lbrakk>?a < ?b; ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?a < ?c

goal (1 subgoal):
 1. A $$ (i, j) = (0::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A $$ (i, j) = (0::'a)

goal (1 subgoal):
 1. is_zero_row_JNF i A \<Longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_zero_row_JNF i A \<Longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
is_zero_row_JNF i A

goal (1 subgoal):
 1. is_zero_row_JNF i A \<Longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_zero_row_JNF i A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_zero_row_JNF i A

goal (1 subgoal):
 1. A $$ (i, j) = (0::'a)
[PROOF STEP]
unfolding is_zero_row_JNF_def
[PROOF STATE]
proof (prove)
using this:
\<forall>j<dim_col A. A $$ (i, j) = (0::'a)

goal (1 subgoal):
 1. A $$ (i, j) = (0::'a)
[PROOF STEP]
using j
[PROOF STATE]
proof (prove)
using this:
\<forall>j<dim_col A. A $$ (i, j) = (0::'a)
j < dim_col A

goal (1 subgoal):
 1. A $$ (i, j) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A $$ (i, j) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A $$ (i, j) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_restricted_swap_inputs:
  "not_restricted (I x1a) G \<Longrightarrow>
   apply_guards G (join_ir i r) \<Longrightarrow>
   apply_guards G (join_ir (i[x1a := x1]) r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>not_restricted (I x1a) G; apply_guards G (join_ir i r)\<rbrakk> \<Longrightarrow> apply_guards G (join_ir (i[x1a := x1]) r)
[PROOF STEP]
proof(induct G)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>not_restricted (I x1a) []; apply_guards [] (join_ir i r)\<rbrakk> \<Longrightarrow> apply_guards [] (join_ir (i[x1a := x1]) r)
 2. \<And>a G. \<lbrakk>\<lbrakk>not_restricted (I x1a) G; apply_guards G (join_ir i r)\<rbrakk> \<Longrightarrow> apply_guards G (join_ir (i[x1a := x1]) r); not_restricted (I x1a) (a # G); apply_guards (a # G) (join_ir i r)\<rbrakk> \<Longrightarrow> apply_guards (a # G) (join_ir (i[x1a := x1]) r)
[PROOF STEP]
case (Cons a G)
[PROOF STATE]
proof (state)
this:
\<lbrakk>not_restricted (I x1a) G; apply_guards G (join_ir i r)\<rbrakk> \<Longrightarrow> apply_guards G (join_ir (i[x1a := x1]) r)
not_restricted (I x1a) (a # G)
apply_guards (a # G) (join_ir i r)

goal (2 subgoals):
 1. \<lbrakk>not_restricted (I x1a) []; apply_guards [] (join_ir i r)\<rbrakk> \<Longrightarrow> apply_guards [] (join_ir (i[x1a := x1]) r)
 2. \<And>a G. \<lbrakk>\<lbrakk>not_restricted (I x1a) G; apply_guards G (join_ir i r)\<rbrakk> \<Longrightarrow> apply_guards G (join_ir (i[x1a := x1]) r); not_restricted (I x1a) (a # G); apply_guards (a # G) (join_ir i r)\<rbrakk> \<Longrightarrow> apply_guards (a # G) (join_ir (i[x1a := x1]) r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>not_restricted (I x1a) G; apply_guards G (join_ir i r)\<rbrakk> \<Longrightarrow> apply_guards G (join_ir (i[x1a := x1]) r)
not_restricted (I x1a) (a # G)
apply_guards (a # G) (join_ir i r)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>not_restricted (I x1a) G; apply_guards G (join_ir i r)\<rbrakk> \<Longrightarrow> apply_guards G (join_ir (i[x1a := x1]) r)
not_restricted (I x1a) (a # G)
apply_guards (a # G) (join_ir i r)

goal (1 subgoal):
 1. apply_guards (a # G) (join_ir (i[x1a := x1]) r)
[PROOF STEP]
apply (simp add: apply_guards_cons not_restricted_cons)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>apply_guards G (join_ir (i[x1a := x1]) r); \<not> gexp_constrains a (V (I x1a)) \<and> not_restricted (I x1a) G; gval a (join_ir i r) = true \<and> apply_guards G (join_ir i r)\<rbrakk> \<Longrightarrow> gval a (join_ir (i[x1a := x1]) r) = true
[PROOF STEP]
using input_not_constrained_gval_swap_inputs
[PROOF STATE]
proof (prove)
using this:
\<not> gexp_constrains ?a (V (I ?v)) \<Longrightarrow> gval ?a (join_ir ?i ?c) = gval ?a (join_ir (?i[?v := ?x]) ?c)

goal (1 subgoal):
 1. \<lbrakk>apply_guards G (join_ir (i[x1a := x1]) r); \<not> gexp_constrains a (V (I x1a)) \<and> not_restricted (I x1a) G; gval a (join_ir i r) = true \<and> apply_guards G (join_ir i r)\<rbrakk> \<Longrightarrow> gval a (join_ir (i[x1a := x1]) r) = true
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
apply_guards (a # G) (join_ir (i[x1a := x1]) r)

goal (1 subgoal):
 1. \<lbrakk>not_restricted (I x1a) []; apply_guards [] (join_ir i r)\<rbrakk> \<Longrightarrow> apply_guards [] (join_ir (i[x1a := x1]) r)
[PROOF STEP]
qed auto


[STATEMENT]
lemma part_UN:
assumes "\<And> n. n \<in> N \<Longrightarrow> part (I n) (P n)"
and "\<And> n1 n2. {n1,n2} \<subseteq> N \<and> n1 \<noteq> n2 \<Longrightarrow> I n1 \<inter> I n2 = {}"
shows "part (UN n : N. I n) (UN n : N. P n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. part (\<Union> (I ` N)) (\<Union> (P ` N))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?n \<in> N \<Longrightarrow> part (I ?n) (P ?n)
{?n1.0, ?n2.0} \<subseteq> N \<and> ?n1.0 \<noteq> ?n2.0 \<Longrightarrow> I ?n1.0 \<inter> I ?n2.0 = {}

goal (1 subgoal):
 1. part (\<Union> (I ` N)) (\<Union> (P ` N))
[PROOF STEP]
unfolding part_def
[PROOF STATE]
proof (prove)
using this:
?n \<in> N \<Longrightarrow> \<Union> (P ?n) = I ?n \<and> (\<forall>J1 J2. J1 \<in> P ?n \<and> J2 \<in> P ?n \<and> J1 \<noteq> J2 \<longrightarrow> J1 \<inter> J2 = {})
{?n1.0, ?n2.0} \<subseteq> N \<and> ?n1.0 \<noteq> ?n2.0 \<Longrightarrow> I ?n1.0 \<inter> I ?n2.0 = {}

goal (1 subgoal):
 1. \<Union> (\<Union> (P ` N)) = \<Union> (I ` N) \<and> (\<forall>J1 J2. J1 \<in> \<Union> (P ` N) \<and> J2 \<in> \<Union> (P ` N) \<and> J1 \<noteq> J2 \<longrightarrow> J1 \<inter> J2 = {})
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>\<And>n. n \<in> N \<Longrightarrow> \<Union> (P n) = I n \<and> (\<forall>J1 J2. J1 \<in> P n \<and> J2 \<in> P n \<and> J1 \<noteq> J2 \<longrightarrow> J1 \<inter> J2 = {}); \<And>n1 n2. n1 \<in> N \<and> n2 \<in> N \<and> n1 \<noteq> n2 \<Longrightarrow> I n1 \<inter> I n2 = {}; xa \<in> N; x \<in> I xa\<rbrakk> \<Longrightarrow> \<exists>y\<in>N. \<exists>xa\<in>P y. x \<in> xa
 2. \<And>J1 J2 x xa xb xc. \<lbrakk>\<And>n. n \<in> N \<Longrightarrow> \<Union> (P n) = I n \<and> (\<forall>J1 J2. J1 \<in> P n \<and> J2 \<in> P n \<and> J1 \<noteq> J2 \<longrightarrow> J1 \<inter> J2 = {}); \<And>n1 n2. n1 \<in> N \<and> n2 \<in> N \<and> n1 \<noteq> n2 \<Longrightarrow> I n1 \<inter> I n2 = {}; x \<in> N; J1 \<in> P x; xa \<in> N; J2 \<in> P xa; xb \<in> J1; xb \<notin> J2; xc \<in> J1; xc \<in> J2\<rbrakk> \<Longrightarrow> False
 3. \<And>J1 J2 x xa xb xc. \<lbrakk>\<And>n. n \<in> N \<Longrightarrow> \<Union> (P n) = I n \<and> (\<forall>J1 J2. J1 \<in> P n \<and> J2 \<in> P n \<and> J1 \<noteq> J2 \<longrightarrow> J1 \<inter> J2 = {}); \<And>n1 n2. n1 \<in> N \<and> n2 \<in> N \<and> n1 \<noteq> n2 \<Longrightarrow> I n1 \<inter> I n2 = {}; x \<in> N; J1 \<in> P x; xa \<in> N; J2 \<in> P xa; xb \<in> J2; xb \<notin> J1; xc \<in> J1; xc \<in> J2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis UnionE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>J1 J2 x xa xb xc. \<lbrakk>\<And>n. n \<in> N \<Longrightarrow> \<Union> (P n) = I n \<and> (\<forall>J1 J2. J1 \<in> P n \<and> J2 \<in> P n \<and> J1 \<noteq> J2 \<longrightarrow> J1 \<inter> J2 = {}); \<And>n1 n2. n1 \<in> N \<and> n2 \<in> N \<and> n1 \<noteq> n2 \<Longrightarrow> I n1 \<inter> I n2 = {}; x \<in> N; J1 \<in> P x; xa \<in> N; J2 \<in> P xa; xb \<in> J1; xb \<notin> J2; xc \<in> J1; xc \<in> J2\<rbrakk> \<Longrightarrow> False
 2. \<And>J1 J2 x xa xb xc. \<lbrakk>\<And>n. n \<in> N \<Longrightarrow> \<Union> (P n) = I n \<and> (\<forall>J1 J2. J1 \<in> P n \<and> J2 \<in> P n \<and> J1 \<noteq> J2 \<longrightarrow> J1 \<inter> J2 = {}); \<And>n1 n2. n1 \<in> N \<and> n2 \<in> N \<and> n1 \<noteq> n2 \<Longrightarrow> I n1 \<inter> I n2 = {}; x \<in> N; J1 \<in> P x; xa \<in> N; J2 \<in> P xa; xb \<in> J2; xb \<notin> J1; xc \<in> J1; xc \<in> J2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis Union_upper disjoint_iff_not_equal insert_absorb insert_subset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>J1 J2 x xa xb xc. \<lbrakk>\<And>n. n \<in> N \<Longrightarrow> \<Union> (P n) = I n \<and> (\<forall>J1 J2. J1 \<in> P n \<and> J2 \<in> P n \<and> J1 \<noteq> J2 \<longrightarrow> J1 \<inter> J2 = {}); \<And>n1 n2. n1 \<in> N \<and> n2 \<in> N \<and> n1 \<noteq> n2 \<Longrightarrow> I n1 \<inter> I n2 = {}; x \<in> N; J1 \<in> P x; xa \<in> N; J2 \<in> P xa; xb \<in> J2; xb \<notin> J1; xc \<in> J1; xc \<in> J2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (metis UnionI disjoint_iff_not_equal)


[STATEMENT]
lemma norm_pre:
  "inner_prod ket_pre ket_pre = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inner_prod ket_pre ket_pre = 1
[PROOF STEP]
unfolding ket_pre_def scalar_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<dim_vec (conjugate (Matrix.vec N (\<lambda>k. if k = 0 then 1 else 0))). Matrix.vec N (\<lambda>k. if k = 0 then 1 else 0) $ i * conjugate (Matrix.vec N (\<lambda>k. if k = 0 then 1 else 0)) $ i) = 1
[PROOF STEP]
using sum_only_one_neq_0[of "{0..<N}" 0 "\<lambda>i. (if i = 0 then 1 else 0) * cnj (if i = 0 then 1 else 0)"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite {0..<N}; 0 \<in> {0..<N}; \<And>i. \<lbrakk>i \<in> {0..<N}; i \<noteq> 0\<rbrakk> \<Longrightarrow> (if i = 0 then 1 else 0) * cnj (if i = 0 then 1 else 0) = 0\<rbrakk> \<Longrightarrow> (\<Sum>i = 0..<N. (if i = 0 then 1 else 0) * cnj (if i = 0 then 1 else 0)) = (if 0 = 0 then 1 else 0) * cnj (if 0 = 0 then 1 else 0)

goal (1 subgoal):
 1. (\<Sum>i = 0..<dim_vec (conjugate (Matrix.vec N (\<lambda>k. if k = 0 then 1 else 0))). Matrix.vec N (\<lambda>k. if k = 0 then 1 else 0) $ i * conjugate (Matrix.vec N (\<lambda>k. if k = 0 then 1 else 0)) $ i) = 1
[PROOF STEP]
by auto


[STATEMENT]
lemma fpxs_val_minus_commute: "fpxs_val (f - g) = fpxs_val (g - f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fpxs_val (f - g) = fpxs_val (g - f)
[PROOF STEP]
by (subst fpxs_val_uminus [symmetric]) (simp del: fpxs_val_uminus)


[STATEMENT]
lemma fpxs_val_power [simp]:
  fixes f :: "'a :: {comm_semiring_1, semiring_no_zero_divisors} fpxs"
  assumes "f \<noteq> 0 \<or> n > 0"
  shows "fpxs_val (f ^ n) = of_nat n * fpxs_val f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fpxs_val (f ^ n) = rat_of_nat n * fpxs_val f
[PROOF STEP]
proof (cases "f = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f = 0 \<Longrightarrow> fpxs_val (f ^ n) = rat_of_nat n * fpxs_val f
 2. f \<noteq> 0 \<Longrightarrow> fpxs_val (f ^ n) = rat_of_nat n * fpxs_val f
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
f \<noteq> 0

goal (2 subgoals):
 1. f = 0 \<Longrightarrow> fpxs_val (f ^ n) = rat_of_nat n * fpxs_val f
 2. f \<noteq> 0 \<Longrightarrow> fpxs_val (f ^ n) = rat_of_nat n * fpxs_val f
[PROOF STEP]
have [simp]: "f ^ n \<noteq> 0" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ^ n \<noteq> 0
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
f \<noteq> 0

goal (1 subgoal):
 1. f ^ n \<noteq> 0
[PROOF STEP]
by (induction n) auto
[PROOF STATE]
proof (state)
this:
f ^ ?n \<noteq> 0

goal (2 subgoals):
 1. f = 0 \<Longrightarrow> fpxs_val (f ^ n) = rat_of_nat n * fpxs_val f
 2. f \<noteq> 0 \<Longrightarrow> fpxs_val (f ^ n) = rat_of_nat n * fpxs_val f
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
f ^ ?n \<noteq> 0

goal (1 subgoal):
 1. fpxs_val (f ^ n) = rat_of_nat n * fpxs_val f
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
f ^ ?n \<noteq> 0
f \<noteq> 0

goal (1 subgoal):
 1. fpxs_val (f ^ n) = rat_of_nat n * fpxs_val f
[PROOF STEP]
by (induction n) (auto simp: algebra_simps)
[PROOF STATE]
proof (state)
this:
fpxs_val (f ^ n) = rat_of_nat n * fpxs_val f

goal (1 subgoal):
 1. f = 0 \<Longrightarrow> fpxs_val (f ^ n) = rat_of_nat n * fpxs_val f
[PROOF STEP]
qed (use assms in \<open>auto simp: power_0_left\<close>)


[STATEMENT]
lemma fpxs_X_power_mult: "fpxs_X_power (rat_of_nat n * m) = fpxs_X_power m ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fpxs_X_power (rat_of_nat n * m) = fpxs_X_power m ^ n
[PROOF STEP]
by (induction n) (auto simp: ring_distribs fpxs_X_power_add)


[STATEMENT]
lemma d_IN_h_source [simp]: "d_IN (h_diff i) (source \<Delta>) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_IN (h_diff i) (source \<Delta>) = 0
[PROOF STEP]
by(simp add: d_IN_def h_diff_def cong del: if_weak_cong)


[STATEMENT]
theorem Theorem_1:
  shows "\<not>(mechanism_stable ds \<phi> \<and> nonbossy ds \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (Bossy''.mechanism_stable ds \<phi> \<and> Bossy''.nonbossy ds \<phi>)
[PROOF STEP]
proof(rule notI, erule conjE)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Bossy''.mechanism_stable ds \<phi>; Bossy''.nonbossy ds \<phi>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume S: "Bossy.mechanism_stable ds \<phi>"
[PROOF STATE]
proof (state)
this:
Bossy''.mechanism_stable ds \<phi>

goal (1 subgoal):
 1. \<lbrakk>Bossy''.mechanism_stable ds \<phi>; Bossy''.nonbossy ds \<phi>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume NB: "Bossy.nonbossy ds \<phi>"
[PROOF STATE]
proof (state)
this:
Bossy''.nonbossy ds \<phi>

goal (1 subgoal):
 1. \<lbrakk>Bossy''.mechanism_stable ds \<phi>; Bossy''.nonbossy ds \<phi>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from S Bossy'_stable BPd'_BCh_mechanism_domain
[PROOF STATE]
proof (chain)
picking this:
Bossy''.mechanism_stable ds \<phi>
Bossy'.stable_on ds ?X = (?X = {d1h3, d3h1} \<or> ?X = {d1h1, d3h3})
ContractsWithBilateralSubstitutesAndIRC Xd Xh BPd' BCh
[PROOF STEP]
consider (A) "\<phi> BPd' BCh ds = {d1h3, d3h1}" | (B) "\<phi> BPd' BCh ds = {d1h1, d3h3}"
[PROOF STATE]
proof (prove)
using this:
Bossy''.mechanism_stable ds \<phi>
Bossy'.stable_on ds ?X = (?X = {d1h3, d3h1} \<or> ?X = {d1h1, d3h3})
ContractsWithBilateralSubstitutesAndIRC Xd Xh BPd' BCh

goal (1 subgoal):
 1. \<lbrakk>\<phi> BPd' BCh ds = {d1h3, d3h1} \<Longrightarrow> thesis; \<phi> BPd' BCh ds = {d1h1, d3h3} \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding mechanism_stable_def
[PROOF STATE]
proof (prove)
using this:
\<forall>Pd Ch. ContractsWithBilateralSubstitutesAndIRC Xd Xh Pd Ch \<longrightarrow> Contracts.stable_on Pd Ch ds (\<phi> Pd Ch ds)
Bossy'.stable_on ds ?X = (?X = {d1h3, d3h1} \<or> ?X = {d1h1, d3h3})
ContractsWithBilateralSubstitutesAndIRC Xd Xh BPd' BCh

goal (1 subgoal):
 1. \<lbrakk>\<phi> BPd' BCh ds = {d1h3, d3h1} \<Longrightarrow> thesis; \<phi> BPd' BCh ds = {d1h1, d3h3} \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<phi> BPd' BCh ds = {d1h3, d3h1} \<Longrightarrow> ?thesis; \<phi> BPd' BCh ds = {d1h1, d3h3} \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<lbrakk>Bossy''.mechanism_stable ds \<phi>; Bossy''.nonbossy ds \<phi>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<phi> BPd' BCh ds = {d1h3, d3h1} \<Longrightarrow> ?thesis; \<phi> BPd' BCh ds = {d1h1, d3h3} \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<phi> BPd' BCh ds = {d1h3, d3h1} \<Longrightarrow> ?thesis; \<phi> BPd' BCh ds = {d1h1, d3h3} \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. False
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<phi> BPd' BCh ds = {d1h3, d3h1} \<Longrightarrow> False
 2. \<phi> BPd' BCh ds = {d1h1, d3h3} \<Longrightarrow> False
[PROOF STEP]
case A
[PROOF STATE]
proof (state)
this:
\<phi> BPd' BCh ds = {d1h3, d3h1}

goal (2 subgoals):
 1. \<phi> BPd' BCh ds = {d1h3, d3h1} \<Longrightarrow> False
 2. \<phi> BPd' BCh ds = {d1h1, d3h3} \<Longrightarrow> False
[PROOF STEP]
from S BPd_BCh_mechanism_domain Bossy_stable
[PROOF STATE]
proof (chain)
picking this:
Bossy''.mechanism_stable ds \<phi>
ContractsWithBilateralSubstitutesAndIRC Xd Xh BPd BCh
Bossy.stable_on ds ?X = (?X = {d1h1, d3h3})
[PROOF STEP]
have "\<phi> BPd BCh ds = {d1h1, d3h3}"
[PROOF STATE]
proof (prove)
using this:
Bossy''.mechanism_stable ds \<phi>
ContractsWithBilateralSubstitutesAndIRC Xd Xh BPd BCh
Bossy.stable_on ds ?X = (?X = {d1h1, d3h3})

goal (1 subgoal):
 1. \<phi> BPd BCh ds = {d1h1, d3h3}
[PROOF STEP]
unfolding mechanism_stable_def
[PROOF STATE]
proof (prove)
using this:
\<forall>Pd Ch. ContractsWithBilateralSubstitutesAndIRC Xd Xh Pd Ch \<longrightarrow> Contracts.stable_on Pd Ch ds (\<phi> Pd Ch ds)
ContractsWithBilateralSubstitutesAndIRC Xd Xh BPd BCh
Bossy.stable_on ds ?X = (?X = {d1h1, d3h3})

goal (1 subgoal):
 1. \<phi> BPd BCh ds = {d1h1, d3h3}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<phi> BPd BCh ds = {d1h1, d3h3}

goal (2 subgoals):
 1. \<phi> BPd' BCh ds = {d1h3, d3h1} \<Longrightarrow> False
 2. \<phi> BPd' BCh ds = {d1h1, d3h3} \<Longrightarrow> False
[PROOF STEP]
with Xd_xs ds xs dset A
[PROOF STATE]
proof (chain)
picking this:
Xd ` {d1h2, d1h3} = {Xd d1h1}
Xd ` {d2h2, d2h3} = {Xd d2h1}
Xd ` {d3h2, d3h3} = {Xd d3h1}
distinct [Xd d1h1, Xd d2h1, Xd d3h1]
distinct [d1h1, d1h2, d1h3, d2h1, d2h2, d2h3, d3h1, d3h2, d3h3]
{Xd d1h1, Xd d2h1, Xd d3h1} \<subseteq> ds
\<phi> BPd' BCh ds = {d1h3, d3h1}
\<phi> BPd BCh ds = {d1h1, d3h3}
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
Xd ` {d1h2, d1h3} = {Xd d1h1}
Xd ` {d2h2, d2h3} = {Xd d2h1}
Xd ` {d3h2, d3h3} = {Xd d3h1}
distinct [Xd d1h1, Xd d2h1, Xd d3h1]
distinct [d1h1, d1h2, d1h3, d2h1, d2h2, d2h3, d3h1, d3h2, d3h3]
{Xd d1h1, Xd d2h1, Xd d3h1} \<subseteq> ds
\<phi> BPd' BCh ds = {d1h3, d3h1}
\<phi> BPd BCh ds = {d1h1, d3h3}

goal (1 subgoal):
 1. False
[PROOF STEP]
using nonbossy_Pd[OF NB BPd_BCh_mechanism_domain BPd'_BCh_mechanism_domain[unfolded BPd'_def]]
[PROOF STATE]
proof (prove)
using this:
Xd ` {d1h2, d1h3} = {Xd d1h1}
Xd ` {d2h2, d2h3} = {Xd d2h1}
Xd ` {d3h2, d3h3} = {Xd d3h1}
distinct [Xd d1h1, Xd d2h1, Xd d3h1]
distinct [d1h1, d1h2, d1h3, d2h1, d2h2, d2h3, d3h1, d3h2, d3h3]
{Xd d1h1, Xd d2h1, Xd d3h1} \<subseteq> ds
\<phi> BPd' BCh ds = {d1h3, d3h1}
\<phi> BPd BCh ds = {d1h1, d3h3}
\<lbrakk>Bossy''.dX (\<phi> BPd BCh ds) (Xd d2h1) = Bossy''.dX (\<phi> (BPd(Xd d2h1 := {})) BCh ds) (Xd d2h1); Xd d2h1 \<in> ds\<rbrakk> \<Longrightarrow> \<phi> BPd BCh ds = \<phi> (BPd(Xd d2h1 := {})) BCh ds

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding BPd'_def[symmetric] dX_def
[PROOF STATE]
proof (prove)
using this:
Xd ` {d1h2, d1h3} = {Xd d1h1}
Xd ` {d2h2, d2h3} = {Xd d2h1}
Xd ` {d3h2, d3h3} = {Xd d3h1}
distinct [Xd d1h1, Xd d2h1, Xd d3h1]
distinct [d1h1, d1h2, d1h3, d2h1, d2h2, d2h3, d3h1, d3h2, d3h3]
{Xd d1h1, Xd d2h1, Xd d3h1} \<subseteq> ds
\<phi> BPd' BCh ds = {d1h3, d3h1}
\<phi> BPd BCh ds = {d1h1, d3h3}
\<lbrakk>{x \<in> \<phi> BPd BCh ds. Xd x = Xd d2h1} = {x \<in> \<phi> BPd' BCh ds. Xd x = Xd d2h1}; Xd d2h1 \<in> ds\<rbrakk> \<Longrightarrow> \<phi> BPd BCh ds = \<phi> BPd' BCh ds

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

goal (1 subgoal):
 1. \<phi> BPd' BCh ds = {d1h1, d3h3} \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi> BPd' BCh ds = {d1h1, d3h3} \<Longrightarrow> False
[PROOF STEP]
case B
[PROOF STATE]
proof (state)
this:
\<phi> BPd' BCh ds = {d1h1, d3h3}

goal (1 subgoal):
 1. \<phi> BPd' BCh ds = {d1h1, d3h3} \<Longrightarrow> False
[PROOF STEP]
from S BPd'_BCh'_mechanism_domain Bossy''_stable
[PROOF STATE]
proof (chain)
picking this:
Bossy''.mechanism_stable ds \<phi>
ContractsWithBilateralSubstitutesAndIRC Xd Xh BPd' BCh'
Bossy''.stable_on ds ?X = (?X = {d3h1, d1h3})
[PROOF STEP]
have "\<phi> BPd' BCh' ds = {d3h1, d1h3}"
[PROOF STATE]
proof (prove)
using this:
Bossy''.mechanism_stable ds \<phi>
ContractsWithBilateralSubstitutesAndIRC Xd Xh BPd' BCh'
Bossy''.stable_on ds ?X = (?X = {d3h1, d1h3})

goal (1 subgoal):
 1. \<phi> BPd' BCh' ds = {d3h1, d1h3}
[PROOF STEP]
unfolding mechanism_stable_def
[PROOF STATE]
proof (prove)
using this:
\<forall>Pd Ch. ContractsWithBilateralSubstitutesAndIRC Xd Xh Pd Ch \<longrightarrow> Contracts.stable_on Pd Ch ds (\<phi> Pd Ch ds)
ContractsWithBilateralSubstitutesAndIRC Xd Xh BPd' BCh'
Bossy''.stable_on ds ?X = (?X = {d3h1, d1h3})

goal (1 subgoal):
 1. \<phi> BPd' BCh' ds = {d3h1, d1h3}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<phi> BPd' BCh' ds = {d3h1, d1h3}

goal (1 subgoal):
 1. \<phi> BPd' BCh ds = {d1h1, d3h3} \<Longrightarrow> False
[PROOF STEP]
with Xh_xs hs xs dset B
[PROOF STATE]
proof (chain)
picking this:
Xh ` {d2h1, d3h1} = {Xh d1h1}
Xh ` {d2h2, d3h2} = {Xh d1h2}
Xh ` {d2h3, d3h3} = {Xh d1h3}
distinct [Xh d1h1, Xh d1h2, Xh d1h3]
distinct [d1h1, d1h2, d1h3, d2h1, d2h2, d2h3, d3h1, d3h2, d3h3]
{Xd d1h1, Xd d2h1, Xd d3h1} \<subseteq> ds
\<phi> BPd' BCh ds = {d1h1, d3h3}
\<phi> BPd' BCh' ds = {d3h1, d1h3}
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
Xh ` {d2h1, d3h1} = {Xh d1h1}
Xh ` {d2h2, d3h2} = {Xh d1h2}
Xh ` {d2h3, d3h3} = {Xh d1h3}
distinct [Xh d1h1, Xh d1h2, Xh d1h3]
distinct [d1h1, d1h2, d1h3, d2h1, d2h2, d2h3, d3h1, d3h2, d3h3]
{Xd d1h1, Xd d2h1, Xd d3h1} \<subseteq> ds
\<phi> BPd' BCh ds = {d1h1, d3h3}
\<phi> BPd' BCh' ds = {d3h1, d1h3}

goal (1 subgoal):
 1. False
[PROOF STEP]
using nonbossy_Ch[OF NB BPd'_BCh_mechanism_domain BPd'_BCh'_mechanism_domain[unfolded BCh'_def]]
[PROOF STATE]
proof (prove)
using this:
Xh ` {d2h1, d3h1} = {Xh d1h1}
Xh ` {d2h2, d3h2} = {Xh d1h2}
Xh ` {d2h3, d3h3} = {Xh d1h3}
distinct [Xh d1h1, Xh d1h2, Xh d1h3]
distinct [d1h1, d1h2, d1h3, d2h1, d2h2, d2h3, d3h1, d3h2, d3h3]
{Xd d1h1, Xd d2h1, Xd d3h1} \<subseteq> ds
\<phi> BPd' BCh ds = {d1h1, d3h3}
\<phi> BPd' BCh' ds = {d3h1, d1h3}
Bossy''.hX (\<phi> BPd' BCh ds) (Xh d1h2) = Bossy''.hX (\<phi> BPd' (BCh(Xh d1h2 := \<lambda>X. set_option (find (\<lambda>x. x \<in> X) [d1h2, d2h2, d3h2]))) ds) (Xh d1h2) \<Longrightarrow> \<phi> BPd' BCh ds = \<phi> BPd' (BCh(Xh d1h2 := \<lambda>X. set_option (find (\<lambda>x. x \<in> X) [d1h2, d2h2, d3h2]))) ds

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding BCh'_def[symmetric] hX_def
[PROOF STATE]
proof (prove)
using this:
Xh ` {d2h1, d3h1} = {Xh d1h1}
Xh ` {d2h2, d3h2} = {Xh d1h2}
Xh ` {d2h3, d3h3} = {Xh d1h3}
distinct [Xh d1h1, Xh d1h2, Xh d1h3]
distinct [d1h1, d1h2, d1h3, d2h1, d2h2, d2h3, d3h1, d3h2, d3h3]
{Xd d1h1, Xd d2h1, Xd d3h1} \<subseteq> ds
\<phi> BPd' BCh ds = {d1h1, d3h3}
\<phi> BPd' BCh' ds = {d3h1, d1h3}
{x \<in> \<phi> BPd' BCh ds. Xh x = Xh d1h2} = {x \<in> \<phi> BPd' BCh' ds. Xh x = Xh d1h2} \<Longrightarrow> \<phi> BPd' BCh ds = \<phi> BPd' BCh' ds

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqvtChainEq:
  fixes P    :: pi
  and   P'   :: pi
  and   perm :: "name prm"

  shows   "P \<Longrightarrow>\<^sub>\<tau> P' = (perm \<bullet> P) \<Longrightarrow>\<^sub>\<tau> (perm \<bullet> P')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>\<tau> P' = perm \<bullet> P \<Longrightarrow>\<^sub>\<tau> perm \<bullet> P'
[PROOF STEP]
by(blast intro: eqvtChainE eqvtChainI)


[STATEMENT]
lemma weakBisimScopeExtChainSym:
  fixes xvec :: "name list"
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"

  assumes "xvec \<sharp>* \<Psi>"
  and     "xvec \<sharp>* Q"

  shows "\<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>(P \<parallel> Q) \<approx> (\<lparr>\<nu>*xvec\<rparr>P) \<parallel> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<parallel> Q \<approx> (\<lparr>\<nu>*xvec\<rparr>P) \<parallel> Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xvec \<sharp>* \<Psi>
xvec \<sharp>* Q

goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<parallel> Q \<approx> (\<lparr>\<nu>*xvec\<rparr>P) \<parallel> Q
[PROOF STEP]
by(induct xvec) (auto intro: weakBisimScopeExtSym weakBisimReflexive weakBisimTransitive weakBisimResPres)


[STATEMENT]
lemma smult_mult2: fixes a :: "'a::comm_ring_1" shows "a *\<^sub>S (A * B) = A * (a *\<^sub>S B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a *\<^sub>S (A * B) = A * a *\<^sub>S B
[PROOF STEP]
by transfer (simp add: sum_distrib_left field_simps)


[STATEMENT]
lemma energy_graph_subsets_commute:
  "energy_graph_subsets U W G = energy_graph_subsets W U G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. energy_graph_subsets U W G = energy_graph_subsets W U G
[PROOF STEP]
by (simp add: energy_graph_subsets_def edge_density_commute)


[STATEMENT]
lemma Ya_ide:
    assumes a': "C.ide a'"
    shows "Y a a' = S.mkIde (Hom.set (a', a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y a a' = S.mkIde (Hom.set (a', a))
[PROOF STEP]
using assms ide_apex Y.Y_simp Hom.map_ide
[PROOF STATE]
proof (prove)
using this:
C.ide a'
C.ide a
C.arr ?f \<Longrightarrow> Y ?f = (\<lambda>g. Hom.map (g, ?f))
\<lbrakk>C.ide ?b; C.ide ?a\<rbrakk> \<Longrightarrow> Hom.map (?b, ?a) = S.mkIde (Hom.set (?b, ?a))

goal (1 subgoal):
 1. Y a a' = S.mkIde (Hom.set (a', a))
[PROOF STEP]
by simp