[STATEMENT]
lemma bij_betw_pos_interval:
  fixes a b::real
  assumes "a<b"
  shows "bij_betw (\<lambda>x. (a+b * x) / (1+x)) {x. x>0} {x. a<x \<and> x<b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (\<lambda>x. (a + b * x) / (1 + x)) {x. 0 < x} {x. a < x \<and> x < b}
[PROOF STEP]
proof (rule bij_betw_imageI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on (\<lambda>x. (a + b * x) / (1 + x)) {x. 0 < x}
 2. (\<lambda>x. (a + b * x) / (1 + x)) ` {x. 0 < x} = {x. a < x \<and> x < b}
[PROOF STEP]
show "inj_on (\<lambda>x. (a + b * x) / (1 + x)) {x. 0 < x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>x. (a + b * x) / (1 + x)) {x. 0 < x}
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>Collect ((<) 0). \<forall>y\<in>Collect ((<) 0). (a + b * x) / (1 + x) = (a + b * y) / (1 + y) \<longrightarrow> x = y
[PROOF STEP]
apply (auto simp add:field_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>0 < x; 0 < y; x * b + y * a = x * a + y * b\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
using assms crossproduct_noteq
[PROOF STATE]
proof (prove)
using this:
a < b
(?a \<noteq> ?b \<and> ?c \<noteq> ?d) = (?a * ?c + ?b * ?d \<noteq> ?a * ?d + ?b * ?c)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>0 < x; 0 < y; x * b + y * a = x * a + y * b\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>x. (a + b * x) / (1 + x)) {x. 0 < x}

goal (1 subgoal):
 1. (\<lambda>x. (a + b * x) / (1 + x)) ` {x. 0 < x} = {x. a < x \<and> x < b}
[PROOF STEP]
have "x \<in> (\<lambda>x. (a + b * x) / (1 + x)) ` {x. 0 < x}" when "a < x" "x < b" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> (\<lambda>x. (a + b * x) / (1 + x)) ` {x. 0 < x}
[PROOF STEP]
proof (rule rev_image_eqI[of "(x-a)/(b-x)"])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (x - a) / (b - x) \<in> {x. 0 < x}
 2. x = (a + b * ((x - a) / (b - x))) / (1 + (x - a) / (b - x))
[PROOF STEP]
define bx where "bx=b-x"
[PROOF STATE]
proof (state)
this:
bx = b - x

goal (2 subgoals):
 1. (x - a) / (b - x) \<in> {x. 0 < x}
 2. x = (a + b * ((x - a) / (b - x))) / (1 + (x - a) / (b - x))
[PROOF STEP]
have x:"x=b-bx"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = b - bx
[PROOF STEP]
unfolding bx_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = b - (b - x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = b - bx

goal (2 subgoals):
 1. (x - a) / (b - x) \<in> {x. 0 < x}
 2. x = (a + b * ((x - a) / (b - x))) / (1 + (x - a) / (b - x))
[PROOF STEP]
have "bx\<noteq>0" "b>a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bx \<noteq> 0 &&& a < b
[PROOF STEP]
unfolding bx_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b - x \<noteq> 0 &&& a < b
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
a < x
x < b

goal (1 subgoal):
 1. b - x \<noteq> 0 &&& a < b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bx \<noteq> 0
a < b

goal (2 subgoals):
 1. (x - a) / (b - x) \<in> {x. 0 < x}
 2. x = (a + b * ((x - a) / (b - x))) / (1 + (x - a) / (b - x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bx \<noteq> 0
a < b
[PROOF STEP]
show " x = (a + b * ((x - a) / (b - x))) / (1 + (x - a) / (b - x))"
[PROOF STATE]
proof (prove)
using this:
bx \<noteq> 0
a < b

goal (1 subgoal):
 1. x = (a + b * ((x - a) / (b - x))) / (1 + (x - a) / (b - x))
[PROOF STEP]
apply (fold bx_def,unfold x)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bx \<noteq> 0; a < b; bx \<noteq> 0; a < b\<rbrakk> \<Longrightarrow> b - bx = (a + b * ((b - bx - a) / bx)) / (1 + (b - bx - a) / bx)
[PROOF STEP]
by (auto simp add:field_simps)
[PROOF STATE]
proof (state)
this:
x = (a + b * ((x - a) / (b - x))) / (1 + (x - a) / (b - x))

goal (1 subgoal):
 1. (x - a) / (b - x) \<in> {x. 0 < x}
[PROOF STEP]
show "(x - a) / (b - x) \<in> {x. 0 < x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x - a) / (b - x) \<in> {x. 0 < x}
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
a < x
x < b

goal (1 subgoal):
 1. (x - a) / (b - x) \<in> {x. 0 < x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x - a) / (b - x) \<in> {x. 0 < x}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>a < ?x; ?x < b\<rbrakk> \<Longrightarrow> ?x \<in> (\<lambda>x. (a + b * x) / (1 + x)) ` {x. 0 < x}

goal (1 subgoal):
 1. (\<lambda>x. (a + b * x) / (1 + x)) ` {x. 0 < x} = {x. a < x \<and> x < b}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>a < ?x; ?x < b\<rbrakk> \<Longrightarrow> ?x \<in> (\<lambda>x. (a + b * x) / (1 + x)) ` {x. 0 < x}
[PROOF STEP]
show "(\<lambda>x. (a + b * x) / (1 + x)) ` {x. 0 < x} = {x. a < x \<and> x < b}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a < ?x; ?x < b\<rbrakk> \<Longrightarrow> ?x \<in> (\<lambda>x. (a + b * x) / (1 + x)) ` {x. 0 < x}

goal (1 subgoal):
 1. (\<lambda>x. (a + b * x) / (1 + x)) ` {x. 0 < x} = {x. a < x \<and> x < b}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a < ?x; ?x < b\<rbrakk> \<Longrightarrow> ?x \<in> (\<lambda>x. (a + b * x) / (1 + x)) ` {x. 0 < x}
a < b

goal (1 subgoal):
 1. (\<lambda>x. (a + b * x) / (1 + x)) ` {x. 0 < x} = {x. a < x \<and> x < b}
[PROOF STEP]
by (auto simp add:divide_simps algebra_simps)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. (a + b * x) / (1 + x)) ` {x. 0 < x} = {x. a < x \<and> x < b}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proots_sphere_pos_interval:
  fixes a b::real
  defines "q1\<equiv>[:a,b:]" and "q2\<equiv>[:1,1:]"
  assumes "p\<noteq>0" "a<b"
  shows "proots_count p {x. a < x \<and> x < b} = proots_count (fcompose p q1 q2) {x. 0 < x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_count p {x. a < x \<and> x < b} = proots_count (fcompose p q1 q2) {x. 0 < x}
[PROOF STEP]
apply (rule proots_fcompose_bij_eq[OF _ \<open>p\<noteq>0\<close>])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. bij_betw (\<lambda>x. poly q1 x / poly q2 x) {x. 0 < x} {x. a < x \<and> x < b}
 2. \<forall>x\<in>{x. 0 < x}. poly q2 x \<noteq> 0
 3. max (degree q1) (degree q2) \<le> 1
 4. \<forall>c. q1 \<noteq> smult c q2
 5. infinite UNIV
[PROOF STEP]
unfolding q1_def q2_def
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. bij_betw (\<lambda>x. poly [:a, b:] x / poly [:1, 1:] x) {x. 0 < x} {x. a < x \<and> x < b}
 2. \<forall>x\<in>{x. 0 < x}. poly [:1, 1:] x \<noteq> 0
 3. max (degree [:a, b:]) (degree [:1, 1:]) \<le> 1
 4. \<forall>c. [:a, b:] \<noteq> smult c [:1, 1:]
 5. infinite UNIV
[PROOF STEP]
using bij_betw_pos_interval[OF \<open>a<b\<close>] \<open>a<b\<close>
[PROOF STATE]
proof (prove)
using this:
bij_betw (\<lambda>x. (a + b * x) / (1 + x)) {x. 0 < x} {x. a < x \<and> x < b}
a < b

goal (5 subgoals):
 1. bij_betw (\<lambda>x. poly [:a, b:] x / poly [:1, 1:] x) {x. 0 < x} {x. a < x \<and> x < b}
 2. \<forall>x\<in>{x. 0 < x}. poly [:1, 1:] x \<noteq> 0
 3. max (degree [:a, b:]) (degree [:1, 1:]) \<le> 1
 4. \<forall>c. [:a, b:] \<noteq> smult c [:1, 1:]
 5. infinite UNIV
[PROOF STEP]
by (auto simp add:algebra_simps infinite_UNIV_char_0)


[STATEMENT]
theorem descartes_roots_test:
  fixes p::"real poly"
  assumes "p\<noteq>0" "a<b"
  shows "proots_count p {x. a < x \<and> x <b} \<le> descartes_roots_test a b p  \<and>
          even (descartes_roots_test a b p - proots_count p {x. a < x \<and> x < b})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_count p {x. a < x \<and> x < b} \<le> descartes_roots_test a b p \<and> even (descartes_roots_test a b p - proots_count p {x. a < x \<and> x < b})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proots_count p {x. a < x \<and> x < b} \<le> descartes_roots_test a b p \<and> even (descartes_roots_test a b p - proots_count p {x. a < x \<and> x < b})
[PROOF STEP]
define q where "q=fcompose p [:a,b:] [:1,1:]"
[PROOF STATE]
proof (state)
this:
q = fcompose p [:a, b:] [:1, 1:]

goal (1 subgoal):
 1. proots_count p {x. a < x \<and> x < b} \<le> descartes_roots_test a b p \<and> even (descartes_roots_test a b p - proots_count p {x. a < x \<and> x < b})
[PROOF STEP]
have "q\<noteq>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<noteq> 0
[PROOF STEP]
unfolding q_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fcompose p [:a, b:] [:1, 1:] \<noteq> 0
[PROOF STEP]
apply (rule fcompose_nzero[OF \<open>p\<noteq>0\<close>])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. [:1, 1:] \<noteq> 0
 2. \<forall>c. [:a, b:] \<noteq> smult c [:1, 1:]
 3. infinite UNIV
[PROOF STEP]
using \<open>a<b\<close> infinite_UNIV_char_0
[PROOF STATE]
proof (prove)
using this:
a < b
infinite UNIV

goal (3 subgoals):
 1. [:1, 1:] \<noteq> 0
 2. \<forall>c. [:a, b:] \<noteq> smult c [:1, 1:]
 3. infinite UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q \<noteq> 0

goal (1 subgoal):
 1. proots_count p {x. a < x \<and> x < b} \<le> descartes_roots_test a b p \<and> even (descartes_roots_test a b p - proots_count p {x. a < x \<and> x < b})
[PROOF STEP]
have "proots_count p {x. a < x \<and> x <b} = proots_count q {x. 0 < x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proots_count p {x. a < x \<and> x < b} = proots_count q {x. 0 < x}
[PROOF STEP]
using proots_sphere_pos_interval[OF \<open>p\<noteq>0\<close> \<open>a<b\<close>,folded q_def]
[PROOF STATE]
proof (prove)
using this:
proots_count p {x. a < x \<and> x < b} = proots_count q {x. 0 < x}

goal (1 subgoal):
 1. proots_count p {x. a < x \<and> x < b} = proots_count q {x. 0 < x}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
proots_count p {x. a < x \<and> x < b} = proots_count q {x. 0 < x}

goal (1 subgoal):
 1. proots_count p {x. a < x \<and> x < b} \<le> descartes_roots_test a b p \<and> even (descartes_roots_test a b p - proots_count p {x. a < x \<and> x < b})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
proots_count p {x. a < x \<and> x < b} = proots_count q {x. 0 < x}

goal (1 subgoal):
 1. proots_count p {x. a < x \<and> x < b} \<le> descartes_roots_test a b p \<and> even (descartes_roots_test a b p - proots_count p {x. a < x \<and> x < b})
[PROOF STEP]
have "int (proots_count q {x. 0 < x}) \<le> changes (coeffs q) \<and>
          even (changes (coeffs q) - int (proots_count q {x. 0 < x}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (proots_count q {x. 0 < x}) \<le> changes (coeffs q) \<and> even (changes (coeffs q) - int (proots_count q {x. 0 < x}))
[PROOF STEP]
by (rule descartes_sign[OF \<open>q\<noteq>0\<close>])
[PROOF STATE]
proof (state)
this:
int (proots_count q {x. 0 < x}) \<le> changes (coeffs q) \<and> even (changes (coeffs q) - int (proots_count q {x. 0 < x}))

goal (1 subgoal):
 1. proots_count p {x. a < x \<and> x < b} \<le> descartes_roots_test a b p \<and> even (descartes_roots_test a b p - proots_count p {x. a < x \<and> x < b})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
int (proots_count q {x. 0 < x}) \<le> changes (coeffs q) \<and> even (changes (coeffs q) - int (proots_count q {x. 0 < x}))
[PROOF STEP]
have "proots_count q {x. 0 < x} \<le> nat (changes (coeffs q)) \<and>
          even (nat (changes (coeffs q)) - proots_count q {x. 0 < x})"
[PROOF STATE]
proof (prove)
using this:
int (proots_count q {x. 0 < x}) \<le> changes (coeffs q) \<and> even (changes (coeffs q) - int (proots_count q {x. 0 < x}))

goal (1 subgoal):
 1. proots_count q {x. 0 < x} \<le> nat (changes (coeffs q)) \<and> even (nat (changes (coeffs q)) - proots_count q {x. 0 < x})
[PROOF STEP]
using even_nat_iff
[PROOF STATE]
proof (prove)
using this:
int (proots_count q {x. 0 < x}) \<le> changes (coeffs q) \<and> even (changes (coeffs q) - int (proots_count q {x. 0 < x}))
0 \<le> ?k \<Longrightarrow> even (nat ?k) = even ?k

goal (1 subgoal):
 1. proots_count q {x. 0 < x} \<le> nat (changes (coeffs q)) \<and> even (nat (changes (coeffs q)) - proots_count q {x. 0 < x})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proots_count q {x. 0 < x} \<le> nat (changes (coeffs q)) \<and> even (nat (changes (coeffs q)) - proots_count q {x. 0 < x})

goal (1 subgoal):
 1. proots_count p {x. a < x \<and> x < b} \<le> descartes_roots_test a b p \<and> even (descartes_roots_test a b p - proots_count p {x. a < x \<and> x < b})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
proots_count p {x. a < x \<and> x < b} = proots_count q {x. 0 < x}
proots_count q {x. 0 < x} \<le> nat (changes (coeffs q)) \<and> even (nat (changes (coeffs q)) - proots_count q {x. 0 < x})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
proots_count p {x. a < x \<and> x < b} = proots_count q {x. 0 < x}
proots_count q {x. 0 < x} \<le> nat (changes (coeffs q)) \<and> even (nat (changes (coeffs q)) - proots_count q {x. 0 < x})

goal (1 subgoal):
 1. proots_count p {x. a < x \<and> x < b} \<le> descartes_roots_test a b p \<and> even (descartes_roots_test a b p - proots_count p {x. a < x \<and> x < b})
[PROOF STEP]
unfolding descartes_roots_test_def
[PROOF STATE]
proof (prove)
using this:
proots_count p {x. a < x \<and> x < b} = proots_count q {x. 0 < x}
proots_count q {x. 0 < x} \<le> nat (changes (coeffs q)) \<and> even (nat (changes (coeffs q)) - proots_count q {x. 0 < x})

goal (1 subgoal):
 1. proots_count p {x. a < x \<and> x < b} \<le> nat (changes (coeffs (fcompose p [:a, b:] [:1, 1:]))) \<and> even (nat (changes (coeffs (fcompose p [:a, b:] [:1, 1:]))) - proots_count p {x. a < x \<and> x < b})
[PROOF STEP]
apply (fold q_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>proots_count p {x. a < x \<and> x < b} = proots_count q {x. 0 < x}; proots_count q {x. 0 < x} \<le> nat (changes (coeffs q)) \<and> even (nat (changes (coeffs q)) - proots_count q {x. 0 < x})\<rbrakk> \<Longrightarrow> proots_count p {x. a < x \<and> x < b} \<le> nat (changes (coeffs q)) \<and> even (nat (changes (coeffs q)) - proots_count p {x. a < x \<and> x < b})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proots_count p {x. a < x \<and> x < b} \<le> descartes_roots_test a b p \<and> even (descartes_roots_test a b p - proots_count p {x. a < x \<and> x < b})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma I_eval: "\<I> \<degree> x \<rightarrow>\<^sub>\<beta> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I> \<degree> x \<rightarrow>\<^sub>\<beta> x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<I> \<degree> x \<rightarrow>\<^sub>\<beta> x
[PROOF STEP]
have "\<I> \<degree> x \<rightarrow>\<^sub>\<beta> Var 0[x/0]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I> \<degree> x \<rightarrow>\<^sub>\<beta> Var 0[x/0]
[PROOF STEP]
unfolding I_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs (Var 0) \<degree> x \<rightarrow>\<^sub>\<beta> Var 0[x/0]
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<I> \<degree> x \<rightarrow>\<^sub>\<beta> Var 0[x/0]

goal (1 subgoal):
 1. \<I> \<degree> x \<rightarrow>\<^sub>\<beta> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<I> \<degree> x \<rightarrow>\<^sub>\<beta> Var 0[x/0]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<I> \<degree> x \<rightarrow>\<^sub>\<beta> Var 0[x/0]

goal (1 subgoal):
 1. \<I> \<degree> x \<rightarrow>\<^sub>\<beta> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<I> \<degree> x \<rightarrow>\<^sub>\<beta> x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma I_equiv[iff]: "\<I> \<degree> x \<leftrightarrow> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I> \<degree> x \<leftrightarrow> x
[PROOF STEP]
using I_eval
[PROOF STATE]
proof (prove)
using this:
\<I> \<degree> ?x \<rightarrow>\<^sub>\<beta> ?x

goal (1 subgoal):
 1. \<I> \<degree> x \<leftrightarrow> x
[PROOF STEP]
..


[STATEMENT]
lemma I_closed[simp]: "liftn n \<I> k = \<I>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftn n \<I> k = \<I>
[PROOF STEP]
unfolding I_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftn n (Abs (Var 0)) k = Abs (Var 0)
[PROOF STEP]
by simp


[STATEMENT]
lemma B_eval1: "\<B> \<degree> g \<rightarrow>\<^sub>\<beta> Abs (Abs (lift (lift g 0) 0 \<degree> (Var 1 \<degree> Var 0)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<B> \<degree> g \<rightarrow>\<^sub>\<beta> Abs (Abs (lift (lift g 0) 0 \<degree> (Var 1 \<degree> Var 0)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<B> \<degree> g \<rightarrow>\<^sub>\<beta> Abs (Abs (lift (lift g 0) 0 \<degree> (Var 1 \<degree> Var 0)))
[PROOF STEP]
have "\<B> \<degree> g \<rightarrow>\<^sub>\<beta> Abs (Abs (Var 2 \<degree> (Var 1 \<degree> Var 0))) [g/0]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<B> \<degree> g \<rightarrow>\<^sub>\<beta> Abs (Abs (Var 2 \<degree> (Var 1 \<degree> Var 0)))[g/0]
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs (Abs (Abs (Var 2 \<degree> (Var 1 \<degree> Var 0)))) \<degree> g \<rightarrow>\<^sub>\<beta> Abs (Abs (Var 2 \<degree> (Var 1 \<degree> Var 0)))[g/0]
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<B> \<degree> g \<rightarrow>\<^sub>\<beta> Abs (Abs (Var 2 \<degree> (Var 1 \<degree> Var 0)))[g/0]

goal (1 subgoal):
 1. \<B> \<degree> g \<rightarrow>\<^sub>\<beta> Abs (Abs (lift (lift g 0) 0 \<degree> (Var 1 \<degree> Var 0)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<B> \<degree> g \<rightarrow>\<^sub>\<beta> Abs (Abs (Var 2 \<degree> (Var 1 \<degree> Var 0)))[g/0]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<B> \<degree> g \<rightarrow>\<^sub>\<beta> Abs (Abs (Var 2 \<degree> (Var 1 \<degree> Var 0)))[g/0]

goal (1 subgoal):
 1. \<B> \<degree> g \<rightarrow>\<^sub>\<beta> Abs (Abs (lift (lift g 0) 0 \<degree> (Var 1 \<degree> Var 0)))
[PROOF STEP]
by (simp add: numerals)
[PROOF STATE]
proof (state)
this:
\<B> \<degree> g \<rightarrow>\<^sub>\<beta> Abs (Abs (lift (lift g 0) 0 \<degree> (Var 1 \<degree> Var 0)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma B_eval2: "\<B> \<degree> g \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (lift g 0 \<degree> (lift f 0 \<degree> Var 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<B> \<degree> g \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (lift g 0 \<degree> (lift f 0 \<degree> Var 0))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<B> \<degree> g \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (lift g 0 \<degree> (lift f 0 \<degree> Var 0))
[PROOF STEP]
have "\<B> \<degree> g \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (Abs (lift (lift g 0) 0 \<degree> (Var 1 \<degree> Var 0))) \<degree> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<B> \<degree> g \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (Abs (lift (lift g 0) 0 \<degree> (Var 1 \<degree> Var 0))) \<degree> f
[PROOF STEP]
using B_eval1
[PROOF STATE]
proof (prove)
using this:
\<B> \<degree> ?g \<rightarrow>\<^sub>\<beta> Abs (Abs (lift (lift ?g 0) 0 \<degree> (Var 1 \<degree> Var 0)))

goal (1 subgoal):
 1. \<B> \<degree> g \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (Abs (lift (lift g 0) 0 \<degree> (Var 1 \<degree> Var 0))) \<degree> f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<B> \<degree> g \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (Abs (lift (lift g 0) 0 \<degree> (Var 1 \<degree> Var 0))) \<degree> f

goal (1 subgoal):
 1. \<B> \<degree> g \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (lift g 0 \<degree> (lift f 0 \<degree> Var 0))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<B> \<degree> g \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (Abs (lift (lift g 0) 0 \<degree> (Var 1 \<degree> Var 0))) \<degree> f

goal (1 subgoal):
 1. \<B> \<degree> g \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (lift g 0 \<degree> (lift f 0 \<degree> Var 0))
[PROOF STEP]
have "... \<rightarrow>\<^sub>\<beta> Abs (lift (lift g 0) 0 \<degree> (Var 1 \<degree> Var 0)) [f/0]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs (Abs (lift (lift g 0) 0 \<degree> (Var 1 \<degree> Var 0))) \<degree> f \<rightarrow>\<^sub>\<beta> Abs (lift (lift g 0) 0 \<degree> (Var 1 \<degree> Var 0))[f/0]
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
Abs (Abs (lift (lift g 0) 0 \<degree> (Var 1 \<degree> Var 0))) \<degree> f \<rightarrow>\<^sub>\<beta> Abs (lift (lift g 0) 0 \<degree> (Var 1 \<degree> Var 0))[f/0]

goal (1 subgoal):
 1. \<B> \<degree> g \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (lift g 0 \<degree> (lift f 0 \<degree> Var 0))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs (Abs (lift (lift g 0) 0 \<degree> (Var 1 \<degree> Var 0))) \<degree> f \<rightarrow>\<^sub>\<beta> Abs (lift (lift g 0) 0 \<degree> (Var 1 \<degree> Var 0))[f/0]

goal (1 subgoal):
 1. \<B> \<degree> g \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (lift g 0 \<degree> (lift f 0 \<degree> Var 0))
[PROOF STEP]
have "... = Abs (lift g 0 \<degree> (lift f 0 \<degree> Var 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs (lift (lift g 0) 0 \<degree> (Var 1 \<degree> Var 0))[f/0] = Abs (lift g 0 \<degree> (lift f 0 \<degree> Var 0))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Abs (lift (lift g 0) 0 \<degree> (Var 1 \<degree> Var 0))[f/0] = Abs (lift g 0 \<degree> (lift f 0 \<degree> Var 0))

goal (1 subgoal):
 1. \<B> \<degree> g \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (lift g 0 \<degree> (lift f 0 \<degree> Var 0))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<B> \<degree> g \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (lift g 0 \<degree> (lift f 0 \<degree> Var 0))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<B> \<degree> g \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (lift g 0 \<degree> (lift f 0 \<degree> Var 0))

goal (1 subgoal):
 1. \<B> \<degree> g \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (lift g 0 \<degree> (lift f 0 \<degree> Var 0))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<B> \<degree> g \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (lift g 0 \<degree> (lift f 0 \<degree> Var 0))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma B_eval: "\<B> \<degree> g \<degree> f \<degree> x \<rightarrow>\<^sub>\<beta>\<^sup>* g \<degree> (f \<degree> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<B> \<degree> g \<degree> f \<degree> x \<rightarrow>\<^sub>\<beta>\<^sup>* g \<degree> (f \<degree> x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<B> \<degree> g \<degree> f \<degree> x \<rightarrow>\<^sub>\<beta>\<^sup>* g \<degree> (f \<degree> x)
[PROOF STEP]
have "\<B> \<degree> g \<degree> f \<degree> x \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (lift g 0 \<degree> (lift f 0 \<degree> Var 0)) \<degree> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<B> \<degree> g \<degree> f \<degree> x \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (lift g 0 \<degree> (lift f 0 \<degree> Var 0)) \<degree> x
[PROOF STEP]
using B_eval2
[PROOF STATE]
proof (prove)
using this:
\<B> \<degree> ?g \<degree> ?f \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (lift ?g 0 \<degree> (lift ?f 0 \<degree> Var 0))

goal (1 subgoal):
 1. \<B> \<degree> g \<degree> f \<degree> x \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (lift g 0 \<degree> (lift f 0 \<degree> Var 0)) \<degree> x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<B> \<degree> g \<degree> f \<degree> x \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (lift g 0 \<degree> (lift f 0 \<degree> Var 0)) \<degree> x

goal (1 subgoal):
 1. \<B> \<degree> g \<degree> f \<degree> x \<rightarrow>\<^sub>\<beta>\<^sup>* g \<degree> (f \<degree> x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<B> \<degree> g \<degree> f \<degree> x \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (lift g 0 \<degree> (lift f 0 \<degree> Var 0)) \<degree> x

goal (1 subgoal):
 1. \<B> \<degree> g \<degree> f \<degree> x \<rightarrow>\<^sub>\<beta>\<^sup>* g \<degree> (f \<degree> x)
[PROOF STEP]
have "... \<rightarrow>\<^sub>\<beta> (lift g 0 \<degree> (lift f 0 \<degree> Var 0)) [x/0]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs (lift g 0 \<degree> (lift f 0 \<degree> Var 0)) \<degree> x \<rightarrow>\<^sub>\<beta> (lift g 0 \<degree> (lift f 0 \<degree> Var 0))[x/0]
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
Abs (lift g 0 \<degree> (lift f 0 \<degree> Var 0)) \<degree> x \<rightarrow>\<^sub>\<beta> (lift g 0 \<degree> (lift f 0 \<degree> Var 0))[x/0]

goal (1 subgoal):
 1. \<B> \<degree> g \<degree> f \<degree> x \<rightarrow>\<^sub>\<beta>\<^sup>* g \<degree> (f \<degree> x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs (lift g 0 \<degree> (lift f 0 \<degree> Var 0)) \<degree> x \<rightarrow>\<^sub>\<beta> (lift g 0 \<degree> (lift f 0 \<degree> Var 0))[x/0]

goal (1 subgoal):
 1. \<B> \<degree> g \<degree> f \<degree> x \<rightarrow>\<^sub>\<beta>\<^sup>* g \<degree> (f \<degree> x)
[PROOF STEP]
have "... = g \<degree> (f \<degree> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lift g 0 \<degree> (lift f 0 \<degree> Var 0))[x/0] = g \<degree> (f \<degree> x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(lift g 0 \<degree> (lift f 0 \<degree> Var 0))[x/0] = g \<degree> (f \<degree> x)

goal (1 subgoal):
 1. \<B> \<degree> g \<degree> f \<degree> x \<rightarrow>\<^sub>\<beta>\<^sup>* g \<degree> (f \<degree> x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<B> \<degree> g \<degree> f \<degree> x \<rightarrow>\<^sub>\<beta>\<^sup>* g \<degree> (f \<degree> x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<B> \<degree> g \<degree> f \<degree> x \<rightarrow>\<^sub>\<beta>\<^sup>* g \<degree> (f \<degree> x)

goal (1 subgoal):
 1. \<B> \<degree> g \<degree> f \<degree> x \<rightarrow>\<^sub>\<beta>\<^sup>* g \<degree> (f \<degree> x)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<B> \<degree> g \<degree> f \<degree> x \<rightarrow>\<^sub>\<beta>\<^sup>* g \<degree> (f \<degree> x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma B_equiv[iff]: "\<B> \<degree> g \<degree> f \<degree> x \<leftrightarrow> g \<degree> (f \<degree> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<B> \<degree> g \<degree> f \<degree> x \<leftrightarrow> g \<degree> (f \<degree> x)
[PROOF STEP]
using B_eval
[PROOF STATE]
proof (prove)
using this:
\<B> \<degree> ?g \<degree> ?f \<degree> ?x \<rightarrow>\<^sub>\<beta>\<^sup>* ?g \<degree> (?f \<degree> ?x)

goal (1 subgoal):
 1. \<B> \<degree> g \<degree> f \<degree> x \<leftrightarrow> g \<degree> (f \<degree> x)
[PROOF STEP]
..


[STATEMENT]
lemma B_closed[simp]: "liftn n \<B> k = \<B>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftn n \<B> k = \<B>
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftn n (Abs (Abs (Abs (Var 2 \<degree> (Var 1 \<degree> Var 0))))) k = Abs (Abs (Abs (Var 2 \<degree> (Var 1 \<degree> Var 0))))
[PROOF STEP]
by simp


[STATEMENT]
lemma T_eval1: "\<T> \<degree> x \<rightarrow>\<^sub>\<beta> Abs (Var 0 \<degree> lift x 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<T> \<degree> x \<rightarrow>\<^sub>\<beta> Abs (Var 0 \<degree> lift x 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<T> \<degree> x \<rightarrow>\<^sub>\<beta> Abs (Var 0 \<degree> lift x 0)
[PROOF STEP]
have "\<T> \<degree> x \<rightarrow>\<^sub>\<beta> Abs (Var 0 \<degree> Var 1) [x/0]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<T> \<degree> x \<rightarrow>\<^sub>\<beta> Abs (Var 0 \<degree> Var 1)[x/0]
[PROOF STEP]
unfolding T_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs (Abs (Var 0 \<degree> Var 1)) \<degree> x \<rightarrow>\<^sub>\<beta> Abs (Var 0 \<degree> Var 1)[x/0]
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<T> \<degree> x \<rightarrow>\<^sub>\<beta> Abs (Var 0 \<degree> Var 1)[x/0]

goal (1 subgoal):
 1. \<T> \<degree> x \<rightarrow>\<^sub>\<beta> Abs (Var 0 \<degree> lift x 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<T> \<degree> x \<rightarrow>\<^sub>\<beta> Abs (Var 0 \<degree> Var 1)[x/0]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<T> \<degree> x \<rightarrow>\<^sub>\<beta> Abs (Var 0 \<degree> Var 1)[x/0]

goal (1 subgoal):
 1. \<T> \<degree> x \<rightarrow>\<^sub>\<beta> Abs (Var 0 \<degree> lift x 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<T> \<degree> x \<rightarrow>\<^sub>\<beta> Abs (Var 0 \<degree> lift x 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma T_eval: "\<T> \<degree> x \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* f \<degree> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<T> \<degree> x \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* f \<degree> x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<T> \<degree> x \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* f \<degree> x
[PROOF STEP]
have "\<T> \<degree> x \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (Var 0 \<degree> lift x 0) \<degree> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<T> \<degree> x \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (Var 0 \<degree> lift x 0) \<degree> f
[PROOF STEP]
using T_eval1
[PROOF STATE]
proof (prove)
using this:
\<T> \<degree> ?x \<rightarrow>\<^sub>\<beta> Abs (Var 0 \<degree> lift ?x 0)

goal (1 subgoal):
 1. \<T> \<degree> x \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (Var 0 \<degree> lift x 0) \<degree> f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<T> \<degree> x \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (Var 0 \<degree> lift x 0) \<degree> f

goal (1 subgoal):
 1. \<T> \<degree> x \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* f \<degree> x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<T> \<degree> x \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* Abs (Var 0 \<degree> lift x 0) \<degree> f

goal (1 subgoal):
 1. \<T> \<degree> x \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* f \<degree> x
[PROOF STEP]
have "... \<rightarrow>\<^sub>\<beta> (Var 0 \<degree> lift x 0) [f/0]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs (Var 0 \<degree> lift x 0) \<degree> f \<rightarrow>\<^sub>\<beta> (Var 0 \<degree> lift x 0)[f/0]
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
Abs (Var 0 \<degree> lift x 0) \<degree> f \<rightarrow>\<^sub>\<beta> (Var 0 \<degree> lift x 0)[f/0]

goal (1 subgoal):
 1. \<T> \<degree> x \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* f \<degree> x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs (Var 0 \<degree> lift x 0) \<degree> f \<rightarrow>\<^sub>\<beta> (Var 0 \<degree> lift x 0)[f/0]

goal (1 subgoal):
 1. \<T> \<degree> x \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* f \<degree> x
[PROOF STEP]
have "... = f \<degree> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Var 0 \<degree> lift x 0)[f/0] = f \<degree> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(Var 0 \<degree> lift x 0)[f/0] = f \<degree> x

goal (1 subgoal):
 1. \<T> \<degree> x \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* f \<degree> x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<T> \<degree> x \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* f \<degree> x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<T> \<degree> x \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* f \<degree> x

goal (1 subgoal):
 1. \<T> \<degree> x \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* f \<degree> x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<T> \<degree> x \<degree> f \<rightarrow>\<^sub>\<beta>\<^sup>* f \<degree> x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma T_equiv[iff]: "\<T> \<degree> x \<degree> f \<leftrightarrow> f \<degree> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<T> \<degree> x \<degree> f \<leftrightarrow> f \<degree> x
[PROOF STEP]
using T_eval
[PROOF STATE]
proof (prove)
using this:
\<T> \<degree> ?x \<degree> ?f \<rightarrow>\<^sub>\<beta>\<^sup>* ?f \<degree> ?x

goal (1 subgoal):
 1. \<T> \<degree> x \<degree> f \<leftrightarrow> f \<degree> x
[PROOF STEP]
..


[STATEMENT]
lemma T_closed[simp]: "liftn n \<T> k = \<T>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftn n \<T> k = \<T>
[PROOF STEP]
unfolding T_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftn n (Abs (Abs (Var 0 \<degree> Var 1))) k = Abs (Abs (Var 0 \<degree> Var 1))
[PROOF STEP]
by simp


[STATEMENT]
lemma sorted_descending_Cons: "sorted_descending (x#xs) \<longleftrightarrow> sorted_descending xs \<and> (\<forall>y\<in>set xs. y \<le> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_descending (x # xs) = (sorted_descending xs \<and> (\<forall>y\<in>set xs. y \<le> x))
[PROOF STEP]
by(induction xs) auto


[STATEMENT]
lemma sorted_descending_tail: "sorted_descending (xs@[x]) \<longleftrightarrow> sorted_descending xs \<and> (\<forall>y\<in>set xs. x \<le> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_descending (xs @ [x]) = (sorted_descending xs \<and> (\<forall>y\<in>set xs. x \<le> y))
[PROOF STEP]
by(induction xs) auto


[STATEMENT]
lemma sorted_descending_append: "sorted_descending (xs @ ys) =
    (sorted_descending xs \<and> sorted_descending ys \<and> (\<forall>x\<in>set xs. \<forall>y\<in>set ys. x \<ge> y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_descending (xs @ ys) = (sorted_descending xs \<and> sorted_descending ys \<and> (\<forall>x\<in>set xs. \<forall>y\<in>set ys. y \<le> x))
[PROOF STEP]
by(induction xs) auto


[STATEMENT]
lemma sorted_descending: "sorted_descending (rev xs) \<longleftrightarrow> sorted xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_descending (rev xs) = sorted xs
[PROOF STEP]
apply(induction xs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. sorted_descending (rev []) = sorted []
 2. \<And>a xs. sorted_descending (rev xs) = sorted xs \<Longrightarrow> sorted_descending (rev (a # xs)) = sorted (a # xs)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs. sorted_descending (rev xs) = sorted xs \<Longrightarrow> sorted_descending (rev (a # xs)) = sorted (a # xs)
[PROOF STEP]
apply(auto simp add: sorted_descending_tail)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sorted_descending_alt: "sorted_descending xs \<longleftrightarrow> sorted (rev xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_descending xs = sorted (rev xs)
[PROOF STEP]
using sorted_descending[of "rev xs"]
[PROOF STATE]
proof (prove)
using this:
sorted_descending (rev (rev xs)) = sorted (rev xs)

goal (1 subgoal):
 1. sorted_descending xs = sorted (rev xs)
[PROOF STEP]
unfolding rev_rev_ident
[PROOF STATE]
proof (prove)
using this:
sorted_descending xs = sorted (rev xs)

goal (1 subgoal):
 1. sorted_descending xs = sorted (rev xs)
[PROOF STEP]
.


[STATEMENT]
lemma sort_descending: "sorted_descending (sort_descending_key (\<lambda>x. x) xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_descending (sort_descending_key (\<lambda>x. x) xs)
[PROOF STEP]
by(simp add: sort_descending_key_def sorted_descending)


[STATEMENT]
lemma sort_descending_key_distinct: "distinct xs \<Longrightarrow> distinct (sort_descending_key f xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct xs \<Longrightarrow> distinct (sort_descending_key f xs)
[PROOF STEP]
by(simp add: sort_descending_key_def)


[STATEMENT]
lemma sorted_descending_sort_descending_key: "sorted_descending (map f (sort_descending_key f xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_descending (map f (sort_descending_key f xs))
[PROOF STEP]
apply(simp add: sort_descending_key_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_descending (map f (rev (sort_key f xs)))
[PROOF STEP]
using sorted_descending
[PROOF STATE]
proof (prove)
using this:
sorted_descending (rev ?xs) = sorted ?xs

goal (1 subgoal):
 1. sorted_descending (map f (rev (sort_key f xs)))
[PROOF STEP]
by (metis rev_map sorted_sort_key)


[STATEMENT]
lemma sorted_descending_split: "sorted_descending (map f l) \<Longrightarrow>
  	\<exists>m n. l = m @ n \<and> (\<forall>e \<in> set m. f (hd l) = f e) \<and> (\<forall>e \<in> set n. f e < f (hd l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_descending (map f l) \<Longrightarrow> \<exists>m n. l = m @ n \<and> (\<forall>e\<in>set m. f (hd l) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd l))
[PROOF STEP]
proof(induction l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sorted_descending (map f []) \<Longrightarrow> \<exists>m n. [] = m @ n \<and> (\<forall>e\<in>set m. f (hd []) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd []))
 2. \<And>a l. \<lbrakk>sorted_descending (map f l) \<Longrightarrow> \<exists>m n. l = m @ n \<and> (\<forall>e\<in>set m. f (hd l) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd l)); sorted_descending (map f (a # l))\<rbrakk> \<Longrightarrow> \<exists>m n. a # l = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # l)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # l)))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
sorted_descending (map f [])

goal (2 subgoals):
 1. sorted_descending (map f []) \<Longrightarrow> \<exists>m n. [] = m @ n \<and> (\<forall>e\<in>set m. f (hd []) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd []))
 2. \<And>a l. \<lbrakk>sorted_descending (map f l) \<Longrightarrow> \<exists>m n. l = m @ n \<and> (\<forall>e\<in>set m. f (hd l) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd l)); sorted_descending (map f (a # l))\<rbrakk> \<Longrightarrow> \<exists>m n. a # l = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # l)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # l)))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
sorted_descending (map f [])

goal (1 subgoal):
 1. \<exists>m n. [] = m @ n \<and> (\<forall>e\<in>set m. f (hd []) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd []))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>m n. [] = m @ n \<and> (\<forall>e\<in>set m. f (hd []) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd []))

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>sorted_descending (map f l) \<Longrightarrow> \<exists>m n. l = m @ n \<and> (\<forall>e\<in>set m. f (hd l) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd l)); sorted_descending (map f (a # l))\<rbrakk> \<Longrightarrow> \<exists>m n. a # l = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # l)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # l)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l. \<lbrakk>sorted_descending (map f l) \<Longrightarrow> \<exists>m n. l = m @ n \<and> (\<forall>e\<in>set m. f (hd l) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd l)); sorted_descending (map f (a # l))\<rbrakk> \<Longrightarrow> \<exists>m n. a # l = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # l)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # l)))
[PROOF STEP]
case (Cons a as)
[PROOF STATE]
proof (state)
this:
sorted_descending (map f as) \<Longrightarrow> \<exists>m n. as = m @ n \<and> (\<forall>e\<in>set m. f (hd as) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd as))
sorted_descending (map f (a # as))

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>sorted_descending (map f l) \<Longrightarrow> \<exists>m n. l = m @ n \<and> (\<forall>e\<in>set m. f (hd l) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd l)); sorted_descending (map f (a # l))\<rbrakk> \<Longrightarrow> \<exists>m n. a # l = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # l)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # l)))
[PROOF STEP]
from Cons(2)
[PROOF STATE]
proof (chain)
picking this:
sorted_descending (map f (a # as))
[PROOF STEP]
have IHm: "sorted_descending (map f as)"
[PROOF STATE]
proof (prove)
using this:
sorted_descending (map f (a # as))

goal (1 subgoal):
 1. sorted_descending (map f as)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sorted_descending (map f as)

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>sorted_descending (map f l) \<Longrightarrow> \<exists>m n. l = m @ n \<and> (\<forall>e\<in>set m. f (hd l) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd l)); sorted_descending (map f (a # l))\<rbrakk> \<Longrightarrow> \<exists>m n. a # l = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # l)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # l)))
[PROOF STEP]
note mIH = Cons(1)[OF this]
[PROOF STATE]
proof (state)
this:
\<exists>m n. as = m @ n \<and> (\<forall>e\<in>set m. f (hd as) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd as))

goal (1 subgoal):
 1. \<And>a l. \<lbrakk>sorted_descending (map f l) \<Longrightarrow> \<exists>m n. l = m @ n \<and> (\<forall>e\<in>set m. f (hd l) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd l)); sorted_descending (map f (a # l))\<rbrakk> \<Longrightarrow> \<exists>m n. a # l = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # l)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # l)))
[PROOF STEP]
thus ?case (is ?kees)
[PROOF STATE]
proof (prove)
using this:
\<exists>m n. as = m @ n \<and> (\<forall>e\<in>set m. f (hd as) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd as))

goal (1 subgoal):
 1. \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
[PROOF STEP]
proof(cases as)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<exists>m n. as = m @ n \<and> (\<forall>e\<in>set m. f (hd as) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd as)); as = []\<rbrakk> \<Longrightarrow> \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
 2. \<And>aa list. \<lbrakk>\<exists>m n. as = m @ n \<and> (\<forall>e\<in>set m. f (hd as) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd as)); as = aa # list\<rbrakk> \<Longrightarrow> \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
as = []

goal (2 subgoals):
 1. \<lbrakk>\<exists>m n. as = m @ n \<and> (\<forall>e\<in>set m. f (hd as) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd as)); as = []\<rbrakk> \<Longrightarrow> \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
 2. \<And>aa list. \<lbrakk>\<exists>m n. as = m @ n \<and> (\<forall>e\<in>set m. f (hd as) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd as)); as = aa # list\<rbrakk> \<Longrightarrow> \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
[PROOF STEP]
show ?kees
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
[PROOF STEP]
unfolding Nil
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m n. [a] = m @ n \<and> (\<forall>e\<in>set m. f (hd [a]) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd [a]))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))

goal (1 subgoal):
 1. \<And>aa list. \<lbrakk>\<exists>m n. as = m @ n \<and> (\<forall>e\<in>set m. f (hd as) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd as)); as = aa # list\<rbrakk> \<Longrightarrow> \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa list. \<lbrakk>\<exists>m n. as = m @ n \<and> (\<forall>e\<in>set m. f (hd as) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd as)); as = aa # list\<rbrakk> \<Longrightarrow> \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
[PROOF STEP]
case (Cons aa ass)
[PROOF STATE]
proof (state)
this:
as = aa # ass

goal (1 subgoal):
 1. \<And>aa list. \<lbrakk>\<exists>m n. as = m @ n \<and> (\<forall>e\<in>set m. f (hd as) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd as)); as = aa # list\<rbrakk> \<Longrightarrow> \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
[PROOF STEP]
show ?kees
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
[PROOF STEP]
proof(cases "f a = f aa")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f a = f aa \<Longrightarrow> \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
 2. f a \<noteq> f aa \<Longrightarrow> \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
f a = f aa

goal (2 subgoals):
 1. f a = f aa \<Longrightarrow> \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
 2. f a \<noteq> f aa \<Longrightarrow> \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
[PROOF STEP]
from mIH
[PROOF STATE]
proof (chain)
picking this:
\<exists>m n. as = m @ n \<and> (\<forall>e\<in>set m. f (hd as) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd as))
[PROOF STEP]
obtain m n where mn: "as = m @ n" "(\<forall>e\<in>set m. f a = f e)" "(\<forall>e\<in>set n. f e < f a)"
[PROOF STATE]
proof (prove)
using this:
\<exists>m n. as = m @ n \<and> (\<forall>e\<in>set m. f (hd as) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd as))

goal (1 subgoal):
 1. (\<And>m n. \<lbrakk>as = m @ n; \<forall>e\<in>set m. f a = f e; \<forall>e\<in>set n. f e < f a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using True local.Cons
[PROOF STATE]
proof (prove)
using this:
\<exists>m n. as = m @ n \<and> (\<forall>e\<in>set m. f (hd as) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd as))
f a = f aa
as = aa # ass

goal (1 subgoal):
 1. (\<And>m n. \<lbrakk>as = m @ n; \<forall>e\<in>set m. f a = f e; \<forall>e\<in>set n. f e < f a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
as = m @ n
\<forall>e\<in>set m. f a = f e
\<forall>e\<in>set n. f e < f a

goal (2 subgoals):
 1. f a = f aa \<Longrightarrow> \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
 2. f a \<noteq> f aa \<Longrightarrow> \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
[PROOF STEP]
have "a # as = a # m @ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a # as = a # m @ n
[PROOF STEP]
using mn(1)
[PROOF STATE]
proof (prove)
using this:
as = m @ n

goal (1 subgoal):
 1. a # as = a # m @ n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a # as = a # m @ n

goal (2 subgoals):
 1. f a = f aa \<Longrightarrow> \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
 2. f a \<noteq> f aa \<Longrightarrow> \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a # as = a # m @ n

goal (2 subgoals):
 1. f a = f aa \<Longrightarrow> \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
 2. f a \<noteq> f aa \<Longrightarrow> \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
[PROOF STEP]
have "\<forall>e\<in>set (a # m). f (hd (a # m)) = f e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>e\<in>set (a # m). f (hd (a # m)) = f e
[PROOF STEP]
unfolding list.sel(1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>e\<in>set (a # m). f a = f e
[PROOF STEP]
using True mn(2)
[PROOF STATE]
proof (prove)
using this:
f a = f aa
\<forall>e\<in>set m. f a = f e

goal (1 subgoal):
 1. \<forall>e\<in>set (a # m). f a = f e
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
f a = f aa
\<forall>e\<in>set m. f a = f e
as = aa # ass

goal (1 subgoal):
 1. \<forall>e\<in>set (a # m). f a = f e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>e\<in>set (a # m). f (hd (a # m)) = f e

goal (2 subgoals):
 1. f a = f aa \<Longrightarrow> \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
 2. f a \<noteq> f aa \<Longrightarrow> \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a # as = a # m @ n
\<forall>e\<in>set (a # m). f (hd (a # m)) = f e
[PROOF STEP]
show "\<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and>
  				(\<forall>e\<in>set n. f e < f (hd (a # as)))"
[PROOF STATE]
proof (prove)
using this:
a # as = a # m @ n
\<forall>e\<in>set (a # m). f (hd (a # m)) = f e

goal (1 subgoal):
 1. \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
[PROOF STEP]
using mn(3)
[PROOF STATE]
proof (prove)
using this:
a # as = a # m @ n
\<forall>e\<in>set (a # m). f (hd (a # m)) = f e
\<forall>e\<in>set n. f e < f a

goal (1 subgoal):
 1. \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
[PROOF STEP]
by (metis append.simps(2) list.sel(1))
[PROOF STATE]
proof (state)
this:
\<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))

goal (1 subgoal):
 1. f a \<noteq> f aa \<Longrightarrow> \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f a \<noteq> f aa \<Longrightarrow> \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
f a \<noteq> f aa

goal (1 subgoal):
 1. f a \<noteq> f aa \<Longrightarrow> \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
[PROOF STEP]
from Cons.prems
[PROOF STATE]
proof (chain)
picking this:
sorted_descending (map f (a # as))
[PROOF STEP]
have "\<forall>y\<in>set (map f as). y < f a"
[PROOF STATE]
proof (prove)
using this:
sorted_descending (map f (a # as))

goal (1 subgoal):
 1. \<forall>y\<in>set (map f as). y < f a
[PROOF STEP]
unfolding list.map(2)
[PROOF STATE]
proof (prove)
using this:
sorted_descending (f a # map f as)

goal (1 subgoal):
 1. \<forall>y\<in>set (map f as). y < f a
[PROOF STEP]
unfolding sorted_descending_Cons
[PROOF STATE]
proof (prove)
using this:
sorted_descending (map f as) \<and> (\<forall>y\<in>set (map f as). y \<le> f a)

goal (1 subgoal):
 1. \<forall>y\<in>set (map f as). y < f a
[PROOF STEP]
unfolding set_map
[PROOF STATE]
proof (prove)
using this:
sorted_descending (map f as) \<and> (\<forall>y\<in>f ` set as. y \<le> f a)

goal (1 subgoal):
 1. \<forall>y\<in>f ` set as. y < f a
[PROOF STEP]
unfolding local.Cons
[PROOF STATE]
proof (prove)
using this:
sorted_descending (map f (aa # ass)) \<and> (\<forall>y\<in>f ` set (aa # ass). y \<le> f a)

goal (1 subgoal):
 1. \<forall>y\<in>f ` set (aa # ass). y < f a
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
sorted_descending (map f (aa # ass)) \<and> (\<forall>y\<in>f ` set (aa # ass). y \<le> f a)
f a \<noteq> f aa

goal (1 subgoal):
 1. \<forall>y\<in>f ` set (aa # ass). y < f a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>set (map f as). y < f a

goal (1 subgoal):
 1. f a \<noteq> f aa \<Longrightarrow> \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>y\<in>set (map f as). y < f a
[PROOF STEP]
have "\<forall>e\<in>set as. f e < f a"
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<in>set (map f as). y < f a

goal (1 subgoal):
 1. \<forall>e\<in>set as. f e < f a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>e\<in>set as. f e < f a

goal (1 subgoal):
 1. f a \<noteq> f aa \<Longrightarrow> \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>e\<in>set as. f e < f a

goal (1 subgoal):
 1. f a \<noteq> f aa \<Longrightarrow> \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
[PROOF STEP]
have "a # as = [a] @ as \<and> (\<forall>e\<in>set [a]. f (hd [a]) = f e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a # as = [a] @ as \<and> (\<forall>e\<in>set [a]. f (hd [a]) = f e)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a # as = [a] @ as \<and> (\<forall>e\<in>set [a]. f (hd [a]) = f e)

goal (1 subgoal):
 1. f a \<noteq> f aa \<Longrightarrow> \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>e\<in>set as. f e < f a
a # as = [a] @ as \<and> (\<forall>e\<in>set [a]. f (hd [a]) = f e)
[PROOF STEP]
show ?kees
[PROOF STATE]
proof (prove)
using this:
\<forall>e\<in>set as. f e < f a
a # as = [a] @ as \<and> (\<forall>e\<in>set [a]. f (hd [a]) = f e)

goal (1 subgoal):
 1. \<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))
[PROOF STEP]
by (metis list.sel(1))
[PROOF STATE]
proof (state)
this:
\<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>m n. a # as = m @ n \<and> (\<forall>e\<in>set m. f (hd (a # as)) = f e) \<and> (\<forall>e\<in>set n. f e < f (hd (a # as)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sort_descending_set_inv[simp]: "set (sort_descending_key k t) = set t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (sort_descending_key k t) = set t
[PROOF STEP]
by (simp add: sort_descending_key_def)


[STATEMENT]
lemma SeqAuto_EmptySet:
 "({@x .True}, (@x .True), {}, {}) \<in> {(S,I,L,D) | S I L D. SeqAuto S I L D}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({SOME x. True}, SOME x. True, {}, {}) \<in> {(S, I, L, D) |S I L D. SeqAuto S I L D}
[PROOF STEP]
by (unfold SeqAuto_def, auto)


[STATEMENT]
lemma Rep_seqauto_tuple:
  "Rep_seqauto SA = (States SA, InitState SA, Labels SA, Delta SA)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_seqauto SA = (States SA, InitState SA, Labels SA, Delta SA)
[PROOF STEP]
by (unfold States_def InitState_def Labels_def Delta_def, auto)


[STATEMENT]
lemma Rep_seqauto_select:
  "(States SA,InitState SA,Labels SA,Delta SA) \<in>  seqauto"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (States SA, InitState SA, Labels SA, Delta SA) \<in> seqauto
[PROOF STEP]
by (rule Rep_seqauto_tuple [THEN subst], rule Rep_seqauto)


[STATEMENT]
lemma SeqAuto_select:
  "SeqAuto (States SA) (InitState SA) (Labels SA) (Delta SA)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SeqAuto (States SA) (InitState SA) (Labels SA) (Delta SA)
[PROOF STEP]
by (cut_tac SA=SA in Rep_seqauto_select, unfold seqauto_def, auto)


[STATEMENT]
lemma neq_States [simp]:
  "States SA \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. States SA \<noteq> {}
[PROOF STEP]
apply (cut_tac Rep_seqauto_select)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (States ?SA1, InitState ?SA1, Labels ?SA1, Delta ?SA1) \<in> seqauto \<Longrightarrow> States SA \<noteq> {}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(States ?SA1, InitState ?SA1, Labels ?SA1, Delta ?SA1) \<in> seqauto; States SA = {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (unfold seqauto_def SeqAuto_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(States ?SA1, InitState ?SA1, Labels ?SA1, Delta ?SA1) \<in> {(S, I, L, D) |S I L D. I \<in> S \<and> S \<noteq> {} \<and> finite S \<and> finite D \<and> (\<forall>(s, l, t)\<in>D. s \<in> S \<and> t \<in> S \<and> l \<in> L)}; States SA = {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma SA_States_disjunct :
 "(States A) \<inter> (States A') = {} \<Longrightarrow> A' \<noteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. States A \<inter> States A' = {} \<Longrightarrow> A' \<noteq> A
[PROOF STEP]
by auto


[STATEMENT]
lemma SA_States_disjunct2 :
 "\<lbrakk> (States A) \<inter> C = {}; States B \<subseteq> C \<rbrakk> \<Longrightarrow> B \<noteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>States A \<inter> C = {}; States B \<subseteq> C\<rbrakk> \<Longrightarrow> B \<noteq> A
[PROOF STEP]
apply (rule SA_States_disjunct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>States A \<inter> C = {}; States B \<subseteq> C\<rbrakk> \<Longrightarrow> States A \<inter> States B = {}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma SA_States_disjunct3 :
 "\<lbrakk> C \<inter> States A = {}; States B \<subseteq> C \<rbrakk> \<Longrightarrow>  States A \<inter> States B = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C \<inter> States A = {}; States B \<subseteq> C\<rbrakk> \<Longrightarrow> States A \<inter> States B = {}
[PROOF STEP]
apply (cut_tac SA=B in neq_States)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C \<inter> States A = {}; States B \<subseteq> C; States B \<noteq> {}\<rbrakk> \<Longrightarrow> States A \<inter> States B = {}
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma EX_State_SA [simp]:
  "\<exists> S. S \<in> States SA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>S. S \<in> States SA
[PROOF STEP]
apply (cut_tac Rep_seqauto_select)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (States ?SA1, InitState ?SA1, Labels ?SA1, Delta ?SA1) \<in> seqauto \<Longrightarrow> \<exists>S. S \<in> States SA
[PROOF STEP]
apply (unfold seqauto_def SeqAuto_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (States ?SA1, InitState ?SA1, Labels ?SA1, Delta ?SA1) \<in> {(S, I, L, D) |S I L D. I \<in> S \<and> S \<noteq> {} \<and> finite S \<and> finite D \<and> (\<forall>(s, l, t)\<in>D. s \<in> S \<and> t \<in> S \<and> l \<in> L)} \<Longrightarrow> \<exists>S. S \<in> States SA
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma finite_States [simp]:
  "finite (States A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (States A)
[PROOF STEP]
apply (cut_tac Rep_seqauto_select)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (States ?SA1, InitState ?SA1, Labels ?SA1, Delta ?SA1) \<in> seqauto \<Longrightarrow> finite (States A)
[PROOF STEP]
apply (unfold seqauto_def SeqAuto_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (States ?SA1, InitState ?SA1, Labels ?SA1, Delta ?SA1) \<in> {(S, I, L, D) |S I L D. I \<in> S \<and> S \<noteq> {} \<and> finite S \<and> finite D \<and> (\<forall>(s, l, t)\<in>D. s \<in> S \<and> t \<in> S \<and> l \<in> L)} \<Longrightarrow> finite (States A)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma finite_Delta [simp]:
  "finite (Delta A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (Delta A)
[PROOF STEP]
apply (cut_tac Rep_seqauto_select)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (States ?SA1, InitState ?SA1, Labels ?SA1, Delta ?SA1) \<in> seqauto \<Longrightarrow> finite (Delta A)
[PROOF STEP]
apply (unfold seqauto_def SeqAuto_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (States ?SA1, InitState ?SA1, Labels ?SA1, Delta ?SA1) \<in> {(S, I, L, D) |S I L D. I \<in> S \<and> S \<noteq> {} \<and> finite S \<and> finite D \<and> (\<forall>(s, l, t)\<in>D. s \<in> S \<and> t \<in> S \<and> l \<in> L)} \<Longrightarrow> finite (Delta A)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma InitState_States [simp]:
  "InitState A \<in> States A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. InitState A \<in> States A
[PROOF STEP]
apply (cut_tac Rep_seqauto_select)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (States ?SA1, InitState ?SA1, Labels ?SA1, Delta ?SA1) \<in> seqauto \<Longrightarrow> InitState A \<in> States A
[PROOF STEP]
apply (unfold seqauto_def SeqAuto_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (States ?SA1, InitState ?SA1, Labels ?SA1, Delta ?SA1) \<in> {(S, I, L, D) |S I L D. I \<in> S \<and> S \<noteq> {} \<and> finite S \<and> finite D \<and> (\<forall>(s, l, t)\<in>D. s \<in> S \<and> t \<in> S \<and> l \<in> L)} \<Longrightarrow> InitState A \<in> States A
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma SeqAuto_EmptySet_States [simp]:
 "(States (Abs_seqauto ({@x. True}, (@x. True), {}, {}))) = {(@x. True)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. States (Abs_seqauto ({SOME x. True}, SOME x. True, {}, {})) = {SOME x. True}
[PROOF STEP]
apply (unfold States_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst \<circ> Rep_seqauto) (Abs_seqauto ({SOME x. True}, SOME x. True, {}, {})) = {SOME x. True}
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Rep_seqauto (Abs_seqauto ({SOME x. True}, SOME x. True, {}, {}))) = {SOME x. True}
[PROOF STEP]
apply (subst Abs_seqauto_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ({SOME x. True}, SOME x. True, {}, {}) \<in> seqauto
 2. fst ({SOME x. True}, SOME x. True, {}, {}) = {SOME x. True}
[PROOF STEP]
apply (unfold seqauto_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ({SOME x. True}, SOME x. True, {}, {}) \<in> {(S, I, L, D) |S I L D. SeqAuto S I L D}
 2. fst ({SOME x. True}, SOME x. True, {}, {}) = {SOME x. True}
[PROOF STEP]
apply (rule SeqAuto_EmptySet)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ({SOME x. True}, SOME x. True, {}, {}) = {SOME x. True}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma SeqAuto_EmptySet_SAEvents [simp]:
 "(SAEvents (Abs_seqauto ({@x. True}, (@x. True), {}, {}))) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SAEvents (Abs_seqauto ({SOME x. True}, SOME x. True, {}, {})) = {}
[PROOF STEP]
apply (unfold SAEvents_def Delta_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>l\<in>Label ((snd \<circ> snd \<circ> snd \<circ> Rep_seqauto) (Abs_seqauto ({SOME x. True}, SOME x. True, {}, {}))). fst (action l) \<union> ExprEvents (expr l)) = {}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>Label (snd (snd (snd (Rep_seqauto (Abs_seqauto ({SOME x. True}, SOME x. True, {}, {})))))). fst (action x) = {} \<and> ExprEvents (expr x) = {}
[PROOF STEP]
apply (subst Abs_seqauto_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ({SOME x. True}, SOME x. True, {}, {}) \<in> seqauto
 2. \<forall>x\<in>Label (snd (snd (snd ({SOME x. True}, SOME x. True, {}, {})))). fst (action x) = {} \<and> ExprEvents (expr x) = {}
[PROOF STEP]
apply (unfold seqauto_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ({SOME x. True}, SOME x. True, {}, {}) \<in> {(S, I, L, D) |S I L D. SeqAuto S I L D}
 2. \<forall>x\<in>Label (snd (snd (snd ({SOME x. True}, SOME x. True, {}, {})))). fst (action x) = {} \<and> ExprEvents (expr x) = {}
[PROOF STEP]
apply (rule SeqAuto_EmptySet)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>Label (snd (snd (snd ({SOME x. True}, SOME x. True, {}, {})))). fst (action x) = {} \<and> ExprEvents (expr x) = {}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Label_Delta_subset [simp]:
  "(Label (Delta SA)) \<subseteq> Labels SA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Label (Delta SA) \<subseteq> Labels SA
[PROOF STEP]
apply (unfold Label_def label_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>t. fst (snd t)) ` Delta SA \<subseteq> Labels SA
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa ab b ac ad ba. (ac, (ad, aa, ab, b), ba) \<in> Delta SA \<Longrightarrow> (ad, aa, ab, b) \<in> Labels SA
[PROOF STEP]
apply (cut_tac SA=SA in SeqAuto_select)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa ab b ac ad ba. \<lbrakk>(ac, (ad, aa, ab, b), ba) \<in> Delta SA; SeqAuto (States SA) (InitState SA) (Labels SA) (Delta SA)\<rbrakk> \<Longrightarrow> (ad, aa, ab, b) \<in> Labels SA
[PROOF STEP]
apply (unfold SeqAuto_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa ab b ac ad ba. \<lbrakk>(ac, (ad, aa, ab, b), ba) \<in> Delta SA; InitState SA \<in> States SA \<and> States SA \<noteq> {} \<and> finite (States SA) \<and> finite (Delta SA) \<and> (\<forall>(s, l, t)\<in>Delta SA. s \<in> States SA \<and> t \<in> States SA \<and> l \<in> Labels SA)\<rbrakk> \<Longrightarrow> (ad, aa, ab, b) \<in> Labels SA
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Target_SAs_Delta_States:
  "Target (\<Union>(Delta ` (SAs HA))) \<subseteq> \<Union>(States ` (SAs HA))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Target (\<Union> (Delta ` SAs HA)) \<subseteq> \<Union> (States ` SAs HA)
[PROOF STEP]
apply (unfold image_def Target_def target_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. \<exists>x\<in>\<Union> {y. \<exists>x\<in>SAs HA. y = Delta x}. y = snd (snd x)} \<subseteq> \<Union> {y. \<exists>x\<in>SAs HA. y = States x}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa a aa ab ac b ba. \<lbrakk>xa \<in> SAs HA; (a, (aa, ab, ac, b), ba) \<in> Delta xa\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>xa\<in>SAs HA. x = States xa) \<and> ba \<in> x
[PROOF STEP]
apply (rename_tac SA Source Trigger Guard Action Update Target)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>SA Source Trigger Guard Action Update Target. \<lbrakk>SA \<in> SAs HA; (Source, (Trigger, Guard, Action, Update), Target) \<in> Delta SA\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>xa\<in>SAs HA. x = States xa) \<and> Target \<in> x
[PROOF STEP]
apply (cut_tac SA=SA in SeqAuto_select)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>SA Source Trigger Guard Action Update Target. \<lbrakk>SA \<in> SAs HA; (Source, (Trigger, Guard, Action, Update), Target) \<in> Delta SA; SeqAuto (States SA) (InitState SA) (Labels SA) (Delta SA)\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>xa\<in>SAs HA. x = States xa) \<and> Target \<in> x
[PROOF STEP]
apply (unfold SeqAuto_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>SA Source Trigger Guard Action Update Target. \<lbrakk>SA \<in> SAs HA; (Source, (Trigger, Guard, Action, Update), Target) \<in> Delta SA; InitState SA \<in> States SA \<and> States SA \<noteq> {} \<and> finite (States SA) \<and> finite (Delta SA) \<and> (\<forall>(s, l, t)\<in>Delta SA. s \<in> States SA \<and> t \<in> States SA \<and> l \<in> Labels SA)\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>xa\<in>SAs HA. x = States xa) \<and> Target \<in> x
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma States_Int_not_mem:
 "(\<Union>(States ` F) Int States SA) = {} \<Longrightarrow> SA \<notin> F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (States ` F) \<inter> States SA = {} \<Longrightarrow> SA \<notin> F
[PROOF STEP]
apply (unfold Int_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> \<Union> (States ` F). x \<in> States SA} = {} \<Longrightarrow> SA \<notin> F
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. (\<forall>xa\<in>F. x \<notin> States xa) \<or> x \<notin> States SA; SA \<in> F\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (subgoal_tac "\<exists> S. S \<in> States SA")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x. (\<forall>xa\<in>F. x \<notin> States xa) \<or> x \<notin> States SA; SA \<in> F; \<exists>S. S \<in> States SA\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<forall>x. (\<forall>xa\<in>F. x \<notin> States xa) \<or> x \<notin> States SA; SA \<in> F\<rbrakk> \<Longrightarrow> \<exists>S. S \<in> States SA
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x. (\<forall>xa\<in>F. x \<notin> States xa) \<or> x \<notin> States SA; SA \<in> F\<rbrakk> \<Longrightarrow> \<exists>S. S \<in> States SA
 2. \<lbrakk>\<forall>x. (\<forall>xa\<in>F. x \<notin> States xa) \<or> x \<notin> States SA; SA \<in> F; \<exists>S. S \<in> States SA\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (rule EX_State_SA)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. (\<forall>xa\<in>F. x \<notin> States xa) \<or> x \<notin> States SA; SA \<in> F; \<exists>S. S \<in> States SA\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S. \<lbrakk>\<forall>x. (\<forall>xa\<in>F. x \<notin> States xa) \<or> x \<notin> States SA; SA \<in> F; S \<in> States SA\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (rename_tac T)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>T. \<lbrakk>\<forall>x. (\<forall>xa\<in>F. x \<notin> States xa) \<or> x \<notin> States SA; SA \<in> F; T \<in> States SA\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule_tac x=T in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>T. \<lbrakk>SA \<in> F; T \<in> States SA; (\<forall>x\<in>F. T \<notin> States x) \<or> T \<notin> States SA\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Delta_target_States [simp]:
  "\<lbrakk> T \<in> Delta A\<rbrakk> \<Longrightarrow> target T \<in> States A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T \<in> Delta A \<Longrightarrow> target T \<in> States A
[PROOF STEP]
apply (cut_tac SA=A in SeqAuto_select)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>T \<in> Delta A; SeqAuto (States A) (InitState A) (Labels A) (Delta A)\<rbrakk> \<Longrightarrow> target T \<in> States A
[PROOF STEP]
apply (unfold SeqAuto_def source_def target_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>T \<in> Delta A; InitState A \<in> States A \<and> States A \<noteq> {} \<and> finite (States A) \<and> finite (Delta A) \<and> (\<forall>(s, l, t)\<in>Delta A. s \<in> States A \<and> t \<in> States A \<and> l \<in> Labels A)\<rbrakk> \<Longrightarrow> snd (snd T) \<in> States A
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Delta_source_States [simp]:
  "\<lbrakk> T \<in> Delta A \<rbrakk> \<Longrightarrow> source T \<in> States A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T \<in> Delta A \<Longrightarrow> source T \<in> States A
[PROOF STEP]
apply (cut_tac SA=A in SeqAuto_select)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>T \<in> Delta A; SeqAuto (States A) (InitState A) (Labels A) (Delta A)\<rbrakk> \<Longrightarrow> source T \<in> States A
[PROOF STEP]
apply (unfold SeqAuto_def source_def target_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>T \<in> Delta A; InitState A \<in> States A \<and> States A \<noteq> {} \<and> finite (States A) \<and> finite (Delta A) \<and> (\<forall>(s, l, t)\<in>Delta A. s \<in> States A \<and> t \<in> States A \<and> l \<in> Labels A)\<rbrakk> \<Longrightarrow> fst T \<in> States A
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [simp]: "validTrans aid trn \<Longrightarrow> lreach aid (srcOf trn) \<Longrightarrow> \<phi> aid trn \<Longrightarrow> comOf aid trn = Internal"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>System_Specification.validTrans trn; System_Specification.reach (srcOf trn); \<phi> aid trn\<rbrakk> \<Longrightarrow> comOf aid trn = Internal
[PROOF STEP]
by (cases trn) (auto elim: Issuer.\<phi>E)


[STATEMENT]
theorem secure: "secure"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. secure
[PROOF STEP]
proof (intro preserve_source_secure ballI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nid. nid \<in> nodes' \<Longrightarrow> Abstract_BD_Security.secure (System_Specification.validFrom istate) (Net.lV nid) (Net.lO nid) (B nid) (BD_Security_IO.never (\<lambda>a. False))
[PROOF STEP]
fix aid
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nid. nid \<in> nodes' \<Longrightarrow> Abstract_BD_Security.secure (System_Specification.validFrom istate) (Net.lV nid) (Net.lO nid) (B nid) (BD_Security_IO.never (\<lambda>a. False))
[PROOF STEP]
assume "aid \<in> AIDs - {AID}"
[PROOF STATE]
proof (state)
this:
aid \<in> nodes'

goal (1 subgoal):
 1. \<And>nid. nid \<in> nodes' \<Longrightarrow> Abstract_BD_Security.secure (System_Specification.validFrom istate) (Net.lV nid) (Net.lO nid) (B nid) (BD_Security_IO.never (\<lambda>a. False))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
aid \<in> nodes'
[PROOF STEP]
show "Net.lsecure aid"
[PROOF STATE]
proof (prove)
using this:
aid \<in> nodes'

goal (1 subgoal):
 1. Abstract_BD_Security.secure (System_Specification.validFrom istate) (Net.lV aid) (Net.lO aid) (B aid) (BD_Security_IO.never (\<lambda>a. False))
[PROOF STEP]
by (intro Abstract_BD_Security.B_id_secure) (auto simp: B_id_def)
[PROOF STATE]
proof (state)
this:
Abstract_BD_Security.secure (System_Specification.validFrom istate) (Net.lV aid) (Net.lO aid) (B aid) (BD_Security_IO.never (\<lambda>a. False))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_first_correct:
  assumes "find_first x xs = Some i"
  shows "i < length xs" "xs ! i = x" "x \<notin> set (take i xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length xs &&& xs ! i = x &&& x \<notin> set (take i xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
find_first x xs = Some i

goal (1 subgoal):
 1. i < length xs &&& xs ! i = x &&& x \<notin> set (take i xs)
[PROOF STEP]
proof (induction xs arbitrary: i)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>i. find_first x [] = Some i \<Longrightarrow> i < length []
 2. \<And>i. find_first x [] = Some i \<Longrightarrow> [] ! i = x
 3. \<And>i. find_first x [] = Some i \<Longrightarrow> x \<notin> set (take i [])
 4. \<And>a xs i. \<lbrakk>\<And>i. find_first x xs = Some i \<Longrightarrow> i < length xs; \<And>i. find_first x xs = Some i \<Longrightarrow> xs ! i = x; \<And>i. find_first x xs = Some i \<Longrightarrow> x \<notin> set (take i xs); find_first x (a # xs) = Some i\<rbrakk> \<Longrightarrow> i < length (a # xs)
 5. \<And>a xs i. \<lbrakk>\<And>i. find_first x xs = Some i \<Longrightarrow> i < length xs; \<And>i. find_first x xs = Some i \<Longrightarrow> xs ! i = x; \<And>i. find_first x xs = Some i \<Longrightarrow> x \<notin> set (take i xs); find_first x (a # xs) = Some i\<rbrakk> \<Longrightarrow> (a # xs) ! i = x
 6. \<And>a xs i. \<lbrakk>\<And>i. find_first x xs = Some i \<Longrightarrow> i < length xs; \<And>i. find_first x xs = Some i \<Longrightarrow> xs ! i = x; \<And>i. find_first x xs = Some i \<Longrightarrow> x \<notin> set (take i xs); find_first x (a # xs) = Some i\<rbrakk> \<Longrightarrow> x \<notin> set (take i (a # xs))
[PROOF STEP]
case (Cons y ys)
[PROOF STATE]
proof (state)
this:
find_first x ys = Some ?i \<Longrightarrow> ?i < length ys
find_first x ys = Some ?i \<Longrightarrow> ys ! ?i = x
find_first x ys = Some ?i \<Longrightarrow> x \<notin> set (take ?i ys)

goal (6 subgoals):
 1. \<And>i. find_first x [] = Some i \<Longrightarrow> i < length []
 2. \<And>i. find_first x [] = Some i \<Longrightarrow> [] ! i = x
 3. \<And>i. find_first x [] = Some i \<Longrightarrow> x \<notin> set (take i [])
 4. \<And>a xs i. \<lbrakk>\<And>i. find_first x xs = Some i \<Longrightarrow> i < length xs; \<And>i. find_first x xs = Some i \<Longrightarrow> xs ! i = x; \<And>i. find_first x xs = Some i \<Longrightarrow> x \<notin> set (take i xs); find_first x (a # xs) = Some i\<rbrakk> \<Longrightarrow> i < length (a # xs)
 5. \<And>a xs i. \<lbrakk>\<And>i. find_first x xs = Some i \<Longrightarrow> i < length xs; \<And>i. find_first x xs = Some i \<Longrightarrow> xs ! i = x; \<And>i. find_first x xs = Some i \<Longrightarrow> x \<notin> set (take i xs); find_first x (a # xs) = Some i\<rbrakk> \<Longrightarrow> (a # xs) ! i = x
 6. \<And>a xs i. \<lbrakk>\<And>i. find_first x xs = Some i \<Longrightarrow> i < length xs; \<And>i. find_first x xs = Some i \<Longrightarrow> xs ! i = x; \<And>i. find_first x xs = Some i \<Longrightarrow> x \<notin> set (take i xs); find_first x (a # xs) = Some i\<rbrakk> \<Longrightarrow> x \<notin> set (take i (a # xs))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
find_first x ys = Some ?i \<Longrightarrow> ?i < length ys
find_first x ys = Some ?i \<Longrightarrow> ys ! ?i = x
find_first x ys = Some ?i \<Longrightarrow> x \<notin> set (take ?i ys)

goal (6 subgoals):
 1. \<And>i. find_first x [] = Some i \<Longrightarrow> i < length []
 2. \<And>i. find_first x [] = Some i \<Longrightarrow> [] ! i = x
 3. \<And>i. find_first x [] = Some i \<Longrightarrow> x \<notin> set (take i [])
 4. \<And>a xs i. \<lbrakk>\<And>i. find_first x xs = Some i \<Longrightarrow> i < length xs; \<And>i. find_first x xs = Some i \<Longrightarrow> xs ! i = x; \<And>i. find_first x xs = Some i \<Longrightarrow> x \<notin> set (take i xs); find_first x (a # xs) = Some i\<rbrakk> \<Longrightarrow> i < length (a # xs)
 5. \<And>a xs i. \<lbrakk>\<And>i. find_first x xs = Some i \<Longrightarrow> i < length xs; \<And>i. find_first x xs = Some i \<Longrightarrow> xs ! i = x; \<And>i. find_first x xs = Some i \<Longrightarrow> x \<notin> set (take i xs); find_first x (a # xs) = Some i\<rbrakk> \<Longrightarrow> (a # xs) ! i = x
 6. \<And>a xs i. \<lbrakk>\<And>i. find_first x xs = Some i \<Longrightarrow> i < length xs; \<And>i. find_first x xs = Some i \<Longrightarrow> xs ! i = x; \<And>i. find_first x xs = Some i \<Longrightarrow> x \<notin> set (take i xs); find_first x (a # xs) = Some i\<rbrakk> \<Longrightarrow> x \<notin> set (take i (a # xs))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
find_first x (y # ys) = Some i

goal (6 subgoals):
 1. \<And>i. find_first x [] = Some i \<Longrightarrow> i < length []
 2. \<And>i. find_first x [] = Some i \<Longrightarrow> [] ! i = x
 3. \<And>i. find_first x [] = Some i \<Longrightarrow> x \<notin> set (take i [])
 4. \<And>a xs i. \<lbrakk>\<And>i. find_first x xs = Some i \<Longrightarrow> i < length xs; \<And>i. find_first x xs = Some i \<Longrightarrow> xs ! i = x; \<And>i. find_first x xs = Some i \<Longrightarrow> x \<notin> set (take i xs); find_first x (a # xs) = Some i\<rbrakk> \<Longrightarrow> i < length (a # xs)
 5. \<And>a xs i. \<lbrakk>\<And>i. find_first x xs = Some i \<Longrightarrow> i < length xs; \<And>i. find_first x xs = Some i \<Longrightarrow> xs ! i = x; \<And>i. find_first x xs = Some i \<Longrightarrow> x \<notin> set (take i xs); find_first x (a # xs) = Some i\<rbrakk> \<Longrightarrow> (a # xs) ! i = x
 6. \<And>a xs i. \<lbrakk>\<And>i. find_first x xs = Some i \<Longrightarrow> i < length xs; \<And>i. find_first x xs = Some i \<Longrightarrow> xs ! i = x; \<And>i. find_first x xs = Some i \<Longrightarrow> x \<notin> set (take i xs); find_first x (a # xs) = Some i\<rbrakk> \<Longrightarrow> x \<notin> set (take i (a # xs))
[PROOF STEP]
with Cons
[PROOF STATE]
proof (chain)
picking this:
find_first x ys = Some ?i \<Longrightarrow> ?i < length ys
find_first x ys = Some ?i \<Longrightarrow> ys ! ?i = x
find_first x ys = Some ?i \<Longrightarrow> x \<notin> set (take ?i ys)
find_first x (y # ys) = Some i
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
find_first x ys = Some ?i \<Longrightarrow> ?i < length ys
find_first x ys = Some ?i \<Longrightarrow> ys ! ?i = x
find_first x ys = Some ?i \<Longrightarrow> x \<notin> set (take ?i ys)
find_first x (y # ys) = Some i

goal (1 subgoal):
 1. i < length (y # ys)
[PROOF STEP]
by (cases "x = y") auto
[PROOF STATE]
proof (state)
this:
i < length (y # ys)

goal (5 subgoals):
 1. \<And>i. find_first x [] = Some i \<Longrightarrow> i < length []
 2. \<And>i. find_first x [] = Some i \<Longrightarrow> [] ! i = x
 3. \<And>i. find_first x [] = Some i \<Longrightarrow> x \<notin> set (take i [])
 4. \<And>a xs i. \<lbrakk>\<And>i. find_first x xs = Some i \<Longrightarrow> i < length xs; \<And>i. find_first x xs = Some i \<Longrightarrow> xs ! i = x; \<And>i. find_first x xs = Some i \<Longrightarrow> x \<notin> set (take i xs); find_first x (a # xs) = Some i\<rbrakk> \<Longrightarrow> (a # xs) ! i = x
 5. \<And>a xs i. \<lbrakk>\<And>i. find_first x xs = Some i \<Longrightarrow> i < length xs; \<And>i. find_first x xs = Some i \<Longrightarrow> xs ! i = x; \<And>i. find_first x xs = Some i \<Longrightarrow> x \<notin> set (take i xs); find_first x (a # xs) = Some i\<rbrakk> \<Longrightarrow> x \<notin> set (take i (a # xs))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
find_first x (y # ys) = Some ?ia2 \<Longrightarrow> ?ia2 < length (y # ys)

goal (5 subgoals):
 1. \<And>i. find_first x [] = Some i \<Longrightarrow> i < length []
 2. \<And>i. find_first x [] = Some i \<Longrightarrow> [] ! i = x
 3. \<And>i. find_first x [] = Some i \<Longrightarrow> x \<notin> set (take i [])
 4. \<And>a xs i. \<lbrakk>\<And>i. find_first x xs = Some i \<Longrightarrow> i < length xs; \<And>i. find_first x xs = Some i \<Longrightarrow> xs ! i = x; \<And>i. find_first x xs = Some i \<Longrightarrow> x \<notin> set (take i xs); find_first x (a # xs) = Some i\<rbrakk> \<Longrightarrow> (a # xs) ! i = x
 5. \<And>a xs i. \<lbrakk>\<And>i. find_first x xs = Some i \<Longrightarrow> i < length xs; \<And>i. find_first x xs = Some i \<Longrightarrow> xs ! i = x; \<And>i. find_first x xs = Some i \<Longrightarrow> x \<notin> set (take i xs); find_first x (a # xs) = Some i\<rbrakk> \<Longrightarrow> x \<notin> set (take i (a # xs))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
find_first x (y # ys) = Some ?ia2 \<Longrightarrow> ?ia2 < length (y # ys)

goal (5 subgoals):
 1. \<And>i. find_first x [] = Some i \<Longrightarrow> i < length []
 2. \<And>i. find_first x [] = Some i \<Longrightarrow> [] ! i = x
 3. \<And>i. find_first x [] = Some i \<Longrightarrow> x \<notin> set (take i [])
 4. \<And>a xs i. \<lbrakk>\<And>i. find_first x xs = Some i \<Longrightarrow> i < length xs; \<And>i. find_first x xs = Some i \<Longrightarrow> xs ! i = x; \<And>i. find_first x xs = Some i \<Longrightarrow> x \<notin> set (take i xs); find_first x (a # xs) = Some i\<rbrakk> \<Longrightarrow> (a # xs) ! i = x
 5. \<And>a xs i. \<lbrakk>\<And>i. find_first x xs = Some i \<Longrightarrow> i < length xs; \<And>i. find_first x xs = Some i \<Longrightarrow> xs ! i = x; \<And>i. find_first x xs = Some i \<Longrightarrow> x \<notin> set (take i xs); find_first x (a # xs) = Some i\<rbrakk> \<Longrightarrow> x \<notin> set (take i (a # xs))
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
find_first x (y # ys) = Some i

goal (5 subgoals):
 1. \<And>i. find_first x [] = Some i \<Longrightarrow> i < length []
 2. \<And>i. find_first x [] = Some i \<Longrightarrow> [] ! i = x
 3. \<And>i. find_first x [] = Some i \<Longrightarrow> x \<notin> set (take i [])
 4. \<And>a xs i. \<lbrakk>\<And>i. find_first x xs = Some i \<Longrightarrow> i < length xs; \<And>i. find_first x xs = Some i \<Longrightarrow> xs ! i = x; \<And>i. find_first x xs = Some i \<Longrightarrow> x \<notin> set (take i xs); find_first x (a # xs) = Some i\<rbrakk> \<Longrightarrow> (a # xs) ! i = x
 5. \<And>a xs i. \<lbrakk>\<And>i. find_first x xs = Some i \<Longrightarrow> i < length xs; \<And>i. find_first x xs = Some i \<Longrightarrow> xs ! i = x; \<And>i. find_first x xs = Some i \<Longrightarrow> x \<notin> set (take i xs); find_first x (a # xs) = Some i\<rbrakk> \<Longrightarrow> x \<notin> set (take i (a # xs))
[PROOF STEP]
with Cons
[PROOF STATE]
proof (chain)
picking this:
find_first x ys = Some ?i \<Longrightarrow> ?i < length ys
find_first x ys = Some ?i \<Longrightarrow> ys ! ?i = x
find_first x ys = Some ?i \<Longrightarrow> x \<notin> set (take ?i ys)
find_first x (y # ys) = Some i
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
find_first x ys = Some ?i \<Longrightarrow> ?i < length ys
find_first x ys = Some ?i \<Longrightarrow> ys ! ?i = x
find_first x ys = Some ?i \<Longrightarrow> x \<notin> set (take ?i ys)
find_first x (y # ys) = Some i

goal (1 subgoal):
 1. (y # ys) ! i = x
[PROOF STEP]
by (cases "x = y") auto
[PROOF STATE]
proof (state)
this:
(y # ys) ! i = x

goal (4 subgoals):
 1. \<And>i. find_first x [] = Some i \<Longrightarrow> i < length []
 2. \<And>i. find_first x [] = Some i \<Longrightarrow> [] ! i = x
 3. \<And>i. find_first x [] = Some i \<Longrightarrow> x \<notin> set (take i [])
 4. \<And>a xs i. \<lbrakk>\<And>i. find_first x xs = Some i \<Longrightarrow> i < length xs; \<And>i. find_first x xs = Some i \<Longrightarrow> xs ! i = x; \<And>i. find_first x xs = Some i \<Longrightarrow> x \<notin> set (take i xs); find_first x (a # xs) = Some i\<rbrakk> \<Longrightarrow> x \<notin> set (take i (a # xs))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
find_first x (y # ys) = Some ?ia2 \<Longrightarrow> (y # ys) ! ?ia2 = x

goal (4 subgoals):
 1. \<And>i. find_first x [] = Some i \<Longrightarrow> i < length []
 2. \<And>i. find_first x [] = Some i \<Longrightarrow> [] ! i = x
 3. \<And>i. find_first x [] = Some i \<Longrightarrow> x \<notin> set (take i [])
 4. \<And>a xs i. \<lbrakk>\<And>i. find_first x xs = Some i \<Longrightarrow> i < length xs; \<And>i. find_first x xs = Some i \<Longrightarrow> xs ! i = x; \<And>i. find_first x xs = Some i \<Longrightarrow> x \<notin> set (take i xs); find_first x (a # xs) = Some i\<rbrakk> \<Longrightarrow> x \<notin> set (take i (a # xs))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
find_first x (y # ys) = Some ?ia2 \<Longrightarrow> (y # ys) ! ?ia2 = x

goal (4 subgoals):
 1. \<And>i. find_first x [] = Some i \<Longrightarrow> i < length []
 2. \<And>i. find_first x [] = Some i \<Longrightarrow> [] ! i = x
 3. \<And>i. find_first x [] = Some i \<Longrightarrow> x \<notin> set (take i [])
 4. \<And>a xs i. \<lbrakk>\<And>i. find_first x xs = Some i \<Longrightarrow> i < length xs; \<And>i. find_first x xs = Some i \<Longrightarrow> xs ! i = x; \<And>i. find_first x xs = Some i \<Longrightarrow> x \<notin> set (take i xs); find_first x (a # xs) = Some i\<rbrakk> \<Longrightarrow> x \<notin> set (take i (a # xs))
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
find_first x (y # ys) = Some i

goal (4 subgoals):
 1. \<And>i. find_first x [] = Some i \<Longrightarrow> i < length []
 2. \<And>i. find_first x [] = Some i \<Longrightarrow> [] ! i = x
 3. \<And>i. find_first x [] = Some i \<Longrightarrow> x \<notin> set (take i [])
 4. \<And>a xs i. \<lbrakk>\<And>i. find_first x xs = Some i \<Longrightarrow> i < length xs; \<And>i. find_first x xs = Some i \<Longrightarrow> xs ! i = x; \<And>i. find_first x xs = Some i \<Longrightarrow> x \<notin> set (take i xs); find_first x (a # xs) = Some i\<rbrakk> \<Longrightarrow> x \<notin> set (take i (a # xs))
[PROOF STEP]
with Cons
[PROOF STATE]
proof (chain)
picking this:
find_first x ys = Some ?i \<Longrightarrow> ?i < length ys
find_first x ys = Some ?i \<Longrightarrow> ys ! ?i = x
find_first x ys = Some ?i \<Longrightarrow> x \<notin> set (take ?i ys)
find_first x (y # ys) = Some i
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
find_first x ys = Some ?i \<Longrightarrow> ?i < length ys
find_first x ys = Some ?i \<Longrightarrow> ys ! ?i = x
find_first x ys = Some ?i \<Longrightarrow> x \<notin> set (take ?i ys)
find_first x (y # ys) = Some i

goal (1 subgoal):
 1. x \<notin> set (take i (y # ys))
[PROOF STEP]
by (cases "x = y") auto
[PROOF STATE]
proof (state)
this:
x \<notin> set (take i (y # ys))

goal (3 subgoals):
 1. \<And>i. find_first x [] = Some i \<Longrightarrow> i < length []
 2. \<And>i. find_first x [] = Some i \<Longrightarrow> [] ! i = x
 3. \<And>i. find_first x [] = Some i \<Longrightarrow> x \<notin> set (take i [])
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
find_first x (y # ys) = Some ?ia2 \<Longrightarrow> x \<notin> set (take ?ia2 (y # ys))

goal (3 subgoals):
 1. \<And>i. find_first x [] = Some i \<Longrightarrow> i < length []
 2. \<And>i. find_first x [] = Some i \<Longrightarrow> [] ! i = x
 3. \<And>i. find_first x [] = Some i \<Longrightarrow> x \<notin> set (take i [])
[PROOF STEP]
qed auto


[STATEMENT]
lemma find_first_none: "x \<notin> set xs \<Longrightarrow> find_first x xs = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> set xs \<Longrightarrow> find_first x xs = None
[PROOF STEP]
by (induct xs) auto


[STATEMENT]
lemma find_first_some_strong:
  assumes "x \<in> set (take n xs)" "n \<le> length xs"
  obtains i where "find_first x xs = Some i" "i < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. \<lbrakk>find_first x xs = Some i; i < n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> set (take n xs)
n \<le> length xs

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>find_first x xs = Some i; i < n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (induction xs arbitrary: thesis n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>thesis n. \<lbrakk>\<And>i. \<lbrakk>find_first x [] = Some i; i < n\<rbrakk> \<Longrightarrow> thesis; x \<in> set (take n []); n \<le> length []\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a xs thesis n. \<lbrakk>\<And>thesis n. \<lbrakk>\<And>i. \<lbrakk>find_first x xs = Some i; i < n\<rbrakk> \<Longrightarrow> thesis; x \<in> set (take n xs); n \<le> length xs\<rbrakk> \<Longrightarrow> thesis; \<And>i. \<lbrakk>find_first x (a # xs) = Some i; i < n\<rbrakk> \<Longrightarrow> thesis; x \<in> set (take n (a # xs)); n \<le> length (a # xs)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (Cons y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>i. \<lbrakk>find_first x ys = Some i; i < ?n\<rbrakk> \<Longrightarrow> ?thesis; x \<in> set (take ?n ys); ?n \<le> length ys\<rbrakk> \<Longrightarrow> ?thesis
\<lbrakk>find_first x (y # ys) = Some ?i; ?i < n\<rbrakk> \<Longrightarrow> thesis
x \<in> set (take n (y # ys))
n \<le> length (y # ys)

goal (2 subgoals):
 1. \<And>thesis n. \<lbrakk>\<And>i. \<lbrakk>find_first x [] = Some i; i < n\<rbrakk> \<Longrightarrow> thesis; x \<in> set (take n []); n \<le> length []\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a xs thesis n. \<lbrakk>\<And>thesis n. \<lbrakk>\<And>i. \<lbrakk>find_first x xs = Some i; i < n\<rbrakk> \<Longrightarrow> thesis; x \<in> set (take n xs); n \<le> length xs\<rbrakk> \<Longrightarrow> thesis; \<And>i. \<lbrakk>find_first x (a # xs) = Some i; i < n\<rbrakk> \<Longrightarrow> thesis; x \<in> set (take n (a # xs)); n \<le> length (a # xs)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (cases "x = y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = y \<Longrightarrow> thesis
 2. x \<noteq> y \<Longrightarrow> thesis
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = y

goal (2 subgoals):
 1. x = y \<Longrightarrow> thesis
 2. x \<noteq> y \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (rule Cons.prems)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. find_first x (y # ys) = Some ?i
 2. ?i < n
[PROOF STEP]
show "find_first x (y # ys) = Some 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_first x (y # ys) = Some 0
[PROOF STEP]
unfolding \<open>x = y\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_first y (y # ys) = Some 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
find_first x (y # ys) = Some 0

goal (1 subgoal):
 1. 0 < n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < n
[PROOF STEP]
show "0 < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>i. \<lbrakk>find_first x ys = Some i; i < ?n\<rbrakk> \<Longrightarrow> ?thesis; x \<in> set (take ?n ys); ?n \<le> length ys\<rbrakk> \<Longrightarrow> ?thesis
\<lbrakk>find_first x (y # ys) = Some ?i; ?i < n\<rbrakk> \<Longrightarrow> thesis
x \<in> set (take n (y # ys))
n \<le> length (y # ys)

goal (1 subgoal):
 1. 0 < n
[PROOF STEP]
by (metis length_pos_if_in_set length_take min.absorb2)
[PROOF STATE]
proof (state)
this:
0 < n

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

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> thesis
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (rule Cons.IH)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i. \<lbrakk>find_first x ys = Some i; i < ?n\<rbrakk> \<Longrightarrow> thesis
 2. x \<in> set (take ?n ys)
 3. ?n \<le> length ys
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i. \<lbrakk>find_first x ys = Some i; i < ?n\<rbrakk> \<Longrightarrow> thesis
 2. x \<in> set (take ?n ys)
 3. ?n \<le> length ys
[PROOF STEP]
assume "find_first x ys = Some i" "i < n - 1"
[PROOF STATE]
proof (state)
this:
find_first x ys = Some i
i < n - 1

goal (3 subgoals):
 1. \<And>i. \<lbrakk>find_first x ys = Some i; i < ?n\<rbrakk> \<Longrightarrow> thesis
 2. x \<in> set (take ?n ys)
 3. ?n \<le> length ys
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> y
find_first x ys = Some i
i < n - 1
[PROOF STEP]
have "find_first x (y # ys) = Some (Suc i)" "Suc i < n"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
find_first x ys = Some i
i < n - 1

goal (1 subgoal):
 1. find_first x (y # ys) = Some (Suc i) &&& Suc i < n
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
find_first x ys = Some i
i < n - 1
x \<noteq> y

goal (1 subgoal):
 1. find_first x (y # ys) = Some (Suc i) &&& Suc i < n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
find_first x (y # ys) = Some (Suc i)
Suc i < n

goal (3 subgoals):
 1. \<And>i. \<lbrakk>find_first x ys = Some i; i < ?n\<rbrakk> \<Longrightarrow> thesis
 2. x \<in> set (take ?n ys)
 3. ?n \<le> length ys
[PROOF STEP]
thus thesis
[PROOF STATE]
proof (prove)
using this:
find_first x (y # ys) = Some (Suc i)
Suc i < n

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
find_first x (y # ys) = Some (Suc i)
Suc i < n
\<lbrakk>\<And>i. \<lbrakk>find_first x ys = Some i; i < ?n\<rbrakk> \<Longrightarrow> ?thesis; x \<in> set (take ?n ys); ?n \<le> length ys\<rbrakk> \<Longrightarrow> ?thesis
\<lbrakk>find_first x (y # ys) = Some ?i; ?i < n\<rbrakk> \<Longrightarrow> thesis
x \<in> set (take n (y # ys))
n \<le> length (y # ys)

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

goal (2 subgoals):
 1. x \<in> set (take (n - 1) ys)
 2. n - 1 \<le> length ys
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> set (take (n - 1) ys)
 2. n - 1 \<le> length ys
[PROOF STEP]
show "x \<in> set (take (n - 1) ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set (take (n - 1) ys)
[PROOF STEP]
using Cons False
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>i. \<lbrakk>find_first x ys = Some i; i < ?n\<rbrakk> \<Longrightarrow> ?thesis; x \<in> set (take ?n ys); ?n \<le> length ys\<rbrakk> \<Longrightarrow> ?thesis
\<lbrakk>find_first x (y # ys) = Some ?i; ?i < n\<rbrakk> \<Longrightarrow> thesis
x \<in> set (take n (y # ys))
n \<le> length (y # ys)
x \<noteq> y

goal (1 subgoal):
 1. x \<in> set (take (n - 1) ys)
[PROOF STEP]
by (metis empty_iff list.set(1) set_ConsD take_Cons')
[PROOF STATE]
proof (state)
this:
x \<in> set (take (n - 1) ys)

goal (1 subgoal):
 1. n - 1 \<le> length ys
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n - 1 \<le> length ys
[PROOF STEP]
show "n - 1 \<le> length ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n - 1 \<le> length ys
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>i. \<lbrakk>find_first x ys = Some i; i < ?n\<rbrakk> \<Longrightarrow> ?thesis; x \<in> set (take ?n ys); ?n \<le> length ys\<rbrakk> \<Longrightarrow> ?thesis
\<lbrakk>find_first x (y # ys) = Some ?i; ?i < n\<rbrakk> \<Longrightarrow> thesis
x \<in> set (take n (y # ys))
n \<le> length (y # ys)

goal (1 subgoal):
 1. n - 1 \<le> length ys
[PROOF STEP]
by (metis One_nat_def le_diff_conv list.size(4))
[PROOF STATE]
proof (state)
this:
n - 1 \<le> length ys

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

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

goal (1 subgoal):
 1. \<And>thesis n. \<lbrakk>\<And>i. \<lbrakk>find_first x [] = Some i; i < n\<rbrakk> \<Longrightarrow> thesis; x \<in> set (take n []); n \<le> length []\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
qed simp