theory Move_C

lemma thread_submonad_args:
  "\<lbrakk> \<And>f v. ext (upd f v) = f (ext v);
     \<And>f1 f2 v. upd f1 (upd f2 v) = upd (f1 \<circ> f2) v;
     \<And>f v. upd (\<lambda>_. ext v) v = v \<rbrakk> \<Longrightarrow>
   submonad_args (thread_fetch ext t) (thread_replace upd t) (tcb_at' t)" apply unfold_locales apply (clarsimp simp: thread_fetch_def thread_replace_def
                           Let_def obj_at'_def projectKOs
                    split: kernel_object.split option.split) apply (clarsimp simp: thread_replace_def Let_def
                   split: kernel_object.split option.split) apply (clarsimp simp: thread_fetch_def thread_replace_def Let_def
                         fun_upd_idem
                  split: kernel_object.splits option.splits) apply (clarsimp simp: obj_at'_def thread_replace_def Let_def projectKOs
                 split: kernel_object.splits option.splits) apply (rename_tac tcb) apply (case_tac tcb, simp add: objBitsKO_def ps_clear_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>f v. ext (upd f v) = f (ext v); \<And>f1 f2 v. upd f1 (upd f2 v) = upd (f1 \<circ> f2) v; \<And>f v. upd (\<lambda>_. ext v) v = v\<rbrakk> \<Longrightarrow> submonad_args (thread_fetch ext t) (thread_replace upd t) (tcb_at' t) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<And>f v. ext (upd f v) = f (ext v); \<And>f1 f2 v. upd f1 (upd f2 v) = upd (f1 \<circ> f2) v; \<And>f v. upd (\<lambda>_. ext v) v = v\<rbrakk> \<Longrightarrow> \<forall>x s. tcb_at' t s \<longrightarrow> thread_fetch ext t (thread_replace upd t x s) = x
 2. \<lbrakk>\<And>f v. ext (upd f v) = f (ext v); \<And>f1 f2 v. upd f1 (upd f2 v) = upd (f1 \<circ> f2) v; \<And>f v. upd (\<lambda>_. ext v) v = v\<rbrakk> \<Longrightarrow> \<forall>x y s. thread_replace upd t x (thread_replace upd t y s) = thread_replace upd t x s
 3. \<lbrakk>\<And>f v. ext (upd f v) = f (ext v); \<And>f1 f2 v. upd f1 (upd f2 v) = upd (f1 \<circ> f2) v; \<And>f v. upd (\<lambda>_. ext v) v = v\<rbrakk> \<Longrightarrow> \<forall>s. thread_replace upd t (thread_fetch ext t s) s = s
 4. \<And>s x. \<lbrakk>\<And>f v. ext (upd f v) = f (ext v); \<And>f1 f2 v. upd f1 (upd f2 v) = upd (f1 \<circ> f2) v; \<And>f v. upd (\<lambda>_. ext v) v = v\<rbrakk> \<Longrightarrow> tcb_at' t (thread_replace upd t x s) = tcb_at' t s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>f v. ext (upd f v) = f (ext v); \<And>f1 f2 v. upd f1 (upd f2 v) = upd (f1 \<circ> f2) v; \<And>f v. upd (\<lambda>_. ext v) v = v\<rbrakk> \<Longrightarrow> \<forall>x y s. thread_replace upd t x (thread_replace upd t y s) = thread_replace upd t x s
 2. \<lbrakk>\<And>f v. ext (upd f v) = f (ext v); \<And>f1 f2 v. upd f1 (upd f2 v) = upd (f1 \<circ> f2) v; \<And>f v. upd (\<lambda>_. ext v) v = v\<rbrakk> \<Longrightarrow> \<forall>s. thread_replace upd t (thread_fetch ext t s) s = s
 3. \<And>s x. \<lbrakk>\<And>f v. ext (upd f v) = f (ext v); \<And>f1 f2 v. upd f1 (upd f2 v) = upd (f1 \<circ> f2) v; \<And>f v. upd (\<lambda>_. ext v) v = v\<rbrakk> \<Longrightarrow> tcb_at' t (thread_replace upd t x s) = tcb_at' t s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>f v. ext (upd f v) = f (ext v); \<And>f1 f2 v. upd f1 (upd f2 v) = upd (f1 \<circ> f2) v; \<And>f v. upd (\<lambda>_. ext v) v = v\<rbrakk> \<Longrightarrow> \<forall>s. thread_replace upd t (thread_fetch ext t s) s = s
 2. \<And>s x. \<lbrakk>\<And>f v. ext (upd f v) = f (ext v); \<And>f1 f2 v. upd f1 (upd f2 v) = upd (f1 \<circ> f2) v; \<And>f v. upd (\<lambda>_. ext v) v = v\<rbrakk> \<Longrightarrow> tcb_at' t (thread_replace upd t x s) = tcb_at' t s proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>\<And>f v. ext (upd f v) = f (ext v); \<And>f1 f2 v. upd f1 (upd f2 v) = upd (f1 \<circ> f2) v; \<And>f v. upd (\<lambda>_. ext v) v = v\<rbrakk> \<Longrightarrow> tcb_at' t (thread_replace upd t x s) = tcb_at' t s proof (prove)
goal (1 subgoal):
 1. \<And>s x x6. \<lbrakk>\<And>f v. ext (upd f v) = f (ext v); \<And>f1 f2 v. upd f1 (upd f2 v) = upd (f1 \<circ> f2) v; \<And>v. upd (\<lambda>_. ext v) v = v; ksPSpace s t = Some (KOTCB x6)\<rbrakk> \<Longrightarrow> (is_aligned t (objBitsKO (KOTCB (upd (\<lambda>_. x) x6))) \<and> ps_clear t (objBitsKO (KOTCB (upd (\<lambda>_. x) x6))) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (upd (\<lambda>_. x) x6))\<rparr>)) = (is_aligned t (objBitsKO (KOTCB x6)) \<and> ps_clear t (objBitsKO (KOTCB x6)) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x tcb. \<lbrakk>\<And>f v. ext (upd f v) = f (ext v); \<And>f1 f2 v. upd f1 (upd f2 v) = upd (f1 \<circ> f2) v; \<And>v. upd (\<lambda>_. ext v) v = v; ksPSpace s t = Some (KOTCB tcb)\<rbrakk> \<Longrightarrow> (is_aligned t (objBitsKO (KOTCB (upd (\<lambda>_. x) tcb))) \<and> ps_clear t (objBitsKO (KOTCB (upd (\<lambda>_. x) tcb))) (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (upd (\<lambda>_. x) tcb))\<rparr>)) = (is_aligned t (objBitsKO (KOTCB tcb)) \<and> ps_clear t (objBitsKO (KOTCB tcb)) s) proof (prove)
goal:
No subgoals!