kings-crown/FVELER_Isabelle huggingface dataset:
theory DetSchedSchedule_AI

lemma set_bound_notification_valid_etcbs[wp]:
  "\<lbrace>valid_etcbs\<rbrace> set_bound_notification ref ntfn \<lbrace>\<lambda>_. valid_etcbs\<rbrace>" apply (simp add: set_bound_notification_def) apply (wp | wpc | simp add: set_object_def get_object_def)+ apply (fastforce simp: valid_etcbs_def st_tcb_at_kh_if_split
                   dest: get_tcb_st_tcb_at) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> set_bound_notification ref ntfn \<lbrace>\<lambda>_. valid_etcbs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
od \<lbrace>\<lambda>_. valid_etcbs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_etcbs s \<Longrightarrow> (\<exists>y. get_tcb ref s = Some y) \<longrightarrow> (\<exists>y. kheap s ref = Some y) \<longrightarrow> a_type (the (kheap s ref)) = ATCB \<longrightarrow> valid_etcbs_2 (ekheap s) (\<lambda>a. if a = ref then Some (TCB (the (get_tcb ref s)\<lparr>tcb_bound_notification := ntfn\<rparr>)) else kheap s a) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_thread_state_runnable_valid_queues:
  "\<lbrace>valid_queues and K (runnable ts)\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. valid_queues\<rbrace>" apply (simp add: set_thread_state_def) apply (wp | wpc | simp add: set_thread_state_ext_def set_object_def get_object_def)+ apply (clarsimp simp: valid_queues_def st_tcb_at_kh_if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues and K (runnable ts)\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues and (\<lambda>y. runnable ts)\<rbrace> do tcb <- gets_the (get_tcb ref);
y <- set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>));
set_thread_state_ext ref
od \<lbrace>\<lambda>_. valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_queues s \<and> runnable ts \<Longrightarrow> (\<exists>y. get_tcb ref s = Some y) \<longrightarrow> (\<exists>y. kheap s ref = Some y) \<longrightarrow> a_type (the (kheap s ref)) = ATCB \<longrightarrow> valid_queues_2 (ready_queues s) (ekheap s) (\<lambda>a. if a = ref then Some (TCB (the (get_tcb ref s)\<lparr>tcb_state := ts\<rparr>)) else kheap s a) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_bound_notification_valid_queues:
  "\<lbrace>valid_queues\<rbrace> set_bound_notification ref ntfn \<lbrace>\<lambda>_. valid_queues\<rbrace>" apply (simp add: set_bound_notification_def) apply (wpsimp wp: set_object_wp) apply (clarsimp simp: valid_queues_def st_tcb_at_kh_if_split) apply (drule_tac x=d in spec) apply (drule_tac x=p in spec) apply clarsimp apply (drule (1) bspec, clarsimp simp: st_tcb_def2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues\<rbrace> set_bound_notification ref ntfn \<lbrace>\<lambda>_. valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues\<rbrace> do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
od \<lbrace>\<lambda>_. valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>valid_queues s; get_tcb ref s = Some y\<rbrakk> \<Longrightarrow> valid_queues_2 (ready_queues s) (ekheap s) (\<lambda>a. if a = ref then Some (TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>)) else kheap s a) proof (prove)
goal (1 subgoal):
 1. \<And>s y d p. \<lbrakk>\<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s \<and> st_tcb_at runnable t s) \<and> distinct (ready_queues s d p); get_tcb ref s = Some y; ref \<in> set (ready_queues s d p)\<rbrakk> \<Longrightarrow> runnable (tcb_state y) proof (prove)
goal (1 subgoal):
 1. \<And>s y d p. \<lbrakk>get_tcb ref s = Some y; ref \<in> set (ready_queues s d p); \<forall>p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s \<and> st_tcb_at runnable t s) \<and> distinct (ready_queues s d p)\<rbrakk> \<Longrightarrow> runnable (tcb_state y) proof (prove)
goal (1 subgoal):
 1. \<And>s y d p. \<lbrakk>get_tcb ref s = Some y; ref \<in> set (ready_queues s d p); (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s \<and> st_tcb_at runnable t s) \<and> distinct (ready_queues s d p)\<rbrakk> \<Longrightarrow> runnable (tcb_state y) proof (prove)
goal (1 subgoal):
 1. \<And>s y d p. \<lbrakk>get_tcb ref s = Some y; ref \<in> set (ready_queues s d p); \<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s \<and> st_tcb_at runnable t s; distinct (ready_queues s d p)\<rbrakk> \<Longrightarrow> runnable (tcb_state y) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_thread_state_ct_not_in_q[wp]:
  "\<lbrace>ct_not_in_q\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. ct_not_in_q\<rbrace>" apply (simp add: set_thread_state_def) apply (simp add: set_thread_state_ext_def set_object_def get_object_def | wp gts_wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_in_q\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. ct_not_in_q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_in_q\<rbrace> do tcb <- gets_the (get_tcb ref);
y <- set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>));
set_thread_state_ext ref
od \<lbrace>\<lambda>_. ct_not_in_q\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_bound_notification_ct_not_in_q[wp]:
  "\<lbrace>ct_not_in_q\<rbrace> set_bound_notification ref ntfn \<lbrace>\<lambda>_. ct_not_in_q\<rbrace>" apply (simp add: set_bound_notification_def) apply (simp add: set_object_def get_object_def | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_in_q\<rbrace> set_bound_notification ref ntfn \<lbrace>\<lambda>_. ct_not_in_q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_in_q\<rbrace> do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
od \<lbrace>\<lambda>_. ct_not_in_q\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_thread_state_cur_is_activatable[wp]:
  "\<lbrace>\<lambda>s. is_activatable (cur_thread s) s\<rbrace>
     set_thread_state ref ts
   \<lbrace>\<lambda>_ (s::det_state). is_activatable (cur_thread s) s\<rbrace>" apply (simp add: set_thread_state_def) apply (simp add: set_thread_state_ext_def set_object_def get_object_def |
         wp set_scheduler_action_wp gts_wp)+ apply (clarsimp simp: is_activatable_def st_tcb_at_kh_if_split
                        pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_activatable (cur_thread s) s\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_ s. is_activatable (cur_thread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_activatable (cur_thread s) s\<rbrace> do tcb <- gets_the (get_tcb ref);
y <- set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>));
set_thread_state_ext ref
od \<lbrace>\<lambda>_ s. is_activatable (cur_thread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. is_activatable (cur_thread s) s \<Longrightarrow> (\<exists>y. get_tcb ref s = Some y) \<longrightarrow> (\<exists>y. kheap s ref = Some y) \<longrightarrow> a_type (the (kheap s ref)) = ATCB \<longrightarrow> (\<forall>st. (cur_thread s = ref \<longrightarrow> runnable st \<or> scheduler_action s \<noteq> resume_cur_thread) \<longrightarrow> st_tcb_at ((=) st) ref (s\<lparr>kheap := \<lambda>a. if a = ref then Some (TCB (the (get_tcb ref s)\<lparr>tcb_state := ts\<rparr>)) else kheap s a\<rparr>) \<longrightarrow> is_activatable_2 (cur_thread s) (scheduler_action s) (\<lambda>a. if a = ref then Some (TCB (the (get_tcb ref s)\<lparr>tcb_state := ts\<rparr>)) else kheap s a)) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_bound_notification_cur_is_activatable[wp]:
  "\<lbrace>\<lambda>s. is_activatable (cur_thread s) s\<rbrace>
     set_bound_notification ref ntfn
   \<lbrace>\<lambda>_ (s::det_state). is_activatable (cur_thread s) s\<rbrace>" apply (simp add: set_bound_notification_def) apply (simp add: set_object_def get_object_def | wp set_scheduler_action_wp)+ apply (clarsimp simp: is_activatable_def st_tcb_at_kh_if_split pred_tcb_at_def
                        obj_at_def get_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_activatable (cur_thread s) s\<rbrace> set_bound_notification ref ntfn \<lbrace>\<lambda>_ s. is_activatable (cur_thread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_activatable (cur_thread s) s\<rbrace> do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
od \<lbrace>\<lambda>_ s. is_activatable (cur_thread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. is_activatable (cur_thread s) s \<Longrightarrow> (\<exists>y. get_tcb ref s = Some y) \<longrightarrow> (\<exists>y. kheap s ref = Some y) \<longrightarrow> a_type (the (kheap s ref)) = ATCB \<longrightarrow> is_activatable_2 (cur_thread s) (scheduler_action s) (\<lambda>a. if a = ref then Some (TCB (the (get_tcb ref s)\<lparr>tcb_bound_notification := ntfn\<rparr>)) else kheap s a) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_thread_state_runnable_weak_valid_sched_action:
  "\<lbrace>weak_valid_sched_action and (\<lambda>s. runnable ts)\<rbrace>
      set_thread_state ref ts
   \<lbrace>\<lambda>_. weak_valid_sched_action\<rbrace>" apply (simp add: set_thread_state_def) apply (simp add: set_thread_state_ext_def set_object_def get_object_def | wp gts_wp)+ apply (clarsimp simp: weak_valid_sched_action_def st_tcb_at_kh_if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>weak_valid_sched_action and (\<lambda>s. runnable ts)\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. weak_valid_sched_action\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>weak_valid_sched_action and (\<lambda>s. runnable ts)\<rbrace> do tcb <- gets_the (get_tcb ref);
y <- set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>));
set_thread_state_ext ref
od \<lbrace>\<lambda>_. weak_valid_sched_action\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. weak_valid_sched_action s \<and> runnable ts \<Longrightarrow> (\<exists>y. get_tcb ref s = Some y) \<longrightarrow> (\<exists>y. kheap s ref = Some y) \<longrightarrow> a_type (the (kheap s ref)) = ATCB \<longrightarrow> (\<forall>st. (cur_thread s = ref \<longrightarrow> runnable st \<or> scheduler_action s \<noteq> resume_cur_thread) \<longrightarrow> st_tcb_at ((=) st) ref (s\<lparr>kheap := \<lambda>a. if a = ref then Some (TCB (the (get_tcb ref s)\<lparr>tcb_state := ts\<rparr>)) else kheap s a\<rparr>) \<longrightarrow> weak_valid_sched_action_2 (scheduler_action s) (ekheap s) (\<lambda>a. if a = ref then Some (TCB (the (get_tcb ref s)\<lparr>tcb_state := ts\<rparr>)) else kheap s a)) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_thread_state_switch_in_cur_domain[wp]:
  "\<lbrace>switch_in_cur_domain\<rbrace>
      set_thread_state ref ts \<lbrace>\<lambda>_. switch_in_cur_domain\<rbrace>" apply (simp add: set_thread_state_def) apply (simp add: set_thread_state_ext_def set_object_def get_object_def
                   | wp set_scheduler_action_wp gts_wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>switch_in_cur_domain\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. switch_in_cur_domain\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>switch_in_cur_domain\<rbrace> do tcb <- gets_the (get_tcb ref);
y <- set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>));
set_thread_state_ext ref
od \<lbrace>\<lambda>_. switch_in_cur_domain\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_bound_notification_switch_in_cur_domain[wp]:
  "\<lbrace>switch_in_cur_domain\<rbrace>
      set_bound_notification ref ts \<lbrace>\<lambda>_. switch_in_cur_domain\<rbrace>" apply (simp add: set_bound_notification_def) apply (simp add: set_object_def get_object_def | wp set_scheduler_action_wp gbn_wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>switch_in_cur_domain\<rbrace> set_bound_notification ref ts \<lbrace>\<lambda>_. switch_in_cur_domain\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>switch_in_cur_domain\<rbrace> do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_bound_notification := ts\<rparr>))
od \<lbrace>\<lambda>_. switch_in_cur_domain\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_bound_notification_weak_valid_sched_action:
  "\<lbrace>weak_valid_sched_action\<rbrace>
      set_bound_notification ref ntfnptr
   \<lbrace>\<lambda>_. weak_valid_sched_action\<rbrace>" apply (simp add: set_bound_notification_def) apply (simp add: set_object_def get_object_def | wp)+ apply (clarsimp simp: weak_valid_sched_action_def st_tcb_at_kh_if_split
                        st_tcb_def2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>weak_valid_sched_action\<rbrace> set_bound_notification ref ntfnptr \<lbrace>\<lambda>_. weak_valid_sched_action\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>weak_valid_sched_action\<rbrace> do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_bound_notification := ntfnptr\<rparr>))
od \<lbrace>\<lambda>_. weak_valid_sched_action\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. weak_valid_sched_action s \<Longrightarrow> (\<exists>y. get_tcb ref s = Some y) \<longrightarrow> (\<exists>y. kheap s ref = Some y) \<longrightarrow> a_type (the (kheap s ref)) = ATCB \<longrightarrow> weak_valid_sched_action_2 (scheduler_action s) (ekheap s) (\<lambda>a. if a = ref then Some (TCB (the (get_tcb ref s)\<lparr>tcb_bound_notification := ntfnptr\<rparr>)) else kheap s a) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_thread_state_runnable_valid_sched_action:
  "\<lbrace>valid_sched_action and (\<lambda>s. runnable ts)\<rbrace>
      set_thread_state ref ts
   \<lbrace>\<lambda>_. valid_sched_action\<rbrace>" apply (simp add: valid_sched_action_def
        | wp set_thread_state_runnable_weak_valid_sched_action)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched_action and (\<lambda>s. runnable ts)\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. valid_sched_action\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_thread_state_cur_ct_in_cur_domain[wp]:
  "\<lbrace>ct_in_cur_domain\<rbrace>
     set_thread_state ref ts \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace>" apply (simp add: set_thread_state_def) apply (simp add: set_thread_state_ext_def set_object_def get_object_def |
        wp set_scheduler_action_wp gts_wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_cur_domain\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_cur_domain\<rbrace> do tcb <- gets_the (get_tcb ref);
y <- set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>));
set_thread_state_ext ref
od \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_bound_notification_cur_ct_in_cur_domain[wp]:
  "\<lbrace>ct_in_cur_domain\<rbrace>
     set_bound_notification ref ts \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace>" apply (simp add: set_bound_notification_def) apply (simp add: set_object_def get_object_def |
        wp set_scheduler_action_wp gbn_wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_cur_domain\<rbrace> set_bound_notification ref ts \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_cur_domain\<rbrace> do tcb <- gets_the (get_tcb ref);
set_object ref (TCB (tcb\<lparr>tcb_bound_notification := ts\<rparr>))
od \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_thread_state_runnable_valid_sched_except_blocked:
  "\<lbrace>valid_sched and (\<lambda>s. runnable ts)\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. valid_sched_except_blocked\<rbrace>" apply (simp add: valid_sched_def | wp set_thread_state_runnable_valid_queues
                                        set_thread_state_runnable_valid_sched_action)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and (\<lambda>s. runnable ts)\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. valid_sched_except_blocked\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_bound_notification_valid_sched_action:
  "\<lbrace>valid_sched_action\<rbrace> set_bound_notification ref ntfn \<lbrace>\<lambda>_. valid_sched_action\<rbrace>" apply (simp add: valid_sched_action_def |
         wp set_bound_notification_weak_valid_sched_action)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched_action\<rbrace> set_bound_notification ref ntfn \<lbrace>\<lambda>_. valid_sched_action\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_bound_notification_valid_sched:
  "\<lbrace>valid_sched\<rbrace> set_bound_notification ref ntfn \<lbrace>\<lambda>_. valid_sched\<rbrace>" apply (simp add: valid_sched_def | wp set_bound_notification_valid_queues
                                        set_bound_notification_valid_sched_action)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> set_bound_notification ref ntfn \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma valid_blocked_valid_blocked_except[simp]:
  "valid_blocked s \<Longrightarrow> valid_blocked_except t s" by (simp add: valid_blocked_def valid_blocked_except_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_blocked s \<Longrightarrow> valid_blocked_except t s
theory DetSchedSchedule_AI

lemma as_user_valid_etcbs[wp]: "\<lbrace>valid_etcbs\<rbrace> as_user ptr s \<lbrace>\<lambda>_. valid_etcbs\<rbrace>" apply (simp add: as_user_def set_object_def get_object_def | wpc | wp)+ by (fastforce simp: valid_etcbs_def st_tcb_at_kh_if_split dest: get_tcb_st_tcb_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> as_user ptr s \<lbrace>\<lambda>_. valid_etcbs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. valid_etcbs sa \<Longrightarrow> (\<exists>y. get_tcb ptr sa = Some y) \<longrightarrow> (\<forall>x\<in>fst (s (arch_tcb_context_get (tcb_arch (the (get_tcb ptr sa))))). \<forall>xa xb. x = (xa, xb) \<longrightarrow> (\<exists>y. kheap sa ptr = Some y) \<longrightarrow> a_type (the (kheap sa ptr)) = ATCB \<longrightarrow> valid_etcbs_2 (ekheap sa) (\<lambda>a. if a = ptr then Some (TCB (the (get_tcb ptr sa)\<lparr>tcb_arch := arch_tcb_context_set xb (tcb_arch (the (get_tcb ptr sa)))\<rparr>)) else kheap sa a))
theory DetSchedSchedule_AI

lemma as_user_weak_valid_sched_action[wp]: "\<lbrace>weak_valid_sched_action\<rbrace> as_user ptr s \<lbrace>\<lambda>_. weak_valid_sched_action\<rbrace>" apply (simp add: as_user_def set_object_def get_object_def | wpc | wp)+ apply (clarsimp simp: weak_valid_sched_action_def st_tcb_at_kh_if_split st_tcb_at_def obj_at_def) by (drule get_tcb_SomeD, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>weak_valid_sched_action\<rbrace> as_user ptr s \<lbrace>\<lambda>_. weak_valid_sched_action\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. weak_valid_sched_action sa \<Longrightarrow> (\<exists>y. get_tcb ptr sa = Some y) \<longrightarrow> (\<forall>x\<in>fst (s (arch_tcb_context_get (tcb_arch (the (get_tcb ptr sa))))). \<forall>xa xb. x = (xa, xb) \<longrightarrow> (\<exists>y. kheap sa ptr = Some y) \<longrightarrow> a_type (the (kheap sa ptr)) = ATCB \<longrightarrow> weak_valid_sched_action_2 (scheduler_action sa) (ekheap sa) (\<lambda>a. if a = ptr then Some (TCB (the (get_tcb ptr sa)\<lparr>tcb_arch := arch_tcb_context_set xb (tcb_arch (the (get_tcb ptr sa)))\<rparr>)) else kheap sa a)) proof (prove)
goal (1 subgoal):
 1. \<And>sa y a b tcb. \<lbrakk>runnable (tcb_state tcb); get_tcb ptr sa = Some y; (a, b) \<in> fst (s (arch_tcb_context_get (tcb_arch y))); kheap sa ptr = Some (TCB tcb); scheduler_action sa = switch_thread ptr\<rbrakk> \<Longrightarrow> runnable (tcb_state y)
theory DetSchedSchedule_AI

lemma as_user_is_activatable[wp]: "\<lbrace>is_activatable t\<rbrace> as_user ptr s \<lbrace>\<lambda>_. is_activatable t\<rbrace>" apply (simp add: as_user_def set_object_def get_object_def | wpc | wp)+ apply (clarsimp simp: is_activatable_def st_tcb_at_kh_if_split st_tcb_at_def obj_at_def) by (drule get_tcb_SomeD, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>is_activatable t\<rbrace> as_user ptr s \<lbrace>\<lambda>_. is_activatable t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. is_activatable t sa \<Longrightarrow> (\<exists>y. get_tcb ptr sa = Some y) \<longrightarrow> (\<forall>x\<in>fst (s (arch_tcb_context_get (tcb_arch (the (get_tcb ptr sa))))). \<forall>xa xb. x = (xa, xb) \<longrightarrow> (\<exists>y. kheap sa ptr = Some y) \<longrightarrow> a_type (the (kheap sa ptr)) = ATCB \<longrightarrow> is_activatable_2 t (scheduler_action sa) (\<lambda>a. if a = ptr then Some (TCB (the (get_tcb ptr sa)\<lparr>tcb_arch := arch_tcb_context_set xb (tcb_arch (the (get_tcb ptr sa)))\<rparr>)) else kheap sa a)) proof (prove)
goal (1 subgoal):
 1. \<And>sa y a b tcb. \<lbrakk>t = ptr; get_tcb ptr sa = Some y; (a, b) \<in> fst (s (arch_tcb_context_get (tcb_arch y))); scheduler_action sa = resume_cur_thread; tcb_state y \<noteq> IdleThreadState; kheap sa ptr = Some (TCB tcb); activatable (tcb_state tcb)\<rbrakk> \<Longrightarrow> runnable (tcb_state y)
theory DetSchedSchedule_AI

lemma as_user_valid_idle_etcb[wp]: "\<lbrace>valid_idle_etcb\<rbrace> as_user ptr s \<lbrace>\<lambda>_. valid_idle_etcb\<rbrace>" by (simp add: as_user_def set_object_def get_object_def | wpc | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle_etcb\<rbrace> as_user ptr s \<lbrace>\<lambda>_. valid_idle_etcb\<rbrace>