[STATEMENT]
lemma lossless_inline[rotated]:
  fixes gpv :: "('a, 'call, 'ret) gpv"
  assumes gpv: "lossless_gpv \<I> gpv" "\<I> \<turnstile>g gpv \<surd>"
  and lossless: "\<And>s x. x \<in> outs_\<I> \<I> \<Longrightarrow> lossless_gpv \<I>' (callee s x)"
  shows "lossless_gpv \<I>' (inline callee gpv s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_gpv \<I>' (inline callee gpv s)
[PROOF STEP]
using gpv
[PROOF STATE]
proof (prove)
using this:
lossless_gpv \<I> gpv
\<I> \<turnstile>g gpv \<surd>

goal (1 subgoal):
 1. lossless_gpv \<I>' (inline callee gpv s)
[PROOF STEP]
proof(induction arbitrary: s rule: lossless_WT_gpv_induct_strong)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
case (lossless_gpv p)
[PROOF STATE]
proof (state)
this:
lossless_spmf p
IO ?out ?c \<in> set_spmf p \<Longrightarrow> ?out \<in> outs_\<I> \<I>
?gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> ?gpv
?gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g ?gpv \<surd>
?gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee ?gpv ?s)

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
have lp: "lossless_gpv \<I> (GPV p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_gpv \<I> (GPV p)
[PROOF STEP]
by(rule lossless_sub_gpvsI)(auto intro: lossless_gpv.hyps)
[PROOF STATE]
proof (state)
this:
lossless_gpv \<I> (GPV p)

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lossless_gpv \<I> (GPV p)

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
have wp: "\<I> \<turnstile>g GPV p \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I> \<turnstile>g GPV p \<surd>
[PROOF STEP]
by(rule WT_sub_gpvsI)(auto intro: lossless_gpv.hyps)
[PROOF STATE]
proof (state)
this:
\<I> \<turnstile>g GPV p \<surd>

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lossless_gpv \<I> (GPV p)
\<I> \<turnstile>g GPV p \<surd>
[PROOF STEP]
have "lossless_spmf (the_gpv (inline callee (GPV p) s))"
[PROOF STATE]
proof (prove)
using this:
lossless_gpv \<I> (GPV p)
\<I> \<turnstile>g GPV p \<surd>

goal (1 subgoal):
 1. lossless_spmf (the_gpv (inline callee (GPV p) s))
[PROOF STEP]
by(auto simp add: inline_sel intro: lossless_spmf_inline1 lossless_gpv_lossless_spmfD[OF lossless])
[PROOF STATE]
proof (state)
this:
lossless_spmf (the_gpv (inline callee (GPV p) s))

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lossless_spmf (the_gpv (inline callee (GPV p) s))

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
lossless_spmf (the_gpv (inline callee (GPV p) s))

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
fix out c input
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
assume IO: "IO out c \<in> set_spmf (the_gpv (inline callee (GPV p) s))"
      and "input \<in> responses_\<I> \<I>' out"
[PROOF STATE]
proof (state)
this:
IO out c \<in> set_spmf (the_gpv (inline callee (GPV p) s))
input \<in> responses_\<I> \<I>' out

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
from IO
[PROOF STATE]
proof (chain)
picking this:
IO out c \<in> set_spmf (the_gpv (inline callee (GPV p) s))
[PROOF STEP]
obtain callee' rpv
      where Inr: "Inr (out, callee', rpv) \<in> set_spmf (inline1 callee (GPV p) s)"
      and c: "c = (\<lambda>input. callee' input \<bind> (\<lambda>(x, y). inline callee (rpv x) y))"
[PROOF STATE]
proof (prove)
using this:
IO out c \<in> set_spmf (the_gpv (inline callee (GPV p) s))

goal (1 subgoal):
 1. (\<And>callee' rpv. \<lbrakk>Inr (out, callee', rpv) \<in> set_spmf (inline1 callee (GPV p) s); c = (\<lambda>input. callee' input \<bind> (\<lambda>(x, y). inline callee (rpv x) y))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(clarsimp simp add: inline_sel split: sum.split_asm)
[PROOF STATE]
proof (state)
this:
Inr (out, callee', rpv) \<in> set_spmf (inline1 callee (GPV p) s)
c = (\<lambda>input. callee' input \<bind> (\<lambda>(x, y). inline callee (rpv x) y))

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
from Inr \<open>input \<in> _\<close> lossless lp wp
[PROOF STATE]
proof (chain)
picking this:
Inr (out, callee', rpv) \<in> set_spmf (inline1 callee (GPV p) s)
input \<in> responses_\<I> \<I>' out
?x \<in> outs_\<I> \<I> \<Longrightarrow> lossless_gpv \<I>' (callee ?s ?x)
lossless_gpv \<I> (GPV p)
\<I> \<turnstile>g GPV p \<surd>
[PROOF STEP]
have "lossless_gpv \<I>' (callee' input)"
[PROOF STATE]
proof (prove)
using this:
Inr (out, callee', rpv) \<in> set_spmf (inline1 callee (GPV p) s)
input \<in> responses_\<I> \<I>' out
?x \<in> outs_\<I> \<I> \<Longrightarrow> lossless_gpv \<I>' (callee ?s ?x)
lossless_gpv \<I> (GPV p)
\<I> \<turnstile>g GPV p \<surd>

goal (1 subgoal):
 1. lossless_gpv \<I>' (callee' input)
[PROOF STEP]
by(rule lossless_inline1)
[PROOF STATE]
proof (state)
this:
lossless_gpv \<I>' (callee' input)

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lossless_gpv \<I>' (callee' input)

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
lossless_gpv \<I>' (callee' input)

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
fix x s'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
assume "(x, s') \<in> results_gpv \<I>' (callee' input)"
[PROOF STATE]
proof (state)
this:
(x, s') \<in> results_gpv \<I>' (callee' input)

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
with Inr
[PROOF STATE]
proof (chain)
picking this:
Inr (out, callee', rpv) \<in> set_spmf (inline1 callee (GPV p) s)
(x, s') \<in> results_gpv \<I>' (callee' input)
[PROOF STEP]
have "rpv x \<in> sub_gpvs \<I> (GPV p)"
[PROOF STATE]
proof (prove)
using this:
Inr (out, callee', rpv) \<in> set_spmf (inline1 callee (GPV p) s)
(x, s') \<in> results_gpv \<I>' (callee' input)

goal (1 subgoal):
 1. rpv x \<in> sub_gpvs \<I> (GPV p)
[PROOF STEP]
using \<open>input \<in> _\<close> wp
[PROOF STATE]
proof (prove)
using this:
Inr (out, callee', rpv) \<in> set_spmf (inline1 callee (GPV p) s)
(x, s') \<in> results_gpv \<I>' (callee' input)
input \<in> responses_\<I> \<I>' out
\<I> \<turnstile>g GPV p \<surd>

goal (1 subgoal):
 1. rpv x \<in> sub_gpvs \<I> (GPV p)
[PROOF STEP]
by(rule inline1_in_sub_gpvs)
[PROOF STATE]
proof (state)
this:
rpv x \<in> sub_gpvs \<I> (GPV p)

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
hence "lossless_gpv \<I>' (inline callee (rpv x) s')"
[PROOF STATE]
proof (prove)
using this:
rpv x \<in> sub_gpvs \<I> (GPV p)

goal (1 subgoal):
 1. lossless_gpv \<I>' (inline callee (rpv x) s')
[PROOF STEP]
by(rule lossless_gpv.IH)
[PROOF STATE]
proof (state)
this:
lossless_gpv \<I>' (inline callee (rpv x) s')

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?x2, ?s'2) \<in> results_gpv \<I>' (callee' input) \<Longrightarrow> lossless_gpv \<I>' (inline callee (rpv ?x2) ?s'2)

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lossless_gpv \<I>' (callee' input)
(?x2, ?s'2) \<in> results_gpv \<I>' (callee' input) \<Longrightarrow> lossless_gpv \<I>' (inline callee (rpv ?x2) ?s'2)
[PROOF STEP]
have "lossless_gpv \<I>' (c input)"
[PROOF STATE]
proof (prove)
using this:
lossless_gpv \<I>' (callee' input)
(?x2, ?s'2) \<in> results_gpv \<I>' (callee' input) \<Longrightarrow> lossless_gpv \<I>' (inline callee (rpv ?x2) ?s'2)

goal (1 subgoal):
 1. lossless_gpv \<I>' (c input)
[PROOF STEP]
unfolding c
[PROOF STATE]
proof (prove)
using this:
lossless_gpv \<I>' (callee' input)
(?x2, ?s'2) \<in> results_gpv \<I>' (callee' input) \<Longrightarrow> lossless_gpv \<I>' (inline callee (rpv ?x2) ?s'2)

goal (1 subgoal):
 1. lossless_gpv \<I>' (callee' input \<bind> (\<lambda>(x, y). inline callee (rpv x) y))
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
lossless_gpv \<I>' (c input)

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>IO ?out2 ?c2 \<in> set_spmf (the_gpv (inline callee (GPV p) s)); ?input2 \<in> responses_\<I> \<I>' ?out2\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (?c2 ?input2)

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lossless_spmf (the_gpv (inline callee (GPV p) s))
\<lbrakk>IO ?out2 ?c2 \<in> set_spmf (the_gpv (inline callee (GPV p) s)); ?input2 \<in> responses_\<I> \<I>' ?out2\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (?c2 ?input2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
lossless_spmf (the_gpv (inline callee (GPV p) s))
\<lbrakk>IO ?out2 ?c2 \<in> set_spmf (the_gpv (inline callee (GPV p) s)); ?input2 \<in> responses_\<I> \<I>' ?out2\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (?c2 ?input2)

goal (1 subgoal):
 1. lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
by(rule lossless_gpvI)
[PROOF STATE]
proof (state)
this:
lossless_gpv \<I>' (inline callee (GPV p) s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma outs'_restrict_gpv: "outs'_gpv (restrict_gpv gpv) \<subseteq> outs_\<I> \<I>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. outs'_gpv (local.restrict_gpv gpv) \<subseteq> outs_\<I> \<I>
[PROOF STEP]
by(blast intro: in_outs'_restrict_gpvD)


[STATEMENT]
lemma subgraph_subset:
  assumes "subgraph G\<^sub>1 G\<^sub>2"
  shows "vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2" "edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2 &&& edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2
 2. edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2
[PROOF STEP]
have vrt:"Id_on (vertices G\<^sub>1) `` vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2"
    and ep:"edge_preserving (Id_on (vertices G\<^sub>1)) (edges G\<^sub>1) (edges G\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Id_on (vertices G\<^sub>1) `` vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2 &&& edge_preserving (Id_on (vertices G\<^sub>1)) (edges G\<^sub>1) (edges G\<^sub>2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
subgraph G\<^sub>1 G\<^sub>2

goal (1 subgoal):
 1. Id_on (vertices G\<^sub>1) `` vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2 &&& edge_preserving (Id_on (vertices G\<^sub>1)) (edges G\<^sub>1) (edges G\<^sub>2)
[PROOF STEP]
unfolding graph_homomorphism_def
[PROOF STATE]
proof (prove)
using this:
vertices G\<^sub>1 = Domain (Id_on (vertices G\<^sub>1)) \<and> graph G\<^sub>1 \<and> graph G\<^sub>2 \<and> Id_on (vertices G\<^sub>1) `` vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2 \<and> univalent (Id_on (vertices G\<^sub>1)) \<and> edge_preserving (Id_on (vertices G\<^sub>1)) (edges G\<^sub>1) (edges G\<^sub>2)

goal (1 subgoal):
 1. Id_on (vertices G\<^sub>1) `` vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2 &&& edge_preserving (Id_on (vertices G\<^sub>1)) (edges G\<^sub>1) (edges G\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Id_on (vertices G\<^sub>1) `` vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2
edge_preserving (Id_on (vertices G\<^sub>1)) (edges G\<^sub>1) (edges G\<^sub>2)

goal (2 subgoals):
 1. vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2
 2. edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2
[PROOF STEP]
hence "edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
Id_on (vertices G\<^sub>1) `` vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2
edge_preserving (Id_on (vertices G\<^sub>1)) (edges G\<^sub>1) (edges G\<^sub>2)

goal (1 subgoal):
 1. edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Id_on (vertices G\<^sub>1) `` vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2
edge_preserving (Id_on (vertices G\<^sub>1)) (edges G\<^sub>1) (edges G\<^sub>2)
subgraph G\<^sub>1 G\<^sub>2

goal (1 subgoal):
 1. edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2
[PROOF STEP]
unfolding edge_preserving
[PROOF STATE]
proof (prove)
using this:
Id_on (vertices G\<^sub>1) `` vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2
on_triple (Id_on (vertices G\<^sub>1)) `` edges G\<^sub>1 \<subseteq> edges G\<^sub>2
subgraph G\<^sub>1 G\<^sub>2

goal (1 subgoal):
 1. edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2

goal (2 subgoals):
 1. vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2
 2. edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2
[PROOF STEP]
thus "vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2" "edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2

goal (1 subgoal):
 1. vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2 &&& edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2
[PROOF STEP]
using vrt
[PROOF STATE]
proof (prove)
using this:
edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2
Id_on (vertices G\<^sub>1) `` vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2

goal (1 subgoal):
 1. vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2 &&& edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vertices G\<^sub>1 \<subseteq> vertices G\<^sub>2
edges (restrict G\<^sub>1) \<subseteq> edges G\<^sub>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma disj_four_cases:
  assumes "A \<or> B \<or> C \<or> D" and "A \<Longrightarrow> P" and "B \<Longrightarrow> P" and "C \<Longrightarrow> P" and "D \<Longrightarrow> P"
  shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<or> B \<or> C \<or> D
A \<Longrightarrow> P
B \<Longrightarrow> P
C \<Longrightarrow> P
D \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
by auto


[STATEMENT]
lemma vrat_fpair_in_fproduct_vrat: "[a\<^sub>\<rat>, b\<^sub>\<rat>]\<^sub>\<circ> \<in>\<^sub>\<circ> \<rat>\<^sub>\<circ> ^\<^sub>\<times> 2\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a\<^sub>\<rat>, b\<^sub>\<rat>]\<^sub>\<circ> \<in>\<^sub>\<circ> \<rat>\<^sub>\<circ> ^\<^sub>\<times> 2\<^sub>\<nat>
[PROOF STEP]
by force


[STATEMENT]
lemma (in Category) IsoCompDef:
  assumes 1: "f \<approx>> g" and 2: "ciso f" and 3: "ciso g"
  shows "(Cinv g) \<approx>> (Cinv f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cinv g \<approx>> Cinv f
[PROOF STEP]
proof(rule CompDefinedI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. Cinv g \<in> mor
 2. Cinv f \<in> mor
 3. cod Cinv g = dom Cinv f
[PROOF STEP]
show "Cinv g \<in> mor" and "Cinv f \<in> mor"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cinv g \<in> mor &&& Cinv f \<in> mor
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f \<approx>> g
ciso f
ciso g

goal (1 subgoal):
 1. Cinv g \<in> mor &&& Cinv f \<in> mor
[PROOF STEP]
by (auto simp add: InvDomCod)
[PROOF STATE]
proof (state)
this:
Cinv g \<in> mor
Cinv f \<in> mor

goal (1 subgoal):
 1. cod Cinv g = dom Cinv f
[PROOF STEP]
have "cod (Cinv g) = dom g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cod Cinv g = dom g
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
ciso g

goal (1 subgoal):
 1. cod Cinv g = dom g
[PROOF STEP]
by (simp add: InvDomCod)
[PROOF STATE]
proof (state)
this:
cod Cinv g = dom g

goal (1 subgoal):
 1. cod Cinv g = dom Cinv f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cod Cinv g = dom g

goal (1 subgoal):
 1. cod Cinv g = dom Cinv f
[PROOF STEP]
have "... = cod f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom g = cod f
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
f \<approx>> g

goal (1 subgoal):
 1. dom g = cod f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dom g = cod f

goal (1 subgoal):
 1. cod Cinv g = dom Cinv f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dom g = cod f

goal (1 subgoal):
 1. cod Cinv g = dom Cinv f
[PROOF STEP]
have "... = dom (Cinv f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cod f = dom Cinv f
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
ciso f

goal (1 subgoal):
 1. cod f = dom Cinv f
[PROOF STEP]
by (simp add: InvDomCod)
[PROOF STATE]
proof (state)
this:
cod f = dom Cinv f

goal (1 subgoal):
 1. cod Cinv g = dom Cinv f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cod Cinv g = dom Cinv f
[PROOF STEP]
show "cod (Cinv g) = dom (Cinv f)"
[PROOF STATE]
proof (prove)
using this:
cod Cinv g = dom Cinv f

goal (1 subgoal):
 1. cod Cinv g = dom Cinv f
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cod Cinv g = dom Cinv f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pmdl_closed_red:
  assumes "pmdl B \<subseteq> pmdl A" and "p \<in> pmdl A" and "red B p q"
  shows "q \<in> pmdl A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> pmdl A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q \<in> pmdl A
[PROOF STEP]
have "q - p \<in> pmdl A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q - p \<in> pmdl A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. q - p \<in> ?A
 2. ?A \<subseteq> pmdl A
[PROOF STEP]
have "p - q \<in> pmdl B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p - q \<in> pmdl B
[PROOF STEP]
by (rule red_diff_in_pmdl, fact)
[PROOF STATE]
proof (state)
this:
p - q \<in> pmdl B

goal (2 subgoals):
 1. q - p \<in> ?A
 2. ?A \<subseteq> pmdl A
[PROOF STEP]
hence "- (p - q) \<in> pmdl B"
[PROOF STATE]
proof (prove)
using this:
p - q \<in> pmdl B

goal (1 subgoal):
 1. - (p - q) \<in> pmdl B
[PROOF STEP]
by (rule pmdl.span_neg)
[PROOF STATE]
proof (state)
this:
- (p - q) \<in> pmdl B

goal (2 subgoals):
 1. q - p \<in> ?A
 2. ?A \<subseteq> pmdl A
[PROOF STEP]
thus "q - p \<in> pmdl B"
[PROOF STATE]
proof (prove)
using this:
- (p - q) \<in> pmdl B

goal (1 subgoal):
 1. q - p \<in> pmdl B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
q - p \<in> pmdl B

goal (1 subgoal):
 1. pmdl B \<subseteq> pmdl A
[PROOF STEP]
qed fact
[PROOF STATE]
proof (state)
this:
q - p \<in> pmdl A

goal (1 subgoal):
 1. q \<in> pmdl A
[PROOF STEP]
from pmdl.span_add[OF this \<open>p \<in> pmdl A\<close>]
[PROOF STATE]
proof (chain)
picking this:
q - p + p \<in> pmdl A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
q - p + p \<in> pmdl A

goal (1 subgoal):
 1. q \<in> pmdl A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
q \<in> pmdl A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fin_steps_plusI:
 "[| (start A,q) : steps A u; u \<noteq> []; fin A p |]
 ==> (p,q) : steps (plus A) u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(start A, q) \<in> steps A u; u \<noteq> []; fin A p\<rbrakk> \<Longrightarrow> (p, q) \<in> steps (RegExp2NA.plus A) u
[PROOF STEP]
apply (case_tac "u")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(start A, q) \<in> steps A u; u \<noteq> []; fin A p; u = []\<rbrakk> \<Longrightarrow> (p, q) \<in> steps (RegExp2NA.plus A) u
 2. \<And>a list. \<lbrakk>(start A, q) \<in> steps A u; u \<noteq> []; fin A p; u = a # list\<rbrakk> \<Longrightarrow> (p, q) \<in> steps (RegExp2NA.plus A) u
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>(start A, q) \<in> steps A u; u \<noteq> []; fin A p; u = a # list\<rbrakk> \<Longrightarrow> (p, q) \<in> steps (RegExp2NA.plus A) u
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>(start A, q) \<in> step A a O steps A list; fin A p; u = a # list\<rbrakk> \<Longrightarrow> (p, q) \<in> step (RegExp2NA.plus A) a O steps (RegExp2NA.plus A) list
[PROOF STEP]
apply (blast intro: steps_plusI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma steps_star_cycle[rule_format]:
 "us \<noteq> [] \<longrightarrow> (\<forall>u \<in> set us. accepts A u) \<longrightarrow> accepts (plus A) (concat us)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. us \<noteq> [] \<longrightarrow> (\<forall>u\<in>set us. accepts A u) \<longrightarrow> accepts (RegExp2NA.plus A) (concat us)
[PROOF STEP]
apply (simp add: accepts_conv_steps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. us \<noteq> [] \<longrightarrow> (\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) \<and> fin A q)
[PROOF STEP]
apply (induct us rule: rev_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. [] \<noteq> [] \<longrightarrow> (\<forall>u\<in>set []. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat []) \<and> fin A q)
 2. \<And>x xs. xs \<noteq> [] \<longrightarrow> (\<forall>u\<in>set xs. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat xs) \<and> fin A q) \<Longrightarrow> xs @ [x] \<noteq> [] \<longrightarrow> (\<forall>u\<in>set (xs @ [x]). \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat (xs @ [x])) \<and> fin A q)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs. xs \<noteq> [] \<longrightarrow> (\<forall>u\<in>set xs. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat xs) \<and> fin A q) \<Longrightarrow> xs @ [x] \<noteq> [] \<longrightarrow> (\<forall>u\<in>set (xs @ [x]). \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat (xs @ [x])) \<and> fin A q)
[PROOF STEP]
apply (rename_tac u us)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u us. us \<noteq> [] \<longrightarrow> (\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) \<and> fin A q) \<Longrightarrow> us @ [u] \<noteq> [] \<longrightarrow> (\<forall>u\<in>set (us @ [u]). \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat (us @ [u])) \<and> fin A q)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u us. us \<noteq> [] \<longrightarrow> (\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) \<and> fin A q) \<Longrightarrow> (\<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<and> (\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) O steps (RegExp2NA.plus A) u \<and> fin A q)
[PROOF STEP]
apply (clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u us q. \<lbrakk>us \<noteq> [] \<longrightarrow> (\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) \<and> fin A q); \<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q; (start A, q) \<in> steps A u; fin A q\<rbrakk> \<Longrightarrow> \<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) O steps (RegExp2NA.plus A) u \<and> fin A q
[PROOF STEP]
apply (case_tac "us = []")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>u us q. \<lbrakk>us \<noteq> [] \<longrightarrow> (\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) \<and> fin A q); \<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q; (start A, q) \<in> steps A u; fin A q; us = []\<rbrakk> \<Longrightarrow> \<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) O steps (RegExp2NA.plus A) u \<and> fin A q
 2. \<And>u us q. \<lbrakk>us \<noteq> [] \<longrightarrow> (\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) \<and> fin A q); \<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q; (start A, q) \<in> steps A u; fin A q; us \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) O steps (RegExp2NA.plus A) u \<and> fin A q
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>u us q. \<lbrakk>(start A, q) \<in> steps A u; fin A q; us = []\<rbrakk> \<Longrightarrow> \<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) u \<and> fin A q
 2. \<And>u us q. \<lbrakk>us \<noteq> [] \<longrightarrow> (\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) \<and> fin A q); \<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q; (start A, q) \<in> steps A u; fin A q; us \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) O steps (RegExp2NA.plus A) u \<and> fin A q
[PROOF STEP]
apply (blast intro: steps_plusI fin_steps_plusI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u us q. \<lbrakk>us \<noteq> [] \<longrightarrow> (\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q) \<longrightarrow> (\<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) \<and> fin A q); \<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q; (start A, q) \<in> steps A u; fin A q; us \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) O steps (RegExp2NA.plus A) u \<and> fin A q
[PROOF STEP]
apply (clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u us q qa. \<lbrakk>\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q; (start A, q) \<in> steps A u; fin A q; us \<noteq> []; (start A, qa) \<in> steps (RegExp2NA.plus A) (concat us); fin A qa\<rbrakk> \<Longrightarrow> \<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) O steps (RegExp2NA.plus A) u \<and> fin A q
[PROOF STEP]
apply (case_tac "u = []")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>u us q qa. \<lbrakk>\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q; (start A, q) \<in> steps A u; fin A q; us \<noteq> []; (start A, qa) \<in> steps (RegExp2NA.plus A) (concat us); fin A qa; u = []\<rbrakk> \<Longrightarrow> \<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) O steps (RegExp2NA.plus A) u \<and> fin A q
 2. \<And>u us q qa. \<lbrakk>\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q; (start A, q) \<in> steps A u; fin A q; us \<noteq> []; (start A, qa) \<in> steps (RegExp2NA.plus A) (concat us); fin A qa; u \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) O steps (RegExp2NA.plus A) u \<and> fin A q
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>u us q qa. \<lbrakk>\<forall>u\<in>set us. \<exists>qa. (q, qa) \<in> steps A u \<and> fin A qa; start A = q; fin A q; us \<noteq> []; (q, qa) \<in> steps (RegExp2NA.plus A) (concat us); fin A qa; u = []\<rbrakk> \<Longrightarrow> \<exists>qa. (q, qa) \<in> steps (RegExp2NA.plus A) (concat us) \<and> fin A qa
 2. \<And>u us q qa. \<lbrakk>\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q; (start A, q) \<in> steps A u; fin A q; us \<noteq> []; (start A, qa) \<in> steps (RegExp2NA.plus A) (concat us); fin A qa; u \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) O steps (RegExp2NA.plus A) u \<and> fin A q
[PROOF STEP]
apply (blast intro: steps_plusI fin_steps_plusI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u us q qa. \<lbrakk>\<forall>u\<in>set us. \<exists>q. (start A, q) \<in> steps A u \<and> fin A q; (start A, q) \<in> steps A u; fin A q; us \<noteq> []; (start A, qa) \<in> steps (RegExp2NA.plus A) (concat us); fin A qa; u \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>q. (start A, q) \<in> steps (RegExp2NA.plus A) (concat us) O steps (RegExp2NA.plus A) u \<and> fin A q
[PROOF STEP]
apply (blast intro: steps_plusI fin_steps_plusI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma proj_poly_syz_eq_zero_iff: "proj_poly_syz n p = 0 \<longleftrightarrow> (component_of_term ` keys p \<subseteq> {0..<n})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (proj_poly_syz n p = 0) = (component_of_term ` keys p \<subseteq> {0..<n})
[PROOF STEP]
unfolding keys_eq_empty[symmetric] keys_proj_poly_syz
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (map_component (\<lambda>k. k + n) -` keys p = {}) = (component_of_term ` keys p \<subseteq> {0..<n})
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. map_component (\<lambda>k. k + n) -` keys p = {} \<Longrightarrow> component_of_term ` keys p \<subseteq> {0..<n}
 2. component_of_term ` keys p \<subseteq> {0..<n} \<Longrightarrow> map_component (\<lambda>k. k + n) -` keys p = {}
[PROOF STEP]
assume "map_component (\<lambda>k. k + n) -` keys p = {}" (is "?A = {}")
[PROOF STATE]
proof (state)
this:
map_component (\<lambda>k. k + n) -` keys p = {}

goal (2 subgoals):
 1. map_component (\<lambda>k. k + n) -` keys p = {} \<Longrightarrow> component_of_term ` keys p \<subseteq> {0..<n}
 2. component_of_term ` keys p \<subseteq> {0..<n} \<Longrightarrow> map_component (\<lambda>k. k + n) -` keys p = {}
[PROOF STEP]
show "component_of_term ` keys p \<subseteq> {0..<n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. component_of_term ` keys p \<subseteq> {0..<n}
[PROOF STEP]
proof (rule, rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> component_of_term ` keys p; x \<notin> {0..<n}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> component_of_term ` keys p; x \<notin> {0..<n}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "i \<in> component_of_term ` keys p"
[PROOF STATE]
proof (state)
this:
i \<in> component_of_term ` keys p

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> component_of_term ` keys p; x \<notin> {0..<n}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in> component_of_term ` keys p
[PROOF STEP]
obtain x where x: "x \<in> keys p" and i: "i = component_of_term x"
[PROOF STATE]
proof (prove)
using this:
i \<in> component_of_term ` keys p

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> keys p; i = component_of_term x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
x \<in> keys p
i = component_of_term x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> component_of_term ` keys p; x \<notin> {0..<n}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "i \<notin> {0..<n}"
[PROOF STATE]
proof (state)
this:
i \<notin> {0..<n}

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> component_of_term ` keys p; x \<notin> {0..<n}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "i - n + n = i"
[PROOF STATE]
proof (prove)
using this:
i \<notin> {0..<n}

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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> component_of_term ` keys p; x \<notin> {0..<n}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence 1: "map_component (\<lambda>k. k - n + n) x = x"
[PROOF STATE]
proof (prove)
using this:
i - n + n = i

goal (1 subgoal):
 1. map_component (\<lambda>k. k - n + n) x = x
[PROOF STEP]
by (simp add: map_component_def i term_simps)
[PROOF STATE]
proof (state)
this:
map_component (\<lambda>k. k - n + n) x = x

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> component_of_term ` keys p; x \<notin> {0..<n}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "map_component (\<lambda>k. k - n) x \<in> ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_component (\<lambda>k. k - n) x \<in> map_component (\<lambda>k. k + n) -` keys p
[PROOF STEP]
by (rule vimageI2, simp add: map_component_comp x 1)
[PROOF STATE]
proof (state)
this:
map_component (\<lambda>k. k - n) x \<in> map_component (\<lambda>k. k + n) -` keys p

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> component_of_term ` keys p; x \<notin> {0..<n}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
map_component (\<lambda>k. k - n) x \<in> map_component (\<lambda>k. k + n) -` keys p

goal (1 subgoal):
 1. False
[PROOF STEP]
by (simp add: \<open>?A = {}\<close>)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
component_of_term ` keys p \<subseteq> {0..<n}

goal (1 subgoal):
 1. component_of_term ` keys p \<subseteq> {0..<n} \<Longrightarrow> map_component (\<lambda>k. k + n) -` keys p = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. component_of_term ` keys p \<subseteq> {0..<n} \<Longrightarrow> map_component (\<lambda>k. k + n) -` keys p = {}
[PROOF STEP]
assume a: "component_of_term ` keys p \<subseteq> {0..<n}"
[PROOF STATE]
proof (state)
this:
component_of_term ` keys p \<subseteq> {0..<n}

goal (1 subgoal):
 1. component_of_term ` keys p \<subseteq> {0..<n} \<Longrightarrow> map_component (\<lambda>k. k + n) -` keys p = {}
[PROOF STEP]
show "map_component (\<lambda>k. k + n) -` keys p = {}" (is "?A = {}")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_component (\<lambda>k. k + n) -` keys p = {}
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map_component (\<lambda>k. k + n) -` keys p \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
assume "?A \<noteq> {}"
[PROOF STATE]
proof (state)
this:
map_component (\<lambda>k. k + n) -` keys p \<noteq> {}

goal (1 subgoal):
 1. map_component (\<lambda>k. k + n) -` keys p \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
map_component (\<lambda>k. k + n) -` keys p \<noteq> {}
[PROOF STEP]
obtain x where "x \<in> ?A"
[PROOF STATE]
proof (prove)
using this:
map_component (\<lambda>k. k + n) -` keys p \<noteq> {}

goal (1 subgoal):
 1. (\<And>x. x \<in> map_component (\<lambda>k. k + n) -` keys p \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> map_component (\<lambda>k. k + n) -` keys p

goal (1 subgoal):
 1. map_component (\<lambda>k. k + n) -` keys p \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
hence "map_component (\<lambda>k. k + n) x \<in> keys p"
[PROOF STATE]
proof (prove)
using this:
x \<in> map_component (\<lambda>k. k + n) -` keys p

goal (1 subgoal):
 1. map_component (\<lambda>k. k + n) x \<in> keys p
[PROOF STEP]
by (rule vimageD)
[PROOF STATE]
proof (state)
this:
map_component (\<lambda>k. k + n) x \<in> keys p

goal (1 subgoal):
 1. map_component (\<lambda>k. k + n) -` keys p \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
with a
[PROOF STATE]
proof (chain)
picking this:
component_of_term ` keys p \<subseteq> {0..<n}
map_component (\<lambda>k. k + n) x \<in> keys p
[PROOF STEP]
have "component_of_term (map_component (\<lambda>k. k + n) x) \<in> {0..<n}"
[PROOF STATE]
proof (prove)
using this:
component_of_term ` keys p \<subseteq> {0..<n}
map_component (\<lambda>k. k + n) x \<in> keys p

goal (1 subgoal):
 1. component_of_term (map_component (\<lambda>k. k + n) x) \<in> {0..<n}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
component_of_term (map_component (\<lambda>k. k + n) x) \<in> {0..<n}

goal (1 subgoal):
 1. map_component (\<lambda>k. k + n) -` keys p \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
component_of_term (map_component (\<lambda>k. k + n) x) \<in> {0..<n}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
map_component (\<lambda>k. k + n) -` keys p = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma to_int_of_int: "to_int (of_int x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_int (of_int x) = x
[PROOF STEP]
by (metis int_of_rat(1) of_rat_of_int_eq to_int_def to_rat_of_rat)


[STATEMENT]
lemma int_tree_none: "emp \<Longrightarrow>\<^sub>A int_tree interval_tree.Tip None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emp \<Longrightarrow>\<^sub>A int_tree Tip None
[PROOF STEP]
by auto2


[STATEMENT]
theorem (in v0_v1_Digraph) menger_trivial:
  assumes "DisjointPaths G v0 v1 paths" "card paths = n"
  shows "\<And>S. Separation G v0 v1 S \<Longrightarrow> card S \<ge> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S. Separation G v0 v1 S \<Longrightarrow> n \<le> card S
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S. Separation G v0 v1 S \<Longrightarrow> n \<le> card S
[PROOF STEP]
interpret DisjointPaths G v0 v1 paths
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DisjointPaths G v0 v1 paths
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
DisjointPaths G v0 v1 paths

goal (1 subgoal):
 1. DisjointPaths G v0 v1 paths
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S. Separation G v0 v1 S \<Longrightarrow> n \<le> card S
[PROOF STEP]
fix S
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S. Separation G v0 v1 S \<Longrightarrow> n \<le> card S
[PROOF STEP]
assume "Separation G v0 v1 S"
[PROOF STATE]
proof (state)
this:
Separation G v0 v1 S

goal (1 subgoal):
 1. \<And>S. Separation G v0 v1 S \<Longrightarrow> n \<le> card S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Separation G v0 v1 S
[PROOF STEP]
interpret S: Separation G v0 v1 S
[PROOF STATE]
proof (prove)
using this:
Separation G v0 v1 S

goal (1 subgoal):
 1. Separation G v0 v1 S
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S. Separation G v0 v1 S \<Longrightarrow> n \<le> card S
[PROOF STEP]
text \<open>
    Our plan is to show @{term "card S \<ge> n"} by defining an injective function from @{term paths}
    into @{term S}.  Because we have @{term "card paths = n"}, the result follows.

    For the injective function, we simply use the observation stated above: Every path needs to
    be separated by @{term S} at some vertex, so we can choose such a vertex.
\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S. Separation G v0 v1 S \<Longrightarrow> n \<le> card S
[PROOF STEP]
define f where "f \<equiv> \<lambda>xs. SOME v. v \<in> S \<and> v \<in> set xs"
[PROOF STATE]
proof (state)
this:
f \<equiv> \<lambda>xs. SOME v. v \<in> S \<and> v \<in> set xs

goal (1 subgoal):
 1. \<And>S. Separation G v0 v1 S \<Longrightarrow> n \<le> card S
[PROOF STEP]
have f_good: "\<And>xs. xs \<in> paths \<Longrightarrow> f xs \<in> S \<and> f xs \<in> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. xs \<in> paths \<Longrightarrow> f xs \<in> S \<and> f xs \<in> set xs
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs. xs \<in> paths \<Longrightarrow> f xs \<in> S \<and> f xs \<in> set xs
[PROOF STEP]
fix xs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs. xs \<in> paths \<Longrightarrow> f xs \<in> S \<and> f xs \<in> set xs
[PROOF STEP]
assume "xs \<in> paths"
[PROOF STATE]
proof (state)
this:
xs \<in> paths

goal (1 subgoal):
 1. \<And>xs. xs \<in> paths \<Longrightarrow> f xs \<in> S \<and> f xs \<in> set xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs \<in> paths
[PROOF STEP]
obtain v where "v \<in> set xs \<inter> S"
[PROOF STATE]
proof (prove)
using this:
xs \<in> paths

goal (1 subgoal):
 1. (\<And>v. v \<in> set xs \<inter> S \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using S.S_separates paths
[PROOF STATE]
proof (prove)
using this:
xs \<in> paths
v0 \<leadsto>?xs\<leadsto> v1 \<Longrightarrow> set ?xs \<inter> S \<noteq> {}
?xs \<in> paths \<Longrightarrow> v0 \<leadsto>?xs\<leadsto> v1

goal (1 subgoal):
 1. (\<And>v. v \<in> set xs \<inter> S \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
v \<in> set xs \<inter> S

goal (1 subgoal):
 1. \<And>xs. xs \<in> paths \<Longrightarrow> f xs \<in> S \<and> f xs \<in> set xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> set xs \<inter> S
[PROOF STEP]
show "f xs \<in> S \<and> f xs \<in> set xs"
[PROOF STATE]
proof (prove)
using this:
v \<in> set xs \<inter> S

goal (1 subgoal):
 1. f xs \<in> S \<and> f xs \<in> set xs
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
using this:
v \<in> set xs \<inter> S

goal (1 subgoal):
 1. (SOME v. v \<in> S \<and> v \<in> set xs) \<in> S \<and> (SOME v. v \<in> S \<and> v \<in> set xs) \<in> set xs
[PROOF STEP]
using someI[of "\<lambda>v. v \<in> S \<and> v \<in> set xs" v]
[PROOF STATE]
proof (prove)
using this:
v \<in> set xs \<inter> S
v \<in> S \<and> v \<in> set xs \<Longrightarrow> (SOME v. v \<in> S \<and> v \<in> set xs) \<in> S \<and> (SOME v. v \<in> S \<and> v \<in> set xs) \<in> set xs

goal (1 subgoal):
 1. (SOME v. v \<in> S \<and> v \<in> set xs) \<in> S \<and> (SOME v. v \<in> S \<and> v \<in> set xs) \<in> set xs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f xs \<in> S \<and> f xs \<in> set xs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?xs \<in> paths \<Longrightarrow> f ?xs \<in> S \<and> f ?xs \<in> set ?xs

goal (1 subgoal):
 1. \<And>S. Separation G v0 v1 S \<Longrightarrow> n \<le> card S
[PROOF STEP]
text \<open>This @{term f} is injective because no two paths intersect in the same vertex.\<close>
[PROOF STATE]
proof (state)
this:
?xs \<in> paths \<Longrightarrow> f ?xs \<in> S \<and> f ?xs \<in> set ?xs

goal (1 subgoal):
 1. \<And>S. Separation G v0 v1 S \<Longrightarrow> n \<le> card S
[PROOF STEP]
have "inj_on f paths"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on f paths
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> paths; y \<in> paths; f x = f y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix xs ys
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> paths; y \<in> paths; f x = f y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume *: "xs \<in> paths" "ys \<in> paths" "f xs = f ys"
[PROOF STATE]
proof (state)
this:
xs \<in> paths
ys \<in> paths
f xs = f ys

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> paths; y \<in> paths; f x = f y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs \<in> paths
ys \<in> paths
f xs = f ys
[PROOF STEP]
obtain v where "v \<in> S" "v \<in> set xs" "v \<in> set ys"
[PROOF STATE]
proof (prove)
using this:
xs \<in> paths
ys \<in> paths
f xs = f ys

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<in> S; v \<in> set xs; v \<in> set ys\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using f_good
[PROOF STATE]
proof (prove)
using this:
xs \<in> paths
ys \<in> paths
f xs = f ys
?xs \<in> paths \<Longrightarrow> f ?xs \<in> S \<and> f ?xs \<in> set ?xs

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<in> S; v \<in> set xs; v \<in> set ys\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
v \<in> S
v \<in> set xs
v \<in> set ys

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> paths; y \<in> paths; f x = f y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> S
v \<in> set xs
v \<in> set ys
[PROOF STEP]
show "xs = ys"
[PROOF STATE]
proof (prove)
using this:
v \<in> S
v \<in> set xs
v \<in> set ys

goal (1 subgoal):
 1. xs = ys
[PROOF STEP]
using *(1,2) paths_disjoint S.v0_notin_S S.v1_notin_S
[PROOF STATE]
proof (prove)
using this:
v \<in> S
v \<in> set xs
v \<in> set ys
xs \<in> paths
ys \<in> paths
\<lbrakk>?xs \<in> paths; ?ys \<in> paths; ?xs \<noteq> ?ys; ?v \<in> set ?xs; ?v \<in> set ?ys\<rbrakk> \<Longrightarrow> ?v = v0 \<or> ?v = v1
v0 \<notin> S
v1 \<notin> S

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

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

goal (1 subgoal):
 1. \<And>S. Separation G v0 v1 S \<Longrightarrow> n \<le> card S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inj_on f paths
[PROOF STEP]
show "card S \<ge> n"
[PROOF STATE]
proof (prove)
using this:
inj_on f paths

goal (1 subgoal):
 1. n \<le> card S
[PROOF STEP]
using assms(2) f_good
[PROOF STATE]
proof (prove)
using this:
inj_on f paths
card paths = n
?xs \<in> paths \<Longrightarrow> f ?xs \<in> S \<and> f ?xs \<in> set ?xs

goal (1 subgoal):
 1. n \<le> card S
[PROOF STEP]
by (metis S.finite_S finite_paths image_subsetI inj_on_iff_card_le)
[PROOF STATE]
proof (state)
this:
n \<le> card S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma desne_order_ow_transfer[transfer_rule]:
  assumes [transfer_rule]: "bi_unique A" "right_total A"
  shows
    "(rel_set A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=))
      dense_order_ow dense_order_ow"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_set A ===> (A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=)) dense_order_ow dense_order_ow
[PROOF STEP]
by
    (
      ow_locale_transfer locale_defs:
        dense_order_ow_def dense_order_ow_axioms_def
    )


[STATEMENT]
lemma (in Semilat) closed_f [simp, intro]: "\<lbrakk>x \<in> A; y \<in> A\<rbrakk>  \<Longrightarrow> x \<squnion>\<^sub>f y \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y \<in> A
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x \<squnion>\<^bsub>f\<^esub> y \<in> A
[PROOF STEP]
by (simp add: closedD [OF closedI])


[STATEMENT]
lemma to_nat_eq [simp]: "to_nat x = to_nat y \<longleftrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mod_type_class.to_nat x = mod_type_class.to_nat y) = (x = y)
[PROOF STEP]
using injD [OF bij_betw_imp_inj_on[OF bij_to_nat]]
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat ?x = mod_type_class.to_nat ?y \<Longrightarrow> ?x = ?y

goal (1 subgoal):
 1. (mod_type_class.to_nat x = mod_type_class.to_nat y) = (x = y)
[PROOF STEP]
by blast


[STATEMENT]
lemma vifunion_vempty_family[simp]: "(\<Union>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. 0) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>I. 0) `\<^sub>\<circ> I) = 0
[PROOF STEP]
by auto


[STATEMENT]
lemma oalist_inv_raw_map_val_pair:
  assumes "oalist_inv_raw xs"
  shows "oalist_inv_raw (map_val_pair f xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oalist_inv_raw (map_val_pair f xs)
[PROOF STEP]
by (rule oalist_inv_raw_map_pair, fact assms, auto)


[STATEMENT]
lemma map_val_raw_cong:
  assumes "\<And>k v. (k, v) \<in> set (fst xs) \<Longrightarrow> f k v = g k v"
  shows "map_val_raw f xs = map_val_raw g xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_val_raw f xs = map_val_raw g xs
[PROOF STEP]
proof (rule map_raw_cong)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>kv. kv \<in> set (fst xs) \<Longrightarrow> (case kv of (k, v) \<Rightarrow> (k, f k v)) = (case kv of (k, v) \<Rightarrow> (k, g k v))
[PROOF STEP]
fix kv
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>kv. kv \<in> set (fst xs) \<Longrightarrow> (case kv of (k, v) \<Rightarrow> (k, f k v)) = (case kv of (k, v) \<Rightarrow> (k, g k v))
[PROOF STEP]
assume "kv \<in> set (fst xs)"
[PROOF STATE]
proof (state)
this:
kv \<in> set (fst xs)

goal (1 subgoal):
 1. \<And>kv. kv \<in> set (fst xs) \<Longrightarrow> (case kv of (k, v) \<Rightarrow> (k, f k v)) = (case kv of (k, v) \<Rightarrow> (k, g k v))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
kv \<in> set (fst xs)

goal (1 subgoal):
 1. \<And>kv. kv \<in> set (fst xs) \<Longrightarrow> (case kv of (k, v) \<Rightarrow> (k, f k v)) = (case kv of (k, v) \<Rightarrow> (k, g k v))
[PROOF STEP]
obtain k v where "kv = (k, v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k v. kv = (k, v) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
kv = (k, v)

goal (1 subgoal):
 1. \<And>kv. kv \<in> set (fst xs) \<Longrightarrow> (case kv of (k, v) \<Rightarrow> (k, f k v)) = (case kv of (k, v) \<Rightarrow> (k, g k v))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
kv \<in> set (fst xs)
kv = (k, v)
[PROOF STEP]
show "(case kv of (k, v) \<Rightarrow> (k, f k v)) = (case kv of (k, v) \<Rightarrow> (k, g k v))"
[PROOF STATE]
proof (prove)
using this:
kv \<in> set (fst xs)
kv = (k, v)

goal (1 subgoal):
 1. (case kv of (k, v) \<Rightarrow> (k, f k v)) = (case kv of (k, v) \<Rightarrow> (k, g k v))
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
this:
(case kv of (k, v) \<Rightarrow> (k, f k v)) = (case kv of (k, v) \<Rightarrow> (k, g k v))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sorted_sorted_domain: "sorted_wrt (lt ko) (sorted_domain ko xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_wrt (lt ko) (sorted_domain ko xs)
[PROOF STEP]
unfolding sorted_domain_def lt_of_key_order.rep_eq[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_wrt (lt_of_key_order (rep_key_order ko)) (sorted_domain_raw ko (list_of_oalist xs))
[PROOF STEP]
using oalist_inv_list_of_oalist
[PROOF STATE]
proof (prove)
using this:
oalist_inv (list_of_oalist ?x)

goal (1 subgoal):
 1. sorted_wrt (lt_of_key_order (rep_key_order ko)) (sorted_domain_raw ko (list_of_oalist xs))
[PROOF STEP]
by (rule sorted_sorted_domain_raw)


[STATEMENT]
lemma IdFtor'Obj:
  assumes "Category C" and "X \<in> obj\<^bsub>CatDom (FId' C)\<^esub>"
  shows "(FId' C) @@ X = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FId' C @@ X = X
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. FId' C @@ X = X
[PROOF STEP]
have "(FId' C) ## id\<^bsub>CatDom (FId' C)\<^esub> X = id\<^bsub>CatCod (FId' C)\<^esub> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FId' C ## id\<^bsub>CatDom FId' C\<^esub> X = id\<^bsub>CatCod FId' C\<^esub> X
[PROOF STEP]
by(simp add: IdentityFunctor'_def)
[PROOF STATE]
proof (state)
this:
FId' C ## id\<^bsub>CatDom FId' C\<^esub> X = id\<^bsub>CatCod FId' C\<^esub> X

goal (1 subgoal):
 1. FId' C @@ X = X
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
FId' C ## id\<^bsub>CatDom FId' C\<^esub> X = id\<^bsub>CatCod FId' C\<^esub> X

goal (1 subgoal):
 1. FId' C @@ X = X
[PROOF STEP]
have "X \<in> obj\<^bsub>CatCod (FId' C)\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<in> obj\<^bsub>CatCod FId' C\<^esub>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Category C
X \<in> obj\<^bsub>CatDom FId' C\<^esub>

goal (1 subgoal):
 1. X \<in> obj\<^bsub>CatCod FId' C\<^esub>
[PROOF STEP]
by (simp add: IdentityFunctor'_def)
[PROOF STATE]
proof (state)
this:
X \<in> obj\<^bsub>CatCod FId' C\<^esub>

goal (1 subgoal):
 1. FId' C @@ X = X
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
FId' C ## id\<^bsub>CatDom FId' C\<^esub> X = id\<^bsub>CatCod FId' C\<^esub> X
X \<in> obj\<^bsub>CatCod FId' C\<^esub>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
FId' C ## id\<^bsub>CatDom FId' C\<^esub> X = id\<^bsub>CatCod FId' C\<^esub> X
X \<in> obj\<^bsub>CatCod FId' C\<^esub>

goal (1 subgoal):
 1. FId' C @@ X = X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
FId' C ## id\<^bsub>CatDom FId' C\<^esub> X = id\<^bsub>CatCod FId' C\<^esub> X
X \<in> obj\<^bsub>CatCod FId' C\<^esub>
Category C
X \<in> obj\<^bsub>CatDom FId' C\<^esub>

goal (1 subgoal):
 1. FId' C @@ X = X
[PROOF STEP]
by (simp add: PreFunctor.FmToFo IdFtor'PreFunctor)
[PROOF STATE]
proof (state)
this:
FId' C @@ X = X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma betw_b_in_path:
  assumes abc: "[a;b;c]"
      and path_ab: "path ac a c"
  shows "b \<in> ac"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<in> ac
[PROOF STEP]
using assms abc_ex_path_unique path_unique
[PROOF STATE]
proof (prove)
using this:
[a;b;c]
path ac a c
[?a;?b;?c] \<Longrightarrow> \<exists>!Q. Q \<in> \<P> \<and> ?a \<in> Q \<and> ?b \<in> Q \<and> ?c \<in> Q
\<lbrakk>path ?ab ?a ?b; path ?ab' ?a ?b\<rbrakk> \<Longrightarrow> ?ab = ?ab'

goal (1 subgoal):
 1. b \<in> ac
[PROOF STEP]
by blast


[STATEMENT]
lemma wlog_endpoints_degenerate:
  assumes path_A: "A\<in>\
"
      and symmetric_Q: "\<And>a b I. Q I a b \<Longrightarrow> Q I b a"
      and Q_implies_path: "\<And>a b I. \<lbrakk>I\<subseteq>A; Q I a b\<rbrakk> \<Longrightarrow> b\<in>A \<and> a\<in>A"
      and symmetric_P: "\<And>I J. \<lbrakk>\<exists>a b. Q I a b; \<exists>a b. Q J a b; P I J\<rbrakk> \<Longrightarrow> P J I"
      and "\<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I\<subseteq>A; J\<subseteq>A\<rbrakk>
            \<Longrightarrow> ((a=b \<and> b=c \<and> c=d) \<longrightarrow> P I J) \<and> ((a=b \<and> b\<noteq>c \<and> c=d) \<longrightarrow> P I J)
              \<and> ((a=b \<and> b=c \<and> c\<noteq>d) \<longrightarrow> P I J) \<and> ((a=b \<and> b\<noteq>c \<and> c\<noteq>d \<and> a\<noteq>d) \<longrightarrow> P I J)
              \<and> ((a\<noteq>b \<and> b=c \<and> c\<noteq>d \<and> a=d) \<longrightarrow> P I J)
              \<and> (([a;b;c] \<and> a=d) \<longrightarrow> P I J) \<and> (([b;a;c] \<and> a=d) \<longrightarrow> P I J)"
    shows "\<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I\<subseteq>A; J\<subseteq>A;
            \<not>(a\<noteq>b \<and> b\<noteq>c \<and> c\<noteq>d \<and> a\<noteq>d \<and> a\<noteq>c \<and> b\<noteq>d)\<rbrakk> \<Longrightarrow> P I J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
text \<open>We first extract some of the assumptions of this lemma into the form
  of other WLOG lemmas' assumptions.\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
have ord1: "\<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I\<subseteq>A; J\<subseteq>A;
              [a;b;c] \<and> a=d\<rbrakk> \<Longrightarrow> P I J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; [a;b;c] \<and> a = d\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
using assms(5)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A\<rbrakk> \<Longrightarrow> (?a = ?b \<and> ?b = ?c \<and> ?c = ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b \<noteq> ?c \<and> ?c = ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a \<noteq> ?d \<longrightarrow> P ?I ?J) \<and> (?a \<noteq> ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d \<longrightarrow> P ?I ?J) \<and> ([?a;?b;?c] \<and> ?a = ?d \<longrightarrow> P ?I ?J) \<and> ([?b;?a;?c] \<and> ?a = ?d \<longrightarrow> P ?I ?J)

goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; [a;b;c] \<and> a = d\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A; [?a;?b;?c] \<and> ?a = ?d\<rbrakk> \<Longrightarrow> P ?I ?J

goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
have ord2: "\<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I\<subseteq>A; J\<subseteq>A;
              [b;a;c] \<and> a=d\<rbrakk> \<Longrightarrow> P I J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; [b;a;c] \<and> a = d\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
using assms(5)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A\<rbrakk> \<Longrightarrow> (?a = ?b \<and> ?b = ?c \<and> ?c = ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b \<noteq> ?c \<and> ?c = ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a \<noteq> ?d \<longrightarrow> P ?I ?J) \<and> (?a \<noteq> ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d \<longrightarrow> P ?I ?J) \<and> ([?a;?b;?c] \<and> ?a = ?d \<longrightarrow> P ?I ?J) \<and> ([?b;?a;?c] \<and> ?a = ?d \<longrightarrow> P ?I ?J)

goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; [b;a;c] \<and> a = d\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A; [?b;?a;?c] \<and> ?a = ?d\<rbrakk> \<Longrightarrow> P ?I ?J

goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
have last_case: "\<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I\<subseteq>A; J\<subseteq>A;
              a\<noteq>b \<and> b\<noteq>c \<and> c\<noteq>d \<and> a=d\<rbrakk> \<Longrightarrow> P I J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
using ord1 ord2 wlog_endpoints_degenerate2 symmetric_P symmetric_Q Q_implies_path path_A
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A; [?a;?b;?c] \<and> ?a = ?d\<rbrakk> \<Longrightarrow> P ?I ?J
\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A; [?b;?a;?c] \<and> ?a = ?d\<rbrakk> \<Longrightarrow> P ?I ?J
\<lbrakk>\<And>a b I. ?Q I a b \<Longrightarrow> ?Q I b a; \<And>a b I A. \<lbrakk>I \<subseteq> A; A \<in> \
; ?Q I a b\<rbrakk> \<Longrightarrow> b \<in> A \<and> a \<in> A; \<And>I J. \<lbrakk>\<exists>a b. ?Q I a b; \<exists>a b. ?Q J a b; ?P I J\<rbrakk> \<Longrightarrow> ?P J I; \<And>I J a b c d A. \<lbrakk>?Q I a b; ?Q J c d; I \<subseteq> A; J \<subseteq> A; A \<in> \
; [a;b;c] \<and> a = d\<rbrakk> \<Longrightarrow> ?P I J; \<And>I J a b c d A. \<lbrakk>?Q I a b; ?Q J c d; I \<subseteq> A; J \<subseteq> A; A \<in> \
; [b;a;c] \<and> a = d\<rbrakk> \<Longrightarrow> ?P I J; ?Q ?I ?a ?b; ?Q ?J ?c ?d; ?I \<subseteq> ?A; ?J \<subseteq> ?A; ?A \<in> \
; ?a \<noteq> ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d\<rbrakk> \<Longrightarrow> ?P ?I ?J
\<lbrakk>\<exists>a b. Q ?I a b; \<exists>a b. Q ?J a b; P ?I ?J\<rbrakk> \<Longrightarrow> P ?J ?I
Q ?I ?a ?b \<Longrightarrow> Q ?I ?b ?a
\<lbrakk>?I \<subseteq> A; Q ?I ?a ?b\<rbrakk> \<Longrightarrow> ?b \<in> A \<and> ?a \<in> A
A \<in> \

goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
by (metis abc_sym some_betw)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A; ?a \<noteq> ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d\<rbrakk> \<Longrightarrow> P ?I ?J

goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
show "\<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I\<subseteq>A; J\<subseteq>A;
            \<not>(a\<noteq>b \<and> b\<noteq>c \<and> c\<noteq>d \<and> a\<noteq>d \<and> a\<noteq>c \<and> b\<noteq>d)\<rbrakk> \<Longrightarrow> P I J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
text \<open>Fix the sets on the path, and obtain the assumptions of \<open>wlog_endpoints_degenerate1\<close>.\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
fix I J
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
assume asm1: "I\<subseteq>A" "J\<subseteq>A"
[PROOF STATE]
proof (state)
this:
I \<subseteq> A
J \<subseteq> A

goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
have two: "\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a=b \<and> b=c \<and> c=d\<rbrakk> \<Longrightarrow> P I J"
            "\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a=b \<and> b\<noteq>c \<and> c=d\<rbrakk> \<Longrightarrow> P I J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c = d\<rbrakk> \<Longrightarrow> P I J) &&& (\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a = b \<and> b \<noteq> c \<and> c = d\<rbrakk> \<Longrightarrow> P I J)
[PROOF STEP]
using \<open>J \<subseteq> A\<close> \<open>I \<subseteq> A\<close> path_A assms(5)
[PROOF STATE]
proof (prove)
using this:
J \<subseteq> A
I \<subseteq> A
A \<in> \

\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A\<rbrakk> \<Longrightarrow> (?a = ?b \<and> ?b = ?c \<and> ?c = ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b \<noteq> ?c \<and> ?c = ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a \<noteq> ?d \<longrightarrow> P ?I ?J) \<and> (?a \<noteq> ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d \<longrightarrow> P ?I ?J) \<and> ([?a;?b;?c] \<and> ?a = ?d \<longrightarrow> P ?I ?J) \<and> ([?b;?a;?c] \<and> ?a = ?d \<longrightarrow> P ?I ?J)

goal (1 subgoal):
 1. (\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c = d\<rbrakk> \<Longrightarrow> P I J) &&& (\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a = b \<and> b \<noteq> c \<and> c = d\<rbrakk> \<Longrightarrow> P I J)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
\<lbrakk>Q I ?a ?b; Q J ?c ?d; ?a = ?b \<and> ?b = ?c \<and> ?c = ?d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I ?a ?b; Q J ?c ?d; ?a = ?b \<and> ?b \<noteq> ?c \<and> ?c = ?d\<rbrakk> \<Longrightarrow> P I J

goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
have one: "\<And> a b c d. \<lbrakk>Q I a b; Q J c d; a=b \<and> b=c \<and> c\<noteq>d\<rbrakk> \<Longrightarrow> P I J"
          "\<And> a b c d. \<lbrakk>Q I a b; Q J c d; a=b \<and> b\<noteq>c \<and> c\<noteq>d \<and> a\<noteq>d\<rbrakk> \<Longrightarrow> P I J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c \<noteq> d\<rbrakk> \<Longrightarrow> P I J) &&& (\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a = b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d\<rbrakk> \<Longrightarrow> P I J)
[PROOF STEP]
using \<open>I \<subseteq> A\<close> \<open>J \<subseteq> A\<close> path_A assms(5)
[PROOF STATE]
proof (prove)
using this:
I \<subseteq> A
J \<subseteq> A
A \<in> \

\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A\<rbrakk> \<Longrightarrow> (?a = ?b \<and> ?b = ?c \<and> ?c = ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b \<noteq> ?c \<and> ?c = ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a \<noteq> ?d \<longrightarrow> P ?I ?J) \<and> (?a \<noteq> ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d \<longrightarrow> P ?I ?J) \<and> ([?a;?b;?c] \<and> ?a = ?d \<longrightarrow> P ?I ?J) \<and> ([?b;?a;?c] \<and> ?a = ?d \<longrightarrow> P ?I ?J)

goal (1 subgoal):
 1. (\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c \<noteq> d\<rbrakk> \<Longrightarrow> P I J) &&& (\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a = b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d\<rbrakk> \<Longrightarrow> P I J)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
\<lbrakk>Q I ?a ?b; Q J ?c ?d; ?a = ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I ?a ?b; Q J ?c ?d; ?a = ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a \<noteq> ?d\<rbrakk> \<Longrightarrow> P I J

goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
have no: "\<And> a b c d. \<lbrakk>Q I a b; Q J c d; a\<noteq>b \<and> b\<noteq>c \<and> c\<noteq>d \<and> a=d\<rbrakk> \<Longrightarrow> P I J"
          "\<And> a b c d. \<lbrakk>Q I a b; Q J c d; a\<noteq>b \<and> b=c \<and> c\<noteq>d \<and> a=d\<rbrakk> \<Longrightarrow> P I J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J) &&& (\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b = c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J)
[PROOF STEP]
using \<open>I \<subseteq> A\<close> \<open>J \<subseteq> A\<close> path_A last_case
[PROOF STATE]
proof (prove)
using this:
I \<subseteq> A
J \<subseteq> A
A \<in> \

\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A; ?a \<noteq> ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d\<rbrakk> \<Longrightarrow> P ?I ?J

goal (1 subgoal):
 1. (\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J) &&& (\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b = c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c d. \<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b = c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
using \<open>I \<subseteq> A\<close> \<open>J \<subseteq> A\<close> path_A assms(5)
[PROOF STATE]
proof (prove)
using this:
I \<subseteq> A
J \<subseteq> A
A \<in> \

\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A\<rbrakk> \<Longrightarrow> (?a = ?b \<and> ?b = ?c \<and> ?c = ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b \<noteq> ?c \<and> ?c = ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a \<noteq> ?d \<longrightarrow> P ?I ?J) \<and> (?a \<noteq> ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d \<longrightarrow> P ?I ?J) \<and> ([?a;?b;?c] \<and> ?a = ?d \<longrightarrow> P ?I ?J) \<and> ([?b;?a;?c] \<and> ?a = ?d \<longrightarrow> P ?I ?J)

goal (1 subgoal):
 1. \<And>a b c d. \<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b = c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>Q I ?a ?b; Q J ?c ?d; ?a \<noteq> ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I ?a ?b; Q J ?c ?d; ?a \<noteq> ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d\<rbrakk> \<Longrightarrow> P I J

goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
text \<open>Now unwrap the remaining object logic and finish the proof.\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>Q I ?a ?b; Q J ?c ?d; ?a \<noteq> ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I ?a ?b; Q J ?c ?d; ?a \<noteq> ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d\<rbrakk> \<Longrightarrow> P I J

goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
fix a b c d
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
assume asm2: "Q I a b" "Q J c d" "\<not>(a\<noteq>b \<and> b\<noteq>c \<and> c\<noteq>d \<and> a\<noteq>d \<and> a\<noteq>c \<and> b\<noteq>d)"
[PROOF STATE]
proof (state)
this:
Q I a b
Q J c d
\<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)

goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
show "P I J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P I J
[PROOF STEP]
using two [where a=a and b=b and c=c and d=d]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a = b \<and> b \<noteq> c \<and> c = d\<rbrakk> \<Longrightarrow> P I J

goal (1 subgoal):
 1. P I J
[PROOF STEP]
using one [where a=a and b=b and c=c and d=d]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a = b \<and> b \<noteq> c \<and> c = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c \<noteq> d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a = b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d\<rbrakk> \<Longrightarrow> P I J

goal (1 subgoal):
 1. P I J
[PROOF STEP]
using no [where a=a and b=b and c=c and d=d]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a = b \<and> b \<noteq> c \<and> c = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c \<noteq> d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a = b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b = c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J

goal (1 subgoal):
 1. P I J
[PROOF STEP]
using wlog_endpoints_degenerate1
        [where I=I and J=J and a=a and b=b and c=c and d=d and P=P and Q=Q]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a = b \<and> b \<noteq> c \<and> c = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c \<noteq> d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a = b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b = c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>\<And>a b I. Q I a b \<Longrightarrow> Q I b a; \<And>I J. \<lbrakk>\<exists>a b. Q I a b; \<exists>a b. Q I a b; P I J\<rbrakk> \<Longrightarrow> P J I; \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c = d \<or> a = b \<and> b \<noteq> c \<and> c = d\<rbrakk> \<Longrightarrow> P I J; \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c \<noteq> d \<or> a = b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d\<rbrakk> \<Longrightarrow> P I J; \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a = d \<or> a \<noteq> b \<and> b = c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J; Q I a b; Q J c d; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J

goal (1 subgoal):
 1. P I J
[PROOF STEP]
using asm1 asm2 symmetric_P last_case assms(5) symmetric_Q
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a = b \<and> b \<noteq> c \<and> c = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c \<noteq> d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a = b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b = c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>\<And>a b I. Q I a b \<Longrightarrow> Q I b a; \<And>I J. \<lbrakk>\<exists>a b. Q I a b; \<exists>a b. Q I a b; P I J\<rbrakk> \<Longrightarrow> P J I; \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c = d \<or> a = b \<and> b \<noteq> c \<and> c = d\<rbrakk> \<Longrightarrow> P I J; \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c \<noteq> d \<or> a = b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d\<rbrakk> \<Longrightarrow> P I J; \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a = d \<or> a \<noteq> b \<and> b = c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J; Q I a b; Q J c d; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
I \<subseteq> A
J \<subseteq> A
Q I a b
Q J c d
\<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)
\<lbrakk>\<exists>a b. Q ?I a b; \<exists>a b. Q ?J a b; P ?I ?J\<rbrakk> \<Longrightarrow> P ?J ?I
\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A; ?a \<noteq> ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d\<rbrakk> \<Longrightarrow> P ?I ?J
\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A\<rbrakk> \<Longrightarrow> (?a = ?b \<and> ?b = ?c \<and> ?c = ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b \<noteq> ?c \<and> ?c = ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a \<noteq> ?d \<longrightarrow> P ?I ?J) \<and> (?a \<noteq> ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d \<longrightarrow> P ?I ?J) \<and> ([?a;?b;?c] \<and> ?a = ?d \<longrightarrow> P ?I ?J) \<and> ([?b;?a;?c] \<and> ?a = ?d \<longrightarrow> P ?I ?J)
Q ?I ?a ?b \<Longrightarrow> Q ?I ?b ?a

goal (1 subgoal):
 1. P I J
[PROOF STEP]
by smt
[PROOF STATE]
proof (state)
this:
P I J

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A; \<not> (?a \<noteq> ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a \<noteq> ?d \<and> ?a \<noteq> ?c \<and> ?b \<noteq> ?d)\<rbrakk> \<Longrightarrow> P ?I ?J

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in gd_term) Macaulay_list_is_GB:
  assumes "is_Groebner_basis G" and "pmdl (set ps) = pmdl G" and "G \<subseteq> phull (set ps)"
  shows "is_Groebner_basis (set (Macaulay_list ps))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_Groebner_basis (set (Macaulay_list ps))
[PROOF STEP]
proof (simp only: GB_alt_3_finite[OF finite_set] pmdl_Macaulay_list, intro ballI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>f \<in> pmdl (set ps); f \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>g\<in>set (Macaulay_list ps). g \<noteq> 0 \<and> lt g adds\<^sub>t lt f
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>f \<in> pmdl (set ps); f \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>g\<in>set (Macaulay_list ps). g \<noteq> 0 \<and> lt g adds\<^sub>t lt f
[PROOF STEP]
assume "f \<in> pmdl (set ps)"
[PROOF STATE]
proof (state)
this:
f \<in> pmdl (set ps)

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f \<in> pmdl (set ps); f \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>g\<in>set (Macaulay_list ps). g \<noteq> 0 \<and> lt g adds\<^sub>t lt f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f \<in> pmdl (set ps)

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f \<in> pmdl (set ps); f \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>g\<in>set (Macaulay_list ps). g \<noteq> 0 \<and> lt g adds\<^sub>t lt f
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
pmdl (set ps) = pmdl G
[PROOF STEP]
have "\<dots> = pmdl G"
[PROOF STATE]
proof (prove)
using this:
pmdl (set ps) = pmdl G

goal (1 subgoal):
 1. pmdl (set ps) = pmdl G
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
pmdl (set ps) = pmdl G

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f \<in> pmdl (set ps); f \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>g\<in>set (Macaulay_list ps). g \<noteq> 0 \<and> lt g adds\<^sub>t lt f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f \<in> pmdl G
[PROOF STEP]
have "f \<in> pmdl G"
[PROOF STATE]
proof (prove)
using this:
f \<in> pmdl G

goal (1 subgoal):
 1. f \<in> pmdl G
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
f \<in> pmdl G

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f \<in> pmdl (set ps); f \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>g\<in>set (Macaulay_list ps). g \<noteq> 0 \<and> lt g adds\<^sub>t lt f
[PROOF STEP]
assume "f \<noteq> 0"
[PROOF STATE]
proof (state)
this:
f \<noteq> 0

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f \<in> pmdl (set ps); f \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>g\<in>set (Macaulay_list ps). g \<noteq> 0 \<and> lt g adds\<^sub>t lt f
[PROOF STEP]
with assms(1) \<open>f \<in> pmdl G\<close>
[PROOF STATE]
proof (chain)
picking this:
is_Groebner_basis G
f \<in> pmdl G
f \<noteq> 0
[PROOF STEP]
obtain g where "g \<in> G" and "g \<noteq> 0" and "lt g adds\<^sub>t lt f"
[PROOF STATE]
proof (prove)
using this:
is_Groebner_basis G
f \<in> pmdl G
f \<noteq> 0

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> G; g \<noteq> 0; lt g adds\<^sub>t lt f\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule GB_adds_lt)
[PROOF STATE]
proof (state)
this:
g \<in> G
g \<noteq> 0
lt g adds\<^sub>t lt f

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f \<in> pmdl (set ps); f \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>g\<in>set (Macaulay_list ps). g \<noteq> 0 \<and> lt g adds\<^sub>t lt f
[PROOF STEP]
from assms(3) \<open>g \<in> G\<close>
[PROOF STATE]
proof (chain)
picking this:
G \<subseteq> phull (set ps)
g \<in> G
[PROOF STEP]
have "g \<in> phull (set ps)"
[PROOF STATE]
proof (prove)
using this:
G \<subseteq> phull (set ps)
g \<in> G

goal (1 subgoal):
 1. g \<in> phull (set ps)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
g \<in> phull (set ps)

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f \<in> pmdl (set ps); f \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>g\<in>set (Macaulay_list ps). g \<noteq> 0 \<and> lt g adds\<^sub>t lt f
[PROOF STEP]
from this \<open>g \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
g \<in> phull (set ps)
g \<noteq> 0
[PROOF STEP]
obtain g' where "g' \<in> set (Macaulay_list ps)" and "g' \<noteq> 0" and "lt g = lt g'"
[PROOF STATE]
proof (prove)
using this:
g \<in> phull (set ps)
g \<noteq> 0

goal (1 subgoal):
 1. (\<And>g'. \<lbrakk>g' \<in> set (Macaulay_list ps); g' \<noteq> 0; lt g = lt g'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule Macaulay_list_lt)
[PROOF STATE]
proof (state)
this:
g' \<in> set (Macaulay_list ps)
g' \<noteq> 0
lt g = lt g'

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f \<in> pmdl (set ps); f \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>g\<in>set (Macaulay_list ps). g \<noteq> 0 \<and> lt g adds\<^sub>t lt f
[PROOF STEP]
show "\<exists>g\<in>set (Macaulay_list ps). g \<noteq> 0 \<and> lt g adds\<^sub>t lt f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>g\<in>set (Macaulay_list ps). g \<noteq> 0 \<and> lt g adds\<^sub>t lt f
[PROOF STEP]
proof (rule, rule)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ?g \<noteq> 0
 2. lt ?g adds\<^sub>t lt f
 3. ?g \<in> set (Macaulay_list ps)
[PROOF STEP]
from \<open>lt g adds\<^sub>t lt f\<close>
[PROOF STATE]
proof (chain)
picking this:
lt g adds\<^sub>t lt f
[PROOF STEP]
show "lt g' adds\<^sub>t lt f"
[PROOF STATE]
proof (prove)
using this:
lt g adds\<^sub>t lt f

goal (1 subgoal):
 1. lt g' adds\<^sub>t lt f
[PROOF STEP]
by (simp only: \<open>lt g = lt g'\<close>)
[PROOF STATE]
proof (state)
this:
lt g' adds\<^sub>t lt f

goal (2 subgoals):
 1. g' \<noteq> 0
 2. g' \<in> set (Macaulay_list ps)
[PROOF STEP]
qed fact+
[PROOF STATE]
proof (state)
this:
\<exists>g\<in>set (Macaulay_list ps). g \<noteq> 0 \<and> lt g adds\<^sub>t lt f

goal:
No subgoals!
[PROOF STEP]
qed