[STATEMENT]
lemma sequential_completion_Runs:
  assumes "sc_completion s vs"
  and "\<And>vs ln. ta_seq_consist P vs (llist_of (convert_RA ln))"
  shows "\<exists>ttas. mthr.Runs s ttas \<and> ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ttas. mthr.Runs s ttas \<and> ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))
[PROOF STEP]
using complete_sc_ta_seq_consist[OF assms] complete_sc_in_Runs[OF assms]
[PROOF STATE]
proof (prove)
using this:
ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (complete_sc s vs)))
mthr.Runs s (complete_sc s vs)

goal (1 subgoal):
 1. \<exists>ttas. mthr.Runs s ttas \<and> ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))
[PROOF STEP]
by blast


[STATEMENT]
lemma cut_and_updateI[intro?]:
  "(\<And>ttas s' t x ta x' m'.
     \<lbrakk> s -\<triangleright>ttas\<rightarrow>* s'; ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)));
       thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>; t \<turnstile> (x, shr s') -ta\<rightarrow> (x', m'); actions_ok s' t ta \<rbrakk>
      \<Longrightarrow> \<exists>ta' x'' m''. t \<turnstile> (x, shr s') -ta'\<rightarrow> (x'', m'') \<and> actions_ok s' t ta' \<and>
                       ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>) \<and>
                       eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))))
    \<Longrightarrow> cut_and_update s vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ttas s' t x ta x' m'. \<lbrakk>s -\<triangleright>ttas\<rightarrow>* s'; ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))); thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>; t \<turnstile> \<langle>x, shr s'\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>; actions_ok s' t ta\<rbrakk> \<Longrightarrow> \<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s' t ta' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>) \<and> eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<Longrightarrow> cut_and_update s vs
[PROOF STEP]
unfolding cut_and_update_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ttas s' t x ta x' m'. \<lbrakk>s -\<triangleright>ttas\<rightarrow>* s'; ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))); thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>; t \<turnstile> \<langle>x, shr s'\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>; actions_ok s' t ta\<rbrakk> \<Longrightarrow> \<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s' t ta' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>) \<and> eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))) \<Longrightarrow> \<forall>ttas s' t x ta x' m'. s -\<triangleright>ttas\<rightarrow>* s' \<longrightarrow> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<longrightarrow> thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor> \<longrightarrow> t \<turnstile> \<langle>x, shr s'\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle> \<longrightarrow> actions_ok s' t ta \<longrightarrow> (\<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s' t ta' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>) \<and> eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))))
[PROOF STEP]
by blast


[STATEMENT]
lemma cut_and_updateD:
  "\<lbrakk> cut_and_update s vs; s -\<triangleright>ttas\<rightarrow>* s'; ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)));
     thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>; t \<turnstile> (x, shr s') -ta\<rightarrow> (x', m'); actions_ok s' t ta \<rbrakk>
  \<Longrightarrow> \<exists>ta' x'' m''. t \<turnstile> (x, shr s') -ta'\<rightarrow> (x'', m'') \<and> actions_ok s' t ta' \<and>
                   ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>) \<and>
                   eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cut_and_update s vs; s -\<triangleright>ttas\<rightarrow>* s'; ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))); thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>; t \<turnstile> \<langle>x, shr s'\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>; actions_ok s' t ta\<rbrakk> \<Longrightarrow> \<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s' t ta' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>) \<and> eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
[PROOF STEP]
unfolding cut_and_update_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ttas s' t x ta x' m'. s -\<triangleright>ttas\<rightarrow>* s' \<longrightarrow> ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) \<longrightarrow> thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor> \<longrightarrow> t \<turnstile> \<langle>x, shr s'\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle> \<longrightarrow> actions_ok s' t ta \<longrightarrow> (\<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s' t ta' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>) \<and> eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas)))); s -\<triangleright>ttas\<rightarrow>* s'; ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))); thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>; t \<turnstile> \<langle>x, shr s'\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>; actions_ok s' t ta\<rbrakk> \<Longrightarrow> \<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s' t ta' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>) \<and> eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
[PROOF STEP]
by blast


[STATEMENT]
lemma cut_and_update_imp_sc_completion:
  "cut_and_update s vs \<Longrightarrow> sc_completion s vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cut_and_update s vs \<Longrightarrow> sc_completion s vs
[PROOF STEP]
apply(rule sc_completionI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ttas s' t x ta x' m'. \<lbrakk>cut_and_update s vs; s -\<triangleright>ttas\<rightarrow>* s'; ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))); thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>; t \<turnstile> \<langle>x, shr s'\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>; actions_ok s' t ta\<rbrakk> \<Longrightarrow> \<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s' t ta' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)
[PROOF STEP]
apply(drule (5) cut_and_updateD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ttas s' t x ta x' m'. \<lbrakk>s -\<triangleright>ttas\<rightarrow>* s'; ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))); thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>; t \<turnstile> \<langle>x, shr s'\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>; actions_ok s' t ta; \<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s' t ta' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>) \<and> eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> \<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s' t ta' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sequential_completion:
  assumes cut_and_update: "cut_and_update s vs"
  and ta_seq_consist_convert_RA: "\<And>vs ln. ta_seq_consist P vs (llist_of (convert_RA ln))"
  and Red: "s -\<triangleright>ttas\<rightarrow>* s'"
  and sc: "ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))"
  and red: "s' -t\<triangleright>ta\<rightarrow> s''"
  shows
  "\<exists>ta' ttas'. mthr.Runs s' (LCons (t, ta') ttas') \<and>
     ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') ttas')))) \<and>
     eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ta' ttas'. mthr.Runs s' (LCons (t, ta') ttas') \<and> ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') ttas')))) \<and> eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>ta' ttas'. mthr.Runs s' (LCons (t, ta') ttas') \<and> ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') ttas')))) \<and> eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
[PROOF STEP]
from red
[PROOF STATE]
proof (chain)
picking this:
s' -t\<triangleright>ta\<rightarrow> s''
[PROOF STEP]
obtain ta' s'''
    where red': "redT s' (t, ta') s'''"
    and sc': "ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil))))"
    and eq: "eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))"
[PROOF STATE]
proof (prove)
using this:
s' -t\<triangleright>ta\<rightarrow> s''

goal (1 subgoal):
 1. (\<And>ta' s'''. \<lbrakk>s' -t\<triangleright>ta'\<rightarrow> s'''; ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil)))); eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x x' m'. \<lbrakk>\<And>ta' s'''. \<lbrakk>s' -t\<triangleright>ta'\<rightarrow> s'''; ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil)))); eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> thesis; t \<turnstile> \<langle>x, shr s'\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>; thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>; actions_ok s' t ta; redT_upd s' t ta x' m' s''\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x n ln. \<lbrakk>\<And>ta' s'''. \<lbrakk>s' -t\<triangleright>ta'\<rightarrow> s'''; ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil)))); eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> thesis; ta = (K$ [], [], [], [], [], convert_RA ln); thr s' t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s' t); may_acquire_all (locks s') t ln; 0 < ln $ n; s'' = (acquire_all (locks s') t ln, (thr s'(t \<mapsto> (x, no_wait_locks)), shr s'), wset s', interrupts s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (redT_normal x x' m')
[PROOF STATE]
proof (state)
this:
t \<turnstile> \<langle>x, shr s'\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>
thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>
actions_ok s' t ta
redT_upd s' t ta x' m' s''

goal (2 subgoals):
 1. \<And>x x' m'. \<lbrakk>\<And>ta' s'''. \<lbrakk>s' -t\<triangleright>ta'\<rightarrow> s'''; ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil)))); eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> thesis; t \<turnstile> \<langle>x, shr s'\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>; thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>; actions_ok s' t ta; redT_upd s' t ta x' m' s''\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x n ln. \<lbrakk>\<And>ta' s'''. \<lbrakk>s' -t\<triangleright>ta'\<rightarrow> s'''; ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil)))); eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> thesis; ta = (K$ [], [], [], [], [], convert_RA ln); thr s' t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s' t); may_acquire_all (locks s') t ln; 0 < ln $ n; s'' = (acquire_all (locks s') t ln, (thr s'(t \<mapsto> (x, no_wait_locks)), shr s'), wset s', interrupts s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
note ts't = \<open>thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>\<close>
      and red = \<open>t \<turnstile> \<langle>x, shr s'\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>\<close>
      and aok = \<open>actions_ok s' t ta\<close>
      and s'' = \<open>redT_upd s' t ta x' m' s''\<close>
[PROOF STATE]
proof (state)
this:
thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>
t \<turnstile> \<langle>x, shr s'\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>
actions_ok s' t ta
redT_upd s' t ta x' m' s''

goal (2 subgoals):
 1. \<And>x x' m'. \<lbrakk>\<And>ta' s'''. \<lbrakk>s' -t\<triangleright>ta'\<rightarrow> s'''; ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil)))); eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> thesis; t \<turnstile> \<langle>x, shr s'\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>; thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>; actions_ok s' t ta; redT_upd s' t ta x' m' s''\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x n ln. \<lbrakk>\<And>ta' s'''. \<lbrakk>s' -t\<triangleright>ta'\<rightarrow> s'''; ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil)))); eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> thesis; ta = (K$ [], [], [], [], [], convert_RA ln); thr s' t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s' t); may_acquire_all (locks s') t ln; 0 < ln $ n; s'' = (acquire_all (locks s') t ln, (thr s'(t \<mapsto> (x, no_wait_locks)), shr s'), wset s', interrupts s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from cut_and_updateD[OF cut_and_update, OF Red sc ts't red aok]
[PROOF STATE]
proof (chain)
picking this:
\<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s' t ta' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>) \<and> eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
[PROOF STEP]
obtain ta' x'' m'' where red: "t \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle>"
      and sc': "ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)"
      and eq: "eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))"
      and aok: "actions_ok s' t ta'"
[PROOF STATE]
proof (prove)
using this:
\<exists>ta' x'' m''. t \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle> \<and> actions_ok s' t ta' \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>) \<and> eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))

goal (1 subgoal):
 1. (\<And>ta' x'' m''. \<lbrakk>t \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle>; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>); eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas))); actions_ok s' t ta'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle>
ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)
eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
actions_ok s' t ta'

goal (2 subgoals):
 1. \<And>x x' m'. \<lbrakk>\<And>ta' s'''. \<lbrakk>s' -t\<triangleright>ta'\<rightarrow> s'''; ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil)))); eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> thesis; t \<turnstile> \<langle>x, shr s'\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>; thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>; actions_ok s' t ta; redT_upd s' t ta x' m' s''\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x n ln. \<lbrakk>\<And>ta' s'''. \<lbrakk>s' -t\<triangleright>ta'\<rightarrow> s'''; ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil)))); eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> thesis; ta = (K$ [], [], [], [], [], convert_RA ln); thr s' t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s' t); may_acquire_all (locks s') t ln; 0 < ln $ n; s'' = (acquire_all (locks s') t ln, (thr s'(t \<mapsto> (x, no_wait_locks)), shr s'), wset s', interrupts s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
obtain ws''' where "redT_updWs t (wset s') \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> ws'''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ws'''. redT_updWs t (wset s') \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> ws''' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using redT_updWs_total
[PROOF STATE]
proof (prove)
using this:
\<exists>ws'. redT_updWs ?t ?ws ?was ws'

goal (1 subgoal):
 1. (\<And>ws'''. redT_updWs t (wset s') \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> ws''' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
redT_updWs t (wset s') \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> ws'''

goal (2 subgoals):
 1. \<And>x x' m'. \<lbrakk>\<And>ta' s'''. \<lbrakk>s' -t\<triangleright>ta'\<rightarrow> s'''; ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil)))); eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> thesis; t \<turnstile> \<langle>x, shr s'\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>; thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>; actions_ok s' t ta; redT_upd s' t ta x' m' s''\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x n ln. \<lbrakk>\<And>ta' s'''. \<lbrakk>s' -t\<triangleright>ta'\<rightarrow> s'''; ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil)))); eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> thesis; ta = (K$ [], [], [], [], [], convert_RA ln); thr s' t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s' t); may_acquire_all (locks s') t ln; 0 < ln $ n; s'' = (acquire_all (locks s') t ln, (thr s'(t \<mapsto> (x, no_wait_locks)), shr s'), wset s', interrupts s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
redT_updWs t (wset s') \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> ws'''
[PROOF STEP]
obtain s''' where s''': "redT_upd s' t ta' x'' m'' s'''"
[PROOF STATE]
proof (prove)
using this:
redT_updWs t (wset s') \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> ws'''

goal (1 subgoal):
 1. (\<And>s'''. redT_upd s' t ta' x'' m'' s''' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
redT_upd s' t ta' x'' m'' s'''

goal (2 subgoals):
 1. \<And>x x' m'. \<lbrakk>\<And>ta' s'''. \<lbrakk>s' -t\<triangleright>ta'\<rightarrow> s'''; ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil)))); eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> thesis; t \<turnstile> \<langle>x, shr s'\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>; thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>; actions_ok s' t ta; redT_upd s' t ta x' m' s''\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x n ln. \<lbrakk>\<And>ta' s'''. \<lbrakk>s' -t\<triangleright>ta'\<rightarrow> s'''; ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil)))); eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> thesis; ta = (K$ [], [], [], [], [], convert_RA ln); thr s' t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s' t); may_acquire_all (locks s') t ln; 0 < ln $ n; s'' = (acquire_all (locks s') t ln, (thr s'(t \<mapsto> (x, no_wait_locks)), shr s'), wset s', interrupts s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
with red \<open>thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>\<close> aok
[PROOF STATE]
proof (chain)
picking this:
t \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle>
thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>
actions_ok s' t ta'
redT_upd s' t ta' x'' m'' s'''
[PROOF STEP]
have "s' -t\<triangleright>ta'\<rightarrow> s'''"
[PROOF STATE]
proof (prove)
using this:
t \<turnstile> \<langle>x, shr s'\<rangle> -ta'\<rightarrow> \<langle>x'', m''\<rangle>
thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>
actions_ok s' t ta'
redT_upd s' t ta' x'' m'' s'''

goal (1 subgoal):
 1. s' -t\<triangleright>ta'\<rightarrow> s'''
[PROOF STEP]
by(rule redT.redT_normal)
[PROOF STATE]
proof (state)
this:
s' -t\<triangleright>ta'\<rightarrow> s'''

goal (2 subgoals):
 1. \<And>x x' m'. \<lbrakk>\<And>ta' s'''. \<lbrakk>s' -t\<triangleright>ta'\<rightarrow> s'''; ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil)))); eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> thesis; t \<turnstile> \<langle>x, shr s'\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>; thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>; actions_ok s' t ta; redT_upd s' t ta x' m' s''\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x n ln. \<lbrakk>\<And>ta' s'''. \<lbrakk>s' -t\<triangleright>ta'\<rightarrow> s'''; ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil)))); eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> thesis; ta = (K$ [], [], [], [], [], convert_RA ln); thr s' t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s' t); may_acquire_all (locks s') t ln; 0 < ln $ n; s'' = (acquire_all (locks s') t ln, (thr s'(t \<mapsto> (x, no_wait_locks)), shr s'), wset s', interrupts s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s' -t\<triangleright>ta'\<rightarrow> s'''

goal (2 subgoals):
 1. \<And>x x' m'. \<lbrakk>\<And>ta' s'''. \<lbrakk>s' -t\<triangleright>ta'\<rightarrow> s'''; ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil)))); eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> thesis; t \<turnstile> \<langle>x, shr s'\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>; thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>; actions_ok s' t ta; redT_upd s' t ta x' m' s''\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x n ln. \<lbrakk>\<And>ta' s'''. \<lbrakk>s' -t\<triangleright>ta'\<rightarrow> s'''; ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil)))); eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> thesis; ta = (K$ [], [], [], [], [], convert_RA ln); thr s' t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s' t); may_acquire_all (locks s') t ln; 0 < ln $ n; s'' = (acquire_all (locks s') t ln, (thr s'(t \<mapsto> (x, no_wait_locks)), shr s'), wset s', interrupts s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from sc sc'
[PROOF STATE]
proof (chain)
picking this:
ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)
[PROOF STEP]
have "ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil))))"
[PROOF STATE]
proof (prove)
using this:
ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, y). \<lbrace>y\<rbrace>\<^bsub>o\<^esub>) ttas))) (llist_of \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub>)

goal (1 subgoal):
 1. ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil))))
[PROOF STEP]
by(auto simp add: lmap_lappend_distrib ta_seq_consist_lappend split_def lconcat_llist_of[symmetric] o_def list_of_lconcat)
[PROOF STATE]
proof (state)
this:
ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil))))

goal (2 subgoals):
 1. \<And>x x' m'. \<lbrakk>\<And>ta' s'''. \<lbrakk>s' -t\<triangleright>ta'\<rightarrow> s'''; ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil)))); eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> thesis; t \<turnstile> \<langle>x, shr s'\<rangle> -ta\<rightarrow> \<langle>x', m'\<rangle>; thr s' t = \<lfloor>(x, no_wait_locks)\<rfloor>; actions_ok s' t ta; redT_upd s' t ta x' m' s''\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x n ln. \<lbrakk>\<And>ta' s'''. \<lbrakk>s' -t\<triangleright>ta'\<rightarrow> s'''; ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil)))); eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> thesis; ta = (K$ [], [], [], [], [], convert_RA ln); thr s' t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s' t); may_acquire_all (locks s') t ln; 0 < ln $ n; s'' = (acquire_all (locks s') t ln, (thr s'(t \<mapsto> (x, no_wait_locks)), shr s'), wset s', interrupts s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s' -t\<triangleright>ta'\<rightarrow> s'''
ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil))))
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
s' -t\<triangleright>ta'\<rightarrow> s'''
ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil))))

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using eq
[PROOF STATE]
proof (prove)
using this:
s' -t\<triangleright>ta'\<rightarrow> s'''
ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil))))
eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))

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

goal (1 subgoal):
 1. \<And>x n ln. \<lbrakk>\<And>ta' s'''. \<lbrakk>s' -t\<triangleright>ta'\<rightarrow> s'''; ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil)))); eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> thesis; ta = (K$ [], [], [], [], [], convert_RA ln); thr s' t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s' t); may_acquire_all (locks s') t ln; 0 < ln $ n; s'' = (acquire_all (locks s') t ln, (thr s'(t \<mapsto> (x, no_wait_locks)), shr s'), wset s', interrupts s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x n ln. \<lbrakk>\<And>ta' s'''. \<lbrakk>s' -t\<triangleright>ta'\<rightarrow> s'''; ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil)))); eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> thesis; ta = (K$ [], [], [], [], [], convert_RA ln); thr s' t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s' t); may_acquire_all (locks s') t ln; 0 < ln $ n; s'' = (acquire_all (locks s') t ln, (thr s'(t \<mapsto> (x, no_wait_locks)), shr s'), wset s', interrupts s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (redT_acquire x ln n)
[PROOF STATE]
proof (state)
this:
ta = (K$ [], [], [], [], [], convert_RA n)
thr s' t = \<lfloor>(x, n)\<rfloor>
\<not> waiting (wset s' t)
may_acquire_all (locks s') t n
0 < n $ ln
s'' = (acquire_all (locks s') t n, (thr s'(t \<mapsto> (x, no_wait_locks)), shr s'), wset s', interrupts s')

goal (1 subgoal):
 1. \<And>x n ln. \<lbrakk>\<And>ta' s'''. \<lbrakk>s' -t\<triangleright>ta'\<rightarrow> s'''; ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil)))); eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> thesis; ta = (K$ [], [], [], [], [], convert_RA ln); thr s' t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s' t); may_acquire_all (locks s') t ln; 0 < ln $ n; s'' = (acquire_all (locks s') t ln, (thr s'(t \<mapsto> (x, no_wait_locks)), shr s'), wset s', interrupts s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence "ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta) LNil))))"
      and "eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))"
[PROOF STATE]
proof (prove)
using this:
ta = (K$ [], [], [], [], [], convert_RA n)
thr s' t = \<lfloor>(x, n)\<rfloor>
\<not> waiting (wset s' t)
may_acquire_all (locks s') t n
0 < n $ ln
s'' = (acquire_all (locks s') t n, (thr s'(t \<mapsto> (x, no_wait_locks)), shr s'), wset s', interrupts s')

goal (1 subgoal):
 1. ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta) LNil)))) &&& eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
[PROOF STEP]
using sc
[PROOF STATE]
proof (prove)
using this:
ta = (K$ [], [], [], [], [], convert_RA n)
thr s' t = \<lfloor>(x, n)\<rfloor>
\<not> waiting (wset s' t)
may_acquire_all (locks s') t n
0 < n $ ln
s'' = (acquire_all (locks s') t n, (thr s'(t \<mapsto> (x, no_wait_locks)), shr s'), wset s', interrupts s')
ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))

goal (1 subgoal):
 1. ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta) LNil)))) &&& eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
[PROOF STEP]
by(simp_all add: lmap_lappend_distrib ta_seq_consist_lappend split_def lconcat_llist_of[symmetric] o_def list_of_lconcat ta_seq_consist_convert_RA ta_seq_consist_imp_eq_upto_seq_inconsist_refl)
[PROOF STATE]
proof (state)
this:
ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta) LNil))))
eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))

goal (1 subgoal):
 1. \<And>x n ln. \<lbrakk>\<And>ta' s'''. \<lbrakk>s' -t\<triangleright>ta'\<rightarrow> s'''; ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil)))); eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))\<rbrakk> \<Longrightarrow> thesis; ta = (K$ [], [], [], [], [], convert_RA ln); thr s' t = \<lfloor>(x, ln)\<rfloor>; \<not> waiting (wset s' t); may_acquire_all (locks s') t ln; 0 < ln $ n; s'' = (acquire_all (locks s') t ln, (thr s'(t \<mapsto> (x, no_wait_locks)), shr s'), wset s', interrupts s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
with red
[PROOF STATE]
proof (chain)
picking this:
s' -t\<triangleright>ta\<rightarrow> s''
ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta) LNil))))
eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
s' -t\<triangleright>ta\<rightarrow> s''
ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta) LNil))))
eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s' -t\<triangleright>ta'\<rightarrow> s'''
ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil))))
eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))

goal (1 subgoal):
 1. \<exists>ta' ttas'. mthr.Runs s' (LCons (t, ta') ttas') \<and> ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') ttas')))) \<and> eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
[PROOF STEP]
txt \<open>Now, find a sequentially consistent completion from @{term "s'''"} onwards.\<close>
[PROOF STATE]
proof (state)
this:
s' -t\<triangleright>ta'\<rightarrow> s'''
ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil))))
eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))

goal (1 subgoal):
 1. \<exists>ta' ttas'. mthr.Runs s' (LCons (t, ta') ttas') \<and> ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') ttas')))) \<and> eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
[PROOF STEP]
from Red red'
[PROOF STATE]
proof (chain)
picking this:
s -\<triangleright>ttas\<rightarrow>* s'
s' -t\<triangleright>ta'\<rightarrow> s'''
[PROOF STEP]
have Red': "s -\<triangleright>ttas @ [(t, ta')]\<rightarrow>* s'''"
[PROOF STATE]
proof (prove)
using this:
s -\<triangleright>ttas\<rightarrow>* s'
s' -t\<triangleright>ta'\<rightarrow> s'''

goal (1 subgoal):
 1. s -\<triangleright>ttas @ [(t, ta')]\<rightarrow>* s'''
[PROOF STEP]
unfolding RedT_def
[PROOF STATE]
proof (prove)
using this:
mthr.Trsys s ttas s'
s' -t\<triangleright>ta'\<rightarrow> s'''

goal (1 subgoal):
 1. mthr.Trsys s (ttas @ [(t, ta')]) s'''
[PROOF STEP]
by(auto intro: rtrancl3p_step)
[PROOF STATE]
proof (state)
this:
s -\<triangleright>ttas @ [(t, ta')]\<rightarrow>* s'''

goal (1 subgoal):
 1. \<exists>ta' ttas'. mthr.Runs s' (LCons (t, ta') ttas') \<and> ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') ttas')))) \<and> eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
[PROOF STEP]
from sc sc'
[PROOF STATE]
proof (chain)
picking this:
ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil))))
[PROOF STEP]
have "ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (llist_of (ttas @ [(t, ta')]))))"
[PROOF STATE]
proof (prove)
using this:
ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil))))

goal (1 subgoal):
 1. ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (llist_of (ttas @ [(t, ta')]))))
[PROOF STEP]
by(simp add: o_def split_def lappend_llist_of_llist_of[symmetric])
[PROOF STATE]
proof (state)
this:
ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (llist_of (ttas @ [(t, ta')]))))

goal (1 subgoal):
 1. \<exists>ta' ttas'. mthr.Runs s' (LCons (t, ta') ttas') \<and> ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') ttas')))) \<and> eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
[PROOF STEP]
with cut_and_update_imp_sc_completion[OF cut_and_update] Red'
[PROOF STATE]
proof (chain)
picking this:
sc_completion s vs
s -\<triangleright>ttas @ [(t, ta')]\<rightarrow>* s'''
ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (llist_of (ttas @ [(t, ta')]))))
[PROOF STEP]
have "sc_completion s''' (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas @ [(t, ta')]))))"
[PROOF STATE]
proof (prove)
using this:
sc_completion s vs
s -\<triangleright>ttas @ [(t, ta')]\<rightarrow>* s'''
ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (llist_of (ttas @ [(t, ta')]))))

goal (1 subgoal):
 1. sc_completion s''' (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas @ [(t, ta')]))))
[PROOF STEP]
by(rule sc_completion_shift)
[PROOF STATE]
proof (state)
this:
sc_completion s''' (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas @ [(t, ta')]))))

goal (1 subgoal):
 1. \<exists>ta' ttas'. mthr.Runs s' (LCons (t, ta') ttas') \<and> ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') ttas')))) \<and> eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
[PROOF STEP]
from sequential_completion_Runs[OF this ta_seq_consist_convert_RA]
[PROOF STATE]
proof (chain)
picking this:
\<exists>ttasa. mthr.Runs s''' ttasa \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas @ [(t, ta')])))) (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttasa))
[PROOF STEP]
obtain ttas' where \<tau>Runs: "mthr.Runs s''' ttas'"
    and sc'': "ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas @ [(t, ta')]))))
                                (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))"
[PROOF STATE]
proof (prove)
using this:
\<exists>ttasa. mthr.Runs s''' ttasa \<and> ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas @ [(t, ta')])))) (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttasa))

goal (1 subgoal):
 1. (\<And>ttas'. \<lbrakk>mthr.Runs s''' ttas'; ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas @ [(t, ta')])))) (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mthr.Runs s''' ttas'
ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas @ [(t, ta')])))) (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))

goal (1 subgoal):
 1. \<exists>ta' ttas'. mthr.Runs s' (LCons (t, ta') ttas') \<and> ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') ttas')))) \<and> eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
[PROOF STEP]
from red' \<tau>Runs
[PROOF STATE]
proof (chain)
picking this:
s' -t\<triangleright>ta'\<rightarrow> s'''
mthr.Runs s''' ttas'
[PROOF STEP]
have "mthr.Runs s' (LCons (t, ta') ttas')"
[PROOF STATE]
proof (prove)
using this:
s' -t\<triangleright>ta'\<rightarrow> s'''
mthr.Runs s''' ttas'

goal (1 subgoal):
 1. mthr.Runs s' (LCons (t, ta') ttas')
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
mthr.Runs s' (LCons (t, ta') ttas')

goal (1 subgoal):
 1. \<exists>ta' ttas'. mthr.Runs s' (LCons (t, ta') ttas') \<and> ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') ttas')))) \<and> eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mthr.Runs s' (LCons (t, ta') ttas')

goal (1 subgoal):
 1. \<exists>ta' ttas'. mthr.Runs s' (LCons (t, ta') ttas') \<and> ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') ttas')))) \<and> eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
[PROOF STEP]
from sc sc' sc''
[PROOF STATE]
proof (chain)
picking this:
ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil))))
ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas @ [(t, ta')])))) (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))
[PROOF STEP]
have "ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') ttas'))))"
[PROOF STATE]
proof (prove)
using this:
ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') LNil))))
ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas @ [(t, ta')])))) (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))

goal (1 subgoal):
 1. ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') ttas'))))
[PROOF STEP]
unfolding lmap_lappend_distrib lconcat_lappend
[PROOF STATE]
proof (prove)
using this:
ta_seq_consist P vs (llist_of (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
ta_seq_consist P vs (lconcat (lappend (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (llist_of ttas)) (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (LCons (t, ta') LNil))))
ta_seq_consist P (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (ttas @ [(t, ta')])))) (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas'))

goal (1 subgoal):
 1. ta_seq_consist P vs (lconcat (lappend (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (llist_of ttas)) (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (LCons (t, ta') ttas'))))
[PROOF STEP]
by(simp add: o_def ta_seq_consist_lappend split_def list_of_lconcat)
[PROOF STATE]
proof (state)
this:
ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') ttas'))))

goal (1 subgoal):
 1. \<exists>ta' ttas'. mthr.Runs s' (LCons (t, ta') ttas') \<and> ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') ttas')))) \<and> eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mthr.Runs s' (LCons (t, ta') ttas')
ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') ttas'))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mthr.Runs s' (LCons (t, ta') ttas')
ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') ttas'))))

goal (1 subgoal):
 1. \<exists>ta' ttas'. mthr.Runs s' (LCons (t, ta') ttas') \<and> ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') ttas')))) \<and> eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
[PROOF STEP]
using eq
[PROOF STATE]
proof (prove)
using this:
mthr.Runs s' (LCons (t, ta') ttas')
ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') ttas'))))
eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))

goal (1 subgoal):
 1. \<exists>ta' ttas'. mthr.Runs s' (LCons (t, ta') ttas') \<and> ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') ttas')))) \<and> eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>ta' ttas'. mthr.Runs s' (LCons (t, ta') ttas') \<and> ta_seq_consist P vs (lconcat (lmap (\<lambda>(t, ta). llist_of \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) (lappend (llist_of ttas) (LCons (t, ta') ttas')))) \<and> eq_upto_seq_inconsist P \<lbrace>ta\<rbrace>\<^bsub>o\<^esub> \<lbrace>ta'\<rbrace>\<^bsub>o\<^esub> (mrw_values P vs (concat (map (\<lambda>(t, ta). \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>) ttas)))

goal:
No subgoals!
[PROOF STEP]
qed


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


[STATEMENT]
lemma shead_bottom_iff[simp]: "(shead\<cdot>xs = \<bottom>) \<longleftrightarrow> (xs = \<bottom> \<or> xs = [::])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (shead\<cdot>xs = \<bottom>) = (xs = \<bottom> \<or> xs = [::])
[PROOF STEP]
by (cases xs) simp_all


[STATEMENT]
lemma stail_bottom_iff[simp]: "(stail\<cdot>xs = \<bottom>) \<longleftrightarrow> (xs = \<bottom> \<or> xs = [::])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (stail\<cdot>xs = \<bottom>) = (xs = \<bottom> \<or> xs = [::])
[PROOF STEP]
by (cases xs) simp_all


[STATEMENT]
lemma match_snil_match_scons_slist_case: "match_snil\<cdot>xs\<cdot>k1 +++ match_scons\<cdot>xs\<cdot>k2 = slist_case\<cdot>k1\<cdot>k2\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match_snil\<cdot>xs\<cdot>k1 +++ match_scons\<cdot>xs\<cdot>k2 = slist_case\<cdot>k1\<cdot>k2\<cdot>xs
[PROOF STEP]
by (cases xs) simp_all


[STATEMENT]
lemma slist_bottom': "slist_case\<cdot>\<bottom>\<cdot>\<bottom>\<cdot>xs = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> [::]. \<bottom>)\<cdot>xs = \<bottom>
[PROOF STEP]
by (cases xs; simp)


[STATEMENT]
lemma slist_bottom[simp]: "slist_case\<cdot>\<bottom>\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> [::]. \<bottom>) = \<bottom>
[PROOF STEP]
by (simp add: cfun_eq_iff slist_bottom')


[STATEMENT]
lemma slist_case_distr:
  "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> f\<cdot>(slist_case\<cdot>g\<cdot>h\<cdot>xs) = slist_case\<cdot>(f\<cdot>g)\<cdot>(\<Lambda> x xs. f\<cdot>(h\<cdot>x\<cdot>xs))\<cdot>xs"
  "slist_case\<cdot>g'\<cdot>h'\<cdot>xs\<cdot>z = slist_case\<cdot>(g'\<cdot>z)\<cdot>(\<Lambda> x xs. h'\<cdot>x\<cdot>xs\<cdot>z)\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> f\<cdot>(slist_case\<cdot>g\<cdot>h\<cdot>xs) = (case xs of [::] \<Rightarrow> f\<cdot>g | x :# xs \<Rightarrow> f\<cdot>(h\<cdot>x\<cdot>xs))) &&& slist_case\<cdot>g'\<cdot>h'\<cdot>xs\<cdot>z = (case xs of [::] \<Rightarrow> g'\<cdot>z | x :# xs \<Rightarrow> h'\<cdot>x\<cdot>xs\<cdot>z)
[PROOF STEP]
by (case_tac [!] xs) simp_all


[STATEMENT]
lemma slist_case_cong:
  assumes "xs = xs'"
  assumes "xs' = [::] \<Longrightarrow> n = n'"
  assumes "\<And>y ys. \<lbrakk>xs' = y :# ys; y \<noteq> \<bottom>; ys \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> c y ys = c' y ys"
  assumes "cont (\<lambda>(x, y). c x y)"
  assumes "cont (\<lambda>(x, y). c' x y)"
  shows "slist_case\<cdot>n\<cdot>(\<Lambda> x xs. c x xs)\<cdot>xs = slist_case\<cdot>n'\<cdot>(\<Lambda> x xs. c' x xs)\<cdot>xs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case xs of [::] \<Rightarrow> n | x :# xs \<Rightarrow> c x xs) = (case xs' of [::] \<Rightarrow> n' | x :# xs \<Rightarrow> c' x xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs = xs'
xs' = [::] \<Longrightarrow> n = n'
\<lbrakk>xs' = ?y :# ?ys; ?y \<noteq> \<bottom>; ?ys \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> c ?y ?ys = c' ?y ?ys
cont (\<lambda>(x, y). c x y)
cont (\<lambda>(x, y). c' x y)

goal (1 subgoal):
 1. (case xs of [::] \<Rightarrow> n | x :# xs \<Rightarrow> c x xs) = (case xs' of [::] \<Rightarrow> n' | x :# xs \<Rightarrow> c' x xs)
[PROOF STEP]
by (cases xs; cases xs'; clarsimp simp: prod_cont_iff)


[STATEMENT]
lemma slist_eq_TT_snil[simp]:
  fixes xs :: "[:'a::Eq:]"
  shows "(eq\<cdot>xs\<cdot>[::] = TT) \<longleftrightarrow> (xs = [::])"
        "(eq\<cdot>[::]\<cdot>xs = TT) \<longleftrightarrow> (xs = [::])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (eq\<cdot>xs\<cdot>[::] = TT) = (xs = [::]) &&& (eq\<cdot>[::]\<cdot>xs = TT) = (xs = [::])
[PROOF STEP]
by (cases xs; simp)+


[STATEMENT]
lemma slist_eq_FF_snil[simp]:
  fixes xs :: "[:'a::Eq:]"
  shows "(eq\<cdot>xs\<cdot>[::] = FF) \<longleftrightarrow> (\<exists>y ys. y \<noteq> \<bottom> \<and> ys \<noteq> \<bottom> \<and> xs = y :# ys)"
        "(eq\<cdot>[::]\<cdot>xs = FF) \<longleftrightarrow> (\<exists>y ys. y \<noteq> \<bottom> \<and> ys \<noteq> \<bottom> \<and> xs = y :# ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (eq\<cdot>xs\<cdot>[::] = FF) = (\<exists>y ys. y \<noteq> \<bottom> \<and> ys \<noteq> \<bottom> \<and> xs = y :# ys) &&& (eq\<cdot>[::]\<cdot>xs = FF) = (\<exists>y ys. y \<noteq> \<bottom> \<and> ys \<noteq> \<bottom> \<and> xs = y :# ys)
[PROOF STEP]
by (cases xs; force)+


[STATEMENT]
lemma slistmem_bottom1[iff]:
  fixes x :: "'a"
  shows "\<not> slistmem x \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> slistmem x \<bottom>
[PROOF STEP]
by rule (induct x "\<bottom>::[:'a:]" rule: slistmem.induct; fastforce)


[STATEMENT]
lemma slistmem_bottom2[iff]:
  fixes xs :: "[:'a:]"
  shows "\<not> slistmem \<bottom> xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> slistmem \<bottom> xs
[PROOF STEP]
by rule (induct "\<bottom>::'a" xs rule: slistmem.induct; fastforce)


[STATEMENT]
lemma slistmem_nil[iff]:
  shows "\<not> slistmem x [::]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> slistmem x [::]
[PROOF STEP]
by (fastforce elim: slistmem.cases)


[STATEMENT]
lemma slistmem_scons[simp]:
  shows "slistmem x (y :# ys) \<longleftrightarrow> (x = y \<and> x \<noteq> \<bottom> \<and> ys \<noteq> \<bottom>) \<or> (slistmem x ys \<and> y \<noteq> \<bottom>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slistmem x (y :# ys) = (x = y \<and> x \<noteq> \<bottom> \<and> ys \<noteq> \<bottom> \<or> slistmem x ys \<and> y \<noteq> \<bottom>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. slistmem x (y :# ys) = (x = y \<and> x \<noteq> \<bottom> \<and> ys \<noteq> \<bottom> \<or> slistmem x ys \<and> y \<noteq> \<bottom>)
[PROOF STEP]
have "x = y \<or> slistmem x ys" if "slistmem x (y :# ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y \<or> slistmem x ys
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
slistmem x (y :# ys)

goal (1 subgoal):
 1. x = y \<or> slistmem x ys
[PROOF STEP]
by (induct "x" "y :# ys" arbitrary: y ys rule: slistmem.induct; force)
[PROOF STATE]
proof (state)
this:
slistmem x (y :# ys) \<Longrightarrow> x = y \<or> slistmem x ys

goal (1 subgoal):
 1. slistmem x (y :# ys) = (x = y \<and> x \<noteq> \<bottom> \<and> ys \<noteq> \<bottom> \<or> slistmem x ys \<and> y \<noteq> \<bottom>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
slistmem x (y :# ys) \<Longrightarrow> x = y \<or> slistmem x ys
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
slistmem x (y :# ys) \<Longrightarrow> x = y \<or> slistmem x ys

goal (1 subgoal):
 1. slistmem x (y :# ys) = (x = y \<and> x \<noteq> \<bottom> \<and> ys \<noteq> \<bottom> \<or> slistmem x ys \<and> y \<noteq> \<bottom>)
[PROOF STEP]
by (auto elim: slistmem.cases intro: slistmem.intros)
[PROOF STATE]
proof (state)
this:
slistmem x (y :# ys) = (x = y \<and> x \<noteq> \<bottom> \<and> ys \<noteq> \<bottom> \<or> slistmem x ys \<and> y \<noteq> \<bottom>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sset_simp[simp]:
  shows "sset \<bottom> = {}"
    and "sset [::] = {}"
    and "\<lbrakk>x \<noteq> \<bottom>; xs \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> sset (x :# xs) = insert x (sset xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sset \<bottom> = {} &&& sset [::] = {} &&& (\<lbrakk>x \<noteq> \<bottom>; xs \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> sset (x :# xs) = insert x (sset xs))
[PROOF STEP]
unfolding sset_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. slistmem x \<bottom>} = {} &&& {x. slistmem x [::]} = {} &&& (\<lbrakk>x \<noteq> \<bottom>; xs \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> {xa. slistmem xa (x :# xs)} = insert x {x. slistmem x xs})
[PROOF STEP]
by (auto elim: slistmem.cases intro: slistmem.intros)


[STATEMENT]
lemma sset_defined[simp]:
  assumes "x \<in> sset xs"
  shows "x \<noteq> \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> \<bottom>
[PROOF STEP]
using assms sset_def
[PROOF STATE]
proof (prove)
using this:
x \<in> sset xs
sset ?xs = {x. slistmem x ?xs}

goal (1 subgoal):
 1. x \<noteq> \<bottom>
[PROOF STEP]
by force


[STATEMENT]
lemma sset_below:
  assumes "y \<in> sset ys"
  assumes "xs \<sqsubseteq> ys"
  assumes "xs \<noteq> \<bottom>"
  obtains x where "x \<in> sset xs" and "x \<sqsubseteq> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> sset xs; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
y \<in> sset ys
xs \<sqsubseteq> ys
xs \<noteq> \<bottom>

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> sset xs; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(induct ys arbitrary: xs)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>xs. \<lbrakk>\<And>x. \<lbrakk>x \<in> sset xs; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> thesis; y \<in> sset \<bottom>; xs \<sqsubseteq> \<bottom>; xs \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> thesis
 2. \<And>xs. \<lbrakk>\<And>x. \<lbrakk>x \<in> sset xs; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> thesis; y \<in> sset [::]; xs \<sqsubseteq> [::]; xs \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> thesis
 3. \<And>a ys xs. \<lbrakk>a \<noteq> \<bottom>; ys \<noteq> \<bottom>; \<And>xs. \<lbrakk>\<And>x. \<lbrakk>x \<in> sset xs; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> thesis; y \<in> sset ys; xs \<sqsubseteq> ys; xs \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> thesis; \<And>x. \<lbrakk>x \<in> sset xs; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> thesis; y \<in> sset (a :# ys); xs \<sqsubseteq> a :# ys; xs \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (scons y ys xs)
[PROOF STATE]
proof (state)
this:
y \<noteq> \<bottom>
ys \<noteq> \<bottom>
\<lbrakk>\<And>x. \<lbrakk>x \<in> sset ?xs; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> thesis; y \<in> sset ys; ?xs \<sqsubseteq> ys; ?xs \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>?x \<in> sset xs; ?x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> thesis
y \<in> sset (y :# ys)
xs \<sqsubseteq> y :# ys
xs \<noteq> \<bottom>

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

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

goal (2 subgoals):
 1. \<And>xs. \<lbrakk>\<And>x. \<lbrakk>x \<in> sset xs; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> thesis; y \<in> sset \<bottom>; xs \<sqsubseteq> \<bottom>; xs \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> thesis
 2. \<And>xs. \<lbrakk>\<And>x. \<lbrakk>x \<in> sset xs; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> thesis; y \<in> sset [::]; xs \<sqsubseteq> [::]; xs \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
qed simp_all


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


[STATEMENT]
lemma snull_bottom_iff[simp]: "(snull\<cdot>xs = \<bottom>) \<longleftrightarrow> (xs = \<bottom>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (snull\<cdot>xs = \<bottom>) = (xs = \<bottom>)
[PROOF STEP]
by (cases xs) simp_all


[STATEMENT]
lemma snull_FF_conv: "(snull\<cdot>xxs = FF) \<longleftrightarrow> (\<exists>x xs. xxs \<noteq> \<bottom> \<and> xxs = x :# xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (snull\<cdot>xxs = FF) = (\<exists>x xs. xxs \<noteq> \<bottom> \<and> xxs = x :# xs)
[PROOF STEP]
by (cases xxs) simp_all


[STATEMENT]
lemma snull_eq_snil: "snull\<cdot>xs = eq\<cdot>xs\<cdot>[::]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snull\<cdot>xs = eq\<cdot>xs\<cdot>[::]
[PROOF STEP]
by (cases xs) simp_all


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


[STATEMENT]
lemma smap_bottom_iff[simp]: "(smap\<cdot>f\<cdot>xs = \<bottom>) \<longleftrightarrow> (xs = \<bottom> \<or> (\<exists>x\<in>sset xs. f\<cdot>x = \<bottom>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (smap\<cdot>f\<cdot>xs = \<bottom>) = (xs = \<bottom> \<or> (\<exists>x\<in>sset xs. f\<cdot>x = \<bottom>))
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma smap_is_snil_conv[simp]:
  "(smap\<cdot>f\<cdot>xs = [::]) \<longleftrightarrow> (xs = [::])"
  "( [::] = smap\<cdot>f\<cdot>xs) \<longleftrightarrow> (xs = [::])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (smap\<cdot>f\<cdot>xs = [::]) = (xs = [::]) &&& ([::] = smap\<cdot>f\<cdot>xs) = (xs = [::])
[PROOF STEP]
by (cases xs; simp)+


[STATEMENT]
lemma smap_strict_scons[simp]:
  assumes "f\<cdot>\<bottom> = \<bottom>"
  shows "smap\<cdot>f\<cdot>(x :# xs) = f\<cdot>x :# smap\<cdot>f\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smap\<cdot>f\<cdot>(x :# xs) = f\<cdot>x :# smap\<cdot>f\<cdot>xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f\<cdot>\<bottom> = \<bottom>

goal (1 subgoal):
 1. smap\<cdot>f\<cdot>(x :# xs) = f\<cdot>x :# smap\<cdot>f\<cdot>xs
[PROOF STEP]
by (cases "x :# xs = \<bottom>"; fastforce)


[STATEMENT]
lemma smap_ID': "smap\<cdot>ID\<cdot>xs = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smap\<cdot>ID\<cdot>xs = xs
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma smap_ID[simp]: "smap\<cdot>ID = ID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smap\<cdot>ID = ID
[PROOF STEP]
by (clarsimp simp: cfun_eq_iff smap_ID')


[STATEMENT]
lemma smap_cong:
  assumes "xs = xs'"
  assumes "\<And>x. x \<in> sset xs \<Longrightarrow> f\<cdot>x = f'\<cdot>x"
  shows "smap\<cdot>f\<cdot>xs = smap\<cdot>f'\<cdot>xs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smap\<cdot>f\<cdot>xs = smap\<cdot>f'\<cdot>xs'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs = xs'
?x \<in> sset xs \<Longrightarrow> f\<cdot>?x = f'\<cdot>?x

goal (1 subgoal):
 1. smap\<cdot>f\<cdot>xs = smap\<cdot>f'\<cdot>xs'
[PROOF STEP]
by (induct xs arbitrary: xs') auto


[STATEMENT]
lemma smap_smap'[simp]:
  assumes "f\<cdot>\<bottom> = \<bottom>"
  shows "smap\<cdot>f\<cdot>(smap\<cdot>g\<cdot>xs) = smap\<cdot>(f oo g)\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smap\<cdot>f\<cdot>(smap\<cdot>g\<cdot>xs) = smap\<cdot>(f oo g)\<cdot>xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f\<cdot>\<bottom> = \<bottom>

goal (1 subgoal):
 1. smap\<cdot>f\<cdot>(smap\<cdot>g\<cdot>xs) = smap\<cdot>(f oo g)\<cdot>xs
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma smap_smap[simp]:
  assumes "f\<cdot>\<bottom> = \<bottom>"
  shows "smap\<cdot>f oo smap\<cdot>g = smap\<cdot>(f oo g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smap\<cdot>f oo smap\<cdot>g = smap\<cdot>(f oo g)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f\<cdot>\<bottom> = \<bottom>

goal (1 subgoal):
 1. smap\<cdot>f oo smap\<cdot>g = smap\<cdot>(f oo g)
[PROOF STEP]
by (clarsimp simp: cfun_eq_iff)


[STATEMENT]
lemma sset_smap[simp]:
  assumes "\<And>x. x \<in> sset xs \<Longrightarrow> f\<cdot>x \<noteq> \<bottom>"
  shows "sset (smap\<cdot>f\<cdot>xs) = { f\<cdot>x | x. x \<in> sset xs }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sset (smap\<cdot>f\<cdot>xs) = {f\<cdot>x |x. x \<in> sset xs}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?x \<in> sset xs \<Longrightarrow> f\<cdot>?x \<noteq> \<bottom>

goal (1 subgoal):
 1. sset (smap\<cdot>f\<cdot>xs) = {f\<cdot>x |x. x \<in> sset xs}
[PROOF STEP]
by (induct xs) auto


[STATEMENT]
lemma shead_smap_distr:
  assumes "f\<cdot>\<bottom> = \<bottom>"
  assumes "\<And>x. x\<in>sset xs \<Longrightarrow> f\<cdot>x \<noteq> \<bottom>"
  shows "shead\<cdot>(smap\<cdot>f\<cdot>xs) = f\<cdot>(shead\<cdot>xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shead\<cdot>(smap\<cdot>f\<cdot>xs) = f\<cdot>(shead\<cdot>xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f\<cdot>\<bottom> = \<bottom>
?x \<in> sset xs \<Longrightarrow> f\<cdot>?x \<noteq> \<bottom>

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


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


[STATEMENT]
lemma sappend_strict2[simp]: "xs :@ \<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs :@ \<bottom> = \<bottom>
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma sappend_bottom_iff[simp]: "(xs :@ ys = \<bottom>) \<longleftrightarrow> (xs = \<bottom> \<or> ys = \<bottom>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs :@ ys = \<bottom>) = (xs = \<bottom> \<or> ys = \<bottom>)
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma sappend_scons[simp]: "(x :# xs) :@ ys = x :# xs :@ ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x :# xs) :@ ys = x :# xs :@ ys
[PROOF STEP]
by (cases "x :# xs = \<bottom>"; fastforce)


[STATEMENT]
lemma sappend_assoc[simp]: "(xs :@ ys) :@ zs = xs :@ (ys :@ zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs :@ ys) :@ zs = xs :@ ys :@ zs
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma sappend_snil_id_left[simp]: "sappend\<cdot>[::] = ID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sappend\<cdot>[::] = ID
[PROOF STEP]
by (simp add: cfun_eq_iff)


[STATEMENT]
lemma sappend_snil_id_right[iff]: "xs :@ [::] = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs :@ [::] = xs
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma snil_append_iff[iff]: "xs :@ ys = [::] \<longleftrightarrow> xs = [::] \<and> ys = [::]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs :@ ys = [::]) = (xs = [::] \<and> ys = [::])
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma smap_sappend[simp]: "smap\<cdot>f\<cdot>(xs :@ ys) = smap\<cdot>f\<cdot>xs :@ smap\<cdot>f\<cdot>ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smap\<cdot>f\<cdot>(xs :@ ys) = smap\<cdot>f\<cdot>xs :@ smap\<cdot>f\<cdot>ys
[PROOF STEP]
by (induct xs; cases "ys = \<bottom>"; simp)


[STATEMENT]
lemma stail_sappend: "stail\<cdot>(xs :@ ys) = (case xs of [::] \<Rightarrow> stail\<cdot>ys | z :# zs \<Rightarrow> zs :@ ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stail\<cdot>(xs :@ ys) = (case xs of [::] \<Rightarrow> stail\<cdot>ys | z :# zs \<Rightarrow> zs :@ ys)
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma stail_append2[simp]: "xs \<noteq> [::] \<Longrightarrow> stail\<cdot>(xs :@ ys) = stail\<cdot>xs :@ ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [::] \<Longrightarrow> stail\<cdot>(xs :@ ys) = stail\<cdot>xs :@ ys
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma slist_case_snoc:
  "g\<cdot>\<bottom>\<cdot>\<bottom> = \<bottom> \<Longrightarrow> slist_case\<cdot>f\<cdot>g\<cdot>(xs :@ [:x:]) = g\<cdot>(shead\<cdot>(xs :@ [:x:]))\<cdot>(stail\<cdot>(xs :@ [:x:]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g\<cdot>\<bottom>\<cdot>\<bottom> = \<bottom> \<Longrightarrow> slist_case\<cdot>f\<cdot>g\<cdot>(xs :@ [:x:]) = g\<cdot>(shead\<cdot>(xs :@ [:x:]))\<cdot>(stail\<cdot>(xs :@ [:x:]))
[PROOF STEP]
by (cases "x = \<bottom>"; cases xs; clarsimp)


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


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

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


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


[STATEMENT]
lemma sall_TT[simp]: "(sall\<cdot>p\<cdot>xs = TT) \<longleftrightarrow> (xs \<noteq> \<bottom> \<and> (\<forall>x\<in>sset xs. p\<cdot>x = TT))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sall\<cdot>p\<cdot>xs = TT) = (xs \<noteq> \<bottom> \<and> (\<forall>x\<in>sset xs. p\<cdot>x = TT))
[PROOF STEP]
by (induct xs) simp_all


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


[STATEMENT]
lemma sfilter_bottom_iff[simp]: "(sfilter\<cdot>p\<cdot>xs = \<bottom>) \<longleftrightarrow> (xs = \<bottom> \<or> (\<exists>x\<in>sset xs. p\<cdot>x = \<bottom>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sfilter\<cdot>p\<cdot>xs = \<bottom>) = (xs = \<bottom> \<or> (\<exists>x\<in>sset xs. p\<cdot>x = \<bottom>))
[PROOF STEP]
by (induct xs) (use trE in auto)


[STATEMENT]
lemma sset_sfilter[simp]:
  assumes "\<And>x. x \<in> sset xs \<Longrightarrow> p\<cdot>x \<noteq> \<bottom>"
  shows "sset (sfilter\<cdot>p\<cdot>xs) = {x |x. x \<in> sset xs \<and> p\<cdot>x = TT}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sset (sfilter\<cdot>p\<cdot>xs) = {x |x. x \<in> sset xs \<and> p\<cdot>x = TT}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?x \<in> sset xs \<Longrightarrow> p\<cdot>?x \<noteq> \<bottom>

goal (1 subgoal):
 1. sset (sfilter\<cdot>p\<cdot>xs) = {x |x. x \<in> sset xs \<and> p\<cdot>x = TT}
[PROOF STEP]
by (induct xs) (fastforce simp: If2_def[symmetric] split: If2_splits)+


[STATEMENT]
lemma sfilter_strict_scons[simp]:
  assumes "p\<cdot>\<bottom> = \<bottom>"
  shows "sfilter\<cdot>p\<cdot>(x :# xs) = If p\<cdot>x then x :# sfilter\<cdot>p\<cdot>xs else sfilter\<cdot>p\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sfilter\<cdot>p\<cdot>(x :# xs) = If p\<cdot>x then x :# sfilter\<cdot>p\<cdot>xs else sfilter\<cdot>p\<cdot>xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p\<cdot>\<bottom> = \<bottom>

goal (1 subgoal):
 1. sfilter\<cdot>p\<cdot>(x :# xs) = If p\<cdot>x then x :# sfilter\<cdot>p\<cdot>xs else sfilter\<cdot>p\<cdot>xs
[PROOF STEP]
by (cases "x = \<bottom>"; cases "xs = \<bottom>"; simp)


[STATEMENT]
lemma sfilter_scons_let:
  assumes "p\<cdot>\<bottom> = \<bottom>"
  shows "sfilter\<cdot>p\<cdot>(x :# xs) = (let xs' = sfilter\<cdot>p\<cdot>xs in If p\<cdot>x then x :# xs' else xs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sfilter\<cdot>p\<cdot>(x :# xs) = (let xs' = sfilter\<cdot>p\<cdot>xs in If p\<cdot>x then x :# xs' else xs')
[PROOF STEP]
unfolding Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sfilter\<cdot>p\<cdot>(x :# xs) = If p\<cdot>x then x :# sfilter\<cdot>p\<cdot>xs else sfilter\<cdot>p\<cdot>xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p\<cdot>\<bottom> = \<bottom>

goal (1 subgoal):
 1. sfilter\<cdot>p\<cdot>(x :# xs) = If p\<cdot>x then x :# sfilter\<cdot>p\<cdot>xs else sfilter\<cdot>p\<cdot>xs
[PROOF STEP]
by simp


[STATEMENT]
lemma sfilter_sappend[simp]: "sfilter\<cdot>p\<cdot>(xs :@ ys) = sfilter\<cdot>p\<cdot>xs :@ sfilter\<cdot>p\<cdot>ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sfilter\<cdot>p\<cdot>(xs :@ ys) = sfilter\<cdot>p\<cdot>xs :@ sfilter\<cdot>p\<cdot>ys
[PROOF STEP]
by (cases "ys"; clarsimp) (induct xs; fastforce simp: If2_def[symmetric] split: If2_splits)


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

goal (1 subgoal):
 1. sfilter\<cdot>(\<Lambda> x. FF)\<cdot>xs = [::]
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma sfilter_const_FF_conv[simp]: "(sfilter\<cdot>(\<Lambda> x. FF)\<cdot>xs = [::]) \<longleftrightarrow> (xs \<noteq> \<bottom>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sfilter\<cdot>(\<Lambda> x. FF)\<cdot>xs = [::]) = (xs \<noteq> \<bottom>)
[PROOF STEP]
by auto


[STATEMENT]
lemma sfilter_const_TT[simp]: "sfilter\<cdot>(\<Lambda> x. TT)\<cdot>xs = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sfilter\<cdot>(\<Lambda> x. TT)\<cdot>xs = xs
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma sfilter_cong:
  assumes "xs = xs'"
  assumes "\<And>x. x \<in> sset xs \<Longrightarrow> p\<cdot>x = p'\<cdot>x"
  shows "sfilter\<cdot>p\<cdot>xs = sfilter\<cdot>p'\<cdot>xs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sfilter\<cdot>p\<cdot>xs = sfilter\<cdot>p'\<cdot>xs'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs = xs'
?x \<in> sset xs \<Longrightarrow> p\<cdot>?x = p'\<cdot>?x

goal (1 subgoal):
 1. sfilter\<cdot>p\<cdot>xs = sfilter\<cdot>p'\<cdot>xs'
[PROOF STEP]
by (induct xs arbitrary: xs') auto


[STATEMENT]
lemma sfilter_snil_conv[simp]: "sfilter\<cdot>p\<cdot>xs = [::] \<longleftrightarrow> sall\<cdot>(neg oo p)\<cdot>xs = TT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sfilter\<cdot>p\<cdot>xs = [::]) = (sall\<cdot>(neg oo p)\<cdot>xs = TT)
[PROOF STEP]
by (induct xs; force simp: If2_def[symmetric] split: If2_splits)


[STATEMENT]
lemma sfilter_sfilter': "sfilter\<cdot>p\<cdot>(sfilter\<cdot>q\<cdot>xs) = sfilter\<cdot>(\<Lambda> x. q\<cdot>x andalso p\<cdot>x)\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sfilter\<cdot>p\<cdot>(sfilter\<cdot>q\<cdot>xs) = sfilter\<cdot>(\<Lambda> x. q\<cdot>x andalso p\<cdot>x)\<cdot>xs
[PROOF STEP]
proof(induct xs)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. sfilter\<cdot>p\<cdot>(sfilter\<cdot>q\<cdot>\<bottom>) = sfilter\<cdot>(\<Lambda> x. q\<cdot>x andalso p\<cdot>x)\<cdot>\<bottom>
 2. sfilter\<cdot>p\<cdot>(sfilter\<cdot>q\<cdot>[::]) = sfilter\<cdot>(\<Lambda> x. q\<cdot>x andalso p\<cdot>x)\<cdot>[::]
 3. \<And>a xs. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; sfilter\<cdot>p\<cdot>(sfilter\<cdot>q\<cdot>xs) = sfilter\<cdot>(\<Lambda> x. q\<cdot>x andalso p\<cdot>x)\<cdot>xs\<rbrakk> \<Longrightarrow> sfilter\<cdot>p\<cdot>(sfilter\<cdot>q\<cdot>(a :# xs)) = sfilter\<cdot>(\<Lambda> x. q\<cdot>x andalso p\<cdot>x)\<cdot>(a :# xs)
[PROOF STEP]
case (scons x xs)
[PROOF STATE]
proof (state)
this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
sfilter\<cdot>p\<cdot>(sfilter\<cdot>q\<cdot>xs) = sfilter\<cdot>(\<Lambda> x. q\<cdot>x andalso p\<cdot>x)\<cdot>xs

goal (3 subgoals):
 1. sfilter\<cdot>p\<cdot>(sfilter\<cdot>q\<cdot>\<bottom>) = sfilter\<cdot>(\<Lambda> x. q\<cdot>x andalso p\<cdot>x)\<cdot>\<bottom>
 2. sfilter\<cdot>p\<cdot>(sfilter\<cdot>q\<cdot>[::]) = sfilter\<cdot>(\<Lambda> x. q\<cdot>x andalso p\<cdot>x)\<cdot>[::]
 3. \<And>a xs. \<lbrakk>a \<noteq> \<bottom>; xs \<noteq> \<bottom>; sfilter\<cdot>p\<cdot>(sfilter\<cdot>q\<cdot>xs) = sfilter\<cdot>(\<Lambda> x. q\<cdot>x andalso p\<cdot>x)\<cdot>xs\<rbrakk> \<Longrightarrow> sfilter\<cdot>p\<cdot>(sfilter\<cdot>q\<cdot>(a :# xs)) = sfilter\<cdot>(\<Lambda> x. q\<cdot>x andalso p\<cdot>x)\<cdot>(a :# xs)
[PROOF STEP]
from scons(1, 2)
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<noteq> \<bottom>
xs \<noteq> \<bottom>

goal (1 subgoal):
 1. sfilter\<cdot>p\<cdot>(sfilter\<cdot>q\<cdot>(x :# xs)) = sfilter\<cdot>(\<Lambda> x. q\<cdot>x andalso p\<cdot>x)\<cdot>(x :# xs)
[PROOF STEP]
by (cases "sfilter\<cdot>q\<cdot>xs = \<bottom>")
       (simp_all add: If_distr If_andalso scons(3)[symmetric] del: sfilter_bottom_iff)
[PROOF STATE]
proof (state)
this:
sfilter\<cdot>p\<cdot>(sfilter\<cdot>q\<cdot>(x :# xs)) = sfilter\<cdot>(\<Lambda> x. q\<cdot>x andalso p\<cdot>x)\<cdot>(x :# xs)

goal (2 subgoals):
 1. sfilter\<cdot>p\<cdot>(sfilter\<cdot>q\<cdot>\<bottom>) = sfilter\<cdot>(\<Lambda> x. q\<cdot>x andalso p\<cdot>x)\<cdot>\<bottom>
 2. sfilter\<cdot>p\<cdot>(sfilter\<cdot>q\<cdot>[::]) = sfilter\<cdot>(\<Lambda> x. q\<cdot>x andalso p\<cdot>x)\<cdot>[::]
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma sfilter_sfilter: "sfilter\<cdot>p oo sfilter\<cdot>q = sfilter\<cdot>(\<Lambda> x. q\<cdot>x andalso p\<cdot>x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sfilter\<cdot>p oo sfilter\<cdot>q = sfilter\<cdot>(\<Lambda> x. q\<cdot>x andalso p\<cdot>x)
[PROOF STEP]
by (clarsimp simp: cfun_eq_iff sfilter_sfilter')


[STATEMENT]
lemma sfilter_smap':
  assumes "p\<cdot>\<bottom> = \<bottom>"
  shows "sfilter\<cdot>p\<cdot>(smap\<cdot>f\<cdot>xs) = smap\<cdot>f\<cdot>(sfilter\<cdot>(p oo f)\<cdot>xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sfilter\<cdot>p\<cdot>(smap\<cdot>f\<cdot>xs) = smap\<cdot>f\<cdot>(sfilter\<cdot>(p oo f)\<cdot>xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p\<cdot>\<bottom> = \<bottom>

goal (1 subgoal):
 1. sfilter\<cdot>p\<cdot>(smap\<cdot>f\<cdot>xs) = smap\<cdot>f\<cdot>(sfilter\<cdot>(p oo f)\<cdot>xs)
[PROOF STEP]
by (induct xs; simp add: If2_def[symmetric] split: If2_splits) (metis slist.con_rews(2) smap.simps(2) smap_strict)


[STATEMENT]
lemma sfilter_smap:
  assumes "p\<cdot>\<bottom> = \<bottom>"
  shows "sfilter\<cdot>p oo smap\<cdot>f = smap\<cdot>f oo sfilter\<cdot>(p oo f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sfilter\<cdot>p oo smap\<cdot>f = smap\<cdot>f oo sfilter\<cdot>(p oo f)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p\<cdot>\<bottom> = \<bottom>

goal (1 subgoal):
 1. sfilter\<cdot>p oo smap\<cdot>f = smap\<cdot>f oo sfilter\<cdot>(p oo f)
[PROOF STEP]
by (clarsimp simp: cfun_eq_iff sfilter_smap')


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


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

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


[STATEMENT]
lemma sfoldl_cong:
  assumes "xs = xs'"
  assumes "z = z'"
  assumes "\<And>x z. x \<in> sset xs \<Longrightarrow> f\<cdot>z\<cdot>x = f'\<cdot>z\<cdot>x"
  shows "sfoldl\<cdot>f\<cdot>z\<cdot>xs = sfoldl\<cdot>f'\<cdot>z'\<cdot>xs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sfoldl\<cdot>f\<cdot>z\<cdot>xs = sfoldl\<cdot>f'\<cdot>z'\<cdot>xs'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs = xs'
z = z'
?x \<in> sset xs \<Longrightarrow> f\<cdot>?z\<cdot>?x = f'\<cdot>?z\<cdot>?x

goal (1 subgoal):
 1. sfoldl\<cdot>f\<cdot>z\<cdot>xs = sfoldl\<cdot>f'\<cdot>z'\<cdot>xs'
[PROOF STEP]
by (induct xs arbitrary: xs' z z') auto


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

goal (1 subgoal):
 1. sfoldl\<cdot>f\<cdot>z\<cdot>(xs :@ ys) = sfoldl\<cdot>f\<cdot>(sfoldl\<cdot>f\<cdot>z\<cdot>xs)\<cdot>ys
[PROOF STEP]
by (cases "ys = \<bottom>", force) (induct xs arbitrary: z; simp)


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


[STATEMENT]
lemma sconcat_scons[simp]:
  shows "sconcat\<cdot>(x :# xs) = x :@ sconcat\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sconcat\<cdot>(x :# xs) = x :@ sconcat\<cdot>xs
[PROOF STEP]
by (cases "x = \<bottom>", force) (induct xs; fastforce)


[STATEMENT]
lemma sconcat_sfoldl_aux: "sfoldl\<cdot>sappend\<cdot>z\<cdot>xs = z :@ sconcat\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sfoldl\<cdot>sappend\<cdot>z\<cdot>xs = z :@ sconcat\<cdot>xs
[PROOF STEP]
by (induct xs arbitrary: z) simp_all


[STATEMENT]
lemma sconcat_sfoldl: "sconcat = sfoldl\<cdot>sappend\<cdot>[::]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sconcat = sfoldl\<cdot>sappend\<cdot>[::]
[PROOF STEP]
by (clarsimp simp: cfun_eq_iff sconcat_sfoldl_aux)


[STATEMENT]
lemma sconcat_sappend[simp]: "sconcat\<cdot>(xs :@ ys) = sconcat\<cdot>xs :@ sconcat\<cdot>ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sconcat\<cdot>(xs :@ ys) = sconcat\<cdot>xs :@ sconcat\<cdot>ys
[PROOF STEP]
by (induct xs) simp_all


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


[STATEMENT]
lemma slength_bottom_iff[simp]: "(slength\<cdot>xs = \<bottom>) \<longleftrightarrow> (xs = \<bottom>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (slength\<cdot>xs = \<bottom>) = (xs = \<bottom>)
[PROOF STEP]
by (induct xs) force+


[STATEMENT]
lemma slength_ge_0: "slength\<cdot>xs = MkI\<cdot>n \<Longrightarrow> n \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slength\<cdot>xs = MkI\<cdot>n \<Longrightarrow> 0 \<le> n
[PROOF STEP]
by (induct xs arbitrary: n) (simp add: one_Integer_def plus_eq_MkI_conv; force)+


[STATEMENT]
lemma slengthE:
  shows "\<lbrakk>xs \<noteq> \<bottom>; \<And>n. \<lbrakk>slength\<cdot>xs = MkI\<cdot>n; 0 \<le> n\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs \<noteq> \<bottom>; \<And>n. \<lbrakk>slength\<cdot>xs = MkI\<cdot>n; 0 \<le> n\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q
[PROOF STEP]
by (meson Integer.exhaust slength_bottom_iff slength_ge_0)


[STATEMENT]
lemma slength_0_conv[simp]:
  "(slength\<cdot>xs = 0) \<longleftrightarrow> (xs = [::])"
  "(slength\<cdot>xs = MkI\<cdot>0) \<longleftrightarrow> (xs = [::])"
  "eq\<cdot>0\<cdot>(slength\<cdot>xs) = snull\<cdot>xs"
  "eq\<cdot>(slength\<cdot>xs)\<cdot>0 = snull\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((slength\<cdot>xs = 0) = (xs = [::]) &&& (slength\<cdot>xs = MkI\<cdot>0) = (xs = [::])) &&& eq\<cdot>0\<cdot>(slength\<cdot>xs) = snull\<cdot>xs &&& eq\<cdot>(slength\<cdot>xs)\<cdot>0 = snull\<cdot>xs
[PROOF STEP]
by (induct xs) (auto simp: one_Integer_def elim: slengthE)


[STATEMENT]
lemma le_slength_0[simp]: "(le\<cdot>0\<cdot>(slength\<cdot>xs) = TT) \<longleftrightarrow> (xs \<noteq> \<bottom>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (le\<cdot>0\<cdot>(slength\<cdot>xs) = TT) = (xs \<noteq> \<bottom>)
[PROOF STEP]
by (cases "slength\<cdot>xs") (auto simp: slength_ge_0 zero_Integer_def)


[STATEMENT]
lemma lt_slength_0[simp]:
  "xs \<noteq> \<bottom> \<Longrightarrow> lt\<cdot>(slength\<cdot>xs)\<cdot>0 = FF"
  "xs \<noteq> \<bottom> \<Longrightarrow> lt\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>xs + 1) = TT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs \<noteq> \<bottom> \<Longrightarrow> lt\<cdot>(slength\<cdot>xs)\<cdot>0 = FF) &&& (xs \<noteq> \<bottom> \<Longrightarrow> lt\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>xs + 1) = TT)
[PROOF STEP]
unfolding zero_Integer_def one_Integer_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs \<noteq> \<bottom> \<Longrightarrow> lt\<cdot>(slength\<cdot>xs)\<cdot>(MkI\<cdot>0) = FF) &&& (xs \<noteq> \<bottom> \<Longrightarrow> lt\<cdot>(slength\<cdot>xs)\<cdot>(slength\<cdot>xs + MkI\<cdot>1) = TT)
[PROOF STEP]
by (auto elim: slengthE)


[STATEMENT]
lemma slength_smap[simp]:
  assumes "\<And>x. x \<noteq> \<bottom> \<Longrightarrow> f\<cdot>x \<noteq> \<bottom>"
  shows "slength\<cdot>(smap\<cdot>f\<cdot>xs) = slength\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slength\<cdot>(smap\<cdot>f\<cdot>xs) = slength\<cdot>xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?x \<noteq> \<bottom> \<Longrightarrow> f\<cdot>?x \<noteq> \<bottom>

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


[STATEMENT]
lemma slength_sappend[simp]: "slength\<cdot>(xs :@ ys) = slength\<cdot>xs + slength\<cdot>ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slength\<cdot>(xs :@ ys) = slength\<cdot>xs + slength\<cdot>ys
[PROOF STEP]
by (cases "ys = \<bottom>", force) (induct xs; force simp: ac_simps)


[STATEMENT]
lemma slength_sfoldl_aux: "sfoldl\<cdot>(\<Lambda> i _. i + 1)\<cdot>z\<cdot>xs = z + slength\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sfoldl\<cdot>(\<Lambda> i uu_. i + 1)\<cdot>z\<cdot>xs = z + slength\<cdot>xs
[PROOF STEP]
by (induct xs arbitrary: z) (simp_all add: ac_simps)


[STATEMENT]
lemma slength_sfoldl: "slength = sfoldl\<cdot>(\<Lambda> i _. i + 1)\<cdot>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slength = sfoldl\<cdot>(\<Lambda> i uu_. i + 1)\<cdot>0
[PROOF STEP]
by (clarsimp simp: cfun_eq_iff slength_sfoldl_aux)


[STATEMENT]
lemma le_slength_plus:
  assumes "xs \<noteq> \<bottom>"
  assumes "n \<noteq> \<bottom>"
  shows "le\<cdot>n\<cdot>(slength\<cdot>xs + n) = TT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le\<cdot>n\<cdot>(slength\<cdot>xs + n) = TT
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> \<bottom>
n \<noteq> \<bottom>

goal (1 subgoal):
 1. le\<cdot>n\<cdot>(slength\<cdot>xs + n) = TT
[PROOF STEP]
by (cases n; force elim: slengthE)


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


[STATEMENT]
lemma srev_bottom_iff[simp]: "(srev\<cdot>xs = \<bottom>) \<longleftrightarrow> (xs = \<bottom>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (srev\<cdot>xs = \<bottom>) = (xs = \<bottom>)
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma srev_scons[simp]: "srev\<cdot>(x :# xs) = srev\<cdot>xs :@ [:x:]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. srev\<cdot>(x :# xs) = srev\<cdot>xs :@ [:x:]
[PROOF STEP]
by (cases "x = \<bottom>", clarsimp) (induct xs; force)


[STATEMENT]
lemma srev_sappend[simp]: "srev\<cdot>(xs :@ ys) = srev\<cdot>ys :@ srev\<cdot>xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. srev\<cdot>(xs :@ ys) = srev\<cdot>ys :@ srev\<cdot>xs
[PROOF STEP]
by (induct xs) simp_all


[STATEMENT]
lemma srev_srev_ident[simp]: "srev\<cdot>(srev\<cdot>xs) = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. srev\<cdot>(srev\<cdot>xs) = xs
[PROOF STEP]
by (induct xs) auto


[STATEMENT]
lemma srev_cases[case_names bottom snil ssnoc]:
  assumes "xs = \<bottom> \<Longrightarrow> P"
  assumes "xs = [::] \<Longrightarrow> P"
  assumes "\<And>y ys. \<lbrakk>y \<noteq> \<bottom>; ys \<noteq> \<bottom>; xs = ys :@ [:y:]\<rbrakk> \<Longrightarrow> P"
  shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs = \<bottom> \<Longrightarrow> P
xs = [::] \<Longrightarrow> P
\<lbrakk>?y \<noteq> \<bottom>; ?ys \<noteq> \<bottom>; xs = ?ys :@ [:?y:]\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
by (metis slist.exhaust srev.simps(1) srev_scons srev_srev_ident srev_strict)