[STATEMENT]
lemma proj2_Col_iff_euclid:
  "proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c) \<longleftrightarrow> real_euclid.Col a b c"
  (is "proj2_Col ?p ?q ?r \<longleftrightarrow> _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c) = real_euclid.Col a b c
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c) \<Longrightarrow> real_euclid.Col a b c
 2. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
let ?a' = "vector2_append1 a"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c) \<Longrightarrow> real_euclid.Col a b c
 2. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
let ?b' = "vector2_append1 b"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c) \<Longrightarrow> real_euclid.Col a b c
 2. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
let ?c' = "vector2_append1 c"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c) \<Longrightarrow> real_euclid.Col a b c
 2. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
let ?a'' = "proj2_rep ?p"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c) \<Longrightarrow> real_euclid.Col a b c
 2. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
let ?b'' = "proj2_rep ?q"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c) \<Longrightarrow> real_euclid.Col a b c
 2. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
let ?c'' = "proj2_rep ?r"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c) \<Longrightarrow> real_euclid.Col a b c
 2. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
from proj2_pt_scalar
[PROOF STATE]
proof (chain)
picking this:
\<exists>c. c \<noteq> 0 \<and> proj2_rep (proj2_pt ?v) = c *\<^sub>R vector2_append1 ?v
[PROOF STEP]
obtain i and j and k where
    "i \<noteq> 0" and "?a'' = i *\<^sub>R ?a'"
    and "j \<noteq> 0" and "?b'' = j *\<^sub>R ?b'"
    and "k \<noteq> 0" and "?c'' = k *\<^sub>R ?c'"
[PROOF STATE]
proof (prove)
using this:
\<exists>c. c \<noteq> 0 \<and> proj2_rep (proj2_pt ?v) = c *\<^sub>R vector2_append1 ?v

goal (1 subgoal):
 1. (\<And>i j k. \<lbrakk>i \<noteq> 0; proj2_rep (proj2_pt a) = i *\<^sub>R vector2_append1 a; j \<noteq> 0; proj2_rep (proj2_pt b) = j *\<^sub>R vector2_append1 b; k \<noteq> 0; proj2_rep (proj2_pt c) = k *\<^sub>R vector2_append1 c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<noteq> 0
proj2_rep (proj2_pt a) = i *\<^sub>R vector2_append1 a
j \<noteq> 0
proj2_rep (proj2_pt b) = j *\<^sub>R vector2_append1 b
k \<noteq> 0
proj2_rep (proj2_pt c) = k *\<^sub>R vector2_append1 c

goal (2 subgoals):
 1. proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c) \<Longrightarrow> real_euclid.Col a b c
 2. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
hence "?a' = (1/i) *\<^sub>R ?a''"
    and "?b' = (1/j) *\<^sub>R ?b''"
    and "?c' = (1/k) *\<^sub>R ?c''"
[PROOF STATE]
proof (prove)
using this:
i \<noteq> 0
proj2_rep (proj2_pt a) = i *\<^sub>R vector2_append1 a
j \<noteq> 0
proj2_rep (proj2_pt b) = j *\<^sub>R vector2_append1 b
k \<noteq> 0
proj2_rep (proj2_pt c) = k *\<^sub>R vector2_append1 c

goal (1 subgoal):
 1. vector2_append1 a = (1 / i) *\<^sub>R proj2_rep (proj2_pt a) &&& vector2_append1 b = (1 / j) *\<^sub>R proj2_rep (proj2_pt b) &&& vector2_append1 c = (1 / k) *\<^sub>R proj2_rep (proj2_pt c)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
vector2_append1 a = (1 / i) *\<^sub>R proj2_rep (proj2_pt a)
vector2_append1 b = (1 / j) *\<^sub>R proj2_rep (proj2_pt b)
vector2_append1 c = (1 / k) *\<^sub>R proj2_rep (proj2_pt c)

goal (2 subgoals):
 1. proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c) \<Longrightarrow> real_euclid.Col a b c
 2. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
vector2_append1 a = (1 / i) *\<^sub>R proj2_rep (proj2_pt a)
vector2_append1 b = (1 / j) *\<^sub>R proj2_rep (proj2_pt b)
vector2_append1 c = (1 / k) *\<^sub>R proj2_rep (proj2_pt c)

goal (2 subgoals):
 1. proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c) \<Longrightarrow> real_euclid.Col a b c
 2. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
assume "proj2_Col ?p ?q ?r"
[PROOF STATE]
proof (state)
this:
proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)

goal (2 subgoals):
 1. proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c) \<Longrightarrow> real_euclid.Col a b c
 2. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
obtain i' and j' and k' where
      "i' *\<^sub>R ?a'' + j' *\<^sub>R ?b'' + k' *\<^sub>R ?c'' = 0" and "i'\<noteq>0 \<or> j'\<noteq>0 \<or> k'\<noteq>0"
[PROOF STATE]
proof (prove)
using this:
proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)

goal (1 subgoal):
 1. (\<And>i' j' k'. \<lbrakk>i' *\<^sub>R proj2_rep (proj2_pt a) + j' *\<^sub>R proj2_rep (proj2_pt b) + k' *\<^sub>R proj2_rep (proj2_pt c) = 0; i' \<noteq> 0 \<or> j' \<noteq> 0 \<or> k' \<noteq> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding proj2_Col_def
[PROOF STATE]
proof (prove)
using this:
\<exists>i j k. i *\<^sub>R proj2_rep (proj2_pt a) + j *\<^sub>R proj2_rep (proj2_pt b) + k *\<^sub>R proj2_rep (proj2_pt c) = 0 \<and> (i \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0)

goal (1 subgoal):
 1. (\<And>i' j' k'. \<lbrakk>i' *\<^sub>R proj2_rep (proj2_pt a) + j' *\<^sub>R proj2_rep (proj2_pt b) + k' *\<^sub>R proj2_rep (proj2_pt c) = 0; i' \<noteq> 0 \<or> j' \<noteq> 0 \<or> k' \<noteq> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i' *\<^sub>R proj2_rep (proj2_pt a) + j' *\<^sub>R proj2_rep (proj2_pt b) + k' *\<^sub>R proj2_rep (proj2_pt c) = 0
i' \<noteq> 0 \<or> j' \<noteq> 0 \<or> k' \<noteq> 0

goal (2 subgoals):
 1. proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c) \<Longrightarrow> real_euclid.Col a b c
 2. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
let ?i'' = "i * i'"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c) \<Longrightarrow> real_euclid.Col a b c
 2. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
let ?j'' = "j * j'"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c) \<Longrightarrow> real_euclid.Col a b c
 2. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
let ?k'' = "k * k'"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c) \<Longrightarrow> real_euclid.Col a b c
 2. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
from \<open>i\<noteq>0\<close> and \<open>j\<noteq>0\<close> and \<open>k\<noteq>0\<close> and \<open>i'\<noteq>0 \<or> j'\<noteq>0 \<or> k'\<noteq>0\<close>
[PROOF STATE]
proof (chain)
picking this:
i \<noteq> 0
j \<noteq> 0
k \<noteq> 0
i' \<noteq> 0 \<or> j' \<noteq> 0 \<or> k' \<noteq> 0
[PROOF STEP]
have "?i''\<noteq>0 \<or> ?j''\<noteq>0 \<or> ?k''\<noteq>0"
[PROOF STATE]
proof (prove)
using this:
i \<noteq> 0
j \<noteq> 0
k \<noteq> 0
i' \<noteq> 0 \<or> j' \<noteq> 0 \<or> k' \<noteq> 0

goal (1 subgoal):
 1. i * i' \<noteq> 0 \<or> j * j' \<noteq> 0 \<or> k * k' \<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i * i' \<noteq> 0 \<or> j * j' \<noteq> 0 \<or> k * k' \<noteq> 0

goal (2 subgoals):
 1. proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c) \<Longrightarrow> real_euclid.Col a b c
 2. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
from \<open>i' *\<^sub>R ?a'' + j' *\<^sub>R ?b'' + k' *\<^sub>R ?c'' = 0\<close>
      and \<open>?a'' = i *\<^sub>R ?a'\<close>
      and \<open>?b'' = j *\<^sub>R ?b'\<close>
      and \<open>?c'' = k *\<^sub>R ?c'\<close>
[PROOF STATE]
proof (chain)
picking this:
i' *\<^sub>R proj2_rep (proj2_pt a) + j' *\<^sub>R proj2_rep (proj2_pt b) + k' *\<^sub>R proj2_rep (proj2_pt c) = 0
proj2_rep (proj2_pt a) = i *\<^sub>R vector2_append1 a
proj2_rep (proj2_pt b) = j *\<^sub>R vector2_append1 b
proj2_rep (proj2_pt c) = k *\<^sub>R vector2_append1 c
[PROOF STEP]
have "?i'' *\<^sub>R ?a' + ?j'' *\<^sub>R ?b' + ?k'' *\<^sub>R ?c' = 0"
[PROOF STATE]
proof (prove)
using this:
i' *\<^sub>R proj2_rep (proj2_pt a) + j' *\<^sub>R proj2_rep (proj2_pt b) + k' *\<^sub>R proj2_rep (proj2_pt c) = 0
proj2_rep (proj2_pt a) = i *\<^sub>R vector2_append1 a
proj2_rep (proj2_pt b) = j *\<^sub>R vector2_append1 b
proj2_rep (proj2_pt c) = k *\<^sub>R vector2_append1 c

goal (1 subgoal):
 1. (i * i') *\<^sub>R vector2_append1 a + (j * j') *\<^sub>R vector2_append1 b + (k * k') *\<^sub>R vector2_append1 c = 0
[PROOF STEP]
by (simp add: ac_simps)
[PROOF STATE]
proof (state)
this:
(i * i') *\<^sub>R vector2_append1 a + (j * j') *\<^sub>R vector2_append1 b + (k * k') *\<^sub>R vector2_append1 c = 0

goal (2 subgoals):
 1. proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c) \<Longrightarrow> real_euclid.Col a b c
 2. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
hence "(?i'' *\<^sub>R ?a' + ?j'' *\<^sub>R ?b' + ?k'' *\<^sub>R ?c')$3 = 0"
[PROOF STATE]
proof (prove)
using this:
(i * i') *\<^sub>R vector2_append1 a + (j * j') *\<^sub>R vector2_append1 b + (k * k') *\<^sub>R vector2_append1 c = 0

goal (1 subgoal):
 1. ((i * i') *\<^sub>R vector2_append1 a + (j * j') *\<^sub>R vector2_append1 b + (k * k') *\<^sub>R vector2_append1 c) $ 3 = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((i * i') *\<^sub>R vector2_append1 a + (j * j') *\<^sub>R vector2_append1 b + (k * k') *\<^sub>R vector2_append1 c) $ 3 = 0

goal (2 subgoals):
 1. proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c) \<Longrightarrow> real_euclid.Col a b c
 2. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
hence "?i'' + ?j'' + ?k'' = 0"
[PROOF STATE]
proof (prove)
using this:
((i * i') *\<^sub>R vector2_append1 a + (j * j') *\<^sub>R vector2_append1 b + (k * k') *\<^sub>R vector2_append1 c) $ 3 = 0

goal (1 subgoal):
 1. i * i' + j * j' + k * k' = 0
[PROOF STEP]
unfolding vector2_append1_def and vector_def
[PROOF STATE]
proof (prove)
using this:
((i * i') *\<^sub>R vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [a $ 1, a $ 2, 1] (\<lambda>n x. 0) 1) + (j * j') *\<^sub>R vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [b $ 1, b $ 2, 1] (\<lambda>n x. 0) 1) + (k * k') *\<^sub>R vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [c $ 1, c $ 2, 1] (\<lambda>n x. 0) 1)) $ 3 = 0

goal (1 subgoal):
 1. i * i' + j * j' + k * k' = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i * i' + j * j' + k * k' = 0

goal (2 subgoals):
 1. proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c) \<Longrightarrow> real_euclid.Col a b c
 2. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
have "(?i'' *\<^sub>R ?a' + ?j'' *\<^sub>R ?b' + ?k'' *\<^sub>R ?c')$1 =
      (?i'' *\<^sub>R a + ?j'' *\<^sub>R b + ?k'' *\<^sub>R c)$1"
      and "(?i'' *\<^sub>R ?a' + ?j'' *\<^sub>R ?b' + ?k'' *\<^sub>R ?c')$2 =
      (?i'' *\<^sub>R a + ?j'' *\<^sub>R b + ?k'' *\<^sub>R c)$2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((i * i') *\<^sub>R vector2_append1 a + (j * j') *\<^sub>R vector2_append1 b + (k * k') *\<^sub>R vector2_append1 c) $ 1 = ((i * i') *\<^sub>R a + (j * j') *\<^sub>R b + (k * k') *\<^sub>R c) $ 1 &&& ((i * i') *\<^sub>R vector2_append1 a + (j * j') *\<^sub>R vector2_append1 b + (k * k') *\<^sub>R vector2_append1 c) $ 2 = ((i * i') *\<^sub>R a + (j * j') *\<^sub>R b + (k * k') *\<^sub>R c) $ 2
[PROOF STEP]
unfolding vector2_append1_def and vector_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((i * i') *\<^sub>R vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [a $ 1, a $ 2, 1] (\<lambda>n x. 0) 1) + (j * j') *\<^sub>R vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [b $ 1, b $ 2, 1] (\<lambda>n x. 0) 1) + (k * k') *\<^sub>R vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [c $ 1, c $ 2, 1] (\<lambda>n x. 0) 1)) $ 1 = ((i * i') *\<^sub>R a + (j * j') *\<^sub>R b + (k * k') *\<^sub>R c) $ 1 &&& ((i * i') *\<^sub>R vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [a $ 1, a $ 2, 1] (\<lambda>n x. 0) 1) + (j * j') *\<^sub>R vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [b $ 1, b $ 2, 1] (\<lambda>n x. 0) 1) + (k * k') *\<^sub>R vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [c $ 1, c $ 2, 1] (\<lambda>n x. 0) 1)) $ 2 = ((i * i') *\<^sub>R a + (j * j') *\<^sub>R b + (k * k') *\<^sub>R c) $ 2
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
((i * i') *\<^sub>R vector2_append1 a + (j * j') *\<^sub>R vector2_append1 b + (k * k') *\<^sub>R vector2_append1 c) $ 1 = ((i * i') *\<^sub>R a + (j * j') *\<^sub>R b + (k * k') *\<^sub>R c) $ 1
((i * i') *\<^sub>R vector2_append1 a + (j * j') *\<^sub>R vector2_append1 b + (k * k') *\<^sub>R vector2_append1 c) $ 2 = ((i * i') *\<^sub>R a + (j * j') *\<^sub>R b + (k * k') *\<^sub>R c) $ 2

goal (2 subgoals):
 1. proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c) \<Longrightarrow> real_euclid.Col a b c
 2. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
with \<open>?i'' *\<^sub>R ?a' + ?j'' *\<^sub>R ?b' + ?k'' *\<^sub>R ?c' = 0\<close>
[PROOF STATE]
proof (chain)
picking this:
(i * i') *\<^sub>R vector2_append1 a + (j * j') *\<^sub>R vector2_append1 b + (k * k') *\<^sub>R vector2_append1 c = 0
((i * i') *\<^sub>R vector2_append1 a + (j * j') *\<^sub>R vector2_append1 b + (k * k') *\<^sub>R vector2_append1 c) $ 1 = ((i * i') *\<^sub>R a + (j * j') *\<^sub>R b + (k * k') *\<^sub>R c) $ 1
((i * i') *\<^sub>R vector2_append1 a + (j * j') *\<^sub>R vector2_append1 b + (k * k') *\<^sub>R vector2_append1 c) $ 2 = ((i * i') *\<^sub>R a + (j * j') *\<^sub>R b + (k * k') *\<^sub>R c) $ 2
[PROOF STEP]
have "?i'' *\<^sub>R a + ?j'' *\<^sub>R b + ?k'' *\<^sub>R c = 0"
[PROOF STATE]
proof (prove)
using this:
(i * i') *\<^sub>R vector2_append1 a + (j * j') *\<^sub>R vector2_append1 b + (k * k') *\<^sub>R vector2_append1 c = 0
((i * i') *\<^sub>R vector2_append1 a + (j * j') *\<^sub>R vector2_append1 b + (k * k') *\<^sub>R vector2_append1 c) $ 1 = ((i * i') *\<^sub>R a + (j * j') *\<^sub>R b + (k * k') *\<^sub>R c) $ 1
((i * i') *\<^sub>R vector2_append1 a + (j * j') *\<^sub>R vector2_append1 b + (k * k') *\<^sub>R vector2_append1 c) $ 2 = ((i * i') *\<^sub>R a + (j * j') *\<^sub>R b + (k * k') *\<^sub>R c) $ 2

goal (1 subgoal):
 1. (i * i') *\<^sub>R a + (j * j') *\<^sub>R b + (k * k') *\<^sub>R c = 0
[PROOF STEP]
by (simp add: vec_eq_iff forall_2)
[PROOF STATE]
proof (state)
this:
(i * i') *\<^sub>R a + (j * j') *\<^sub>R b + (k * k') *\<^sub>R c = 0

goal (2 subgoals):
 1. proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c) \<Longrightarrow> real_euclid.Col a b c
 2. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
have "dep2 (b - a) (c - a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dep2 (b - a) (c - a)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> dep2 (b - a) (c - a)
 2. \<not> ?P \<Longrightarrow> dep2 (b - a) (c - a)
[PROOF STEP]
assume "?k'' = 0"
[PROOF STATE]
proof (state)
this:
k * k' = 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> dep2 (b - a) (c - a)
 2. \<not> ?P \<Longrightarrow> dep2 (b - a) (c - a)
[PROOF STEP]
with \<open>?i'' + ?j'' + ?k'' = 0\<close>
[PROOF STATE]
proof (chain)
picking this:
i * i' + j * j' + k * k' = 0
k * k' = 0
[PROOF STEP]
have "?j'' = -?i''"
[PROOF STATE]
proof (prove)
using this:
i * i' + j * j' + k * k' = 0
k * k' = 0

goal (1 subgoal):
 1. j * j' = - (i * i')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
j * j' = - (i * i')

goal (2 subgoals):
 1. ?P \<Longrightarrow> dep2 (b - a) (c - a)
 2. \<not> ?P \<Longrightarrow> dep2 (b - a) (c - a)
[PROOF STEP]
with \<open>?i''\<noteq>0 \<or> ?j''\<noteq>0 \<or> ?k''\<noteq>0\<close> and \<open>?k'' = 0\<close>
[PROOF STATE]
proof (chain)
picking this:
i * i' \<noteq> 0 \<or> j * j' \<noteq> 0 \<or> k * k' \<noteq> 0
k * k' = 0
j * j' = - (i * i')
[PROOF STEP]
have "?i'' \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
i * i' \<noteq> 0 \<or> j * j' \<noteq> 0 \<or> k * k' \<noteq> 0
k * k' = 0
j * j' = - (i * i')

goal (1 subgoal):
 1. i * i' \<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i * i' \<noteq> 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> dep2 (b - a) (c - a)
 2. \<not> ?P \<Longrightarrow> dep2 (b - a) (c - a)
[PROOF STEP]
from \<open>?i'' *\<^sub>R a + ?j'' *\<^sub>R b + ?k'' *\<^sub>R c = 0\<close>
        and \<open>?k'' = 0\<close> and \<open>?j'' = -?i''\<close>
[PROOF STATE]
proof (chain)
picking this:
(i * i') *\<^sub>R a + (j * j') *\<^sub>R b + (k * k') *\<^sub>R c = 0
k * k' = 0
j * j' = - (i * i')
[PROOF STEP]
have "?i'' *\<^sub>R a + (-?i'' *\<^sub>R b) = 0"
[PROOF STATE]
proof (prove)
using this:
(i * i') *\<^sub>R a + (j * j') *\<^sub>R b + (k * k') *\<^sub>R c = 0
k * k' = 0
j * j' = - (i * i')

goal (1 subgoal):
 1. (i * i') *\<^sub>R a + - (i * i') *\<^sub>R b = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(i * i') *\<^sub>R a + - (i * i') *\<^sub>R b = 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> dep2 (b - a) (c - a)
 2. \<not> ?P \<Longrightarrow> dep2 (b - a) (c - a)
[PROOF STEP]
with \<open>?i'' \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
i * i' \<noteq> 0
(i * i') *\<^sub>R a + - (i * i') *\<^sub>R b = 0
[PROOF STEP]
have "a = b"
[PROOF STATE]
proof (prove)
using this:
i * i' \<noteq> 0
(i * i') *\<^sub>R a + - (i * i') *\<^sub>R b = 0

goal (1 subgoal):
 1. a = b
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
a = b

goal (2 subgoals):
 1. ?P \<Longrightarrow> dep2 (b - a) (c - a)
 2. \<not> ?P \<Longrightarrow> dep2 (b - a) (c - a)
[PROOF STEP]
hence "b - a = 0 *\<^sub>R (c - a)"
[PROOF STATE]
proof (prove)
using this:
a = b

goal (1 subgoal):
 1. b - a = 0 *\<^sub>R (c - a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b - a = 0 *\<^sub>R (c - a)

goal (2 subgoals):
 1. ?P \<Longrightarrow> dep2 (b - a) (c - a)
 2. \<not> ?P \<Longrightarrow> dep2 (b - a) (c - a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
b - a = 0 *\<^sub>R (c - a)

goal (2 subgoals):
 1. ?P \<Longrightarrow> dep2 (b - a) (c - a)
 2. \<not> ?P \<Longrightarrow> dep2 (b - a) (c - a)
[PROOF STEP]
have "c - a = 1 *\<^sub>R (c - a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c - a = 1 *\<^sub>R (c - a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c - a = 1 *\<^sub>R (c - a)

goal (2 subgoals):
 1. ?P \<Longrightarrow> dep2 (b - a) (c - a)
 2. \<not> ?P \<Longrightarrow> dep2 (b - a) (c - a)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
b - a = 0 *\<^sub>R (c - a)
c - a = 1 *\<^sub>R (c - a)
[PROOF STEP]
have "\<exists> x t s. b - a = t *\<^sub>R x \<and> c - a = s *\<^sub>R x"
[PROOF STATE]
proof (prove)
using this:
b - a = 0 *\<^sub>R (c - a)
c - a = 1 *\<^sub>R (c - a)

goal (1 subgoal):
 1. \<exists>x t s. b - a = t *\<^sub>R x \<and> c - a = s *\<^sub>R x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x t s. b - a = t *\<^sub>R x \<and> c - a = s *\<^sub>R x

goal (2 subgoals):
 1. ?P \<Longrightarrow> dep2 (b - a) (c - a)
 2. \<not> ?P \<Longrightarrow> dep2 (b - a) (c - a)
[PROOF STEP]
thus "dep2 (b - a) (c - a)"
[PROOF STATE]
proof (prove)
using this:
\<exists>x t s. b - a = t *\<^sub>R x \<and> c - a = s *\<^sub>R x

goal (1 subgoal):
 1. dep2 (b - a) (c - a)
[PROOF STEP]
unfolding dep2_def
[PROOF STATE]
proof (prove)
using this:
\<exists>x t s. b - a = t *\<^sub>R x \<and> c - a = s *\<^sub>R x

goal (1 subgoal):
 1. \<exists>w r s. b - a = r *\<^sub>R w \<and> c - a = s *\<^sub>R w
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
dep2 (b - a) (c - a)

goal (1 subgoal):
 1. k * k' \<noteq> 0 \<Longrightarrow> dep2 (b - a) (c - a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k * k' \<noteq> 0 \<Longrightarrow> dep2 (b - a) (c - a)
[PROOF STEP]
assume "?k'' \<noteq> 0"
[PROOF STATE]
proof (state)
this:
k * k' \<noteq> 0

goal (1 subgoal):
 1. k * k' \<noteq> 0 \<Longrightarrow> dep2 (b - a) (c - a)
[PROOF STEP]
from \<open>?i'' + ?j'' + ?k'' = 0\<close>
[PROOF STATE]
proof (chain)
picking this:
i * i' + j * j' + k * k' = 0
[PROOF STEP]
have "?i'' = -(?j'' + ?k'')"
[PROOF STATE]
proof (prove)
using this:
i * i' + j * j' + k * k' = 0

goal (1 subgoal):
 1. i * i' = - (j * j' + k * k')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i * i' = - (j * j' + k * k')

goal (1 subgoal):
 1. k * k' \<noteq> 0 \<Longrightarrow> dep2 (b - a) (c - a)
[PROOF STEP]
with \<open>?i'' *\<^sub>R a + ?j'' *\<^sub>R b + ?k'' *\<^sub>R c = 0\<close>
[PROOF STATE]
proof (chain)
picking this:
(i * i') *\<^sub>R a + (j * j') *\<^sub>R b + (k * k') *\<^sub>R c = 0
i * i' = - (j * j' + k * k')
[PROOF STEP]
have "-(?j'' + ?k'') *\<^sub>R a + ?j'' *\<^sub>R b + ?k'' *\<^sub>R c = 0"
[PROOF STATE]
proof (prove)
using this:
(i * i') *\<^sub>R a + (j * j') *\<^sub>R b + (k * k') *\<^sub>R c = 0
i * i' = - (j * j' + k * k')

goal (1 subgoal):
 1. - (j * j' + k * k') *\<^sub>R a + (j * j') *\<^sub>R b + (k * k') *\<^sub>R c = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- (j * j' + k * k') *\<^sub>R a + (j * j') *\<^sub>R b + (k * k') *\<^sub>R c = 0

goal (1 subgoal):
 1. k * k' \<noteq> 0 \<Longrightarrow> dep2 (b - a) (c - a)
[PROOF STEP]
hence "?k'' *\<^sub>R (c - a) = - ?j'' *\<^sub>R (b - a)"
[PROOF STATE]
proof (prove)
using this:
- (j * j' + k * k') *\<^sub>R a + (j * j') *\<^sub>R b + (k * k') *\<^sub>R c = 0

goal (1 subgoal):
 1. (k * k') *\<^sub>R (c - a) = - (j * j') *\<^sub>R (b - a)
[PROOF STEP]
by (simp add: scaleR_left_distrib
          scaleR_right_diff_distrib
          scaleR_left_diff_distrib
          algebra_simps)
[PROOF STATE]
proof (state)
this:
(k * k') *\<^sub>R (c - a) = - (j * j') *\<^sub>R (b - a)

goal (1 subgoal):
 1. k * k' \<noteq> 0 \<Longrightarrow> dep2 (b - a) (c - a)
[PROOF STEP]
hence "(1/?k'') *\<^sub>R ?k'' *\<^sub>R (c - a) = (-?j'' / ?k'') *\<^sub>R (b - a)"
[PROOF STATE]
proof (prove)
using this:
(k * k') *\<^sub>R (c - a) = - (j * j') *\<^sub>R (b - a)

goal (1 subgoal):
 1. (1 / (k * k')) *\<^sub>R (k * k') *\<^sub>R (c - a) = (- (j * j') / (k * k')) *\<^sub>R (b - a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(1 / (k * k')) *\<^sub>R (k * k') *\<^sub>R (c - a) = (- (j * j') / (k * k')) *\<^sub>R (b - a)

goal (1 subgoal):
 1. k * k' \<noteq> 0 \<Longrightarrow> dep2 (b - a) (c - a)
[PROOF STEP]
with \<open>?k'' \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
k * k' \<noteq> 0
(1 / (k * k')) *\<^sub>R (k * k') *\<^sub>R (c - a) = (- (j * j') / (k * k')) *\<^sub>R (b - a)
[PROOF STEP]
have "c - a = (-?j'' / ?k'') *\<^sub>R (b - a)"
[PROOF STATE]
proof (prove)
using this:
k * k' \<noteq> 0
(1 / (k * k')) *\<^sub>R (k * k') *\<^sub>R (c - a) = (- (j * j') / (k * k')) *\<^sub>R (b - a)

goal (1 subgoal):
 1. c - a = (- (j * j') / (k * k')) *\<^sub>R (b - a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c - a = (- (j * j') / (k * k')) *\<^sub>R (b - a)

goal (1 subgoal):
 1. k * k' \<noteq> 0 \<Longrightarrow> dep2 (b - a) (c - a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c - a = (- (j * j') / (k * k')) *\<^sub>R (b - a)

goal (1 subgoal):
 1. k * k' \<noteq> 0 \<Longrightarrow> dep2 (b - a) (c - a)
[PROOF STEP]
have "b - a = 1 *\<^sub>R (b - a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b - a = 1 *\<^sub>R (b - a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b - a = 1 *\<^sub>R (b - a)

goal (1 subgoal):
 1. k * k' \<noteq> 0 \<Longrightarrow> dep2 (b - a) (c - a)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
c - a = (- (j * j') / (k * k')) *\<^sub>R (b - a)
b - a = 1 *\<^sub>R (b - a)
[PROOF STEP]
have "\<exists> x t s. b - a = t *\<^sub>R x \<and> c - a = s *\<^sub>R x"
[PROOF STATE]
proof (prove)
using this:
c - a = (- (j * j') / (k * k')) *\<^sub>R (b - a)
b - a = 1 *\<^sub>R (b - a)

goal (1 subgoal):
 1. \<exists>x t s. b - a = t *\<^sub>R x \<and> c - a = s *\<^sub>R x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x t s. b - a = t *\<^sub>R x \<and> c - a = s *\<^sub>R x

goal (1 subgoal):
 1. k * k' \<noteq> 0 \<Longrightarrow> dep2 (b - a) (c - a)
[PROOF STEP]
thus "dep2 (b - a) (c - a)"
[PROOF STATE]
proof (prove)
using this:
\<exists>x t s. b - a = t *\<^sub>R x \<and> c - a = s *\<^sub>R x

goal (1 subgoal):
 1. dep2 (b - a) (c - a)
[PROOF STEP]
unfolding dep2_def
[PROOF STATE]
proof (prove)
using this:
\<exists>x t s. b - a = t *\<^sub>R x \<and> c - a = s *\<^sub>R x

goal (1 subgoal):
 1. \<exists>w r s. b - a = r *\<^sub>R w \<and> c - a = s *\<^sub>R w
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
dep2 (b - a) (c - a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
dep2 (b - a) (c - a)

goal (2 subgoals):
 1. proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c) \<Longrightarrow> real_euclid.Col a b c
 2. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
with Col_dep2
[PROOF STATE]
proof (chain)
picking this:
real_euclid.Col ?a ?b ?c = dep2 (?b - ?a) (?c - ?a)
dep2 (b - a) (c - a)
[PROOF STEP]
show "real_euclid.Col a b c"
[PROOF STATE]
proof (prove)
using this:
real_euclid.Col ?a ?b ?c = dep2 (?b - ?a) (?c - ?a)
dep2 (b - a) (c - a)

goal (1 subgoal):
 1. real_euclid.Col a b c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_euclid.Col a b c

goal (1 subgoal):
 1. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c) \<Longrightarrow> real_euclid.Col a b c

goal (1 subgoal):
 1. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c) \<Longrightarrow> real_euclid.Col a b c

goal (1 subgoal):
 1. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
assume "real_euclid.Col a b c"
[PROOF STATE]
proof (state)
this:
real_euclid.Col a b c

goal (1 subgoal):
 1. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
with Col_dep2
[PROOF STATE]
proof (chain)
picking this:
real_euclid.Col ?a ?b ?c = dep2 (?b - ?a) (?c - ?a)
real_euclid.Col a b c
[PROOF STEP]
have "dep2 (b - a) (c - a)"
[PROOF STATE]
proof (prove)
using this:
real_euclid.Col ?a ?b ?c = dep2 (?b - ?a) (?c - ?a)
real_euclid.Col a b c

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

goal (1 subgoal):
 1. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dep2 (b - a) (c - a)
[PROOF STEP]
obtain x and t and s where "b - a = t *\<^sub>R x" and "c - a = s *\<^sub>R x"
[PROOF STATE]
proof (prove)
using this:
dep2 (b - a) (c - a)

goal (1 subgoal):
 1. (\<And>t x s. \<lbrakk>b - a = t *\<^sub>R x; c - a = s *\<^sub>R x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding dep2_def
[PROOF STATE]
proof (prove)
using this:
\<exists>w r s. b - a = r *\<^sub>R w \<and> c - a = s *\<^sub>R w

goal (1 subgoal):
 1. (\<And>t x s. \<lbrakk>b - a = t *\<^sub>R x; c - a = s *\<^sub>R x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b - a = t *\<^sub>R x
c - a = s *\<^sub>R x

goal (1 subgoal):
 1. real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
show "proj2_Col ?p ?q ?r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
 2. \<not> ?P \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
assume "t = 0"
[PROOF STATE]
proof (state)
this:
t = 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
 2. \<not> ?P \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
with \<open>b - a = t *\<^sub>R x\<close>
[PROOF STATE]
proof (chain)
picking this:
b - a = t *\<^sub>R x
t = 0
[PROOF STEP]
have "a = b"
[PROOF STATE]
proof (prove)
using this:
b - a = t *\<^sub>R x
t = 0

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
 2. \<not> ?P \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
with proj2_Col_coincide
[PROOF STATE]
proof (chain)
picking this:
proj2_Col ?a ?a ?c
a = b
[PROOF STEP]
show "proj2_Col ?p ?q ?r"
[PROOF STATE]
proof (prove)
using this:
proj2_Col ?a ?a ?c
a = b

goal (1 subgoal):
 1. proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)

goal (1 subgoal):
 1. t \<noteq> 0 \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t \<noteq> 0 \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
assume "t \<noteq> 0"
[PROOF STATE]
proof (state)
this:
t \<noteq> 0

goal (1 subgoal):
 1. t \<noteq> 0 \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
from \<open>b - a = t *\<^sub>R x\<close> and \<open>c - a = s *\<^sub>R x\<close>
[PROOF STATE]
proof (chain)
picking this:
b - a = t *\<^sub>R x
c - a = s *\<^sub>R x
[PROOF STEP]
have "s *\<^sub>R (b - a) = t *\<^sub>R (c - a)"
[PROOF STATE]
proof (prove)
using this:
b - a = t *\<^sub>R x
c - a = s *\<^sub>R x

goal (1 subgoal):
 1. s *\<^sub>R (b - a) = t *\<^sub>R (c - a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s *\<^sub>R (b - a) = t *\<^sub>R (c - a)

goal (1 subgoal):
 1. t \<noteq> 0 \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
hence "(s - t) *\<^sub>R a + (-s) *\<^sub>R b + t *\<^sub>R c = 0"
[PROOF STATE]
proof (prove)
using this:
s *\<^sub>R (b - a) = t *\<^sub>R (c - a)

goal (1 subgoal):
 1. (s - t) *\<^sub>R a + - s *\<^sub>R b + t *\<^sub>R c = 0
[PROOF STEP]
by (simp add: scaleR_right_diff_distrib
          scaleR_left_diff_distrib
          algebra_simps)
[PROOF STATE]
proof (state)
this:
(s - t) *\<^sub>R a + - s *\<^sub>R b + t *\<^sub>R c = 0

goal (1 subgoal):
 1. t \<noteq> 0 \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
hence "((s - t) *\<^sub>R ?a' + (-s) *\<^sub>R ?b' + t *\<^sub>R ?c')$1 = 0"
        and "((s - t) *\<^sub>R ?a' + (-s) *\<^sub>R ?b' + t *\<^sub>R ?c')$2 = 0"
[PROOF STATE]
proof (prove)
using this:
(s - t) *\<^sub>R a + - s *\<^sub>R b + t *\<^sub>R c = 0

goal (1 subgoal):
 1. ((s - t) *\<^sub>R vector2_append1 a + - s *\<^sub>R vector2_append1 b + t *\<^sub>R vector2_append1 c) $ 1 = 0 &&& ((s - t) *\<^sub>R vector2_append1 a + - s *\<^sub>R vector2_append1 b + t *\<^sub>R vector2_append1 c) $ 2 = 0
[PROOF STEP]
unfolding vector2_append1_def and vector_def
[PROOF STATE]
proof (prove)
using this:
(s - t) *\<^sub>R a + - s *\<^sub>R b + t *\<^sub>R c = 0

goal (1 subgoal):
 1. ((s - t) *\<^sub>R vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [a $ 1, a $ 2, 1] (\<lambda>n x. 0) 1) + - s *\<^sub>R vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [b $ 1, b $ 2, 1] (\<lambda>n x. 0) 1) + t *\<^sub>R vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [c $ 1, c $ 2, 1] (\<lambda>n x. 0) 1)) $ 1 = 0 &&& ((s - t) *\<^sub>R vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [a $ 1, a $ 2, 1] (\<lambda>n x. 0) 1) + - s *\<^sub>R vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [b $ 1, b $ 2, 1] (\<lambda>n x. 0) 1) + t *\<^sub>R vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [c $ 1, c $ 2, 1] (\<lambda>n x. 0) 1)) $ 2 = 0
[PROOF STEP]
by (simp_all add: vec_eq_iff)
[PROOF STATE]
proof (state)
this:
((s - t) *\<^sub>R vector2_append1 a + - s *\<^sub>R vector2_append1 b + t *\<^sub>R vector2_append1 c) $ 1 = 0
((s - t) *\<^sub>R vector2_append1 a + - s *\<^sub>R vector2_append1 b + t *\<^sub>R vector2_append1 c) $ 2 = 0

goal (1 subgoal):
 1. t \<noteq> 0 \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
((s - t) *\<^sub>R vector2_append1 a + - s *\<^sub>R vector2_append1 b + t *\<^sub>R vector2_append1 c) $ 1 = 0
((s - t) *\<^sub>R vector2_append1 a + - s *\<^sub>R vector2_append1 b + t *\<^sub>R vector2_append1 c) $ 2 = 0

goal (1 subgoal):
 1. t \<noteq> 0 \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
have "((s - t) *\<^sub>R ?a' + (-s) *\<^sub>R ?b' + t *\<^sub>R ?c')$3 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((s - t) *\<^sub>R vector2_append1 a + - s *\<^sub>R vector2_append1 b + t *\<^sub>R vector2_append1 c) $ 3 = 0
[PROOF STEP]
unfolding vector2_append1_def and vector_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((s - t) *\<^sub>R vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [a $ 1, a $ 2, 1] (\<lambda>n x. 0) 1) + - s *\<^sub>R vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [b $ 1, b $ 2, 1] (\<lambda>n x. 0) 1) + t *\<^sub>R vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [c $ 1, c $ 2, 1] (\<lambda>n x. 0) 1)) $ 3 = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((s - t) *\<^sub>R vector2_append1 a + - s *\<^sub>R vector2_append1 b + t *\<^sub>R vector2_append1 c) $ 3 = 0

goal (1 subgoal):
 1. t \<noteq> 0 \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
((s - t) *\<^sub>R vector2_append1 a + - s *\<^sub>R vector2_append1 b + t *\<^sub>R vector2_append1 c) $ 1 = 0
((s - t) *\<^sub>R vector2_append1 a + - s *\<^sub>R vector2_append1 b + t *\<^sub>R vector2_append1 c) $ 2 = 0
((s - t) *\<^sub>R vector2_append1 a + - s *\<^sub>R vector2_append1 b + t *\<^sub>R vector2_append1 c) $ 3 = 0
[PROOF STEP]
have "(s - t) *\<^sub>R ?a' + (-s) *\<^sub>R ?b' + t *\<^sub>R ?c' = 0"
[PROOF STATE]
proof (prove)
using this:
((s - t) *\<^sub>R vector2_append1 a + - s *\<^sub>R vector2_append1 b + t *\<^sub>R vector2_append1 c) $ 1 = 0
((s - t) *\<^sub>R vector2_append1 a + - s *\<^sub>R vector2_append1 b + t *\<^sub>R vector2_append1 c) $ 2 = 0
((s - t) *\<^sub>R vector2_append1 a + - s *\<^sub>R vector2_append1 b + t *\<^sub>R vector2_append1 c) $ 3 = 0

goal (1 subgoal):
 1. (s - t) *\<^sub>R vector2_append1 a + - s *\<^sub>R vector2_append1 b + t *\<^sub>R vector2_append1 c = 0
[PROOF STEP]
by (simp add: vec_eq_iff forall_3)
[PROOF STATE]
proof (state)
this:
(s - t) *\<^sub>R vector2_append1 a + - s *\<^sub>R vector2_append1 b + t *\<^sub>R vector2_append1 c = 0

goal (1 subgoal):
 1. t \<noteq> 0 \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
with \<open>?a' = (1/i) *\<^sub>R ?a''\<close>
        and \<open>?b' = (1/j) *\<^sub>R ?b''\<close>
        and \<open>?c' = (1/k) *\<^sub>R ?c''\<close>
[PROOF STATE]
proof (chain)
picking this:
vector2_append1 a = (1 / i) *\<^sub>R proj2_rep (proj2_pt a)
vector2_append1 b = (1 / j) *\<^sub>R proj2_rep (proj2_pt b)
vector2_append1 c = (1 / k) *\<^sub>R proj2_rep (proj2_pt c)
(s - t) *\<^sub>R vector2_append1 a + - s *\<^sub>R vector2_append1 b + t *\<^sub>R vector2_append1 c = 0
[PROOF STEP]
have "((s - t)/i) *\<^sub>R ?a'' + (-s/j) *\<^sub>R ?b'' + (t/k) *\<^sub>R ?c'' = 0"
[PROOF STATE]
proof (prove)
using this:
vector2_append1 a = (1 / i) *\<^sub>R proj2_rep (proj2_pt a)
vector2_append1 b = (1 / j) *\<^sub>R proj2_rep (proj2_pt b)
vector2_append1 c = (1 / k) *\<^sub>R proj2_rep (proj2_pt c)
(s - t) *\<^sub>R vector2_append1 a + - s *\<^sub>R vector2_append1 b + t *\<^sub>R vector2_append1 c = 0

goal (1 subgoal):
 1. ((s - t) / i) *\<^sub>R proj2_rep (proj2_pt a) + (- s / j) *\<^sub>R proj2_rep (proj2_pt b) + (t / k) *\<^sub>R proj2_rep (proj2_pt c) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((s - t) / i) *\<^sub>R proj2_rep (proj2_pt a) + (- s / j) *\<^sub>R proj2_rep (proj2_pt b) + (t / k) *\<^sub>R proj2_rep (proj2_pt c) = 0

goal (1 subgoal):
 1. t \<noteq> 0 \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
((s - t) / i) *\<^sub>R proj2_rep (proj2_pt a) + (- s / j) *\<^sub>R proj2_rep (proj2_pt b) + (t / k) *\<^sub>R proj2_rep (proj2_pt c) = 0

goal (1 subgoal):
 1. t \<noteq> 0 \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
from \<open>t \<noteq> 0\<close> and \<open>k \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
t \<noteq> 0
k \<noteq> 0
[PROOF STEP]
have "t/k \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
t \<noteq> 0
k \<noteq> 0

goal (1 subgoal):
 1. t / k \<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t / k \<noteq> 0

goal (1 subgoal):
 1. t \<noteq> 0 \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
((s - t) / i) *\<^sub>R proj2_rep (proj2_pt a) + (- s / j) *\<^sub>R proj2_rep (proj2_pt b) + (t / k) *\<^sub>R proj2_rep (proj2_pt c) = 0
t / k \<noteq> 0
[PROOF STEP]
show "proj2_Col ?p ?q ?r"
[PROOF STATE]
proof (prove)
using this:
((s - t) / i) *\<^sub>R proj2_rep (proj2_pt a) + (- s / j) *\<^sub>R proj2_rep (proj2_pt b) + (t / k) *\<^sub>R proj2_rep (proj2_pt c) = 0
t / k \<noteq> 0

goal (1 subgoal):
 1. proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)
[PROOF STEP]
unfolding proj2_Col_def
[PROOF STATE]
proof (prove)
using this:
((s - t) / i) *\<^sub>R proj2_rep (proj2_pt a) + (- s / j) *\<^sub>R proj2_rep (proj2_pt b) + (t / k) *\<^sub>R proj2_rep (proj2_pt c) = 0
t / k \<noteq> 0

goal (1 subgoal):
 1. \<exists>i j k. i *\<^sub>R proj2_rep (proj2_pt a) + j *\<^sub>R proj2_rep (proj2_pt b) + k *\<^sub>R proj2_rep (proj2_pt c) = 0 \<and> (i \<noteq> 0 \<or> j \<noteq> 0 \<or> k \<noteq> 0)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
real_euclid.Col a b c \<Longrightarrow> proj2_Col (proj2_pt a) (proj2_pt b) (proj2_pt c)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_Col_iff_euclid_cart2:
  assumes "z_non_zero p" and "z_non_zero q" and "z_non_zero r"
  shows
  "proj2_Col p q r \<longleftrightarrow> real_euclid.Col (cart2_pt p) (cart2_pt q) (cart2_pt r)"
  (is "_ \<longleftrightarrow> real_euclid.Col ?a ?b ?c")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_Col p q r = real_euclid.Col (cart2_pt p) (cart2_pt q) (cart2_pt r)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj2_Col p q r = real_euclid.Col (cart2_pt p) (cart2_pt q) (cart2_pt r)
[PROOF STEP]
from \<open>z_non_zero p\<close> and \<open>z_non_zero q\<close> and \<open>z_non_zero r\<close>
[PROOF STATE]
proof (chain)
picking this:
z_non_zero p
z_non_zero q
z_non_zero r
[PROOF STEP]
have "proj2_pt ?a = p" and "proj2_pt ?b = q" and "proj2_pt ?c = r"
[PROOF STATE]
proof (prove)
using this:
z_non_zero p
z_non_zero q
z_non_zero r

goal (1 subgoal):
 1. proj2_pt (cart2_pt p) = p &&& proj2_pt (cart2_pt q) = q &&& proj2_pt (cart2_pt r) = r
[PROOF STEP]
by (simp_all add: proj2_cart2)
[PROOF STATE]
proof (state)
this:
proj2_pt (cart2_pt p) = p
proj2_pt (cart2_pt q) = q
proj2_pt (cart2_pt r) = r

goal (1 subgoal):
 1. proj2_Col p q r = real_euclid.Col (cart2_pt p) (cart2_pt q) (cart2_pt r)
[PROOF STEP]
with proj2_Col_iff_euclid [of ?a ?b ?c]
[PROOF STATE]
proof (chain)
picking this:
proj2_Col (proj2_pt (cart2_pt p)) (proj2_pt (cart2_pt q)) (proj2_pt (cart2_pt r)) = real_euclid.Col (cart2_pt p) (cart2_pt q) (cart2_pt r)
proj2_pt (cart2_pt p) = p
proj2_pt (cart2_pt q) = q
proj2_pt (cart2_pt r) = r
[PROOF STEP]
show "proj2_Col p q r \<longleftrightarrow> real_euclid.Col ?a ?b ?c"
[PROOF STATE]
proof (prove)
using this:
proj2_Col (proj2_pt (cart2_pt p)) (proj2_pt (cart2_pt q)) (proj2_pt (cart2_pt r)) = real_euclid.Col (cart2_pt p) (cart2_pt q) (cart2_pt r)
proj2_pt (cart2_pt p) = p
proj2_pt (cart2_pt q) = q
proj2_pt (cart2_pt r) = r

goal (1 subgoal):
 1. proj2_Col p q r = real_euclid.Col (cart2_pt p) (cart2_pt q) (cart2_pt r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_Col p q r = real_euclid.Col (cart2_pt p) (cart2_pt q) (cart2_pt r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma euclid_Col_cart2_incident:
  assumes "z_non_zero p" and "z_non_zero q" and "z_non_zero r" and "p \<noteq> q"
  and "proj2_incident p l" and "proj2_incident q l"
  and "real_euclid.Col (cart2_pt p) (cart2_pt q) (cart2_pt r)"
  (is "real_euclid.Col ?cp ?cq ?cr")
  shows "proj2_incident r l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_incident r l
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj2_incident r l
[PROOF STEP]
from \<open>z_non_zero p\<close> and \<open>z_non_zero q\<close> and \<open>z_non_zero r\<close>
    and \<open>real_euclid.Col ?cp ?cq ?cr\<close>
[PROOF STATE]
proof (chain)
picking this:
z_non_zero p
z_non_zero q
z_non_zero r
real_euclid.Col (cart2_pt p) (cart2_pt q) (cart2_pt r)
[PROOF STEP]
have "proj2_Col p q r"
[PROOF STATE]
proof (prove)
using this:
z_non_zero p
z_non_zero q
z_non_zero r
real_euclid.Col (cart2_pt p) (cart2_pt q) (cart2_pt r)

goal (1 subgoal):
 1. proj2_Col p q r
[PROOF STEP]
by (subst proj2_Col_iff_euclid_cart2, simp_all)
[PROOF STATE]
proof (state)
this:
proj2_Col p q r

goal (1 subgoal):
 1. proj2_incident r l
[PROOF STEP]
hence "proj2_set_Col {p,q,r}"
[PROOF STATE]
proof (prove)
using this:
proj2_Col p q r

goal (1 subgoal):
 1. proj2_set_Col {p, q, r}
[PROOF STEP]
by (simp add: proj2_Col_iff_set_Col)
[PROOF STATE]
proof (state)
this:
proj2_set_Col {p, q, r}

goal (1 subgoal):
 1. proj2_incident r l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
proj2_set_Col {p, q, r}
[PROOF STEP]
obtain m where
    "proj2_incident p m" and "proj2_incident q m" and "proj2_incident r m"
[PROOF STATE]
proof (prove)
using this:
proj2_set_Col {p, q, r}

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>proj2_incident p m; proj2_incident q m; proj2_incident r m\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (unfold proj2_set_Col_def, auto)
[PROOF STATE]
proof (state)
this:
proj2_incident p m
proj2_incident q m
proj2_incident r m

goal (1 subgoal):
 1. proj2_incident r l
[PROOF STEP]
from \<open>p \<noteq> q\<close> and \<open>proj2_incident p l\<close> and \<open>proj2_incident q l\<close>
    and \<open>proj2_incident p m\<close> and \<open>proj2_incident q m\<close> and proj2_incident_unique
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> q
proj2_incident p l
proj2_incident q l
proj2_incident p m
proj2_incident q m
\<lbrakk>proj2_incident ?p ?l; proj2_incident ?q ?l; proj2_incident ?p ?m; proj2_incident ?q ?m\<rbrakk> \<Longrightarrow> ?p = ?q \<or> ?l = ?m
[PROOF STEP]
have "l = m"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> q
proj2_incident p l
proj2_incident q l
proj2_incident p m
proj2_incident q m
\<lbrakk>proj2_incident ?p ?l; proj2_incident ?q ?l; proj2_incident ?p ?m; proj2_incident ?q ?m\<rbrakk> \<Longrightarrow> ?p = ?q \<or> ?l = ?m

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

goal (1 subgoal):
 1. proj2_incident r l
[PROOF STEP]
with \<open>proj2_incident r m\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_incident r m
l = m
[PROOF STEP]
show "proj2_incident r l"
[PROOF STATE]
proof (prove)
using this:
proj2_incident r m
l = m

goal (1 subgoal):
 1. proj2_incident r l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_incident r l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma euclid_B_cart2_common_line:
  assumes "z_non_zero p" and "z_non_zero q" and "z_non_zero r"
  and "B\<^sub>\<real> (cart2_pt p) (cart2_pt q) (cart2_pt r)"
  (is "B\<^sub>\<real> ?cp ?cq ?cr")
  shows "\<exists> l. proj2_incident p l \<and> proj2_incident q l \<and> proj2_incident r l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. proj2_incident p l \<and> proj2_incident q l \<and> proj2_incident r l
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>l. proj2_incident p l \<and> proj2_incident q l \<and> proj2_incident r l
[PROOF STEP]
from \<open>z_non_zero p\<close> and \<open>z_non_zero q\<close> and \<open>z_non_zero r\<close>
    and \<open>B\<^sub>\<real> ?cp ?cq ?cr\<close> and proj2_Col_iff_euclid_cart2
[PROOF STATE]
proof (chain)
picking this:
z_non_zero p
z_non_zero q
z_non_zero r
B\<^sub>\<real> cart2_pt p cart2_pt q cart2_pt r
\<lbrakk>z_non_zero ?p; z_non_zero ?q; z_non_zero ?r\<rbrakk> \<Longrightarrow> proj2_Col ?p ?q ?r = real_euclid.Col (cart2_pt ?p) (cart2_pt ?q) (cart2_pt ?r)
[PROOF STEP]
have "proj2_Col p q r"
[PROOF STATE]
proof (prove)
using this:
z_non_zero p
z_non_zero q
z_non_zero r
B\<^sub>\<real> cart2_pt p cart2_pt q cart2_pt r
\<lbrakk>z_non_zero ?p; z_non_zero ?q; z_non_zero ?r\<rbrakk> \<Longrightarrow> proj2_Col ?p ?q ?r = real_euclid.Col (cart2_pt ?p) (cart2_pt ?q) (cart2_pt ?r)

goal (1 subgoal):
 1. proj2_Col p q r
[PROOF STEP]
by (unfold real_euclid.Col_def) simp
[PROOF STATE]
proof (state)
this:
proj2_Col p q r

goal (1 subgoal):
 1. \<exists>l. proj2_incident p l \<and> proj2_incident q l \<and> proj2_incident r l
[PROOF STEP]
hence "proj2_set_Col {p,q,r}"
[PROOF STATE]
proof (prove)
using this:
proj2_Col p q r

goal (1 subgoal):
 1. proj2_set_Col {p, q, r}
[PROOF STEP]
by (simp add: proj2_Col_iff_set_Col)
[PROOF STATE]
proof (state)
this:
proj2_set_Col {p, q, r}

goal (1 subgoal):
 1. \<exists>l. proj2_incident p l \<and> proj2_incident q l \<and> proj2_incident r l
[PROOF STEP]
thus "\<exists> l. proj2_incident p l \<and> proj2_incident q l \<and> proj2_incident r l"
[PROOF STATE]
proof (prove)
using this:
proj2_set_Col {p, q, r}

goal (1 subgoal):
 1. \<exists>l. proj2_incident p l \<and> proj2_incident q l \<and> proj2_incident r l
[PROOF STEP]
by (unfold proj2_set_Col_def) simp
[PROOF STATE]
proof (state)
this:
\<exists>l. proj2_incident p l \<and> proj2_incident q l \<and> proj2_incident r l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cart2_append1_between:
  assumes "z_non_zero p" and "z_non_zero q" and "z_non_zero r"
  shows "B\<^sub>\<real> (cart2_pt p) (cart2_pt q) (cart2_pt r)
  \<longleftrightarrow> (\<exists> k\<ge>0. k \<le> 1
  \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (B\<^sub>\<real> cart2_pt p cart2_pt q cart2_pt r) = (\<exists>k\<ge>0. k \<le> 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (B\<^sub>\<real> cart2_pt p cart2_pt q cart2_pt r) = (\<exists>k\<ge>0. k \<le> 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p)
[PROOF STEP]
let ?cp = "cart2_pt p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (B\<^sub>\<real> cart2_pt p cart2_pt q cart2_pt r) = (\<exists>k\<ge>0. k \<le> 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p)
[PROOF STEP]
let ?cq = "cart2_pt q"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (B\<^sub>\<real> cart2_pt p cart2_pt q cart2_pt r) = (\<exists>k\<ge>0. k \<le> 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p)
[PROOF STEP]
let ?cr = "cart2_pt r"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (B\<^sub>\<real> cart2_pt p cart2_pt q cart2_pt r) = (\<exists>k\<ge>0. k \<le> 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p)
[PROOF STEP]
let ?cp1 = "vector2_append1 ?cp"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (B\<^sub>\<real> cart2_pt p cart2_pt q cart2_pt r) = (\<exists>k\<ge>0. k \<le> 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p)
[PROOF STEP]
let ?cq1 = "vector2_append1 ?cq"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (B\<^sub>\<real> cart2_pt p cart2_pt q cart2_pt r) = (\<exists>k\<ge>0. k \<le> 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p)
[PROOF STEP]
let ?cr1 = "vector2_append1 ?cr"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (B\<^sub>\<real> cart2_pt p cart2_pt q cart2_pt r) = (\<exists>k\<ge>0. k \<le> 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p)
[PROOF STEP]
from \<open>z_non_zero p\<close> and \<open>z_non_zero q\<close> and \<open>z_non_zero r\<close>
[PROOF STATE]
proof (chain)
picking this:
z_non_zero p
z_non_zero q
z_non_zero r
[PROOF STEP]
have "?cp1 = cart2_append1 p"
    and "?cq1 = cart2_append1 q"
    and "?cr1 = cart2_append1 r"
[PROOF STATE]
proof (prove)
using this:
z_non_zero p
z_non_zero q
z_non_zero r

goal (1 subgoal):
 1. vector2_append1 (cart2_pt p) = cart2_append1 p &&& vector2_append1 (cart2_pt q) = cart2_append1 q &&& vector2_append1 (cart2_pt r) = cart2_append1 r
[PROOF STEP]
by (simp_all add: cart2_append1)
[PROOF STATE]
proof (state)
this:
vector2_append1 (cart2_pt p) = cart2_append1 p
vector2_append1 (cart2_pt q) = cart2_append1 q
vector2_append1 (cart2_pt r) = cart2_append1 r

goal (1 subgoal):
 1. (B\<^sub>\<real> cart2_pt p cart2_pt q cart2_pt r) = (\<exists>k\<ge>0. k \<le> 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p)
[PROOF STEP]
have "\<forall> k. ?cq - ?cp = k *\<^sub>R (?cr - ?cp) \<longleftrightarrow> ?cq = k *\<^sub>R ?cr + (1 - k) *\<^sub>R ?cp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k. (cart2_pt q - cart2_pt p = k *\<^sub>R (cart2_pt r - cart2_pt p)) = (cart2_pt q = k *\<^sub>R cart2_pt r + (1 - k) *\<^sub>R cart2_pt p)
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
\<forall>k. (cart2_pt q - cart2_pt p = k *\<^sub>R (cart2_pt r - cart2_pt p)) = (cart2_pt q = k *\<^sub>R cart2_pt r + (1 - k) *\<^sub>R cart2_pt p)

goal (1 subgoal):
 1. (B\<^sub>\<real> cart2_pt p cart2_pt q cart2_pt r) = (\<exists>k\<ge>0. k \<le> 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p)
[PROOF STEP]
hence "\<forall> k. ?cq - ?cp = k *\<^sub>R (?cr - ?cp)
    \<longleftrightarrow> ?cq1 = k *\<^sub>R ?cr1 + (1 - k) *\<^sub>R ?cp1"
[PROOF STATE]
proof (prove)
using this:
\<forall>k. (cart2_pt q - cart2_pt p = k *\<^sub>R (cart2_pt r - cart2_pt p)) = (cart2_pt q = k *\<^sub>R cart2_pt r + (1 - k) *\<^sub>R cart2_pt p)

goal (1 subgoal):
 1. \<forall>k. (cart2_pt q - cart2_pt p = k *\<^sub>R (cart2_pt r - cart2_pt p)) = (vector2_append1 (cart2_pt q) = k *\<^sub>R vector2_append1 (cart2_pt r) + (1 - k) *\<^sub>R vector2_append1 (cart2_pt p))
[PROOF STEP]
unfolding vector2_append1_def and vector_def
[PROOF STATE]
proof (prove)
using this:
\<forall>k. (cart2_pt q - cart2_pt p = k *\<^sub>R (cart2_pt r - cart2_pt p)) = (cart2_pt q = k *\<^sub>R cart2_pt r + (1 - k) *\<^sub>R cart2_pt p)

goal (1 subgoal):
 1. \<forall>k. (cart2_pt q - cart2_pt p = k *\<^sub>R (cart2_pt r - cart2_pt p)) = (vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [cart2_pt q $ 1, cart2_pt q $ 2, 1] (\<lambda>n x. 0) 1) = k *\<^sub>R vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [cart2_pt r $ 1, cart2_pt r $ 2, 1] (\<lambda>n x. 0) 1) + (1 - k) *\<^sub>R vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [cart2_pt p $ 1, cart2_pt p $ 2, 1] (\<lambda>n x. 0) 1))
[PROOF STEP]
by (simp add: vec_eq_iff forall_2 forall_3)
[PROOF STATE]
proof (state)
this:
\<forall>k. (cart2_pt q - cart2_pt p = k *\<^sub>R (cart2_pt r - cart2_pt p)) = (vector2_append1 (cart2_pt q) = k *\<^sub>R vector2_append1 (cart2_pt r) + (1 - k) *\<^sub>R vector2_append1 (cart2_pt p))

goal (1 subgoal):
 1. (B\<^sub>\<real> cart2_pt p cart2_pt q cart2_pt r) = (\<exists>k\<ge>0. k \<le> 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p)
[PROOF STEP]
with \<open>?cp1 = cart2_append1 p\<close>
    and \<open>?cq1 = cart2_append1 q\<close>
    and \<open>?cr1 = cart2_append1 r\<close>
[PROOF STATE]
proof (chain)
picking this:
vector2_append1 (cart2_pt p) = cart2_append1 p
vector2_append1 (cart2_pt q) = cart2_append1 q
vector2_append1 (cart2_pt r) = cart2_append1 r
\<forall>k. (cart2_pt q - cart2_pt p = k *\<^sub>R (cart2_pt r - cart2_pt p)) = (vector2_append1 (cart2_pt q) = k *\<^sub>R vector2_append1 (cart2_pt r) + (1 - k) *\<^sub>R vector2_append1 (cart2_pt p))
[PROOF STEP]
have "\<forall> k. ?cq - ?cp = k *\<^sub>R (?cr - ?cp)
    \<longleftrightarrow> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p"
[PROOF STATE]
proof (prove)
using this:
vector2_append1 (cart2_pt p) = cart2_append1 p
vector2_append1 (cart2_pt q) = cart2_append1 q
vector2_append1 (cart2_pt r) = cart2_append1 r
\<forall>k. (cart2_pt q - cart2_pt p = k *\<^sub>R (cart2_pt r - cart2_pt p)) = (vector2_append1 (cart2_pt q) = k *\<^sub>R vector2_append1 (cart2_pt r) + (1 - k) *\<^sub>R vector2_append1 (cart2_pt p))

goal (1 subgoal):
 1. \<forall>k. (cart2_pt q - cart2_pt p = k *\<^sub>R (cart2_pt r - cart2_pt p)) = (cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>k. (cart2_pt q - cart2_pt p = k *\<^sub>R (cart2_pt r - cart2_pt p)) = (cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p)

goal (1 subgoal):
 1. (B\<^sub>\<real> cart2_pt p cart2_pt q cart2_pt r) = (\<exists>k\<ge>0. k \<le> 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p)
[PROOF STEP]
thus "B\<^sub>\<real> (cart2_pt p) (cart2_pt q) (cart2_pt r)
    \<longleftrightarrow> (\<exists> k\<ge>0. k \<le> 1
    \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p)"
[PROOF STATE]
proof (prove)
using this:
\<forall>k. (cart2_pt q - cart2_pt p = k *\<^sub>R (cart2_pt r - cart2_pt p)) = (cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p)

goal (1 subgoal):
 1. (B\<^sub>\<real> cart2_pt p cart2_pt q cart2_pt r) = (\<exists>k\<ge>0. k \<le> 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p)
[PROOF STEP]
by (unfold real_euclid_B_def) simp
[PROOF STATE]
proof (state)
this:
(B\<^sub>\<real> cart2_pt p cart2_pt q cart2_pt r) = (\<exists>k\<ge>0. k \<le> 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cart2_append1_between_right_strict:
  assumes "z_non_zero p" and "z_non_zero q" and "z_non_zero r"
  and "B\<^sub>\<real> (cart2_pt p) (cart2_pt q) (cart2_pt r)" and "q \<noteq> r"
  shows "\<exists> k\<ge>0. k < 1
  \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k\<ge>0. k < 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k\<ge>0. k < 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p
[PROOF STEP]
from \<open>z_non_zero p\<close> and \<open>z_non_zero q\<close> and \<open>z_non_zero r\<close>
    and \<open>B\<^sub>\<real> (cart2_pt p) (cart2_pt q) (cart2_pt r)\<close> and cart2_append1_between
[PROOF STATE]
proof (chain)
picking this:
z_non_zero p
z_non_zero q
z_non_zero r
B\<^sub>\<real> cart2_pt p cart2_pt q cart2_pt r
\<lbrakk>z_non_zero ?p; z_non_zero ?q; z_non_zero ?r\<rbrakk> \<Longrightarrow> (B\<^sub>\<real> cart2_pt ?p cart2_pt ?q cart2_pt ?r) = (\<exists>k\<ge>0. k \<le> 1 \<and> cart2_append1 ?q = k *\<^sub>R cart2_append1 ?r + (1 - k) *\<^sub>R cart2_append1 ?p)
[PROOF STEP]
obtain k where "k \<ge> 0" and "k \<le> 1"
    and "cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p"
[PROOF STATE]
proof (prove)
using this:
z_non_zero p
z_non_zero q
z_non_zero r
B\<^sub>\<real> cart2_pt p cart2_pt q cart2_pt r
\<lbrakk>z_non_zero ?p; z_non_zero ?q; z_non_zero ?r\<rbrakk> \<Longrightarrow> (B\<^sub>\<real> cart2_pt ?p cart2_pt ?q cart2_pt ?r) = (\<exists>k\<ge>0. k \<le> 1 \<and> cart2_append1 ?q = k *\<^sub>R cart2_append1 ?r + (1 - k) *\<^sub>R cart2_append1 ?p)

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>0 \<le> k; k \<le> 1; cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> k
k \<le> 1
cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p

goal (1 subgoal):
 1. \<exists>k\<ge>0. k < 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p
[PROOF STEP]
have "k \<noteq> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<noteq> 1
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k = 1 \<Longrightarrow> False
[PROOF STEP]
assume "k = 1"
[PROOF STATE]
proof (state)
this:
k = 1

goal (1 subgoal):
 1. k = 1 \<Longrightarrow> False
[PROOF STEP]
with \<open>cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p\<close>
[PROOF STATE]
proof (chain)
picking this:
cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p
k = 1
[PROOF STEP]
have "cart2_append1 q = cart2_append1 r"
[PROOF STATE]
proof (prove)
using this:
cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p
k = 1

goal (1 subgoal):
 1. cart2_append1 q = cart2_append1 r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cart2_append1 q = cart2_append1 r

goal (1 subgoal):
 1. k = 1 \<Longrightarrow> False
[PROOF STEP]
with \<open>z_non_zero q\<close>
[PROOF STATE]
proof (chain)
picking this:
z_non_zero q
cart2_append1 q = cart2_append1 r
[PROOF STEP]
have "q = r"
[PROOF STATE]
proof (prove)
using this:
z_non_zero q
cart2_append1 q = cart2_append1 r

goal (1 subgoal):
 1. q = r
[PROOF STEP]
by (rule cart2_append1_inj)
[PROOF STATE]
proof (state)
this:
q = r

goal (1 subgoal):
 1. k = 1 \<Longrightarrow> False
[PROOF STEP]
with \<open>q \<noteq> r\<close>
[PROOF STATE]
proof (chain)
picking this:
q \<noteq> r
q = r
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
q \<noteq> r
q = r

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
k \<noteq> 1

goal (1 subgoal):
 1. \<exists>k\<ge>0. k < 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p
[PROOF STEP]
with \<open>k \<le> 1\<close>
[PROOF STATE]
proof (chain)
picking this:
k \<le> 1
k \<noteq> 1
[PROOF STEP]
have "k < 1"
[PROOF STATE]
proof (prove)
using this:
k \<le> 1
k \<noteq> 1

goal (1 subgoal):
 1. k < 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k < 1

goal (1 subgoal):
 1. \<exists>k\<ge>0. k < 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p
[PROOF STEP]
with \<open>k \<ge> 0\<close>
    and \<open>cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p\<close>
[PROOF STATE]
proof (chain)
picking this:
0 \<le> k
cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p
k < 1
[PROOF STEP]
show "\<exists> k\<ge>0. k < 1
    \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p"
[PROOF STATE]
proof (prove)
using this:
0 \<le> k
cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p
k < 1

goal (1 subgoal):
 1. \<exists>k\<ge>0. k < 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p
[PROOF STEP]
by (simp add: exI [of _ k])
[PROOF STATE]
proof (state)
this:
\<exists>k\<ge>0. k < 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cart2_append1_between_strict:
  assumes "z_non_zero p" and "z_non_zero q" and "z_non_zero r"
  and "B\<^sub>\<real> (cart2_pt p) (cart2_pt q) (cart2_pt r)" and "q \<noteq> p" and "q \<noteq> r"
  shows "\<exists> k>0. k < 1
  \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k>0. k < 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k>0. k < 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p
[PROOF STEP]
from \<open>z_non_zero p\<close> and \<open>z_non_zero q\<close> and \<open>z_non_zero r\<close>
    and \<open>B\<^sub>\<real> (cart2_pt p) (cart2_pt q) (cart2_pt r)\<close> and \<open>q \<noteq> r\<close>
    and cart2_append1_between_right_strict [of p q r]
[PROOF STATE]
proof (chain)
picking this:
z_non_zero p
z_non_zero q
z_non_zero r
B\<^sub>\<real> cart2_pt p cart2_pt q cart2_pt r
q \<noteq> r
\<lbrakk>z_non_zero p; z_non_zero q; z_non_zero r; B\<^sub>\<real> cart2_pt p cart2_pt q cart2_pt r; q \<noteq> r\<rbrakk> \<Longrightarrow> \<exists>k\<ge>0. k < 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p
[PROOF STEP]
obtain k where "k \<ge> 0" and "k < 1"
    and "cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p"
[PROOF STATE]
proof (prove)
using this:
z_non_zero p
z_non_zero q
z_non_zero r
B\<^sub>\<real> cart2_pt p cart2_pt q cart2_pt r
q \<noteq> r
\<lbrakk>z_non_zero p; z_non_zero q; z_non_zero r; B\<^sub>\<real> cart2_pt p cart2_pt q cart2_pt r; q \<noteq> r\<rbrakk> \<Longrightarrow> \<exists>k\<ge>0. k < 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>0 \<le> k; k < 1; cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> k
k < 1
cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p

goal (1 subgoal):
 1. \<exists>k>0. k < 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p
[PROOF STEP]
have "k \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<noteq> 0
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k = 0 \<Longrightarrow> False
[PROOF STEP]
assume "k = 0"
[PROOF STATE]
proof (state)
this:
k = 0

goal (1 subgoal):
 1. k = 0 \<Longrightarrow> False
[PROOF STEP]
with \<open>cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p\<close>
[PROOF STATE]
proof (chain)
picking this:
cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p
k = 0
[PROOF STEP]
have "cart2_append1 q = cart2_append1 p"
[PROOF STATE]
proof (prove)
using this:
cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p
k = 0

goal (1 subgoal):
 1. cart2_append1 q = cart2_append1 p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cart2_append1 q = cart2_append1 p

goal (1 subgoal):
 1. k = 0 \<Longrightarrow> False
[PROOF STEP]
with \<open>z_non_zero q\<close>
[PROOF STATE]
proof (chain)
picking this:
z_non_zero q
cart2_append1 q = cart2_append1 p
[PROOF STEP]
have "q = p"
[PROOF STATE]
proof (prove)
using this:
z_non_zero q
cart2_append1 q = cart2_append1 p

goal (1 subgoal):
 1. q = p
[PROOF STEP]
by (rule cart2_append1_inj)
[PROOF STATE]
proof (state)
this:
q = p

goal (1 subgoal):
 1. k = 0 \<Longrightarrow> False
[PROOF STEP]
with \<open>q \<noteq> p\<close>
[PROOF STATE]
proof (chain)
picking this:
q \<noteq> p
q = p
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
q \<noteq> p
q = p

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
k \<noteq> 0

goal (1 subgoal):
 1. \<exists>k>0. k < 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p
[PROOF STEP]
with \<open>k \<ge> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
0 \<le> k
k \<noteq> 0
[PROOF STEP]
have "k > 0"
[PROOF STATE]
proof (prove)
using this:
0 \<le> k
k \<noteq> 0

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

goal (1 subgoal):
 1. \<exists>k>0. k < 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p
[PROOF STEP]
with \<open>k < 1\<close>
    and \<open>cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p\<close>
[PROOF STATE]
proof (chain)
picking this:
k < 1
cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p
0 < k
[PROOF STEP]
show "\<exists> k>0. k < 1
    \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p"
[PROOF STATE]
proof (prove)
using this:
k < 1
cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p
0 < k

goal (1 subgoal):
 1. \<exists>k>0. k < 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p
[PROOF STEP]
by (simp add: exI [of _ k])
[PROOF STATE]
proof (state)
this:
\<exists>k>0. k < 1 \<and> cart2_append1 q = k *\<^sub>R cart2_append1 r + (1 - k) *\<^sub>R cart2_append1 p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exe_const_type_of_ok: "
  alist_conds cto \<Longrightarrow>
  (\<forall>ty \<in> Map.ran (map_of cto) . typ_ok_sig (map_of cto, ta, sa) ty)
  \<longleftrightarrow> (\<forall>ty \<in> snd ` set cto  . typ_ok_sig (map_of cto, ta, sa) ty)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alist_conds cto \<Longrightarrow> (\<forall>ty\<in>ran (map_of cto). typ_ok_sig (map_of cto, ta, sa) ty) = (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, ta, sa) ty)
[PROOF STEP]
by (simp add: ran_distinct)


[STATEMENT]
lemma exe_wf_sig_imp_wf_sig:
  assumes "alist_conds cto" "alist_conds tao" "exe_osig_conds sa" "(exe_wf_osig sa
  \<and> fst ` set (exetcsigs sa) = fst ` set tao
  \<and> (\<forall>type \<in> fst ` set (exetcsigs sa).
      (\<forall>ars \<in> snd ` set (the (lookup (\<lambda>k. k=type) (exetcsigs sa))) .
      the (lookup (\<lambda>k. k=type) tao) = length ars)))
  \<and> (\<forall>ty \<in> snd ` set cto . typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)"
  shows "wf_sig (map_of cto, map_of tao, translate_osig sa)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
fix type y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
assume p: "exe_osig_conds sa" "trans (fst (translate_osig sa))" "snd (translate_osig sa) type = Some y"
[PROOF STATE]
proof (state)
this:
exe_osig_conds sa
trans (fst (translate_osig sa))
snd (translate_osig sa) type = Some y

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
hence "exe_ars_conds (exetcsigs sa)"
[PROOF STATE]
proof (prove)
using this:
exe_osig_conds sa
trans (fst (translate_osig sa))
snd (translate_osig sa) type = Some y

goal (1 subgoal):
 1. exe_ars_conds (snd sa)
[PROOF STEP]
using exe_osig_conds_def
[PROOF STATE]
proof (prove)
using this:
exe_osig_conds sa
trans (fst (translate_osig sa))
snd (translate_osig sa) type = Some y
exe_osig_conds ?a \<equiv> exe_class_conds (fst ?a) \<and> exe_ars_conds (snd ?a)

goal (1 subgoal):
 1. exe_ars_conds (snd sa)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
exe_ars_conds (snd sa)

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
from p
[PROOF STATE]
proof (chain)
picking this:
exe_osig_conds sa
trans (fst (translate_osig sa))
snd (translate_osig sa) type = Some y
[PROOF STEP]
have "translate_ars (exetcsigs sa) type = Some y"
[PROOF STATE]
proof (prove)
using this:
exe_osig_conds sa
trans (fst (translate_osig sa))
snd (translate_osig sa) type = Some y

goal (1 subgoal):
 1. translate_ars (snd sa) type = Some y
[PROOF STEP]
by (metis snd_conv translate_osig.elims)
[PROOF STATE]
proof (state)
this:
translate_ars (snd sa) type = Some y

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
hence "(type, y) \<in> set (map (apsnd map_of) (exetcsigs sa))"
[PROOF STATE]
proof (prove)
using this:
translate_ars (snd sa) type = Some y

goal (1 subgoal):
 1. (type, y) \<in> set (map (apsnd map_of) (snd sa))
[PROOF STEP]
using map_of_SomeD
[PROOF STATE]
proof (prove)
using this:
translate_ars (snd sa) type = Some y
map_of ?xs ?k = Some ?y \<Longrightarrow> (?k, ?y) \<in> set ?xs

goal (1 subgoal):
 1. (type, y) \<in> set (map (apsnd map_of) (snd sa))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(type, y) \<in> set (map (apsnd map_of) (snd sa))

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
hence "type \<in> fst ` set (exetcsigs sa)"
[PROOF STATE]
proof (prove)
using this:
(type, y) \<in> set (map (apsnd map_of) (snd sa))

goal (1 subgoal):
 1. type \<in> fst ` set (snd sa)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
type \<in> fst ` set (snd sa)

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
type \<in> fst ` set (snd sa)
[PROOF STEP]
obtain x where "lookup (\<lambda>x. x=type) (exetcsigs sa) = Some x"
[PROOF STATE]
proof (prove)
using this:
type \<in> fst ` set (snd sa)

goal (1 subgoal):
 1. (\<And>x. lookup (\<lambda>x. x = type) (snd sa) = Some x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using key_present_imp_eq_lookup_finds_value
[PROOF STATE]
proof (prove)
using this:
type \<in> fst ` set (snd sa)
?k \<in> fst ` set ?al \<Longrightarrow> \<exists>v. lookup (\<lambda>x. x = ?k) ?al = Some v

goal (1 subgoal):
 1. (\<And>x. lookup (\<lambda>x. x = type) (snd sa) = Some x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>x. x = type) (snd sa) = Some x

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
hence "map_of x = y"
[PROOF STATE]
proof (prove)
using this:
lookup (\<lambda>x. x = type) (snd sa) = Some x

goal (1 subgoal):
 1. map_of x = y
[PROOF STEP]
by (metis \<open>exe_ars_conds (snd sa)\<close> \<open>translate_ars (snd sa) type = Some y\<close>
          exe_ars_conds_def in_alist_imp_in_map_of lookup_eq_map_of_ap
          map_of_SomeD option.sel)
[PROOF STATE]
proof (state)
this:
map_of x = y

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
have "\<exists>y. (type, y) \<in> set tao"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y. (type, y) \<in> set tao
[PROOF STEP]
using \<open>type \<in> fst ` set (exetcsigs sa)\<close> assms(4)
[PROOF STATE]
proof (prove)
using this:
type \<in> fst ` set (snd sa)
(exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)

goal (1 subgoal):
 1. \<exists>y. (type, y) \<in> set tao
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>y. (type, y) \<in> set tao

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>exe_osig_conds sa; trans (fst (translate_osig sa)); snd (translate_osig sa) ?type2 = Some ?y2\<rbrakk> \<Longrightarrow> \<exists>y. (?type2, y) \<in> set tao

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
note 1 = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>exe_osig_conds sa; trans (fst (translate_osig sa)); snd (translate_osig sa) ?type2 = Some ?y2\<rbrakk> \<Longrightarrow> \<exists>y. (?type2, y) \<in> set tao

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>exe_osig_conds sa; trans (fst (translate_osig sa)); snd (translate_osig sa) ?type2 = Some ?y2\<rbrakk> \<Longrightarrow> \<exists>y. (?type2, y) \<in> set tao

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
fix ars type y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
assume p: "exe_osig_conds sa"
      "trans (fst (translate_osig sa))"
      "\<forall>x\<in>set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) (snd x)"
      "ars \<in> ran y"
      "snd (translate_osig sa) type = Some y"
[PROOF STATE]
proof (state)
this:
exe_osig_conds sa
trans (fst (translate_osig sa))
\<forall>x\<in>set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) (snd x)
ars \<in> ran y
snd (translate_osig sa) type = Some y

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
hence "exe_ars_conds (exetcsigs sa)"
[PROOF STATE]
proof (prove)
using this:
exe_osig_conds sa
trans (fst (translate_osig sa))
\<forall>x\<in>set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) (snd x)
ars \<in> ran y
snd (translate_osig sa) type = Some y

goal (1 subgoal):
 1. exe_ars_conds (snd sa)
[PROOF STEP]
using exe_osig_conds_def
[PROOF STATE]
proof (prove)
using this:
exe_osig_conds sa
trans (fst (translate_osig sa))
\<forall>x\<in>set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) (snd x)
ars \<in> ran y
snd (translate_osig sa) type = Some y
exe_osig_conds ?a \<equiv> exe_class_conds (fst ?a) \<and> exe_ars_conds (snd ?a)

goal (1 subgoal):
 1. exe_ars_conds (snd sa)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
exe_ars_conds (snd sa)

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
from p(1-2) p(5)
[PROOF STATE]
proof (chain)
picking this:
exe_osig_conds sa
trans (fst (translate_osig sa))
snd (translate_osig sa) type = Some y
[PROOF STEP]
have "translate_ars (exetcsigs sa) type = Some y"
[PROOF STATE]
proof (prove)
using this:
exe_osig_conds sa
trans (fst (translate_osig sa))
snd (translate_osig sa) type = Some y

goal (1 subgoal):
 1. translate_ars (snd sa) type = Some y
[PROOF STEP]
by (metis snd_conv translate_osig.elims)
[PROOF STATE]
proof (state)
this:
translate_ars (snd sa) type = Some y

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
hence "(type, y) \<in> set (map (apsnd map_of) (exetcsigs sa))"
[PROOF STATE]
proof (prove)
using this:
translate_ars (snd sa) type = Some y

goal (1 subgoal):
 1. (type, y) \<in> set (map (apsnd map_of) (snd sa))
[PROOF STEP]
using map_of_SomeD
[PROOF STATE]
proof (prove)
using this:
translate_ars (snd sa) type = Some y
map_of ?xs ?k = Some ?y \<Longrightarrow> (?k, ?y) \<in> set ?xs

goal (1 subgoal):
 1. (type, y) \<in> set (map (apsnd map_of) (snd sa))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(type, y) \<in> set (map (apsnd map_of) (snd sa))

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
hence dom: "type \<in> fst ` set (exetcsigs sa)"
[PROOF STATE]
proof (prove)
using this:
(type, y) \<in> set (map (apsnd map_of) (snd sa))

goal (1 subgoal):
 1. type \<in> fst ` set (snd sa)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
type \<in> fst ` set (snd sa)

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
type \<in> fst ` set (snd sa)
[PROOF STEP]
obtain x where x: "lookup (\<lambda>x. x=type) (exetcsigs sa) = Some x"
[PROOF STATE]
proof (prove)
using this:
type \<in> fst ` set (snd sa)

goal (1 subgoal):
 1. (\<And>x. lookup (\<lambda>x. x = type) (snd sa) = Some x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using key_present_imp_eq_lookup_finds_value
[PROOF STATE]
proof (prove)
using this:
type \<in> fst ` set (snd sa)
?k \<in> fst ` set ?al \<Longrightarrow> \<exists>v. lookup (\<lambda>x. x = ?k) ?al = Some v

goal (1 subgoal):
 1. (\<And>x. lookup (\<lambda>x. x = type) (snd sa) = Some x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>x. x = type) (snd sa) = Some x

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
hence "map_of x = y"
[PROOF STATE]
proof (prove)
using this:
lookup (\<lambda>x. x = type) (snd sa) = Some x

goal (1 subgoal):
 1. map_of x = y
[PROOF STEP]
by (metis \<open>exe_ars_conds (snd sa)\<close> \<open>translate_ars (snd sa) type = Some y\<close>
            exe_ars_conds_def in_alist_imp_in_map_of lookup_eq_map_of_ap map_of_SomeD option.sel)
[PROOF STATE]
proof (state)
this:
map_of x = y

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
have "ars \<in> snd ` set x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ars \<in> snd ` set x
[PROOF STEP]
by (metis \<open>map_of x = y\<close> image_iff in_range_if_ex_key map_of_SomeD p(4) snd_conv)
[PROOF STATE]
proof (state)
this:
ars \<in> snd ` set x

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
have "type \<in> fst ` set tao"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. type \<in> fst ` set tao
[PROOF STEP]
apply (simp add: \<open>type \<in> fst ` set (exetcsigs sa)\<close> assms(4))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. type \<in> fst ` set tao
[PROOF STEP]
using assms(4) dom
[PROOF STATE]
proof (prove)
using this:
(exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
type \<in> fst ` set (snd sa)

goal (1 subgoal):
 1. type \<in> fst ` set tao
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
type \<in> fst ` set tao

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
type \<in> fst ` set tao

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
have 1: "(\<forall>ars \<in> snd ` set (the (lookup (\<lambda>k. k=type) (exetcsigs sa))) .
        the (lookup (\<lambda>k. k=type) tao) = length ars)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars
[PROOF STEP]
using \<open>type \<in> fst ` set (exetcsigs sa)\<close> assms(4)
[PROOF STATE]
proof (prove)
using this:
type \<in> fst ` set (snd sa)
(exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)

goal (1 subgoal):
 1. \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
type \<in> fst ` set tao
\<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars
[PROOF STEP]
have "the (lookup (\<lambda>k. k = type) tao) = length ars"
[PROOF STATE]
proof (prove)
using this:
type \<in> fst ` set tao
\<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars

goal (1 subgoal):
 1. the (lookup (\<lambda>k. k = type) tao) = length ars
[PROOF STEP]
using \<open>lookup (\<lambda>x. x = type) (exetcsigs sa) = Some x\<close> \<open>map_of x = y\<close>
            in_range_if_ex_key map_of_SomeD option.sel p(3) snd_conv
[PROOF STATE]
proof (prove)
using this:
type \<in> fst ` set tao
\<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars
lookup (\<lambda>x. x = type) (snd sa) = Some x
map_of x = y
(?v \<in> ran ?m) = (\<exists>k. ?m k = Some ?v)
map_of ?xs ?k = Some ?y \<Longrightarrow> (?k, ?y) \<in> set ?xs
the (Some ?x2.0) = ?x2.0
\<forall>x\<in>set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) (snd x)
snd (?x1.0, ?x2.0) = ?x2.0

goal (1 subgoal):
 1. the (lookup (\<lambda>k. k = type) tao) = length ars
[PROOF STEP]
by (simp add: 1 \<open>ars \<in> snd ` set x\<close>)
[PROOF STATE]
proof (state)
this:
the (lookup (\<lambda>k. k = type) tao) = length ars

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
hence "the (map_of tao type) = length ars"
[PROOF STATE]
proof (prove)
using this:
the (lookup (\<lambda>k. k = type) tao) = length ars

goal (1 subgoal):
 1. the (map_of tao type) = length ars
[PROOF STEP]
by (metis \<open>the (lookup (\<lambda>k. k = type) tao) = length ars\<close> lookup_eq_map_of_ap)
[PROOF STATE]
proof (state)
this:
the (map_of tao type) = length ars

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>exe_osig_conds sa; trans (fst (translate_osig sa)); \<forall>x\<in>set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) (snd x); ?ars2 \<in> ran ?y2; snd (translate_osig sa) ?type2 = Some ?y2\<rbrakk> \<Longrightarrow> the (map_of tao ?type2) = length ?ars2

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
note 2 = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>exe_osig_conds sa; trans (fst (translate_osig sa)); \<forall>x\<in>set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) (snd x); ?ars2 \<in> ran ?y2; snd (translate_osig sa) ?type2 = Some ?y2\<rbrakk> \<Longrightarrow> the (map_of tao ?type2) = length ?ars2

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>exe_osig_conds sa; trans (fst (translate_osig sa)); \<forall>x\<in>set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) (snd x); ?ars2 \<in> ran ?y2; snd (translate_osig sa) ?type2 = Some ?y2\<rbrakk> \<Longrightarrow> the (map_of tao ?type2) = length ?ars2

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
fix a b x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
assume p: "fst ` set b = fst ` set tao"
      "(x, y) \<in> set tao"
      "sa = (a, b)"
[PROOF STATE]
proof (state)
this:
fst ` set b = fst ` set tao
(x, y) \<in> set tao
sa = (a, b)

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
have "x \<in> fst ` set b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> fst ` set b
[PROOF STEP]
by (metis fst_conv image_iff p(1) p(2))
[PROOF STATE]
proof (state)
this:
x \<in> fst ` set b

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
x \<in> fst ` set b
[PROOF STEP]
obtain ars where "lookup (\<lambda>k. k=x) b = Some ars"
[PROOF STATE]
proof (prove)
using this:
x \<in> fst ` set b

goal (1 subgoal):
 1. (\<And>ars. lookup (\<lambda>k. k = x) b = Some ars \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis key_present_imp_eq_lookup_finds_value)
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>k. k = x) b = Some ars

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
hence "(x,ars) \<in> set b"
[PROOF STATE]
proof (prove)
using this:
lookup (\<lambda>k. k = x) b = Some ars

goal (1 subgoal):
 1. (x, ars) \<in> set b
[PROOF STEP]
by (simp add: lookup_present_eq_key')
[PROOF STATE]
proof (state)
this:
(x, ars) \<in> set b

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
hence "lookup (\<lambda>k. k=x) (map (apsnd map_of) b) = Some (map_of ars)"
[PROOF STATE]
proof (prove)
using this:
(x, ars) \<in> set b

goal (1 subgoal):
 1. lookup (\<lambda>k. k = x) (map (apsnd map_of) b) = Some (map_of ars)
[PROOF STEP]
by (metis assms(3) exe_ars_conds_def exe_osig_conds_def in_alist_imp_in_map_of
          lookup_eq_map_of_ap p(3) snd_conv translate_ars.simps)
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>k. k = x) (map (apsnd map_of) b) = Some (map_of ars)

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
hence "\<exists>y. map_of (map (apsnd map_of) b) x = Some y"
[PROOF STATE]
proof (prove)
using this:
lookup (\<lambda>k. k = x) (map (apsnd map_of) b) = Some (map_of ars)

goal (1 subgoal):
 1. \<exists>y. map_of (map (apsnd map_of) b) x = Some y
[PROOF STEP]
by (metis lookup_eq_map_of_ap)
[PROOF STATE]
proof (state)
this:
\<exists>y. map_of (map (apsnd map_of) b) x = Some y

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>fst ` set ?b2 = fst ` set tao; (?x2, ?y2) \<in> set tao; sa = (?a2, ?b2)\<rbrakk> \<Longrightarrow> \<exists>y. map_of (map (apsnd map_of) ?b2) ?x2 = Some y

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
note 3 = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>fst ` set ?b2 = fst ` set tao; (?x2, ?y2) \<in> set tao; sa = (?a2, ?b2)\<rbrakk> \<Longrightarrow> \<exists>y. map_of (map (apsnd map_of) ?b2) ?x2 = Some y

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>fst ` set ?b2 = fst ` set tao; (?x2, ?y2) \<in> set tao; sa = (?a2, ?b2)\<rbrakk> \<Longrightarrow> \<exists>y. map_of (map (apsnd map_of) ?b2) ?x2 = Some y

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
fix a b x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
assume p: "alist_conds cto"
      "x \<in> ran (map_of cto)"
      "sa = (a, b)"
[PROOF STATE]
proof (state)
this:
alist_conds cto
x \<in> ran (map_of cto)
sa = (a, b)

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
have "typ_ok_sig (map_of cto, map_of tao, set a,  map_of (map (apsnd map_of) b)) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. typ_ok_sig (map_of cto, map_of tao, set a, map_of (map (apsnd map_of) b)) x
[PROOF STEP]
using assms(4) p(1) p(2) p(3) ran_distinct
[PROOF STATE]
proof (prove)
using this:
(exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
alist_conds cto
x \<in> ran (map_of cto)
sa = (a, b)
distinct (map fst ?al) \<Longrightarrow> ran (map_of ?al) = snd ` set ?al

goal (1 subgoal):
 1. typ_ok_sig (map_of cto, map_of tao, set a, map_of (map (apsnd map_of) b)) x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
typ_ok_sig (map_of cto, map_of tao, set a, map_of (map (apsnd map_of) b)) x

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>alist_conds cto; ?x2 \<in> ran (map_of cto); sa = (?a2, ?b2)\<rbrakk> \<Longrightarrow> typ_ok_sig (map_of cto, map_of tao, set ?a2, map_of (map (apsnd map_of) ?b2)) ?x2

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
note 4 = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>alist_conds cto; ?x2 \<in> ran (map_of cto); sa = (?a2, ?b2)\<rbrakk> \<Longrightarrow> typ_ok_sig (map_of cto, map_of tao, set ?a2, map_of (map (apsnd map_of) ?b2)) ?x2

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
have "wf_osig (translate_osig sa)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_osig (translate_osig sa)
[PROOF STEP]
using assms(4) wf_osig_iff_exe_wf_osig
[PROOF STATE]
proof (prove)
using this:
(exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)
wf_osig (translate_osig ?oss) = exe_wf_osig ?oss

goal (1 subgoal):
 1. wf_osig (translate_osig sa)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
wf_osig (translate_osig sa)

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
wf_osig (translate_osig sa)

goal (1 subgoal):
 1. wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
apply (cases sa)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>wf_osig (translate_osig sa); sa = (a, b)\<rbrakk> \<Longrightarrow> wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
using 1 2 3 4 assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>exe_osig_conds sa; trans (fst (translate_osig sa)); snd (translate_osig sa) ?type2 = Some ?y2\<rbrakk> \<Longrightarrow> \<exists>y. (?type2, y) \<in> set tao
\<lbrakk>exe_osig_conds sa; trans (fst (translate_osig sa)); \<forall>x\<in>set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) (snd x); ?ars2 \<in> ran ?y2; snd (translate_osig sa) ?type2 = Some ?y2\<rbrakk> \<Longrightarrow> the (map_of tao ?type2) = length ?ars2
\<lbrakk>fst ` set ?b2 = fst ` set tao; (?x2, ?y2) \<in> set tao; sa = (?a2, ?b2)\<rbrakk> \<Longrightarrow> \<exists>y. map_of (map (apsnd map_of) ?b2) ?x2 = Some y
\<lbrakk>alist_conds cto; ?x2 \<in> ran (map_of cto); sa = (?a2, ?b2)\<rbrakk> \<Longrightarrow> typ_ok_sig (map_of cto, map_of tao, set ?a2, map_of (map (apsnd map_of) ?b2)) ?x2
alist_conds cto
alist_conds tao
exe_osig_conds sa
(exe_wf_osig sa \<and> fst ` set (snd sa) = fst ` set tao \<and> (\<forall>type\<in>fst ` set (snd sa). \<forall>ars\<in>snd ` set (the (lookup (\<lambda>k. k = type) (snd sa))). the (lookup (\<lambda>k. k = type) tao) = length ars)) \<and> (\<forall>ty\<in>snd ` set cto. typ_ok_sig (map_of cto, map_of tao, translate_osig sa) ty)

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>wf_osig (translate_osig sa); sa = (a, b)\<rbrakk> \<Longrightarrow> wf_sig (map_of cto, map_of tao, translate_osig sa)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf_sig (map_of cto, map_of tao, translate_osig sa)

goal:
No subgoals!
[PROOF STEP]
qed