theory IpcCancel_AI

lemma cancel_all_helper:
  " \<lbrace>valid_objs and
    (\<lambda>s. \<forall>t \<in> set queue. st_tcb_at (\<lambda>st. \<not> halted st) t s) \<rbrace>
     mapM_x (\<lambda>t. do y \<leftarrow> set_thread_state t Structures_A.Restart;
                    do_extended_op (tcb_sched_enqueue_ext t) od) queue
   \<lbrace>\<lambda>rv. valid_objs\<rbrace>" apply (rule hoare_strengthen_post) apply (rule mapM_x_wp [where S="set queue", simplified]) apply (wp, simp, wp hoare_vcg_const_Ball_lift sts_st_tcb_at_cases, simp) apply (clarsimp elim: pred_tcb_weakenE) apply (erule(1) my_BallE) apply (clarsimp simp: st_tcb_def2) apply (frule(1) valid_tcb_objs) apply (clarsimp simp: valid_tcb_def valid_tcb_state_def
                          cte_wp_at_cases tcb_cap_cases_def
                   dest!: get_tcb_SomeD) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and (\<lambda>s. \<forall>t\<in>set queue. st_tcb_at (\<lambda>st. \<not> halted st) t s)\<rbrace> mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
do_extended_op (tcb_sched_enqueue_ext t)
od) queue \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>valid_objs and (\<lambda>s. \<forall>t\<in>set queue. st_tcb_at (\<lambda>st. \<not> halted st) t s)\<rbrace> mapM_x (\<lambda>t. do y <- set_thread_state t Restart;
do_extended_op (tcb_sched_enqueue_ext t)
od) queue \<lbrace>?Q\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> valid_objs s proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> set queue \<Longrightarrow> \<lbrace>valid_objs and (\<lambda>s. \<forall>t\<in>set queue. st_tcb_at (\<lambda>st. \<not> halted st) t s)\<rbrace> do y <- set_thread_state x Restart;
do_extended_op (tcb_sched_enqueue_ext x)
od \<lbrace>\<lambda>rv. valid_objs and (\<lambda>s. \<forall>t\<in>set queue. st_tcb_at (\<lambda>st. \<not> halted st) t s)\<rbrace>
 2. set queue \<subseteq> set queue
 3. \<And>rv s. (valid_objs and (\<lambda>s. \<forall>t\<in>set queue. st_tcb_at (\<lambda>st. \<not> halted st) t s)) s \<Longrightarrow> valid_objs s proof (prove)
goal (3 subgoals):
 1. \<And>x s. \<lbrakk>x \<in> set queue; valid_objs s \<and> (\<forall>t\<in>set queue. st_tcb_at (\<lambda>st. \<not> halted st) t s)\<rbrakk> \<Longrightarrow> valid_tcb_state Restart s
 2. set queue \<subseteq> set queue
 3. \<And>rv s. (valid_objs and (\<lambda>s. \<forall>t\<in>set queue. st_tcb_at (\<lambda>st. \<not> halted st) t s)) s \<Longrightarrow> valid_objs s proof (prove)
goal (3 subgoals):
 1. \<And>x s. \<lbrakk>x \<in> set queue; valid_objs s; \<forall>t\<in>set queue. st_tcb_at (\<lambda>st. \<not> halted st) t s\<rbrakk> \<Longrightarrow> valid_tcb_state Restart s
 2. set queue \<subseteq> set queue
 3. \<And>rv s. (valid_objs and (\<lambda>s. \<forall>t\<in>set queue. st_tcb_at (\<lambda>st. \<not> halted st) t s)) s \<Longrightarrow> valid_objs s proof (prove)
goal (3 subgoals):
 1. \<And>x s. \<lbrakk>x \<in> set queue; valid_objs s; st_tcb_at (\<lambda>st. \<not> halted st) x s\<rbrakk> \<Longrightarrow> valid_tcb_state Restart s
 2. set queue \<subseteq> set queue
 3. \<And>rv s. (valid_objs and (\<lambda>s. \<forall>t\<in>set queue. st_tcb_at (\<lambda>st. \<not> halted st) t s)) s \<Longrightarrow> valid_objs s proof (prove)
goal (3 subgoals):
 1. \<And>x s tcb. \<lbrakk>x \<in> set queue; valid_objs s; get_tcb x s = Some tcb; \<not> halted (tcb_state tcb)\<rbrakk> \<Longrightarrow> valid_tcb_state Restart s
 2. set queue \<subseteq> set queue
 3. \<And>rv s. (valid_objs and (\<lambda>s. \<forall>t\<in>set queue. st_tcb_at (\<lambda>st. \<not> halted st) t s)) s \<Longrightarrow> valid_objs s proof (prove)
goal (3 subgoals):
 1. \<And>x s tcb. \<lbrakk>x \<in> set queue; valid_objs s; get_tcb x s = Some tcb; \<not> halted (tcb_state tcb); valid_tcb x tcb s\<rbrakk> \<Longrightarrow> valid_tcb_state Restart s
 2. set queue \<subseteq> set queue
 3. \<And>rv s. (valid_objs and (\<lambda>s. \<forall>t\<in>set queue. st_tcb_at (\<lambda>st. \<not> halted st) t s)) s \<Longrightarrow> valid_objs s proof (prove)
goal (2 subgoals):
 1. set queue \<subseteq> set queue
 2. \<And>rv s. (valid_objs and (\<lambda>s. \<forall>t\<in>set queue. st_tcb_at (\<lambda>st. \<not> halted st) t s)) s \<Longrightarrow> valid_objs s proof (prove)
goal:
No subgoals!