[STATEMENT]
lemma compatible_refl:
  assumes coms_secure: "list_all com_sifum_secure cmds"
  assumes low_eq: "mem\<^sub>1 =\<^sup>l mem\<^sub>2"
  shows "makes_compatible (add_initial_modes cmds, mem\<^sub>1)
                          (add_initial_modes cmds, mem\<^sub>2)
                          (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. makes_compatible (add_initial_modes cmds, mem\<^sub>1) (add_initial_modes cmds, mem\<^sub>2) (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. makes_compatible (add_initial_modes cmds, mem\<^sub>1) (add_initial_modes cmds, mem\<^sub>2) (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2))
[PROOF STEP]
let ?n = "length cmds"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. makes_compatible (add_initial_modes cmds, mem\<^sub>1) (add_initial_modes cmds, mem\<^sub>2) (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2))
[PROOF STEP]
let ?mems = "replicate ?n (mem\<^sub>1, mem\<^sub>2)" and
      ?mdss = "replicate ?n mds\<^sub>s"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. makes_compatible (add_initial_modes cmds, mem\<^sub>1) (add_initial_modes cmds, mem\<^sub>2) (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2))
[PROOF STEP]
let ?X = "differing_vars_lists mem\<^sub>1 mem\<^sub>2 ?mems"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. makes_compatible (add_initial_modes cmds, mem\<^sub>1) (add_initial_modes cmds, mem\<^sub>2) (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2))
[PROOF STEP]
have diff_empty: "\<forall> i < ?n. ?X i = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<length cmds. differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i = {}
[PROOF STEP]
by (metis differing_vars_initially_empty ex_in_conv min.idem zip_replicate)
[PROOF STATE]
proof (state)
this:
\<forall>i<length cmds. differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i = {}

goal (1 subgoal):
 1. makes_compatible (add_initial_modes cmds, mem\<^sub>1) (add_initial_modes cmds, mem\<^sub>2) (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. makes_compatible (add_initial_modes cmds, mem\<^sub>1) (add_initial_modes cmds, mem\<^sub>2) (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2))
[PROOF STEP]
unfolding add_initial_modes_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. makes_compatible (zip cmds (replicate (length cmds) mds\<^sub>s), mem\<^sub>1) (zip cmds (replicate (length cmds) mds\<^sub>s), mem\<^sub>2) (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. length (zip cmds (replicate (length cmds) mds\<^sub>s)) = length (zip cmds (replicate (length cmds) mds\<^sub>s)) \<and> length (zip cmds (replicate (length cmds) mds\<^sub>s)) = length (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2))
 2. \<And>i \<sigma>. \<lbrakk>i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s)); dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i\<rbrakk> \<Longrightarrow> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, subst \<sigma> (fst (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i))) \<approx> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, subst \<sigma> (snd (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i)))
 3. \<And>i x. \<lbrakk>i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s)); mem\<^sub>1 x = mem\<^sub>2 x \<or> dma x = High\<rbrakk> \<Longrightarrow> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i
 4. length (zip cmds (replicate (length cmds) mds\<^sub>s)) = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<or> (\<forall>x. \<exists>i<length (zip cmds (replicate (length cmds) mds\<^sub>s)). x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i)
[PROOF STEP]
show "length (zip cmds ?mdss) = length (zip cmds ?mdss) \<and> length (zip cmds ?mdss) = length ?mems"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (zip cmds (replicate (length cmds) mds\<^sub>s)) = length (zip cmds (replicate (length cmds) mds\<^sub>s)) \<and> length (zip cmds (replicate (length cmds) mds\<^sub>s)) = length (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (zip cmds (replicate (length cmds) mds\<^sub>s)) = length (zip cmds (replicate (length cmds) mds\<^sub>s)) \<and> length (zip cmds (replicate (length cmds) mds\<^sub>s)) = length (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2))

goal (3 subgoals):
 1. \<And>i \<sigma>. \<lbrakk>i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s)); dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i\<rbrakk> \<Longrightarrow> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, subst \<sigma> (fst (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i))) \<approx> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, subst \<sigma> (snd (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i)))
 2. \<And>i x. \<lbrakk>i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s)); mem\<^sub>1 x = mem\<^sub>2 x \<or> dma x = High\<rbrakk> \<Longrightarrow> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i
 3. length (zip cmds (replicate (length cmds) mds\<^sub>s)) = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<or> (\<forall>x. \<exists>i<length (zip cmds (replicate (length cmds) mds\<^sub>s)). x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i \<sigma>. \<lbrakk>i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s)); dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i\<rbrakk> \<Longrightarrow> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, subst \<sigma> (fst (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i))) \<approx> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, subst \<sigma> (snd (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i)))
 2. \<And>i x. \<lbrakk>i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s)); mem\<^sub>1 x = mem\<^sub>2 x \<or> dma x = High\<rbrakk> \<Longrightarrow> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i
 3. length (zip cmds (replicate (length cmds) mds\<^sub>s)) = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<or> (\<forall>x. \<exists>i<length (zip cmds (replicate (length cmds) mds\<^sub>s)). x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i)
[PROOF STEP]
fix i \<sigma>
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i \<sigma>. \<lbrakk>i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s)); dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i\<rbrakk> \<Longrightarrow> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, subst \<sigma> (fst (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i))) \<approx> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, subst \<sigma> (snd (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i)))
 2. \<And>i x. \<lbrakk>i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s)); mem\<^sub>1 x = mem\<^sub>2 x \<or> dma x = High\<rbrakk> \<Longrightarrow> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i
 3. length (zip cmds (replicate (length cmds) mds\<^sub>s)) = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<or> (\<forall>x. \<exists>i<length (zip cmds (replicate (length cmds) mds\<^sub>s)). x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i)
[PROOF STEP]
let ?mems\<^sub>1i = "fst (?mems ! i)" and ?mems\<^sub>2i = "snd (?mems ! i)"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i \<sigma>. \<lbrakk>i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s)); dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i\<rbrakk> \<Longrightarrow> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, subst \<sigma> (fst (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i))) \<approx> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, subst \<sigma> (snd (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i)))
 2. \<And>i x. \<lbrakk>i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s)); mem\<^sub>1 x = mem\<^sub>2 x \<or> dma x = High\<rbrakk> \<Longrightarrow> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i
 3. length (zip cmds (replicate (length cmds) mds\<^sub>s)) = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<or> (\<forall>x. \<exists>i<length (zip cmds (replicate (length cmds) mds\<^sub>s)). x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i)
[PROOF STEP]
assume i: "i < length (zip cmds ?mdss)"
[PROOF STATE]
proof (state)
this:
i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s))

goal (3 subgoals):
 1. \<And>i \<sigma>. \<lbrakk>i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s)); dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i\<rbrakk> \<Longrightarrow> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, subst \<sigma> (fst (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i))) \<approx> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, subst \<sigma> (snd (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i)))
 2. \<And>i x. \<lbrakk>i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s)); mem\<^sub>1 x = mem\<^sub>2 x \<or> dma x = High\<rbrakk> \<Longrightarrow> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i
 3. length (zip cmds (replicate (length cmds) mds\<^sub>s)) = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<or> (\<forall>x. \<exists>i<length (zip cmds (replicate (length cmds) mds\<^sub>s)). x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i)
[PROOF STEP]
with coms_secure
[PROOF STATE]
proof (chain)
picking this:
list_all com_sifum_secure cmds
i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s))
[PROOF STEP]
have "com_sifum_secure (cmds ! i)"
[PROOF STATE]
proof (prove)
using this:
list_all com_sifum_secure cmds
i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s))

goal (1 subgoal):
 1. com_sifum_secure (cmds ! i)
[PROOF STEP]
using coms_secure
[PROOF STATE]
proof (prove)
using this:
list_all com_sifum_secure cmds
i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s))
list_all com_sifum_secure cmds

goal (1 subgoal):
 1. com_sifum_secure (cmds ! i)
[PROOF STEP]
by (metis length_map length_replicate list_all_length map_snd_zip)
[PROOF STATE]
proof (state)
this:
com_sifum_secure (cmds ! i)

goal (3 subgoals):
 1. \<And>i \<sigma>. \<lbrakk>i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s)); dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i\<rbrakk> \<Longrightarrow> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, subst \<sigma> (fst (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i))) \<approx> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, subst \<sigma> (snd (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i)))
 2. \<And>i x. \<lbrakk>i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s)); mem\<^sub>1 x = mem\<^sub>2 x \<or> dma x = High\<rbrakk> \<Longrightarrow> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i
 3. length (zip cmds (replicate (length cmds) mds\<^sub>s)) = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<or> (\<forall>x. \<exists>i<length (zip cmds (replicate (length cmds) mds\<^sub>s)). x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i)
[PROOF STEP]
with i
[PROOF STATE]
proof (chain)
picking this:
i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s))
com_sifum_secure (cmds ! i)
[PROOF STEP]
have "\<And> mem\<^sub>1 mem\<^sub>2. mem\<^sub>1 =\<^bsub>mds\<^sub>s\<^esub>\<^sup>l mem\<^sub>2 \<Longrightarrow>
      (zip cmds (replicate ?n mds\<^sub>s) ! i, mem\<^sub>1) \<approx> (zip cmds (replicate ?n mds\<^sub>s) ! i, mem\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s))
com_sifum_secure (cmds ! i)

goal (1 subgoal):
 1. \<And>mem\<^sub>1 mem\<^sub>2. mem\<^sub>1 =\<^bsub>mds\<^sub>s\<^esub>\<^sup>l mem\<^sub>2 \<Longrightarrow> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, mem\<^sub>1) \<approx> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, mem\<^sub>2)
[PROOF STEP]
using com_sifum_secure_def low_indistinguishable_def
[PROOF STATE]
proof (prove)
using this:
i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s))
com_sifum_secure (cmds ! i)
com_sifum_secure ?c = ?c \<sim>\<^bsub>mds\<^sub>s\<^esub> ?c
?c\<^sub>1 \<sim>\<^bsub>?mds\<^esub> ?c\<^sub>2 = (\<forall>mem\<^sub>1 mem\<^sub>2. mem\<^sub>1 =\<^bsub>?mds\<^esub>\<^sup>l mem\<^sub>2 \<longrightarrow> \<langle>?c\<^sub>1, ?mds, mem\<^sub>1\<rangle> \<approx> \<langle>?c\<^sub>2, ?mds, mem\<^sub>2\<rangle>)

goal (1 subgoal):
 1. \<And>mem\<^sub>1 mem\<^sub>2. mem\<^sub>1 =\<^bsub>mds\<^sub>s\<^esub>\<^sup>l mem\<^sub>2 \<Longrightarrow> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, mem\<^sub>1) \<approx> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, mem\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?mem\<^sub>15 =\<^bsub>mds\<^sub>s\<^esub>\<^sup>l ?mem\<^sub>25 \<Longrightarrow> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, ?mem\<^sub>15) \<approx> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, ?mem\<^sub>25)

goal (3 subgoals):
 1. \<And>i \<sigma>. \<lbrakk>i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s)); dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i\<rbrakk> \<Longrightarrow> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, subst \<sigma> (fst (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i))) \<approx> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, subst \<sigma> (snd (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i)))
 2. \<And>i x. \<lbrakk>i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s)); mem\<^sub>1 x = mem\<^sub>2 x \<or> dma x = High\<rbrakk> \<Longrightarrow> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i
 3. length (zip cmds (replicate (length cmds) mds\<^sub>s)) = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<or> (\<forall>x. \<exists>i<length (zip cmds (replicate (length cmds) mds\<^sub>s)). x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?mem\<^sub>15 =\<^bsub>mds\<^sub>s\<^esub>\<^sup>l ?mem\<^sub>25 \<Longrightarrow> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, ?mem\<^sub>15) \<approx> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, ?mem\<^sub>25)

goal (3 subgoals):
 1. \<And>i \<sigma>. \<lbrakk>i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s)); dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i\<rbrakk> \<Longrightarrow> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, subst \<sigma> (fst (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i))) \<approx> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, subst \<sigma> (snd (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i)))
 2. \<And>i x. \<lbrakk>i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s)); mem\<^sub>1 x = mem\<^sub>2 x \<or> dma x = High\<rbrakk> \<Longrightarrow> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i
 3. length (zip cmds (replicate (length cmds) mds\<^sub>s)) = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<or> (\<forall>x. \<exists>i<length (zip cmds (replicate (length cmds) mds\<^sub>s)). x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i)
[PROOF STEP]
from i
[PROOF STATE]
proof (chain)
picking this:
i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s))
[PROOF STEP]
have "?mems\<^sub>1i = mem\<^sub>1" "?mems\<^sub>2i = mem\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s))

goal (1 subgoal):
 1. fst (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i) = mem\<^sub>1 &&& snd (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i) = mem\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i) = mem\<^sub>1
snd (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i) = mem\<^sub>2

goal (3 subgoals):
 1. \<And>i \<sigma>. \<lbrakk>i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s)); dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i\<rbrakk> \<Longrightarrow> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, subst \<sigma> (fst (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i))) \<approx> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, subst \<sigma> (snd (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i)))
 2. \<And>i x. \<lbrakk>i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s)); mem\<^sub>1 x = mem\<^sub>2 x \<or> dma x = High\<rbrakk> \<Longrightarrow> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i
 3. length (zip cmds (replicate (length cmds) mds\<^sub>s)) = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<or> (\<forall>x. \<exists>i<length (zip cmds (replicate (length cmds) mds\<^sub>s)). x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i)
[PROOF STEP]
with low_eq
[PROOF STATE]
proof (chain)
picking this:
mem\<^sub>1 =\<^sup>l mem\<^sub>2
fst (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i) = mem\<^sub>1
snd (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i) = mem\<^sub>2
[PROOF STEP]
have "?mems\<^sub>1i [\<mapsto> \<sigma>] =\<^bsub>mds\<^sub>s\<^esub>\<^sup>l ?mems\<^sub>2i [\<mapsto> \<sigma>]"
[PROOF STATE]
proof (prove)
using this:
mem\<^sub>1 =\<^sup>l mem\<^sub>2
fst (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i) = mem\<^sub>1
snd (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i) = mem\<^sub>2

goal (1 subgoal):
 1. subst \<sigma> (fst (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i)) =\<^bsub>mds\<^sub>s\<^esub>\<^sup>l subst \<sigma> (snd (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i))
[PROOF STEP]
by (auto simp: subst_def mds\<^sub>s_def low_mds_eq_def low_eq_def, case_tac "\<sigma> x", auto)
[PROOF STATE]
proof (state)
this:
subst \<sigma> (fst (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i)) =\<^bsub>mds\<^sub>s\<^esub>\<^sup>l subst \<sigma> (snd (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i))

goal (3 subgoals):
 1. \<And>i \<sigma>. \<lbrakk>i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s)); dom \<sigma> = differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i\<rbrakk> \<Longrightarrow> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, subst \<sigma> (fst (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i))) \<approx> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, subst \<sigma> (snd (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i)))
 2. \<And>i x. \<lbrakk>i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s)); mem\<^sub>1 x = mem\<^sub>2 x \<or> dma x = High\<rbrakk> \<Longrightarrow> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i
 3. length (zip cmds (replicate (length cmds) mds\<^sub>s)) = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<or> (\<forall>x. \<exists>i<length (zip cmds (replicate (length cmds) mds\<^sub>s)). x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?mem\<^sub>15 =\<^bsub>mds\<^sub>s\<^esub>\<^sup>l ?mem\<^sub>25 \<Longrightarrow> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, ?mem\<^sub>15) \<approx> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, ?mem\<^sub>25)
subst \<sigma> (fst (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i)) =\<^bsub>mds\<^sub>s\<^esub>\<^sup>l subst \<sigma> (snd (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i))
[PROOF STEP]
show "(zip cmds ?mdss ! i, ?mems\<^sub>1i [\<mapsto> \<sigma>]) \<approx> (zip cmds ?mdss ! i, ?mems\<^sub>2i [\<mapsto> \<sigma>])"
[PROOF STATE]
proof (prove)
using this:
?mem\<^sub>15 =\<^bsub>mds\<^sub>s\<^esub>\<^sup>l ?mem\<^sub>25 \<Longrightarrow> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, ?mem\<^sub>15) \<approx> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, ?mem\<^sub>25)
subst \<sigma> (fst (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i)) =\<^bsub>mds\<^sub>s\<^esub>\<^sup>l subst \<sigma> (snd (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i))

goal (1 subgoal):
 1. (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, subst \<sigma> (fst (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i))) \<approx> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, subst \<sigma> (snd (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(zip cmds (replicate (length cmds) mds\<^sub>s) ! i, subst \<sigma> (fst (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i))) \<approx> (zip cmds (replicate (length cmds) mds\<^sub>s) ! i, subst \<sigma> (snd (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2) ! i)))

goal (2 subgoals):
 1. \<And>i x. \<lbrakk>i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s)); mem\<^sub>1 x = mem\<^sub>2 x \<or> dma x = High\<rbrakk> \<Longrightarrow> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i
 2. length (zip cmds (replicate (length cmds) mds\<^sub>s)) = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<or> (\<forall>x. \<exists>i<length (zip cmds (replicate (length cmds) mds\<^sub>s)). x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i x. \<lbrakk>i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s)); mem\<^sub>1 x = mem\<^sub>2 x \<or> dma x = High\<rbrakk> \<Longrightarrow> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i
 2. length (zip cmds (replicate (length cmds) mds\<^sub>s)) = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<or> (\<forall>x. \<exists>i<length (zip cmds (replicate (length cmds) mds\<^sub>s)). x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i)
[PROOF STEP]
fix i x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i x. \<lbrakk>i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s)); mem\<^sub>1 x = mem\<^sub>2 x \<or> dma x = High\<rbrakk> \<Longrightarrow> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i
 2. length (zip cmds (replicate (length cmds) mds\<^sub>s)) = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<or> (\<forall>x. \<exists>i<length (zip cmds (replicate (length cmds) mds\<^sub>s)). x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i)
[PROOF STEP]
assume "i < length (zip cmds ?mdss)"
[PROOF STATE]
proof (state)
this:
i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s))

goal (2 subgoals):
 1. \<And>i x. \<lbrakk>i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s)); mem\<^sub>1 x = mem\<^sub>2 x \<or> dma x = High\<rbrakk> \<Longrightarrow> x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i
 2. length (zip cmds (replicate (length cmds) mds\<^sub>s)) = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<or> (\<forall>x. \<exists>i<length (zip cmds (replicate (length cmds) mds\<^sub>s)). x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i)
[PROOF STEP]
with diff_empty
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length cmds. differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i = {}
i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s))
[PROOF STEP]
show "x \<notin> ?X i"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length cmds. differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i = {}
i \<sqsubset> length (zip cmds (replicate (length cmds) mds\<^sub>s))

goal (1 subgoal):
 1. x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i

goal (1 subgoal):
 1. length (zip cmds (replicate (length cmds) mds\<^sub>s)) = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<or> (\<forall>x. \<exists>i<length (zip cmds (replicate (length cmds) mds\<^sub>s)). x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (zip cmds (replicate (length cmds) mds\<^sub>s)) = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<or> (\<forall>x. \<exists>i<length (zip cmds (replicate (length cmds) mds\<^sub>s)). x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i)
[PROOF STEP]
show "(length (zip cmds ?mdss) = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2) \<or> (\<forall> x. \<exists> i < length (zip cmds ?mdss). x \<notin> ?X i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (zip cmds (replicate (length cmds) mds\<^sub>s)) = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<or> (\<forall>x. \<exists>i<length (zip cmds (replicate (length cmds) mds\<^sub>s)). x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i)
[PROOF STEP]
using diff_empty
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length cmds. differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i = {}

goal (1 subgoal):
 1. length (zip cmds (replicate (length cmds) mds\<^sub>s)) = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<or> (\<forall>x. \<exists>i<length (zip cmds (replicate (length cmds) mds\<^sub>s)). x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i)
[PROOF STEP]
by (metis bot_less bot_nat_def empty_iff length_zip low_eq min_0L)
[PROOF STATE]
proof (state)
this:
length (zip cmds (replicate (length cmds) mds\<^sub>s)) = 0 \<and> mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<or> (\<forall>x. \<exists>i<length (zip cmds (replicate (length cmds) mds\<^sub>s)). x \<notin> differing_vars_lists mem\<^sub>1 mem\<^sub>2 (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2)) i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
makes_compatible (add_initial_modes cmds, mem\<^sub>1) (add_initial_modes cmds, mem\<^sub>2) (replicate (length cmds) (mem\<^sub>1, mem\<^sub>2))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem sifum_compositionality:
  assumes com_secure: "list_all com_sifum_secure cmds"
  assumes no_assms: "no_assumptions_on_termination cmds"
  assumes sound_modes: "\<forall> mem. sound_mode_use (add_initial_modes cmds, mem)"
  shows "prog_sifum_secure cmds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prog_sifum_secure cmds
[PROOF STEP]
unfolding prog_sifum_secure_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. no_assumptions_on_termination cmds \<and> (\<forall>mem\<^sub>1 mem\<^sub>2. mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<longrightarrow> (\<forall>k cms\<^sub>1' mem\<^sub>1'. (add_initial_modes cmds, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1') \<longrightarrow> (\<exists>cms\<^sub>2' mem\<^sub>2'. (add_initial_modes cmds, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> length cms\<^sub>2' = length cms\<^sub>1' \<and> (\<forall>x. dma x = Low \<and> (\<forall>i<length cms\<^sub>1'. x \<notin> snd (cms\<^sub>1' ! i) AsmNoRead) \<longrightarrow> mem\<^sub>1' x = mem\<^sub>2' x))))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
list_all com_sifum_secure cmds
no_assumptions_on_termination cmds
\<forall>mem. sound_mode_use (add_initial_modes cmds, mem)

goal (1 subgoal):
 1. no_assumptions_on_termination cmds \<and> (\<forall>mem\<^sub>1 mem\<^sub>2. mem\<^sub>1 =\<^sup>l mem\<^sub>2 \<longrightarrow> (\<forall>k cms\<^sub>1' mem\<^sub>1'. (add_initial_modes cmds, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1') \<longrightarrow> (\<exists>cms\<^sub>2' mem\<^sub>2'. (add_initial_modes cmds, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> length cms\<^sub>2' = length cms\<^sub>1' \<and> (\<forall>x. dma x = Low \<and> (\<forall>i<length cms\<^sub>1'. x \<notin> snd (cms\<^sub>1' ! i) AsmNoRead) \<longrightarrow> mem\<^sub>1' x = mem\<^sub>2' x))))
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>mem\<^sub>1 mem\<^sub>2 k cms\<^sub>1' mem\<^sub>1'. \<lbrakk>list_all com_sifum_secure cmds; no_assumptions_on_termination cmds; \<forall>mem. sound_mode_use (add_initial_modes cmds, mem); mem\<^sub>1 =\<^sup>l mem\<^sub>2; (add_initial_modes cmds, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1')\<rbrakk> \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2'. (add_initial_modes cmds, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> length cms\<^sub>2' = length cms\<^sub>1' \<and> (\<forall>x. dma x = Low \<and> (\<forall>i<length cms\<^sub>1'. x \<notin> snd (cms\<^sub>1' ! i) AsmNoRead) \<longrightarrow> mem\<^sub>1' x = mem\<^sub>2' x)
[PROOF STEP]
fix mem\<^sub>1 mem\<^sub>2 :: "'Var \<Rightarrow> 'Val"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>mem\<^sub>1 mem\<^sub>2 k cms\<^sub>1' mem\<^sub>1'. \<lbrakk>list_all com_sifum_secure cmds; no_assumptions_on_termination cmds; \<forall>mem. sound_mode_use (add_initial_modes cmds, mem); mem\<^sub>1 =\<^sup>l mem\<^sub>2; (add_initial_modes cmds, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1')\<rbrakk> \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2'. (add_initial_modes cmds, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> length cms\<^sub>2' = length cms\<^sub>1' \<and> (\<forall>x. dma x = Low \<and> (\<forall>i<length cms\<^sub>1'. x \<notin> snd (cms\<^sub>1' ! i) AsmNoRead) \<longrightarrow> mem\<^sub>1' x = mem\<^sub>2' x)
[PROOF STEP]
fix k cms\<^sub>1' mem\<^sub>1'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>mem\<^sub>1 mem\<^sub>2 k cms\<^sub>1' mem\<^sub>1'. \<lbrakk>list_all com_sifum_secure cmds; no_assumptions_on_termination cmds; \<forall>mem. sound_mode_use (add_initial_modes cmds, mem); mem\<^sub>1 =\<^sup>l mem\<^sub>2; (add_initial_modes cmds, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1')\<rbrakk> \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2'. (add_initial_modes cmds, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> length cms\<^sub>2' = length cms\<^sub>1' \<and> (\<forall>x. dma x = Low \<and> (\<forall>i<length cms\<^sub>1'. x \<notin> snd (cms\<^sub>1' ! i) AsmNoRead) \<longrightarrow> mem\<^sub>1' x = mem\<^sub>2' x)
[PROOF STEP]
let ?n = "length cmds"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>mem\<^sub>1 mem\<^sub>2 k cms\<^sub>1' mem\<^sub>1'. \<lbrakk>list_all com_sifum_secure cmds; no_assumptions_on_termination cmds; \<forall>mem. sound_mode_use (add_initial_modes cmds, mem); mem\<^sub>1 =\<^sup>l mem\<^sub>2; (add_initial_modes cmds, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1')\<rbrakk> \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2'. (add_initial_modes cmds, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> length cms\<^sub>2' = length cms\<^sub>1' \<and> (\<forall>x. dma x = Low \<and> (\<forall>i<length cms\<^sub>1'. x \<notin> snd (cms\<^sub>1' ! i) AsmNoRead) \<longrightarrow> mem\<^sub>1' x = mem\<^sub>2' x)
[PROOF STEP]
let ?mems = "zip (replicate ?n mem\<^sub>1) (replicate ?n mem\<^sub>2)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>mem\<^sub>1 mem\<^sub>2 k cms\<^sub>1' mem\<^sub>1'. \<lbrakk>list_all com_sifum_secure cmds; no_assumptions_on_termination cmds; \<forall>mem. sound_mode_use (add_initial_modes cmds, mem); mem\<^sub>1 =\<^sup>l mem\<^sub>2; (add_initial_modes cmds, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1')\<rbrakk> \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2'. (add_initial_modes cmds, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> length cms\<^sub>2' = length cms\<^sub>1' \<and> (\<forall>x. dma x = Low \<and> (\<forall>i<length cms\<^sub>1'. x \<notin> snd (cms\<^sub>1' ! i) AsmNoRead) \<longrightarrow> mem\<^sub>1' x = mem\<^sub>2' x)
[PROOF STEP]
assume low_eq: "mem\<^sub>1 =\<^sup>l mem\<^sub>2"
[PROOF STATE]
proof (state)
this:
mem\<^sub>1 =\<^sup>l mem\<^sub>2

goal (1 subgoal):
 1. \<And>mem\<^sub>1 mem\<^sub>2 k cms\<^sub>1' mem\<^sub>1'. \<lbrakk>list_all com_sifum_secure cmds; no_assumptions_on_termination cmds; \<forall>mem. sound_mode_use (add_initial_modes cmds, mem); mem\<^sub>1 =\<^sup>l mem\<^sub>2; (add_initial_modes cmds, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1')\<rbrakk> \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2'. (add_initial_modes cmds, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> length cms\<^sub>2' = length cms\<^sub>1' \<and> (\<forall>x. dma x = Low \<and> (\<forall>i<length cms\<^sub>1'. x \<notin> snd (cms\<^sub>1' ! i) AsmNoRead) \<longrightarrow> mem\<^sub>1' x = mem\<^sub>2' x)
[PROOF STEP]
with com_secure
[PROOF STATE]
proof (chain)
picking this:
list_all com_sifum_secure cmds
mem\<^sub>1 =\<^sup>l mem\<^sub>2
[PROOF STEP]
have compat:
    "makes_compatible (add_initial_modes cmds, mem\<^sub>1) (add_initial_modes cmds, mem\<^sub>2) ?mems"
[PROOF STATE]
proof (prove)
using this:
list_all com_sifum_secure cmds
mem\<^sub>1 =\<^sup>l mem\<^sub>2

goal (1 subgoal):
 1. makes_compatible (add_initial_modes cmds, mem\<^sub>1) (add_initial_modes cmds, mem\<^sub>2) (zip (replicate (length cmds) mem\<^sub>1) (replicate (length cmds) mem\<^sub>2))
[PROOF STEP]
by (metis compatible_refl fst_conv length_replicate map_replicate snd_conv zip_eq_conv)
[PROOF STATE]
proof (state)
this:
makes_compatible (add_initial_modes cmds, mem\<^sub>1) (add_initial_modes cmds, mem\<^sub>2) (zip (replicate (length cmds) mem\<^sub>1) (replicate (length cmds) mem\<^sub>2))

goal (1 subgoal):
 1. \<And>mem\<^sub>1 mem\<^sub>2 k cms\<^sub>1' mem\<^sub>1'. \<lbrakk>list_all com_sifum_secure cmds; no_assumptions_on_termination cmds; \<forall>mem. sound_mode_use (add_initial_modes cmds, mem); mem\<^sub>1 =\<^sup>l mem\<^sub>2; (add_initial_modes cmds, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1')\<rbrakk> \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2'. (add_initial_modes cmds, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> length cms\<^sub>2' = length cms\<^sub>1' \<and> (\<forall>x. dma x = Low \<and> (\<forall>i<length cms\<^sub>1'. x \<notin> snd (cms\<^sub>1' ! i) AsmNoRead) \<longrightarrow> mem\<^sub>1' x = mem\<^sub>2' x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
makes_compatible (add_initial_modes cmds, mem\<^sub>1) (add_initial_modes cmds, mem\<^sub>2) (zip (replicate (length cmds) mem\<^sub>1) (replicate (length cmds) mem\<^sub>2))

goal (1 subgoal):
 1. \<And>mem\<^sub>1 mem\<^sub>2 k cms\<^sub>1' mem\<^sub>1'. \<lbrakk>list_all com_sifum_secure cmds; no_assumptions_on_termination cmds; \<forall>mem. sound_mode_use (add_initial_modes cmds, mem); mem\<^sub>1 =\<^sup>l mem\<^sub>2; (add_initial_modes cmds, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1')\<rbrakk> \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2'. (add_initial_modes cmds, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> length cms\<^sub>2' = length cms\<^sub>1' \<and> (\<forall>x. dma x = Low \<and> (\<forall>i<length cms\<^sub>1'. x \<notin> snd (cms\<^sub>1' ! i) AsmNoRead) \<longrightarrow> mem\<^sub>1' x = mem\<^sub>2' x)
[PROOF STEP]
assume eval: "(add_initial_modes cmds, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1')"
[PROOF STATE]
proof (state)
this:
(add_initial_modes cmds, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1')

goal (1 subgoal):
 1. \<And>mem\<^sub>1 mem\<^sub>2 k cms\<^sub>1' mem\<^sub>1'. \<lbrakk>list_all com_sifum_secure cmds; no_assumptions_on_termination cmds; \<forall>mem. sound_mode_use (add_initial_modes cmds, mem); mem\<^sub>1 =\<^sup>l mem\<^sub>2; (add_initial_modes cmds, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1')\<rbrakk> \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2'. (add_initial_modes cmds, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> length cms\<^sub>2' = length cms\<^sub>1' \<and> (\<forall>x. dma x = Low \<and> (\<forall>i<length cms\<^sub>1'. x \<notin> snd (cms\<^sub>1' ! i) AsmNoRead) \<longrightarrow> mem\<^sub>1' x = mem\<^sub>2' x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
makes_compatible (add_initial_modes cmds, mem\<^sub>1) (add_initial_modes cmds, mem\<^sub>2) (zip (replicate (length cmds) mem\<^sub>1) (replicate (length cmds) mem\<^sub>2))
(add_initial_modes cmds, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1')
[PROOF STEP]
obtain cms\<^sub>2' mem\<^sub>2' mems'
    where p: "map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and>
             (add_initial_modes cmds, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and>
             makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'"
[PROOF STATE]
proof (prove)
using this:
makes_compatible (add_initial_modes cmds, mem\<^sub>1) (add_initial_modes cmds, mem\<^sub>2) (zip (replicate (length cmds) mem\<^sub>1) (replicate (length cmds) mem\<^sub>2))
(add_initial_modes cmds, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1')

goal (1 subgoal):
 1. (\<And>cms\<^sub>2' mem\<^sub>2' mems'. map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (add_initial_modes cmds, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using sound_modes makes_compatible_eval_k
[PROOF STATE]
proof (prove)
using this:
makes_compatible (add_initial_modes cmds, mem\<^sub>1) (add_initial_modes cmds, mem\<^sub>2) (zip (replicate (length cmds) mem\<^sub>1) (replicate (length cmds) mem\<^sub>2))
(add_initial_modes cmds, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1')
\<forall>mem. sound_mode_use (add_initial_modes cmds, mem)
\<lbrakk>makes_compatible (?cms\<^sub>1, ?mem\<^sub>1) (?cms\<^sub>2, ?mem\<^sub>2) ?mems; map snd ?cms\<^sub>1 = map snd ?cms\<^sub>2; sound_mode_use (?cms\<^sub>1, ?mem\<^sub>1); sound_mode_use (?cms\<^sub>2, ?mem\<^sub>2); (?cms\<^sub>1, ?mem\<^sub>1) \<rightarrow>\<^bsub>?k\<^esub> (?cms\<^sub>1', ?mem\<^sub>1')\<rbrakk> \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2' mems'. sound_mode_use (?cms\<^sub>1', ?mem\<^sub>1') \<and> sound_mode_use (cms\<^sub>2', mem\<^sub>2') \<and> map snd ?cms\<^sub>1' = map snd cms\<^sub>2' \<and> (?cms\<^sub>2, ?mem\<^sub>2) \<rightarrow>\<^bsub>?k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (?cms\<^sub>1', ?mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'

goal (1 subgoal):
 1. (\<And>cms\<^sub>2' mem\<^sub>2' mems'. map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (add_initial_modes cmds, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (add_initial_modes cmds, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'

goal (1 subgoal):
 1. \<And>mem\<^sub>1 mem\<^sub>2 k cms\<^sub>1' mem\<^sub>1'. \<lbrakk>list_all com_sifum_secure cmds; no_assumptions_on_termination cmds; \<forall>mem. sound_mode_use (add_initial_modes cmds, mem); mem\<^sub>1 =\<^sup>l mem\<^sub>2; (add_initial_modes cmds, mem\<^sub>1) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>1', mem\<^sub>1')\<rbrakk> \<Longrightarrow> \<exists>cms\<^sub>2' mem\<^sub>2'. (add_initial_modes cmds, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> length cms\<^sub>2' = length cms\<^sub>1' \<and> (\<forall>x. dma x = Low \<and> (\<forall>i<length cms\<^sub>1'. x \<notin> snd (cms\<^sub>1' ! i) AsmNoRead) \<longrightarrow> mem\<^sub>1' x = mem\<^sub>2' x)
[PROOF STEP]
thus "\<exists> cms\<^sub>2' mem\<^sub>2'. (add_initial_modes cmds, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and>
                        map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and>
                        length cms\<^sub>2' = length cms\<^sub>1' \<and>
                        (\<forall> x. dma x = Low \<and> (\<forall> i < length cms\<^sub>1'. x \<notin> snd (cms\<^sub>1' ! i) AsmNoRead)
          \<longrightarrow> mem\<^sub>1' x = mem\<^sub>2' x)"
[PROOF STATE]
proof (prove)
using this:
map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (add_initial_modes cmds, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'

goal (1 subgoal):
 1. \<exists>cms\<^sub>2' mem\<^sub>2'. (add_initial_modes cmds, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> length cms\<^sub>2' = length cms\<^sub>1' \<and> (\<forall>x. dma x = Low \<and> (\<forall>i<length cms\<^sub>1'. x \<notin> snd (cms\<^sub>1' ! i) AsmNoRead) \<longrightarrow> mem\<^sub>1' x = mem\<^sub>2' x)
[PROOF STEP]
using p compat_low_eq
[PROOF STATE]
proof (prove)
using this:
map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (add_initial_modes cmds, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'
map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> (add_initial_modes cmds, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> makes_compatible (cms\<^sub>1', mem\<^sub>1') (cms\<^sub>2', mem\<^sub>2') mems'
\<lbrakk>makes_compatible (?cms\<^sub>1, ?mem\<^sub>1) (?cms\<^sub>2, ?mem\<^sub>2) ?mems; map snd ?cms\<^sub>1 = map snd ?cms\<^sub>2; dma ?x = Low; \<forall>i<length ?cms\<^sub>1. ?x \<notin> snd (?cms\<^sub>1 ! i) AsmNoRead\<rbrakk> \<Longrightarrow> ?mem\<^sub>1 ?x = ?mem\<^sub>2 ?x

goal (1 subgoal):
 1. \<exists>cms\<^sub>2' mem\<^sub>2'. (add_initial_modes cmds, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> length cms\<^sub>2' = length cms\<^sub>1' \<and> (\<forall>x. dma x = Low \<and> (\<forall>i<length cms\<^sub>1'. x \<notin> snd (cms\<^sub>1' ! i) AsmNoRead) \<longrightarrow> mem\<^sub>1' x = mem\<^sub>2' x)
[PROOF STEP]
by (metis length_map)
[PROOF STATE]
proof (state)
this:
\<exists>cms\<^sub>2' mem\<^sub>2'. (add_initial_modes cmds, mem\<^sub>2) \<rightarrow>\<^bsub>k\<^esub> (cms\<^sub>2', mem\<^sub>2') \<and> map snd cms\<^sub>1' = map snd cms\<^sub>2' \<and> length cms\<^sub>2' = length cms\<^sub>1' \<and> (\<forall>x. dma x = Low \<and> (\<forall>i<length cms\<^sub>1'. x \<notin> snd (cms\<^sub>1' ! i) AsmNoRead) \<longrightarrow> mem\<^sub>1' x = mem\<^sub>2' x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma collinear_translate_iff: "collinear (((+) a) ` A) \<longleftrightarrow> collinear A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. collinear ((+) a ` A) = collinear A
[PROOF STEP]
by (auto simp: collinear_def)


[STATEMENT]
lemma angle_altdef: "angle a b c = arccos ((a - b) \<bullet> (c - b) / (dist a b * dist c b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. angle a b c = arccos ((a - b) \<bullet> (c - b) / (dist a b * dist c b))
[PROOF STEP]
by (simp add: angle_def vangle_def dist_norm)


[STATEMENT]
lemma vangle_0_left [simp]: "vangle 0 v = pi / 2"
  and vangle_0_right [simp]: "vangle u 0 = pi / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vangle (0::'a) v = pi / 2 &&& vangle u (0::'b) = pi / 2
[PROOF STEP]
by (simp_all add: vangle_def)


[STATEMENT]
lemma vangle_refl [simp]: "u \<noteq> 0 \<Longrightarrow> vangle u u = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<noteq> (0::'a) \<Longrightarrow> vangle u u = 0
[PROOF STEP]
by (simp add: vangle_def dot_square_norm power2_eq_square)


[STATEMENT]
lemma angle_refl [simp]: "angle a a b = pi / 2" "angle a b b = pi / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. angle a a b = pi / 2 &&& angle a b b = pi / 2
[PROOF STEP]
by (simp_all add: angle_def)


[STATEMENT]
lemma angle_refl_mid [simp]: "a \<noteq> b \<Longrightarrow> angle a b a = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> angle a b a = 0
[PROOF STEP]
by (simp add: angle_def)


[STATEMENT]
lemma cos_vangle: "cos (vangle u v) = u \<bullet> v / (norm u * norm v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cos (vangle u v) = u \<bullet> v / (norm u * norm v)
[PROOF STEP]
unfolding vangle_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cos (if u = (0::'a) \<or> v = (0::'a) then pi / 2 else arccos (u \<bullet> v / (norm u * norm v))) = u \<bullet> v / (norm u * norm v)
[PROOF STEP]
using Cauchy_Schwarz_ineq2[of u v]
[PROOF STATE]
proof (prove)
using this:
\<bar>u \<bullet> v\<bar> \<le> norm u * norm v

goal (1 subgoal):
 1. cos (if u = (0::'a) \<or> v = (0::'a) then pi / 2 else arccos (u \<bullet> v / (norm u * norm v))) = u \<bullet> v / (norm u * norm v)
[PROOF STEP]
by (auto simp: field_simps)


[STATEMENT]
lemma cos_angle: "cos (angle a b c) = (a - b) \<bullet> (c - b) / (dist a b * dist c b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cos (angle a b c) = (a - b) \<bullet> (c - b) / (dist a b * dist c b)
[PROOF STEP]
by (simp add: angle_def cos_vangle dist_norm)


[STATEMENT]
lemma inner_conv_angle: "(a - b) \<bullet> (c - b) = dist a b * dist c b * cos (angle a b c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a - b) \<bullet> (c - b) = dist a b * dist c b * cos (angle a b c)
[PROOF STEP]
by (simp add: cos_angle)


[STATEMENT]
lemma vangle_commute: "vangle u v = vangle v u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vangle u v = vangle v u
[PROOF STEP]
by (simp add: vangle_def inner_commute mult.commute)


[STATEMENT]
lemma vangle_nonneg: "vangle u v \<ge> 0" and vangle_le_pi: "vangle u v \<le> pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> vangle u v &&& vangle u v \<le> pi
[PROOF STEP]
using Cauchy_Schwarz_ineq2[of u v]
[PROOF STATE]
proof (prove)
using this:
\<bar>u \<bullet> v\<bar> \<le> norm u * norm v

goal (1 subgoal):
 1. 0 \<le> vangle u v &&& vangle u v \<le> pi
[PROOF STEP]
by (auto simp: vangle_def field_simps intro!: arccos_lbound arccos_ubound)


[STATEMENT]
lemma angle_nonneg: "angle a b c \<ge> 0" and angle_le_pi: "angle a b c \<le> pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> angle a b c &&& angle a b c \<le> pi
[PROOF STEP]
using vangle_bounds
[PROOF STATE]
proof (prove)
using this:
0 \<le> vangle ?u ?v
vangle ?u ?v \<le> pi

goal (1 subgoal):
 1. 0 \<le> angle a b c &&& angle a b c \<le> pi
[PROOF STEP]
unfolding angle_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> vangle ?u ?v
vangle ?u ?v \<le> pi

goal (1 subgoal):
 1. 0 \<le> vangle (a - b) (c - b) &&& vangle (a - b) (c - b) \<le> pi
[PROOF STEP]
by blast+


[STATEMENT]
lemma sin_vangle_nonneg: "sin (vangle u v) \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> sin (vangle u v)
[PROOF STEP]
using vangle_bounds
[PROOF STATE]
proof (prove)
using this:
0 \<le> vangle ?u ?v
vangle ?u ?v \<le> pi

goal (1 subgoal):
 1. 0 \<le> sin (vangle u v)
[PROOF STEP]
by (rule sin_ge_zero)


[STATEMENT]
lemma sin_angle_nonneg: "sin (angle a b c) \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> sin (angle a b c)
[PROOF STEP]
using angle_bounds
[PROOF STATE]
proof (prove)
using this:
0 \<le> angle ?a ?b ?c
angle ?a ?b ?c \<le> pi

goal (1 subgoal):
 1. 0 \<le> sin (angle a b c)
[PROOF STEP]
by (rule sin_ge_zero)


[STATEMENT]
lemma vangle_eq_0D:
  assumes "vangle u v = 0"
  shows   "norm u *\<^sub>R v = norm v *\<^sub>R u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm u *\<^sub>R v = norm v *\<^sub>R u
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. norm u *\<^sub>R v = norm v *\<^sub>R u
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
vangle u v = 0
[PROOF STEP]
have "u \<bullet> v = norm u * norm v"
[PROOF STATE]
proof (prove)
using this:
vangle u v = 0

goal (1 subgoal):
 1. u \<bullet> v = norm u * norm v
[PROOF STEP]
using arccos_eq_iff[of "(u \<bullet> v) / (norm u * norm v)" 1] Cauchy_Schwarz_ineq2[of u v]
[PROOF STATE]
proof (prove)
using this:
vangle u v = 0
\<bar>u \<bullet> v / (norm u * norm v)\<bar> \<le> 1 \<and> \<bar>1\<bar> \<le> 1 \<Longrightarrow> (arccos (u \<bullet> v / (norm u * norm v)) = arccos 1) = (u \<bullet> v / (norm u * norm v) = 1)
\<bar>u \<bullet> v\<bar> \<le> norm u * norm v

goal (1 subgoal):
 1. u \<bullet> v = norm u * norm v
[PROOF STEP]
by (fastforce simp: vangle_def split: if_split_asm)
[PROOF STATE]
proof (state)
this:
u \<bullet> v = norm u * norm v

goal (1 subgoal):
 1. norm u *\<^sub>R v = norm v *\<^sub>R u
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
u \<bullet> v = norm u * norm v

goal (1 subgoal):
 1. norm u *\<^sub>R v = norm v *\<^sub>R u
[PROOF STEP]
by (subst (asm) norm_cauchy_schwarz_eq) simp_all
[PROOF STATE]
proof (state)
this:
norm u *\<^sub>R v = norm v *\<^sub>R u

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vangle_eq_piD:
  assumes "vangle u v = pi"
  shows   "norm u *\<^sub>R v + norm v *\<^sub>R u = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm u *\<^sub>R v + norm v *\<^sub>R u = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. norm u *\<^sub>R v + norm v *\<^sub>R u = (0::'a)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
vangle u v = pi
[PROOF STEP]
have "(-u) \<bullet> v = norm (-u) * norm v"
[PROOF STATE]
proof (prove)
using this:
vangle u v = pi

goal (1 subgoal):
 1. - u \<bullet> v = norm (- u) * norm v
[PROOF STEP]
using arccos_eq_iff[of "(u \<bullet> v) / (norm u * norm v)" "-1"] Cauchy_Schwarz_ineq2[of u v]
[PROOF STATE]
proof (prove)
using this:
vangle u v = pi
\<bar>u \<bullet> v / (norm u * norm v)\<bar> \<le> 1 \<and> \<bar>- 1\<bar> \<le> 1 \<Longrightarrow> (arccos (u \<bullet> v / (norm u * norm v)) = arccos (- 1)) = (u \<bullet> v / (norm u * norm v) = - 1)
\<bar>u \<bullet> v\<bar> \<le> norm u * norm v

goal (1 subgoal):
 1. - u \<bullet> v = norm (- u) * norm v
[PROOF STEP]
by (simp add: field_simps vangle_def split: if_split_asm)
[PROOF STATE]
proof (state)
this:
- u \<bullet> v = norm (- u) * norm v

goal (1 subgoal):
 1. norm u *\<^sub>R v + norm v *\<^sub>R u = (0::'a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
- u \<bullet> v = norm (- u) * norm v

goal (1 subgoal):
 1. norm u *\<^sub>R v + norm v *\<^sub>R u = (0::'a)
[PROOF STEP]
by (subst (asm) norm_cauchy_schwarz_eq) simp_all
[PROOF STATE]
proof (state)
this:
norm u *\<^sub>R v + norm v *\<^sub>R u = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dist_triangle_eq:
  fixes a b c :: "'a :: real_inner"
  shows "(dist a c = dist a b + dist b c) \<longleftrightarrow> dist a b *\<^sub>R (c - b) + dist b c *\<^sub>R (a - b) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dist a c = dist a b + dist b c) = (dist a b *\<^sub>R (c - b) + dist b c *\<^sub>R (a - b) = (0::'a))
[PROOF STEP]
using norm_triangle_eq[of "b - a" "c - b"]
[PROOF STATE]
proof (prove)
using this:
(norm (b - a + (c - b)) = norm (b - a) + norm (c - b)) = (norm (b - a) *\<^sub>R (c - b) = norm (c - b) *\<^sub>R (b - a))

goal (1 subgoal):
 1. (dist a c = dist a b + dist b c) = (dist a b *\<^sub>R (c - b) + dist b c *\<^sub>R (a - b) = (0::'a))
[PROOF STEP]
by (simp add: dist_norm norm_minus_commute algebra_simps)


[STATEMENT]
lemma angle_eq_pi_imp_dist_additive:
  assumes "angle a b c = pi"
  shows   "dist a c = dist a b + dist b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist a c = dist a b + dist b c
[PROOF STEP]
using vangle_eq_piD[OF assms[unfolded angle_def]]
[PROOF STATE]
proof (prove)
using this:
norm (a - b) *\<^sub>R (c - b) + norm (c - b) *\<^sub>R (a - b) = (0::'a)

goal (1 subgoal):
 1. dist a c = dist a b + dist b c
[PROOF STEP]
by (subst dist_triangle_eq) (simp add: dist_norm norm_minus_commute)


[STATEMENT]
lemma orthogonal_iff_vangle: "orthogonal u v \<longleftrightarrow> vangle u v = pi / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. orthogonal u v = (vangle u v = pi / 2)
[PROOF STEP]
using arccos_eq_iff[of "u \<bullet> v / (norm u * norm v)" 0] Cauchy_Schwarz_ineq2[of u v]
[PROOF STATE]
proof (prove)
using this:
\<bar>u \<bullet> v / (norm u * norm v)\<bar> \<le> 1 \<and> \<bar>0\<bar> \<le> 1 \<Longrightarrow> (arccos (u \<bullet> v / (norm u * norm v)) = arccos 0) = (u \<bullet> v / (norm u * norm v) = 0)
\<bar>u \<bullet> v\<bar> \<le> norm u * norm v

goal (1 subgoal):
 1. orthogonal u v = (vangle u v = pi / 2)
[PROOF STEP]
by (auto simp: vangle_def orthogonal_def)


[STATEMENT]
lemma cos_minus1_imp_pi:
  assumes "cos x = -1" "x \<ge> 0" "x < 3 * pi"
  shows   "x = pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = pi
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = pi
[PROOF STEP]
have "cos (x - pi) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cos (x - pi) = 1
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
this:
cos (x - pi) = 1

goal (1 subgoal):
 1. x = pi
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cos (x - pi) = 1
[PROOF STEP]
obtain n :: int where n: "of_int n = (x / pi - 1) / 2"
[PROOF STATE]
proof (prove)
using this:
cos (x - pi) = 1

goal (1 subgoal):
 1. (\<And>n. real_of_int n = (x / pi - 1) / 2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (subst (asm) cos_one_2pi_int) (auto simp: field_simps)
[PROOF STATE]
proof (state)
this:
real_of_int n = (x / pi - 1) / 2

goal (1 subgoal):
 1. x = pi
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of_int n = (x / pi - 1) / 2

goal (1 subgoal):
 1. x = pi
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
cos x = - 1
0 \<le> x
x < 3 * pi
[PROOF STEP]
have "\<dots> \<in> {-1<..<1}"
[PROOF STATE]
proof (prove)
using this:
cos x = - 1
0 \<le> x
x < 3 * pi

goal (1 subgoal):
 1. (x / pi - 1) / 2 \<in> {- 1<..<1}
[PROOF STEP]
by (auto simp: field_simps)
[PROOF STATE]
proof (state)
this:
(x / pi - 1) / 2 \<in> {- 1<..<1}

goal (1 subgoal):
 1. x = pi
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real_of_int n \<in> {- 1<..<1}
[PROOF STEP]
have "n = 0"
[PROOF STATE]
proof (prove)
using this:
real_of_int n \<in> {- 1<..<1}

goal (1 subgoal):
 1. n = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n = 0

goal (1 subgoal):
 1. x = pi
[PROOF STEP]
with n
[PROOF STATE]
proof (chain)
picking this:
real_of_int n = (x / pi - 1) / 2
n = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
real_of_int n = (x / pi - 1) / 2
n = 0

goal (1 subgoal):
 1. x = pi
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = pi

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vangle_eqI:
  assumes "u \<noteq> 0" "v \<noteq> 0" "w \<noteq> 0" "x \<noteq> 0"
  assumes "(u \<bullet> v) * norm w * norm x = (w \<bullet> x) * norm u * norm v"
  shows   "vangle u v = vangle w x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vangle u v = vangle w x
[PROOF STEP]
using assms Cauchy_Schwarz_ineq2[of u v] Cauchy_Schwarz_ineq2[of w x]
[PROOF STATE]
proof (prove)
using this:
u \<noteq> (0::'a)
v \<noteq> (0::'a)
w \<noteq> (0::'b)
x \<noteq> (0::'b)
u \<bullet> v * norm w * norm x = w \<bullet> x * norm u * norm v
\<bar>u \<bullet> v\<bar> \<le> norm u * norm v
\<bar>w \<bullet> x\<bar> \<le> norm w * norm x

goal (1 subgoal):
 1. vangle u v = vangle w x
[PROOF STEP]
unfolding vangle_def
[PROOF STATE]
proof (prove)
using this:
u \<noteq> (0::'a)
v \<noteq> (0::'a)
w \<noteq> (0::'b)
x \<noteq> (0::'b)
u \<bullet> v * norm w * norm x = w \<bullet> x * norm u * norm v
\<bar>u \<bullet> v\<bar> \<le> norm u * norm v
\<bar>w \<bullet> x\<bar> \<le> norm w * norm x

goal (1 subgoal):
 1. (if u = (0::'a) \<or> v = (0::'a) then pi / 2 else arccos (u \<bullet> v / (norm u * norm v))) = (if w = (0::'b) \<or> x = (0::'b) then pi / 2 else arccos (w \<bullet> x / (norm w * norm x)))
[PROOF STEP]
by (auto simp: arccos_eq_iff field_simps)


[STATEMENT]
lemma angle_eqI:
  assumes "a \<noteq> b" "a \<noteq> c" "d \<noteq> e" "d \<noteq> f"
  assumes "((b-a) \<bullet> (c-a)) * dist d e * dist d f = ((e-d) \<bullet> (f-d)) * dist a b * dist a c"
  shows   "angle b a c = angle e d f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. angle b a c = angle e d f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<noteq> b
a \<noteq> c
d \<noteq> e
d \<noteq> f
(b - a) \<bullet> (c - a) * dist d e * dist d f = (e - d) \<bullet> (f - d) * dist a b * dist a c

goal (1 subgoal):
 1. angle b a c = angle e d f
[PROOF STEP]
unfolding angle_def
[PROOF STATE]
proof (prove)
using this:
a \<noteq> b
a \<noteq> c
d \<noteq> e
d \<noteq> f
(b - a) \<bullet> (c - a) * dist d e * dist d f = (e - d) \<bullet> (f - d) * dist a b * dist a c

goal (1 subgoal):
 1. vangle (b - a) (c - a) = vangle (e - d) (f - d)
[PROOF STEP]
by (intro vangle_eqI) (simp_all add: dist_norm norm_minus_commute)


[STATEMENT]
lemma cos_vangle_eqD: "cos (vangle u v) = cos (vangle w x) \<Longrightarrow> vangle u v = vangle w x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cos (vangle u v) = cos (vangle w x) \<Longrightarrow> vangle u v = vangle w x
[PROOF STEP]
by (rule cos_inj_pi) (simp_all add: vangle_bounds)


[STATEMENT]
lemma cos_angle_eqD: "cos (angle a b c) = cos (angle d e f) \<Longrightarrow> angle a b c = angle d e f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cos (angle a b c) = cos (angle d e f) \<Longrightarrow> angle a b c = angle d e f
[PROOF STEP]
unfolding angle_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cos (vangle (a - b) (c - b)) = cos (vangle (d - e) (f - e)) \<Longrightarrow> vangle (a - b) (c - b) = vangle (d - e) (f - e)
[PROOF STEP]
by (rule cos_vangle_eqD)


[STATEMENT]
lemma sin_vangle_zero_iff: "sin (vangle u v) = 0 \<longleftrightarrow> vangle u v \<in> {0, pi}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sin (vangle u v) = 0) = (vangle u v \<in> {0, pi})
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sin (vangle u v) = 0 \<Longrightarrow> vangle u v \<in> {0, pi}
 2. vangle u v \<in> {0, pi} \<Longrightarrow> sin (vangle u v) = 0
[PROOF STEP]
assume "sin (vangle u v) = 0"
[PROOF STATE]
proof (state)
this:
sin (vangle u v) = 0

goal (2 subgoals):
 1. sin (vangle u v) = 0 \<Longrightarrow> vangle u v \<in> {0, pi}
 2. vangle u v \<in> {0, pi} \<Longrightarrow> sin (vangle u v) = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sin (vangle u v) = 0
[PROOF STEP]
obtain n :: int where n: "of_int n = vangle u v / pi"
[PROOF STATE]
proof (prove)
using this:
sin (vangle u v) = 0

goal (1 subgoal):
 1. (\<And>n. real_of_int n = vangle u v / pi \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (subst (asm) sin_zero_iff_int2) auto
[PROOF STATE]
proof (state)
this:
real_of_int n = vangle u v / pi

goal (2 subgoals):
 1. sin (vangle u v) = 0 \<Longrightarrow> vangle u v \<in> {0, pi}
 2. vangle u v \<in> {0, pi} \<Longrightarrow> sin (vangle u v) = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of_int n = vangle u v / pi

goal (2 subgoals):
 1. sin (vangle u v) = 0 \<Longrightarrow> vangle u v \<in> {0, pi}
 2. vangle u v \<in> {0, pi} \<Longrightarrow> sin (vangle u v) = 0
[PROOF STEP]
have "\<dots> \<in> {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vangle u v / pi \<in> {0..1}
[PROOF STEP]
using vangle_bounds
[PROOF STATE]
proof (prove)
using this:
0 \<le> vangle ?u ?v
vangle ?u ?v \<le> pi

goal (1 subgoal):
 1. vangle u v / pi \<in> {0..1}
[PROOF STEP]
by (auto simp: field_simps)
[PROOF STATE]
proof (state)
this:
vangle u v / pi \<in> {0..1}

goal (2 subgoals):
 1. sin (vangle u v) = 0 \<Longrightarrow> vangle u v \<in> {0, pi}
 2. vangle u v \<in> {0, pi} \<Longrightarrow> sin (vangle u v) = 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real_of_int n \<in> {0..1}
[PROOF STEP]
have "n \<in> {0,1}"
[PROOF STATE]
proof (prove)
using this:
real_of_int n \<in> {0..1}

goal (1 subgoal):
 1. n \<in> {0, 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<in> {0, 1}

goal (2 subgoals):
 1. sin (vangle u v) = 0 \<Longrightarrow> vangle u v \<in> {0, pi}
 2. vangle u v \<in> {0, pi} \<Longrightarrow> sin (vangle u v) = 0
[PROOF STEP]
thus "vangle u v \<in> {0,pi}"
[PROOF STATE]
proof (prove)
using this:
n \<in> {0, 1}

goal (1 subgoal):
 1. vangle u v \<in> {0, pi}
[PROOF STEP]
using n
[PROOF STATE]
proof (prove)
using this:
n \<in> {0, 1}
real_of_int n = vangle u v / pi

goal (1 subgoal):
 1. vangle u v \<in> {0, pi}
[PROOF STEP]
by (auto simp: field_simps)
[PROOF STATE]
proof (state)
this:
vangle u v \<in> {0, pi}

goal (1 subgoal):
 1. vangle u v \<in> {0, pi} \<Longrightarrow> sin (vangle u v) = 0
[PROOF STEP]
qed auto


[STATEMENT]
lemma sin_angle_zero_iff: "sin (angle a b c) = 0 \<longleftrightarrow> angle a b c \<in> {0, pi}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sin (angle a b c) = 0) = (angle a b c \<in> {0, pi})
[PROOF STEP]
unfolding angle_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sin (vangle (a - b) (c - b)) = 0) = (vangle (a - b) (c - b) \<in> {0, pi})
[PROOF STEP]
by (simp only: sin_vangle_zero_iff)


[STATEMENT]
lemma vangle_collinear: "vangle u v \<in> {0, pi} \<Longrightarrow> collinear {0, u, v}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vangle u v \<in> {0, pi} \<Longrightarrow> collinear {0::'a, u, v}
[PROOF STEP]
apply (subst norm_cauchy_schwarz_equal [symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vangle u v \<in> {0, pi} \<Longrightarrow> \<bar>u \<bullet> v\<bar> = norm u * norm v
[PROOF STEP]
apply (subst norm_cauchy_schwarz_abs_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vangle u v \<in> {0, pi} \<Longrightarrow> norm u *\<^sub>R v = norm v *\<^sub>R u \<or> norm u *\<^sub>R v = - norm v *\<^sub>R u
[PROOF STEP]
apply (auto dest!: vangle_eq_0D vangle_eq_piD simp: eq_neg_iff_add_eq_0)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma angle_collinear: "angle a b c \<in> {0, pi} \<Longrightarrow> collinear {a, b, c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. angle a b c \<in> {0, pi} \<Longrightarrow> collinear {a, b, c}
[PROOF STEP]
apply (unfold angle_def, drule vangle_collinear)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. collinear {0::'a, a - b, c - b} \<Longrightarrow> collinear {a, b, c}
[PROOF STEP]
apply (subst collinear_translate_iff[symmetric, of _ "-b"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. collinear {0::'a, a - b, c - b} \<Longrightarrow> collinear ((+) (- b) ` {a, b, c})
[PROOF STEP]
apply (auto simp: insert_commute)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma not_collinear_vangle: "\<not>collinear {0,u,v} \<Longrightarrow> vangle u v \<in> {0<..<pi}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> collinear {0::'a, u, v} \<Longrightarrow> vangle u v \<in> {0<..<pi}
[PROOF STEP]
using vangle_bounds[of u v] vangle_collinear[of u v]
[PROOF STATE]
proof (prove)
using this:
0 \<le> vangle u v
vangle u v \<le> pi
vangle u v \<in> {0, pi} \<Longrightarrow> collinear {0::'a, u, v}

goal (1 subgoal):
 1. \<not> collinear {0::'a, u, v} \<Longrightarrow> vangle u v \<in> {0<..<pi}
[PROOF STEP]
by (cases "vangle u v = 0 \<or> vangle u v = pi") auto


[STATEMENT]
lemma not_collinear_angle: "\<not>collinear {a,b,c} \<Longrightarrow> angle a b c \<in> {0<..<pi}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> collinear {a, b, c} \<Longrightarrow> angle a b c \<in> {0<..<pi}
[PROOF STEP]
using angle_bounds[of a b c] angle_collinear[of a b c]
[PROOF STATE]
proof (prove)
using this:
0 \<le> angle a b c
angle a b c \<le> pi
angle a b c \<in> {0, pi} \<Longrightarrow> collinear {a, b, c}

goal (1 subgoal):
 1. \<not> collinear {a, b, c} \<Longrightarrow> angle a b c \<in> {0<..<pi}
[PROOF STEP]
by (cases "angle a b c = 0 \<or> angle a b c = pi") auto


[STATEMENT]
lemma vangle_scales:
  assumes "0 < c"
  shows "vangle (c *\<^sub>R v\<^sub>1) v\<^sub>2 = vangle v\<^sub>1 v\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vangle (c *\<^sub>R v\<^sub>1) v\<^sub>2 = vangle v\<^sub>1 v\<^sub>2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < c

goal (1 subgoal):
 1. vangle (c *\<^sub>R v\<^sub>1) v\<^sub>2 = vangle v\<^sub>1 v\<^sub>2
[PROOF STEP]
unfolding vangle_def
[PROOF STATE]
proof (prove)
using this:
0 < c

goal (1 subgoal):
 1. (if c *\<^sub>R v\<^sub>1 = (0::'a) \<or> v\<^sub>2 = (0::'a) then pi / 2 else arccos (c *\<^sub>R v\<^sub>1 \<bullet> v\<^sub>2 / (norm (c *\<^sub>R v\<^sub>1) * norm v\<^sub>2))) = (if v\<^sub>1 = (0::'a) \<or> v\<^sub>2 = (0::'a) then pi / 2 else arccos (v\<^sub>1 \<bullet> v\<^sub>2 / (norm v\<^sub>1 * norm v\<^sub>2)))
[PROOF STEP]
by auto


[STATEMENT]
lemma vangle_inverse:
  "vangle (- v\<^sub>1) v\<^sub>2 = pi - vangle v\<^sub>1 v\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vangle (- v\<^sub>1) v\<^sub>2 = pi - vangle v\<^sub>1 v\<^sub>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vangle (- v\<^sub>1) v\<^sub>2 = pi - vangle v\<^sub>1 v\<^sub>2
[PROOF STEP]
have "\<bar>v\<^sub>1 \<bullet> v\<^sub>2 / (norm v\<^sub>1 * norm v\<^sub>2)\<bar> \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>v\<^sub>1 \<bullet> v\<^sub>2 / (norm v\<^sub>1 * norm v\<^sub>2)\<bar> \<le> 1
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<bar>v\<^sub>1 \<bullet> v\<^sub>2 / (norm v\<^sub>1 * norm v\<^sub>2)\<bar> \<le> 1
 2. \<not> ?P \<Longrightarrow> \<bar>v\<^sub>1 \<bullet> v\<^sub>2 / (norm v\<^sub>1 * norm v\<^sub>2)\<bar> \<le> 1
[PROOF STEP]
assume "v\<^sub>1 \<noteq> 0 \<and> v\<^sub>2 \<noteq> 0"
[PROOF STATE]
proof (state)
this:
v\<^sub>1 \<noteq> (0::'a) \<and> v\<^sub>2 \<noteq> (0::'a)

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<bar>v\<^sub>1 \<bullet> v\<^sub>2 / (norm v\<^sub>1 * norm v\<^sub>2)\<bar> \<le> 1
 2. \<not> ?P \<Longrightarrow> \<bar>v\<^sub>1 \<bullet> v\<^sub>2 / (norm v\<^sub>1 * norm v\<^sub>2)\<bar> \<le> 1
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
v\<^sub>1 \<noteq> (0::'a) \<and> v\<^sub>2 \<noteq> (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v\<^sub>1 \<noteq> (0::'a) \<and> v\<^sub>2 \<noteq> (0::'a)

goal (1 subgoal):
 1. \<bar>v\<^sub>1 \<bullet> v\<^sub>2 / (norm v\<^sub>1 * norm v\<^sub>2)\<bar> \<le> 1
[PROOF STEP]
by (simp add: Cauchy_Schwarz_ineq2)
[PROOF STATE]
proof (state)
this:
\<bar>v\<^sub>1 \<bullet> v\<^sub>2 / (norm v\<^sub>1 * norm v\<^sub>2)\<bar> \<le> 1

goal (1 subgoal):
 1. \<not> (v\<^sub>1 \<noteq> (0::'a) \<and> v\<^sub>2 \<noteq> (0::'a)) \<Longrightarrow> \<bar>v\<^sub>1 \<bullet> v\<^sub>2 / (norm v\<^sub>1 * norm v\<^sub>2)\<bar> \<le> 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (v\<^sub>1 \<noteq> (0::'a) \<and> v\<^sub>2 \<noteq> (0::'a)) \<Longrightarrow> \<bar>v\<^sub>1 \<bullet> v\<^sub>2 / (norm v\<^sub>1 * norm v\<^sub>2)\<bar> \<le> 1
[PROOF STEP]
assume "\<not> (v\<^sub>1 \<noteq> 0 \<and> v\<^sub>2 \<noteq> 0)"
[PROOF STATE]
proof (state)
this:
\<not> (v\<^sub>1 \<noteq> (0::'a) \<and> v\<^sub>2 \<noteq> (0::'a))

goal (1 subgoal):
 1. \<not> (v\<^sub>1 \<noteq> (0::'a) \<and> v\<^sub>2 \<noteq> (0::'a)) \<Longrightarrow> \<bar>v\<^sub>1 \<bullet> v\<^sub>2 / (norm v\<^sub>1 * norm v\<^sub>2)\<bar> \<le> 1
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> (v\<^sub>1 \<noteq> (0::'a) \<and> v\<^sub>2 \<noteq> (0::'a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (v\<^sub>1 \<noteq> (0::'a) \<and> v\<^sub>2 \<noteq> (0::'a))

goal (1 subgoal):
 1. \<bar>v\<^sub>1 \<bullet> v\<^sub>2 / (norm v\<^sub>1 * norm v\<^sub>2)\<bar> \<le> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>v\<^sub>1 \<bullet> v\<^sub>2 / (norm v\<^sub>1 * norm v\<^sub>2)\<bar> \<le> 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<bar>v\<^sub>1 \<bullet> v\<^sub>2 / (norm v\<^sub>1 * norm v\<^sub>2)\<bar> \<le> 1

goal (1 subgoal):
 1. vangle (- v\<^sub>1) v\<^sub>2 = pi - vangle v\<^sub>1 v\<^sub>2
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<bar>v\<^sub>1 \<bullet> v\<^sub>2 / (norm v\<^sub>1 * norm v\<^sub>2)\<bar> \<le> 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>v\<^sub>1 \<bullet> v\<^sub>2 / (norm v\<^sub>1 * norm v\<^sub>2)\<bar> \<le> 1

goal (1 subgoal):
 1. vangle (- v\<^sub>1) v\<^sub>2 = pi - vangle v\<^sub>1 v\<^sub>2
[PROOF STEP]
unfolding vangle_def
[PROOF STATE]
proof (prove)
using this:
\<bar>v\<^sub>1 \<bullet> v\<^sub>2 / (norm v\<^sub>1 * norm v\<^sub>2)\<bar> \<le> 1

goal (1 subgoal):
 1. (if - v\<^sub>1 = (0::'a) \<or> v\<^sub>2 = (0::'a) then pi / 2 else arccos (- v\<^sub>1 \<bullet> v\<^sub>2 / (norm (- v\<^sub>1) * norm v\<^sub>2))) = pi - (if v\<^sub>1 = (0::'a) \<or> v\<^sub>2 = (0::'a) then pi / 2 else arccos (v\<^sub>1 \<bullet> v\<^sub>2 / (norm v\<^sub>1 * norm v\<^sub>2)))
[PROOF STEP]
by (simp add: arccos_minus_abs)
[PROOF STATE]
proof (state)
this:
vangle (- v\<^sub>1) v\<^sub>2 = pi - vangle v\<^sub>1 v\<^sub>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma orthogonal_iff_angle:
  shows "orthogonal (A - B) (C - B) \<longleftrightarrow> angle A B C = pi / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. orthogonal (A - B) (C - B) = (angle A B C = pi / 2)
[PROOF STEP]
unfolding angle_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. orthogonal (A - B) (C - B) = (vangle (A - B) (C - B) = pi / 2)
[PROOF STEP]
by (auto simp only: orthogonal_iff_vangle)


[STATEMENT]
lemma angle_inverse:
  assumes "between (A, C) B"
  assumes "A \<noteq> B" "B \<noteq> C"
  shows "angle A B D = pi - angle C B D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. angle A B D = pi - angle C B D
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. angle A B D = pi - angle C B D
[PROOF STEP]
from \<open>between (A, C) B\<close>
[PROOF STATE]
proof (chain)
picking this:
between (A, C) B
[PROOF STEP]
obtain u where u: "u \<ge> 0" "u \<le> 1"
    and X: "B = u *\<^sub>R A + (1 - u) *\<^sub>R C"
[PROOF STATE]
proof (prove)
using this:
between (A, C) B

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>0 \<le> u; u \<le> 1; B = u *\<^sub>R A + (1 - u) *\<^sub>R C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis add.commute betweenE between_commute)
[PROOF STATE]
proof (state)
this:
0 \<le> u
u \<le> 1
B = u *\<^sub>R A + (1 - u) *\<^sub>R C

goal (1 subgoal):
 1. angle A B D = pi - angle C B D
[PROOF STEP]
from \<open>A \<noteq> B\<close> \<open>B \<noteq> C\<close> X
[PROOF STATE]
proof (chain)
picking this:
A \<noteq> B
B \<noteq> C
B = u *\<^sub>R A + (1 - u) *\<^sub>R C
[PROOF STEP]
have "u \<noteq> 0" "u \<noteq> 1"
[PROOF STATE]
proof (prove)
using this:
A \<noteq> B
B \<noteq> C
B = u *\<^sub>R A + (1 - u) *\<^sub>R C

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

goal (1 subgoal):
 1. angle A B D = pi - angle C B D
[PROOF STEP]
have "0 < ((1 - u) / u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < (1 - u) / u
[PROOF STEP]
using \<open>u \<noteq> 0\<close> \<open>u \<noteq> 1\<close> \<open>u \<ge> 0\<close> \<open>u \<le> 1\<close>
[PROOF STATE]
proof (prove)
using this:
u \<noteq> 0
u \<noteq> 1
0 \<le> u
u \<le> 1

goal (1 subgoal):
 1. 0 < (1 - u) / u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < (1 - u) / u

goal (1 subgoal):
 1. angle A B D = pi - angle C B D
[PROOF STEP]
from X
[PROOF STATE]
proof (chain)
picking this:
B = u *\<^sub>R A + (1 - u) *\<^sub>R C
[PROOF STEP]
have "A - B = - (1 - u) *\<^sub>R (C - A)"
[PROOF STATE]
proof (prove)
using this:
B = u *\<^sub>R A + (1 - u) *\<^sub>R C

goal (1 subgoal):
 1. A - B = - (1 - u) *\<^sub>R (C - A)
[PROOF STEP]
by (simp add: real_vector.scale_right_diff_distrib real_vector.scale_left_diff_distrib)
[PROOF STATE]
proof (state)
this:
A - B = - (1 - u) *\<^sub>R (C - A)

goal (1 subgoal):
 1. angle A B D = pi - angle C B D
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A - B = - (1 - u) *\<^sub>R (C - A)

goal (1 subgoal):
 1. angle A B D = pi - angle C B D
[PROOF STEP]
from X
[PROOF STATE]
proof (chain)
picking this:
B = u *\<^sub>R A + (1 - u) *\<^sub>R C
[PROOF STEP]
have "C - B = u *\<^sub>R (C - A)"
[PROOF STATE]
proof (prove)
using this:
B = u *\<^sub>R A + (1 - u) *\<^sub>R C

goal (1 subgoal):
 1. C - B = u *\<^sub>R (C - A)
[PROOF STEP]
by (simp add: scaleR_diff_left real_vector.scale_right_diff_distrib)
[PROOF STATE]
proof (state)
this:
C - B = u *\<^sub>R (C - A)

goal (1 subgoal):
 1. angle A B D = pi - angle C B D
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A - B = - (1 - u) *\<^sub>R (C - A)
C - B = u *\<^sub>R (C - A)
[PROOF STEP]
have "A - B = - (((1 - u) / u) *\<^sub>R (C - B))"
[PROOF STATE]
proof (prove)
using this:
A - B = - (1 - u) *\<^sub>R (C - A)
C - B = u *\<^sub>R (C - A)

goal (1 subgoal):
 1. A - B = - (((1 - u) / u) *\<^sub>R (C - B))
[PROOF STEP]
using \<open>u \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
A - B = - (1 - u) *\<^sub>R (C - A)
C - B = u *\<^sub>R (C - A)
u \<noteq> 0

goal (1 subgoal):
 1. A - B = - (((1 - u) / u) *\<^sub>R (C - B))
[PROOF STEP]
by simp (metis minus_diff_eq real_vector.scale_minus_left)
[PROOF STATE]
proof (state)
this:
A - B = - (((1 - u) / u) *\<^sub>R (C - B))

goal (1 subgoal):
 1. angle A B D = pi - angle C B D
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
A - B = - (((1 - u) / u) *\<^sub>R (C - B))
[PROOF STEP]
have "vangle (A - B) (D - B) = pi - vangle (C - B) (D - B)"
[PROOF STATE]
proof (prove)
using this:
A - B = - (((1 - u) / u) *\<^sub>R (C - B))

goal (1 subgoal):
 1. vangle (A - B) (D - B) = pi - vangle (C - B) (D - B)
[PROOF STEP]
using \<open>0 < (1 - u) / u\<close>
[PROOF STATE]
proof (prove)
using this:
A - B = - (((1 - u) / u) *\<^sub>R (C - B))
0 < (1 - u) / u

goal (1 subgoal):
 1. vangle (A - B) (D - B) = pi - vangle (C - B) (D - B)
[PROOF STEP]
by (simp add: vangle_inverse vangle_scales)
[PROOF STATE]
proof (state)
this:
vangle (A - B) (D - B) = pi - vangle (C - B) (D - B)

goal (1 subgoal):
 1. angle A B D = pi - angle C B D
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
vangle (A - B) (D - B) = pi - vangle (C - B) (D - B)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vangle (A - B) (D - B) = pi - vangle (C - B) (D - B)

goal (1 subgoal):
 1. angle A B D = pi - angle C B D
[PROOF STEP]
unfolding angle_def
[PROOF STATE]
proof (prove)
using this:
vangle (A - B) (D - B) = pi - vangle (C - B) (D - B)

goal (1 subgoal):
 1. vangle (A - B) (D - B) = pi - vangle (C - B) (D - B)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
angle A B D = pi - angle C B D

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma strictly_between_implies_angle_eq_pi:
  assumes "between (A, C) B"
  assumes "A \<noteq> B" "B \<noteq> C"
  shows "angle A B C = pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. angle A B C = pi
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. angle A B C = pi
[PROOF STEP]
from \<open>between (A, C) B\<close>
[PROOF STATE]
proof (chain)
picking this:
between (A, C) B
[PROOF STEP]
obtain u where u: "u \<ge> 0" "u \<le> 1"
    and X: "B = u *\<^sub>R A + (1 - u) *\<^sub>R C"
[PROOF STATE]
proof (prove)
using this:
between (A, C) B

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>0 \<le> u; u \<le> 1; B = u *\<^sub>R A + (1 - u) *\<^sub>R C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis add.commute betweenE between_commute)
[PROOF STATE]
proof (state)
this:
0 \<le> u
u \<le> 1
B = u *\<^sub>R A + (1 - u) *\<^sub>R C

goal (1 subgoal):
 1. angle A B C = pi
[PROOF STEP]
from \<open>A \<noteq> B\<close> \<open>B \<noteq> C\<close> X
[PROOF STATE]
proof (chain)
picking this:
A \<noteq> B
B \<noteq> C
B = u *\<^sub>R A + (1 - u) *\<^sub>R C
[PROOF STEP]
have "u \<noteq> 0" "u \<noteq> 1"
[PROOF STATE]
proof (prove)
using this:
A \<noteq> B
B \<noteq> C
B = u *\<^sub>R A + (1 - u) *\<^sub>R C

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

goal (1 subgoal):
 1. angle A B C = pi
[PROOF STEP]
from \<open>A \<noteq> B\<close> \<open>B \<noteq> C\<close> \<open>between (A, C) B\<close>
[PROOF STATE]
proof (chain)
picking this:
A \<noteq> B
B \<noteq> C
between (A, C) B
[PROOF STEP]
have "A \<noteq> C"
[PROOF STATE]
proof (prove)
using this:
A \<noteq> B
B \<noteq> C
between (A, C) B

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

goal (1 subgoal):
 1. angle A B C = pi
[PROOF STEP]
from X
[PROOF STATE]
proof (chain)
picking this:
B = u *\<^sub>R A + (1 - u) *\<^sub>R C
[PROOF STEP]
have "A - B = - (1 - u) *\<^sub>R (C - A)"
[PROOF STATE]
proof (prove)
using this:
B = u *\<^sub>R A + (1 - u) *\<^sub>R C

goal (1 subgoal):
 1. A - B = - (1 - u) *\<^sub>R (C - A)
[PROOF STEP]
by (simp add: real_vector.scale_right_diff_distrib real_vector.scale_left_diff_distrib)
[PROOF STATE]
proof (state)
this:
A - B = - (1 - u) *\<^sub>R (C - A)

goal (1 subgoal):
 1. angle A B C = pi
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A - B = - (1 - u) *\<^sub>R (C - A)

goal (1 subgoal):
 1. angle A B C = pi
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
A - B = - (1 - u) *\<^sub>R (C - A)
[PROOF STEP]
have "dist A B = norm ((1 - u) *\<^sub>R (C - A))"
[PROOF STATE]
proof (prove)
using this:
A - B = - (1 - u) *\<^sub>R (C - A)

goal (1 subgoal):
 1. dist A B = norm ((1 - u) *\<^sub>R (C - A))
[PROOF STEP]
using \<open>u \<ge> 0\<close> \<open>u \<le> 1\<close>
[PROOF STATE]
proof (prove)
using this:
A - B = - (1 - u) *\<^sub>R (C - A)
0 \<le> u
u \<le> 1

goal (1 subgoal):
 1. dist A B = norm ((1 - u) *\<^sub>R (C - A))
[PROOF STEP]
by (simp add: dist_norm)
[PROOF STATE]
proof (state)
this:
dist A B = norm ((1 - u) *\<^sub>R (C - A))

goal (1 subgoal):
 1. angle A B C = pi
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dist A B = norm ((1 - u) *\<^sub>R (C - A))

goal (1 subgoal):
 1. angle A B C = pi
[PROOF STEP]
from X
[PROOF STATE]
proof (chain)
picking this:
B = u *\<^sub>R A + (1 - u) *\<^sub>R C
[PROOF STEP]
have "C - B = u *\<^sub>R (C - A)"
[PROOF STATE]
proof (prove)
using this:
B = u *\<^sub>R A + (1 - u) *\<^sub>R C

goal (1 subgoal):
 1. C - B = u *\<^sub>R (C - A)
[PROOF STEP]
by (simp add: scaleR_diff_left real_vector.scale_right_diff_distrib)
[PROOF STATE]
proof (state)
this:
C - B = u *\<^sub>R (C - A)

goal (1 subgoal):
 1. angle A B C = pi
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
C - B = u *\<^sub>R (C - A)

goal (1 subgoal):
 1. angle A B C = pi
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
C - B = u *\<^sub>R (C - A)
[PROOF STEP]
have "dist C B = norm (u *\<^sub>R (C - A))"
[PROOF STATE]
proof (prove)
using this:
C - B = u *\<^sub>R (C - A)

goal (1 subgoal):
 1. dist C B = norm (u *\<^sub>R (C - A))
[PROOF STEP]
by (simp add: dist_norm)
[PROOF STATE]
proof (state)
this:
dist C B = norm (u *\<^sub>R (C - A))

goal (1 subgoal):
 1. angle A B C = pi
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A - B = - (1 - u) *\<^sub>R (C - A)
dist A B = norm ((1 - u) *\<^sub>R (C - A))
C - B = u *\<^sub>R (C - A)
dist C B = norm (u *\<^sub>R (C - A))
[PROOF STEP]
have "(A - B) \<bullet> (C - B) / (dist A B * dist C B) = u * (u - 1) / (\<bar>1 - u\<bar> * \<bar>u\<bar>)"
[PROOF STATE]
proof (prove)
using this:
A - B = - (1 - u) *\<^sub>R (C - A)
dist A B = norm ((1 - u) *\<^sub>R (C - A))
C - B = u *\<^sub>R (C - A)
dist C B = norm (u *\<^sub>R (C - A))

goal (1 subgoal):
 1. (A - B) \<bullet> (C - B) / (dist A B * dist C B) = u * (u - 1) / (\<bar>1 - u\<bar> * \<bar>u\<bar>)
[PROOF STEP]
using \<open>A \<noteq> C\<close>
[PROOF STATE]
proof (prove)
using this:
A - B = - (1 - u) *\<^sub>R (C - A)
dist A B = norm ((1 - u) *\<^sub>R (C - A))
C - B = u *\<^sub>R (C - A)
dist C B = norm (u *\<^sub>R (C - A))
A \<noteq> C

goal (1 subgoal):
 1. (A - B) \<bullet> (C - B) / (dist A B * dist C B) = u * (u - 1) / (\<bar>1 - u\<bar> * \<bar>u\<bar>)
[PROOF STEP]
by (simp add: dot_square_norm power2_eq_square)
[PROOF STATE]
proof (state)
this:
(A - B) \<bullet> (C - B) / (dist A B * dist C B) = u * (u - 1) / (\<bar>1 - u\<bar> * \<bar>u\<bar>)

goal (1 subgoal):
 1. angle A B C = pi
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(A - B) \<bullet> (C - B) / (dist A B * dist C B) = u * (u - 1) / (\<bar>1 - u\<bar> * \<bar>u\<bar>)

goal (1 subgoal):
 1. angle A B C = pi
[PROOF STEP]
have "\<dots> = - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u * (u - 1) / (\<bar>1 - u\<bar> * \<bar>u\<bar>) = - 1
[PROOF STEP]
using \<open>u \<noteq> 0\<close> \<open>u \<noteq> 1\<close> \<open>u \<ge> 0\<close> \<open>u \<le> 1\<close>
[PROOF STATE]
proof (prove)
using this:
u \<noteq> 0
u \<noteq> 1
0 \<le> u
u \<le> 1

goal (1 subgoal):
 1. u * (u - 1) / (\<bar>1 - u\<bar> * \<bar>u\<bar>) = - 1
[PROOF STEP]
by (simp add: divide_eq_minus_1_iff)
[PROOF STATE]
proof (state)
this:
u * (u - 1) / (\<bar>1 - u\<bar> * \<bar>u\<bar>) = - 1

goal (1 subgoal):
 1. angle A B C = pi
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(A - B) \<bullet> (C - B) / (dist A B * dist C B) = - 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(A - B) \<bullet> (C - B) / (dist A B * dist C B) = - 1

goal (1 subgoal):
 1. angle A B C = pi
[PROOF STEP]
unfolding angle_altdef
[PROOF STATE]
proof (prove)
using this:
(A - B) \<bullet> (C - B) / (dist A B * dist C B) = - 1

goal (1 subgoal):
 1. arccos ((A - B) \<bullet> (C - B) / (dist A B * dist C B)) = pi
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
angle A B C = pi

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma degree_normalized_le_1: "degree_normalized x S \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree_normalized x S \<le> 1
[PROOF STEP]
proof(cases "finite S")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite S \<Longrightarrow> degree_normalized x S \<le> 1
 2. infinite S \<Longrightarrow> degree_normalized x S \<le> 1
[PROOF STEP]
assume hA: "finite S"
[PROOF STATE]
proof (state)
this:
finite S

goal (2 subgoals):
 1. finite S \<Longrightarrow> degree_normalized x S \<le> 1
 2. infinite S \<Longrightarrow> degree_normalized x S \<le> 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite S
[PROOF STEP]
have "card (neighbors_ss x S) \<le> card S"
[PROOF STATE]
proof (prove)
using this:
finite S

goal (1 subgoal):
 1. card (neighbors_ss x S) \<le> card S
[PROOF STEP]
using neighbors_ss_def card_mono hA
[PROOF STATE]
proof (prove)
using this:
finite S
neighbors_ss ?x ?Y \<equiv> {y \<in> ?Y. vert_adj ?x y}
\<lbrakk>finite ?B; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> card ?A \<le> card ?B
finite S

goal (1 subgoal):
 1. card (neighbors_ss x S) \<le> card S
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
card (neighbors_ss x S) \<le> card S

goal (2 subgoals):
 1. finite S \<Longrightarrow> degree_normalized x S \<le> 1
 2. infinite S \<Longrightarrow> degree_normalized x S \<le> 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card (neighbors_ss x S) \<le> card S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card (neighbors_ss x S) \<le> card S

goal (1 subgoal):
 1. degree_normalized x S \<le> 1
[PROOF STEP]
using degree_normalized_def divide_le_eq_1
[PROOF STATE]
proof (prove)
using this:
card (neighbors_ss x S) \<le> card S
degree_normalized ?v ?S \<equiv> real (card (neighbors_ss ?v ?S)) / real (card ?S)
(?b / ?a \<le> (1::?'a)) = ((0::?'a) < ?a \<and> ?b \<le> ?a \<or> ?a < (0::?'a) \<and> ?a \<le> ?b \<or> ?a = (0::?'a))

goal (1 subgoal):
 1. degree_normalized x S \<le> 1
[PROOF STEP]
by (metis antisym_conv3 of_nat_le_iff of_nat_less_0_iff)
[PROOF STATE]
proof (state)
this:
degree_normalized x S \<le> 1

goal (1 subgoal):
 1. infinite S \<Longrightarrow> degree_normalized x S \<le> 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite S \<Longrightarrow> degree_normalized x S \<le> 1
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
infinite S

goal (1 subgoal):
 1. infinite S \<Longrightarrow> degree_normalized x S \<le> 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
infinite S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
infinite S

goal (1 subgoal):
 1. degree_normalized x S \<le> 1
[PROOF STEP]
using degree_normalized_def
[PROOF STATE]
proof (prove)
using this:
infinite S
degree_normalized ?v ?S \<equiv> real (card (neighbors_ss ?v ?S)) / real (card ?S)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma codegree_neighbors: "codegree v u = card (neighborhood v \<inter> neighborhood u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codegree v u = card (neighborhood v \<inter> neighborhood u)
[PROOF STEP]
unfolding codegree_def neighborhood_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {x \<in> V. vert_adj v x \<and> vert_adj u x} = card ({va \<in> V. vert_adj v va} \<inter> {v \<in> V. vert_adj u v})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card {x \<in> V. vert_adj v x \<and> vert_adj u x} = card ({va \<in> V. vert_adj v va} \<inter> {v \<in> V. vert_adj u v})
[PROOF STEP]
have "{x \<in> V. vert_adj v x \<and> vert_adj u x} = {va \<in> V. vert_adj v va} \<inter> {v \<in> V. vert_adj u v}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> V. vert_adj v x \<and> vert_adj u x} = {va \<in> V. vert_adj v va} \<inter> {v \<in> V. vert_adj u v}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{x \<in> V. vert_adj v x \<and> vert_adj u x} = {va \<in> V. vert_adj v va} \<inter> {v \<in> V. vert_adj u v}

goal (1 subgoal):
 1. card {x \<in> V. vert_adj v x \<and> vert_adj u x} = card ({va \<in> V. vert_adj v va} \<inter> {v \<in> V. vert_adj u v})
[PROOF STEP]
thus "card {x \<in> V. vert_adj v x \<and> vert_adj u x} = card ({va \<in> V. vert_adj v va} \<inter> {v \<in> V. vert_adj u v})"
[PROOF STATE]
proof (prove)
using this:
{x \<in> V. vert_adj v x \<and> vert_adj u x} = {va \<in> V. vert_adj v va} \<inter> {v \<in> V. vert_adj u v}

goal (1 subgoal):
 1. card {x \<in> V. vert_adj v x \<and> vert_adj u x} = card ({va \<in> V. vert_adj v va} \<inter> {v \<in> V. vert_adj u v})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card {x \<in> V. vert_adj v x \<and> vert_adj u x} = card ({va \<in> V. vert_adj v va} \<inter> {v \<in> V. vert_adj u v})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma codegree_sym: "codegree v u = codegree u v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codegree v u = codegree u v
[PROOF STEP]
by (simp add: Int_commute codegree_neighbors)


[STATEMENT]
lemma codegree_normalized_altX:
  assumes "x \<in> X" and "x' \<in> X"
  shows "codegree_normalized x x' Y = card (neighbors_ss x Y \<inter> neighbors_ss x' Y) / card Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codegree_normalized x x' Y = real (card (neighbors_ss x Y \<inter> neighbors_ss x' Y)) / real (card Y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. codegree_normalized x x' Y = real (card (neighbors_ss x Y \<inter> neighbors_ss x' Y)) / real (card Y)
[PROOF STEP]
have "((neighbors_ss x Y) \<inter> (neighbors_ss x' Y)) = neighborhood x \<inter> neighborhood x'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. neighbors_ss x Y \<inter> neighbors_ss x' Y = neighborhood x \<inter> neighborhood x'
[PROOF STEP]
using neighbors_ss_eq_neighborhoodX assms
[PROOF STATE]
proof (prove)
using this:
?v \<in> X \<Longrightarrow> neighborhood ?v = neighbors_ss ?v Y
x \<in> X
x' \<in> X

goal (1 subgoal):
 1. neighbors_ss x Y \<inter> neighbors_ss x' Y = neighborhood x \<inter> neighborhood x'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
neighbors_ss x Y \<inter> neighbors_ss x' Y = neighborhood x \<inter> neighborhood x'

goal (1 subgoal):
 1. codegree_normalized x x' Y = real (card (neighbors_ss x Y \<inter> neighbors_ss x' Y)) / real (card Y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
neighbors_ss x Y \<inter> neighbors_ss x' Y = neighborhood x \<inter> neighborhood x'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
neighbors_ss x Y \<inter> neighbors_ss x' Y = neighborhood x \<inter> neighborhood x'

goal (1 subgoal):
 1. codegree_normalized x x' Y = real (card (neighbors_ss x Y \<inter> neighbors_ss x' Y)) / real (card Y)
[PROOF STEP]
unfolding codegree_normalized_def
[PROOF STATE]
proof (prove)
using this:
neighbors_ss x Y \<inter> neighbors_ss x' Y = neighborhood x \<inter> neighborhood x'

goal (1 subgoal):
 1. real (codegree x x') / real (card Y) = real (card (neighbors_ss x Y \<inter> neighbors_ss x' Y)) / real (card Y)
[PROOF STEP]
using codegree_def codegree_neighbors
[PROOF STATE]
proof (prove)
using this:
neighbors_ss x Y \<inter> neighbors_ss x' Y = neighborhood x \<inter> neighborhood x'
codegree ?v ?u \<equiv> card {x \<in> V. vert_adj ?v x \<and> vert_adj ?u x}
codegree ?v ?u = card (neighborhood ?v \<inter> neighborhood ?u)

goal (1 subgoal):
 1. real (codegree x x') / real (card Y) = real (card (neighbors_ss x Y \<inter> neighbors_ss x' Y)) / real (card Y)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
codegree_normalized x x' Y = real (card (neighbors_ss x Y \<inter> neighbors_ss x' Y)) / real (card Y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma codegree_normalized_altY:
  assumes "y \<in> Y" and "y' \<in> Y"
  shows "codegree_normalized y y' X = card (neighbors_ss y X \<inter> neighbors_ss y' X) / card X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codegree_normalized y y' X = real (card (neighbors_ss y X \<inter> neighbors_ss y' X)) / real (card X)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. codegree_normalized y y' X = real (card (neighbors_ss y X \<inter> neighbors_ss y' X)) / real (card X)
[PROOF STEP]
have "neighbors_ss y X \<inter> neighbors_ss y' X = neighborhood y \<inter> neighborhood y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. neighbors_ss y X \<inter> neighbors_ss y' X = neighborhood y \<inter> neighborhood y'
[PROOF STEP]
using neighbors_ss_eq_neighborhoodY assms
[PROOF STATE]
proof (prove)
using this:
?v \<in> Y \<Longrightarrow> neighborhood ?v = neighbors_ss ?v X
y \<in> Y
y' \<in> Y

goal (1 subgoal):
 1. neighbors_ss y X \<inter> neighbors_ss y' X = neighborhood y \<inter> neighborhood y'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
neighbors_ss y X \<inter> neighbors_ss y' X = neighborhood y \<inter> neighborhood y'

goal (1 subgoal):
 1. codegree_normalized y y' X = real (card (neighbors_ss y X \<inter> neighbors_ss y' X)) / real (card X)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
neighbors_ss y X \<inter> neighbors_ss y' X = neighborhood y \<inter> neighborhood y'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
neighbors_ss y X \<inter> neighbors_ss y' X = neighborhood y \<inter> neighborhood y'

goal (1 subgoal):
 1. codegree_normalized y y' X = real (card (neighbors_ss y X \<inter> neighbors_ss y' X)) / real (card X)
[PROOF STEP]
unfolding codegree_normalized_def
[PROOF STATE]
proof (prove)
using this:
neighbors_ss y X \<inter> neighbors_ss y' X = neighborhood y \<inter> neighborhood y'

goal (1 subgoal):
 1. real (codegree y y') / real (card X) = real (card (neighbors_ss y X \<inter> neighbors_ss y' X)) / real (card X)
[PROOF STEP]
using codegree_def codegree_neighbors
[PROOF STATE]
proof (prove)
using this:
neighbors_ss y X \<inter> neighbors_ss y' X = neighborhood y \<inter> neighborhood y'
codegree ?v ?u \<equiv> card {x \<in> V. vert_adj ?v x \<and> vert_adj ?u x}
codegree ?v ?u = card (neighborhood ?v \<inter> neighborhood ?u)

goal (1 subgoal):
 1. real (codegree y y') / real (card X) = real (card (neighbors_ss y X \<inter> neighbors_ss y' X)) / real (card X)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
codegree_normalized y y' X = real (card (neighbors_ss y X \<inter> neighbors_ss y' X)) / real (card X)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma codegree_normalized_sym: "codegree_normalized u v S = codegree_normalized v u S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codegree_normalized u v S = codegree_normalized v u S
[PROOF STEP]
unfolding codegree_normalized_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (codegree u v) / real (card S) = real (codegree v u) / real (card S)
[PROOF STEP]
using codegree_sym
[PROOF STATE]
proof (prove)
using this:
codegree ?v ?u = codegree ?u ?v

goal (1 subgoal):
 1. real (codegree u v) / real (card S) = real (codegree v u) / real (card S)
[PROOF STEP]
by simp


[STATEMENT]
lemma bad_pair_sym:
  assumes "bad_pair v u S c" shows "bad_pair u v S c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bad_pair u v S c
[PROOF STEP]
using assms bad_pair_def codegree_normalized_def
[PROOF STATE]
proof (prove)
using this:
bad_pair v u S c
bad_pair ?v ?u ?S ?c \<equiv> codegree_normalized ?v ?u ?S < ?c
codegree_normalized ?v ?u ?S \<equiv> real (codegree ?v ?u) / real (card ?S)

goal (1 subgoal):
 1. bad_pair u v S c
[PROOF STEP]
by (simp add: codegree_normalized_sym)


[STATEMENT]
lemma bad_pair_set_ss: "bad_pair_set S T c \<subseteq> S \<times> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bad_pair_set S T c \<subseteq> S \<times> S
[PROOF STEP]
by (auto simp add: bad_pair_set_def)


[STATEMENT]
lemma bad_pair_set_filter_alt:
  "bad_pair_set S T c = Set.filter (\<lambda> p . bad_pair (fst p) (snd p) T c) (S \<times> S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bad_pair_set S T c = Set.filter (\<lambda>p. bad_pair (fst p) (snd p) T c) (S \<times> S)
[PROOF STEP]
using bad_pair_set_def
[PROOF STATE]
proof (prove)
using this:
bad_pair_set ?S ?T ?c \<equiv> {(u, v). (u, v) \<in> ?S \<times> ?S \<and> bad_pair u v ?T ?c}

goal (1 subgoal):
 1. bad_pair_set S T c = Set.filter (\<lambda>p. bad_pair (fst p) (snd p) T c) (S \<times> S)
[PROOF STEP]
by auto