theory IsolatedThreadAction

lemma isolate_thread_actions_rewrite_bind:
  "\<lbrakk> inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s)
                  f (isolate_thread_actions idx f' f'' f''');
     \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s)
               (g x)
               (isolate_thread_actions idx (g' x) g'' g''');
     thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x);
     \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace> \<rbrakk>
    \<Longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s)
               (f >>= g) (isolate_thread_actions idx
                                  (f' >>= g') (g'' o f'') (g''' o f'''))" apply (rule monadic_rewrite_guard_imp) apply (rule monadic_rewrite_trans) apply (rule monadic_rewrite_bind, assumption+) apply (wp isolate_thread_actions_tcbs_at) apply simp apply (subst isolate_thread_actions_wrap_bind, assumption) apply (rule monadic_rewrite_in_isolate_thread_actions, assumption) apply (rule monadic_rewrite_transverse) apply (rule monadic_rewrite_bind_l) apply (erule(1) thread_actions_isolatableD) apply (rule thread_actions_isolatableD, assumption+) apply (rule hoare_vcg_all_lift, assumption) apply (simp add: liftM_def id_def) apply (rule monadic_rewrite_refl) apply (simp add: obj_at_partial_overwrite_If) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (f >>= g) (isolate_thread_actions idx (f' >>= g') (g'' \<circ> f'') (g''' \<circ> f''')) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite False True ?Q (f >>= g) (isolate_thread_actions idx (f' >>= g') (g'' \<circ> f'') (g''' \<circ> f'''))
 2. \<And>s. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite False True ?P3 (f >>= g) ?g3
 2. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite False True ?Q3 ?g3 (isolate_thread_actions idx (f' >>= g') (g'' \<circ> f'') (g''' \<circ> f'''))
 3. \<And>s. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> (?P3 and ?Q3) s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?R6\<rbrace> isolate_thread_actions idx f' f'' f''' \<lbrace>\<lambda>x s. \<forall>x. tcb_at' (idx x) s\<rbrace>
 2. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite False True ?Q3 (do x <- isolate_thread_actions idx f' f'' f''';
isolate_thread_actions idx (g' x) g'' g'''
od) (isolate_thread_actions idx (f' >>= g') (g'' \<circ> f'') (g''' \<circ> f'''))
 3. \<And>s. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>x. tcb_at' (idx x) s) and ?R6 and ?Q3) s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>
 2. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite False True ?Q3 (do x <- isolate_thread_actions idx f' f'' f''';
isolate_thread_actions idx (g' x) g'' g'''
od) (isolate_thread_actions idx (f' >>= g') (g'' \<circ> f'') (g''' \<circ> f'''))
 3. \<And>s. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>x. tcb_at' (idx x) s) and (\<lambda>s. \<forall>x. tcb_at' (idx x) s) and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite False True ?Q3 (do x <- isolate_thread_actions idx f' f'' f''';
isolate_thread_actions idx (g' x) g'' g'''
od) (isolate_thread_actions idx (f' >>= g') (g'' \<circ> f'') (g''' \<circ> f'''))
 2. \<And>s. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>x. tcb_at' (idx x) s) and (\<lambda>s. \<forall>x. tcb_at' (idx x) s) and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite False True ?Q3 (isolate_thread_actions idx (do x <- isolate_thread_actions idx f' id id;
isolate_thread_actions idx (g' x) id id
od) (g'' \<circ> f'') (g''' \<circ> f''')) (isolate_thread_actions idx (f' >>= g') (g'' \<circ> f'') (g''' \<circ> f'''))
 2. \<And>s. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>x. tcb_at' (idx x) s) and (\<lambda>s. \<forall>x. tcb_at' (idx x) s) and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite False True ?P18 (do x <- isolate_thread_actions idx f' id id;
isolate_thread_actions idx (g' x) id id
od) (f' >>= g')
 2. \<And>s. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>x. tcb_at' (idx x) s) and (\<lambda>s. \<forall>x. tcb_at' (idx x) s) and (\<lambda>s. ?P18 (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>))) s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite False True ?Q26 (f' >>= g') ?b26
 2. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite False True ?P26 (do x <- isolate_thread_actions idx f' id id;
isolate_thread_actions idx (g' x) id id
od) ?b26
 3. \<And>s. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>x. tcb_at' (idx x) s) and (\<lambda>s. \<forall>x. tcb_at' (idx x) s) and (\<lambda>s. (?P26 and ?Q26) (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>))) s proof (prove)
goal (5 subgoals):
 1. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite False True ?P29 f' ?g29
 2. \<And>x. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite False True (?Q29 x) (g' x) (?j29 x)
 3. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?R29\<rbrace> f' \<lbrace>?Q29\<rbrace>
 4. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite False True ?P26 (do x <- isolate_thread_actions idx f' id id;
isolate_thread_actions idx (g' x) id id
od) (?g29 >>= ?j29)
 5. \<And>s. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>x. tcb_at' (idx x) s) and (\<lambda>s. \<forall>x. tcb_at' (idx x) s) and (\<lambda>s. (?P26 and (?P29 and ?R29)) (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>))) s proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite False True (?Q29 x) (g' x) (?j29 x)
 2. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?R29\<rbrace> f' \<lbrace>?Q29\<rbrace>
 3. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite False True ?P26 (do x <- isolate_thread_actions idx f' id id;
isolate_thread_actions idx (g' x) id id
od) (isolate_thread_actions idx f' id id >>= ?j29)
 4. \<And>s. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>x. tcb_at' (idx x) s) and (\<lambda>s. \<forall>x. tcb_at' (idx x) s) and (\<lambda>s. (?P26 and ((\<lambda>s. \<forall>x. tcb_at' (idx x) s) and ?R29)) (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>))) s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?R29\<rbrace> f' \<lbrace>\<lambda>x s. \<forall>x. tcb_at' (idx x) s\<rbrace>
 2. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite False True ?P26 (do x <- isolate_thread_actions idx f' id id;
isolate_thread_actions idx (g' x) id id
od) (do x <- isolate_thread_actions idx f' id id;
isolate_thread_actions idx (g' x) id id
od)
 3. \<And>s. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>x. tcb_at' (idx x) s) and (\<lambda>s. \<forall>x. tcb_at' (idx x) s) and (\<lambda>s. (?P26 and ((\<lambda>s. \<forall>x. tcb_at' (idx x) s) and ?R29)) (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>))) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite False True ?P26 (do x <- isolate_thread_actions idx f' id id;
isolate_thread_actions idx (g' x) id id
od) (do x <- isolate_thread_actions idx f' id id;
isolate_thread_actions idx (g' x) id id
od)
 2. \<And>s. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>x. tcb_at' (idx x) s) and (\<lambda>s. \<forall>x. tcb_at' (idx x) s) and (\<lambda>s. (?P26 and ((\<lambda>s. \<forall>x. tcb_at' (idx x) s) and (\<lambda>s. \<forall>x. tcb_at' (idx x) s))) (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>))) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>\<rbrakk> \<Longrightarrow> monadic_rewrite False True ?P26 (do x <- isolate_thread_actions idx f' (\<lambda>a. a) (\<lambda>a. a);
isolate_thread_actions idx (g' x) (\<lambda>a. a) (\<lambda>a. a)
od) (do x <- isolate_thread_actions idx f' (\<lambda>x. x) (\<lambda>x. x);
isolate_thread_actions idx (g' x) (\<lambda>x. x) (\<lambda>x. x)
od)
 2. \<And>s. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>x. tcb_at' (idx x) s) and (\<lambda>s. \<forall>x. tcb_at' (idx x) s) and (\<lambda>s. (?P26 and ((\<lambda>s. \<forall>x. tcb_at' (idx x) s) and (\<lambda>s. \<forall>x. tcb_at' (idx x) s))) (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>inj idx; monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) f (isolate_thread_actions idx f' f'' f'''); \<And>x. monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (g x) (isolate_thread_actions idx (g' x) g'' g'''); thread_actions_isolatable idx f'; \<And>x. thread_actions_isolatable idx (g' x); \<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f' \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>x. tcb_at' (idx x) s) and (\<lambda>s. \<forall>x. tcb_at' (idx x) s) and (\<lambda>s. ((\<lambda>_. True) and ((\<lambda>s. \<forall>x. tcb_at' (idx x) s) and (\<lambda>s. \<forall>x. tcb_at' (idx x) s))) (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>))) s proof (prove)
goal:
No subgoals!