[STATEMENT]
lemma supto_split1: \<comment>\<open>From \<open>HOL.List\<close>\<close>
  assumes "i \<le> j"
  assumes "j \<le> k"
  shows "supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>(j - 1)) :@ supto\<cdot>(MkI\<cdot>j)\<cdot>(MkI\<cdot>k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>(j - 1)) :@ supto\<cdot>(MkI\<cdot>j)\<cdot>(MkI\<cdot>k)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<le> j
j \<le> k

goal (1 subgoal):
 1. supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>(j - 1)) :@ supto\<cdot>(MkI\<cdot>j)\<cdot>(MkI\<cdot>k)
[PROOF STEP]
proof (induct j rule: int_ge_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i \<le> k \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>(i - 1)) :@ supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k)
 2. \<And>ia. \<lbrakk>i \<le> ia; ia \<le> k \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>(ia - 1)) :@ supto\<cdot>(MkI\<cdot>ia)\<cdot>(MkI\<cdot>k); ia + 1 \<le> k\<rbrakk> \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>(ia + 1 - 1)) :@ supto\<cdot>(MkI\<cdot>(ia + 1))\<cdot>(MkI\<cdot>k)
[PROOF STEP]
case (step l)
[PROOF STATE]
proof (state)
this:
i \<le> l
l \<le> k \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>(l - 1)) :@ supto\<cdot>(MkI\<cdot>l)\<cdot>(MkI\<cdot>k)
l + 1 \<le> k

goal (2 subgoals):
 1. i \<le> k \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>(i - 1)) :@ supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k)
 2. \<And>ia. \<lbrakk>i \<le> ia; ia \<le> k \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>(ia - 1)) :@ supto\<cdot>(MkI\<cdot>ia)\<cdot>(MkI\<cdot>k); ia + 1 \<le> k\<rbrakk> \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>(ia + 1 - 1)) :@ supto\<cdot>(MkI\<cdot>(ia + 1))\<cdot>(MkI\<cdot>k)
[PROOF STEP]
with supto_simp(2) supto_snoc
[PROOF STATE]
proof (chain)
picking this:
?i \<le> ?j \<Longrightarrow> supto\<cdot>(MkI\<cdot>?i)\<cdot>(MkI\<cdot>?j) = MkI\<cdot>?i :# supto\<cdot>(MkI\<cdot>?i + 1)\<cdot>(MkI\<cdot>?j)
?i \<le> ?j \<Longrightarrow> supto\<cdot>(MkI\<cdot>?i)\<cdot>(MkI\<cdot>?j) = supto\<cdot>(MkI\<cdot>?i)\<cdot>(MkI\<cdot>?j - 1) :@ [:MkI\<cdot>?j:]
i \<le> l
l \<le> k \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>(l - 1)) :@ supto\<cdot>(MkI\<cdot>l)\<cdot>(MkI\<cdot>k)
l + 1 \<le> k
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?i \<le> ?j \<Longrightarrow> supto\<cdot>(MkI\<cdot>?i)\<cdot>(MkI\<cdot>?j) = MkI\<cdot>?i :# supto\<cdot>(MkI\<cdot>?i + 1)\<cdot>(MkI\<cdot>?j)
?i \<le> ?j \<Longrightarrow> supto\<cdot>(MkI\<cdot>?i)\<cdot>(MkI\<cdot>?j) = supto\<cdot>(MkI\<cdot>?i)\<cdot>(MkI\<cdot>?j - 1) :@ [:MkI\<cdot>?j:]
i \<le> l
l \<le> k \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>(l - 1)) :@ supto\<cdot>(MkI\<cdot>l)\<cdot>(MkI\<cdot>k)
l + 1 \<le> k

goal (1 subgoal):
 1. supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>(l + 1 - 1)) :@ supto\<cdot>(MkI\<cdot>(l + 1))\<cdot>(MkI\<cdot>k)
[PROOF STEP]
by (clarsimp simp: one_Integer_def)
[PROOF STATE]
proof (state)
this:
supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>(l + 1 - 1)) :@ supto\<cdot>(MkI\<cdot>(l + 1))\<cdot>(MkI\<cdot>k)

goal (1 subgoal):
 1. i \<le> k \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>(i - 1)) :@ supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k)
[PROOF STEP]
qed simp


[STATEMENT]
lemma supto_split2: \<comment>\<open>From \<open>HOL.List\<close>\<close>
  assumes "i \<le> j"
  assumes "j \<le> k"
  shows "supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) :@ supto\<cdot>(MkI\<cdot>(j + 1))\<cdot>(MkI\<cdot>k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) :@ supto\<cdot>(MkI\<cdot>(j + 1))\<cdot>(MkI\<cdot>k)
[PROOF STEP]
proof(cases "j + 1 \<le> k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. j + 1 \<le> k \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) :@ supto\<cdot>(MkI\<cdot>(j + 1))\<cdot>(MkI\<cdot>k)
 2. \<not> j + 1 \<le> k \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) :@ supto\<cdot>(MkI\<cdot>(j + 1))\<cdot>(MkI\<cdot>k)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
j + 1 \<le> k

goal (2 subgoals):
 1. j + 1 \<le> k \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) :@ supto\<cdot>(MkI\<cdot>(j + 1))\<cdot>(MkI\<cdot>k)
 2. \<not> j + 1 \<le> k \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) :@ supto\<cdot>(MkI\<cdot>(j + 1))\<cdot>(MkI\<cdot>k)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
i \<le> j
j \<le> k
j + 1 \<le> k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<le> j
j \<le> k
j + 1 \<le> k

goal (1 subgoal):
 1. supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) :@ supto\<cdot>(MkI\<cdot>(j + 1))\<cdot>(MkI\<cdot>k)
[PROOF STEP]
by (subst supto_split1[where j="j + 1" and k=k]; clarsimp simp: one_Integer_def)
[PROOF STATE]
proof (state)
this:
supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) :@ supto\<cdot>(MkI\<cdot>(j + 1))\<cdot>(MkI\<cdot>k)

goal (1 subgoal):
 1. \<not> j + 1 \<le> k \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) :@ supto\<cdot>(MkI\<cdot>(j + 1))\<cdot>(MkI\<cdot>k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> j + 1 \<le> k \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) :@ supto\<cdot>(MkI\<cdot>(j + 1))\<cdot>(MkI\<cdot>k)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> j + 1 \<le> k

goal (1 subgoal):
 1. \<not> j + 1 \<le> k \<Longrightarrow> supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) :@ supto\<cdot>(MkI\<cdot>(j + 1))\<cdot>(MkI\<cdot>k)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
i \<le> j
j \<le> k
\<not> j + 1 \<le> k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<le> j
j \<le> k
\<not> j + 1 \<le> k

goal (1 subgoal):
 1. supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) :@ supto\<cdot>(MkI\<cdot>(j + 1))\<cdot>(MkI\<cdot>k)
[PROOF STEP]
by (clarsimp simp: one_Integer_def not_le)
[PROOF STATE]
proof (state)
this:
supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>j) :@ supto\<cdot>(MkI\<cdot>(j + 1))\<cdot>(MkI\<cdot>k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma supto_split3: \<comment>\<open>From \<open>HOL.List\<close>\<close>
  assumes "i \<le> j"
  assumes "j \<le> k"
  shows "supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>(j - 1)) :@ MkI\<cdot>j :# supto\<cdot>(MkI\<cdot>(j + 1))\<cdot>(MkI\<cdot>k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>(j - 1)) :@ MkI\<cdot>j :# supto\<cdot>(MkI\<cdot>(j + 1))\<cdot>(MkI\<cdot>k)
[PROOF STEP]
using assms supto_simp(2) supto_split1
[PROOF STATE]
proof (prove)
using this:
i \<le> j
j \<le> k
?i \<le> ?j \<Longrightarrow> supto\<cdot>(MkI\<cdot>?i)\<cdot>(MkI\<cdot>?j) = MkI\<cdot>?i :# supto\<cdot>(MkI\<cdot>?i + 1)\<cdot>(MkI\<cdot>?j)
\<lbrakk>?i \<le> ?j; ?j \<le> ?k\<rbrakk> \<Longrightarrow> supto\<cdot>(MkI\<cdot>?i)\<cdot>(MkI\<cdot>?k) = supto\<cdot>(MkI\<cdot>?i)\<cdot>(MkI\<cdot>(?j - 1)) :@ supto\<cdot>(MkI\<cdot>?j)\<cdot>(MkI\<cdot>?k)

goal (1 subgoal):
 1. supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>k) = supto\<cdot>(MkI\<cdot>i)\<cdot>(MkI\<cdot>(j - 1)) :@ MkI\<cdot>j :# supto\<cdot>(MkI\<cdot>(j + 1))\<cdot>(MkI\<cdot>k)
[PROOF STEP]
by (metis one_Integer_def plus_MkI_MkI)


[STATEMENT]
lemma sinits_stake':
  shows "sinits\<cdot>xs = smap\<cdot>(\<Lambda> i. stake\<cdot>i\<cdot>xs)\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sinits\<cdot>xs = smap\<cdot>(\<Lambda> i. stake\<cdot>i\<cdot>xs)\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>xs))
[PROOF STEP]
proof(induct xs rule: srev_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. sinits\<cdot>\<bottom> = smap\<cdot>(\<Lambda> i. stake\<cdot>i\<cdot>\<bottom>)\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>\<bottom>))
 2. sinits\<cdot>[::] = smap\<cdot>(\<Lambda> i. stake\<cdot>i\<cdot>[::])\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>[::]))
 3. \<And>x xs. \<lbrakk>x \<noteq> \<bottom>; xs \<noteq> \<bottom>; sinits\<cdot>xs = smap\<cdot>(\<Lambda> i. stake\<cdot>i\<cdot>xs)\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>xs))\<rbrakk> \<Longrightarrow> sinits\<cdot>(xs :@ [:x:]) = smap\<cdot>(\<Lambda> i. stake\<cdot>i\<cdot>(xs :@ [:x:]))\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>(xs :@ [:x:])))
[PROOF STEP]
case (ssnoc x xs)
[PROOF STATE]
proof (state)
this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
sinits\<cdot>xs = smap\<cdot>(\<Lambda> i. stake\<cdot>i\<cdot>xs)\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>xs))

goal (3 subgoals):
 1. sinits\<cdot>\<bottom> = smap\<cdot>(\<Lambda> i. stake\<cdot>i\<cdot>\<bottom>)\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>\<bottom>))
 2. sinits\<cdot>[::] = smap\<cdot>(\<Lambda> i. stake\<cdot>i\<cdot>[::])\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>[::]))
 3. \<And>x xs. \<lbrakk>x \<noteq> \<bottom>; xs \<noteq> \<bottom>; sinits\<cdot>xs = smap\<cdot>(\<Lambda> i. stake\<cdot>i\<cdot>xs)\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>xs))\<rbrakk> \<Longrightarrow> sinits\<cdot>(xs :@ [:x:]) = smap\<cdot>(\<Lambda> i. stake\<cdot>i\<cdot>(xs :@ [:x:]))\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>(xs :@ [:x:])))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
sinits\<cdot>xs = smap\<cdot>(\<Lambda> i. stake\<cdot>i\<cdot>xs)\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>xs))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
sinits\<cdot>xs = smap\<cdot>(\<Lambda> i. stake\<cdot>i\<cdot>xs)\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>xs))

goal (1 subgoal):
 1. sinits\<cdot>(xs :@ [:x:]) = smap\<cdot>(\<Lambda> i. stake\<cdot>i\<cdot>(xs :@ [:x:]))\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>(xs :@ [:x:])))
[PROOF STEP]
apply (clarsimp simp: zero_Integer_def one_Integer_def stake_all
                simp del: supto_simp
                   elim!: slengthE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<noteq> \<bottom>; sinits\<cdot>xs = smap\<cdot>(\<Lambda> i. stake\<cdot>i\<cdot>xs)\<cdot>(supto\<cdot>(MkI\<cdot>0)\<cdot>(MkI\<cdot>(n - 1))) :@ [:xs:]; slength\<cdot>xs = MkI\<cdot>n; 0 \<le> n\<rbrakk> \<Longrightarrow> smap\<cdot>(\<Lambda> i. stake\<cdot>i\<cdot>xs)\<cdot>(supto\<cdot>(MkI\<cdot>0)\<cdot>(MkI\<cdot>(n - 1))) :@ [:xs, xs :@ [:x:]:] = smap\<cdot>(\<Lambda> i. stake\<cdot>i\<cdot>xs :@ (If le\<cdot>(i - MkI\<cdot>n)\<cdot>(MkI\<cdot>0) then [::] else x :# stake\<cdot>(i - MkI\<cdot>n - MkI\<cdot>1)\<cdot>[::]))\<cdot>(supto\<cdot>(MkI\<cdot>0)\<cdot>(MkI\<cdot>(n - 1))) :@ [:xs, xs :@ [:x:]:]
[PROOF STEP]
apply (rule arg_cong, rule smap_cong[OF refl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xa. \<lbrakk>x \<noteq> \<bottom>; sinits\<cdot>xs = smap\<cdot>(\<Lambda> i. stake\<cdot>i\<cdot>xs)\<cdot>(supto\<cdot>(MkI\<cdot>0)\<cdot>(MkI\<cdot>(n - 1))) :@ [:xs:]; slength\<cdot>xs = MkI\<cdot>n; 0 \<le> n; xa \<in> sset (supto\<cdot>(MkI\<cdot>0)\<cdot>(MkI\<cdot>(n - 1)))\<rbrakk> \<Longrightarrow> (\<Lambda> i. stake\<cdot>i\<cdot>xs)\<cdot>xa = (\<Lambda> i. stake\<cdot>i\<cdot>xs :@ (If le\<cdot>(i - MkI\<cdot>n)\<cdot>(MkI\<cdot>0) then [::] else x :# stake\<cdot>(i - MkI\<cdot>n - MkI\<cdot>1)\<cdot>[::]))\<cdot>xa
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
sinits\<cdot>(xs :@ [:x:]) = smap\<cdot>(\<Lambda> i. stake\<cdot>i\<cdot>(xs :@ [:x:]))\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>(xs :@ [:x:])))

goal (2 subgoals):
 1. sinits\<cdot>\<bottom> = smap\<cdot>(\<Lambda> i. stake\<cdot>i\<cdot>\<bottom>)\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>\<bottom>))
 2. sinits\<cdot>[::] = smap\<cdot>(\<Lambda> i. stake\<cdot>i\<cdot>[::])\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>[::]))
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma stails_sdrop':
  shows "stails\<cdot>xs = smap\<cdot>(\<Lambda> i. sdrop\<cdot>i\<cdot>xs)\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stails\<cdot>xs = smap\<cdot>(\<Lambda> i. sdrop\<cdot>i\<cdot>xs)\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>xs))
[PROOF STEP]
proof(induct xs rule: srev_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. stails\<cdot>\<bottom> = smap\<cdot>(\<Lambda> i. sdrop\<cdot>i\<cdot>\<bottom>)\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>\<bottom>))
 2. stails\<cdot>[::] = smap\<cdot>(\<Lambda> i. sdrop\<cdot>i\<cdot>[::])\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>[::]))
 3. \<And>x xs. \<lbrakk>x \<noteq> \<bottom>; xs \<noteq> \<bottom>; stails\<cdot>xs = smap\<cdot>(\<Lambda> i. sdrop\<cdot>i\<cdot>xs)\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>xs))\<rbrakk> \<Longrightarrow> stails\<cdot>(xs :@ [:x:]) = smap\<cdot>(\<Lambda> i. sdrop\<cdot>i\<cdot>(xs :@ [:x:]))\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>(xs :@ [:x:])))
[PROOF STEP]
case (ssnoc x xs)
[PROOF STATE]
proof (state)
this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
stails\<cdot>xs = smap\<cdot>(\<Lambda> i. sdrop\<cdot>i\<cdot>xs)\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>xs))

goal (3 subgoals):
 1. stails\<cdot>\<bottom> = smap\<cdot>(\<Lambda> i. sdrop\<cdot>i\<cdot>\<bottom>)\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>\<bottom>))
 2. stails\<cdot>[::] = smap\<cdot>(\<Lambda> i. sdrop\<cdot>i\<cdot>[::])\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>[::]))
 3. \<And>x xs. \<lbrakk>x \<noteq> \<bottom>; xs \<noteq> \<bottom>; stails\<cdot>xs = smap\<cdot>(\<Lambda> i. sdrop\<cdot>i\<cdot>xs)\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>xs))\<rbrakk> \<Longrightarrow> stails\<cdot>(xs :@ [:x:]) = smap\<cdot>(\<Lambda> i. sdrop\<cdot>i\<cdot>(xs :@ [:x:]))\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>(xs :@ [:x:])))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
stails\<cdot>xs = smap\<cdot>(\<Lambda> i. sdrop\<cdot>i\<cdot>xs)\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>xs))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
stails\<cdot>xs = smap\<cdot>(\<Lambda> i. sdrop\<cdot>i\<cdot>xs)\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>xs))

goal (1 subgoal):
 1. stails\<cdot>(xs :@ [:x:]) = smap\<cdot>(\<Lambda> i. sdrop\<cdot>i\<cdot>(xs :@ [:x:]))\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>(xs :@ [:x:])))
[PROOF STEP]
apply (clarsimp simp: zero_Integer_def one_Integer_def sdrop_all
                simp del: supto_simp
                   elim!: slengthE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<noteq> \<bottom>; stails\<cdot>xs = smap\<cdot>(\<Lambda> i. sdrop\<cdot>i\<cdot>xs)\<cdot>(supto\<cdot>(MkI\<cdot>0)\<cdot>(MkI\<cdot>(n - 1))) :@ [:[::]:]; slength\<cdot>xs = MkI\<cdot>n; 0 \<le> n\<rbrakk> \<Longrightarrow> smap\<cdot>((\<Lambda> ys. ys :@ [:x:]) oo (\<Lambda> i. sdrop\<cdot>i\<cdot>xs))\<cdot>(supto\<cdot>(MkI\<cdot>0)\<cdot>(MkI\<cdot>(n - 1))) :@ [:[:x:], [::]:] = smap\<cdot>(\<Lambda> i. sdrop\<cdot>i\<cdot>xs :@ sdrop\<cdot>(i - MkI\<cdot>n)\<cdot>[:x:])\<cdot>(supto\<cdot>(MkI\<cdot>0)\<cdot>(MkI\<cdot>(n - 1))) :@ [:[:x:], [::]:]
[PROOF STEP]
apply (rule arg_cong, rule smap_cong[OF refl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xa. \<lbrakk>x \<noteq> \<bottom>; stails\<cdot>xs = smap\<cdot>(\<Lambda> i. sdrop\<cdot>i\<cdot>xs)\<cdot>(supto\<cdot>(MkI\<cdot>0)\<cdot>(MkI\<cdot>(n - 1))) :@ [:[::]:]; slength\<cdot>xs = MkI\<cdot>n; 0 \<le> n; xa \<in> sset (supto\<cdot>(MkI\<cdot>0)\<cdot>(MkI\<cdot>(n - 1)))\<rbrakk> \<Longrightarrow> ((\<Lambda> ys. ys :@ [:x:]) oo (\<Lambda> i. sdrop\<cdot>i\<cdot>xs))\<cdot>xa = (\<Lambda> i. sdrop\<cdot>i\<cdot>xs :@ sdrop\<cdot>(i - MkI\<cdot>n)\<cdot>[:x:])\<cdot>xa
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n k. \<lbrakk>x \<noteq> \<bottom>; stails\<cdot>xs = xs :# smap\<cdot>(\<Lambda> i. sdrop\<cdot>i\<cdot>xs)\<cdot>(supto\<cdot>1\<cdot>(MkI\<cdot>(n - 1))) :@ [:[::]:]; slength\<cdot>xs = MkI\<cdot>n; 0 \<le> k; k < n\<rbrakk> \<Longrightarrow> sdrop\<cdot>(MkI\<cdot>k)\<cdot>xs :@ [:x:] = sdrop\<cdot>(MkI\<cdot>k)\<cdot>xs :@ sdrop\<cdot>(MkI\<cdot>(k - n))\<cdot>[:x:]
[PROOF STEP]
apply (subst (3) sdrop_neg; fastforce simp: zero_Integer_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
stails\<cdot>(xs :@ [:x:]) = smap\<cdot>(\<Lambda> i. sdrop\<cdot>i\<cdot>(xs :@ [:x:]))\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>(xs :@ [:x:])))

goal (2 subgoals):
 1. stails\<cdot>\<bottom> = smap\<cdot>(\<Lambda> i. sdrop\<cdot>i\<cdot>\<bottom>)\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>\<bottom>))
 2. stails\<cdot>[::] = smap\<cdot>(\<Lambda> i. sdrop\<cdot>i\<cdot>[::])\<cdot>(supto\<cdot>0\<cdot>(slength\<cdot>[::]))
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma sdrop_elem_stails[iff]:
  assumes "xs \<noteq> \<bottom>"
  shows "sdrop\<cdot>(MkI\<cdot>i)\<cdot>xs \<in> sset (stails\<cdot>xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sdrop\<cdot>(MkI\<cdot>i)\<cdot>xs \<in> sset (stails\<cdot>xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> \<bottom>

goal (1 subgoal):
 1. sdrop\<cdot>(MkI\<cdot>i)\<cdot>xs \<in> sset (stails\<cdot>xs)
[PROOF STEP]
by (clarsimp simp: stails_sdrop' zero_Integer_def one_Integer_def elim!: slengthE)
   (metis add.left_neutral le_MkI_MkI le_cases not_less sdrop_all sdrop_neg zero_Integer_def zless_imp_add1_zle)


[STATEMENT]
lemma slast_strict[simp]:
  "slast\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slast\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by fixrec_simp


[STATEMENT]
lemma slast_singleton[simp]: "slast\<cdot>[:x:] = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slast\<cdot>[:x:] = x
[PROOF STEP]
by (cases "x = \<bottom>"; simp)


[STATEMENT]
lemma slast_sappend_ssnoc[simp]:
  assumes "xs \<noteq> \<bottom>"
  shows "slast\<cdot>(xs :@ [:x:]) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slast\<cdot>(xs :@ [:x:]) = x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> \<bottom>

goal (1 subgoal):
 1. slast\<cdot>(xs :@ [:x:]) = x
[PROOF STEP]
proof(induct xs)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<bottom> \<noteq> \<bottom> \<Longrightarrow> slast\<cdot>(\<bottom> :@ [:x:]) = x
 2. [::] \<noteq> \<bottom> \<Longrightarrow> slast\<cdot>([::] :@ [:x:]) = x
 3. \<And>a xs. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; xs \<noteq> \<bottom> \<Longrightarrow> slast\<cdot>(xs :@ [:x:]) = x; a :# xs \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> slast\<cdot>((a :# xs) :@ [:x:]) = x
[PROOF STEP]
case (scons y ys)
[PROOF STATE]
proof (state)
this:
y \<noteq> \<bottom>
ys \<noteq> \<bottom>
ys \<noteq> \<bottom> \<Longrightarrow> slast\<cdot>(ys :@ [:x:]) = x
y :# ys \<noteq> \<bottom>

goal (3 subgoals):
 1. \<bottom> \<noteq> \<bottom> \<Longrightarrow> slast\<cdot>(\<bottom> :@ [:x:]) = x
 2. [::] \<noteq> \<bottom> \<Longrightarrow> slast\<cdot>([::] :@ [:x:]) = x
 3. \<And>a xs. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; xs \<noteq> \<bottom> \<Longrightarrow> slast\<cdot>(xs :@ [:x:]) = x; a :# xs \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> slast\<cdot>((a :# xs) :@ [:x:]) = x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<noteq> \<bottom>
ys \<noteq> \<bottom>
ys \<noteq> \<bottom> \<Longrightarrow> slast\<cdot>(ys :@ [:x:]) = x
y :# ys \<noteq> \<bottom>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
y \<noteq> \<bottom>
ys \<noteq> \<bottom>
ys \<noteq> \<bottom> \<Longrightarrow> slast\<cdot>(ys :@ [:x:]) = x
y :# ys \<noteq> \<bottom>

goal (1 subgoal):
 1. slast\<cdot>((y :# ys) :@ [:x:]) = x
[PROOF STEP]
by (cases "x = \<bottom>"; simp; cases ys; simp)
[PROOF STATE]
proof (state)
this:
slast\<cdot>((y :# ys) :@ [:x:]) = x

goal (2 subgoals):
 1. \<bottom> \<noteq> \<bottom> \<Longrightarrow> slast\<cdot>(\<bottom> :@ [:x:]) = x
 2. [::] \<noteq> \<bottom> \<Longrightarrow> slast\<cdot>([::] :@ [:x:]) = x
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma sbutlast_strict[simp]:
  "sbutlast\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sbutlast\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by fixrec_simp


[STATEMENT]
lemma sbutlast_sappend_ssnoc[simp]:
  assumes "x \<noteq> \<bottom>"
  shows "sbutlast\<cdot>(xs :@ [:x:]) = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sbutlast\<cdot>(xs :@ [:x:]) = xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<noteq> \<bottom>

goal (1 subgoal):
 1. sbutlast\<cdot>(xs :@ [:x:]) = xs
[PROOF STEP]
proof(induct xs)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. x \<noteq> \<bottom> \<Longrightarrow> sbutlast\<cdot>(\<bottom> :@ [:x:]) = \<bottom>
 2. x \<noteq> \<bottom> \<Longrightarrow> sbutlast\<cdot>([::] :@ [:x:]) = [::]
 3. \<And>a xs. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; x \<noteq> \<bottom> \<Longrightarrow> sbutlast\<cdot>(xs :@ [:x:]) = xs; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> sbutlast\<cdot>((a :# xs) :@ [:x:]) = a :# xs
[PROOF STEP]
case (scons y ys)
[PROOF STATE]
proof (state)
this:
y \<noteq> \<bottom>
ys \<noteq> \<bottom>
x \<noteq> \<bottom> \<Longrightarrow> sbutlast\<cdot>(ys :@ [:x:]) = ys
x \<noteq> \<bottom>

goal (3 subgoals):
 1. x \<noteq> \<bottom> \<Longrightarrow> sbutlast\<cdot>(\<bottom> :@ [:x:]) = \<bottom>
 2. x \<noteq> \<bottom> \<Longrightarrow> sbutlast\<cdot>([::] :@ [:x:]) = [::]
 3. \<And>a xs. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; x \<noteq> \<bottom> \<Longrightarrow> sbutlast\<cdot>(xs :@ [:x:]) = xs; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> sbutlast\<cdot>((a :# xs) :@ [:x:]) = a :# xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<noteq> \<bottom>
ys \<noteq> \<bottom>
x \<noteq> \<bottom> \<Longrightarrow> sbutlast\<cdot>(ys :@ [:x:]) = ys
x \<noteq> \<bottom>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
y \<noteq> \<bottom>
ys \<noteq> \<bottom>
x \<noteq> \<bottom> \<Longrightarrow> sbutlast\<cdot>(ys :@ [:x:]) = ys
x \<noteq> \<bottom>

goal (1 subgoal):
 1. sbutlast\<cdot>((y :# ys) :@ [:x:]) = y :# ys
[PROOF STEP]
by (cases ys; simp)
[PROOF STATE]
proof (state)
this:
sbutlast\<cdot>((y :# ys) :@ [:x:]) = y :# ys

goal (2 subgoals):
 1. x \<noteq> \<bottom> \<Longrightarrow> sbutlast\<cdot>(\<bottom> :@ [:x:]) = \<bottom>
 2. x \<noteq> \<bottom> \<Longrightarrow> sbutlast\<cdot>([::] :@ [:x:]) = [::]
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma prefix_strict[simp]: "prefix\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by (clarsimp simp: cfun_eq_iff) fixrec_simp


[STATEMENT]
lemma prefix_bottom_iff[simp]: "(prefix\<cdot>xs\<cdot>ys = \<bottom>) \<longleftrightarrow> (xs = \<bottom> \<or> ys = \<bottom>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (prefix\<cdot>xs\<cdot>ys = \<bottom>) = (xs = \<bottom> \<or> ys = \<bottom>)
[PROOF STEP]
proof(induct xs arbitrary: ys)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>ys. (prefix\<cdot>\<bottom>\<cdot>ys = \<bottom>) = (\<bottom> = \<bottom> \<or> ys = \<bottom>)
 2. \<And>ys. (prefix\<cdot>[::]\<cdot>ys = \<bottom>) = ([::] = \<bottom> \<or> ys = \<bottom>)
 3. \<And>a xs ys. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>ys. (prefix\<cdot>xs\<cdot>ys = \<bottom>) = (xs = \<bottom> \<or> ys = \<bottom>)\<rbrakk> \<Longrightarrow> (prefix\<cdot>(a :# xs)\<cdot>ys = \<bottom>) = (a :# xs = \<bottom> \<or> ys = \<bottom>)
[PROOF STEP]
case (snil ys)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>ys. (prefix\<cdot>\<bottom>\<cdot>ys = \<bottom>) = (\<bottom> = \<bottom> \<or> ys = \<bottom>)
 2. \<And>ys. (prefix\<cdot>[::]\<cdot>ys = \<bottom>) = ([::] = \<bottom> \<or> ys = \<bottom>)
 3. \<And>a xs ys. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>ys. (prefix\<cdot>xs\<cdot>ys = \<bottom>) = (xs = \<bottom> \<or> ys = \<bottom>)\<rbrakk> \<Longrightarrow> (prefix\<cdot>(a :# xs)\<cdot>ys = \<bottom>) = (a :# xs = \<bottom> \<or> ys = \<bottom>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (prefix\<cdot>[::]\<cdot>ys = \<bottom>) = ([::] = \<bottom> \<or> ys = \<bottom>)
[PROOF STEP]
by (cases ys) simp_all
[PROOF STATE]
proof (state)
this:
(prefix\<cdot>[::]\<cdot>ys = \<bottom>) = ([::] = \<bottom> \<or> ys = \<bottom>)

goal (2 subgoals):
 1. \<And>ys. (prefix\<cdot>\<bottom>\<cdot>ys = \<bottom>) = (\<bottom> = \<bottom> \<or> ys = \<bottom>)
 2. \<And>a xs ys. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>ys. (prefix\<cdot>xs\<cdot>ys = \<bottom>) = (xs = \<bottom> \<or> ys = \<bottom>)\<rbrakk> \<Longrightarrow> (prefix\<cdot>(a :# xs)\<cdot>ys = \<bottom>) = (a :# xs = \<bottom> \<or> ys = \<bottom>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ys. (prefix\<cdot>\<bottom>\<cdot>ys = \<bottom>) = (\<bottom> = \<bottom> \<or> ys = \<bottom>)
 2. \<And>a xs ys. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>ys. (prefix\<cdot>xs\<cdot>ys = \<bottom>) = (xs = \<bottom> \<or> ys = \<bottom>)\<rbrakk> \<Longrightarrow> (prefix\<cdot>(a :# xs)\<cdot>ys = \<bottom>) = (a :# xs = \<bottom> \<or> ys = \<bottom>)
[PROOF STEP]
case (scons a xs)
[PROOF STATE]
proof (state)
this:
a \<noteq> \<bottom>
xs \<noteq> \<bottom>
(prefix\<cdot>xs\<cdot>?ys = \<bottom>) = (xs = \<bottom> \<or> ?ys = \<bottom>)

goal (2 subgoals):
 1. \<And>ys. (prefix\<cdot>\<bottom>\<cdot>ys = \<bottom>) = (\<bottom> = \<bottom> \<or> ys = \<bottom>)
 2. \<And>a xs ys. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>ys. (prefix\<cdot>xs\<cdot>ys = \<bottom>) = (xs = \<bottom> \<or> ys = \<bottom>)\<rbrakk> \<Longrightarrow> (prefix\<cdot>(a :# xs)\<cdot>ys = \<bottom>) = (a :# xs = \<bottom> \<or> ys = \<bottom>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> \<bottom>
xs \<noteq> \<bottom>
(prefix\<cdot>xs\<cdot>?ys = \<bottom>) = (xs = \<bottom> \<or> ?ys = \<bottom>)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
a \<noteq> \<bottom>
xs \<noteq> \<bottom>
(prefix\<cdot>xs\<cdot>?ys = \<bottom>) = (xs = \<bottom> \<or> ?ys = \<bottom>)

goal (1 subgoal):
 1. (prefix\<cdot>(a :# xs)\<cdot>ys = \<bottom>) = (a :# xs = \<bottom> \<or> ys = \<bottom>)
[PROOF STEP]
by (cases ys) simp_all
[PROOF STATE]
proof (state)
this:
(prefix\<cdot>(a :# xs)\<cdot>ys = \<bottom>) = (a :# xs = \<bottom> \<or> ys = \<bottom>)

goal (1 subgoal):
 1. \<And>ys. (prefix\<cdot>\<bottom>\<cdot>ys = \<bottom>) = (\<bottom> = \<bottom> \<or> ys = \<bottom>)
[PROOF STEP]
qed simp


[STATEMENT]
lemma prefix_definedD:
  assumes "prefix\<cdot>xs\<cdot>ys = TT"
  shows "xs \<noteq> \<bottom> \<and> ys \<noteq> \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<noteq> \<bottom> \<and> ys \<noteq> \<bottom>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prefix\<cdot>xs\<cdot>ys = TT

goal (1 subgoal):
 1. xs \<noteq> \<bottom> \<and> ys \<noteq> \<bottom>
[PROOF STEP]
by (induct xs arbitrary: ys) auto


[STATEMENT]
lemma prefix_refl[simp]:
  assumes "xs \<noteq> \<bottom>"
  shows "prefix\<cdot>xs\<cdot>xs = TT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix\<cdot>xs\<cdot>xs = TT
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> \<bottom>

goal (1 subgoal):
 1. prefix\<cdot>xs\<cdot>xs = TT
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma prefix_refl_conv[simp]: "(prefix\<cdot>xs\<cdot>xs = TT) \<longleftrightarrow> (xs \<noteq> \<bottom>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (prefix\<cdot>xs\<cdot>xs = TT) = (xs \<noteq> \<bottom>)
[PROOF STEP]
by auto


[STATEMENT]
lemma  prefix_of_snil[simp]: "prefix\<cdot>xs\<cdot>[::] = (case xs of [::] \<Rightarrow> TT | x :# xs \<Rightarrow> FF)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix\<cdot>xs\<cdot>[::] = (case xs of [::] \<Rightarrow> TT | x :# xs \<Rightarrow> FF)
[PROOF STEP]
by (cases xs) simp_all


[STATEMENT]
lemma prefix_singleton_TT:
  shows "prefix\<cdot>[:x:]\<cdot>ys = TT \<longleftrightarrow> (x \<noteq> \<bottom> \<and> (\<exists>zs. zs \<noteq> \<bottom> \<and> ys = x :# zs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (prefix\<cdot>[:x:]\<cdot>ys = TT) = (x \<noteq> \<bottom> \<and> (\<exists>zs. zs \<noteq> \<bottom> \<and> ys = x :# zs))
[PROOF STEP]
by (cases "x = \<bottom>"; clarsimp; cases ys; fastforce)


[STATEMENT]
lemma prefix_singleton_FF:
  shows "prefix\<cdot>[:x:]\<cdot>ys = FF \<longleftrightarrow> (x \<noteq> \<bottom> \<and> (ys = [::] \<or> (\<exists>z zs. z \<noteq> \<bottom> \<and> zs \<noteq> \<bottom> \<and> ys = z :# zs \<and> x \<noteq> z)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (prefix\<cdot>[:x:]\<cdot>ys = FF) = (x \<noteq> \<bottom> \<and> (ys = [::] \<or> (\<exists>z zs. z \<noteq> \<bottom> \<and> zs \<noteq> \<bottom> \<and> ys = z :# zs \<and> x \<noteq> z)))
[PROOF STEP]
by (cases "x = \<bottom>"; clarsimp; cases ys; fastforce)


[STATEMENT]
lemma prefix_FF_not_snilD:
  assumes "prefix\<cdot>xs\<cdot>ys = FF"
  shows "xs \<noteq> [::]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [::]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prefix\<cdot>xs\<cdot>ys = FF

goal (1 subgoal):
 1. xs \<noteq> [::]
[PROOF STEP]
by (cases xs; cases ys; simp)


[STATEMENT]
lemma prefix_slength:
  assumes "prefix\<cdot>xs\<cdot>ys = TT"
  shows "le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>ys) = TT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>ys) = TT
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prefix\<cdot>xs\<cdot>ys = TT

goal (1 subgoal):
 1. le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>ys) = TT
[PROOF STEP]
proof(induct ys arbitrary: xs)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>xs. prefix\<cdot>xs\<cdot>\<bottom> = TT \<Longrightarrow> le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>\<bottom>) = TT
 2. \<And>xs. prefix\<cdot>xs\<cdot>[::] = TT \<Longrightarrow> le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>[::]) = TT
 3. \<And>a ys xs. \<lbrakk>a \<noteq> \<bottom>; ys \<noteq> \<bottom>; \<And>xs. prefix\<cdot>xs\<cdot>ys = TT \<Longrightarrow> le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>ys) = TT; prefix\<cdot>xs\<cdot>(a :# ys) = TT\<rbrakk> \<Longrightarrow> le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>(a :# ys)) = TT
[PROOF STEP]
case (snil xs)
[PROOF STATE]
proof (state)
this:
prefix\<cdot>xs\<cdot>[::] = TT

goal (3 subgoals):
 1. \<And>xs. prefix\<cdot>xs\<cdot>\<bottom> = TT \<Longrightarrow> le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>\<bottom>) = TT
 2. \<And>xs. prefix\<cdot>xs\<cdot>[::] = TT \<Longrightarrow> le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>[::]) = TT
 3. \<And>a ys xs. \<lbrakk>a \<noteq> \<bottom>; ys \<noteq> \<bottom>; \<And>xs. prefix\<cdot>xs\<cdot>ys = TT \<Longrightarrow> le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>ys) = TT; prefix\<cdot>xs\<cdot>(a :# ys) = TT\<rbrakk> \<Longrightarrow> le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>(a :# ys)) = TT
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prefix\<cdot>xs\<cdot>[::] = TT
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
prefix\<cdot>xs\<cdot>[::] = TT

goal (1 subgoal):
 1. le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>[::]) = TT
[PROOF STEP]
by (cases xs) simp_all
[PROOF STATE]
proof (state)
this:
le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>[::]) = TT

goal (2 subgoals):
 1. \<And>xs. prefix\<cdot>xs\<cdot>\<bottom> = TT \<Longrightarrow> le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>\<bottom>) = TT
 2. \<And>a ys xs. \<lbrakk>a \<noteq> \<bottom>; ys \<noteq> \<bottom>; \<And>xs. prefix\<cdot>xs\<cdot>ys = TT \<Longrightarrow> le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>ys) = TT; prefix\<cdot>xs\<cdot>(a :# ys) = TT\<rbrakk> \<Longrightarrow> le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>(a :# ys)) = TT
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs. prefix\<cdot>xs\<cdot>\<bottom> = TT \<Longrightarrow> le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>\<bottom>) = TT
 2. \<And>a ys xs. \<lbrakk>a \<noteq> \<bottom>; ys \<noteq> \<bottom>; \<And>xs. prefix\<cdot>xs\<cdot>ys = TT \<Longrightarrow> le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>ys) = TT; prefix\<cdot>xs\<cdot>(a :# ys) = TT\<rbrakk> \<Longrightarrow> le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>(a :# ys)) = TT
[PROOF STEP]
case (scons a ys)
[PROOF STATE]
proof (state)
this:
a \<noteq> \<bottom>
ys \<noteq> \<bottom>
prefix\<cdot>?xs\<cdot>ys = TT \<Longrightarrow> le\<cdot>(slength\<cdot>?xs)\<cdot>(slength\<cdot>ys) = TT
prefix\<cdot>xs\<cdot>(a :# ys) = TT

goal (2 subgoals):
 1. \<And>xs. prefix\<cdot>xs\<cdot>\<bottom> = TT \<Longrightarrow> le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>\<bottom>) = TT
 2. \<And>a ys xs. \<lbrakk>a \<noteq> \<bottom>; ys \<noteq> \<bottom>; \<And>xs. prefix\<cdot>xs\<cdot>ys = TT \<Longrightarrow> le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>ys) = TT; prefix\<cdot>xs\<cdot>(a :# ys) = TT\<rbrakk> \<Longrightarrow> le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>(a :# ys)) = TT
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> \<bottom>
ys \<noteq> \<bottom>
prefix\<cdot>?xs\<cdot>ys = TT \<Longrightarrow> le\<cdot>(slength\<cdot>?xs)\<cdot>(slength\<cdot>ys) = TT
prefix\<cdot>xs\<cdot>(a :# ys) = TT
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
a \<noteq> \<bottom>
ys \<noteq> \<bottom>
prefix\<cdot>?xs\<cdot>ys = TT \<Longrightarrow> le\<cdot>(slength\<cdot>?xs)\<cdot>(slength\<cdot>ys) = TT
prefix\<cdot>xs\<cdot>(a :# ys) = TT

goal (1 subgoal):
 1. le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>(a :# ys)) = TT
[PROOF STEP]
by (cases xs) (simp_all add: le_plus_1)
[PROOF STATE]
proof (state)
this:
le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>(a :# ys)) = TT

goal (1 subgoal):
 1. \<And>xs. prefix\<cdot>xs\<cdot>\<bottom> = TT \<Longrightarrow> le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>\<bottom>) = TT
[PROOF STEP]
qed simp


[STATEMENT]
lemma prefix_slength_strengthen: "prefix\<cdot>xs\<cdot>ys = (le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>ys) andalso prefix\<cdot>xs\<cdot>ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix\<cdot>xs\<cdot>ys = (le\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>ys) andalso prefix\<cdot>xs\<cdot>ys)
[PROOF STEP]
by (rule andalso_weaken_left) (auto dest: prefix_slength)


[STATEMENT]
lemma prefix_scons_snil[simp]: "prefix\<cdot>(x :# xs)\<cdot>[::] \<noteq> TT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix\<cdot>(x :# xs)\<cdot>[::] \<noteq> TT
[PROOF STEP]
by (cases "x :# xs \<noteq> \<bottom>") auto


[STATEMENT]
lemma scons_prefix_scons[simp]:
  "(prefix\<cdot>(x :# xs)\<cdot>(y :# ys) = TT) \<longleftrightarrow> (eq\<cdot>x\<cdot>y = TT \<and> prefix\<cdot>xs\<cdot>ys = TT)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (prefix\<cdot>(x :# xs)\<cdot>(y :# ys) = TT) = (eq\<cdot>x\<cdot>y = TT \<and> prefix\<cdot>xs\<cdot>ys = TT)
[PROOF STEP]
by (cases "x :# xs \<noteq> \<bottom> \<and> y :# ys \<noteq> \<bottom>") auto


[STATEMENT]
lemma append_prefixD:
  assumes "prefix\<cdot>(xs :@ ys)\<cdot>zs = TT"
  shows "prefix\<cdot>xs\<cdot>zs = TT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix\<cdot>xs\<cdot>zs = TT
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prefix\<cdot>(xs :@ ys)\<cdot>zs = TT

goal (1 subgoal):
 1. prefix\<cdot>xs\<cdot>zs = TT
[PROOF STEP]
proof(induct xs arbitrary: zs)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>zs. prefix\<cdot>(\<bottom> :@ ys)\<cdot>zs = TT \<Longrightarrow> prefix\<cdot>\<bottom>\<cdot>zs = TT
 2. \<And>zs. prefix\<cdot>([::] :@ ys)\<cdot>zs = TT \<Longrightarrow> prefix\<cdot>[::]\<cdot>zs = TT
 3. \<And>a xs zs. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>zs. prefix\<cdot>(xs :@ ys)\<cdot>zs = TT \<Longrightarrow> prefix\<cdot>xs\<cdot>zs = TT; prefix\<cdot>((a :# xs) :@ ys)\<cdot>zs = TT\<rbrakk> \<Longrightarrow> prefix\<cdot>(a :# xs)\<cdot>zs = TT
[PROOF STEP]
case (snil zs)
[PROOF STATE]
proof (state)
this:
prefix\<cdot>([::] :@ ys)\<cdot>zs = TT

goal (3 subgoals):
 1. \<And>zs. prefix\<cdot>(\<bottom> :@ ys)\<cdot>zs = TT \<Longrightarrow> prefix\<cdot>\<bottom>\<cdot>zs = TT
 2. \<And>zs. prefix\<cdot>([::] :@ ys)\<cdot>zs = TT \<Longrightarrow> prefix\<cdot>[::]\<cdot>zs = TT
 3. \<And>a xs zs. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>zs. prefix\<cdot>(xs :@ ys)\<cdot>zs = TT \<Longrightarrow> prefix\<cdot>xs\<cdot>zs = TT; prefix\<cdot>((a :# xs) :@ ys)\<cdot>zs = TT\<rbrakk> \<Longrightarrow> prefix\<cdot>(a :# xs)\<cdot>zs = TT
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prefix\<cdot>([::] :@ ys)\<cdot>zs = TT
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
prefix\<cdot>([::] :@ ys)\<cdot>zs = TT

goal (1 subgoal):
 1. prefix\<cdot>[::]\<cdot>zs = TT
[PROOF STEP]
using prefix.simps(2)
[PROOF STATE]
proof (prove)
using this:
prefix\<cdot>([::] :@ ys)\<cdot>zs = TT
?ys \<noteq> \<bottom> \<Longrightarrow> prefix\<cdot>[::]\<cdot>?ys = TT

goal (1 subgoal):
 1. prefix\<cdot>[::]\<cdot>zs = TT
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
prefix\<cdot>[::]\<cdot>zs = TT

goal (2 subgoals):
 1. \<And>zs. prefix\<cdot>(\<bottom> :@ ys)\<cdot>zs = TT \<Longrightarrow> prefix\<cdot>\<bottom>\<cdot>zs = TT
 2. \<And>a xs zs. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>zs. prefix\<cdot>(xs :@ ys)\<cdot>zs = TT \<Longrightarrow> prefix\<cdot>xs\<cdot>zs = TT; prefix\<cdot>((a :# xs) :@ ys)\<cdot>zs = TT\<rbrakk> \<Longrightarrow> prefix\<cdot>(a :# xs)\<cdot>zs = TT
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>zs. prefix\<cdot>(\<bottom> :@ ys)\<cdot>zs = TT \<Longrightarrow> prefix\<cdot>\<bottom>\<cdot>zs = TT
 2. \<And>a xs zs. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>zs. prefix\<cdot>(xs :@ ys)\<cdot>zs = TT \<Longrightarrow> prefix\<cdot>xs\<cdot>zs = TT; prefix\<cdot>((a :# xs) :@ ys)\<cdot>zs = TT\<rbrakk> \<Longrightarrow> prefix\<cdot>(a :# xs)\<cdot>zs = TT
[PROOF STEP]
case (scons x xs zs)
[PROOF STATE]
proof (state)
this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
prefix\<cdot>(xs :@ ys)\<cdot>?zs = TT \<Longrightarrow> prefix\<cdot>xs\<cdot>?zs = TT
prefix\<cdot>((x :# xs) :@ ys)\<cdot>zs = TT

goal (2 subgoals):
 1. \<And>zs. prefix\<cdot>(\<bottom> :@ ys)\<cdot>zs = TT \<Longrightarrow> prefix\<cdot>\<bottom>\<cdot>zs = TT
 2. \<And>a xs zs. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>zs. prefix\<cdot>(xs :@ ys)\<cdot>zs = TT \<Longrightarrow> prefix\<cdot>xs\<cdot>zs = TT; prefix\<cdot>((a :# xs) :@ ys)\<cdot>zs = TT\<rbrakk> \<Longrightarrow> prefix\<cdot>(a :# xs)\<cdot>zs = TT
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
prefix\<cdot>(xs :@ ys)\<cdot>?zs = TT \<Longrightarrow> prefix\<cdot>xs\<cdot>?zs = TT
prefix\<cdot>((x :# xs) :@ ys)\<cdot>zs = TT
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
prefix\<cdot>(xs :@ ys)\<cdot>?zs = TT \<Longrightarrow> prefix\<cdot>xs\<cdot>?zs = TT
prefix\<cdot>((x :# xs) :@ ys)\<cdot>zs = TT

goal (1 subgoal):
 1. prefix\<cdot>(x :# xs)\<cdot>zs = TT
[PROOF STEP]
by (metis prefix.simps(1) prefix_scons_snil sappend_scons scons_prefix_scons slist.exhaust)
[PROOF STATE]
proof (state)
this:
prefix\<cdot>(x :# xs)\<cdot>zs = TT

goal (1 subgoal):
 1. \<And>zs. prefix\<cdot>(\<bottom> :@ ys)\<cdot>zs = TT \<Longrightarrow> prefix\<cdot>\<bottom>\<cdot>zs = TT
[PROOF STEP]
qed simp


[STATEMENT]
lemma same_prefix_prefix[simp]:
  assumes "xs \<noteq> \<bottom>"
  shows "prefix\<cdot>(xs :@ ys)\<cdot>(xs :@ zs) = prefix\<cdot>ys\<cdot>zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix\<cdot>(xs :@ ys)\<cdot>(xs :@ zs) = prefix\<cdot>ys\<cdot>zs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> \<bottom>

goal (1 subgoal):
 1. prefix\<cdot>(xs :@ ys)\<cdot>(xs :@ zs) = prefix\<cdot>ys\<cdot>zs
[PROOF STEP]
proof(cases "ys = \<bottom>" "zs = \<bottom>" rule: bool.exhaust[case_product bool.exhaust])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>xs \<noteq> \<bottom>; (ys = \<bottom>) = True; (zs = \<bottom>) = True\<rbrakk> \<Longrightarrow> prefix\<cdot>(xs :@ ys)\<cdot>(xs :@ zs) = prefix\<cdot>ys\<cdot>zs
 2. \<lbrakk>xs \<noteq> \<bottom>; (ys = \<bottom>) = True; (zs = \<bottom>) = False\<rbrakk> \<Longrightarrow> prefix\<cdot>(xs :@ ys)\<cdot>(xs :@ zs) = prefix\<cdot>ys\<cdot>zs
 3. \<lbrakk>xs \<noteq> \<bottom>; (ys = \<bottom>) = False; (zs = \<bottom>) = True\<rbrakk> \<Longrightarrow> prefix\<cdot>(xs :@ ys)\<cdot>(xs :@ zs) = prefix\<cdot>ys\<cdot>zs
 4. \<lbrakk>xs \<noteq> \<bottom>; (ys = \<bottom>) = False; (zs = \<bottom>) = False\<rbrakk> \<Longrightarrow> prefix\<cdot>(xs :@ ys)\<cdot>(xs :@ zs) = prefix\<cdot>ys\<cdot>zs
[PROOF STEP]
case False_False
[PROOF STATE]
proof (state)
this:
(ys = \<bottom>) = False
(zs = \<bottom>) = False

goal (4 subgoals):
 1. \<lbrakk>xs \<noteq> \<bottom>; (ys = \<bottom>) = True; (zs = \<bottom>) = True\<rbrakk> \<Longrightarrow> prefix\<cdot>(xs :@ ys)\<cdot>(xs :@ zs) = prefix\<cdot>ys\<cdot>zs
 2. \<lbrakk>xs \<noteq> \<bottom>; (ys = \<bottom>) = True; (zs = \<bottom>) = False\<rbrakk> \<Longrightarrow> prefix\<cdot>(xs :@ ys)\<cdot>(xs :@ zs) = prefix\<cdot>ys\<cdot>zs
 3. \<lbrakk>xs \<noteq> \<bottom>; (ys = \<bottom>) = False; (zs = \<bottom>) = True\<rbrakk> \<Longrightarrow> prefix\<cdot>(xs :@ ys)\<cdot>(xs :@ zs) = prefix\<cdot>ys\<cdot>zs
 4. \<lbrakk>xs \<noteq> \<bottom>; (ys = \<bottom>) = False; (zs = \<bottom>) = False\<rbrakk> \<Longrightarrow> prefix\<cdot>(xs :@ ys)\<cdot>(xs :@ zs) = prefix\<cdot>ys\<cdot>zs
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
xs \<noteq> \<bottom>
(ys = \<bottom>) = False
(zs = \<bottom>) = False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> \<bottom>
(ys = \<bottom>) = False
(zs = \<bottom>) = False

goal (1 subgoal):
 1. prefix\<cdot>(xs :@ ys)\<cdot>(xs :@ zs) = prefix\<cdot>ys\<cdot>zs
[PROOF STEP]
by (induct xs) simp_all
[PROOF STATE]
proof (state)
this:
prefix\<cdot>(xs :@ ys)\<cdot>(xs :@ zs) = prefix\<cdot>ys\<cdot>zs

goal (3 subgoals):
 1. \<lbrakk>xs \<noteq> \<bottom>; (ys = \<bottom>) = True; (zs = \<bottom>) = True\<rbrakk> \<Longrightarrow> prefix\<cdot>(xs :@ ys)\<cdot>(xs :@ zs) = prefix\<cdot>ys\<cdot>zs
 2. \<lbrakk>xs \<noteq> \<bottom>; (ys = \<bottom>) = True; (zs = \<bottom>) = False\<rbrakk> \<Longrightarrow> prefix\<cdot>(xs :@ ys)\<cdot>(xs :@ zs) = prefix\<cdot>ys\<cdot>zs
 3. \<lbrakk>xs \<noteq> \<bottom>; (ys = \<bottom>) = False; (zs = \<bottom>) = True\<rbrakk> \<Longrightarrow> prefix\<cdot>(xs :@ ys)\<cdot>(xs :@ zs) = prefix\<cdot>ys\<cdot>zs
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma eq_prefix_TT:
  assumes "eq\<cdot>xs\<cdot>ys = TT"
  shows "prefix\<cdot>xs\<cdot>ys = TT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix\<cdot>xs\<cdot>ys = TT
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eq\<cdot>xs\<cdot>ys = TT

goal (1 subgoal):
 1. prefix\<cdot>xs\<cdot>ys = TT
[PROOF STEP]
by (induct xs arbitrary: ys) (case_tac ys; simp)+


[STATEMENT]
lemma prefix_eq_FF:
  assumes "prefix\<cdot>xs\<cdot>ys = FF"
  shows "eq\<cdot>xs\<cdot>ys = FF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq\<cdot>xs\<cdot>ys = FF
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prefix\<cdot>xs\<cdot>ys = FF

goal (1 subgoal):
 1. eq\<cdot>xs\<cdot>ys = FF
[PROOF STEP]
by (induct xs arbitrary: ys) (case_tac ys; auto)+


[STATEMENT]
lemma prefix_slength_eq:
  shows "eq\<cdot>xs\<cdot>ys = (eq\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>ys) andalso prefix\<cdot>xs\<cdot>ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq\<cdot>xs\<cdot>ys = (eq\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>ys) andalso prefix\<cdot>xs\<cdot>ys)
[PROOF STEP]
proof(induct xs arbitrary: ys)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>ys. eq\<cdot>\<bottom>\<cdot>ys = (eq\<cdot>(slength\<cdot>\<bottom>)\<cdot>(slength\<cdot>ys) andalso prefix\<cdot>\<bottom>\<cdot>ys)
 2. \<And>ys. eq\<cdot>[::]\<cdot>ys = (eq\<cdot>(slength\<cdot>[::])\<cdot>(slength\<cdot>ys) andalso prefix\<cdot>[::]\<cdot>ys)
 3. \<And>a xs ys. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>ys. eq\<cdot>xs\<cdot>ys = (eq\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>ys) andalso prefix\<cdot>xs\<cdot>ys)\<rbrakk> \<Longrightarrow> eq\<cdot>(a :# xs)\<cdot>ys = (eq\<cdot>(slength\<cdot>(a :# xs))\<cdot>(slength\<cdot>ys) andalso prefix\<cdot>(a :# xs)\<cdot>ys)
[PROOF STEP]
case (snil ys)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>ys. eq\<cdot>\<bottom>\<cdot>ys = (eq\<cdot>(slength\<cdot>\<bottom>)\<cdot>(slength\<cdot>ys) andalso prefix\<cdot>\<bottom>\<cdot>ys)
 2. \<And>ys. eq\<cdot>[::]\<cdot>ys = (eq\<cdot>(slength\<cdot>[::])\<cdot>(slength\<cdot>ys) andalso prefix\<cdot>[::]\<cdot>ys)
 3. \<And>a xs ys. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>ys. eq\<cdot>xs\<cdot>ys = (eq\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>ys) andalso prefix\<cdot>xs\<cdot>ys)\<rbrakk> \<Longrightarrow> eq\<cdot>(a :# xs)\<cdot>ys = (eq\<cdot>(slength\<cdot>(a :# xs))\<cdot>(slength\<cdot>ys) andalso prefix\<cdot>(a :# xs)\<cdot>ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq\<cdot>[::]\<cdot>ys = (eq\<cdot>(slength\<cdot>[::])\<cdot>(slength\<cdot>ys) andalso prefix\<cdot>[::]\<cdot>ys)
[PROOF STEP]
by (cases ys; clarsimp simp: one_Integer_def elim!: slengthE)
[PROOF STATE]
proof (state)
this:
eq\<cdot>[::]\<cdot>ys = (eq\<cdot>(slength\<cdot>[::])\<cdot>(slength\<cdot>ys) andalso prefix\<cdot>[::]\<cdot>ys)

goal (2 subgoals):
 1. \<And>ys. eq\<cdot>\<bottom>\<cdot>ys = (eq\<cdot>(slength\<cdot>\<bottom>)\<cdot>(slength\<cdot>ys) andalso prefix\<cdot>\<bottom>\<cdot>ys)
 2. \<And>a xs ys. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>ys. eq\<cdot>xs\<cdot>ys = (eq\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>ys) andalso prefix\<cdot>xs\<cdot>ys)\<rbrakk> \<Longrightarrow> eq\<cdot>(a :# xs)\<cdot>ys = (eq\<cdot>(slength\<cdot>(a :# xs))\<cdot>(slength\<cdot>ys) andalso prefix\<cdot>(a :# xs)\<cdot>ys)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ys. eq\<cdot>\<bottom>\<cdot>ys = (eq\<cdot>(slength\<cdot>\<bottom>)\<cdot>(slength\<cdot>ys) andalso prefix\<cdot>\<bottom>\<cdot>ys)
 2. \<And>a xs ys. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>ys. eq\<cdot>xs\<cdot>ys = (eq\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>ys) andalso prefix\<cdot>xs\<cdot>ys)\<rbrakk> \<Longrightarrow> eq\<cdot>(a :# xs)\<cdot>ys = (eq\<cdot>(slength\<cdot>(a :# xs))\<cdot>(slength\<cdot>ys) andalso prefix\<cdot>(a :# xs)\<cdot>ys)
[PROOF STEP]
case (scons x xs ys)
[PROOF STATE]
proof (state)
this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
eq\<cdot>xs\<cdot>?ys = (eq\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>?ys) andalso prefix\<cdot>xs\<cdot>?ys)

goal (2 subgoals):
 1. \<And>ys. eq\<cdot>\<bottom>\<cdot>ys = (eq\<cdot>(slength\<cdot>\<bottom>)\<cdot>(slength\<cdot>ys) andalso prefix\<cdot>\<bottom>\<cdot>ys)
 2. \<And>a xs ys. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>ys. eq\<cdot>xs\<cdot>ys = (eq\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>ys) andalso prefix\<cdot>xs\<cdot>ys)\<rbrakk> \<Longrightarrow> eq\<cdot>(a :# xs)\<cdot>ys = (eq\<cdot>(slength\<cdot>(a :# xs))\<cdot>(slength\<cdot>ys) andalso prefix\<cdot>(a :# xs)\<cdot>ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
eq\<cdot>xs\<cdot>?ys = (eq\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>?ys) andalso prefix\<cdot>xs\<cdot>?ys)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
eq\<cdot>xs\<cdot>?ys = (eq\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>?ys) andalso prefix\<cdot>xs\<cdot>?ys)

goal (1 subgoal):
 1. eq\<cdot>(x :# xs)\<cdot>ys = (eq\<cdot>(slength\<cdot>(x :# xs))\<cdot>(slength\<cdot>ys) andalso prefix\<cdot>(x :# xs)\<cdot>ys)
[PROOF STEP]
by (cases ys; clarsimp simp: zero_Integer_def one_Integer_def elim!: slengthE)
[PROOF STATE]
proof (state)
this:
eq\<cdot>(x :# xs)\<cdot>ys = (eq\<cdot>(slength\<cdot>(x :# xs))\<cdot>(slength\<cdot>ys) andalso prefix\<cdot>(x :# xs)\<cdot>ys)

goal (1 subgoal):
 1. \<And>ys. eq\<cdot>\<bottom>\<cdot>ys = (eq\<cdot>(slength\<cdot>\<bottom>)\<cdot>(slength\<cdot>ys) andalso prefix\<cdot>\<bottom>\<cdot>ys)
[PROOF STEP]
qed simp


[STATEMENT]
lemma stake_slength_plus_1:
  shows "stake\<cdot>(slength\<cdot>xs + 1)\<cdot>(y :# ys) = y :# stake\<cdot>(slength\<cdot>xs)\<cdot>ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stake\<cdot>(slength\<cdot>xs + 1)\<cdot>(y :# ys) = y :# stake\<cdot>(slength\<cdot>xs)\<cdot>ys
[PROOF STEP]
by (cases "xs = \<bottom>" "y = \<bottom>" "ys = \<bottom>" rule: bool.exhaust[case_product bool.exhaust bool.exhaust]; clarsimp)
   (auto simp: If2_def[symmetric] zero_Integer_def one_Integer_def split: If2_splits elim!: slengthE)


[STATEMENT]
lemma sdrop_slength_plus_1:
  assumes "y \<noteq> \<bottom>"
  shows "sdrop\<cdot>(slength\<cdot>xs + 1)\<cdot>(y :# ys) = sdrop\<cdot>(slength\<cdot>xs)\<cdot>ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sdrop\<cdot>(slength\<cdot>xs + 1)\<cdot>(y :# ys) = sdrop\<cdot>(slength\<cdot>xs)\<cdot>ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
y \<noteq> \<bottom>

goal (1 subgoal):
 1. sdrop\<cdot>(slength\<cdot>xs + 1)\<cdot>(y :# ys) = sdrop\<cdot>(slength\<cdot>xs)\<cdot>ys
[PROOF STEP]
by (subst sdrop.simps;
    cases "xs = \<bottom>"; clarsimp; cases "ys = \<bottom>";
    clarsimp simp: If2_def[symmetric] zero_Integer_def one_Integer_def split: If2_splits elim!: slengthE)


[STATEMENT]
lemma eq_take_length_prefix: "prefix\<cdot>xs\<cdot>ys = eq\<cdot>xs\<cdot>(stake\<cdot>(slength\<cdot>xs)\<cdot>ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix\<cdot>xs\<cdot>ys = eq\<cdot>xs\<cdot>(stake\<cdot>(slength\<cdot>xs)\<cdot>ys)
[PROOF STEP]
proof (induct xs arbitrary: ys)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>ys. prefix\<cdot>\<bottom>\<cdot>ys = eq\<cdot>\<bottom>\<cdot>(stake\<cdot>(slength\<cdot>\<bottom>)\<cdot>ys)
 2. \<And>ys. prefix\<cdot>[::]\<cdot>ys = eq\<cdot>[::]\<cdot>(stake\<cdot>(slength\<cdot>[::])\<cdot>ys)
 3. \<And>a xs ys. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>ys. prefix\<cdot>xs\<cdot>ys = eq\<cdot>xs\<cdot>(stake\<cdot>(slength\<cdot>xs)\<cdot>ys)\<rbrakk> \<Longrightarrow> prefix\<cdot>(a :# xs)\<cdot>ys = eq\<cdot>(a :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(a :# xs))\<cdot>ys)
[PROOF STEP]
case (snil ys)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>ys. prefix\<cdot>\<bottom>\<cdot>ys = eq\<cdot>\<bottom>\<cdot>(stake\<cdot>(slength\<cdot>\<bottom>)\<cdot>ys)
 2. \<And>ys. prefix\<cdot>[::]\<cdot>ys = eq\<cdot>[::]\<cdot>(stake\<cdot>(slength\<cdot>[::])\<cdot>ys)
 3. \<And>a xs ys. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>ys. prefix\<cdot>xs\<cdot>ys = eq\<cdot>xs\<cdot>(stake\<cdot>(slength\<cdot>xs)\<cdot>ys)\<rbrakk> \<Longrightarrow> prefix\<cdot>(a :# xs)\<cdot>ys = eq\<cdot>(a :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(a :# xs))\<cdot>ys)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix\<cdot>[::]\<cdot>ys = eq\<cdot>[::]\<cdot>(stake\<cdot>(slength\<cdot>[::])\<cdot>ys)
[PROOF STEP]
by (cases ys; clarsimp)
[PROOF STATE]
proof (state)
this:
prefix\<cdot>[::]\<cdot>ys = eq\<cdot>[::]\<cdot>(stake\<cdot>(slength\<cdot>[::])\<cdot>ys)

goal (2 subgoals):
 1. \<And>ys. prefix\<cdot>\<bottom>\<cdot>ys = eq\<cdot>\<bottom>\<cdot>(stake\<cdot>(slength\<cdot>\<bottom>)\<cdot>ys)
 2. \<And>a xs ys. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>ys. prefix\<cdot>xs\<cdot>ys = eq\<cdot>xs\<cdot>(stake\<cdot>(slength\<cdot>xs)\<cdot>ys)\<rbrakk> \<Longrightarrow> prefix\<cdot>(a :# xs)\<cdot>ys = eq\<cdot>(a :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(a :# xs))\<cdot>ys)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ys. prefix\<cdot>\<bottom>\<cdot>ys = eq\<cdot>\<bottom>\<cdot>(stake\<cdot>(slength\<cdot>\<bottom>)\<cdot>ys)
 2. \<And>a xs ys. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>ys. prefix\<cdot>xs\<cdot>ys = eq\<cdot>xs\<cdot>(stake\<cdot>(slength\<cdot>xs)\<cdot>ys)\<rbrakk> \<Longrightarrow> prefix\<cdot>(a :# xs)\<cdot>ys = eq\<cdot>(a :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(a :# xs))\<cdot>ys)
[PROOF STEP]
case (scons x xs ys)
[PROOF STATE]
proof (state)
this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
prefix\<cdot>xs\<cdot>?ys = eq\<cdot>xs\<cdot>(stake\<cdot>(slength\<cdot>xs)\<cdot>?ys)

goal (2 subgoals):
 1. \<And>ys. prefix\<cdot>\<bottom>\<cdot>ys = eq\<cdot>\<bottom>\<cdot>(stake\<cdot>(slength\<cdot>\<bottom>)\<cdot>ys)
 2. \<And>a xs ys. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>ys. prefix\<cdot>xs\<cdot>ys = eq\<cdot>xs\<cdot>(stake\<cdot>(slength\<cdot>xs)\<cdot>ys)\<rbrakk> \<Longrightarrow> prefix\<cdot>(a :# xs)\<cdot>ys = eq\<cdot>(a :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(a :# xs))\<cdot>ys)
[PROOF STEP]
note IH = this
[PROOF STATE]
proof (state)
this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
prefix\<cdot>xs\<cdot>?ys = eq\<cdot>xs\<cdot>(stake\<cdot>(slength\<cdot>xs)\<cdot>?ys)

goal (2 subgoals):
 1. \<And>ys. prefix\<cdot>\<bottom>\<cdot>ys = eq\<cdot>\<bottom>\<cdot>(stake\<cdot>(slength\<cdot>\<bottom>)\<cdot>ys)
 2. \<And>a xs ys. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; \<And>ys. prefix\<cdot>xs\<cdot>ys = eq\<cdot>xs\<cdot>(stake\<cdot>(slength\<cdot>xs)\<cdot>ys)\<rbrakk> \<Longrightarrow> prefix\<cdot>(a :# xs)\<cdot>ys = eq\<cdot>(a :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(a :# xs))\<cdot>ys)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
[PROOF STEP]
proof (cases "slength\<cdot>xs = \<bottom>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. slength\<cdot>xs = \<bottom> \<Longrightarrow> prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
 2. slength\<cdot>xs \<noteq> \<bottom> \<Longrightarrow> prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
slength\<cdot>xs = \<bottom>

goal (2 subgoals):
 1. slength\<cdot>xs = \<bottom> \<Longrightarrow> prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
 2. slength\<cdot>xs \<noteq> \<bottom> \<Longrightarrow> prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
slength\<cdot>xs = \<bottom>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
slength\<cdot>xs = \<bottom>

goal (1 subgoal):
 1. prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)

goal (1 subgoal):
 1. slength\<cdot>xs \<noteq> \<bottom> \<Longrightarrow> prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. slength\<cdot>xs \<noteq> \<bottom> \<Longrightarrow> prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
slength\<cdot>xs \<noteq> \<bottom>

goal (1 subgoal):
 1. slength\<cdot>xs \<noteq> \<bottom> \<Longrightarrow> prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
[PROOF STEP]
proof (cases ys)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ys = \<bottom> \<Longrightarrow> prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
 2. ys = [::] \<Longrightarrow> prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
 3. \<And>a slist. \<lbrakk>ys = a :# slist; a \<noteq> \<bottom>; slist \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
[PROOF STEP]
case bottom
[PROOF STATE]
proof (state)
this:
ys = \<bottom>

goal (3 subgoals):
 1. ys = \<bottom> \<Longrightarrow> prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
 2. ys = [::] \<Longrightarrow> prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
 3. \<And>a slist. \<lbrakk>ys = a :# slist; a \<noteq> \<bottom>; slist \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ys = \<bottom>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ys = \<bottom>

goal (1 subgoal):
 1. prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
ys = \<bottom>
slength\<cdot>xs \<noteq> \<bottom>

goal (1 subgoal):
 1. prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
[PROOF STEP]
using le_slength_plus[of xs 1]
[PROOF STATE]
proof (prove)
using this:
ys = \<bottom>
slength\<cdot>xs \<noteq> \<bottom>
\<lbrakk>xs \<noteq> \<bottom>; 1 \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> le\<cdot>1\<cdot>(slength\<cdot>xs + 1) = TT

goal (1 subgoal):
 1. prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)

goal (2 subgoals):
 1. ys = [::] \<Longrightarrow> prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
 2. \<And>a slist. \<lbrakk>ys = a :# slist; a \<noteq> \<bottom>; slist \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ys = [::] \<Longrightarrow> prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
 2. \<And>a slist. \<lbrakk>ys = a :# slist; a \<noteq> \<bottom>; slist \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
[PROOF STEP]
case snil
[PROOF STATE]
proof (state)
this:
ys = [::]

goal (2 subgoals):
 1. ys = [::] \<Longrightarrow> prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
 2. \<And>a slist. \<lbrakk>ys = a :# slist; a \<noteq> \<bottom>; slist \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ys = [::]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ys = [::]

goal (1 subgoal):
 1. prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
[PROOF STEP]
using False and IH(1,2)
[PROOF STATE]
proof (prove)
using this:
ys = [::]
slength\<cdot>xs \<noteq> \<bottom>
x \<noteq> \<bottom>
xs \<noteq> \<bottom>

goal (1 subgoal):
 1. prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)

goal (1 subgoal):
 1. \<And>a slist. \<lbrakk>ys = a :# slist; a \<noteq> \<bottom>; slist \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a slist. \<lbrakk>ys = a :# slist; a \<noteq> \<bottom>; slist \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
[PROOF STEP]
case (scons z zs)
[PROOF STATE]
proof (state)
this:
ys = z :# zs
z \<noteq> \<bottom>
zs \<noteq> \<bottom>

goal (1 subgoal):
 1. \<And>a slist. \<lbrakk>ys = a :# slist; a \<noteq> \<bottom>; slist \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ys = z :# zs
z \<noteq> \<bottom>
zs \<noteq> \<bottom>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ys = z :# zs
z \<noteq> \<bottom>
zs \<noteq> \<bottom>

goal (1 subgoal):
 1. prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
[PROOF STEP]
using False and IH(1,2) IH(3)[of zs]
[PROOF STATE]
proof (prove)
using this:
ys = z :# zs
z \<noteq> \<bottom>
zs \<noteq> \<bottom>
slength\<cdot>xs \<noteq> \<bottom>
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
prefix\<cdot>xs\<cdot>zs = eq\<cdot>xs\<cdot>(stake\<cdot>(slength\<cdot>xs)\<cdot>zs)

goal (1 subgoal):
 1. prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)
[PROOF STEP]
by (simp add: stake_slength_plus_1 monofun_cfun_arg)
[PROOF STATE]
proof (state)
this:
prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
prefix\<cdot>(x :# xs)\<cdot>ys = eq\<cdot>(x :# xs)\<cdot>(stake\<cdot>(slength\<cdot>(x :# xs))\<cdot>ys)

goal (1 subgoal):
 1. \<And>ys. prefix\<cdot>\<bottom>\<cdot>ys = eq\<cdot>\<bottom>\<cdot>(stake\<cdot>(slength\<cdot>\<bottom>)\<cdot>ys)
[PROOF STEP]
qed simp


[STATEMENT]
lemma prefix_sdrop_slength:
  assumes "prefix\<cdot>xs\<cdot>ys = TT"
  shows "xs :@ sdrop\<cdot>(slength\<cdot>xs)\<cdot>ys = ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs :@ sdrop\<cdot>(slength\<cdot>xs)\<cdot>ys = ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prefix\<cdot>xs\<cdot>ys = TT

goal (1 subgoal):
 1. xs :@ sdrop\<cdot>(slength\<cdot>xs)\<cdot>ys = ys
[PROOF STEP]
by (induct xs arbitrary: ys) (case_tac ys; simp add: sdrop_slength_plus_1)+


[STATEMENT]
lemma prefix_sdrop_prefix_eq:
  assumes "prefix\<cdot>xs\<cdot>ys = TT"
  shows "eq\<cdot>(sdrop\<cdot>(slength\<cdot>xs)\<cdot>ys)\<cdot>[::] = eq\<cdot>ys\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq\<cdot>(sdrop\<cdot>(slength\<cdot>xs)\<cdot>ys)\<cdot>[::] = eq\<cdot>ys\<cdot>xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prefix\<cdot>xs\<cdot>ys = TT

goal (1 subgoal):
 1. eq\<cdot>(sdrop\<cdot>(slength\<cdot>xs)\<cdot>ys)\<cdot>[::] = eq\<cdot>ys\<cdot>xs
[PROOF STEP]
by (induct xs arbitrary: ys) (case_tac ys; simp add: sdrop_slength_plus_1)+


[STATEMENT]
lemma pt_set_nil:
  fixes Xs :: "'a set"
  assumes pt: "pt TYPE('a) TYPE ('x)"
  and     at: "at TYPE('x)"

  shows "([]::'x prm)\<bullet>Xs = Xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<bullet> Xs = Xs
[PROOF STEP]
by(auto simp add: perm_set_def pt1[OF pt])


[STATEMENT]
lemma pt_set_append:
  fixes pi1 :: "'x prm"
  and   pi2 :: "'x prm"
  and   Xs  :: "'a set"
  assumes pt: "pt TYPE('a) TYPE ('x)"
  and     at: "at TYPE('x)"

  shows "(pi1@pi2)\<bullet>Xs = pi1\<bullet>(pi2\<bullet>Xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pi1 @ pi2) \<bullet> Xs = pi1 \<bullet> pi2 \<bullet> Xs
[PROOF STEP]
by(auto simp add: perm_set_def pt2[OF pt])


[STATEMENT]
lemma pt_set_prm_eq:
  fixes pi1 :: "'x prm"
  and   pi2 :: "'x prm"
  and   Xs  :: "'a set"
  assumes pt: "pt TYPE('a) TYPE ('x)"
  and     at: "at TYPE('x)"

  shows "pi1 \<triangleq> pi2  \<Longrightarrow> pi1\<bullet>Xs = pi2\<bullet>Xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  pi1 \<triangleq> pi2  \<Longrightarrow> pi1 \<bullet> Xs = pi2 \<bullet> Xs
[PROOF STEP]
by(auto simp add: perm_set_def pt3[OF pt])


[STATEMENT]
lemma pt_set_inst:
  assumes pt: "pt TYPE('a) TYPE ('x)"
  and     at: "at TYPE('x)"

  shows "pt TYPE('a set) TYPE('x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pt TYPE('a set) TYPE('x)
[PROOF STEP]
apply(simp add: pt_def pt_set_nil[OF pt, OF at] pt_set_append[OF pt, OF at])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>pi1 pi2.  pi1 \<triangleq> pi2  \<longrightarrow> (\<forall>x. pi1 \<bullet> x = pi2 \<bullet> x)
[PROOF STEP]
apply(clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pi1 pi2 x.  pi1 \<triangleq> pi2  \<Longrightarrow> pi1 \<bullet> x = pi2 \<bullet> x
[PROOF STEP]
by(rule pt_set_prm_eq[OF pt, OF at])


[STATEMENT]
lemma pt_ball_eqvt:
  fixes pi :: "'a prm"
  and   Xs :: "'b set"
  and   P :: "'b \<Rightarrow> bool"

  assumes pt: "pt TYPE('b) TYPE('a)"
  and     at: "at TYPE('a)"

  shows "(pi \<bullet> (\<forall>x \<in> Xs. P x)) = (\<forall>x \<in> (pi \<bullet> Xs). pi \<bullet> P (rev pi \<bullet> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pi \<bullet> (\<forall>x\<in>Xs. P x) = (\<forall>x\<in>pi \<bullet> Xs. pi \<bullet> P (rev pi \<bullet> x))
[PROOF STEP]
apply(auto simp add: perm_bool)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x\<in>Xs. P x; x \<in> pi \<bullet> Xs\<rbrakk> \<Longrightarrow> P (rev pi \<bullet> x)
 2. \<And>x. \<lbrakk>\<forall>x\<in>pi \<bullet> Xs. P (rev pi \<bullet> x); x \<in> Xs\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
apply(drule_tac pi="rev pi" in pt_set_bij2[OF pt, OF at])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x\<in>Xs. P x; rev pi \<bullet> x \<in> rev pi \<bullet> pi \<bullet> Xs\<rbrakk> \<Longrightarrow> P (rev pi \<bullet> x)
 2. \<And>x. \<lbrakk>\<forall>x\<in>pi \<bullet> Xs. P (rev pi \<bullet> x); x \<in> Xs\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
apply(simp add: pt_rev_pi[OF pt_set_inst[OF pt, OF at], OF at])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x\<in>pi \<bullet> Xs. P (rev pi \<bullet> x); x \<in> Xs\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
apply(drule_tac pi="pi" in pt_set_bij2[OF pt, OF at])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x\<in>pi \<bullet> Xs. P (rev pi \<bullet> x); pi \<bullet> x \<in> pi \<bullet> Xs\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
apply(erule_tac x="pi \<bullet> x" in ballE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>pi \<bullet> x \<in> pi \<bullet> Xs; P (rev pi \<bullet> pi \<bullet> x)\<rbrakk> \<Longrightarrow> P x
 2. \<And>x. \<lbrakk>pi \<bullet> x \<in> pi \<bullet> Xs; pi \<bullet> x \<notin> pi \<bullet> Xs\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
apply(simp add: pt_rev_pi[OF pt, OF at])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>pi \<bullet> x \<in> pi \<bullet> Xs; pi \<bullet> x \<notin> pi \<bullet> Xs\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
by simp


[STATEMENT]
lemma perm_cart_prod:
  fixes Xs :: "'b set"
  and   Ys :: "'c set"
  and   p  :: "'a prm"

  assumes pt1: "pt TYPE('b) TYPE('a)"
  and     pt2: "pt TYPE('c) TYPE('a)"
  and     at:  "at TYPE('a)"

  shows "(p \<bullet> (Xs \<times> Ys)) = (((p \<bullet> Xs) \<times> (p \<bullet> Ys))::(('b \<times> 'c) set))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> Xs \<times> Ys = (p \<bullet> Xs) \<times> p \<bullet> Ys
[PROOF STEP]
by(auto simp add: perm_set_def)


[STATEMENT]
lemma supp_member:
  fixes Xs :: "'b set"
  and   x  :: 'a

  assumes pt: "pt TYPE('b) TYPE('a)"
  and     at: "at TYPE('a)"
  and     fs: "fs TYPE('b) TYPE('a)"
  and     "finite Xs"
  and     "x \<in> ((supp Xs)::'a set)"

  obtains X where "(X::'b) \<in> Xs" and "x \<in> supp X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>X. \<lbrakk>X \<in> Xs; x \<in> supp X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>X. \<lbrakk>X \<in> Xs; x \<in> supp X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from \<open>finite Xs\<close> \<open>x \<in> supp Xs\<close>
[PROOF STATE]
proof (chain)
picking this:
finite Xs
x \<in> supp Xs
[PROOF STEP]
have "\<exists>X::'b. (X \<in> Xs) \<and> (x \<in> (supp X))"
[PROOF STATE]
proof (prove)
using this:
finite Xs
x \<in> supp Xs

goal (1 subgoal):
 1. \<exists>X. X \<in> Xs \<and> x \<in> supp X
[PROOF STEP]
proof(induct rule: finite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> supp {} \<Longrightarrow> \<exists>X. X \<in> {} \<and> x \<in> supp X
 2. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; x \<in> supp F \<Longrightarrow> \<exists>X. X \<in> F \<and> x \<in> supp X; x \<in> supp (insert xa F)\<rbrakk> \<Longrightarrow> \<exists>X. X \<in> insert xa F \<and> x \<in> supp X
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
x \<in> supp {}

goal (2 subgoals):
 1. x \<in> supp {} \<Longrightarrow> \<exists>X. X \<in> {} \<and> x \<in> supp X
 2. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; x \<in> supp F \<Longrightarrow> \<exists>X. X \<in> F \<and> x \<in> supp X; x \<in> supp (insert xa F)\<rbrakk> \<Longrightarrow> \<exists>X. X \<in> insert xa F \<and> x \<in> supp X
[PROOF STEP]
from \<open>x \<in> ((supp {})::'a set)\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> supp {}
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
x \<in> supp {}

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

goal (2 subgoals):
 1. x \<in> supp {} \<Longrightarrow> \<exists>X. X \<in> {} \<and> x \<in> supp X
 2. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; x \<in> supp F \<Longrightarrow> \<exists>X. X \<in> F \<and> x \<in> supp X; x \<in> supp (insert xa F)\<rbrakk> \<Longrightarrow> \<exists>X. X \<in> insert xa F \<and> x \<in> supp X
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. \<exists>X. X \<in> {} \<and> x \<in> supp X
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>X. X \<in> {} \<and> x \<in> supp X

goal (1 subgoal):
 1. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; x \<in> supp F \<Longrightarrow> \<exists>X. X \<in> F \<and> x \<in> supp X; x \<in> supp (insert xa F)\<rbrakk> \<Longrightarrow> \<exists>X. X \<in> insert xa F \<and> x \<in> supp X
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; x \<in> supp F \<Longrightarrow> \<exists>X. X \<in> F \<and> x \<in> supp X; x \<in> supp (insert xa F)\<rbrakk> \<Longrightarrow> \<exists>X. X \<in> insert xa F \<and> x \<in> supp X
[PROOF STEP]
case(insert y Xs)
[PROOF STATE]
proof (state)
this:
finite Xs
y \<notin> Xs
x \<in> supp Xs \<Longrightarrow> \<exists>X. X \<in> Xs \<and> x \<in> supp X
x \<in> supp (insert y Xs)

goal (1 subgoal):
 1. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; x \<in> supp F \<Longrightarrow> \<exists>X. X \<in> F \<and> x \<in> supp X; x \<in> supp (insert xa F)\<rbrakk> \<Longrightarrow> \<exists>X. X \<in> insert xa F \<and> x \<in> supp X
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>X. X \<in> insert y Xs \<and> x \<in> supp X
[PROOF STEP]
proof(case_tac "x \<in> supp y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> supp y \<Longrightarrow> \<exists>X. X \<in> insert y Xs \<and> x \<in> supp X
 2. x \<notin> supp y \<Longrightarrow> \<exists>X. X \<in> insert y Xs \<and> x \<in> supp X
[PROOF STEP]
assume "x \<in> supp y"
[PROOF STATE]
proof (state)
this:
x \<in> supp y

goal (2 subgoals):
 1. x \<in> supp y \<Longrightarrow> \<exists>X. X \<in> insert y Xs \<and> x \<in> supp X
 2. x \<notin> supp y \<Longrightarrow> \<exists>X. X \<in> insert y Xs \<and> x \<in> supp X
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> supp y

goal (1 subgoal):
 1. \<exists>X. X \<in> insert y Xs \<and> x \<in> supp X
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>X. X \<in> insert y Xs \<and> x \<in> supp X

goal (1 subgoal):
 1. x \<notin> supp y \<Longrightarrow> \<exists>X. X \<in> insert y Xs \<and> x \<in> supp X
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<notin> supp y \<Longrightarrow> \<exists>X. X \<in> insert y Xs \<and> x \<in> supp X
[PROOF STEP]
assume "x \<notin> supp y"
[PROOF STATE]
proof (state)
this:
x \<notin> supp y

goal (1 subgoal):
 1. x \<notin> supp y \<Longrightarrow> \<exists>X. X \<in> insert y Xs \<and> x \<in> supp X
[PROOF STEP]
with \<open>x \<in> supp(insert y Xs)\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> supp (insert y Xs)
x \<notin> supp y
[PROOF STEP]
have "x \<in> supp Xs"
[PROOF STATE]
proof (prove)
using this:
x \<in> supp (insert y Xs)
x \<notin> supp y

goal (1 subgoal):
 1. x \<in> supp Xs
[PROOF STEP]
by(simp add: supp_fin_insert[OF pt, OF at, OF fs, OF \<open>finite Xs\<close>])
[PROOF STATE]
proof (state)
this:
x \<in> supp Xs

goal (1 subgoal):
 1. x \<notin> supp y \<Longrightarrow> \<exists>X. X \<in> insert y Xs \<and> x \<in> supp X
[PROOF STEP]
with \<open>x \<in> supp Xs \<Longrightarrow> \<exists>X. X \<in> Xs \<and> x \<in> supp X\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> supp Xs \<Longrightarrow> \<exists>X. X \<in> Xs \<and> x \<in> supp X
x \<in> supp Xs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> supp Xs \<Longrightarrow> \<exists>X. X \<in> Xs \<and> x \<in> supp X
x \<in> supp Xs

goal (1 subgoal):
 1. \<exists>X. X \<in> insert y Xs \<and> x \<in> supp X
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>X. X \<in> insert y Xs \<and> x \<in> supp X

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>X. X \<in> insert y Xs \<and> x \<in> supp X

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>X. X \<in> Xs \<and> x \<in> supp X

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>X \<in> Xs; x \<in> supp X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?X \<in> Xs; x \<in> supp ?X\<rbrakk> \<Longrightarrow> thesis
\<exists>X. X \<in> Xs \<and> x \<in> supp X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?X \<in> Xs; x \<in> supp ?X\<rbrakk> \<Longrightarrow> thesis
\<exists>X. X \<in> Xs \<and> x \<in> supp X

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma supp_cart_prod_empty[simp]:
  fixes Xs :: "'b set"

  shows "supp (Xs \<times> {}) = ({}::'a set)"
  and   "supp ({} \<times> Xs) = ({}::'a set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp (Xs \<times> {}) = {} &&& supp ({} \<times> Xs) = {}
[PROOF STEP]
by(auto simp add: supp_set_empty)


[STATEMENT]
lemma supp_cart_prod:
  fixes Xs :: "'b set"
  and   Ys :: "'c set"

  assumes pt1: "pt TYPE('b) TYPE('a)"
  and     pt2: "pt TYPE('c) TYPE('a)"
  and     fs1: "fs TYPE('b) TYPE('a)"
  and     fs2: "fs TYPE('c) TYPE('a)"
  and     at:  "at TYPE('a)"
  and     f1:  "finite Xs"
  and     f2:  "finite Ys"
  and     a:   "Xs \<noteq> {}"
  and     b:   "Ys \<noteq> {}"

  shows "((supp (Xs \<times> Ys))::'a set) = ((supp Xs) \<union> (supp Ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp (Xs \<times> Ys) = supp Xs \<union> supp Ys
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. supp (Xs \<times> Ys) = supp Xs \<union> supp Ys
[PROOF STEP]
from f1 f2
[PROOF STATE]
proof (chain)
picking this:
finite Xs
finite Ys
[PROOF STEP]
have f3: "finite(Xs \<times> Ys)"
[PROOF STATE]
proof (prove)
using this:
finite Xs
finite Ys

goal (1 subgoal):
 1. finite (Xs \<times> Ys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (Xs \<times> Ys)

goal (1 subgoal):
 1. supp (Xs \<times> Ys) = supp Xs \<union> supp Ys
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp (Xs \<times> Ys) = supp Xs \<union> supp Ys
[PROOF STEP]
apply(simp add: supp_of_fin_sets[OF pt_prod_inst[OF pt1, OF pt2], OF at, OF fs_prod_inst[OF fs1, OF fs2], OF f3] supp_prod)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (supp ` (Xs \<times> Ys)) = supp Xs \<union> supp Ys
[PROOF STEP]
apply(rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<Union> (supp ` (Xs \<times> Ys)) \<subseteq> supp Xs \<union> supp Ys
 2. supp Xs \<union> supp Ys \<subseteq> \<Union> (supp ` (Xs \<times> Ys))
[PROOF STEP]
using Union_included_in_supp[OF pt1, OF at, OF fs1, OF f1] Union_included_in_supp[OF pt2, OF at, OF fs2, OF f2]
[PROOF STATE]
proof (prove)
using this:
\<Union> (supp ` Xs) \<subseteq> supp Xs
\<Union> (supp ` Ys) \<subseteq> supp Ys

goal (2 subgoals):
 1. \<Union> (supp ` (Xs \<times> Ys)) \<subseteq> supp Xs \<union> supp Ys
 2. supp Xs \<union> supp Ys \<subseteq> \<Union> (supp ` (Xs \<times> Ys))
[PROOF STEP]
apply(force simp add: supp_prod)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp Xs \<union> supp Ys \<subseteq> \<Union> (supp ` (Xs \<times> Ys))
[PROOF STEP]
using a b
[PROOF STATE]
proof (prove)
using this:
Xs \<noteq> {}
Ys \<noteq> {}

goal (1 subgoal):
 1. supp Xs \<union> supp Ys \<subseteq> \<Union> (supp ` (Xs \<times> Ys))
[PROOF STEP]
apply(auto simp add: supp_prod)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa xb. \<lbrakk>x \<in> Xs; xa \<in> Ys; xb \<in> supp Xs\<rbrakk> \<Longrightarrow> \<exists>x\<in>Xs. \<exists>y\<in>Ys. xb \<in> supp x \<or> xb \<in> supp y
 2. \<And>x xa xb. \<lbrakk>x \<in> Xs; xa \<in> Ys; xb \<in> supp Ys\<rbrakk> \<Longrightarrow> \<exists>x\<in>Xs. \<exists>y\<in>Ys. xb \<in> supp x \<or> xb \<in> supp y
[PROOF STEP]
using supp_member[OF pt1, OF at, OF fs1, OF f1]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> supp Xs; \<And>X. \<lbrakk>X \<in> Xs; ?x \<in> supp X\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (2 subgoals):
 1. \<And>x xa xb. \<lbrakk>x \<in> Xs; xa \<in> Ys; xb \<in> supp Xs\<rbrakk> \<Longrightarrow> \<exists>x\<in>Xs. \<exists>y\<in>Ys. xb \<in> supp x \<or> xb \<in> supp y
 2. \<And>x xa xb. \<lbrakk>x \<in> Xs; xa \<in> Ys; xb \<in> supp Ys\<rbrakk> \<Longrightarrow> \<exists>x\<in>Xs. \<exists>y\<in>Ys. xb \<in> supp x \<or> xb \<in> supp y
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>x \<in> Xs; xa \<in> Ys; xb \<in> supp Ys\<rbrakk> \<Longrightarrow> \<exists>x\<in>Xs. \<exists>y\<in>Ys. xb \<in> supp x \<or> xb \<in> supp y
[PROOF STEP]
using supp_member[OF pt2, OF at, OF fs2, OF f2]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> supp Ys; \<And>X. \<lbrakk>X \<in> Ys; ?x \<in> supp X\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>x \<in> Xs; xa \<in> Ys; xb \<in> supp Ys\<rbrakk> \<Longrightarrow> \<exists>x\<in>Xs. \<exists>y\<in>Ys. xb \<in> supp x \<or> xb \<in> supp y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
supp (Xs \<times> Ys) = supp Xs \<union> supp Ys

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fresh_cart_prod:
  fixes x  :: 'a
  and   Xs :: "'b set"
  and   Ys :: "'c set"

  assumes pt1: "pt TYPE('b) TYPE('a)"
  and     pt2: "pt TYPE('c) TYPE('a)"
  and     fs1: "fs TYPE('b) TYPE('a)"
  and     fs2: "fs TYPE('c) TYPE('a)"
  and     at:  "at TYPE('a)"
  and     f1:  "finite Xs"
  and     f2:  "finite Ys"
  and     a:   "Xs \<noteq> {}"
  and     b:   "Ys \<noteq> {}"

  shows "(x \<sharp> (Xs \<times> Ys)) = (x \<sharp> Xs \<and> x \<sharp> Ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sharp> Xs \<times> Ys = (x \<sharp> Xs \<and> x \<sharp> Ys)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
pt TYPE('b) TYPE('a)
pt TYPE('c) TYPE('a)
fs TYPE('b) TYPE('a)
fs TYPE('c) TYPE('a)
at TYPE('a)
finite Xs
finite Ys
Xs \<noteq> {}
Ys \<noteq> {}

goal (1 subgoal):
 1. x \<sharp> Xs \<times> Ys = (x \<sharp> Xs \<and> x \<sharp> Ys)
[PROOF STEP]
by(simp add: supp_cart_prod fresh_def)


[STATEMENT]
lemma fresh_star_cart_prod:
  fixes Zs   :: "'a set"
  and   xvec :: "'a list"
  and   Xs   :: "'b set"
  and   Ys   :: "'c set"

  assumes pt1: "pt TYPE('b) TYPE('a)"
  and     pt2: "pt TYPE('c) TYPE('a)"
  and     fs1: "fs TYPE('b) TYPE('a)"
  and     fs2: "fs TYPE('c) TYPE('a)"
  and     at:  "at TYPE('a)"
  and     f1:  "finite Xs"
  and     f2:  "finite Ys"
  and     a:   "Xs \<noteq> {}"
  and     b:   "Ys \<noteq> {}"

  shows "(Zs \<sharp>* (Xs \<times> Ys)) = (Zs \<sharp>* Xs \<and> Zs \<sharp>* Ys)"
  and   "(xvec \<sharp>* (Xs \<times> Ys)) = (xvec \<sharp>* Xs \<and> xvec \<sharp>* Ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Zs \<sharp>* (Xs \<times> Ys) = (Zs \<sharp>* Xs \<and> Zs \<sharp>* Ys) &&& xvec \<sharp>* (Xs \<times> Ys) = (xvec \<sharp>* Xs \<and> xvec \<sharp>* Ys)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
pt TYPE('b) TYPE('a)
pt TYPE('c) TYPE('a)
fs TYPE('b) TYPE('a)
fs TYPE('c) TYPE('a)
at TYPE('a)
finite Xs
finite Ys
Xs \<noteq> {}
Ys \<noteq> {}

goal (1 subgoal):
 1. Zs \<sharp>* (Xs \<times> Ys) = (Zs \<sharp>* Xs \<and> Zs \<sharp>* Ys) &&& xvec \<sharp>* (Xs \<times> Ys) = (xvec \<sharp>* Xs \<and> xvec \<sharp>* Ys)
[PROOF STEP]
by(force simp add: fresh_cart_prod fresh_star_def)+


[STATEMENT]
lemma permCommute:
  fixes p  :: "'a prm"
  and   q  :: "'a prm"
  and   P  :: 'x
  and   Xs :: "'a set"
  and   Ys :: "'a set"

  assumes pt: "pt TYPE('x) TYPE('a)"
  and     at: "at TYPE('a)"
  and     a: "(set p) \<subseteq> Xs \<times> Ys"
  and     b: "Xs \<sharp>* q"
  and     c: "Ys \<sharp>* q"

  shows "p \<bullet> q \<bullet> P = q \<bullet> p \<bullet> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> q \<bullet> P = q \<bullet> p \<bullet> P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<bullet> q \<bullet> P = q \<bullet> p \<bullet> P
[PROOF STEP]
have "p \<bullet> q \<bullet> P = (p \<bullet> q) \<bullet> p \<bullet> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> q \<bullet> P = (p \<bullet> q) \<bullet> p \<bullet> P
[PROOF STEP]
by(rule pt_perm_compose[OF pt, OF at])
[PROOF STATE]
proof (state)
this:
p \<bullet> q \<bullet> P = (p \<bullet> q) \<bullet> p \<bullet> P

goal (1 subgoal):
 1. p \<bullet> q \<bullet> P = q \<bullet> p \<bullet> P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p \<bullet> q \<bullet> P = (p \<bullet> q) \<bullet> p \<bullet> P

goal (1 subgoal):
 1. p \<bullet> q \<bullet> P = q \<bullet> p \<bullet> P
[PROOF STEP]
from at
[PROOF STATE]
proof (chain)
picking this:
at TYPE('a)
[PROOF STEP]
have "pt TYPE('a) TYPE('a)"
[PROOF STATE]
proof (prove)
using this:
at TYPE('a)

goal (1 subgoal):
 1. pt TYPE('a) TYPE('a)
[PROOF STEP]
by(rule at_pt_inst)
[PROOF STATE]
proof (state)
this:
pt TYPE('a) TYPE('a)

goal (1 subgoal):
 1. p \<bullet> q \<bullet> P = q \<bullet> p \<bullet> P
[PROOF STEP]
hence "pt TYPE(('a \<times> 'a) list) TYPE('a)"
[PROOF STATE]
proof (prove)
using this:
pt TYPE('a) TYPE('a)

goal (1 subgoal):
 1. pt TYPE(('a \<times> 'a) list) TYPE('a)
[PROOF STEP]
by(force intro: pt_prod_inst pt_list_inst)
[PROOF STATE]
proof (state)
this:
pt TYPE(('a \<times> 'a) list) TYPE('a)

goal (1 subgoal):
 1. p \<bullet> q \<bullet> P = q \<bullet> p \<bullet> P
[PROOF STEP]
hence "p \<bullet> q = q"
[PROOF STATE]
proof (prove)
using this:
pt TYPE(('a \<times> 'a) list) TYPE('a)

goal (1 subgoal):
 1. p \<bullet> q = q
[PROOF STEP]
using at a b c
[PROOF STATE]
proof (prove)
using this:
pt TYPE(('a \<times> 'a) list) TYPE('a)
at TYPE('a)
set p \<subseteq> Xs \<times> Ys
Xs \<sharp>* q
Ys \<sharp>* q

goal (1 subgoal):
 1. p \<bullet> q = q
[PROOF STEP]
by(rule pt_freshs_freshs)
[PROOF STATE]
proof (state)
this:
p \<bullet> q = q

goal (1 subgoal):
 1. p \<bullet> q \<bullet> P = q \<bullet> p \<bullet> P
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p \<bullet> q \<bullet> P = (p \<bullet> q) \<bullet> p \<bullet> P
p \<bullet> q = q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p \<bullet> q \<bullet> P = (p \<bullet> q) \<bullet> p \<bullet> P
p \<bullet> q = q

goal (1 subgoal):
 1. p \<bullet> q \<bullet> P = q \<bullet> p \<bullet> P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p \<bullet> q \<bullet> P = q \<bullet> p \<bullet> P

goal:
No subgoals!
[PROOF STEP]
qed