[STATEMENT]
lemma exec_move_exec_1:
  assumes exec: "exec_move ci P t body h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  and sees: "P \<turnstile> C sees M : Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D"
  shows "exec_1 (compP2 P) t (xcp, h, (stk, loc, C, M, pc) # frs) ta (xcp', h', (stk', loc', C, M, pc') # frs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -ta-jvm\<rightarrow> (xcp', h', (stk', loc', C, M, pc') # frs)
[PROOF STEP]
using exec
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t body h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -ta-jvm\<rightarrow> (xcp', h', (stk', loc', C, M, pc') # frs)
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 body) (compxE2 body 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -ta-jvm\<rightarrow> (xcp', h', (stk', loc', C, M, pc') # frs)
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (compE2 body ! pc) (compP2 P) t h stk loc undefined undefined pc []; pc < length (compE2 body); ci_app ci (compE2 body ! pc) (compP2 P) h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -ta-jvm\<rightarrow> (xcp', h', (stk', loc', C, M, pc') # frs)
 2. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table (compP2 P) (cname_of h xcpa) pc (compxE2 body 0 0) = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -ta-jvm\<rightarrow> (xcp', h', (stk', loc', C, M, pc') # frs)
[PROOF STEP]
case exec_instr
[PROOF STATE]
proof (state)
this:
xcp = None
(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (compE2 body ! pc) (compP2 P) t h stk loc undefined undefined pc []
pc < length (compE2 body)
ci_app ci (compE2 body ! pc) (compP2 P) h stk loc undefined undefined pc []

goal (2 subgoals):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (compE2 body ! pc) (compP2 P) t h stk loc undefined undefined pc []; pc < length (compE2 body); ci_app ci (compE2 body ! pc) (compP2 P) h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -ta-jvm\<rightarrow> (xcp', h', (stk', loc', C, M, pc') # frs)
 2. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table (compP2 P) (cname_of h xcpa) pc (compxE2 body 0 0) = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -ta-jvm\<rightarrow> (xcp', h', (stk', loc', C, M, pc') # frs)
[PROOF STEP]
note [simp] = \<open>xcp = None\<close>
    and exec = \<open>(ta, xcp', h', [(stk', loc', undefined, undefined, pc')])
                \<in> exec_instr (compE2 body ! pc) (compP2 P) t h stk loc undefined undefined pc []\<close>
[PROOF STATE]
proof (state)
this:
xcp = None
(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (compE2 body ! pc) (compP2 P) t h stk loc undefined undefined pc []

goal (2 subgoals):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (compE2 body ! pc) (compP2 P) t h stk loc undefined undefined pc []; pc < length (compE2 body); ci_app ci (compE2 body ! pc) (compP2 P) h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -ta-jvm\<rightarrow> (xcp', h', (stk', loc', C, M, pc') # frs)
 2. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table (compP2 P) (cname_of h xcpa) pc (compxE2 body 0 0) = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -ta-jvm\<rightarrow> (xcp', h', (stk', loc', C, M, pc') # frs)
[PROOF STEP]
from exec
[PROOF STATE]
proof (chain)
picking this:
(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (compE2 body ! pc) (compP2 P) t h stk loc undefined undefined pc []
[PROOF STEP]
have "(ta, xcp', h', [(stk', loc', C, M, pc')])
                \<in> exec_instr (compE2 body ! pc) (compP2 P) t h stk loc C M pc []"
[PROOF STATE]
proof (prove)
using this:
(ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (compE2 body ! pc) (compP2 P) t h stk loc undefined undefined pc []

goal (1 subgoal):
 1. (ta, xcp', h', [(stk', loc', C, M, pc')]) \<in> exec_instr (compE2 body ! pc) (compP2 P) t h stk loc C M pc []
[PROOF STEP]
by(rule exec_instr_CM_change)
[PROOF STATE]
proof (state)
this:
(ta, xcp', h', [(stk', loc', C, M, pc')]) \<in> exec_instr (compE2 body ! pc) (compP2 P) t h stk loc C M pc []

goal (2 subgoals):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (compE2 body ! pc) (compP2 P) t h stk loc undefined undefined pc []; pc < length (compE2 body); ci_app ci (compE2 body ! pc) (compP2 P) h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -ta-jvm\<rightarrow> (xcp', h', (stk', loc', C, M, pc') # frs)
 2. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table (compP2 P) (cname_of h xcpa) pc (compxE2 body 0 0) = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -ta-jvm\<rightarrow> (xcp', h', (stk', loc', C, M, pc') # frs)
[PROOF STEP]
from exec_instr_frs_offer[OF this, of frs]
[PROOF STATE]
proof (chain)
picking this:
(ta, xcp', h', (stk', loc', C, M, pc') # [] @ frs) \<in> exec_instr (compE2 body ! pc) (compP2 P) t h stk loc C M pc ([] @ frs)
[PROOF STEP]
have "(ta, xcp', h', (stk', loc', C, M, pc') # frs)
        \<in> exec_instr (compE2 body ! pc) (compP2 P) t h stk loc C M pc frs"
[PROOF STATE]
proof (prove)
using this:
(ta, xcp', h', (stk', loc', C, M, pc') # [] @ frs) \<in> exec_instr (compE2 body ! pc) (compP2 P) t h stk loc C M pc ([] @ frs)

goal (1 subgoal):
 1. (ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (compE2 body ! pc) (compP2 P) t h stk loc C M pc frs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (compE2 body ! pc) (compP2 P) t h stk loc C M pc frs

goal (2 subgoals):
 1. \<lbrakk>xcp = None; (ta, xcp', h', [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (compE2 body ! pc) (compP2 P) t h stk loc undefined undefined pc []; pc < length (compE2 body); ci_app ci (compE2 body ! pc) (compP2 P) h stk loc undefined undefined pc []\<rbrakk> \<Longrightarrow> compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -ta-jvm\<rightarrow> (xcp', h', (stk', loc', C, M, pc') # frs)
 2. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table (compP2 P) (cname_of h xcpa) pc (compxE2 body 0 0) = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -ta-jvm\<rightarrow> (xcp', h', (stk', loc', C, M, pc') # frs)
[PROOF STEP]
with sees \<open>pc < length (compE2 body)\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D
pc < length (compE2 body)
(ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (compE2 body ! pc) (compP2 P) t h stk loc C M pc frs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D
pc < length (compE2 body)
(ta, xcp', h', (stk', loc', C, M, pc') # frs) \<in> exec_instr (compE2 body ! pc) (compP2 P) t h stk loc C M pc frs

goal (1 subgoal):
 1. compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -ta-jvm\<rightarrow> (xcp', h', (stk', loc', C, M, pc') # frs)
[PROOF STEP]
by(simp add: exec_1_iff compP2_def compMb2_def nth_append)
[PROOF STATE]
proof (state)
this:
compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -ta-jvm\<rightarrow> (xcp', h', (stk', loc', C, M, pc') # frs)

goal (1 subgoal):
 1. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table (compP2 P) (cname_of h xcpa) pc (compxE2 body 0 0) = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -ta-jvm\<rightarrow> (xcp', h', (stk', loc', C, M, pc') # frs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table (compP2 P) (cname_of h xcpa) pc (compxE2 body 0 0) = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -ta-jvm\<rightarrow> (xcp', h', (stk', loc', C, M, pc') # frs)
[PROOF STEP]
case exec_catch
[PROOF STATE]
proof (state)
this:
xcp = \<lfloor>xcp_\<rfloor>
ta = \<lbrace>\<rbrace>
h' = h
stk' = Addr xcp_ # drop (length stk - d_) stk
loc' = loc
xcp' = None
match_ex_table (compP2 P) (cname_of h xcp_) pc (compxE2 body 0 0) = \<lfloor>(pc', d_)\<rfloor>
d_ \<le> length stk

goal (1 subgoal):
 1. \<And>xcpa d. \<lbrakk>xcp = \<lfloor>xcpa\<rfloor>; ta = \<lbrace>\<rbrace>; h' = h; stk' = Addr xcpa # drop (length stk - d) stk; loc' = loc; xcp' = None; match_ex_table (compP2 P) (cname_of h xcpa) pc (compxE2 body 0 0) = \<lfloor>(pc', d)\<rfloor>; d \<le> length stk\<rbrakk> \<Longrightarrow> compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -ta-jvm\<rightarrow> (xcp', h', (stk', loc', C, M, pc') # frs)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
xcp = \<lfloor>xcp_\<rfloor>
ta = \<lbrace>\<rbrace>
h' = h
stk' = Addr xcp_ # drop (length stk - d_) stk
loc' = loc
xcp' = None
match_ex_table (compP2 P) (cname_of h xcp_) pc (compxE2 body 0 0) = \<lfloor>(pc', d_)\<rfloor>
d_ \<le> length stk

goal (1 subgoal):
 1. compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -ta-jvm\<rightarrow> (xcp', h', (stk', loc', C, M, pc') # frs)
[PROOF STEP]
using sees_method_compP[OF sees, of "\<lambda>C M Ts T. compMb2"]
[PROOF STATE]
proof (prove)
using this:
xcp = \<lfloor>xcp_\<rfloor>
ta = \<lbrace>\<rbrace>
h' = h
stk' = Addr xcp_ # drop (length stk - d_) stk
loc' = loc
xcp' = None
match_ex_table (compP2 P) (cname_of h xcp_) pc (compxE2 body 0 0) = \<lfloor>(pc', d_)\<rfloor>
d_ \<le> length stk
compP (\<lambda>C M Ts T. compMb2) P \<turnstile> C sees M: Ts\<rightarrow>T = map_option compMb2 \<lfloor>body\<rfloor> in D

goal (1 subgoal):
 1. compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -ta-jvm\<rightarrow> (xcp', h', (stk', loc', C, M, pc') # frs)
[PROOF STEP]
by(simp add: exec_1_iff compMb2_def compP2_def)
[PROOF STATE]
proof (state)
this:
compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -ta-jvm\<rightarrow> (xcp', h', (stk', loc', C, M, pc') # frs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<tau>exec_move_\<tau>exec_1:
  assumes exec: "\<tau>exec_move ci P t body h (stk, loc, pc, xcp) (stk', loc', pc', xcp')"
  and sees: "P \<turnstile> C sees M : Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D"
  shows "\<tau>exec_1 (compP2 P) t (xcp, h, (stk, loc, C, M, pc) # frs) (xcp', h, (stk', loc', C, M, pc') # frs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_1 (compP2 P) t (xcp, h, (stk, loc, C, M, pc) # frs) (xcp', h, (stk', loc', C, M, pc') # frs)
[PROOF STEP]
proof(rule \<tau>exec_1I)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -\<lbrace>\<rbrace>-jvm\<rightarrow> (xcp', h, (stk', loc', C, M, pc') # frs)
 2. \<tau>Move2 (compP2 P) (xcp, h, (stk, loc, C, M, pc) # frs)
[PROOF STEP]
from exec
[PROOF STATE]
proof (chain)
picking this:
\<tau>exec_move ci P t body h (stk, loc, pc, xcp) (stk', loc', pc', xcp')
[PROOF STEP]
obtain exec': "exec_move ci P t body h (stk, loc, pc, xcp) \<epsilon> h (stk', loc', pc', xcp')"
    and \<tau>: "\<tau>move2 P h stk body pc xcp"
[PROOF STATE]
proof (prove)
using this:
\<tau>exec_move ci P t body h (stk, loc, pc, xcp) (stk', loc', pc', xcp')

goal (1 subgoal):
 1. (\<lbrakk>exec_move ci P t body h (stk, loc, pc, xcp) \<lbrace>\<rbrace> h (stk', loc', pc', xcp'); \<tau>move2 P h stk body pc xcp\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule \<tau>exec_moveE)
[PROOF STATE]
proof (state)
this:
exec_move ci P t body h (stk, loc, pc, xcp) \<lbrace>\<rbrace> h (stk', loc', pc', xcp')
\<tau>move2 P h stk body pc xcp

goal (2 subgoals):
 1. compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -\<lbrace>\<rbrace>-jvm\<rightarrow> (xcp', h, (stk', loc', C, M, pc') # frs)
 2. \<tau>Move2 (compP2 P) (xcp, h, (stk, loc, C, M, pc) # frs)
[PROOF STEP]
have "exec_1 (compP2 P) t (xcp, h, (stk, loc, C, M, pc) # frs) \<epsilon> (xcp', h, (stk', loc', C, M, pc') # frs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -\<lbrace>\<rbrace>-jvm\<rightarrow> (xcp', h, (stk', loc', C, M, pc') # frs)
[PROOF STEP]
using exec' sees
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t body h (stk, loc, pc, xcp) \<lbrace>\<rbrace> h (stk', loc', pc', xcp')
P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D

goal (1 subgoal):
 1. compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -\<lbrace>\<rbrace>-jvm\<rightarrow> (xcp', h, (stk', loc', C, M, pc') # frs)
[PROOF STEP]
by(rule exec_move_exec_1)
[PROOF STATE]
proof (state)
this:
compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -\<lbrace>\<rbrace>-jvm\<rightarrow> (xcp', h, (stk', loc', C, M, pc') # frs)

goal (2 subgoals):
 1. compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -\<lbrace>\<rbrace>-jvm\<rightarrow> (xcp', h, (stk', loc', C, M, pc') # frs)
 2. \<tau>Move2 (compP2 P) (xcp, h, (stk, loc, C, M, pc) # frs)
[PROOF STEP]
thus "compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -\<epsilon>-jvm\<rightarrow> (xcp', h, (stk', loc', C, M, pc') # frs)"
[PROOF STATE]
proof (prove)
using this:
compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -\<lbrace>\<rbrace>-jvm\<rightarrow> (xcp', h, (stk', loc', C, M, pc') # frs)

goal (1 subgoal):
 1. compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -\<lbrace>\<rbrace>-jvm\<rightarrow> (xcp', h, (stk', loc', C, M, pc') # frs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -\<lbrace>\<rbrace>-jvm\<rightarrow> (xcp', h, (stk', loc', C, M, pc') # frs)

goal (1 subgoal):
 1. \<tau>Move2 (compP2 P) (xcp, h, (stk, loc, C, M, pc) # frs)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
compP2 P,t \<turnstile> (xcp, h, (stk, loc, C, M, pc) # frs) -\<lbrace>\<rbrace>-jvm\<rightarrow> (xcp', h, (stk', loc', C, M, pc') # frs)

goal (1 subgoal):
 1. \<tau>Move2 (compP2 P) (xcp, h, (stk, loc, C, M, pc) # frs)
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<tau>Move2 (compP2 P) (xcp, h, (stk, loc, C, M, pc) # frs)
[PROOF STEP]
assume [simp]: "xcp = \<lfloor>a\<rfloor>"
[PROOF STATE]
proof (state)
this:
xcp = \<lfloor>a\<rfloor>

goal (1 subgoal):
 1. \<tau>Move2 (compP2 P) (xcp, h, (stk, loc, C, M, pc) # frs)
[PROOF STEP]
from sees_method_compP[OF sees, of "\<lambda>C M Ts T. compMb2"]
[PROOF STATE]
proof (chain)
picking this:
compP (\<lambda>C M Ts T. compMb2) P \<turnstile> C sees M: Ts\<rightarrow>T = map_option compMb2 \<lfloor>body\<rfloor> in D
[PROOF STEP]
have "ex_table_of (compP2 P) C M = compxE2 body 0 0"
[PROOF STATE]
proof (prove)
using this:
compP (\<lambda>C M Ts T. compMb2) P \<turnstile> C sees M: Ts\<rightarrow>T = map_option compMb2 \<lfloor>body\<rfloor> in D

goal (1 subgoal):
 1. ex_table_of (compP2 P) C M = compxE2 body 0 0
[PROOF STEP]
by(simp add: compP2_def compMb2_def)
[PROOF STATE]
proof (state)
this:
ex_table_of (compP2 P) C M = compxE2 body 0 0

goal (1 subgoal):
 1. \<tau>Move2 (compP2 P) (xcp, h, (stk, loc, C, M, pc) # frs)
[PROOF STEP]
hence "match_ex_table (compP2 P) (cname_of h a) pc (ex_table_of (compP2 P) C M) \<noteq> None" "pc < length (compE2 body)"
[PROOF STATE]
proof (prove)
using this:
ex_table_of (compP2 P) C M = compxE2 body 0 0

goal (1 subgoal):
 1. match_ex_table (compP2 P) (cname_of h a) pc (ex_table_of (compP2 P) C M) \<noteq> None &&& pc < length (compE2 body)
[PROOF STEP]
using exec' sees
[PROOF STATE]
proof (prove)
using this:
ex_table_of (compP2 P) C M = compxE2 body 0 0
exec_move ci P t body h (stk, loc, pc, xcp) \<lbrace>\<rbrace> h (stk', loc', pc', xcp')
P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D

goal (1 subgoal):
 1. match_ex_table (compP2 P) (cname_of h a) pc (ex_table_of (compP2 P) C M) \<noteq> None &&& pc < length (compE2 body)
[PROOF STEP]
by(auto simp add: exec_move_def elim: exec_meth.cases)
[PROOF STATE]
proof (state)
this:
match_ex_table (compP2 P) (cname_of h a) pc (ex_table_of (compP2 P) C M) \<noteq> None
pc < length (compE2 body)

goal (1 subgoal):
 1. \<tau>Move2 (compP2 P) (xcp, h, (stk, loc, C, M, pc) # frs)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
xcp = \<lfloor>?a22\<rfloor> \<Longrightarrow> match_ex_table (compP2 P) (cname_of h ?a22) pc (ex_table_of (compP2 P) C M) \<noteq> None
xcp = \<lfloor>?a22\<rfloor> \<Longrightarrow> pc < length (compE2 body)

goal (1 subgoal):
 1. \<tau>Move2 (compP2 P) (xcp, h, (stk, loc, C, M, pc) # frs)
[PROOF STEP]
with \<tau> sees sees_method_compP[OF sees, of "\<lambda>C M Ts T. compMb2"]
[PROOF STATE]
proof (chain)
picking this:
\<tau>move2 P h stk body pc xcp
P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D
compP (\<lambda>C M Ts T. compMb2) P \<turnstile> C sees M: Ts\<rightarrow>T = map_option compMb2 \<lfloor>body\<rfloor> in D
xcp = \<lfloor>?a22\<rfloor> \<Longrightarrow> match_ex_table (compP2 P) (cname_of h ?a22) pc (ex_table_of (compP2 P) C M) \<noteq> None
xcp = \<lfloor>?a22\<rfloor> \<Longrightarrow> pc < length (compE2 body)
[PROOF STEP]
show "\<tau>Move2 (compP2 P) (xcp, h, (stk, loc, C, M, pc) # frs)"
[PROOF STATE]
proof (prove)
using this:
\<tau>move2 P h stk body pc xcp
P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D
compP (\<lambda>C M Ts T. compMb2) P \<turnstile> C sees M: Ts\<rightarrow>T = map_option compMb2 \<lfloor>body\<rfloor> in D
xcp = \<lfloor>?a22\<rfloor> \<Longrightarrow> match_ex_table (compP2 P) (cname_of h ?a22) pc (ex_table_of (compP2 P) C M) \<noteq> None
xcp = \<lfloor>?a22\<rfloor> \<Longrightarrow> pc < length (compE2 body)

goal (1 subgoal):
 1. \<tau>Move2 (compP2 P) (xcp, h, (stk, loc, C, M, pc) # frs)
[PROOF STEP]
unfolding \<tau>Move2_compP2[OF sees]
[PROOF STATE]
proof (prove)
using this:
\<tau>move2 P h stk body pc xcp
P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D
compP (\<lambda>C M Ts T. compMb2) P \<turnstile> C sees M: Ts\<rightarrow>T = map_option compMb2 \<lfloor>body\<rfloor> in D
xcp = \<lfloor>?a22\<rfloor> \<Longrightarrow> match_ex_table (compP2 P) (cname_of h ?a22) pc (ex_table_of (compP2 P) C M) \<noteq> None
xcp = \<lfloor>?a22\<rfloor> \<Longrightarrow> pc < length (compE2 body)

goal (1 subgoal):
 1. case xcp of None \<Rightarrow> \<tau>move2 P h stk body pc xcp \<or> pc = length (compE2 body) | \<lfloor>a\<rfloor> \<Rightarrow> pc < Suc (length (compE2 body))
[PROOF STEP]
by(fastforce simp add: compP2_def compMb2_def)
[PROOF STATE]
proof (state)
this:
\<tau>Move2 (compP2 P) (xcp, h, (stk, loc, C, M, pc) # frs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<tau>Exec_mover_\<tau>Exec_1r:
  assumes move: "\<tau>Exec_mover ci P t body h (stk, loc, pc, xcp) (stk', loc', pc', xcp')"
  and sees: "P \<turnstile> C sees M : Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D"
  shows "\<tau>Exec_1r (compP2 P) t (xcp, h, (stk, loc, C, M, pc) # frs') (xcp', h, (stk', loc', C, M, pc') # frs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_1r (compP2 P) t (xcp, h, (stk, loc, C, M, pc) # frs') (xcp', h, (stk', loc', C, M, pc') # frs')
[PROOF STEP]
using move
[PROOF STATE]
proof (prove)
using this:
\<tau>Exec_mover ci P t body h (stk, loc, pc, xcp) (stk', loc', pc', xcp')

goal (1 subgoal):
 1. \<tau>Exec_1r (compP2 P) t (xcp, h, (stk, loc, C, M, pc) # frs') (xcp', h, (stk', loc', C, M, pc') # frs')
[PROOF STEP]
by(induct rule: \<tau>Execr_induct)(blast intro: rtranclp.rtrancl_into_rtrancl \<tau>exec_move_\<tau>exec_1[OF _ sees])+


[STATEMENT]
lemma \<tau>Exec_movet_\<tau>Exec_1t:
  assumes move: "\<tau>Exec_movet ci P t body h (stk, loc, pc, xcp) (stk', loc', pc', xcp')"
  and sees: "P \<turnstile> C sees M : Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D"
  shows "\<tau>Exec_1t (compP2 P) t (xcp, h, (stk, loc, C, M, pc) # frs') (xcp', h, (stk', loc', C, M, pc') # frs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_1t (compP2 P) t (xcp, h, (stk, loc, C, M, pc) # frs') (xcp', h, (stk', loc', C, M, pc') # frs')
[PROOF STEP]
using move
[PROOF STATE]
proof (prove)
using this:
\<tau>Exec_movet ci P t body h (stk, loc, pc, xcp) (stk', loc', pc', xcp')

goal (1 subgoal):
 1. \<tau>Exec_1t (compP2 P) t (xcp, h, (stk, loc, C, M, pc) # frs') (xcp', h, (stk', loc', C, M, pc') # frs')
[PROOF STEP]
by(induct rule: \<tau>Exect_induct)(blast intro: tranclp.trancl_into_trancl \<tau>exec_move_\<tau>exec_1[OF _ sees])+


[STATEMENT]
lemma \<tau>Exec_1t_rtranclpD:
  "\<tau>Exec_1t P t (xcp, h, frs) (xcp', h', frs')
  \<Longrightarrow> (\<lambda>((xcp, frs), h) ((xcp', frs'), h'). exec_1 P t (xcp, h, frs) \<epsilon> (xcp', h', frs') \<and> \<tau>Move2 P (xcp, h, frs))^++ ((xcp, frs), h) ((xcp', frs'), h')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_1t P t (xcp, h, frs) (xcp', h', frs') \<Longrightarrow> (\<lambda>((xcp, frs), h) ((xcp', frs'), h'). P,t \<turnstile> (xcp, h, frs) -\<lbrace>\<rbrace>-jvm\<rightarrow> (xcp', h', frs') \<and> \<tau>Move2 P (xcp, h, frs))\<^sup>+\<^sup>+ ((xcp, frs), h) ((xcp', frs'), h')
[PROOF STEP]
by(induct rule: tranclp_induct3)(fastforce intro: tranclp.trancl_into_trancl)+


[STATEMENT]
lemma exec_meth_length_compE2_stack_xliftD:
  "exec_meth ci P (compE2 e) (stack_xlift d (compxE2 e 0 0)) t h (stk, loc, pc, xcp) ta h' s'
  \<Longrightarrow> pc < length (compE2 e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci P (compE2 e) (stack_xlift d (compxE2 e 0 0)) t h (stk, loc, pc, xcp) ta h' s' \<Longrightarrow> pc < length (compE2 e)
[PROOF STEP]
by(cases s')(auto simp add: stack_xlift_compxE2)


[STATEMENT]
lemma exec_meth_length_pc_xt_Nil:
  "exec_meth ci P ins [] t h (stk, loc, pc, xcp) ta h' s' \<Longrightarrow> pc < length ins"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci P ins [] t h (stk, loc, pc, xcp) ta h' s' \<Longrightarrow> pc < length ins
[PROOF STEP]
apply(erule exec_meth.cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>taa xcpa h'a stk' loc' pc' pca ha stka loca. \<lbrakk>h = ha; (stk, loc, pc, xcp) = (stka, loca, pca, None); ta = taa; h' = h'a; s' = (stk', loc', pc', xcpa); (taa, xcpa, h'a, [(stk', loc', undefined, undefined, pc')]) \<in> exec_instr (ins ! pca) P t ha stka loca undefined undefined pca []; pca < length ins; ci_app ci (ins ! pca) P ha stka loca undefined undefined pca []\<rbrakk> \<Longrightarrow> pc < length ins
 2. \<And>ha xcpa pca pc' d stka loca. \<lbrakk>h = ha; (stk, loc, pc, xcp) = (stka, loca, pca, \<lfloor>xcpa\<rfloor>); ta = \<lbrace>\<rbrace>; h' = ha; s' = (Addr xcpa # drop (length stka - d) stka, loca, pc', None); match_ex_table P (cname_of ha xcpa) pca [] = \<lfloor>(pc', d)\<rfloor>; d \<le> length stka\<rbrakk> \<Longrightarrow> pc < length ins
[PROOF STEP]
apply(auto dest: match_ex_table_pc_length_compE2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma BinOp_exec2D:
  assumes exec: "exec_meth ci (compP2 P) (compE2 (e1 \<guillemotleft>bop\<guillemotright> e2)) (compxE2 (e1 \<guillemotleft>bop\<guillemotright> e2) 0 0) t h (stk @ [v1], loc, length (compE2 e1) + pc, xcp) ta h' (stk', loc', pc', xcp')"
  and pc: "pc < length (compE2 e2)"
  shows "exec_meth ci (compP2 P) (compE2 e2) (stack_xlift (length [v1]) (compxE2 e2 0 0)) t h (stk @ [v1], loc, pc, xcp) ta h' (stk', loc', pc' - length (compE2 e1), xcp') \<and> pc' \<ge> length (compE2 e1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e2) (stack_xlift (length [v1]) (compxE2 e2 0 0)) t h (stk @ [v1], loc, pc, xcp) ta h' (stk', loc', pc' - length (compE2 e1), xcp') \<and> length (compE2 e1) \<le> pc'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. exec_meth ci (compP2 P) (compE2 e2) (stack_xlift (length [v1]) (compxE2 e2 0 0)) t h (stk @ [v1], loc, pc, xcp) ta h' (stk', loc', pc' - length (compE2 e1), xcp')
 2. length (compE2 e1) \<le> pc'
[PROOF STEP]
from exec
[PROOF STATE]
proof (chain)
picking this:
exec_meth ci (compP2 P) (compE2 (e1 \<guillemotleft>bop\<guillemotright> e2)) (compxE2 (e1 \<guillemotleft>bop\<guillemotright> e2) 0 0) t h (stk @ [v1], loc, length (compE2 e1) + pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
have "exec_meth ci (compP2 P) ((compE2 e1 @ compE2 e2) @ [BinOpInstr bop])
     (compxE2 e1 0 0 @ shift (length (compE2 e1)) (stack_xlift (length [v1]) (compxE2 e2 0 0))) t h
     (stk @ [v1], loc, length (compE2 e1) + pc, xcp) ta h' (stk', loc', pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 (e1 \<guillemotleft>bop\<guillemotright> e2)) (compxE2 (e1 \<guillemotleft>bop\<guillemotright> e2) 0 0) t h (stk @ [v1], loc, length (compE2 e1) + pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) ((compE2 e1 @ compE2 e2) @ [BinOpInstr bop]) (compxE2 e1 0 0 @ shift (length (compE2 e1)) (stack_xlift (length [v1]) (compxE2 e2 0 0))) t h (stk @ [v1], loc, length (compE2 e1) + pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
by(simp add: compxE2_size_convs compxE2_stack_xlift_convs)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) ((compE2 e1 @ compE2 e2) @ [BinOpInstr bop]) (compxE2 e1 0 0 @ shift (length (compE2 e1)) (stack_xlift (length [v1]) (compxE2 e2 0 0))) t h (stk @ [v1], loc, length (compE2 e1) + pc, xcp) ta h' (stk', loc', pc', xcp')

goal (2 subgoals):
 1. exec_meth ci (compP2 P) (compE2 e2) (stack_xlift (length [v1]) (compxE2 e2 0 0)) t h (stk @ [v1], loc, pc, xcp) ta h' (stk', loc', pc' - length (compE2 e1), xcp')
 2. length (compE2 e1) \<le> pc'
[PROOF STEP]
hence exec': "exec_meth ci (compP2 P) (compE2 e1 @ compE2 e2) (compxE2 e1 0 0 @ shift (length (compE2 e1)) (stack_xlift (length [v1]) (compxE2 e2 0 0))) t h
     (stk @ [v1], loc, length (compE2 e1) + pc, xcp) ta h' (stk', loc', pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) ((compE2 e1 @ compE2 e2) @ [BinOpInstr bop]) (compxE2 e1 0 0 @ shift (length (compE2 e1)) (stack_xlift (length [v1]) (compxE2 e2 0 0))) t h (stk @ [v1], loc, length (compE2 e1) + pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e1 @ compE2 e2) (compxE2 e1 0 0 @ shift (length (compE2 e1)) (stack_xlift (length [v1]) (compxE2 e2 0 0))) t h (stk @ [v1], loc, length (compE2 e1) + pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
by(rule exec_meth_take) (simp add: pc)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e1 @ compE2 e2) (compxE2 e1 0 0 @ shift (length (compE2 e1)) (stack_xlift (length [v1]) (compxE2 e2 0 0))) t h (stk @ [v1], loc, length (compE2 e1) + pc, xcp) ta h' (stk', loc', pc', xcp')

goal (2 subgoals):
 1. exec_meth ci (compP2 P) (compE2 e2) (stack_xlift (length [v1]) (compxE2 e2 0 0)) t h (stk @ [v1], loc, pc, xcp) ta h' (stk', loc', pc' - length (compE2 e1), xcp')
 2. length (compE2 e1) \<le> pc'
[PROOF STEP]
thus "exec_meth ci (compP2 P) (compE2 e2) (stack_xlift (length [v1]) (compxE2 e2 0 0)) t h
     (stk @ [v1], loc, pc, xcp) ta h' (stk', loc', pc' - length (compE2 e1), xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e1 @ compE2 e2) (compxE2 e1 0 0 @ shift (length (compE2 e1)) (stack_xlift (length [v1]) (compxE2 e2 0 0))) t h (stk @ [v1], loc, length (compE2 e1) + pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e2) (stack_xlift (length [v1]) (compxE2 e2 0 0)) t h (stk @ [v1], loc, pc, xcp) ta h' (stk', loc', pc' - length (compE2 e1), xcp')
[PROOF STEP]
by(rule exec_meth_drop_xt) auto
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e2) (stack_xlift (length [v1]) (compxE2 e2 0 0)) t h (stk @ [v1], loc, pc, xcp) ta h' (stk', loc', pc' - length (compE2 e1), xcp')

goal (1 subgoal):
 1. length (compE2 e1) \<le> pc'
[PROOF STEP]
from exec'
[PROOF STATE]
proof (chain)
picking this:
exec_meth ci (compP2 P) (compE2 e1 @ compE2 e2) (compxE2 e1 0 0 @ shift (length (compE2 e1)) (stack_xlift (length [v1]) (compxE2 e2 0 0))) t h (stk @ [v1], loc, length (compE2 e1) + pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
show "pc' \<ge> length (compE2 e1)"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e1 @ compE2 e2) (compxE2 e1 0 0 @ shift (length (compE2 e1)) (stack_xlift (length [v1]) (compxE2 e2 0 0))) t h (stk @ [v1], loc, length (compE2 e1) + pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. length (compE2 e1) \<le> pc'
[PROOF STEP]
by(rule exec_meth_drop_xt_pc)(auto)
[PROOF STATE]
proof (state)
this:
length (compE2 e1) \<le> pc'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Call_execParamD:
  assumes exec: "exec_meth ci (compP2 P) (compE2 (obj\<bullet>M'(ps))) (compxE2 (obj\<bullet>M'(ps)) 0 0) t h (stk @ [v], loc, length (compE2 obj) + pc, xcp) ta h' (stk', loc', pc', xcp')"
  and pc: "pc < length (compEs2 ps)"
  shows "exec_meth ci (compP2 P) (compEs2 ps) (stack_xlift (length [v]) (compxEs2 ps 0 0)) t h (stk @ [v], loc, pc, xcp) ta h' (stk', loc', pc' - length (compE2 obj), xcp') \<and> pc' \<ge> length (compE2 obj)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compEs2 ps) (stack_xlift (length [v]) (compxEs2 ps 0 0)) t h (stk @ [v], loc, pc, xcp) ta h' (stk', loc', pc' - length (compE2 obj), xcp') \<and> length (compE2 obj) \<le> pc'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. exec_meth ci (compP2 P) (compEs2 ps) (stack_xlift (length [v]) (compxEs2 ps 0 0)) t h (stk @ [v], loc, pc, xcp) ta h' (stk', loc', pc' - length (compE2 obj), xcp')
 2. length (compE2 obj) \<le> pc'
[PROOF STEP]
from exec
[PROOF STATE]
proof (chain)
picking this:
exec_meth ci (compP2 P) (compE2 (obj\<bullet>M'(ps))) (compxE2 (obj\<bullet>M'(ps)) 0 0) t h (stk @ [v], loc, length (compE2 obj) + pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
have "exec_meth ci (compP2 P) ((compE2 obj @ compEs2 ps) @ [Invoke M' (length ps)])
     (compxE2 obj 0 0 @ shift (length (compE2 obj)) (stack_xlift (length [v]) (compxEs2 ps 0 0))) t h
     (stk @ [v], loc, length (compE2 obj) + pc, xcp) ta h' (stk', loc', pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 (obj\<bullet>M'(ps))) (compxE2 (obj\<bullet>M'(ps)) 0 0) t h (stk @ [v], loc, length (compE2 obj) + pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) ((compE2 obj @ compEs2 ps) @ [Invoke M' (length ps)]) (compxE2 obj 0 0 @ shift (length (compE2 obj)) (stack_xlift (length [v]) (compxEs2 ps 0 0))) t h (stk @ [v], loc, length (compE2 obj) + pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
by(simp add: compxEs2_size_convs compxEs2_stack_xlift_convs)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) ((compE2 obj @ compEs2 ps) @ [Invoke M' (length ps)]) (compxE2 obj 0 0 @ shift (length (compE2 obj)) (stack_xlift (length [v]) (compxEs2 ps 0 0))) t h (stk @ [v], loc, length (compE2 obj) + pc, xcp) ta h' (stk', loc', pc', xcp')

goal (2 subgoals):
 1. exec_meth ci (compP2 P) (compEs2 ps) (stack_xlift (length [v]) (compxEs2 ps 0 0)) t h (stk @ [v], loc, pc, xcp) ta h' (stk', loc', pc' - length (compE2 obj), xcp')
 2. length (compE2 obj) \<le> pc'
[PROOF STEP]
hence exec': "exec_meth ci (compP2 P) (compE2 obj @ compEs2 ps) (compxE2 obj 0 0 @ shift (length (compE2 obj)) (stack_xlift (length [v]) (compxEs2 ps 0 0))) t h
     (stk @ [v], loc, length (compE2 obj) + pc, xcp) ta h' (stk', loc', pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) ((compE2 obj @ compEs2 ps) @ [Invoke M' (length ps)]) (compxE2 obj 0 0 @ shift (length (compE2 obj)) (stack_xlift (length [v]) (compxEs2 ps 0 0))) t h (stk @ [v], loc, length (compE2 obj) + pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 obj @ compEs2 ps) (compxE2 obj 0 0 @ shift (length (compE2 obj)) (stack_xlift (length [v]) (compxEs2 ps 0 0))) t h (stk @ [v], loc, length (compE2 obj) + pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
by(rule exec_meth_take)(simp add: pc)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 obj @ compEs2 ps) (compxE2 obj 0 0 @ shift (length (compE2 obj)) (stack_xlift (length [v]) (compxEs2 ps 0 0))) t h (stk @ [v], loc, length (compE2 obj) + pc, xcp) ta h' (stk', loc', pc', xcp')

goal (2 subgoals):
 1. exec_meth ci (compP2 P) (compEs2 ps) (stack_xlift (length [v]) (compxEs2 ps 0 0)) t h (stk @ [v], loc, pc, xcp) ta h' (stk', loc', pc' - length (compE2 obj), xcp')
 2. length (compE2 obj) \<le> pc'
[PROOF STEP]
thus "exec_meth ci (compP2 P) (compEs2 ps) (stack_xlift (length [v]) (compxEs2 ps 0 0)) t h (stk @ [v], loc, pc, xcp) ta h' (stk', loc', pc' - length (compE2 obj), xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 obj @ compEs2 ps) (compxE2 obj 0 0 @ shift (length (compE2 obj)) (stack_xlift (length [v]) (compxEs2 ps 0 0))) t h (stk @ [v], loc, length (compE2 obj) + pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compEs2 ps) (stack_xlift (length [v]) (compxEs2 ps 0 0)) t h (stk @ [v], loc, pc, xcp) ta h' (stk', loc', pc' - length (compE2 obj), xcp')
[PROOF STEP]
by(rule exec_meth_drop_xt) auto
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compEs2 ps) (stack_xlift (length [v]) (compxEs2 ps 0 0)) t h (stk @ [v], loc, pc, xcp) ta h' (stk', loc', pc' - length (compE2 obj), xcp')

goal (1 subgoal):
 1. length (compE2 obj) \<le> pc'
[PROOF STEP]
from exec'
[PROOF STATE]
proof (chain)
picking this:
exec_meth ci (compP2 P) (compE2 obj @ compEs2 ps) (compxE2 obj 0 0 @ shift (length (compE2 obj)) (stack_xlift (length [v]) (compxEs2 ps 0 0))) t h (stk @ [v], loc, length (compE2 obj) + pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
show "pc' \<ge> length (compE2 obj)"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 obj @ compEs2 ps) (compxE2 obj 0 0 @ shift (length (compE2 obj)) (stack_xlift (length [v]) (compxEs2 ps 0 0))) t h (stk @ [v], loc, length (compE2 obj) + pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. length (compE2 obj) \<le> pc'
[PROOF STEP]
by(rule exec_meth_drop_xt_pc)(auto)
[PROOF STATE]
proof (state)
this:
length (compE2 obj) \<le> pc'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exec_move_length_compE2D [dest]:
  "exec_move ci P t e h (stk, loc, pc, xcp) ta h' s' \<Longrightarrow> pc < length (compE2 e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t e h (stk, loc, pc, xcp) ta h' s' \<Longrightarrow> pc < length (compE2 e)
[PROOF STEP]
by(cases s')(auto simp add: exec_move_def)


[STATEMENT]
lemma exec_moves_length_compEs2D [dest]:
  "exec_moves ci P t es h (stk, loc, pc, xcp) ta h' s' \<Longrightarrow> pc < length (compEs2 es)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_moves ci P t es h (stk, loc, pc, xcp) ta h' s' \<Longrightarrow> pc < length (compEs2 es)
[PROOF STEP]
by(cases s')(auto simp add: exec_moves_def)


[STATEMENT]
lemma exec_meth_ci_appD:
  "\<lbrakk> exec_meth ci P ins xt t h (stk, loc, pc, None) ta h' fr' \<rbrakk>
  \<Longrightarrow>  ci_app ci (ins ! pc) P h stk loc undefined undefined pc []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci P ins xt t h (stk, loc, pc, None) ta h' fr' \<Longrightarrow> ci_app ci (ins ! pc) P h stk loc undefined undefined pc []
[PROOF STEP]
by(cases fr')(simp add: exec_meth_instr)


[STATEMENT]
lemma exec_move_ci_appD:
  "exec_move ci P t E h (stk, loc, pc, None) ta h' fr'
  \<Longrightarrow> ci_app ci (compE2 E ! pc) (compP2 P) h stk loc undefined undefined pc []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t E h (stk, loc, pc, None) ta h' fr' \<Longrightarrow> ci_app ci (compE2 E ! pc) (compP2 P) h stk loc undefined undefined pc []
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 E) (compxE2 E 0 0) t h (stk, loc, pc, None) ta h' fr' \<Longrightarrow> ci_app ci (compE2 E ! pc) (compP2 P) h stk loc undefined undefined pc []
[PROOF STEP]
by(rule exec_meth_ci_appD)


[STATEMENT]
lemma exec_moves_ci_appD:
  "exec_moves ci P t Es h (stk, loc, pc, None) ta h' fr'
  \<Longrightarrow> ci_app ci (compEs2 Es ! pc) (compP2 P) h stk loc undefined undefined pc []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_moves ci P t Es h (stk, loc, pc, None) ta h' fr' \<Longrightarrow> ci_app ci (compEs2 Es ! pc) (compP2 P) h stk loc undefined undefined pc []
[PROOF STEP]
unfolding exec_moves_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compEs2 Es) (compxEs2 Es 0 0) t h (stk, loc, pc, None) ta h' fr' \<Longrightarrow> ci_app ci (compEs2 Es ! pc) (compP2 P) h stk loc undefined undefined pc []
[PROOF STEP]
by(rule exec_meth_ci_appD)


[STATEMENT]
lemma \<tau>instr_stk_append_check:
  "check_instr' i P h stk loc C M pc frs \<Longrightarrow> \<tau>instr P h (stk @ vs) i = \<tau>instr P h stk i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check_instr' i P h stk loc C M pc frs \<Longrightarrow> \<tau>instr P h (stk @ vs) i = \<tau>instr P h stk i
[PROOF STEP]
by(cases i)(simp_all add: nth_append)


[STATEMENT]
lemma \<tau>instr_stk_drop_exec_move:
  "exec_move ci P t e h (stk, loc, pc, None) ta h' fr'
  \<Longrightarrow> \<tau>instr (compP2 P) h (stk @ vs) (compE2 e ! pc) = \<tau>instr (compP2 P) h stk (compE2 e ! pc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t e h (stk, loc, pc, None) ta h' fr' \<Longrightarrow> \<tau>instr (compP2 P) h (stk @ vs) (compE2 e ! pc) = \<tau>instr (compP2 P) h stk (compE2 e ! pc)
[PROOF STEP]
apply(drule exec_move_ci_appD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ci_app ci (compE2 e ! pc) (compP2 P) h stk loc undefined undefined pc [] \<Longrightarrow> \<tau>instr (compP2 P) h (stk @ vs) (compE2 e ! pc) = \<tau>instr (compP2 P) h stk (compE2 e ! pc)
[PROOF STEP]
apply(drule wf_ciD2_ci_app)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check_instr' (compE2 e ! pc) (compP2 P) h stk loc undefined undefined pc [] \<Longrightarrow> \<tau>instr (compP2 P) h (stk @ vs) (compE2 e ! pc) = \<tau>instr (compP2 P) h stk (compE2 e ! pc)
[PROOF STEP]
apply(erule \<tau>instr_stk_append_check)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma \<tau>instr_stk_drop_exec_moves:
  "exec_moves ci P t es h (stk, loc, pc, None) ta h' fr'
  \<Longrightarrow> \<tau>instr (compP2 P) h (stk @ vs) (compEs2 es ! pc) = \<tau>instr (compP2 P) h stk (compEs2 es ! pc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_moves ci P t es h (stk, loc, pc, None) ta h' fr' \<Longrightarrow> \<tau>instr (compP2 P) h (stk @ vs) (compEs2 es ! pc) = \<tau>instr (compP2 P) h stk (compEs2 es ! pc)
[PROOF STEP]
apply(drule exec_moves_ci_appD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ci_app ci (compEs2 es ! pc) (compP2 P) h stk loc undefined undefined pc [] \<Longrightarrow> \<tau>instr (compP2 P) h (stk @ vs) (compEs2 es ! pc) = \<tau>instr (compP2 P) h stk (compEs2 es ! pc)
[PROOF STEP]
apply(drule wf_ciD2_ci_app)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check_instr' (compEs2 es ! pc) (compP2 P) h stk loc undefined undefined pc [] \<Longrightarrow> \<tau>instr (compP2 P) h (stk @ vs) (compEs2 es ! pc) = \<tau>instr (compP2 P) h stk (compEs2 es ! pc)
[PROOF STEP]
apply(erule \<tau>instr_stk_append_check)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma C_simp[simp]: "blinfun_apply (C x y) (dx, dy) =
  (dx * C11 x y + dy * C12 x y,
   dx * C21 x y + dy * C22 x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. blinfun_apply (C x y) (dx, dy) = (dx * C11 x y + dy * C12 x y, dx * C21 x y + dy * C22 x y)
[PROOF STEP]
by (auto simp: C_def blinfun_of_matrix_apply Basis_prod_def)


[STATEMENT]
lemma C_continuous[continuous_intros]:
  "continuous_on S (\<lambda>x. local.C (f x) (g x))"
  if "continuous_on S f" "continuous_on S g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on S (\<lambda>x. C (f x) (g x))
[PROOF STEP]
unfolding C_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on S (\<lambda>x. blinfun_of_matrix ((\<lambda>_ _. 0)((1, 0) := (\<lambda>_. 0)((1, 0) := C11 (f x) (g x), (0, 1) := C12 (f x) (g x)), (0, 1) := (\<lambda>_. 0)((1, 0) := C21 (f x) (g x), (0, 1) := C22 (f x) (g x)))))
[PROOF STEP]
by (auto intro!: continuous_on_blinfun_of_matrix continuous_intros that
      simp: Basis_prod_def C_partials)


[STATEMENT]
lemma trapC_eq:
  shows "trapC = {p. (fst p)^2 + (snd p)^2 - 4 \<le> 0} \<inter> {p. 1/4 - ((fst p)^2 + (snd p)^2) \<le> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trapC = {p. (fst p)\<^sup>2 + (snd p)\<^sup>2 - 4 \<le> 0} \<inter> {p. 1 / 4 - ((fst p)\<^sup>2 + (snd p)\<^sup>2) \<le> 0}
[PROOF STEP]
unfolding trapC_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cball (0, 0) 2 - ball (0, 0) (1 / 2) = {p. (fst p)\<^sup>2 + (snd p)\<^sup>2 - 4 \<le> 0} \<inter> {p. 1 / 4 - ((fst p)\<^sup>2 + (snd p)\<^sup>2) \<le> 0}
[PROOF STEP]
apply (auto simp add: dist_Pair_Pair)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>sqrt (a\<^sup>2 + b\<^sup>2) \<le> 2; \<not> sqrt (a\<^sup>2 + b\<^sup>2) * 2 < 1\<rbrakk> \<Longrightarrow> a\<^sup>2 + b\<^sup>2 \<le> 4
 2. \<And>a b. \<lbrakk>sqrt (a\<^sup>2 + b\<^sup>2) \<le> 2; \<not> sqrt (a\<^sup>2 + b\<^sup>2) * 2 < 1\<rbrakk> \<Longrightarrow> 1 \<le> a\<^sup>2 * 4 + b\<^sup>2 * 4
 3. \<And>a b. \<lbrakk>a\<^sup>2 + b\<^sup>2 \<le> 4; 1 \<le> a\<^sup>2 * 4 + b\<^sup>2 * 4\<rbrakk> \<Longrightarrow> sqrt (a\<^sup>2 + b\<^sup>2) \<le> 2
 4. \<And>a b. \<lbrakk>a\<^sup>2 + b\<^sup>2 \<le> 4; 1 \<le> a\<^sup>2 * 4 + b\<^sup>2 * 4; sqrt (a\<^sup>2 + b\<^sup>2) * 2 < 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using real_sqrt_le_iff
[PROOF STATE]
proof (prove)
using this:
(sqrt ?x \<le> sqrt ?y) = (?x \<le> ?y)

goal (4 subgoals):
 1. \<And>a b. \<lbrakk>sqrt (a\<^sup>2 + b\<^sup>2) \<le> 2; \<not> sqrt (a\<^sup>2 + b\<^sup>2) * 2 < 1\<rbrakk> \<Longrightarrow> a\<^sup>2 + b\<^sup>2 \<le> 4
 2. \<And>a b. \<lbrakk>sqrt (a\<^sup>2 + b\<^sup>2) \<le> 2; \<not> sqrt (a\<^sup>2 + b\<^sup>2) * 2 < 1\<rbrakk> \<Longrightarrow> 1 \<le> a\<^sup>2 * 4 + b\<^sup>2 * 4
 3. \<And>a b. \<lbrakk>a\<^sup>2 + b\<^sup>2 \<le> 4; 1 \<le> a\<^sup>2 * 4 + b\<^sup>2 * 4\<rbrakk> \<Longrightarrow> sqrt (a\<^sup>2 + b\<^sup>2) \<le> 2
 4. \<And>a b. \<lbrakk>a\<^sup>2 + b\<^sup>2 \<le> 4; 1 \<le> a\<^sup>2 * 4 + b\<^sup>2 * 4; sqrt (a\<^sup>2 + b\<^sup>2) * 2 < 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>sqrt (a\<^sup>2 + b\<^sup>2) \<le> 2; \<not> sqrt (a\<^sup>2 + b\<^sup>2) * 2 < 1\<rbrakk> \<Longrightarrow> 1 \<le> a\<^sup>2 * 4 + b\<^sup>2 * 4
 2. \<And>a b. \<lbrakk>a\<^sup>2 + b\<^sup>2 \<le> 4; 1 \<le> a\<^sup>2 * 4 + b\<^sup>2 * 4\<rbrakk> \<Longrightarrow> sqrt (a\<^sup>2 + b\<^sup>2) \<le> 2
 3. \<And>a b. \<lbrakk>a\<^sup>2 + b\<^sup>2 \<le> 4; 1 \<le> a\<^sup>2 * 4 + b\<^sup>2 * 4; sqrt (a\<^sup>2 + b\<^sup>2) * 2 < 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (smt four_x_squared one_le_power real_sqrt_ge_0_iff real_sqrt_pow2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a\<^sup>2 + b\<^sup>2 \<le> 4; 1 \<le> a\<^sup>2 * 4 + b\<^sup>2 * 4\<rbrakk> \<Longrightarrow> sqrt (a\<^sup>2 + b\<^sup>2) \<le> 2
 2. \<And>a b. \<lbrakk>a\<^sup>2 + b\<^sup>2 \<le> 4; 1 \<le> a\<^sup>2 * 4 + b\<^sup>2 * 4; sqrt (a\<^sup>2 + b\<^sup>2) * 2 < 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using real_sqrt_le_mono
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> sqrt ?x \<le> sqrt ?y

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>a\<^sup>2 + b\<^sup>2 \<le> 4; 1 \<le> a\<^sup>2 * 4 + b\<^sup>2 * 4\<rbrakk> \<Longrightarrow> sqrt (a\<^sup>2 + b\<^sup>2) \<le> 2
 2. \<And>a b. \<lbrakk>a\<^sup>2 + b\<^sup>2 \<le> 4; 1 \<le> a\<^sup>2 * 4 + b\<^sup>2 * 4; sqrt (a\<^sup>2 + b\<^sup>2) * 2 < 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a\<^sup>2 + b\<^sup>2 \<le> 4; 1 \<le> a\<^sup>2 * 4 + b\<^sup>2 * 4; sqrt (a\<^sup>2 + b\<^sup>2) * 2 < 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a\<^sup>2 + b\<^sup>2 \<le> 4; 1 \<le> a\<^sup>2 * 4 + b\<^sup>2 * 4; sqrt (a\<^sup>2 + b\<^sup>2) * 2 < 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix a :: real and b :: real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a\<^sup>2 + b\<^sup>2 \<le> 4; 1 \<le> a\<^sup>2 * 4 + b\<^sup>2 * 4; sqrt (a\<^sup>2 + b\<^sup>2) * 2 < 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume a1: "sqrt (a\<^sup>2 + b\<^sup>2) * 2 < 1"
[PROOF STATE]
proof (state)
this:
sqrt (a\<^sup>2 + b\<^sup>2) * 2 < 1

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a\<^sup>2 + b\<^sup>2 \<le> 4; 1 \<le> a\<^sup>2 * 4 + b\<^sup>2 * 4; sqrt (a\<^sup>2 + b\<^sup>2) * 2 < 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume a2: "1 \<le> a\<^sup>2 * 4 + b\<^sup>2 * 4"
[PROOF STATE]
proof (state)
this:
1 \<le> a\<^sup>2 * 4 + b\<^sup>2 * 4

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a\<^sup>2 + b\<^sup>2 \<le> 4; 1 \<le> a\<^sup>2 * 4 + b\<^sup>2 * 4; sqrt (a\<^sup>2 + b\<^sup>2) * 2 < 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "\<forall>r. 1 \<le> sqrt r \<or> \<not> 1 \<le> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>r. 1 \<le> sqrt r \<or> \<not> 1 \<le> r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>r. 1 \<le> sqrt r \<or> \<not> 1 \<le> r

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a\<^sup>2 + b\<^sup>2 \<le> 4; 1 \<le> a\<^sup>2 * 4 + b\<^sup>2 * 4; sqrt (a\<^sup>2 + b\<^sup>2) * 2 < 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>r. 1 \<le> sqrt r \<or> \<not> 1 \<le> r
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<forall>r. 1 \<le> sqrt r \<or> \<not> 1 \<le> r

goal (1 subgoal):
 1. False
[PROOF STEP]
using a2 a1
[PROOF STATE]
proof (prove)
using this:
\<forall>r. 1 \<le> sqrt r \<or> \<not> 1 \<le> r
1 \<le> a\<^sup>2 * 4 + b\<^sup>2 * 4
sqrt (a\<^sup>2 + b\<^sup>2) * 2 < 1

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis (no_types) Groups.mult_ac(2) distrib_left linorder_not_le real_sqrt_four real_sqrt_mult)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma x_in_trapC:
  shows "(2,0) \<in> trapC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (2, 0) \<in> trapC
[PROOF STEP]
unfolding trapC_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (2, 0) \<in> cball (0, 0) 2 - ball (0, 0) (1 / 2)
[PROOF STEP]
by (auto simp add: dist_Pair_Pair)


[STATEMENT]
lemma compact_trapC:
  shows "compact trapC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compact trapC
[PROOF STEP]
unfolding trapC_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compact (cball (0, 0) 2 - ball (0, 0) (1 / 2))
[PROOF STEP]
using compact_cball compact_diff
[PROOF STATE]
proof (prove)
using this:
compact (cball ?x ?e)
\<lbrakk>compact ?S; open ?T\<rbrakk> \<Longrightarrow> compact (?S - ?T)

goal (1 subgoal):
 1. compact (cball (0, 0) 2 - ball (0, 0) (1 / 2))
[PROOF STEP]
by blast


[STATEMENT]
lemma nonempty_trapC:
  shows "trapC \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trapC \<noteq> {}
[PROOF STEP]
using x_in_trapC
[PROOF STATE]
proof (prove)
using this:
(2, 0) \<in> trapC

goal (1 subgoal):
 1. trapC \<noteq> {}
[PROOF STEP]
by auto


[STATEMENT]
lemma origin_fixpoint:
  assumes "(\<lambda>(x, y). (cx x y, cy x y)) (a,b) = 0"
  shows "a = (0::real)" "b = (0::real)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = 0 &&& b = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(case (a, b) of (x, y) \<Rightarrow> (cx x y, cy x y)) = 0

goal (1 subgoal):
 1. a = 0 &&& b = 0
[PROOF STEP]
unfolding cx_def cy_def zero_prod_def
[PROOF STATE]
proof (prove)
using this:
(case (a, b) of (x, y) \<Rightarrow> (- y + x * (1 - x\<^sup>2 - y\<^sup>2), x + y * (1 - x\<^sup>2 - y\<^sup>2))) = (0, 0)

goal (1 subgoal):
 1. a = 0 &&& b = 0
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a * (1 - a\<^sup>2 - b\<^sup>2) = b; a + b * (1 - a\<^sup>2 - b\<^sup>2) = 0\<rbrakk> \<Longrightarrow> a = 0
 2. \<lbrakk>a * (1 - a\<^sup>2 - b\<^sup>2) = b; a + b * (1 - a\<^sup>2 - b\<^sup>2) = 0\<rbrakk> \<Longrightarrow> b = 0
[PROOF STEP]
apply (sos "((((A<0 * R<1) + (([28859/65536*a + 5089/8192*b + ~1/2] * A=0) + (([~5089/8192*a + 17219/65536*b + ~1/2] * A=1) + (R<1 * ((R<11853/65536 * [~16384/11853*a^2 + ~11585/11853*b^2 + 302/1317*a*b + a + 1940/3951*b]^2) + ((R<73630271/776798208 * [a^2 + 64177444/73630271*b^2 + 44531712/73630271*a*b + ~131061126/73630271*b]^2) + ((R<70211653911/4825433440256 * [~77895776116/70211653911*b^2 + 5825642465/10030236273*a*b + b]^2) + ((R<48375415273/657341564387328 * [~36776393918/48375415273*b^2 + a*b]^2) + (R<18852430195/11096159253659648 * [b^2]^2)))))))))) & (((A<0 * (A<0 * R<1)) + (([b] * A=0) + (([~1*a] * A=1) + (R<1 * (R<1 * [b]^2)))))))")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a * (1 - a\<^sup>2 - b\<^sup>2) = b; a + b * (1 - a\<^sup>2 - b\<^sup>2) = 0\<rbrakk> \<Longrightarrow> b = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>a * (1 - a\<^sup>2 - b\<^sup>2) = b; a + b * (1 - a\<^sup>2 - b\<^sup>2) = 0\<rbrakk> \<Longrightarrow> b = 0
[PROOF STEP]
assume a1: "a * (1 - a\<^sup>2 - b\<^sup>2) = b"
[PROOF STATE]
proof (state)
this:
a * (1 - a\<^sup>2 - b\<^sup>2) = b

goal (1 subgoal):
 1. \<lbrakk>a * (1 - a\<^sup>2 - b\<^sup>2) = b; a + b * (1 - a\<^sup>2 - b\<^sup>2) = 0\<rbrakk> \<Longrightarrow> b = 0
[PROOF STEP]
assume a2: "a + b * (1 - a\<^sup>2 - b\<^sup>2) = 0"
[PROOF STATE]
proof (state)
this:
a + b * (1 - a\<^sup>2 - b\<^sup>2) = 0

goal (1 subgoal):
 1. \<lbrakk>a * (1 - a\<^sup>2 - b\<^sup>2) = b; a + b * (1 - a\<^sup>2 - b\<^sup>2) = 0\<rbrakk> \<Longrightarrow> b = 0
[PROOF STEP]
have f3: "\<forall>r ra. - (ra::real) * r = ra * - r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>r ra. - ra * r = ra * - r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>r ra. - ra * r = ra * - r

goal (1 subgoal):
 1. \<lbrakk>a * (1 - a\<^sup>2 - b\<^sup>2) = b; a + b * (1 - a\<^sup>2 - b\<^sup>2) = 0\<rbrakk> \<Longrightarrow> b = 0
[PROOF STEP]
have "- b * (1 - a\<^sup>2 - b\<^sup>2) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - b * (1 - a\<^sup>2 - b\<^sup>2) = a
[PROOF STEP]
using a2
[PROOF STATE]
proof (prove)
using this:
a + b * (1 - a\<^sup>2 - b\<^sup>2) = 0

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

goal (1 subgoal):
 1. \<lbrakk>a * (1 - a\<^sup>2 - b\<^sup>2) = b; a + b * (1 - a\<^sup>2 - b\<^sup>2) = 0\<rbrakk> \<Longrightarrow> b = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
- b * (1 - a\<^sup>2 - b\<^sup>2) = a
[PROOF STEP]
have "\<exists>r ra. b * b - ra * (r * (ra * - r)) = 0"
[PROOF STATE]
proof (prove)
using this:
- b * (1 - a\<^sup>2 - b\<^sup>2) = a

goal (1 subgoal):
 1. \<exists>r ra. b * b - ra * (r * (ra * - r)) = 0
[PROOF STEP]
using f3 a1
[PROOF STATE]
proof (prove)
using this:
- b * (1 - a\<^sup>2 - b\<^sup>2) = a
\<forall>r ra. - ra * r = ra * - r
a * (1 - a\<^sup>2 - b\<^sup>2) = b

goal (1 subgoal):
 1. \<exists>r ra. b * b - ra * (r * (ra * - r)) = 0
[PROOF STEP]
by (metis (no_types) c.vec_simps(15) right_minus_eq)
[PROOF STATE]
proof (state)
this:
\<exists>r ra. b * b - ra * (r * (ra * - r)) = 0

goal (1 subgoal):
 1. \<lbrakk>a * (1 - a\<^sup>2 - b\<^sup>2) = b; a + b * (1 - a\<^sup>2 - b\<^sup>2) = 0\<rbrakk> \<Longrightarrow> b = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>r ra. b * b - ra * (r * (ra * - r)) = 0
[PROOF STEP]
have "\<exists>r. b * b - r * - r = 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>r ra. b * b - ra * (r * (ra * - r)) = 0

goal (1 subgoal):
 1. \<exists>r. b * b - r * - r = 0
[PROOF STEP]
using f3
[PROOF STATE]
proof (prove)
using this:
\<exists>r ra. b * b - ra * (r * (ra * - r)) = 0
\<forall>r ra. - ra * r = ra * - r

goal (1 subgoal):
 1. \<exists>r. b * b - r * - r = 0
[PROOF STEP]
by (metis (no_types) c.vec_simps(14))
[PROOF STATE]
proof (state)
this:
\<exists>r. b * b - r * - r = 0

goal (1 subgoal):
 1. \<lbrakk>a * (1 - a\<^sup>2 - b\<^sup>2) = b; a + b * (1 - a\<^sup>2 - b\<^sup>2) = 0\<rbrakk> \<Longrightarrow> b = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>r. b * b - r * - r = 0
[PROOF STEP]
show "b = 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>r. b * b - r * - r = 0

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma origin_not_trapC:
  shows "0 \<notin> trapC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<notin> trapC
[PROOF STEP]
unfolding trapC_def zero_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0, 0) \<notin> cball (0, 0) 2 - ball (0, 0) (1 / 2)
[PROOF STEP]
by auto


[STATEMENT]
lemma regular_trapC:
  shows "0 \<notin> (\<lambda>(x, y). (cx x y, cy x y)) ` trapC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<notin> (\<lambda>(x, y). (cx x y, cy x y)) ` trapC
[PROOF STEP]
using origin_fixpoint origin_not_trapC
[PROOF STATE]
proof (prove)
using this:
(case (?a, ?b) of (x, y) \<Rightarrow> (cx x y, cy x y)) = 0 \<Longrightarrow> ?a = 0
(case (?a, ?b) of (x, y) \<Rightarrow> (cx x y, cy x y)) = 0 \<Longrightarrow> ?b = 0
0 \<notin> trapC

goal (1 subgoal):
 1. 0 \<notin> (\<lambda>(x, y). (cx x y, cy x y)) ` trapC
[PROOF STEP]
by (smt UNIV_I UNIV_I UNIV_def case_prodE2 imageE c.flow_initial_time_if
      c.rev.flow_initial_time_if mem_Collect_eq zero_prod_def)


[STATEMENT]
lemma positively_invariant_outer:
  shows "c.positively_invariant  {p. (\<lambda>p. (fst p)\<^sup>2 + (snd p)\<^sup>2 - 4) p \<le> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c.positively_invariant {p. (fst p)\<^sup>2 + (snd p)\<^sup>2 - 4 \<le> 0}
[PROOF STEP]
apply (rule c.positively_invariant_le[of "\<lambda>p.-2*((fst p)^2+(snd p)^2)" _  "\<lambda>x p. 2 * fst x * fst p + 2 * snd x * snd p" ])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. continuous_on UNIV (\<lambda>p. - 2 * ((fst p)\<^sup>2 + (snd p)\<^sup>2))
 2. \<And>x. ((\<lambda>x. (fst x)\<^sup>2 + (snd x)\<^sup>2 - 4) has_derivative (\<lambda>p. 2 * fst x * fst p + 2 * snd x * snd p)) (at x)
 3. \<And>s. 2 * fst s * fst (case s of (x, y) \<Rightarrow> (cx x y, cy x y)) + 2 * snd s * snd (case s of (x, y) \<Rightarrow> (cx x y, cy x y)) \<le> - 2 * ((fst s)\<^sup>2 + (snd s)\<^sup>2) * ((fst s)\<^sup>2 + (snd s)\<^sup>2 - 4)
[PROOF STEP]
apply (auto intro!: continuous_intros derivative_eq_intros)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. 2 * a * cx a b + 2 * b * cy a b \<le> (- (2 * a\<^sup>2) - 2 * b\<^sup>2) * (a\<^sup>2 + b\<^sup>2 - 4)
[PROOF STEP]
unfolding cx_def cy_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. 2 * a * (- b + a * (1 - a\<^sup>2 - b\<^sup>2)) + 2 * b * (a + b * (1 - a\<^sup>2 - b\<^sup>2)) \<le> (- (2 * a\<^sup>2) - 2 * b\<^sup>2) * (a\<^sup>2 + b\<^sup>2 - 4)
[PROOF STEP]
by (sos "(((A<0 * R<1) + (R<1 * ((R<6 * [a]^2) + (R<6 * [b]^2)))))")


[STATEMENT]
lemma positively_invariant_inner:
  shows "c.positively_invariant  {p. (\<lambda>p. 1/4 - ((fst p)\<^sup>2 + (snd p)\<^sup>2)) p \<le> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c.positively_invariant {p. 1 / 4 - ((fst p)\<^sup>2 + (snd p)\<^sup>2) \<le> 0}
[PROOF STEP]
apply (rule c.positively_invariant_le[of "\<lambda>p.-2*((fst p)^2+(snd p)^2)" _ "\<lambda>x p. - 2 * fst x * fst p - 2 * snd x * snd p"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. continuous_on UNIV (\<lambda>p. - 2 * ((fst p)\<^sup>2 + (snd p)\<^sup>2))
 2. \<And>x. ((\<lambda>x. 1 / 4 - ((fst x)\<^sup>2 + (snd x)\<^sup>2)) has_derivative (\<lambda>p. - 2 * fst x * fst p - 2 * snd x * snd p)) (at x)
 3. \<And>s. - 2 * fst s * fst (case s of (x, y) \<Rightarrow> (cx x y, cy x y)) - 2 * snd s * snd (case s of (x, y) \<Rightarrow> (cx x y, cy x y)) \<le> - 2 * ((fst s)\<^sup>2 + (snd s)\<^sup>2) * (1 / 4 - ((fst s)\<^sup>2 + (snd s)\<^sup>2))
[PROOF STEP]
apply (auto intro!: continuous_intros derivative_eq_intros)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. - (2 * a * cx a b) - 2 * b * cy a b \<le> (- (2 * a\<^sup>2) - 2 * b\<^sup>2) * (1 / 4 - (a\<^sup>2 + b\<^sup>2))
[PROOF STEP]
unfolding cx_def cy_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. - (2 * a * (- b + a * (1 - a\<^sup>2 - b\<^sup>2))) - 2 * b * (a + b * (1 - a\<^sup>2 - b\<^sup>2)) \<le> (- (2 * a\<^sup>2) - 2 * b\<^sup>2) * (1 / 4 - (a\<^sup>2 + b\<^sup>2))
[PROOF STEP]
by (sos "(((A<0 * R<1) + (R<1 * ((R<3/2 * [a]^2) + (R<3/2 * [b]^2)))))")


[STATEMENT]
lemma positively_invariant_trapC:
  shows "c.positively_invariant trapC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c.positively_invariant trapC
[PROOF STEP]
unfolding trapC_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c.positively_invariant ({p. (fst p)\<^sup>2 + (snd p)\<^sup>2 - 4 \<le> 0} \<inter> {p. 1 / 4 - ((fst p)\<^sup>2 + (snd p)\<^sup>2) \<le> 0})
[PROOF STEP]
apply (rule c.positively_invariant_conj)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. c.positively_invariant {p. (fst p)\<^sup>2 + (snd p)\<^sup>2 - 4 \<le> 0}
 2. c.positively_invariant {p. 1 / 4 - ((fst p)\<^sup>2 + (snd p)\<^sup>2) \<le> 0}
[PROOF STEP]
using positively_invariant_outer
[PROOF STATE]
proof (prove)
using this:
c.positively_invariant {p. (fst p)\<^sup>2 + (snd p)\<^sup>2 - 4 \<le> 0}

goal (2 subgoals):
 1. c.positively_invariant {p. (fst p)\<^sup>2 + (snd p)\<^sup>2 - 4 \<le> 0}
 2. c.positively_invariant {p. 1 / 4 - ((fst p)\<^sup>2 + (snd p)\<^sup>2) \<le> 0}
[PROOF STEP]
apply (metis (no_types, lifting) Collect_cong case_prodE case_prodI2 case_prod_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c.positively_invariant {p. 1 / 4 - ((fst p)\<^sup>2 + (snd p)\<^sup>2) \<le> 0}
[PROOF STEP]
using positively_invariant_inner
[PROOF STATE]
proof (prove)
using this:
c.positively_invariant {p. 1 / 4 - ((fst p)\<^sup>2 + (snd p)\<^sup>2) \<le> 0}

goal (1 subgoal):
 1. c.positively_invariant {p. 1 / 4 - ((fst p)\<^sup>2 + (snd p)\<^sup>2) \<le> 0}
[PROOF STEP]
by (metis (no_types, lifting) Collect_cong case_prodE case_prodI2 case_prod_conv)


[STATEMENT]
theorem c_has_periodic_orbit:
  obtains y where "c.periodic_orbit y" "c.flow0 y ` UNIV \<subseteq> trapC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>c.periodic_orbit y; range (c.flow0 y) \<subseteq> trapC\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>c.periodic_orbit y; range (c.flow0 y) \<subseteq> trapC\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from c.poincare_bendixson_applied[OF compact_trapC _ nonempty_trapC positively_invariant_trapC regular_trapC]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>trapC \<subseteq> UNIV; \<And>y. \<lbrakk>c.periodic_orbit y; range (c.flow0 y) \<subseteq> trapC\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>trapC \<subseteq> UNIV; \<And>y. \<lbrakk>c.periodic_orbit y; range (c.flow0 y) \<subseteq> trapC\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>trapC \<subseteq> UNIV; \<And>y. \<lbrakk>c.periodic_orbit y; range (c.flow0 y) \<subseteq> trapC\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
\<lbrakk>c.periodic_orbit ?y1; range (c.flow0 ?y1) \<subseteq> trapC\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma crev: "t \<in> {1/8 .. 1/8} \<longrightarrow> (x, y) \<in> {(2, 0) .. (2, 0)} \<longrightarrow>
   t \<in> c.rev.existence_ivl0 (x, y) \<and> c.rev.flow0 (x, y) t \<in> {(5.15, -0.651)..(5.18, -0.647)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> point_ivl (1 / 8) \<longrightarrow> (x, y) \<in> point_ivl (2, 0) \<longrightarrow> t \<in> c.rev.existence_ivl0 (x, y) \<and> c.rev.flow0 (x, y) t \<in> {(515 / 10\<^sup>2, - (651 / 10 ^ 3))..(518 / 10\<^sup>2, - (647 / 10 ^ 3))}
[PROOF STEP]
by (tactic \<open>ode_bnds_tac @{thms c_fas_def} 30 20 7 12 [(0, 1, "0x000000")] (* "crev.out" *) "" @{context} 1\<close>)


[STATEMENT]
theorem c_has_limit_cycle:
  obtains y where "c.limit_cycle y" "range (c.flow0 y) \<subseteq> trapC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>c.limit_cycle y; range (c.flow0 y) \<subseteq> trapC\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>c.limit_cycle y; range (c.flow0 y) \<subseteq> trapC\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define E where "E = {(5.15, -0.651)..(5.18, -0.647)::real*real}"
[PROOF STATE]
proof (state)
this:
E = {(515 / 10\<^sup>2, - (651 / 10 ^ 3))..(518 / 10\<^sup>2, - (647 / 10 ^ 3))}

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>c.limit_cycle y; range (c.flow0 y) \<subseteq> trapC\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from crev
[PROOF STATE]
proof (chain)
picking this:
?t \<in> point_ivl (1 / 8) \<longrightarrow> (?x, ?y) \<in> point_ivl (2, 0) \<longrightarrow> ?t \<in> c.rev.existence_ivl0 (?x, ?y) \<and> c.rev.flow0 (?x, ?y) ?t \<in> {(515 / 10\<^sup>2, - (651 / 10 ^ 3))..(518 / 10\<^sup>2, - (647 / 10 ^ 3))}
[PROOF STEP]
have "c.rev.flow0 (2, 0) (1/8) \<in> E"
[PROOF STATE]
proof (prove)
using this:
?t \<in> point_ivl (1 / 8) \<longrightarrow> (?x, ?y) \<in> point_ivl (2, 0) \<longrightarrow> ?t \<in> c.rev.existence_ivl0 (?x, ?y) \<and> c.rev.flow0 (?x, ?y) ?t \<in> {(515 / 10\<^sup>2, - (651 / 10 ^ 3))..(518 / 10\<^sup>2, - (647 / 10 ^ 3))}

goal (1 subgoal):
 1. c.rev.flow0 (2, 0) (1 / 8) \<in> E
[PROOF STEP]
by (auto simp: E_def)
[PROOF STATE]
proof (state)
this:
c.rev.flow0 (2, 0) (1 / 8) \<in> E

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>c.limit_cycle y; range (c.flow0 y) \<subseteq> trapC\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c.rev.flow0 (2, 0) (1 / 8) \<in> E

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>c.limit_cycle y; range (c.flow0 y) \<subseteq> trapC\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "E \<inter> trapC = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E \<inter> trapC = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. E \<inter> trapC = {}
[PROOF STEP]
have "norm x > 2" if "x \<in> E" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 < norm x
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<in> E

goal (1 subgoal):
 1. 2 < norm x
[PROOF STEP]
apply (auto simp: norm_prod_def less_eq_prod_def E_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>103 \<le> fst x * 20; - (651 / 1000) \<le> snd x; fst x * 50 \<le> 259; snd x \<le> - (647 / 1000)\<rbrakk> \<Longrightarrow> 2 < sqrt ((fst x)\<^sup>2 + (snd x)\<^sup>2)
[PROOF STEP]
by (smt power2_less_eq_zero_iff real_less_rsqrt zero_compare_simps(9))
[PROOF STATE]
proof (state)
this:
?x1 \<in> E \<Longrightarrow> 2 < norm ?x1

goal (1 subgoal):
 1. E \<inter> trapC = {}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?x1 \<in> E \<Longrightarrow> 2 < norm ?x1

goal (1 subgoal):
 1. E \<inter> trapC = {}
[PROOF STEP]
have "norm x \<le> 2" if "x \<in> trapC" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm x \<le> 2
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
x \<in> trapC

goal (1 subgoal):
 1. norm x \<le> 2
[PROOF STEP]
by (auto simp: trapC_def dist_prod_def norm_prod_def)
[PROOF STATE]
proof (state)
this:
?x1 \<in> trapC \<Longrightarrow> norm ?x1 \<le> 2

goal (1 subgoal):
 1. E \<inter> trapC = {}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?x1 \<in> E \<Longrightarrow> 2 < norm ?x1
?x1 \<in> trapC \<Longrightarrow> norm ?x1 \<le> 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> E \<Longrightarrow> 2 < norm ?x1
?x1 \<in> trapC \<Longrightarrow> norm ?x1 \<le> 2

goal (1 subgoal):
 1. E \<inter> trapC = {}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
E \<inter> trapC = {}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
E \<inter> trapC = {}

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>c.limit_cycle y; range (c.flow0 y) \<subseteq> trapC\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
c.rev.flow0 (2, 0) (1 / 8) \<in> E
E \<inter> trapC = {}
[PROOF STEP]
have "c.rev.flow0 (2, 0) (1 / 8) \<notin> trapC"
[PROOF STATE]
proof (prove)
using this:
c.rev.flow0 (2, 0) (1 / 8) \<in> E
E \<inter> trapC = {}

goal (1 subgoal):
 1. c.rev.flow0 (2, 0) (1 / 8) \<notin> trapC
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
c.rev.flow0 (2, 0) (1 / 8) \<notin> trapC

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>c.limit_cycle y; range (c.flow0 y) \<subseteq> trapC\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from c.poincare_bendixson_limit_cycle[OF compact_trapC subset_UNIV x_in_trapC positively_invariant_trapC regular_trapC this] that
[PROOF STATE]
proof (chain)
picking this:
(\<And>y. \<lbrakk>c.limit_cycle y; range (c.flow0 y) \<subseteq> trapC\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
\<lbrakk>c.limit_cycle ?y1; range (c.flow0 ?y1) \<subseteq> trapC\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<And>y. \<lbrakk>c.limit_cycle y; range (c.flow0 y) \<subseteq> trapC\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
\<lbrakk>c.limit_cycle ?y1; range (c.flow0 ?y1) \<subseteq> trapC\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma A_simp[simp]: "blinfun_apply (A x y) (dx, dy) =
  (dx * A11 x y + dy * A12 x y,
   dx * A21 x y + dy * A22 x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. blinfun_apply (A x y) (dx, dy) = (dx * A11 x y + dy * A12 x y, dx * A21 x y + dy * A22 x y)
[PROOF STEP]
by (auto simp: A_def blinfun_of_matrix_apply Basis_prod_def)


[STATEMENT]
lemma A_continuous[continuous_intros]:
  "continuous_on S (\<lambda>x. local.A (f x) (g x))"
  if "continuous_on S f" "continuous_on S g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on S (\<lambda>x. A (f x) (g x))
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on S (\<lambda>x. blinfun_of_matrix ((\<lambda>_ _. 0)((1, 0) := (\<lambda>_. 0)((1, 0) := A11 (f x) (g x), (0, 1) := A12 (f x) (g x)), (0, 1) := (\<lambda>_. 0)((1, 0) := A21 (f x) (g x), (0, 1) := A22 (f x) (g x)))))
[PROOF STEP]
by (auto intro!: continuous_on_blinfun_of_matrix continuous_intros that
      simp: Basis_prod_def A_partials)


[STATEMENT]
lemma positively_invariant_y:
  shows "g.positively_invariant {p . - snd p \<le> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g.positively_invariant {p. - snd p \<le> 0}
[PROOF STEP]
apply (rule g.positively_invariant_le[of "\<lambda>p. -(0.08 + (fst p)^2)" _ "\<lambda>x p. - snd p"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. continuous_on UNIV (\<lambda>p. - (8 / 10\<^sup>2 + (fst p)\<^sup>2))
 2. \<And>x. ((\<lambda>x. - snd x) has_derivative (\<lambda>p. - snd p)) (at x)
 3. \<And>s. - snd (case s of (x, y) \<Rightarrow> (gx x y, gy x y)) \<le> - (8 / 10\<^sup>2 + (fst s)\<^sup>2) * - snd s
[PROOF STEP]
apply (auto intro!: continuous_intros derivative_eq_intros)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. (- (2 / 25) - a\<^sup>2) * b \<le> gy a b
[PROOF STEP]
unfolding gy_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. (- (2 / 25) - a\<^sup>2) * b \<le> 6 / 10 - 8 / 10\<^sup>2 * b - a\<^sup>2 * b
[PROOF STEP]
by (sos "()")


[STATEMENT]
lemma positively_invariant_pos_quad:
  shows "g.positively_invariant pos_quad"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g.positively_invariant pos_quad
[PROOF STEP]
unfolding pos_quad_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g.positively_invariant ({p. - snd p \<le> 0} \<inter> {p. - fst p \<le> 0})
[PROOF STEP]
apply (rule g.positively_invariant_le_domain[OF positively_invariant_y, of "\<lambda>p. fst p * snd p -1"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. continuous_on {p. - snd p \<le> 0} (\<lambda>p. fst p * snd p - 1)
 2. \<And>x. ((\<lambda>x. - fst x) has_derivative ?V' x) (at x)
 3. \<And>s. s \<in> {p. - snd p \<le> 0} \<Longrightarrow> ?V' s (case s of (x, y) \<Rightarrow> (gx x y, gy x y)) \<le> (fst s * snd s - 1) * - fst s
[PROOF STEP]
apply (auto intro!: continuous_intros derivative_eq_intros)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. 0 \<le> b \<Longrightarrow> (a * b - 1) * a \<le> gx a b
[PROOF STEP]
unfolding gx_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. 0 \<le> b \<Longrightarrow> (a * b - 1) * a \<le> - a + 8 / 10\<^sup>2 * b + a\<^sup>2 * b
[PROOF STEP]
by (sos "(((A<0 * R<1) + (((A<0 * R<1) * (R<11/14 * [1]^2)) + ((A<=0 * R<1) * (R<1/7 * [1]^2)))))")


[STATEMENT]
lemma positively_invariant_y_upper:
  shows "g.positively_invariant {p. (snd p) - 751/100 \<le> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g.positively_invariant {p. snd p - 751 / 100 \<le> 0}
[PROOF STEP]
apply (rule g.positively_invariant_barrier)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. ((\<lambda>x. snd x - 751 / 100) has_derivative ?V' x) (at x)
 2. continuous_on UNIV (\<lambda>x. ?V' x (case x of (x, y) \<Rightarrow> (gx x y, gy x y)))
 3. \<And>s. snd s - 751 / 100 = 0 \<Longrightarrow> ?V' s (case s of (x, y) \<Rightarrow> (gx x y, gy x y)) < 0
[PROOF STEP]
apply (auto intro!: continuous_intros derivative_eq_intros)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. b * 100 = 751 \<Longrightarrow> gy a b < 0
[PROOF STEP]
unfolding gy_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. b * 100 = 751 \<Longrightarrow> 6 / 10 - 8 / 10\<^sup>2 * b - a\<^sup>2 * b < 0
[PROOF STEP]
by (sos "((R<1 + ((R<1 * (R<18775/2 * [a]^2)) + ((A<=0 * R<1) * (R<1250 * [1]^2)))))")


[STATEMENT]
lemma arith2:
  shows "(y::real) \<le> 751/100 \<and> x + (y::real) = 812/100 \<Longrightarrow> 3/5 - (x::real) < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> 751 / 100 \<and> x + y = 812 / 100 \<Longrightarrow> 3 / 5 - x < 0
[PROOF STEP]
by linarith


[STATEMENT]
lemma positively_invariant_trapG1:
  shows "g.positively_invariant trapG1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g.positively_invariant trapG1
[PROOF STEP]
unfolding trapG1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g.positively_invariant (pos_quad \<inter> ({p. snd p - 751 / 100 \<le> 0} \<inter> {p. fst p + snd p - 812 / 100 \<le> 0}))
[PROOF STEP]
apply (rule g.positively_invariant_conj[OF positively_invariant_pos_quad])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g.positively_invariant ({p. snd p - 751 / 100 \<le> 0} \<inter> {p. fst p + snd p - 812 / 100 \<le> 0})
[PROOF STEP]
apply (rule g.positively_invariant_barrier_domain[OF positively_invariant_y_upper])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. ((\<lambda>x. fst x + snd x - 812 / 100) has_derivative ?V'2 x) (at x)
 2. continuous_on {p. snd p - 751 / 100 \<le> 0} (\<lambda>x. ?V'2 x (case x of (x, y) \<Rightarrow> (gx x y, gy x y)))
 3. \<And>s. \<lbrakk>s \<in> {p. snd p - 751 / 100 \<le> 0}; fst s + snd s - 812 / 100 = 0\<rbrakk> \<Longrightarrow> ?V'2 s (case s of (x, y) \<Rightarrow> (gx x y, gy x y)) < 0
[PROOF STEP]
apply (auto intro!: continuous_intros derivative_eq_intros)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>b * 100 \<le> 751; a * 25 + b * 25 = 203\<rbrakk> \<Longrightarrow> gx a b + gy a b < 0
[PROOF STEP]
unfolding gx_def gy_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>b * 100 \<le> 751; a * 25 + b * 25 = 203\<rbrakk> \<Longrightarrow> - a + 8 / 10\<^sup>2 * b + a\<^sup>2 * b + (6 / 10 - 8 / 10\<^sup>2 * b - a\<^sup>2 * b) < 0
[PROOF STEP]
by auto


[STATEMENT]
lemma p1_has_derivative:
  shows "((\<lambda>x. p1 (fst x) (snd x)) has_derivative p1d x) (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. p1 (fst x) (snd x)) has_derivative p1d x) (at x)
[PROOF STEP]
unfolding p1_def p1d_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. - (21 / 34) - 69 * fst x / 38 + 19 * (fst x)\<^sup>2 / 15 - 9 * fst x ^ 3 / 28 - 6 * fst x ^ 4 / 43 + 14 * snd x / 29 + 31 * fst x * snd x / 21 + 182 * (fst x)\<^sup>2 * snd x / 47 - 35 * fst x ^ 3 * snd x / 16 - 3 * (snd x)\<^sup>2 / 17 - 2 * fst x * (snd x)\<^sup>2 / 9 - 31 * (fst x)\<^sup>2 * (snd x)\<^sup>2 / 20 + snd x ^ 3 / 102 + fst x * snd x ^ 3 / 59) has_derivative (\<lambda>xa. 38 * (fst xa * fst x) / 15 - 69 * fst xa / 38 - 27 * (fst xa * (fst x)\<^sup>2) / 28 - 24 * (fst xa * fst x ^ 3) / 43 + 14 * snd xa / 29 + (651 * (fst x * snd xa) + 651 * (fst xa * snd x)) / 441 + (8554 * ((fst x)\<^sup>2 * snd xa) + 17108 * (fst xa * (fst x * snd x))) / 2209 - (560 * (fst x ^ 3 * snd xa) + 1680 * (fst xa * ((fst x)\<^sup>2 * snd x))) / 256 - 6 * (snd xa * snd x) / 17 - (36 * (fst x * (snd xa * snd x)) + 18 * (fst xa * (snd x)\<^sup>2)) / 81 - (1240 * ((fst x)\<^sup>2 * (snd xa * snd x)) + 1240 * (fst xa * (fst x * (snd x)\<^sup>2))) / 400 + snd xa * (snd x)\<^sup>2 / 34 + (177 * (fst x * (snd xa * (snd x)\<^sup>2)) + fst xa * snd x ^ 3 * 59) / 3481)) (at x)
[PROOF STEP]
by (auto intro!: continuous_intros derivative_eq_intros)


[STATEMENT]
lemma p1_not_equil:
  shows " p1 x y \<le> 0 \<Longrightarrow> gx x y \<noteq> 0 \<or> gy x y \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p1 x y \<le> 0 \<Longrightarrow> gx x y \<noteq> 0 \<or> gy x y \<noteq> 0
[PROOF STEP]
unfolding gx_def gy_def p1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (21 / 34) - 69 * x / 38 + 19 * x\<^sup>2 / 15 - 9 * x ^ 3 / 28 - 6 * x ^ 4 / 43 + 14 * y / 29 + 31 * x * y / 21 + 182 * x\<^sup>2 * y / 47 - 35 * x ^ 3 * y / 16 - 3 * y\<^sup>2 / 17 - 2 * x * y\<^sup>2 / 9 - 31 * x\<^sup>2 * y\<^sup>2 / 20 + y ^ 3 / 102 + x * y ^ 3 / 59 \<le> 0 \<Longrightarrow> - x + 8 / 10\<^sup>2 * y + x\<^sup>2 * y \<noteq> 0 \<or> 6 / 10 - 8 / 10\<^sup>2 * y - x\<^sup>2 * y \<noteq> 0
[PROOF STEP]
by (sos "()")


[STATEMENT]
lemma list_interval2: "list_interval [a, b] [c, d] = {[x, y] | x y. x \<in> {a .. c} \<and> y \<in> {b .. d}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_interval [a, b] [c, d] = {[x, y] |x y. x \<in> {a..c} \<and> y \<in> {b..d}}
[PROOF STEP]
apply (auto simp: list_interval_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>list_all2 (\<le>) [a, b] x; list_all2 (\<le>) x [c, d]\<rbrakk> \<Longrightarrow> \<exists>xa y. x = [xa, y] \<and> a \<le> xa \<and> xa \<le> c \<and> b \<le> y \<and> y \<le> d
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all2 (\<le>) [a, b] x; list_all2 (\<le>) x [c, d]\<rbrakk> \<Longrightarrow> \<exists>xa y. x = [xa, y] \<and> a \<le> xa \<and> xa \<le> c \<and> b \<le> y \<and> y \<le> d
[PROOF STEP]
apply (cases x)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>list_all2 (\<le>) [a, b] x; list_all2 (\<le>) x [c, d]; x = []\<rbrakk> \<Longrightarrow> \<exists>xa y. x = [xa, y] \<and> a \<le> xa \<and> xa \<le> c \<and> b \<le> y \<and> y \<le> d
 2. \<And>aa list. \<lbrakk>list_all2 (\<le>) [a, b] x; list_all2 (\<le>) x [c, d]; x = aa # list\<rbrakk> \<Longrightarrow> \<exists>xa y. x = [xa, y] \<and> a \<le> xa \<and> xa \<le> c \<and> b \<le> y \<and> y \<le> d
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa list. \<lbrakk>x = aa # list; a \<le> aa; list_all2 (\<le>) [b] list; aa \<le> c; list_all2 (\<le>) list [d]\<rbrakk> \<Longrightarrow> \<exists>y. list = [y] \<and> b \<le> y \<and> y \<le> d
[PROOF STEP]
subgoal for y zs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = y # zs; a \<le> y; list_all2 (\<le>) [b] zs; y \<le> c; list_all2 (\<le>) zs [d]\<rbrakk> \<Longrightarrow> \<exists>y. zs = [y] \<and> b \<le> y \<and> y \<le> d
[PROOF STEP]
apply (cases zs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x = y # zs; a \<le> y; list_all2 (\<le>) [b] zs; y \<le> c; list_all2 (\<le>) zs [d]; zs = []\<rbrakk> \<Longrightarrow> \<exists>y. zs = [y] \<and> b \<le> y \<and> y \<le> d
 2. \<And>aa list. \<lbrakk>x = y # zs; a \<le> y; list_all2 (\<le>) [b] zs; y \<le> c; list_all2 (\<le>) zs [d]; zs = aa # list\<rbrakk> \<Longrightarrow> \<exists>y. zs = [y] \<and> b \<le> y \<and> y \<le> d
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma g_arith_nonneg: "g_arith a b \<ge> 0"
  if a: "0 \<le> a" "a \<le> 8.24" and b: "0 \<le> b" "b \<le> 7.51"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> g_arith a b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 \<le> g_arith a b
[PROOF STEP]
have "prove_nonneg [(0, 1, ''0x000000'')] 1000000 30 (slp_of_fas [hd g_arith_fas]) [aforms_of_ivls [0, 0]
    [float_divr 30 824 100, float_divr 30 751 100]]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prove_nonneg [(0, 1, ''0x000000'')] 1000000 30 (slp_of_fas [hd g_arith_fas]) [aforms_of_ivls [0, 0] (map real_of_float [float_divr 30 824 100, float_divr 30 751 100])]
[PROOF STEP]
by eval\<comment> \<open>slow: 60s\<close>
[PROOF STATE]
proof (state)
this:
prove_nonneg [(0, 1, ''0x000000'')] 1000000 30 (slp_of_fas [hd g_arith_fas]) [aforms_of_ivls [0, 0] (map real_of_float [float_divr 30 824 100, float_divr 30 751 100])]

goal (1 subgoal):
 1. 0 \<le> g_arith a b
[PROOF STEP]
from prove_nonneg[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<forall>XS\<in>set [aforms_of_ivls [0, 0] (map real_of_float [float_divr 30 824 100, float_divr 30 751 100])]. \<forall>xs\<in>Joints XS. 0 \<le> interpret_floatarith (hd g_arith_fas) xs
[PROOF STEP]
have "0 \<le> interpret_floatarith (hd g_arith_fas) [a, b]"
[PROOF STATE]
proof (prove)
using this:
\<forall>XS\<in>set [aforms_of_ivls [0, 0] (map real_of_float [float_divr 30 824 100, float_divr 30 751 100])]. \<forall>xs\<in>Joints XS. 0 \<le> interpret_floatarith (hd g_arith_fas) xs

goal (1 subgoal):
 1. 0 \<le> interpret_floatarith (hd g_arith_fas) [a, b]
[PROOF STEP]
apply (auto simp: g_arith_fas)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xs\<in>Joints (aforms_of_ivls [0, 0] [real_of_float (float_divr 30 824 100), real_of_float (float_divr 30 751 100)]). 0 \<le> interpret_floatarith (hd g_arith_fas) xs \<Longrightarrow> 0 \<le> interpret_floatarith (hd g_arith_fas) [a, b]
[PROOF STEP]
apply (subst (asm) Joints_aforms_of_ivls)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. list_all2 (\<le>) [0, 0] [real_of_float (float_divr 30 824 100), real_of_float (float_divr 30 751 100)]
 2. \<forall>xs\<in>list_interval [0, 0] [real_of_float (float_divr 30 824 100), real_of_float (float_divr 30 751 100)]. 0 \<le> interpret_floatarith (hd g_arith_fas) xs \<Longrightarrow> 0 \<le> interpret_floatarith (hd g_arith_fas) [a, b]
[PROOF STEP]
apply (auto )
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. 0 \<le> real_of_float (float_divr 30 824 100)
 2. 0 \<le> real_of_float (float_divr 30 751 100)
 3. \<forall>xs\<in>list_interval [0, 0] [real_of_float (float_divr 30 824 100), real_of_float (float_divr 30 751 100)]. 0 \<le> interpret_floatarith (hd g_arith_fas) xs \<Longrightarrow> 0 \<le> interpret_floatarith (hd g_arith_fas) [a, b]
[PROOF STEP]
apply (smt divide_nonneg_nonneg float_divr float_numeral rel_simps(27))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 \<le> real_of_float (float_divr 30 751 100)
 2. \<forall>xs\<in>list_interval [0, 0] [real_of_float (float_divr 30 824 100), real_of_float (float_divr 30 751 100)]. 0 \<le> interpret_floatarith (hd g_arith_fas) xs \<Longrightarrow> 0 \<le> interpret_floatarith (hd g_arith_fas) [a, b]
[PROOF STEP]
apply (smt divide_nonneg_nonneg float_divr float_numeral rel_simps(27))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xs\<in>list_interval [0, 0] [real_of_float (float_divr 30 824 100), real_of_float (float_divr 30 751 100)]. 0 \<le> interpret_floatarith (hd g_arith_fas) xs \<Longrightarrow> 0 \<le> interpret_floatarith (hd g_arith_fas) [a, b]
[PROOF STEP]
apply (subst (asm) list_interval2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xs\<in>{[x, y] |x y. x \<in> {0..real_of_float (float_divr 30 824 100)} \<and> y \<in> {0..real_of_float (float_divr 30 751 100)}}. 0 \<le> interpret_floatarith (hd g_arith_fas) xs \<Longrightarrow> 0 \<le> interpret_floatarith (hd g_arith_fas) [a, b]
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xs. (\<exists>x y. xs = [x, y] \<and> 0 \<le> x \<and> x \<le> real_of_float (float_divr 30 824 100) \<and> 0 \<le> y \<and> y \<le> real_of_float (float_divr 30 751 100)) \<longrightarrow> 0 \<le> interpret_floatarith (hd g_arith_fas) xs \<Longrightarrow> 0 \<le> interpret_floatarith (hd g_arith_fas) [a, b]
[PROOF STEP]
apply (drule spec[where x="[a, b]"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x y. [a, b] = [x, y] \<and> 0 \<le> x \<and> x \<le> real_of_float (float_divr 30 824 100) \<and> 0 \<le> y \<and> y \<le> real_of_float (float_divr 30 751 100)) \<longrightarrow> 0 \<le> interpret_floatarith (hd g_arith_fas) [a, b] \<Longrightarrow> 0 \<le> interpret_floatarith (hd g_arith_fas) [a, b]
[PROOF STEP]
using a b
[PROOF STATE]
proof (prove)
using this:
0 \<le> a
a \<le> 824 / 10\<^sup>2
0 \<le> b
b \<le> 751 / 10\<^sup>2

goal (1 subgoal):
 1. (\<exists>x y. [a, b] = [x, y] \<and> 0 \<le> x \<and> x \<le> real_of_float (float_divr 30 824 100) \<and> 0 \<le> y \<and> y \<le> real_of_float (float_divr 30 751 100)) \<longrightarrow> 0 \<le> interpret_floatarith (hd g_arith_fas) [a, b] \<Longrightarrow> 0 \<le> interpret_floatarith (hd g_arith_fas) [a, b]
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 \<le> a; a * 25 \<le> 206; 0 \<le> b; b * 100 \<le> 751; \<not> 0 \<le> interpret_floatarith (hd g_arith_fas) [a, b]\<rbrakk> \<Longrightarrow> a \<le> real_of_float (float_divr 30 824 100)
 2. \<lbrakk>0 \<le> a; a * 25 \<le> 206; 0 \<le> b; b * 100 \<le> 751; \<not> 0 \<le> interpret_floatarith (hd g_arith_fas) [a, b]\<rbrakk> \<Longrightarrow> b \<le> real_of_float (float_divr 30 751 100)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> a; a * 25 \<le> 206; 0 \<le> b; b * 100 \<le> 751; \<not> 0 \<le> interpret_floatarith (hd g_arith_fas) [a, b]\<rbrakk> \<Longrightarrow> a \<le> real_of_float (float_divr 30 824 100)
[PROOF STEP]
by (rule order_trans[OF _ float_divr]) simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> a; a * 25 \<le> 206; 0 \<le> b; b * 100 \<le> 751; \<not> 0 \<le> interpret_floatarith (hd g_arith_fas) [a, b]\<rbrakk> \<Longrightarrow> b \<le> real_of_float (float_divr 30 751 100)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> a; a * 25 \<le> 206; 0 \<le> b; b * 100 \<le> 751; \<not> 0 \<le> interpret_floatarith (hd g_arith_fas) [a, b]\<rbrakk> \<Longrightarrow> b \<le> real_of_float (float_divr 30 751 100)
[PROOF STEP]
by (rule order_trans[OF _ float_divr]) simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
0 \<le> interpret_floatarith (hd g_arith_fas) [a, b]

goal (1 subgoal):
 1. 0 \<le> g_arith a b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 \<le> interpret_floatarith (hd g_arith_fas) [a, b]

goal (1 subgoal):
 1. 0 \<le> g_arith a b
[PROOF STEP]
have "\<dots> = g_arith a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (hd g_arith_fas) [a, b] = g_arith a b
[PROOF STEP]
by (auto simp: g_arith_fas_def g_arith_def p1_def p1d_def gx_def gy_def)
[PROOF STATE]
proof (state)
this:
interpret_floatarith (hd g_arith_fas) [a, b] = g_arith a b

goal (1 subgoal):
 1. 0 \<le> g_arith a b
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 \<le> g_arith a b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> g_arith a b

goal (1 subgoal):
 1. 0 \<le> g_arith a b
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
0 \<le> g_arith a b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trap_arithmetic:
  "p1d (a, b) (gx a b, gy a b) \<le> (- (27 / 25) - a\<^sup>2 + 2 * a * b) * p1 a b" if "(a, b) \<in> trapG1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p1d (a, b) (gx a b, gy a b) \<le> (- (27 / 25) - a\<^sup>2 + 2 * a * b) * p1 a b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p1d (a, b) (gx a b, gy a b) \<le> (- (27 / 25) - a\<^sup>2 + 2 * a * b) * p1 a b
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
(a, b) \<in> trapG1
[PROOF STEP]
have b: "0 \<le> b" "b \<le> 7.51"
    and a: "0 \<le> a" "a \<le> 8.24"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> trapG1

goal (1 subgoal):
 1. (0 \<le> b &&& b \<le> 751 / 10\<^sup>2) &&& 0 \<le> a &&& a \<le> 824 / 10\<^sup>2
[PROOF STEP]
by (auto simp: trapG1_def pos_quad_def)
[PROOF STATE]
proof (state)
this:
0 \<le> b
b \<le> 751 / 10\<^sup>2
0 \<le> a
a \<le> 824 / 10\<^sup>2

goal (1 subgoal):
 1. p1d (a, b) (gx a b, gy a b) \<le> (- (27 / 25) - a\<^sup>2 + 2 * a * b) * p1 a b
[PROOF STEP]
from g_arith_nonneg[OF a b]
[PROOF STATE]
proof (chain)
picking this:
0 \<le> g_arith a b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> g_arith a b

goal (1 subgoal):
 1. p1d (a, b) (gx a b, gy a b) \<le> (- (27 / 25) - a\<^sup>2 + 2 * a * b) * p1 a b
[PROOF STEP]
by (simp add: g_arith_def)
[PROOF STATE]
proof (state)
this:
p1d (a, b) (gx a b, gy a b) \<le> (- (27 / 25) - a\<^sup>2 + 2 * a * b) * p1 a b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma positively_invariant_trapG:
  shows "g.positively_invariant trapG"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g.positively_invariant trapG
[PROOF STEP]
unfolding trapG_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g.positively_invariant (trapG1 \<inter> {p. p1 (fst p) (snd p) \<le> 0})
[PROOF STEP]
apply (rule g.positively_invariant_le_domain[OF positively_invariant_trapG1 _ p1_has_derivative,
        of "\<lambda>p. -1.08 - (fst p)^2 + 2 * fst p * snd p"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. continuous_on trapG1 (\<lambda>p. - (108 / 10\<^sup>2) - (fst p)\<^sup>2 + 2 * fst p * snd p)
 2. \<And>s. s \<in> trapG1 \<Longrightarrow> p1d s (case s of (x, y) \<Rightarrow> (gx x y, gy x y)) \<le> (- (108 / 10\<^sup>2) - (fst s)\<^sup>2 + 2 * fst s * snd s) * p1 (fst s) (snd s)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on trapG1 (\<lambda>p. - (108 / 10\<^sup>2) - (fst p)\<^sup>2 + 2 * fst p * snd p)
[PROOF STEP]
by (auto intro!: continuous_intros derivative_eq_intros simp add: pos_quad_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> trapG1 \<Longrightarrow> p1d s (case s of (x, y) \<Rightarrow> (gx x y, gy x y)) \<le> (- (108 / 10\<^sup>2) - (fst s)\<^sup>2 + 2 * fst s * snd s) * p1 (fst s) (snd s)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> trapG1 \<Longrightarrow> p1d (a, b) (gx a b, gy a b) \<le> (- (27 / 25) - a\<^sup>2 + 2 * a * b) * p1 a b
[PROOF STEP]
by (rule trap_arithmetic)


[STATEMENT]
lemma regular_trapG:
  shows "0 \<notin> (\<lambda>(x, y). (gx x y, gy x y)) ` trapG"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<notin> (\<lambda>(x, y). (gx x y, gy x y)) ` trapG
[PROOF STEP]
unfolding trapG_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<notin> (\<lambda>(x, y). (gx x y, gy x y)) ` (trapG1 \<inter> {p. p1 (fst p) (snd p) \<le> 0})
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(gx a b, gy a b) = 0; (a, b) \<in> trapG1; p1 a b \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using p1_not_equil
[PROOF STATE]
proof (prove)
using this:
p1 ?x ?y \<le> 0 \<Longrightarrow> gx ?x ?y \<noteq> 0 \<or> gy ?x ?y \<noteq> 0

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(gx a b, gy a b) = 0; (a, b) \<in> trapG1; p1 a b \<le> 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by force


[STATEMENT]
lemma arith:
  "\<And>a b::real. 0 \<le> b \<Longrightarrow>
           0 \<le> a \<Longrightarrow>
           b * 100 \<le> 751 \<Longrightarrow>
           a * 25 + b * 25 \<le> 203 \<Longrightarrow> norm a + norm b \<le> 20"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>0 \<le> b; 0 \<le> a; b * 100 \<le> 751; a * 25 + b * 25 \<le> 203\<rbrakk> \<Longrightarrow> norm a + norm b \<le> 20
[PROOF STEP]
by auto


[STATEMENT]
lemma trapG1_subset:
  shows "trapG1 \<subseteq> cball (0::real \<times> real) 20"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trapG1 \<subseteq> cball 0 20
[PROOF STEP]
unfolding trapG1_def pos_quad_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {p. - snd p \<le> 0} \<inter> {p. - fst p \<le> 0} \<inter> ({p. snd p - 751 / 100 \<le> 0} \<inter> {p. fst p + snd p - 812 / 100 \<le> 0}) \<subseteq> cball 0 20
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>0 \<le> b; 0 \<le> a; b * 100 \<le> 751; a * 25 + b * 25 \<le> 203\<rbrakk> \<Longrightarrow> norm (a, b) \<le> 20
[PROOF STEP]
using arith norm_Pair_le
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<le> ?b; 0 \<le> ?a; ?b * 100 \<le> 751; ?a * 25 + ?b * 25 \<le> 203\<rbrakk> \<Longrightarrow> norm ?a + norm ?b \<le> 20
norm (?x, ?y) \<le> norm ?x + norm ?y

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>0 \<le> b; 0 \<le> a; b * 100 \<le> 751; a * 25 + b * 25 \<le> 203\<rbrakk> \<Longrightarrow> norm (a, b) \<le> 20
[PROOF STEP]
by smt


[STATEMENT]
lemma compact_subset_closed:
  assumes "compact S" "closed T"
  assumes "T \<subseteq> S"
  shows "compact T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compact T
[PROOF STEP]
using compact_Int_closed[OF assms(1-2)] assms(3)
[PROOF STATE]
proof (prove)
using this:
compact (S \<inter> T)
T \<subseteq> S

goal (1 subgoal):
 1. compact T
[PROOF STEP]
by (simp add: inf_absorb2)


[STATEMENT]
lemma compact_trapG1:
  shows "compact trapG1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compact trapG1
[PROOF STEP]
apply (auto intro!: compact_subset_closed[OF _ _ trapG1_subset])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed trapG1
[PROOF STEP]
unfolding trapG1_def pos_quad_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed ({p. - snd p \<le> 0} \<inter> {p. - fst p \<le> 0} \<inter> ({p. snd p - 751 / 100 \<le> 0} \<inter> {p. fst p + snd p - 812 / 100 \<le> 0}))
[PROOF STEP]
by (auto intro!: closed_Collect_le continuous_intros)


[STATEMENT]
lemma compact_trapG:
  shows "compact trapG"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compact trapG
[PROOF STEP]
unfolding trapG_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compact (trapG1 \<inter> {p. p1 (fst p) (snd p) \<le> 0})
[PROOF STEP]
by (auto intro!: compact_Int_closed compact_trapG1 closed_Collect_le continuous_intros simp add: p1_def)


[STATEMENT]
lemma x_in_trapG:
  shows "(1,0) \<in> trapG"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1, 0) \<in> trapG
[PROOF STEP]
unfolding trapG_def trapG1_def pos_quad_def p1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1, 0) \<in> {p. - snd p \<le> 0} \<inter> {p. - fst p \<le> 0} \<inter> ({p. snd p - 751 / 100 \<le> 0} \<inter> {p. fst p + snd p - 812 / 100 \<le> 0}) \<inter> {p. - (21 / 34) - 69 * fst p / 38 + 19 * (fst p)\<^sup>2 / 15 - 9 * fst p ^ 3 / 28 - 6 * fst p ^ 4 / 43 + 14 * snd p / 29 + 31 * fst p * snd p / 21 + 182 * (fst p)\<^sup>2 * snd p / 47 - 35 * fst p ^ 3 * snd p / 16 - 3 * (snd p)\<^sup>2 / 17 - 2 * fst p * (snd p)\<^sup>2 / 9 - 31 * (fst p)\<^sup>2 * (snd p)\<^sup>2 / 20 + snd p ^ 3 / 102 + fst p * snd p ^ 3 / 59 \<le> 0}
[PROOF STEP]
by (auto simp add: dist_Pair_Pair)


[STATEMENT]
lemma grev: "t \<in> {1/8 .. 1/8} \<longrightarrow> (x, y) \<in> {(1, 0) .. (1, 0)} \<longrightarrow>
   t \<in> g.rev.existence_ivl0 (x, y) \<and> g.rev.flow0 (x, y) t \<in>
    {(1.1, -0.09) .. (1.2, -0.08)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> point_ivl (1 / 8) \<longrightarrow> (x, y) \<in> point_ivl (1, 0) \<longrightarrow> t \<in> g.rev.existence_ivl0 (x, y) \<and> g.rev.flow0 (x, y) t \<in> {(11 / 10, - (9 / 10\<^sup>2))..(12 / 10, - (8 / 10\<^sup>2))}
[PROOF STEP]
by (tactic \<open>ode_bnds_tac @{thms g_fas_def} 30 20 7 12 [(0, 1, "0x000000")] (* "grev.out" *) "" @{context} 1\<close>)


[STATEMENT]
theorem g_has_limit_cycle:
  obtains y where "g.limit_cycle y" "range (g.flow0 y) \<subseteq> trapG"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>g.limit_cycle y; range (g.flow0 y) \<subseteq> trapG\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>g.limit_cycle y; range (g.flow0 y) \<subseteq> trapG\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define E::"(real*real) set" where "E = {(1.1, -0.09) .. (1.2, -0.08)}"
[PROOF STATE]
proof (state)
this:
E = {(11 / 10, - (9 / 10\<^sup>2))..(12 / 10, - (8 / 10\<^sup>2))}

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>g.limit_cycle y; range (g.flow0 y) \<subseteq> trapG\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from grev
[PROOF STATE]
proof (chain)
picking this:
?t \<in> point_ivl (1 / 8) \<longrightarrow> (?x, ?y) \<in> point_ivl (1, 0) \<longrightarrow> ?t \<in> g.rev.existence_ivl0 (?x, ?y) \<and> g.rev.flow0 (?x, ?y) ?t \<in> {(11 / 10, - (9 / 10\<^sup>2))..(12 / 10, - (8 / 10\<^sup>2))}
[PROOF STEP]
have "g.rev.flow0 (1, 0) (1/8) \<in> E"
[PROOF STATE]
proof (prove)
using this:
?t \<in> point_ivl (1 / 8) \<longrightarrow> (?x, ?y) \<in> point_ivl (1, 0) \<longrightarrow> ?t \<in> g.rev.existence_ivl0 (?x, ?y) \<and> g.rev.flow0 (?x, ?y) ?t \<in> {(11 / 10, - (9 / 10\<^sup>2))..(12 / 10, - (8 / 10\<^sup>2))}

goal (1 subgoal):
 1. g.rev.flow0 (1, 0) (1 / 8) \<in> E
[PROOF STEP]
by (auto simp: E_def)
[PROOF STATE]
proof (state)
this:
g.rev.flow0 (1, 0) (1 / 8) \<in> E

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>g.limit_cycle y; range (g.flow0 y) \<subseteq> trapG\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
g.rev.flow0 (1, 0) (1 / 8) \<in> E

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>g.limit_cycle y; range (g.flow0 y) \<subseteq> trapG\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "E \<inter> trapG = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E \<inter> trapG = {}
[PROOF STEP]
by (auto simp: trapG_def E_def trapG1_def pos_quad_def)
[PROOF STATE]
proof (state)
this:
E \<inter> trapG = {}

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>g.limit_cycle y; range (g.flow0 y) \<subseteq> trapG\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
g.rev.flow0 (1, 0) (1 / 8) \<in> E
E \<inter> trapG = {}
[PROOF STEP]
have "g.rev.flow0 (1, 0) (1 / 8) \<notin> trapG"
[PROOF STATE]
proof (prove)
using this:
g.rev.flow0 (1, 0) (1 / 8) \<in> E
E \<inter> trapG = {}

goal (1 subgoal):
 1. g.rev.flow0 (1, 0) (1 / 8) \<notin> trapG
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
g.rev.flow0 (1, 0) (1 / 8) \<notin> trapG

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>g.limit_cycle y; range (g.flow0 y) \<subseteq> trapG\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from g.poincare_bendixson_limit_cycle[OF compact_trapG subset_UNIV x_in_trapG positively_invariant_trapG regular_trapG this] that
[PROOF STATE]
proof (chain)
picking this:
(\<And>y. \<lbrakk>g.limit_cycle y; range (g.flow0 y) \<subseteq> trapG\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
\<lbrakk>g.limit_cycle ?y1; range (g.flow0 ?y1) \<subseteq> trapG\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<And>y. \<lbrakk>g.limit_cycle y; range (g.flow0 y) \<subseteq> trapG\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
\<lbrakk>g.limit_cycle ?y1; range (g.flow0 ?y1) \<subseteq> trapG\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed