[STATEMENT]
lemma leads_to_wf:
  fixes Is :: "('a seq_pred \<times> ('a \<Rightarrow> 'b)) set"
  assumes "wf (R :: 'b rel)"
  assumes W1: "(\<box>(\<^bold>\<exists>\<phi>. \<lceil>\<langle>\<phi>\<in>fst ` Is\<rangle>\<rceil> \<^bold>\<and> (P \<^bold>\<longrightarrow> \<phi>))) \<sigma>"
  assumes W2: "\<forall>(\<phi>, \<delta>)\<in>Is. \<exists>(\<phi>', \<delta>')\<in>insert (Q, \<delta>0) Is. \<forall>t. (\<phi> \<^bold>\<and> \<lceil>\<delta> \<^bold>= \<langle>t\<rangle>\<rceil> \<^bold>\<leadsto> \<phi>' \<^bold>\<and> \<lceil>\<delta>' \<^bold>\<otimes> \<langle>t\<rangle> \<^bold>\<in> \<langle>R\<rangle>\<rceil>) \<sigma>"
  shows "(P \<^bold>\<leadsto> Q) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<box>(\<lambda>s. P s \<longrightarrow> (\<diamond>Q) s)) \<sigma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<box>(\<lambda>s. P s \<longrightarrow> (\<diamond>Q) s)) \<sigma>
[PROOF STEP]
have "(\<phi> \<^bold>\<and> \<lceil>\<delta> \<^bold>= \<langle>t\<rangle>\<rceil> \<^bold>\<leadsto> Q) \<sigma>" if "(\<phi>, \<delta>) \<in> Is" for \<phi> \<delta> t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<box>(\<lambda>s. \<phi> s \<and> \<lceil>\<lambda>s. \<delta> s = t\<rceil> s \<longrightarrow> (\<diamond>Q) s)) \<sigma>
[PROOF STEP]
using \<open>wf R\<close> that W2
[PROOF STATE]
proof (prove)
using this:
wf R
(\<phi>, \<delta>) \<in> Is
\<forall>(\<phi>, \<delta>)\<in>Is. \<exists>(\<phi>', \<delta>')\<in>insert (Q, \<delta>0) Is. \<forall>t. (\<box>(\<lambda>s. \<phi> s \<and> \<lceil>\<lambda>s. \<delta> s = t\<rceil> s \<longrightarrow> (\<diamond>(\<lambda>s. \<phi>' s \<and> \<lceil>\<lambda>s. (\<delta>' s, t) \<in> R\<rceil> s)) s)) \<sigma>

goal (1 subgoal):
 1. (\<box>(\<lambda>s. \<phi> s \<and> \<lceil>\<lambda>s. \<delta> s = t\<rceil> s \<longrightarrow> (\<diamond>Q) s)) \<sigma>
[PROOF STEP]
apply (induct t arbitrary: \<phi> \<delta>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x \<phi> \<delta>. \<lbrakk>\<And>y \<phi> \<delta>. \<lbrakk>(y, x) \<in> R; (\<phi>, \<delta>) \<in> Is; \<forall>(\<phi>, \<delta>)\<in>Is. \<exists>(\<phi>', \<delta>')\<in>insert (Q, \<delta>0) Is. \<forall>t. (\<box>(\<lambda>s. \<phi> s \<and> \<lceil>\<lambda>s. \<delta> s = t\<rceil> s \<longrightarrow> (\<diamond>(\<lambda>s. \<phi>' s \<and> \<lceil>\<lambda>s. (\<delta>' s, t) \<in> R\<rceil> s)) s)) \<sigma>\<rbrakk> \<Longrightarrow> (\<box>(\<lambda>s. \<phi> s \<and> \<lceil>\<lambda>s. \<delta> s = y\<rceil> s \<longrightarrow> (\<diamond>Q) s)) \<sigma>; (\<phi>, \<delta>) \<in> Is; \<forall>(\<phi>, \<delta>)\<in>Is. \<exists>(\<phi>', \<delta>')\<in>insert (Q, \<delta>0) Is. \<forall>t. (\<box>(\<lambda>s. \<phi> s \<and> \<lceil>\<lambda>s. \<delta> s = t\<rceil> s \<longrightarrow> (\<diamond>(\<lambda>s. \<phi>' s \<and> \<lceil>\<lambda>s. (\<delta>' s, t) \<in> R\<rceil> s)) s)) \<sigma>\<rbrakk> \<Longrightarrow> (\<box>(\<lambda>s. \<phi> s \<and> \<lceil>\<lambda>s. \<delta> s = x\<rceil> s \<longrightarrow> (\<diamond>Q) s)) \<sigma>
[PROOF STEP]
unfolding LTL.defs split_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x \<phi> \<delta>. \<lbrakk>\<And>y \<phi> \<delta>. \<lbrakk>(y, x) \<in> R; (\<phi>, \<delta>) \<in> Is; \<forall>p\<in>Is. \<exists>pa\<in>insert (Q, \<delta>0) Is. \<forall>t i. fst p (\<sigma> |\<^sub>s i) \<and> snd p ((\<sigma> |\<^sub>s i) 0) = t \<longrightarrow> (\<exists>ia. (fst pa (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (snd pa ((\<sigma> |\<^sub>s i |\<^sub>s ia) 0), t) \<in> R) \<and> (\<forall>k<ia. True))\<rbrakk> \<Longrightarrow> \<forall>i. \<phi> (\<sigma> |\<^sub>s i) \<and> \<delta> ((\<sigma> |\<^sub>s i) 0) = y \<longrightarrow> (\<exists>ia. Q (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True)); (\<phi>, \<delta>) \<in> Is; \<forall>p\<in>Is. \<exists>pa\<in>insert (Q, \<delta>0) Is. \<forall>t i. fst p (\<sigma> |\<^sub>s i) \<and> snd p ((\<sigma> |\<^sub>s i) 0) = t \<longrightarrow> (\<exists>ia. (fst pa (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (snd pa ((\<sigma> |\<^sub>s i |\<^sub>s ia) 0), t) \<in> R) \<and> (\<forall>k<ia. True))\<rbrakk> \<Longrightarrow> \<forall>i. \<phi> (\<sigma> |\<^sub>s i) \<and> \<delta> ((\<sigma> |\<^sub>s i) 0) = x \<longrightarrow> (\<exists>ia. Q (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<phi> \<delta> i. \<lbrakk>\<And>y \<phi> \<delta>'. \<lbrakk>(y, \<delta> (\<sigma> i)) \<in> R; (\<phi>, \<delta>') \<in> Is\<rbrakk> \<Longrightarrow> \<forall>i. \<phi> (\<sigma> |\<^sub>s i) \<and> \<delta>' (\<sigma> i) = y \<longrightarrow> (\<exists>ia. Q (\<sigma> |\<^sub>s i + ia)); (\<phi>, \<delta>) \<in> Is; \<forall>p\<in>Is. (\<forall>i. fst p (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>ia. Q (\<sigma> |\<^sub>s i + ia) \<and> (\<delta>0 (\<sigma> (i + ia)), snd p (\<sigma> i)) \<in> R)) \<or> (\<exists>pa\<in>Is. \<forall>i. fst p (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>ia. fst pa (\<sigma> |\<^sub>s i + ia) \<and> (snd pa (\<sigma> (i + ia)), snd p (\<sigma> i)) \<in> R)); \<phi> (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> \<exists>ia. Q (\<sigma> |\<^sub>s i + ia)
[PROOF STEP]
apply (metis (no_types, opaque_lifting) ab_semigroup_add_class.add_ac(1) fst_eqD snd_conv surjective_pairing)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(?\<phi>, ?\<delta>) \<in> Is \<Longrightarrow> (\<box>(\<lambda>s. ?\<phi> s \<and> \<lceil>\<lambda>s. ?\<delta> s = ?t\<rceil> s \<longrightarrow> (\<diamond>Q) s)) \<sigma>

goal (1 subgoal):
 1. (\<box>(\<lambda>s. P s \<longrightarrow> (\<diamond>Q) s)) \<sigma>
[PROOF STEP]
with W1
[PROOF STATE]
proof (chain)
picking this:
(\<box>(\<lambda>s. \<exists>x. \<lceil>\<lambda>s. x \<in> fst ` Is\<rceil> s \<and> (P s \<longrightarrow> x s))) \<sigma>
(?\<phi>, ?\<delta>) \<in> Is \<Longrightarrow> (\<box>(\<lambda>s. ?\<phi> s \<and> \<lceil>\<lambda>s. ?\<delta> s = ?t\<rceil> s \<longrightarrow> (\<diamond>Q) s)) \<sigma>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<box>(\<lambda>s. \<exists>x. \<lceil>\<lambda>s. x \<in> fst ` Is\<rceil> s \<and> (P s \<longrightarrow> x s))) \<sigma>
(?\<phi>, ?\<delta>) \<in> Is \<Longrightarrow> (\<box>(\<lambda>s. ?\<phi> s \<and> \<lceil>\<lambda>s. ?\<delta> s = ?t\<rceil> s \<longrightarrow> (\<diamond>Q) s)) \<sigma>

goal (1 subgoal):
 1. (\<box>(\<lambda>s. P s \<longrightarrow> (\<diamond>Q) s)) \<sigma>
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<box>(\<lambda>s. \<exists>x. \<lceil>\<lambda>s. x \<in> fst ` Is\<rceil> s \<and> (P s \<longrightarrow> x s))) \<sigma>; \<And>\<phi> \<delta> t. (\<phi>, \<delta>) \<in> Is \<Longrightarrow> (\<box>(\<lambda>s. \<phi> s \<and> \<lceil>\<lambda>s. \<delta> s = t\<rceil> s \<longrightarrow> (\<diamond>Q) s)) \<sigma>\<rbrakk> \<Longrightarrow> (\<box>(\<lambda>s. P s \<longrightarrow> (\<diamond>Q) s)) \<sigma>
[PROOF STEP]
apply (rule alwaysI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>(\<box>(\<lambda>s. \<exists>x. \<lceil>\<lambda>s. x \<in> fst ` Is\<rceil> s \<and> (P s \<longrightarrow> x s))) \<sigma>; \<And>\<phi> \<delta> t. (\<phi>, \<delta>) \<in> Is \<Longrightarrow> (\<box>(\<lambda>s. \<phi> s \<and> \<lceil>\<lambda>s. \<delta> s = t\<rceil> s \<longrightarrow> (\<diamond>Q) s)) \<sigma>\<rbrakk> \<Longrightarrow> P (\<sigma> |\<^sub>s i) \<longrightarrow> (\<diamond>Q) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>(\<box>(\<lambda>s. \<exists>x. \<lceil>\<lambda>s. x \<in> fst ` Is\<rceil> s \<and> (P s \<longrightarrow> x s))) \<sigma>; \<And>\<phi> \<delta> t. (\<phi>, \<delta>) \<in> Is \<Longrightarrow> (\<box>(\<lambda>s. \<phi> s \<and> \<lceil>\<lambda>s. \<delta> s = t\<rceil> s \<longrightarrow> (\<diamond>Q) s)) \<sigma>; P (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (\<diamond>Q) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply (erule_tac i=i in alwaysE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<And>\<phi> \<delta> t. (\<phi>, \<delta>) \<in> Is \<Longrightarrow> (\<box>(\<lambda>s. \<phi> s \<and> \<lceil>\<lambda>s. \<delta> s = t\<rceil> s \<longrightarrow> (\<diamond>Q) s)) \<sigma>; P (\<sigma> |\<^sub>s i); \<exists>x. \<lceil>\<lambda>s. x \<in> fst ` Is\<rceil> (\<sigma> |\<^sub>s i) \<and> (P (\<sigma> |\<^sub>s i) \<longrightarrow> x (\<sigma> |\<^sub>s i))\<rbrakk> \<Longrightarrow> (\<diamond>Q) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i a b. \<lbrakk>\<And>\<phi> \<delta> t. (\<phi>, \<delta>) \<in> Is \<Longrightarrow> (\<box>(\<lambda>s. \<phi> s \<and> \<lceil>\<lambda>s. \<delta> s = t\<rceil> s \<longrightarrow> (\<diamond>Q) s)) \<sigma>; P (\<sigma> |\<^sub>s i); (a, b) \<in> Is; a (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (\<diamond>Q) (\<sigma> |\<^sub>s i)
[PROOF STEP]
using alwaysD suffix_state_prop
[PROOF STATE]
proof (prove)
using this:
(\<box>?P) ?\<sigma> \<Longrightarrow> ?P (?\<sigma> |\<^sub>s ?i)
\<lceil>?P\<rceil> (?\<sigma> |\<^sub>s ?i) = ?P (?\<sigma> ?i)

goal (1 subgoal):
 1. \<And>i a b. \<lbrakk>\<And>\<phi> \<delta> t. (\<phi>, \<delta>) \<in> Is \<Longrightarrow> (\<box>(\<lambda>s. \<phi> s \<and> \<lceil>\<lambda>s. \<delta> s = t\<rceil> s \<longrightarrow> (\<diamond>Q) s)) \<sigma>; P (\<sigma> |\<^sub>s i); (a, b) \<in> Is; a (\<sigma> |\<^sub>s i)\<rbrakk> \<Longrightarrow> (\<diamond>Q) (\<sigma> |\<^sub>s i)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<box>(\<lambda>s. P s \<longrightarrow> (\<diamond>Q) s)) \<sigma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakly_fair_def2:
  shows "weakly_fair enabled taken = \<box>(\<^bold>\<not>\<box>(enabled \<^bold>\<and> \<^bold>\<not>taken))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weakly_fair enabled taken = \<box>(\<lambda>s. \<not> (\<box>(\<lambda>s. enabled s \<and> \<not> taken s)) s)
[PROOF STEP]
unfolding weakly_fair_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<box>(\<lambda>s. (\<box>enabled) s \<longrightarrow> (\<diamond>taken) s) = \<box>(\<lambda>s. \<not> (\<box>(\<lambda>s. enabled s \<and> \<not> taken s)) s)
[PROOF STEP]
by (metis (full_types) always_conj_distrib norm(18))


[STATEMENT]
lemma weakly_fair_def3:
  shows "weakly_fair enabled taken = (\<diamond>\<box>enabled \<^bold>\<longrightarrow> \<box>\<diamond>taken)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weakly_fair enabled taken = (\<lambda>s. (\<diamond>\<box>enabled) s \<longrightarrow> (\<box>\<diamond>taken) s)
[PROOF STEP]
unfolding weakly_fair_def2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<box>(\<lambda>s. \<not> (\<box>(\<lambda>s. enabled s \<and> \<not> taken s)) s) = (\<lambda>s. (\<diamond>\<box>enabled) s \<longrightarrow> (\<box>\<diamond>taken) s)
[PROOF STEP]
apply (clarsimp simp: fun_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<box>\<diamond>(\<lambda>s. enabled s \<longrightarrow> taken s)) x = ((\<diamond>\<box>enabled) x \<longrightarrow> (\<box>\<diamond>taken) x)
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<forall>i. \<exists>ia. (enabled (x |\<^sub>s i |\<^sub>s ia) \<longrightarrow> taken (x |\<^sub>s i |\<^sub>s ia)) \<and> (\<forall>k<ia. True)) = ((\<exists>i. (\<forall>ia. enabled (x |\<^sub>s i |\<^sub>s ia)) \<and> (\<forall>k<i. True)) \<longrightarrow> (\<forall>i. \<exists>ia. taken (x |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True)))
[PROOF STEP]
(* True, but can we get there deductively? *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<forall>i. \<exists>ia. (enabled (x |\<^sub>s i |\<^sub>s ia) \<longrightarrow> taken (x |\<^sub>s i |\<^sub>s ia)) \<and> (\<forall>k<ia. True)) = ((\<exists>i. (\<forall>ia. enabled (x |\<^sub>s i |\<^sub>s ia)) \<and> (\<forall>k<i. True)) \<longrightarrow> (\<forall>i. \<exists>ia. taken (x |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True)))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x i ia. \<lbrakk>\<forall>i. \<exists>ia. enabled (x |\<^sub>s i + ia) \<longrightarrow> taken (x |\<^sub>s i + ia); \<forall>ia. enabled (x |\<^sub>s i + ia)\<rbrakk> \<Longrightarrow> \<exists>i. taken (x |\<^sub>s ia + i)
[PROOF STEP]
apply (metis (full_types) add.left_commute semiring_normalization_rules(25))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma weakly_fair_def4:
  shows "weakly_fair enabled taken = \<box>\<diamond>(enabled \<^bold>\<longrightarrow> taken)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weakly_fair enabled taken = \<box>\<diamond>(\<lambda>s. enabled s \<longrightarrow> taken s)
[PROOF STEP]
using weakly_fair_def2
[PROOF STATE]
proof (prove)
using this:
weakly_fair ?enabled ?taken = \<box>(\<lambda>s. \<not> (\<box>(\<lambda>s. ?enabled s \<and> \<not> ?taken s)) s)

goal (1 subgoal):
 1. weakly_fair enabled taken = \<box>\<diamond>(\<lambda>s. enabled s \<longrightarrow> taken s)
[PROOF STEP]
by force


[STATEMENT]
lemma mp_weakly_fair:
  assumes "weakly_fair enabled taken \<sigma>"
  assumes "(\<box>enabled) \<sigma>"
  shows "(\<diamond>taken) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<diamond>taken) \<sigma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
weakly_fair enabled taken \<sigma>
(\<box>enabled) \<sigma>

goal (1 subgoal):
 1. (\<diamond>taken) \<sigma>
[PROOF STEP]
unfolding weakly_fair_def
[PROOF STATE]
proof (prove)
using this:
(\<box>(\<lambda>s. (\<box>enabled) s \<longrightarrow> (\<diamond>taken) s)) \<sigma>
(\<box>enabled) \<sigma>

goal (1 subgoal):
 1. (\<diamond>taken) \<sigma>
[PROOF STEP]
using always_imp_mp
[PROOF STATE]
proof (prove)
using this:
(\<box>(\<lambda>s. (\<box>enabled) s \<longrightarrow> (\<diamond>taken) s)) \<sigma>
(\<box>enabled) \<sigma>
\<lbrakk>(\<box>(\<lambda>s. ?P s \<longrightarrow> ?Q s)) ?\<sigma>; ?P ?\<sigma>\<rbrakk> \<Longrightarrow> ?Q ?\<sigma>

goal (1 subgoal):
 1. (\<diamond>taken) \<sigma>
[PROOF STEP]
by blast


[STATEMENT]
lemma always_weakly_fair:
  shows "\<box>(weakly_fair enabled taken) = weakly_fair enabled taken"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<box>weakly_fair enabled taken = weakly_fair enabled taken
[PROOF STEP]
unfolding weakly_fair_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<box>\<box>(\<lambda>s. (\<box>enabled) s \<longrightarrow> (\<diamond>taken) s) = \<box>(\<lambda>s. (\<box>enabled) s \<longrightarrow> (\<diamond>taken) s)
[PROOF STEP]
by simp


[STATEMENT]
lemma eventually_weakly_fair:
  shows "\<diamond>(weakly_fair enabled taken) = weakly_fair enabled taken"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<diamond>weakly_fair enabled taken = weakly_fair enabled taken
[PROOF STEP]
unfolding weakly_fair_def2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<diamond>\<box>(\<lambda>s. \<not> (\<box>(\<lambda>s. enabled s \<and> \<not> taken s)) s) = \<box>(\<lambda>s. \<not> (\<box>(\<lambda>s. enabled s \<and> \<not> taken s)) s)
[PROOF STEP]
by (simp add: always_eventually_always)


[STATEMENT]
lemma weakly_fair_weaken:
  assumes "(enabled' \<^bold>\<hookrightarrow> enabled) \<sigma>"
  assumes "(taken \<^bold>\<hookrightarrow> taken') \<sigma>"
  shows "(weakly_fair enabled taken \<^bold>\<hookrightarrow>  weakly_fair enabled' taken') \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<box>(\<lambda>s. weakly_fair enabled taken s \<longrightarrow> weakly_fair enabled' taken' s)) \<sigma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<box>(\<lambda>s. enabled' s \<longrightarrow> enabled s)) \<sigma>
(\<box>(\<lambda>s. taken s \<longrightarrow> taken' s)) \<sigma>

goal (1 subgoal):
 1. (\<box>(\<lambda>s. weakly_fair enabled taken s \<longrightarrow> weakly_fair enabled' taken' s)) \<sigma>
[PROOF STEP]
unfolding weakly_fair_def defs
[PROOF STATE]
proof (prove)
using this:
\<forall>i. enabled' (\<sigma> |\<^sub>s i) \<longrightarrow> enabled (\<sigma> |\<^sub>s i)
\<forall>i. taken (\<sigma> |\<^sub>s i) \<longrightarrow> taken' (\<sigma> |\<^sub>s i)

goal (1 subgoal):
 1. \<forall>i. (\<forall>ia. (\<forall>ib. enabled (\<sigma> |\<^sub>s i |\<^sub>s ia |\<^sub>s ib)) \<longrightarrow> (\<exists>ib. taken (\<sigma> |\<^sub>s i |\<^sub>s ia |\<^sub>s ib) \<and> (\<forall>k<ib. True))) \<longrightarrow> (\<forall>ia. (\<forall>ib. enabled' (\<sigma> |\<^sub>s i |\<^sub>s ia |\<^sub>s ib)) \<longrightarrow> (\<exists>ib. taken' (\<sigma> |\<^sub>s i |\<^sub>s ia |\<^sub>s ib) \<and> (\<forall>k<ib. True)))
[PROOF STEP]
by simp blast


[STATEMENT]
lemma weakly_fair_unless_until:
  shows "(weakly_fair enabled taken \<^bold>\<and> (enabled \<^bold>\<hookrightarrow> enabled \<W> taken)) = (enabled \<^bold>\<hookrightarrow> enabled \<U> taken)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. weakly_fair enabled taken s \<and> (\<box>(\<lambda>s. enabled s \<longrightarrow> (enabled \<W> taken) s)) s) = \<box>(\<lambda>s. enabled s \<longrightarrow> (enabled \<U> taken) s)
[PROOF STEP]
unfolding defs weakly_fair_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. (\<forall>i. (\<forall>ia. enabled (s |\<^sub>s i |\<^sub>s ia)) \<longrightarrow> (\<exists>ia. taken (s |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True))) \<and> (\<forall>i. enabled (s |\<^sub>s i) \<longrightarrow> (\<exists>ia. taken (s |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. enabled (s |\<^sub>s i |\<^sub>s k))) \<or> (\<forall>ia. enabled (s |\<^sub>s i |\<^sub>s ia)))) = (\<lambda>\<sigma>. \<forall>i. enabled (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>ia. taken (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. enabled (\<sigma> |\<^sub>s i |\<^sub>s k))))
[PROOF STEP]
apply (auto simp: fun_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x i. \<lbrakk>\<forall>i. enabled (x |\<^sub>s i) \<longrightarrow> (\<exists>ia. taken (x |\<^sub>s i + ia) \<and> (\<forall>k<ia. enabled (x |\<^sub>s i + k))); \<forall>ia. enabled (x |\<^sub>s i + ia)\<rbrakk> \<Longrightarrow> \<exists>ia. taken (x |\<^sub>s i + ia)
[PROOF STEP]
apply (metis add.right_neutral)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma stable_leads_to_eventually:
  assumes "(enabled \<^bold>\<hookrightarrow> \<circle>(enabled \<^bold>\<or> taken)) \<sigma>"
  shows "(enabled \<^bold>\<hookrightarrow> (\<box>enabled \<^bold>\<or> \<diamond>taken)) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<box>(\<lambda>s. enabled s \<longrightarrow> (\<box>enabled) s \<or> (\<diamond>taken) s)) \<sigma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<box>(\<lambda>s. enabled s \<longrightarrow> (\<circle>(\<lambda>s. enabled s \<or> taken s)) s)) \<sigma>

goal (1 subgoal):
 1. (\<box>(\<lambda>s. enabled s \<longrightarrow> (\<box>enabled) s \<or> (\<diamond>taken) s)) \<sigma>
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
using this:
\<forall>i. enabled (\<sigma> |\<^sub>s i) \<longrightarrow> enabled (\<sigma> |\<^sub>s i |\<^sub>s 1) \<or> taken (\<sigma> |\<^sub>s i |\<^sub>s 1)

goal (1 subgoal):
 1. \<forall>i. enabled (\<sigma> |\<^sub>s i) \<longrightarrow> (\<forall>ia. enabled (\<sigma> |\<^sub>s i |\<^sub>s ia)) \<or> (\<exists>ia. taken (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True))
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. enabled (\<sigma> |\<^sub>s i) \<longrightarrow> enabled (\<sigma> |\<^sub>s i |\<^sub>s 1) \<or> taken (\<sigma> |\<^sub>s i |\<^sub>s 1) \<Longrightarrow> \<forall>i. enabled (\<sigma> |\<^sub>s i) \<longrightarrow> (\<forall>ia. enabled (\<sigma> |\<^sub>s i |\<^sub>s ia)) \<or> (\<exists>ia. taken (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True))
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i. enabled (\<sigma> |\<^sub>s i) \<longrightarrow> enabled (\<sigma> |\<^sub>s i |\<^sub>s 1) \<or> taken (\<sigma> |\<^sub>s i |\<^sub>s 1); \<not> (\<forall>i. enabled (\<sigma> |\<^sub>s i) \<longrightarrow> (\<forall>ia. enabled (\<sigma> |\<^sub>s i |\<^sub>s ia)) \<or> (\<exists>ia. taken (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True)))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i ia. \<lbrakk>\<forall>i. enabled (\<sigma> |\<^sub>s i) \<longrightarrow> enabled (\<sigma> |\<^sub>s Suc i) \<or> taken (\<sigma> |\<^sub>s Suc i); enabled (\<sigma> |\<^sub>s i); \<forall>ia. \<not> taken (\<sigma> |\<^sub>s i + ia); \<not> enabled (\<sigma> |\<^sub>s i + ia)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule (1) ex_least_nat_less[where P="\<lambda>j. \<not> enabled (\<sigma> |\<^sub>s i + j)" for i, simplified])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i ia. \<lbrakk>\<forall>i. enabled (\<sigma> |\<^sub>s i) \<longrightarrow> enabled (\<sigma> |\<^sub>s Suc i) \<or> taken (\<sigma> |\<^sub>s Suc i); enabled (\<sigma> |\<^sub>s i); \<forall>ia. \<not> taken (\<sigma> |\<^sub>s i + ia); \<exists>k<ia. (\<forall>ia\<le>k. enabled (\<sigma> |\<^sub>s i + ia)) \<and> \<not> enabled (\<sigma> |\<^sub>s Suc (i + k))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i ia k. \<lbrakk>\<forall>i. enabled (\<sigma> |\<^sub>s i) \<longrightarrow> enabled (\<sigma> |\<^sub>s Suc i) \<or> taken (\<sigma> |\<^sub>s Suc i); enabled (\<sigma> |\<^sub>s i); \<forall>ia. \<not> taken (\<sigma> |\<^sub>s i + ia); k < ia; \<forall>ia\<le>k. enabled (\<sigma> |\<^sub>s i + ia); \<not> enabled (\<sigma> |\<^sub>s Suc (i + k))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis add_Suc_right leI less_irrefl_nat)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma weakly_fair_stable_leads_to:
  assumes "(weakly_fair enabled taken) \<sigma>"
  assumes "(enabled \<^bold>\<hookrightarrow> \<circle>(enabled \<^bold>\<or> taken)) \<sigma>"
  shows "(enabled \<^bold>\<leadsto> taken) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<box>(\<lambda>s. enabled s \<longrightarrow> (\<diamond>taken) s)) \<sigma>
[PROOF STEP]
using stable_leads_to_eventually[OF assms(2)] assms(1)
[PROOF STATE]
proof (prove)
using this:
(\<box>(\<lambda>s. enabled s \<longrightarrow> (\<box>enabled) s \<or> (\<diamond>taken) s)) \<sigma>
weakly_fair enabled taken \<sigma>

goal (1 subgoal):
 1. (\<box>(\<lambda>s. enabled s \<longrightarrow> (\<diamond>taken) s)) \<sigma>
[PROOF STEP]
unfolding defs weakly_fair_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i. enabled (\<sigma> |\<^sub>s i) \<longrightarrow> (\<forall>ia. enabled (\<sigma> |\<^sub>s i |\<^sub>s ia)) \<or> (\<exists>ia. taken (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True))
\<forall>i. (\<forall>ia. enabled (\<sigma> |\<^sub>s i |\<^sub>s ia)) \<longrightarrow> (\<exists>ia. taken (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True))

goal (1 subgoal):
 1. \<forall>i. enabled (\<sigma> |\<^sub>s i) \<longrightarrow> (\<exists>ia. taken (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True))
[PROOF STEP]
by (auto simp: fun_eq_iff)


[STATEMENT]
lemma weakly_fair_stable_leads_to_via:
  assumes "(weakly_fair enabled taken) \<sigma>"
  assumes "(enabled \<^bold>\<hookrightarrow> \<circle>(enabled \<^bold>\<or> taken)) \<sigma>"
  shows "(enabled \<^bold>\<hookrightarrow> enabled \<U> taken) \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<box>(\<lambda>s. enabled s \<longrightarrow> (enabled \<U> taken) s)) \<sigma>
[PROOF STEP]
using stable_unless[OF assms(2)] assms(1)
[PROOF STATE]
proof (prove)
using this:
(\<box>(\<lambda>s. enabled s \<longrightarrow> (enabled \<W> taken) s)) \<sigma>
weakly_fair enabled taken \<sigma>

goal (1 subgoal):
 1. (\<box>(\<lambda>s. enabled s \<longrightarrow> (enabled \<U> taken) s)) \<sigma>
[PROOF STEP]
by (metis (mono_tags) weakly_fair_unless_until)


[STATEMENT]
lemma strongly_fair_def2:
  "strongly_fair enabled taken = \<box>(\<^bold>\<not>\<box>(\<diamond>enabled \<^bold>\<and> \<^bold>\<not>taken))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strongly_fair enabled taken = \<box>(\<lambda>s. \<not> (\<box>(\<lambda>s. (\<diamond>enabled) s \<and> \<not> taken s)) s)
[PROOF STEP]
unfolding strongly_fair_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<box>(\<lambda>s. (\<box>\<diamond>enabled) s \<longrightarrow> (\<diamond>taken) s) = \<box>(\<lambda>s. \<not> (\<box>(\<lambda>s. (\<diamond>enabled) s \<and> \<not> taken s)) s)
[PROOF STEP]
by (metis weakly_fair_def weakly_fair_def2)


[STATEMENT]
lemma strongly_fair_def3:
  "strongly_fair enabled taken = (\<box>\<diamond>enabled \<^bold>\<longrightarrow> \<box>\<diamond>taken)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strongly_fair enabled taken = (\<lambda>s. (\<box>\<diamond>enabled) s \<longrightarrow> (\<box>\<diamond>taken) s)
[PROOF STEP]
unfolding strongly_fair_def2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<box>(\<lambda>s. \<not> (\<box>(\<lambda>s. (\<diamond>enabled) s \<and> \<not> taken s)) s) = (\<lambda>s. (\<box>\<diamond>enabled) s \<longrightarrow> (\<box>\<diamond>taken) s)
[PROOF STEP]
by (metis (full_types) always_eventually_always weakly_fair_def2 weakly_fair_def3)


[STATEMENT]
lemma always_strongly_fair:
  "\<box>(strongly_fair enabled taken) = strongly_fair enabled taken"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<box>strongly_fair enabled taken = strongly_fair enabled taken
[PROOF STEP]
unfolding strongly_fair_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<box>\<box>(\<lambda>s. (\<box>\<diamond>enabled) s \<longrightarrow> (\<diamond>taken) s) = \<box>(\<lambda>s. (\<box>\<diamond>enabled) s \<longrightarrow> (\<diamond>taken) s)
[PROOF STEP]
by simp


[STATEMENT]
lemma eventually_strongly_fair:
  "\<diamond>(strongly_fair enabled taken) = strongly_fair enabled taken"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<diamond>strongly_fair enabled taken = strongly_fair enabled taken
[PROOF STEP]
unfolding strongly_fair_def2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<diamond>\<box>(\<lambda>s. \<not> (\<box>(\<lambda>s. (\<diamond>enabled) s \<and> \<not> taken s)) s) = \<box>(\<lambda>s. \<not> (\<box>(\<lambda>s. (\<diamond>enabled) s \<and> \<not> taken s)) s)
[PROOF STEP]
by (simp add: always_eventually_always)


[STATEMENT]
lemma strongly_fair_disj_distrib: \<comment> \<open>not true for \<open>weakly_fair\<close>\<close>
  "strongly_fair (enabled1 \<^bold>\<or> enabled2) taken = (strongly_fair enabled1 taken \<^bold>\<and> strongly_fair enabled2 taken)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strongly_fair (\<lambda>s. enabled1 s \<or> enabled2 s) taken = (\<lambda>s. strongly_fair enabled1 taken s \<and> strongly_fair enabled2 taken s)
[PROOF STEP]
unfolding strongly_fair_def defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<sigma>. \<forall>i. (\<forall>ia. \<exists>ib. (enabled1 (\<sigma> |\<^sub>s i |\<^sub>s ia |\<^sub>s ib) \<or> enabled2 (\<sigma> |\<^sub>s i |\<^sub>s ia |\<^sub>s ib)) \<and> (\<forall>k<ib. True)) \<longrightarrow> (\<exists>ia. taken (\<sigma> |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True))) = (\<lambda>s. (\<forall>i. (\<forall>ia. \<exists>ib. enabled1 (s |\<^sub>s i |\<^sub>s ia |\<^sub>s ib) \<and> (\<forall>k<ib. True)) \<longrightarrow> (\<exists>ia. taken (s |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True))) \<and> (\<forall>i. (\<forall>ia. \<exists>ib. enabled2 (s |\<^sub>s i |\<^sub>s ia |\<^sub>s ib) \<and> (\<forall>k<ib. True)) \<longrightarrow> (\<exists>ia. taken (s |\<^sub>s i |\<^sub>s ia) \<and> (\<forall>k<ia. True))))
[PROOF STEP]
apply (auto simp: fun_eq_iff)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x i. \<lbrakk>\<forall>i. (\<forall>ia. \<exists>ib. enabled1 (x |\<^sub>s i + ia + ib) \<or> enabled2 (x |\<^sub>s i + ia + ib)) \<longrightarrow> (\<exists>ia. taken (x |\<^sub>s i + ia)); \<forall>ia. \<exists>ib. enabled1 (x |\<^sub>s i + ia + ib)\<rbrakk> \<Longrightarrow> \<exists>ia. taken (x |\<^sub>s i + ia)
 2. \<And>x i. \<lbrakk>\<forall>i. (\<forall>ia. \<exists>ib. enabled1 (x |\<^sub>s i + ia + ib) \<or> enabled2 (x |\<^sub>s i + ia + ib)) \<longrightarrow> (\<exists>ia. taken (x |\<^sub>s i + ia)); \<forall>ia. \<exists>ib. enabled2 (x |\<^sub>s i + ia + ib)\<rbrakk> \<Longrightarrow> \<exists>ia. taken (x |\<^sub>s i + ia)
 3. \<And>x i. \<lbrakk>\<forall>i. (\<forall>ia. \<exists>ib. enabled1 (x |\<^sub>s i + ia + ib)) \<longrightarrow> (\<exists>ia. taken (x |\<^sub>s i + ia)); \<forall>i. (\<forall>ia. \<exists>ib. enabled2 (x |\<^sub>s i + ia + ib)) \<longrightarrow> (\<exists>ia. taken (x |\<^sub>s i + ia)); \<forall>ia. \<exists>ib. enabled1 (x |\<^sub>s i + ia + ib) \<or> enabled2 (x |\<^sub>s i + ia + ib)\<rbrakk> \<Longrightarrow> \<exists>ia. taken (x |\<^sub>s i + ia)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x i. \<lbrakk>\<forall>i. (\<forall>ia. \<exists>ib. enabled1 (x |\<^sub>s i + ia + ib) \<or> enabled2 (x |\<^sub>s i + ia + ib)) \<longrightarrow> (\<exists>ia. taken (x |\<^sub>s i + ia)); \<forall>ia. \<exists>ib. enabled2 (x |\<^sub>s i + ia + ib)\<rbrakk> \<Longrightarrow> \<exists>ia. taken (x |\<^sub>s i + ia)
 2. \<And>x i. \<lbrakk>\<forall>i. (\<forall>ia. \<exists>ib. enabled1 (x |\<^sub>s i + ia + ib)) \<longrightarrow> (\<exists>ia. taken (x |\<^sub>s i + ia)); \<forall>i. (\<forall>ia. \<exists>ib. enabled2 (x |\<^sub>s i + ia + ib)) \<longrightarrow> (\<exists>ia. taken (x |\<^sub>s i + ia)); \<forall>ia. \<exists>ib. enabled1 (x |\<^sub>s i + ia + ib) \<or> enabled2 (x |\<^sub>s i + ia + ib)\<rbrakk> \<Longrightarrow> \<exists>ia. taken (x |\<^sub>s i + ia)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x i. \<lbrakk>\<forall>i. (\<forall>ia. \<exists>ib. enabled1 (x |\<^sub>s i + ia + ib)) \<longrightarrow> (\<exists>ia. taken (x |\<^sub>s i + ia)); \<forall>i. (\<forall>ia. \<exists>ib. enabled2 (x |\<^sub>s i + ia + ib)) \<longrightarrow> (\<exists>ia. taken (x |\<^sub>s i + ia)); \<forall>ia. \<exists>ib. enabled1 (x |\<^sub>s i + ia + ib) \<or> enabled2 (x |\<^sub>s i + ia + ib)\<rbrakk> \<Longrightarrow> \<exists>ia. taken (x |\<^sub>s i + ia)
[PROOF STEP]
apply (metis (full_types) semiring_normalization_rules(25))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma strongly_fair_imp_weakly_fair:
  assumes "strongly_fair enabled taken \<sigma>"
  shows "weakly_fair enabled taken \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weakly_fair enabled taken \<sigma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
strongly_fair enabled taken \<sigma>

goal (1 subgoal):
 1. weakly_fair enabled taken \<sigma>
[PROOF STEP]
unfolding strongly_fair_def3 weakly_fair_def3
[PROOF STATE]
proof (prove)
using this:
(\<box>\<diamond>enabled) \<sigma> \<longrightarrow> (\<box>\<diamond>taken) \<sigma>

goal (1 subgoal):
 1. (\<diamond>\<box>enabled) \<sigma> \<longrightarrow> (\<box>\<diamond>taken) \<sigma>
[PROOF STEP]
by (simp add: eventually_always_imp_always_eventually)


[STATEMENT]
lemma always_enabled_weakly_fair_strongly_fair:
  assumes "(\<box>enabled) \<sigma>"
  shows "weakly_fair enabled taken \<sigma> = strongly_fair enabled taken \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weakly_fair enabled taken \<sigma> = strongly_fair enabled taken \<sigma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<box>enabled) \<sigma>

goal (1 subgoal):
 1. weakly_fair enabled taken \<sigma> = strongly_fair enabled taken \<sigma>
[PROOF STEP]
by (metis strongly_fair_def3 strongly_fair_imp_weakly_fair unfold(2) weakly_fair_def3)


[STATEMENT]
lemma safety_state_prop:
  shows "safety \<lceil>P\<rceil>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. safety \<lceil>P\<rceil>
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. safety (\<lambda>\<sigma>. P (\<sigma> 0))
[PROOF STEP]
by (rule safety_state_prop)


[STATEMENT]
lemma safety_Next:
  assumes "safety P"
  shows "safety (\<circle>P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. safety (\<circle>P)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
safety P

goal (1 subgoal):
 1. safety (\<circle>P)
[PROOF STEP]
unfolding defs safety_def
[PROOF STATE]
proof (prove)
using this:
\<forall>\<sigma>. \<not> P \<sigma> \<longrightarrow> (\<exists>i. \<forall>\<beta>. \<not> P (stake i \<sigma> @- \<beta>))

goal (1 subgoal):
 1. \<forall>\<sigma>. \<not> P (\<sigma> |\<^sub>s 1) \<longrightarrow> (\<exists>i. \<forall>\<beta>. \<not> P (stake i \<sigma> @- \<beta> |\<^sub>s 1))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. \<lbrakk>\<forall>\<sigma>. \<not> P \<sigma> \<longrightarrow> (\<exists>i. \<forall>\<beta>. \<not> P (stake i \<sigma> @- \<beta>)); \<not> P (\<sigma> |\<^sub>s Suc 0)\<rbrakk> \<Longrightarrow> \<exists>i. \<forall>\<beta>. (i = 0 \<longrightarrow> \<not> P (\<beta> |\<^sub>s Suc 0)) \<and> (0 < i \<longrightarrow> \<not> P (tl (stake i \<sigma>) @- \<beta>))
[PROOF STEP]
apply (metis (mono_tags) One_nat_def list.sel(3) nat.simps(3) stake.simps(2))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma safety_unless:
  assumes "safety P"
  assumes "safety Q"
  shows "safety (P \<W> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. safety (P \<W> Q)
[PROOF STEP]
proof(rule safetyI2)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma>. (\<And>i. \<exists>\<beta>. (P \<W> Q) (stake i \<sigma> @- \<beta>)) \<Longrightarrow> (P \<W> Q) \<sigma>
[PROOF STEP]
fix \<sigma>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma>. (\<And>i. \<exists>\<beta>. (P \<W> Q) (stake i \<sigma> @- \<beta>)) \<Longrightarrow> (P \<W> Q) \<sigma>
[PROOF STEP]
assume X: "\<exists>\<beta>. (P \<W> Q) (stake i \<sigma> @- \<beta>)" for i
[PROOF STATE]
proof (state)
this:
\<exists>\<beta>. (P \<W> Q) (stake ?i \<sigma> @- \<beta>)

goal (1 subgoal):
 1. \<And>\<sigma>. (\<And>i. \<exists>\<beta>. (P \<W> Q) (stake i \<sigma> @- \<beta>)) \<Longrightarrow> (P \<W> Q) \<sigma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<beta>. (P \<W> Q) (stake ?i \<sigma> @- \<beta>)
[PROOF STEP]
show "(P \<W> Q) \<sigma>"
[PROOF STATE]
proof (prove)
using this:
\<exists>\<beta>. (P \<W> Q) (stake ?i \<sigma> @- \<beta>)

goal (1 subgoal):
 1. (P \<W> Q) \<sigma>
[PROOF STEP]
proof(cases "\<forall>i j. \<exists>\<beta>. P (\<sigma>(i \<rightarrow> j) @- \<beta>)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>i. \<exists>\<beta>. (P \<W> Q) (stake i \<sigma> @- \<beta>); \<forall>i j. \<exists>\<beta>. P (\<sigma>(i \<rightarrow> j) @- \<beta>)\<rbrakk> \<Longrightarrow> (P \<W> Q) \<sigma>
 2. \<lbrakk>\<And>i. \<exists>\<beta>. (P \<W> Q) (stake i \<sigma> @- \<beta>); \<not> (\<forall>i j. \<exists>\<beta>. P (\<sigma>(i \<rightarrow> j) @- \<beta>))\<rbrakk> \<Longrightarrow> (P \<W> Q) \<sigma>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>i j. \<exists>\<beta>. P (\<sigma>(i \<rightarrow> j) @- \<beta>)

goal (2 subgoals):
 1. \<lbrakk>\<And>i. \<exists>\<beta>. (P \<W> Q) (stake i \<sigma> @- \<beta>); \<forall>i j. \<exists>\<beta>. P (\<sigma>(i \<rightarrow> j) @- \<beta>)\<rbrakk> \<Longrightarrow> (P \<W> Q) \<sigma>
 2. \<lbrakk>\<And>i. \<exists>\<beta>. (P \<W> Q) (stake i \<sigma> @- \<beta>); \<not> (\<forall>i j. \<exists>\<beta>. P (\<sigma>(i \<rightarrow> j) @- \<beta>))\<rbrakk> \<Longrightarrow> (P \<W> Q) \<sigma>
[PROOF STEP]
with \<open>safety P\<close>
[PROOF STATE]
proof (chain)
picking this:
safety P
\<forall>i j. \<exists>\<beta>. P (\<sigma>(i \<rightarrow> j) @- \<beta>)
[PROOF STEP]
have "\<forall>i. P (\<sigma> |\<^sub>s i)"
[PROOF STATE]
proof (prove)
using this:
safety P
\<forall>i j. \<exists>\<beta>. P (\<sigma>(i \<rightarrow> j) @- \<beta>)

goal (1 subgoal):
 1. \<forall>i. P (\<sigma> |\<^sub>s i)
[PROOF STEP]
unfolding safety_def2
[PROOF STATE]
proof (prove)
using this:
\<forall>\<sigma>. (\<forall>i. \<exists>\<beta>. P (stake i \<sigma> @- \<beta>)) \<longrightarrow> P \<sigma>
\<forall>i j. \<exists>\<beta>. P (\<sigma>(i \<rightarrow> j) @- \<beta>)

goal (1 subgoal):
 1. \<forall>i. P (\<sigma> |\<^sub>s i)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>i. P (\<sigma> |\<^sub>s i)

goal (2 subgoals):
 1. \<lbrakk>\<And>i. \<exists>\<beta>. (P \<W> Q) (stake i \<sigma> @- \<beta>); \<forall>i j. \<exists>\<beta>. P (\<sigma>(i \<rightarrow> j) @- \<beta>)\<rbrakk> \<Longrightarrow> (P \<W> Q) \<sigma>
 2. \<lbrakk>\<And>i. \<exists>\<beta>. (P \<W> Q) (stake i \<sigma> @- \<beta>); \<not> (\<forall>i j. \<exists>\<beta>. P (\<sigma>(i \<rightarrow> j) @- \<beta>))\<rbrakk> \<Longrightarrow> (P \<W> Q) \<sigma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. P (\<sigma> |\<^sub>s i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>i. P (\<sigma> |\<^sub>s i)

goal (1 subgoal):
 1. (P \<W> Q) \<sigma>
[PROOF STEP]
by (blast intro: unless_alwaysI)
[PROOF STATE]
proof (state)
this:
(P \<W> Q) \<sigma>

goal (1 subgoal):
 1. \<lbrakk>\<And>i. \<exists>\<beta>. (P \<W> Q) (stake i \<sigma> @- \<beta>); \<not> (\<forall>i j. \<exists>\<beta>. P (\<sigma>(i \<rightarrow> j) @- \<beta>))\<rbrakk> \<Longrightarrow> (P \<W> Q) \<sigma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. \<exists>\<beta>. (P \<W> Q) (stake i \<sigma> @- \<beta>); \<not> (\<forall>i j. \<exists>\<beta>. P (\<sigma>(i \<rightarrow> j) @- \<beta>))\<rbrakk> \<Longrightarrow> (P \<W> Q) \<sigma>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>i j. \<exists>\<beta>. P (\<sigma>(i \<rightarrow> j) @- \<beta>))

goal (1 subgoal):
 1. \<lbrakk>\<And>i. \<exists>\<beta>. (P \<W> Q) (stake i \<sigma> @- \<beta>); \<not> (\<forall>i j. \<exists>\<beta>. P (\<sigma>(i \<rightarrow> j) @- \<beta>))\<rbrakk> \<Longrightarrow> (P \<W> Q) \<sigma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>i j. \<exists>\<beta>. P (\<sigma>(i \<rightarrow> j) @- \<beta>))
[PROOF STEP]
obtain k k' where "\<forall>\<beta>. \<not> P (\<sigma>(k \<rightarrow> k') @- \<beta>)"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>i j. \<exists>\<beta>. P (\<sigma>(i \<rightarrow> j) @- \<beta>))

goal (1 subgoal):
 1. (\<And>k' k. \<forall>\<beta>. \<not> P (\<sigma>(k \<rightarrow> k') @- \<beta>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
\<forall>\<beta>. \<not> P (\<sigma>(k \<rightarrow> k') @- \<beta>)

goal (1 subgoal):
 1. \<lbrakk>\<And>i. \<exists>\<beta>. (P \<W> Q) (stake i \<sigma> @- \<beta>); \<not> (\<forall>i j. \<exists>\<beta>. P (\<sigma>(i \<rightarrow> j) @- \<beta>))\<rbrakk> \<Longrightarrow> (P \<W> Q) \<sigma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<beta>. \<not> P (\<sigma>(k \<rightarrow> k') @- \<beta>)
[PROOF STEP]
have "\<forall>i u. k + k' \<le> i \<longrightarrow> \<not>P ((stake i \<sigma> @- u) |\<^sub>s k)"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<beta>. \<not> P (\<sigma>(k \<rightarrow> k') @- \<beta>)

goal (1 subgoal):
 1. \<forall>i u. k + k' \<le> i \<longrightarrow> \<not> P (stake i \<sigma> @- u |\<^sub>s k)
[PROOF STEP]
by (metis add.commute diff_add stake_shift_stake_shift stake_suffix_drop suffix_shift)
[PROOF STATE]
proof (state)
this:
\<forall>i u. k + k' \<le> i \<longrightarrow> \<not> P (stake i \<sigma> @- u |\<^sub>s k)

goal (1 subgoal):
 1. \<lbrakk>\<And>i. \<exists>\<beta>. (P \<W> Q) (stake i \<sigma> @- \<beta>); \<not> (\<forall>i j. \<exists>\<beta>. P (\<sigma>(i \<rightarrow> j) @- \<beta>))\<rbrakk> \<Longrightarrow> (P \<W> Q) \<sigma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i u. k + k' \<le> i \<longrightarrow> \<not> P (stake i \<sigma> @- u |\<^sub>s k)
[PROOF STEP]
have "\<forall>i u. k + k' \<le> i \<and> (P \<W> Q) (stake i \<sigma> @- u) \<longrightarrow> (\<exists>m\<le>k. Q ((stake i \<sigma> @- u) |\<^sub>s m) \<and> (\<forall>p<m. P ((stake i \<sigma> @- u) |\<^sub>s p)))"
[PROOF STATE]
proof (prove)
using this:
\<forall>i u. k + k' \<le> i \<longrightarrow> \<not> P (stake i \<sigma> @- u |\<^sub>s k)

goal (1 subgoal):
 1. \<forall>i u. k + k' \<le> i \<and> (P \<W> Q) (stake i \<sigma> @- u) \<longrightarrow> (\<exists>m\<le>k. Q (stake i \<sigma> @- u |\<^sub>s m) \<and> (\<forall>p<m. P (stake i \<sigma> @- u |\<^sub>s p)))
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
using this:
\<forall>i u. k + k' \<le> i \<longrightarrow> \<not> P (stake i \<sigma> @- u |\<^sub>s k)

goal (1 subgoal):
 1. \<forall>i u. k + k' \<le> i \<and> ((\<exists>ia. Q (stake i \<sigma> @- u |\<^sub>s ia) \<and> (\<forall>k<ia. P (stake i \<sigma> @- u |\<^sub>s k))) \<or> (\<forall>ia. P (stake i \<sigma> @- u |\<^sub>s ia))) \<longrightarrow> (\<exists>m\<le>k. Q (stake i \<sigma> @- u |\<^sub>s m) \<and> (\<forall>p<m. P (stake i \<sigma> @- u |\<^sub>s p)))
[PROOF STEP]
using leI
[PROOF STATE]
proof (prove)
using this:
\<forall>i u. k + k' \<le> i \<longrightarrow> \<not> P (stake i \<sigma> @- u |\<^sub>s k)
\<not> ?x < ?y \<Longrightarrow> ?y \<le> ?x

goal (1 subgoal):
 1. \<forall>i u. k + k' \<le> i \<and> ((\<exists>ia. Q (stake i \<sigma> @- u |\<^sub>s ia) \<and> (\<forall>k<ia. P (stake i \<sigma> @- u |\<^sub>s k))) \<or> (\<forall>ia. P (stake i \<sigma> @- u |\<^sub>s ia))) \<longrightarrow> (\<exists>m\<le>k. Q (stake i \<sigma> @- u |\<^sub>s m) \<and> (\<forall>p<m. P (stake i \<sigma> @- u |\<^sub>s p)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>i u. k + k' \<le> i \<and> (P \<W> Q) (stake i \<sigma> @- u) \<longrightarrow> (\<exists>m\<le>k. Q (stake i \<sigma> @- u |\<^sub>s m) \<and> (\<forall>p<m. P (stake i \<sigma> @- u |\<^sub>s p)))

goal (1 subgoal):
 1. \<lbrakk>\<And>i. \<exists>\<beta>. (P \<W> Q) (stake i \<sigma> @- \<beta>); \<not> (\<forall>i j. \<exists>\<beta>. P (\<sigma>(i \<rightarrow> j) @- \<beta>))\<rbrakk> \<Longrightarrow> (P \<W> Q) \<sigma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i u. k + k' \<le> i \<and> (P \<W> Q) (stake i \<sigma> @- u) \<longrightarrow> (\<exists>m\<le>k. Q (stake i \<sigma> @- u |\<^sub>s m) \<and> (\<forall>p<m. P (stake i \<sigma> @- u |\<^sub>s p)))
[PROOF STEP]
have "\<forall>i u. k + k' \<le> i \<and> (P \<W> Q) (stake i \<sigma> @- u) \<longrightarrow> (\<exists>m\<le>k. Q (\<sigma>(m \<rightarrow> i - m) @- u) \<and> (\<forall>p<m. P (\<sigma>(p \<rightarrow> i - p) @- u)))"
[PROOF STATE]
proof (prove)
using this:
\<forall>i u. k + k' \<le> i \<and> (P \<W> Q) (stake i \<sigma> @- u) \<longrightarrow> (\<exists>m\<le>k. Q (stake i \<sigma> @- u |\<^sub>s m) \<and> (\<forall>p<m. P (stake i \<sigma> @- u |\<^sub>s p)))

goal (1 subgoal):
 1. \<forall>i u. k + k' \<le> i \<and> (P \<W> Q) (stake i \<sigma> @- u) \<longrightarrow> (\<exists>m\<le>k. Q (\<sigma>(m \<rightarrow> i - m) @- u) \<and> (\<forall>p<m. P (\<sigma>(p \<rightarrow> i - p) @- u)))
[PROOF STEP]
by (metis stake_suffix add_leE nat_less_le order_trans)
[PROOF STATE]
proof (state)
this:
\<forall>i u. k + k' \<le> i \<and> (P \<W> Q) (stake i \<sigma> @- u) \<longrightarrow> (\<exists>m\<le>k. Q (\<sigma>(m \<rightarrow> i - m) @- u) \<and> (\<forall>p<m. P (\<sigma>(p \<rightarrow> i - p) @- u)))

goal (1 subgoal):
 1. \<lbrakk>\<And>i. \<exists>\<beta>. (P \<W> Q) (stake i \<sigma> @- \<beta>); \<not> (\<forall>i j. \<exists>\<beta>. P (\<sigma>(i \<rightarrow> j) @- \<beta>))\<rbrakk> \<Longrightarrow> (P \<W> Q) \<sigma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i u. k + k' \<le> i \<and> (P \<W> Q) (stake i \<sigma> @- u) \<longrightarrow> (\<exists>m\<le>k. Q (\<sigma>(m \<rightarrow> i - m) @- u) \<and> (\<forall>p<m. P (\<sigma>(p \<rightarrow> i - p) @- u)))
[PROOF STEP]
have "\<forall>i. \<exists>n\<ge>i. \<exists>m\<le>k. \<exists>u. Q (\<sigma>(m \<rightarrow> n - m) @- u) \<and> (\<forall>p<m. P (\<sigma>(p \<rightarrow> n - p) @- u))"
[PROOF STATE]
proof (prove)
using this:
\<forall>i u. k + k' \<le> i \<and> (P \<W> Q) (stake i \<sigma> @- u) \<longrightarrow> (\<exists>m\<le>k. Q (\<sigma>(m \<rightarrow> i - m) @- u) \<and> (\<forall>p<m. P (\<sigma>(p \<rightarrow> i - p) @- u)))

goal (1 subgoal):
 1. \<forall>i. \<exists>n\<ge>i. \<exists>m\<le>k. \<exists>u. Q (\<sigma>(m \<rightarrow> n - m) @- u) \<and> (\<forall>p<m. P (\<sigma>(p \<rightarrow> n - p) @- u))
[PROOF STEP]
using X
[PROOF STATE]
proof (prove)
using this:
\<forall>i u. k + k' \<le> i \<and> (P \<W> Q) (stake i \<sigma> @- u) \<longrightarrow> (\<exists>m\<le>k. Q (\<sigma>(m \<rightarrow> i - m) @- u) \<and> (\<forall>p<m. P (\<sigma>(p \<rightarrow> i - p) @- u)))
\<exists>\<beta>. (P \<W> Q) (stake ?i \<sigma> @- \<beta>)

goal (1 subgoal):
 1. \<forall>i. \<exists>n\<ge>i. \<exists>m\<le>k. \<exists>u. Q (\<sigma>(m \<rightarrow> n - m) @- u) \<and> (\<forall>p<m. P (\<sigma>(p \<rightarrow> n - p) @- u))
[PROOF STEP]
by (metis add.commute le_add1)
[PROOF STATE]
proof (state)
this:
\<forall>i. \<exists>n\<ge>i. \<exists>m\<le>k. \<exists>u. Q (\<sigma>(m \<rightarrow> n - m) @- u) \<and> (\<forall>p<m. P (\<sigma>(p \<rightarrow> n - p) @- u))

goal (1 subgoal):
 1. \<lbrakk>\<And>i. \<exists>\<beta>. (P \<W> Q) (stake i \<sigma> @- \<beta>); \<not> (\<forall>i j. \<exists>\<beta>. P (\<sigma>(i \<rightarrow> j) @- \<beta>))\<rbrakk> \<Longrightarrow> (P \<W> Q) \<sigma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. \<exists>n\<ge>i. \<exists>m\<le>k. \<exists>u. Q (\<sigma>(m \<rightarrow> n - m) @- u) \<and> (\<forall>p<m. P (\<sigma>(p \<rightarrow> n - p) @- u))
[PROOF STEP]
have "\<exists>m\<le>k. \<forall>i. \<exists>n\<ge>i. \<exists>u. Q (\<sigma>(m \<rightarrow> n - m) @- u) \<and> (\<forall>p<m. P (\<sigma>(p \<rightarrow> n - p) @- u))"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<exists>n\<ge>i. \<exists>m\<le>k. \<exists>u. Q (\<sigma>(m \<rightarrow> n - m) @- u) \<and> (\<forall>p<m. P (\<sigma>(p \<rightarrow> n - p) @- u))

goal (1 subgoal):
 1. \<exists>m\<le>k. \<forall>i. \<exists>n\<ge>i. \<exists>u. Q (\<sigma>(m \<rightarrow> n - m) @- u) \<and> (\<forall>p<m. P (\<sigma>(p \<rightarrow> n - p) @- u))
[PROOF STEP]
by (simp add: always_eventually_pigeonhole)
[PROOF STATE]
proof (state)
this:
\<exists>m\<le>k. \<forall>i. \<exists>n\<ge>i. \<exists>u. Q (\<sigma>(m \<rightarrow> n - m) @- u) \<and> (\<forall>p<m. P (\<sigma>(p \<rightarrow> n - p) @- u))

goal (1 subgoal):
 1. \<lbrakk>\<And>i. \<exists>\<beta>. (P \<W> Q) (stake i \<sigma> @- \<beta>); \<not> (\<forall>i j. \<exists>\<beta>. P (\<sigma>(i \<rightarrow> j) @- \<beta>))\<rbrakk> \<Longrightarrow> (P \<W> Q) \<sigma>
[PROOF STEP]
with \<open>safety P\<close> \<open>safety Q\<close>
[PROOF STATE]
proof (chain)
picking this:
safety P
safety Q
\<exists>m\<le>k. \<forall>i. \<exists>n\<ge>i. \<exists>u. Q (\<sigma>(m \<rightarrow> n - m) @- u) \<and> (\<forall>p<m. P (\<sigma>(p \<rightarrow> n - p) @- u))
[PROOF STEP]
show "(P \<W> Q) \<sigma>"
[PROOF STATE]
proof (prove)
using this:
safety P
safety Q
\<exists>m\<le>k. \<forall>i. \<exists>n\<ge>i. \<exists>u. Q (\<sigma>(m \<rightarrow> n - m) @- u) \<and> (\<forall>p<m. P (\<sigma>(p \<rightarrow> n - p) @- u))

goal (1 subgoal):
 1. (P \<W> Q) \<sigma>
[PROOF STEP]
unfolding defs
[PROOF STATE]
proof (prove)
using this:
safety P
safety Q
\<exists>m\<le>k. \<forall>i. \<exists>n\<ge>i. \<exists>u. Q (\<sigma>(m \<rightarrow> n - m) @- u) \<and> (\<forall>p<m. P (\<sigma>(p \<rightarrow> n - p) @- u))

goal (1 subgoal):
 1. (\<exists>i. Q (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. P (\<sigma> |\<^sub>s k))) \<or> (\<forall>i. P (\<sigma> |\<^sub>s i))
[PROOF STEP]
by (metis Nat.le_diff_conv2 add_leE safety_always_eventually)
[PROOF STATE]
proof (state)
this:
(P \<W> Q) \<sigma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(P \<W> Q) \<sigma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma safety_always:
  assumes "safety P"
  shows "safety (\<box>P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. safety (\<box>P)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
safety P

goal (1 subgoal):
 1. safety (\<box>P)
[PROOF STEP]
by (metis norm(20) safety_def safety_unless)


[STATEMENT]
lemma absolute_liveness_eventually:
  shows "absolute_liveness P \<longleftrightarrow> (\<exists>\<sigma>. P \<sigma>) \<and> P = \<diamond>P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. absolute_liveness P = ((\<exists>\<sigma>. P \<sigma>) \<and> P = \<diamond>P)
[PROOF STEP]
unfolding absolute_liveness_def defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Ex P \<and> (\<forall>\<sigma> \<alpha>. P \<sigma> \<longrightarrow> P (\<alpha> @- \<sigma>))) = ((\<exists>\<sigma>. P \<sigma>) \<and> P = (\<lambda>\<sigma>. \<exists>i. P (\<sigma> |\<^sub>s i) \<and> (\<forall>k<i. True)))
[PROOF STEP]
by (metis cancel_comm_monoid_add_class.diff_cancel drop_eq_Nil order_refl shift.simps(1) stake_suffix_id suffix_shift suffix_zero)


[STATEMENT]
lemma stable_always:
  shows "stable P \<longleftrightarrow> (\<exists>\<sigma>. P \<sigma>) \<and> P = \<box>P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Infinite_Sequences.stable P = ((\<exists>\<sigma>. P \<sigma>) \<and> P = \<box>P)
[PROOF STEP]
unfolding stable_def defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Ex P \<and> (\<forall>\<sigma> i. P \<sigma> \<longrightarrow> P (\<sigma> |\<^sub>s i))) = ((\<exists>\<sigma>. P \<sigma>) \<and> P = (\<lambda>\<sigma>. \<forall>i. P (\<sigma> |\<^sub>s i)))
[PROOF STEP]
by (metis suffix_zero)


[STATEMENT]
lemma fairness_weakly_fair:
  assumes "\<exists>s. taken s"
  shows "fairness (weakly_fair \<lceil>enabled\<rceil> \<lceil>taken\<rceil>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fairness (weakly_fair \<lceil>enabled\<rceil> \<lceil>taken\<rceil>)
[PROOF STEP]
unfolding fairness_def stable_def absolute_liveness_def weakly_fair_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Ex (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<and> (\<forall>\<sigma> i. (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<sigma> \<longrightarrow> (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<sigma> |\<^sub>s i))) \<and> Ex (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<and> (\<forall>\<sigma> \<alpha>. (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<sigma> \<longrightarrow> (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<alpha> @- \<sigma>))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<exists>s. taken s

goal (1 subgoal):
 1. (Ex (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<and> (\<forall>\<sigma> i. (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<sigma> \<longrightarrow> (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<sigma> |\<^sub>s i))) \<and> Ex (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<and> (\<forall>\<sigma> \<alpha>. (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<sigma> \<longrightarrow> (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<alpha> @- \<sigma>))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s. taken s \<Longrightarrow> Ex (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s))
 2. \<And>s \<sigma> i. \<lbrakk>taken s; (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<sigma>\<rbrakk> \<Longrightarrow> (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<sigma> |\<^sub>s i)
 3. \<And>s. taken s \<Longrightarrow> Ex (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s))
 4. \<And>s \<sigma> \<alpha>. \<lbrakk>taken s; (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<sigma>\<rbrakk> \<Longrightarrow> (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<alpha> @- \<sigma>)
[PROOF STEP]
apply (rule_tac x="\<lambda>_ .s" in exI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s. taken s \<Longrightarrow> (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<lambda>_. s)
 2. \<And>s \<sigma> i. \<lbrakk>taken s; (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<sigma>\<rbrakk> \<Longrightarrow> (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<sigma> |\<^sub>s i)
 3. \<And>s. taken s \<Longrightarrow> Ex (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s))
 4. \<And>s \<sigma> \<alpha>. \<lbrakk>taken s; (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<sigma>\<rbrakk> \<Longrightarrow> (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<alpha> @- \<sigma>)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s \<sigma> i. \<lbrakk>taken s; (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<sigma>\<rbrakk> \<Longrightarrow> (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<sigma> |\<^sub>s i)
 2. \<And>s. taken s \<Longrightarrow> Ex (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s))
 3. \<And>s \<sigma> \<alpha>. \<lbrakk>taken s; (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<sigma>\<rbrakk> \<Longrightarrow> (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<alpha> @- \<sigma>)
[PROOF STEP]
apply (simp add: alwaysD)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. taken s \<Longrightarrow> Ex (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s))
 2. \<And>s \<sigma> \<alpha>. \<lbrakk>taken s; (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<sigma>\<rbrakk> \<Longrightarrow> (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<alpha> @- \<sigma>)
[PROOF STEP]
apply (rule_tac x="\<lambda>_ .s" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. taken s \<Longrightarrow> (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<lambda>_. s)
 2. \<And>s \<sigma> \<alpha>. \<lbrakk>taken s; (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<sigma>\<rbrakk> \<Longrightarrow> (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<alpha> @- \<sigma>)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s \<sigma> \<alpha>. \<lbrakk>taken s; (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<sigma>\<rbrakk> \<Longrightarrow> (\<box>(\<lambda>s. (\<box>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<alpha> @- \<sigma>)
[PROOF STEP]
apply (metis (full_types) absolute_liveness_def absolute_liveness_eventually eventually_weakly_fair weakly_fair_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fairness_strongly_fair:
  assumes "\<exists>s. taken s"
  shows "fairness (strongly_fair \<lceil>enabled\<rceil> \<lceil>taken\<rceil>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fairness (strongly_fair \<lceil>enabled\<rceil> \<lceil>taken\<rceil>)
[PROOF STEP]
unfolding fairness_def stable_def absolute_liveness_def strongly_fair_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Ex (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<and> (\<forall>\<sigma> i. (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<sigma> \<longrightarrow> (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<sigma> |\<^sub>s i))) \<and> Ex (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<and> (\<forall>\<sigma> \<alpha>. (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<sigma> \<longrightarrow> (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<alpha> @- \<sigma>))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<exists>s. taken s

goal (1 subgoal):
 1. (Ex (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<and> (\<forall>\<sigma> i. (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<sigma> \<longrightarrow> (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<sigma> |\<^sub>s i))) \<and> Ex (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<and> (\<forall>\<sigma> \<alpha>. (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<sigma> \<longrightarrow> (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<alpha> @- \<sigma>))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s. taken s \<Longrightarrow> Ex (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s))
 2. \<And>s \<sigma> i. \<lbrakk>taken s; (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<sigma>\<rbrakk> \<Longrightarrow> (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<sigma> |\<^sub>s i)
 3. \<And>s. taken s \<Longrightarrow> Ex (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s))
 4. \<And>s \<sigma> \<alpha>. \<lbrakk>taken s; (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<sigma>\<rbrakk> \<Longrightarrow> (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<alpha> @- \<sigma>)
[PROOF STEP]
apply (rule_tac x="\<lambda>_ .s" in exI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s. taken s \<Longrightarrow> (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<lambda>_. s)
 2. \<And>s \<sigma> i. \<lbrakk>taken s; (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<sigma>\<rbrakk> \<Longrightarrow> (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<sigma> |\<^sub>s i)
 3. \<And>s. taken s \<Longrightarrow> Ex (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s))
 4. \<And>s \<sigma> \<alpha>. \<lbrakk>taken s; (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<sigma>\<rbrakk> \<Longrightarrow> (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<alpha> @- \<sigma>)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s \<sigma> i. \<lbrakk>taken s; (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<sigma>\<rbrakk> \<Longrightarrow> (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<sigma> |\<^sub>s i)
 2. \<And>s. taken s \<Longrightarrow> Ex (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s))
 3. \<And>s \<sigma> \<alpha>. \<lbrakk>taken s; (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<sigma>\<rbrakk> \<Longrightarrow> (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<alpha> @- \<sigma>)
[PROOF STEP]
apply (simp add: alwaysD)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. taken s \<Longrightarrow> Ex (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s))
 2. \<And>s \<sigma> \<alpha>. \<lbrakk>taken s; (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<sigma>\<rbrakk> \<Longrightarrow> (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<alpha> @- \<sigma>)
[PROOF STEP]
apply (rule_tac x="\<lambda>_ .s" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. taken s \<Longrightarrow> (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<lambda>_. s)
 2. \<And>s \<sigma> \<alpha>. \<lbrakk>taken s; (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<sigma>\<rbrakk> \<Longrightarrow> (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<alpha> @- \<sigma>)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s \<sigma> \<alpha>. \<lbrakk>taken s; (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) \<sigma>\<rbrakk> \<Longrightarrow> (\<box>(\<lambda>s. (\<box>\<diamond>\<lceil>enabled\<rceil>) s \<longrightarrow> (\<diamond>\<lceil>taken\<rceil>) s)) (\<alpha> @- \<sigma>)
[PROOF STEP]
apply (metis (full_types) absolute_liveness_def absolute_liveness_eventually eventually_weakly_fair weakly_fair_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "i \<le> length ys \<Longrightarrow> sublist_at xs ys i \<longleftrightarrow> sublist_at' xs ys i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> length ys \<Longrightarrow> sublist_at xs ys i = sublist_at' xs ys i
[PROOF STEP]
unfolding sublist_at'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> length ys \<Longrightarrow> sublist_at xs ys i = (take (length xs) (drop i ys) = xs)
[PROOF STEP]
by (induction xs ys i rule: sublist_at.induct) auto


[STATEMENT]
lemma sublist_lengths: "sublist_at xs ys i \<Longrightarrow> i + length xs \<le> length ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sublist_at xs ys i \<Longrightarrow> i + length xs \<le> length ys
[PROOF STEP]
by (induction xs ys i rule: sublist_at.induct) auto


[STATEMENT]
lemma sublist_step[intro]:
  "\<lbrakk>i + length xs < length ys; sublist_at xs ys i; ys!(i + length xs) = x\<rbrakk> \<Longrightarrow> sublist_at (xs@[x]) ys i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i + length xs < length ys; sublist_at xs ys i; ys ! (i + length xs) = x\<rbrakk> \<Longrightarrow> sublist_at (xs @ [x]) ys i
[PROOF STEP]
apply (induction xs ys i rule: sublist_at.induct)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>xa xs y ys. \<lbrakk>\<lbrakk>0 + length xs < length ys; sublist_at xs ys 0; ys ! (0 + length xs) = x\<rbrakk> \<Longrightarrow> sublist_at (xs @ [x]) ys 0; 0 + length (xa # xs) < length (y # ys); sublist_at (xa # xs) (y # ys) 0; (y # ys) ! (0 + length (xa # xs)) = x\<rbrakk> \<Longrightarrow> sublist_at ((xa # xs) @ [x]) (y # ys) 0
 2. \<And>xs y ys i. \<lbrakk>\<lbrakk>i + length xs < length ys; sublist_at xs ys i; ys ! (i + length xs) = x\<rbrakk> \<Longrightarrow> sublist_at (xs @ [x]) ys i; Suc i + length xs < length (y # ys); sublist_at xs (y # ys) (Suc i); (y # ys) ! (Suc i + length xs) = x\<rbrakk> \<Longrightarrow> sublist_at (xs @ [x]) (y # ys) (Suc i)
 3. \<And>ys. \<lbrakk>0 + length [] < length ys; sublist_at [] ys 0; ys ! (0 + length []) = x\<rbrakk> \<Longrightarrow> sublist_at ([] @ [x]) ys 0
 4. \<And>v va uv_. \<lbrakk>uv_ + length (v # va) < length []; sublist_at (v # va) [] uv_; [] ! (uv_ + length (v # va)) = x\<rbrakk> \<Longrightarrow> sublist_at ((v # va) @ [x]) [] uv_
 5. \<And>uu_ v. \<lbrakk>Suc v + length uu_ < length []; sublist_at uu_ [] (Suc v); [] ! (Suc v + length uu_) = x\<rbrakk> \<Longrightarrow> sublist_at (uu_ @ [x]) [] (Suc v)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ys. \<lbrakk>ys \<noteq> []; x = ys ! 0\<rbrakk> \<Longrightarrow> sublist_at [ys ! 0] ys 0
[PROOF STEP]
using sublist_at.elims(3)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> sublist_at ?x ?xa ?xb; \<And>x xs y ys. \<lbrakk>?x = x # xs; ?xa = y # ys; ?xb = 0; \<not> (x = y \<and> sublist_at xs ys 0)\<rbrakk> \<Longrightarrow> ?P; \<And>xs y ys i. \<lbrakk>?x = xs; ?xa = y # ys; ?xb = Suc i; \<not> sublist_at xs ys i\<rbrakk> \<Longrightarrow> ?P; \<And>v va uv_. \<lbrakk>?x = v # va; ?xa = []; ?xb = uv_\<rbrakk> \<Longrightarrow> ?P; \<And>uu_ v. \<lbrakk>?x = uu_; ?xa = []; ?xb = Suc v\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. \<And>ys. \<lbrakk>ys \<noteq> []; x = ys ! 0\<rbrakk> \<Longrightarrow> sublist_at [ys ! 0] ys 0
[PROOF STEP]
by fastforce


[STATEMENT]
lemma all_positions_sublist:
"\<lbrakk>i + length xs \<le> length ys; \<forall>jj<length xs. ys!(i+jj) = xs!jj\<rbrakk> \<Longrightarrow> sublist_at xs ys i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i + length xs \<le> length ys; \<forall>jj<length xs. ys ! (i + jj) = xs ! jj\<rbrakk> \<Longrightarrow> sublist_at xs ys i
[PROOF STEP]
proof (induction xs rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>i + length [] \<le> length ys; \<forall>jj<length []. ys ! (i + jj) = [] ! jj\<rbrakk> \<Longrightarrow> sublist_at [] ys i
 2. \<And>x xs. \<lbrakk>\<lbrakk>i + length xs \<le> length ys; \<forall>jj<length xs. ys ! (i + jj) = xs ! jj\<rbrakk> \<Longrightarrow> sublist_at xs ys i; i + length (xs @ [x]) \<le> length ys; \<forall>jj<length (xs @ [x]). ys ! (i + jj) = (xs @ [x]) ! jj\<rbrakk> \<Longrightarrow> sublist_at (xs @ [x]) ys i
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
i + length [] \<le> length ys
\<forall>jj<length []. ys ! (i + jj) = [] ! jj

goal (2 subgoals):
 1. \<lbrakk>i + length [] \<le> length ys; \<forall>jj<length []. ys ! (i + jj) = [] ! jj\<rbrakk> \<Longrightarrow> sublist_at [] ys i
 2. \<And>x xs. \<lbrakk>\<lbrakk>i + length xs \<le> length ys; \<forall>jj<length xs. ys ! (i + jj) = xs ! jj\<rbrakk> \<Longrightarrow> sublist_at xs ys i; i + length (xs @ [x]) \<le> length ys; \<forall>jj<length (xs @ [x]). ys ! (i + jj) = (xs @ [x]) ! jj\<rbrakk> \<Longrightarrow> sublist_at (xs @ [x]) ys i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i + length [] \<le> length ys
\<forall>jj<length []. ys ! (i + jj) = [] ! jj
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i + length [] \<le> length ys
\<forall>jj<length []. ys ! (i + jj) = [] ! jj

goal (1 subgoal):
 1. sublist_at [] ys i
[PROOF STEP]
by (simp add: Nil_is_sublist)
[PROOF STATE]
proof (state)
this:
sublist_at [] ys i

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>i + length xs \<le> length ys; \<forall>jj<length xs. ys ! (i + jj) = xs ! jj\<rbrakk> \<Longrightarrow> sublist_at xs ys i; i + length (xs @ [x]) \<le> length ys; \<forall>jj<length (xs @ [x]). ys ! (i + jj) = (xs @ [x]) ! jj\<rbrakk> \<Longrightarrow> sublist_at (xs @ [x]) ys i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>i + length xs \<le> length ys; \<forall>jj<length xs. ys ! (i + jj) = xs ! jj\<rbrakk> \<Longrightarrow> sublist_at xs ys i; i + length (xs @ [x]) \<le> length ys; \<forall>jj<length (xs @ [x]). ys ! (i + jj) = (xs @ [x]) ! jj\<rbrakk> \<Longrightarrow> sublist_at (xs @ [x]) ys i
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i + length xs \<le> length ys; \<forall>jj<length xs. ys ! (i + jj) = xs ! jj\<rbrakk> \<Longrightarrow> sublist_at xs ys i
i + length (xs @ [x]) \<le> length ys
\<forall>jj<length (xs @ [x]). ys ! (i + jj) = (xs @ [x]) ! jj

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>i + length xs \<le> length ys; \<forall>jj<length xs. ys ! (i + jj) = xs ! jj\<rbrakk> \<Longrightarrow> sublist_at xs ys i; i + length (xs @ [x]) \<le> length ys; \<forall>jj<length (xs @ [x]). ys ! (i + jj) = (xs @ [x]) ! jj\<rbrakk> \<Longrightarrow> sublist_at (xs @ [x]) ys i
[PROOF STEP]
from \<open>i + length (xs @ [x]) \<le> length ys\<close>
[PROOF STATE]
proof (chain)
picking this:
i + length (xs @ [x]) \<le> length ys
[PROOF STEP]
have "i + length xs \<le> length ys"
[PROOF STATE]
proof (prove)
using this:
i + length (xs @ [x]) \<le> length ys

goal (1 subgoal):
 1. i + length xs \<le> length ys
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i + length xs \<le> length ys

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>i + length xs \<le> length ys; \<forall>jj<length xs. ys ! (i + jj) = xs ! jj\<rbrakk> \<Longrightarrow> sublist_at xs ys i; i + length (xs @ [x]) \<le> length ys; \<forall>jj<length (xs @ [x]). ys ! (i + jj) = (xs @ [x]) ! jj\<rbrakk> \<Longrightarrow> sublist_at (xs @ [x]) ys i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i + length xs \<le> length ys

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>i + length xs \<le> length ys; \<forall>jj<length xs. ys ! (i + jj) = xs ! jj\<rbrakk> \<Longrightarrow> sublist_at xs ys i; i + length (xs @ [x]) \<le> length ys; \<forall>jj<length (xs @ [x]). ys ! (i + jj) = (xs @ [x]) ! jj\<rbrakk> \<Longrightarrow> sublist_at (xs @ [x]) ys i
[PROOF STEP]
have "\<forall>jj<length xs. ys!(i + jj) = xs!jj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>jj<length xs. ys ! (i + jj) = xs ! jj
[PROOF STEP]
by (simp add: nth_append snoc.prems(2))
[PROOF STATE]
proof (state)
this:
\<forall>jj<length xs. ys ! (i + jj) = xs ! jj

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>i + length xs \<le> length ys; \<forall>jj<length xs. ys ! (i + jj) = xs ! jj\<rbrakk> \<Longrightarrow> sublist_at xs ys i; i + length (xs @ [x]) \<le> length ys; \<forall>jj<length (xs @ [x]). ys ! (i + jj) = (xs @ [x]) ! jj\<rbrakk> \<Longrightarrow> sublist_at (xs @ [x]) ys i
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i + length xs \<le> length ys
\<forall>jj<length xs. ys ! (i + jj) = xs ! jj
[PROOF STEP]
have "sublist_at xs ys i"
[PROOF STATE]
proof (prove)
using this:
i + length xs \<le> length ys
\<forall>jj<length xs. ys ! (i + jj) = xs ! jj

goal (1 subgoal):
 1. sublist_at xs ys i
[PROOF STEP]
using snoc.IH
[PROOF STATE]
proof (prove)
using this:
i + length xs \<le> length ys
\<forall>jj<length xs. ys ! (i + jj) = xs ! jj
\<lbrakk>i + length xs \<le> length ys; \<forall>jj<length xs. ys ! (i + jj) = xs ! jj\<rbrakk> \<Longrightarrow> sublist_at xs ys i

goal (1 subgoal):
 1. sublist_at xs ys i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sublist_at xs ys i

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>\<lbrakk>i + length xs \<le> length ys; \<forall>jj<length xs. ys ! (i + jj) = xs ! jj\<rbrakk> \<Longrightarrow> sublist_at xs ys i; i + length (xs @ [x]) \<le> length ys; \<forall>jj<length (xs @ [x]). ys ! (i + jj) = (xs @ [x]) ! jj\<rbrakk> \<Longrightarrow> sublist_at (xs @ [x]) ys i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sublist_at xs ys i
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
sublist_at xs ys i

goal (1 subgoal):
 1. sublist_at (xs @ [x]) ys i
[PROOF STEP]
using snoc.prems
[PROOF STATE]
proof (prove)
using this:
sublist_at xs ys i
i + length (xs @ [x]) \<le> length ys
\<forall>jj<length (xs @ [x]). ys ! (i + jj) = (xs @ [x]) ! jj

goal (1 subgoal):
 1. sublist_at (xs @ [x]) ys i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sublist_at (xs @ [x]) ys i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sublist_all_positions: "sublist_at xs ys i \<Longrightarrow> \<forall>jj<length xs. ys!(i+jj) = xs!jj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sublist_at xs ys i \<Longrightarrow> \<forall>jj<length xs. ys ! (i + jj) = xs ! jj
[PROOF STEP]
by (induction xs ys i rule: sublist_at.induct) (auto simp: nth_Cons')


[STATEMENT]
lemma sublist_at_altdef:
  "sublist_at xs ys i \<longleftrightarrow> (\<exists>ps ss. ys = ps@xs@ss \<and> i = length ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sublist_at xs ys i = (\<exists>ps ss. ys = ps @ xs @ ss \<and> i = length ps)
[PROOF STEP]
proof (induction xs ys i rule: sublist_at.induct)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x xs y ys. sublist_at xs ys 0 = (\<exists>ps ss. ys = ps @ xs @ ss \<and> 0 = length ps) \<Longrightarrow> sublist_at (x # xs) (y # ys) 0 = (\<exists>ps ss. y # ys = ps @ (x # xs) @ ss \<and> 0 = length ps)
 2. \<And>xs y ys i. sublist_at xs ys i = (\<exists>ps ss. ys = ps @ xs @ ss \<and> i = length ps) \<Longrightarrow> sublist_at xs (y # ys) (Suc i) = (\<exists>ps ss. y # ys = ps @ xs @ ss \<and> Suc i = length ps)
 3. \<And>ys. sublist_at [] ys 0 = (\<exists>ps ss. ys = ps @ [] @ ss \<and> 0 = length ps)
 4. \<And>v va uv_. sublist_at (v # va) [] uv_ = (\<exists>ps ss. [] = ps @ (v # va) @ ss \<and> uv_ = length ps)
 5. \<And>uu_ v. sublist_at uu_ [] (Suc v) = (\<exists>ps ss. [] = ps @ uu_ @ ss \<and> Suc v = length ps)
[PROOF STEP]
case (2 ss t ts i)
[PROOF STATE]
proof (state)
this:
sublist_at ss ts i = (\<exists>ps ssa. ts = ps @ ss @ ssa \<and> i = length ps)

goal (5 subgoals):
 1. \<And>x xs y ys. sublist_at xs ys 0 = (\<exists>ps ss. ys = ps @ xs @ ss \<and> 0 = length ps) \<Longrightarrow> sublist_at (x # xs) (y # ys) 0 = (\<exists>ps ss. y # ys = ps @ (x # xs) @ ss \<and> 0 = length ps)
 2. \<And>xs y ys i. sublist_at xs ys i = (\<exists>ps ss. ys = ps @ xs @ ss \<and> i = length ps) \<Longrightarrow> sublist_at xs (y # ys) (Suc i) = (\<exists>ps ss. y # ys = ps @ xs @ ss \<and> Suc i = length ps)
 3. \<And>ys. sublist_at [] ys 0 = (\<exists>ps ss. ys = ps @ [] @ ss \<and> 0 = length ps)
 4. \<And>v va uv_. sublist_at (v # va) [] uv_ = (\<exists>ps ss. [] = ps @ (v # va) @ ss \<and> uv_ = length ps)
 5. \<And>uu_ v. sublist_at uu_ [] (Suc v) = (\<exists>ps ss. [] = ps @ uu_ @ ss \<and> Suc v = length ps)
[PROOF STEP]
show "sublist_at ss (t#ts) (Suc i) \<longleftrightarrow> (\<exists>xs ys. t#ts = xs@ss@ys \<and> Suc i = length xs)"
    (is "?lhs \<longleftrightarrow> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sublist_at ss (t # ts) (Suc i) = (\<exists>xs ys. t # ts = xs @ ss @ ys \<and> Suc i = length xs)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sublist_at ss (t # ts) (Suc i) \<Longrightarrow> \<exists>xs ys. t # ts = xs @ ss @ ys \<and> Suc i = length xs
 2. \<exists>xs ys. t # ts = xs @ ss @ ys \<and> Suc i = length xs \<Longrightarrow> sublist_at ss (t # ts) (Suc i)
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
sublist_at ss (t # ts) (Suc i)

goal (2 subgoals):
 1. sublist_at ss (t # ts) (Suc i) \<Longrightarrow> \<exists>xs ys. t # ts = xs @ ss @ ys \<and> Suc i = length xs
 2. \<exists>xs ys. t # ts = xs @ ss @ ys \<and> Suc i = length xs \<Longrightarrow> sublist_at ss (t # ts) (Suc i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sublist_at ss (t # ts) (Suc i)
[PROOF STEP]
have "sublist_at ss ts i"
[PROOF STATE]
proof (prove)
using this:
sublist_at ss (t # ts) (Suc i)

goal (1 subgoal):
 1. sublist_at ss ts i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sublist_at ss ts i

goal (2 subgoals):
 1. sublist_at ss (t # ts) (Suc i) \<Longrightarrow> \<exists>xs ys. t # ts = xs @ ss @ ys \<and> Suc i = length xs
 2. \<exists>xs ys. t # ts = xs @ ss @ ys \<and> Suc i = length xs \<Longrightarrow> sublist_at ss (t # ts) (Suc i)
[PROOF STEP]
with "2.IH"
[PROOF STATE]
proof (chain)
picking this:
sublist_at ss ts i = (\<exists>ps ssa. ts = ps @ ss @ ssa \<and> i = length ps)
sublist_at ss ts i
[PROOF STEP]
obtain xs where "\<exists>ys. ts = xs@ss@ys \<and> i = length xs"
[PROOF STATE]
proof (prove)
using this:
sublist_at ss ts i = (\<exists>ps ssa. ts = ps @ ss @ ssa \<and> i = length ps)
sublist_at ss ts i

goal (1 subgoal):
 1. (\<And>xs. \<exists>ys. ts = xs @ ss @ ys \<and> i = length xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>ys. ts = xs @ ss @ ys \<and> i = length xs

goal (2 subgoals):
 1. sublist_at ss (t # ts) (Suc i) \<Longrightarrow> \<exists>xs ys. t # ts = xs @ ss @ ys \<and> Suc i = length xs
 2. \<exists>xs ys. t # ts = xs @ ss @ ys \<and> Suc i = length xs \<Longrightarrow> sublist_at ss (t # ts) (Suc i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>ys. ts = xs @ ss @ ys \<and> i = length xs
[PROOF STEP]
have "\<exists>ys. t#ts = (t#xs)@ss@ys \<and> Suc i = length (t#xs)"
[PROOF STATE]
proof (prove)
using this:
\<exists>ys. ts = xs @ ss @ ys \<and> i = length xs

goal (1 subgoal):
 1. \<exists>ys. t # ts = (t # xs) @ ss @ ys \<and> Suc i = length (t # xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>ys. t # ts = (t # xs) @ ss @ ys \<and> Suc i = length (t # xs)

goal (2 subgoals):
 1. sublist_at ss (t # ts) (Suc i) \<Longrightarrow> \<exists>xs ys. t # ts = xs @ ss @ ys \<and> Suc i = length xs
 2. \<exists>xs ys. t # ts = xs @ ss @ ys \<and> Suc i = length xs \<Longrightarrow> sublist_at ss (t # ts) (Suc i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>ys. t # ts = (t # xs) @ ss @ ys \<and> Suc i = length (t # xs)
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
using this:
\<exists>ys. t # ts = (t # xs) @ ss @ ys \<and> Suc i = length (t # xs)

goal (1 subgoal):
 1. \<exists>xs ys. t # ts = xs @ ss @ ys \<and> Suc i = length xs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>xs ys. t # ts = xs @ ss @ ys \<and> Suc i = length xs

goal (1 subgoal):
 1. \<exists>xs ys. t # ts = xs @ ss @ ys \<and> Suc i = length xs \<Longrightarrow> sublist_at ss (t # ts) (Suc i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>xs ys. t # ts = xs @ ss @ ys \<and> Suc i = length xs \<Longrightarrow> sublist_at ss (t # ts) (Suc i)
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
\<exists>xs ys. t # ts = xs @ ss @ ys \<and> Suc i = length xs

goal (1 subgoal):
 1. \<exists>xs ys. t # ts = xs @ ss @ ys \<and> Suc i = length xs \<Longrightarrow> sublist_at ss (t # ts) (Suc i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>xs ys. t # ts = xs @ ss @ ys \<and> Suc i = length xs
[PROOF STEP]
obtain xs where "\<exists>ys. t#ts = xs@ss@ys \<and> length xs = Suc i"
[PROOF STATE]
proof (prove)
using this:
\<exists>xs ys. t # ts = xs @ ss @ ys \<and> Suc i = length xs

goal (1 subgoal):
 1. (\<And>xs. \<exists>ys. t # ts = xs @ ss @ ys \<and> length xs = Suc i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (blast dest: sym)
[PROOF STATE]
proof (state)
this:
\<exists>ys. t # ts = xs @ ss @ ys \<and> length xs = Suc i

goal (1 subgoal):
 1. \<exists>xs ys. t # ts = xs @ ss @ ys \<and> Suc i = length xs \<Longrightarrow> sublist_at ss (t # ts) (Suc i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>ys. t # ts = xs @ ss @ ys \<and> length xs = Suc i
[PROOF STEP]
have "\<exists>ys. ts = (tl xs)@ss@ys \<and> i = length (tl xs)"
[PROOF STATE]
proof (prove)
using this:
\<exists>ys. t # ts = xs @ ss @ ys \<and> length xs = Suc i

goal (1 subgoal):
 1. \<exists>ys. ts = tl xs @ ss @ ys \<and> i = length (tl xs)
[PROOF STEP]
by (auto simp add: length_Suc_conv)
[PROOF STATE]
proof (state)
this:
\<exists>ys. ts = tl xs @ ss @ ys \<and> i = length (tl xs)

goal (1 subgoal):
 1. \<exists>xs ys. t # ts = xs @ ss @ ys \<and> Suc i = length xs \<Longrightarrow> sublist_at ss (t # ts) (Suc i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>ys. ts = tl xs @ ss @ ys \<and> i = length (tl xs)
[PROOF STEP]
have "\<exists>xs ys. ts = xs@ss@ys \<and> i = length xs"
[PROOF STATE]
proof (prove)
using this:
\<exists>ys. ts = tl xs @ ss @ ys \<and> i = length (tl xs)

goal (1 subgoal):
 1. \<exists>xs ys. ts = xs @ ss @ ys \<and> i = length xs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>xs ys. ts = xs @ ss @ ys \<and> i = length xs

goal (1 subgoal):
 1. \<exists>xs ys. t # ts = xs @ ss @ ys \<and> Suc i = length xs \<Longrightarrow> sublist_at ss (t # ts) (Suc i)
[PROOF STEP]
with "2.IH"
[PROOF STATE]
proof (chain)
picking this:
sublist_at ss ts i = (\<exists>ps ssa. ts = ps @ ss @ ssa \<and> i = length ps)
\<exists>xs ys. ts = xs @ ss @ ys \<and> i = length xs
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
using this:
sublist_at ss ts i = (\<exists>ps ssa. ts = ps @ ss @ ssa \<and> i = length ps)
\<exists>xs ys. ts = xs @ ss @ ys \<and> i = length xs

goal (1 subgoal):
 1. sublist_at ss (t # ts) (Suc i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sublist_at ss (t # ts) (Suc i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sublist_at ss (t # ts) (Suc i) = (\<exists>xs ys. t # ts = xs @ ss @ ys \<and> Suc i = length xs)

goal (4 subgoals):
 1. \<And>x xs y ys. sublist_at xs ys 0 = (\<exists>ps ss. ys = ps @ xs @ ss \<and> 0 = length ps) \<Longrightarrow> sublist_at (x # xs) (y # ys) 0 = (\<exists>ps ss. y # ys = ps @ (x # xs) @ ss \<and> 0 = length ps)
 2. \<And>ys. sublist_at [] ys 0 = (\<exists>ps ss. ys = ps @ [] @ ss \<and> 0 = length ps)
 3. \<And>v va uv_. sublist_at (v # va) [] uv_ = (\<exists>ps ss. [] = ps @ (v # va) @ ss \<and> uv_ = length ps)
 4. \<And>uu_ v. sublist_at uu_ [] (Suc v) = (\<exists>ps ss. [] = ps @ uu_ @ ss \<and> Suc v = length ps)
[PROOF STEP]
qed auto


[STATEMENT]
lemma is_arg_min_id: "is_arg_min id P i \<longleftrightarrow> P i \<and> (\<forall>ii<i. \<not>P ii)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_arg_min id P i = (P i \<and> (\<forall>ii<i. \<not> P ii))
[PROOF STEP]
unfolding is_arg_min_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P i \<and> (\<nexists>y. P y \<and> id y < id i)) = (P i \<and> (\<forall>ii<i. \<not> P ii))
[PROOF STEP]
by auto


[STATEMENT]
lemma kmp_result: "kmp_SPEC s t =
  RETURN (if sublist s t then Some (LEAST i. sublist_at s t i) else None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kmp_SPEC s t = RETURN (if sublist s t then Some (LEAST i. sublist_at s t i) else None)
[PROOF STEP]
unfolding kmp_SPEC_def sublist_iff_sublist_at
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SPEC (case_option (\<not> Ex (sublist_at s t)) (\<lambda>i. sublist_at s t i \<and> (\<forall>ii<i. \<not> sublist_at s t ii))) = RETURN (if Ex (sublist_at s t) then Some (LEAST i. sublist_at s t i) else None)
[PROOF STEP]
apply (auto intro: LeastI dest: not_less_Least split: option.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x x2. \<lbrakk>sublist_at s t x; sublist_at s t x2; \<forall>ii<x2. \<not> sublist_at s t ii\<rbrakk> \<Longrightarrow> x2 = Least (sublist_at s t)
[PROOF STEP]
by (meson LeastI nat_neq_iff not_less_Least)


[STATEMENT]
lemma "s \<noteq> [] \<Longrightarrow> naive_algorithm s t \<le> kmp_SPEC s t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<noteq> [] \<Longrightarrow> naive_algorithm s t \<le> kmp_SPEC s t
[PROOF STEP]
unfolding naive_algorithm_def kmp_SPEC_def I_out_na_def I_in_na_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<noteq> [] \<Longrightarrow> (let i = 0; j = 0; pos = None in WHILE\<^sub>T\<^bsup>\<lambda>(i, j, pos). (\<forall>ii<i. \<not> sublist_at s t ii) \<and> (case pos of None \<Rightarrow> j = 0 | Some p \<Rightarrow> p = i \<and> sublist_at s t i)\<^esup> (\<lambda>(i, uu_, pos). i + length s \<le> length t \<and> pos = None) (\<lambda>(i, j, pos). WHILE\<^sub>T\<^bsup>\<lambda>(j, pos). case pos of None \<Rightarrow> j < length s \<and> (\<forall>jj<j. t ! (i + jj) = s ! jj) | Some p \<Rightarrow> sublist_at s t i\<^esup> (\<lambda>(j, pos). t ! (i + j) = s ! j \<and> pos = None) (\<lambda>(j, uu_). let j = j + 1 in if j = length s then RETURN (j, Some i) else RETURN (j, None)) (j, pos) \<bind> (\<lambda>(uu_, pos). if pos = None then let i = i + 1; j = 0 in RETURN (i, j, None) else RETURN (i, j, Some i))) (i, j, pos) \<bind> (\<lambda>(uu_, uu_, pos). RETURN pos)) \<le> SPEC (case_option (\<not> Ex (sublist_at s t)) (\<lambda>i. sublist_at s t i \<and> (\<forall>ii<i. \<not> sublist_at s t ii)))
[PROOF STEP]
apply (refine_vcg
    WHILEIT_rule[where R="measure (\<lambda>(i,_,pos). length t - i + (if pos = None then 1 else 0))"]
    WHILEIT_rule[where R="measure (\<lambda>(j,_::nat option). length s - j)"]
    )
[PROOF STATE]
proof (prove)
goal (16 subgoals):
 1. s \<noteq> [] \<Longrightarrow> wf (measure (\<lambda>(i, uu_, pos). length t - i + (if pos = None then 1 else 0)))
 2. \<And>x1 x2 x1a x2a ii. \<lbrakk>s \<noteq> []; x2 = (x1a, x2a); (0, 0, None) = (x1, x2); ii < x1\<rbrakk> \<Longrightarrow> \<not> sublist_at s t ii
 3. \<And>x1 x2 x1a x2a. \<lbrakk>s \<noteq> []; x2 = (x1a, x2a); (0, 0, None) = (x1, x2)\<rbrakk> \<Longrightarrow> case x2a of None \<Rightarrow> x1a = 0 | Some p \<Rightarrow> p = x1 \<and> sublist_at s t x1
 4. \<And>sa a b aa ba. \<lbrakk>s \<noteq> []; case sa of (i, j, pos) \<Rightarrow> (\<forall>ii<i. \<not> sublist_at s t ii) \<and> (case pos of None \<Rightarrow> j = 0 | Some p \<Rightarrow> p = i \<and> sublist_at s t i); case sa of (i, uu_, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; sa = (a, b); b = (aa, ba)\<rbrakk> \<Longrightarrow> wf (measure (\<lambda>(j, uu_). length s - j))
 5. \<And>sa a b aa ba x1 x2. \<lbrakk>s \<noteq> []; case sa of (i, j, pos) \<Rightarrow> (\<forall>ii<i. \<not> sublist_at s t ii) \<and> (case pos of None \<Rightarrow> j = 0 | Some p \<Rightarrow> p = i \<and> sublist_at s t i); case sa of (i, uu_, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; sa = (a, b); b = (aa, ba); (aa, ba) = (x1, x2)\<rbrakk> \<Longrightarrow> case x2 of None \<Rightarrow> x1 < length s \<and> (\<forall>jj<x1. t ! (a + jj) = s ! jj) | Some p \<Rightarrow> sublist_at s t a
 6. \<And>sa a b aa ba saa ab bb x1 x2. \<lbrakk>s \<noteq> []; case sa of (i, j, pos) \<Rightarrow> (\<forall>ii<i. \<not> sublist_at s t ii) \<and> (case pos of None \<Rightarrow> j = 0 | Some p \<Rightarrow> p = i \<and> sublist_at s t i); case sa of (i, uu_, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; sa = (a, b); b = (aa, ba); case saa of (j, None) \<Rightarrow> j < length s \<and> (\<forall>jj<j. t ! (a + jj) = s ! jj) | (j, Some p) \<Rightarrow> sublist_at s t a; case saa of (j, pos) \<Rightarrow> t ! (a + j) = s ! j \<and> pos = None; saa = (ab, bb); ab + 1 = length s; (ab + 1, Some a) = (x1, x2)\<rbrakk> \<Longrightarrow> case x2 of None \<Rightarrow> x1 < length s \<and> (\<forall>jj<x1. t ! (a + jj) = s ! jj) | Some p \<Rightarrow> sublist_at s t a
 7. \<And>sa a b aa ba saa ab bb. \<lbrakk>s \<noteq> []; case sa of (i, j, pos) \<Rightarrow> (\<forall>ii<i. \<not> sublist_at s t ii) \<and> (case pos of None \<Rightarrow> j = 0 | Some p \<Rightarrow> p = i \<and> sublist_at s t i); case sa of (i, uu_, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; sa = (a, b); b = (aa, ba); case saa of (j, None) \<Rightarrow> j < length s \<and> (\<forall>jj<j. t ! (a + jj) = s ! jj) | (j, Some p) \<Rightarrow> sublist_at s t a; case saa of (j, pos) \<Rightarrow> t ! (a + j) = s ! j \<and> pos = None; saa = (ab, bb); ab + 1 = length s\<rbrakk> \<Longrightarrow> ((ab + 1, Some a), saa) \<in> measure (\<lambda>(j, uu_). length s - j)
 8. \<And>sa a b aa ba saa ab bb x1 x2. \<lbrakk>s \<noteq> []; case sa of (i, j, pos) \<Rightarrow> (\<forall>ii<i. \<not> sublist_at s t ii) \<and> (case pos of None \<Rightarrow> j = 0 | Some p \<Rightarrow> p = i \<and> sublist_at s t i); case sa of (i, uu_, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; sa = (a, b); b = (aa, ba); case saa of (j, None) \<Rightarrow> j < length s \<and> (\<forall>jj<j. t ! (a + jj) = s ! jj) | (j, Some p) \<Rightarrow> sublist_at s t a; case saa of (j, pos) \<Rightarrow> t ! (a + j) = s ! j \<and> pos = None; saa = (ab, bb); ab + 1 \<noteq> length s; (ab + 1, None) = (x1, x2)\<rbrakk> \<Longrightarrow> case x2 of None \<Rightarrow> x1 < length s \<and> (\<forall>jj<x1. t ! (a + jj) = s ! jj) | Some p \<Rightarrow> sublist_at s t a
 9. \<And>sa a b aa ba saa ab bb. \<lbrakk>s \<noteq> []; case sa of (i, j, pos) \<Rightarrow> (\<forall>ii<i. \<not> sublist_at s t ii) \<and> (case pos of None \<Rightarrow> j = 0 | Some p \<Rightarrow> p = i \<and> sublist_at s t i); case sa of (i, uu_, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; sa = (a, b); b = (aa, ba); case saa of (j, None) \<Rightarrow> j < length s \<and> (\<forall>jj<j. t ! (a + jj) = s ! jj) | (j, Some p) \<Rightarrow> sublist_at s t a; case saa of (j, pos) \<Rightarrow> t ! (a + j) = s ! j \<and> pos = None; saa = (ab, bb); ab + 1 \<noteq> length s\<rbrakk> \<Longrightarrow> ((ab + 1, None), saa) \<in> measure (\<lambda>(j, uu_). length s - j)
 10. \<And>sa a b aa ba saa ab bb x1 x2 x1a x2a ii. \<lbrakk>s \<noteq> []; case sa of (i, j, pos) \<Rightarrow> (\<forall>ii<i. \<not> sublist_at s t ii) \<and> (case pos of None \<Rightarrow> j = 0 | Some p \<Rightarrow> p = i \<and> sublist_at s t i); case sa of (i, uu_, pos) \<Rightarrow> i + length s \<le> length t \<and> pos = None; sa = (a, b); b = (aa, ba); case saa of (j, None) \<Rightarrow> j < length s \<and> (\<forall>jj<j. t ! (a + jj) = s ! jj) | (j, Some p) \<Rightarrow> sublist_at s t a; \<not> (case saa of (j, pos) \<Rightarrow> t ! (a + j) = s ! j \<and> pos = None); saa = (ab, bb); bb = None; x2 = (x1a, x2a); (a + 1, 0, None) = (x1, x2); ii < x1\<rbrakk> \<Longrightarrow> \<not> sublist_at s t ii
A total of 16 subgoals...
[PROOF STEP]
apply (vc_solve solve: asm_rl)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>ab aba. \<lbrakk>s \<noteq> []; \<forall>ii<ab. \<not> sublist_at s t ii; Suc (ab + aba) \<le> length t; \<forall>jj<aba. t ! (ab + jj) = s ! jj; t ! (ab + aba) = s ! aba; length s = Suc aba\<rbrakk> \<Longrightarrow> sublist_at s t ab
 2. \<And>ab aba jj. \<lbrakk>s \<noteq> []; \<forall>ii<ab. \<not> sublist_at s t ii; ab + length s \<le> length t; t ! (ab + aba) = s ! aba; Suc aba \<noteq> length s; aba < length s; \<forall>jj<aba. t ! (ab + jj) = s ! jj; jj < Suc aba\<rbrakk> \<Longrightarrow> t ! (ab + jj) = s ! jj
 3. \<And>ab aba ii. \<lbrakk>s \<noteq> []; \<forall>ii<ab. \<not> sublist_at s t ii; ab + length s \<le> length t; t ! (ab + aba) \<noteq> s ! aba; ii < Suc ab; aba < length s; \<forall>jj<aba. t ! (ab + jj) = s ! jj; sublist_at s t ii\<rbrakk> \<Longrightarrow> False
 4. \<And>ab aaa baa. \<lbrakk>s \<noteq> []; ab + length s \<le> length t \<longrightarrow> (\<exists>y. baa = Some y); \<forall>ii<ab. \<not> sublist_at s t ii; case baa of None \<Rightarrow> aaa = 0 | Some p \<Rightarrow> p = ab \<and> sublist_at s t ab\<rbrakk> \<Longrightarrow> case baa of None \<Rightarrow> \<not> Ex (sublist_at s t) | Some i \<Rightarrow> sublist_at s t i \<and> (\<forall>ii<i. \<not> sublist_at s t ii)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<noteq> []; \<forall>ii<ab_. \<not> sublist_at s t ii; Suc (ab_ + aba_) \<le> length t; \<forall>jj<aba_. t ! (ab_ + jj) = s ! jj; t ! (ab_ + aba_) = s ! aba_; length s = Suc aba_\<rbrakk> \<Longrightarrow> sublist_at s t ab_
[PROOF STEP]
by (metis add_Suc_right all_positions_sublist less_antisym)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ab aba jj. \<lbrakk>s \<noteq> []; \<forall>ii<ab. \<not> sublist_at s t ii; ab + length s \<le> length t; t ! (ab + aba) = s ! aba; Suc aba \<noteq> length s; aba < length s; \<forall>jj<aba. t ! (ab + jj) = s ! jj; jj < Suc aba\<rbrakk> \<Longrightarrow> t ! (ab + jj) = s ! jj
 2. \<And>ab aba ii. \<lbrakk>s \<noteq> []; \<forall>ii<ab. \<not> sublist_at s t ii; ab + length s \<le> length t; t ! (ab + aba) \<noteq> s ! aba; ii < Suc ab; aba < length s; \<forall>jj<aba. t ! (ab + jj) = s ! jj; sublist_at s t ii\<rbrakk> \<Longrightarrow> False
 3. \<And>ab aaa baa. \<lbrakk>s \<noteq> []; ab + length s \<le> length t \<longrightarrow> (\<exists>y. baa = Some y); \<forall>ii<ab. \<not> sublist_at s t ii; case baa of None \<Rightarrow> aaa = 0 | Some p \<Rightarrow> p = ab \<and> sublist_at s t ab\<rbrakk> \<Longrightarrow> case baa of None \<Rightarrow> \<not> Ex (sublist_at s t) | Some i \<Rightarrow> sublist_at s t i \<and> (\<forall>ii<i. \<not> sublist_at s t ii)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<noteq> []; \<forall>ii<ab_. \<not> sublist_at s t ii; ab_ + length s \<le> length t; t ! (ab_ + aba_) = s ! aba_; Suc aba_ \<noteq> length s; aba_ < length s; \<forall>jj<aba_. t ! (ab_ + jj) = s ! jj; jj_ < Suc aba_\<rbrakk> \<Longrightarrow> t ! (ab_ + jj_) = s ! jj_
[PROOF STEP]
using less_Suc_eq
[PROOF STATE]
proof (prove)
using this:
(?m < Suc ?n) = (?m < ?n \<or> ?m = ?n)

goal (1 subgoal):
 1. \<lbrakk>s \<noteq> []; \<forall>ii<ab_. \<not> sublist_at s t ii; ab_ + length s \<le> length t; t ! (ab_ + aba_) = s ! aba_; Suc aba_ \<noteq> length s; aba_ < length s; \<forall>jj<aba_. t ! (ab_ + jj) = s ! jj; jj_ < Suc aba_\<rbrakk> \<Longrightarrow> t ! (ab_ + jj_) = s ! jj_
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ab aba ii. \<lbrakk>s \<noteq> []; \<forall>ii<ab. \<not> sublist_at s t ii; ab + length s \<le> length t; t ! (ab + aba) \<noteq> s ! aba; ii < Suc ab; aba < length s; \<forall>jj<aba. t ! (ab + jj) = s ! jj; sublist_at s t ii\<rbrakk> \<Longrightarrow> False
 2. \<And>ab aaa baa. \<lbrakk>s \<noteq> []; ab + length s \<le> length t \<longrightarrow> (\<exists>y. baa = Some y); \<forall>ii<ab. \<not> sublist_at s t ii; case baa of None \<Rightarrow> aaa = 0 | Some p \<Rightarrow> p = ab \<and> sublist_at s t ab\<rbrakk> \<Longrightarrow> case baa of None \<Rightarrow> \<not> Ex (sublist_at s t) | Some i \<Rightarrow> sublist_at s t i \<and> (\<forall>ii<i. \<not> sublist_at s t ii)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<noteq> []; \<forall>ii<ab_. \<not> sublist_at s t ii; ab_ + length s \<le> length t; t ! (ab_ + aba_) \<noteq> s ! aba_; ii_ < Suc ab_; aba_ < length s; \<forall>jj<aba_. t ! (ab_ + jj) = s ! jj; sublist_at s t ii_\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (metis less_SucE sublist_all_positions)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ab aaa baa. \<lbrakk>s \<noteq> []; ab + length s \<le> length t \<longrightarrow> (\<exists>y. baa = Some y); \<forall>ii<ab. \<not> sublist_at s t ii; case baa of None \<Rightarrow> aaa = 0 | Some p \<Rightarrow> p = ab \<and> sublist_at s t ab\<rbrakk> \<Longrightarrow> case baa of None \<Rightarrow> \<not> Ex (sublist_at s t) | Some i \<Rightarrow> sublist_at s t i \<and> (\<forall>ii<i. \<not> sublist_at s t ii)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<noteq> []; ab_ + length s \<le> length t \<longrightarrow> (\<exists>y. baa_ = Some y); \<forall>ii<ab_. \<not> sublist_at s t ii; case baa_ of None \<Rightarrow> aaa_ = 0 | Some p \<Rightarrow> p = ab_ \<and> sublist_at s t ab_\<rbrakk> \<Longrightarrow> case baa_ of None \<Rightarrow> \<not> Ex (sublist_at s t) | Some i \<Rightarrow> sublist_at s t i \<and> (\<forall>ii<i. \<not> sublist_at s t ii)
[PROOF STEP]
by (auto split: option.splits) (metis sublist_lengths add_less_cancel_right leI le_less_trans)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma borderE[elim]:
  fixes xs ys :: "'a list"
  assumes "border xs ys"
  obtains "prefix xs ys" and "suffix xs ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>prefix xs ys; suffix xs ys\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
border xs ys

goal (1 subgoal):
 1. (\<lbrakk>prefix xs ys; suffix xs ys\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding border_def
[PROOF STATE]
proof (prove)
using this:
prefix xs ys \<and> suffix xs ys

goal (1 subgoal):
 1. (\<lbrakk>prefix xs ys; suffix xs ys\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast