kings-crown/FVELER_Isabelle huggingface dataset:
theory DetSchedSchedule_AI

lemma unbind_notification_valid_sched[wp]:
  "\<lbrace>valid_sched\<rbrace> unbind_notification ntfnptr \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (simp add: unbind_notification_def) apply (rule hoare_seq_ext[OF _ gbn_sp]) apply (case_tac ntfnptra, simp, wp, simp) apply (clarsimp) apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) apply (wp set_bound_notification_valid_sched, clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> unbind_notification ntfnptr \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> do ntfnptra <- get_bound_notification ntfnptr;
case ntfnptra of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
y <- set_notification ntfnptr' (ntfn_set_bound_tcb ntfn None);
set_bound_notification ntfnptr None
od
od \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfnptra. \<lbrace>bound_tcb_at ((=) ntfnptra) ntfnptr and valid_sched\<rbrace> case ntfnptra of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
y <- set_notification ntfnptr' (ntfn_set_bound_tcb ntfn None);
set_bound_notification ntfnptr None
od \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfnptra a. ntfnptra = Some a \<Longrightarrow> \<lbrace>bound_tcb_at ((=) ntfnptra) ntfnptr and valid_sched\<rbrace> case ntfnptra of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
y <- set_notification ntfnptr' (ntfn_set_bound_tcb ntfn None);
set_bound_notification ntfnptr None
od \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrace>bound_tcb_at ((=) (Some a)) ntfnptr and valid_sched\<rbrace> do ntfn <- get_notification a;
y <- set_notification a (ntfn_set_bound_tcb ntfn None);
set_bound_notification ntfnptr None
od \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a ntfn. \<lbrace>ko_at (Notification ntfn) a and (bound_tcb_at ((=) (Some a)) ntfnptr and valid_sched)\<rbrace> do y <- set_notification a (ntfn_set_bound_tcb ntfn None);
set_bound_notification ntfnptr None
od \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma reply_cancel_ipc_valid_sched[wp]:
  "\<lbrace>valid_sched\<rbrace> reply_cancel_ipc tptr \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (simp add: reply_cancel_ipc_def) apply (wp hoare_drop_imps thread_set_not_state_valid_sched | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> reply_cancel_ipc tptr \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> do y <- thread_set (tcb_fault_update (\<lambda>_. None)) tptr;
cap <- get_cap (tptr, tcb_cnode_index 2);
descs <- gets (descendants_of (tptr, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>a b. descs = {(a, b)});
select descs >>= cap_delete_one
od)
od \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma st_tcb_at_not:
  "st_tcb_at (\<lambda>st. \<not> P st) t s = (\<not> st_tcb_at P t s \<and> tcb_at t s)" apply (clarsimp simp: not_pred_tcb) apply (fastforce simp: st_tcb_at_tcb_at) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_tcb_at (\<lambda>st. \<not> P st) t s = (\<not> st_tcb_at P t s \<and> tcb_at t s) proof (prove)
goal (1 subgoal):
 1. st_tcb_at (\<lambda>st. \<not> P st) t s = ((tcb_at t s \<longrightarrow> st_tcb_at (\<lambda>a. \<not> P a) t s) \<and> tcb_at t s) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_thread_state_not_runnable_valid_queues:
  "\<lbrace>valid_queues and ct_not_in_q and (\<lambda>s. st_tcb_at (\<lambda>ts. \<not> runnable ts) ref s)\<rbrace>
     set_thread_state ref ts
   \<lbrace>\<lambda>_. valid_queues\<rbrace>" apply (simp add: set_thread_state_def) apply (simp add: set_thread_state_ext_def set_object_def get_object_def | wp)+ apply (fastforce simp: valid_queues_def st_tcb_at_kh_if_split ct_not_in_q_def
                         st_tcb_at_not) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues and ct_not_in_q and st_tcb_at (\<lambda>ts. \<not> runnable ts) ref\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues and ct_not_in_q and st_tcb_at (\<lambda>ts. \<not> runnable ts) ref\<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> ct_not_in_q s \<and> st_tcb_at (\<lambda>ts. \<not> runnable ts) ref 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_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_thread_state_not_runnable_weak_valid_sched_action:
  "\<lbrace>weak_valid_sched_action and (\<lambda>s. st_tcb_at (\<lambda>ts. \<not> runnable ts) ref s)\<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
                        st_tcb_at_not) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>weak_valid_sched_action and st_tcb_at (\<lambda>ts. \<not> runnable ts) ref\<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 st_tcb_at (\<lambda>ts. \<not> runnable ts) ref\<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> st_tcb_at (\<lambda>ts. \<not> runnable ts) ref 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> 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_not_runnable_valid_sched_action:
  "\<lbrace>valid_sched_action and (\<lambda>s. st_tcb_at (\<lambda>ts. \<not> runnable ts) ref s)\<rbrace>
      set_thread_state ref ts
   \<lbrace>\<lambda>_. valid_sched_action\<rbrace>" apply (simp add: valid_sched_action_def |
         wp set_thread_state_not_runnable_weak_valid_sched_action)+ done

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

lemma set_thread_state_not_runnable_valid_sched:
  "\<lbrace>valid_sched and (\<lambda>s. st_tcb_at (\<lambda>ts. \<not> runnable ts) ref s) and K (\<not> runnable ts)\<rbrace>
     set_thread_state ref ts
   \<lbrace>\<lambda>_. valid_sched\<rbrace>" apply (simp add: valid_sched_def |
         wp set_thread_state_not_runnable_valid_queues
                                        set_thread_state_not_runnable_valid_sched_action
                                        set_thread_state_not_runnable_valid_blocked)+ done

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

lemma blocked_cancel_ipc_valid_sched[wp]:
  "\<lbrace>valid_sched and (\<lambda>s. st_tcb_at (\<lambda>ts. \<not> runnable ts) tptr s)\<rbrace>
     blocked_cancel_ipc ts tptr
   \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (simp add: blocked_cancel_ipc_def) apply (wp set_thread_state_not_runnable_valid_sched) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and st_tcb_at (\<lambda>ts. \<not> runnable ts) tptr\<rbrace> blocked_cancel_ipc ts tptr \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and st_tcb_at (\<lambda>ts. \<not> runnable ts) tptr\<rbrace> do epptr <- get_blocking_object ts;
ep <- get_endpoint epptr;
queue <- get_ep_queue ep;
y <- set_endpoint epptr (case remove1 tptr queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 tptr queue));
set_thread_state tptr Inactive
od \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_sched and st_tcb_at (\<lambda>ts. \<not> runnable ts) tptr) s \<Longrightarrow> valid_sched s \<and> st_tcb_at (\<lambda>ts. \<not> runnable ts) tptr s \<and> K (\<not> runnable Inactive) s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma cancel_signal_valid_sched[wp]:
  "\<lbrace>valid_sched and (\<lambda>s. st_tcb_at (\<lambda>ts. \<not> runnable ts) tptr s)\<rbrace>
     cancel_signal tptr ntfnptr
   \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (simp add: cancel_signal_def) apply (wp set_thread_state_not_runnable_valid_sched hoare_drop_imps | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and st_tcb_at (\<lambda>ts. \<not> runnable ts) tptr\<rbrace> cancel_signal tptr ntfnptr \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and st_tcb_at (\<lambda>ts. \<not> runnable ts) tptr\<rbrace> do ntfn <- get_notification ntfnptr;
queue <- case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfnptr (ntfn_set_obj ntfn (case remove1 tptr queue of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (remove1 tptr queue)));
set_thread_state tptr Inactive
od \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma (in DetSchedSchedule_AI) cancel_ipc_valid_sched[wp]:
  "\<lbrace>valid_sched\<rbrace> cancel_ipc tptr \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (simp add: cancel_ipc_def get_thread_state_def thread_get_def) apply (wp | wpc)+ apply (fastforce intro: st_tcb_at_get_lift) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> cancel_ipc tptr \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> do tcb <- gets_the (get_tcb tptr);
case tcb_state tcb of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc (tcb_state tcb) tptr | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc (tcb_state tcb) tptr | BlockedOnReply \<Rightarrow> reply_cancel_ipc tptr | BlockedOnNotification x \<Rightarrow> cancel_signal tptr x | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_sched s \<Longrightarrow> get_tcb tptr s \<noteq> None \<longrightarrow> (tcb_state (the (get_tcb tptr s)) = Running \<longrightarrow> valid_sched s) \<and> (inactive (tcb_state (the (get_tcb tptr s))) \<longrightarrow> valid_sched s) \<and> (tcb_state (the (get_tcb tptr s)) = Restart \<longrightarrow> valid_sched s) \<and> (\<forall>x xa. tcb_state (the (get_tcb tptr s)) = BlockedOnReceive x xa \<longrightarrow> (valid_sched and st_tcb_at (\<lambda>ts. \<not> runnable ts) tptr) s) \<and> (\<forall>x xa. tcb_state (the (get_tcb tptr s)) = BlockedOnSend x xa \<longrightarrow> (valid_sched and st_tcb_at (\<lambda>ts. \<not> runnable ts) tptr) s) \<and> (awaiting_reply (tcb_state (the (get_tcb tptr s))) \<longrightarrow> valid_sched s) \<and> (\<forall>x. tcb_state (the (get_tcb tptr s)) = BlockedOnNotification x \<longrightarrow> (valid_sched and st_tcb_at (\<lambda>ts. \<not> runnable ts) tptr) s) \<and> (idle (tcb_state (the (get_tcb tptr s))) \<longrightarrow> valid_sched s) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_scheduler_action_simple_sched_action[wp]:
  "\<lbrace>K $ simple_sched_action_2 action\<rbrace>
    set_scheduler_action action
   \<lbrace>\<lambda>rv. simple_sched_action\<rbrace>" by (simp add: set_scheduler_action_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K $ simple_sched_action_2 action\<rbrace> set_scheduler_action action \<lbrace>\<lambda>rv. simple_sched_action\<rbrace>
theory DetSchedSchedule_AI

lemma reschedule_required_simple_sched_action[wp]:
  "\<lbrace>simple_sched_action\<rbrace> reschedule_required  \<lbrace>\<lambda>rv. simple_sched_action\<rbrace>" by (simp add: reschedule_required_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>simple_sched_action\<rbrace> reschedule_required \<lbrace>\<lambda>rv. simple_sched_action\<rbrace>
theory DetSchedSchedule_AI

lemma rec_del_valid_sched'[wp]:
  "\<lbrace>valid_sched and simple_sched_action\<rbrace>
    rec_del call
   \<lbrace>\<lambda>rv. valid_sched and simple_sched_action\<rbrace>" apply (rule rec_del_preservation) apply (wp preemption_point_inv' | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and simple_sched_action\<rbrace> rec_del call \<lbrace>\<lambda>rv. valid_sched and simple_sched_action\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s sl1 sl2. \<lbrace>valid_sched and simple_sched_action\<rbrace> cap_swap_for_delete sl1 sl2 \<lbrace>\<lambda>rv. valid_sched and simple_sched_action\<rbrace>
 2. \<And>s sl cap. \<lbrace>valid_sched and simple_sched_action\<rbrace> set_cap sl cap \<lbrace>\<lambda>rv. valid_sched and simple_sched_action\<rbrace>
 3. \<And>s sl opt. \<lbrace>valid_sched and simple_sched_action\<rbrace> empty_slot sl opt \<lbrace>\<lambda>rv. valid_sched and simple_sched_action\<rbrace>
 4. \<And>s cap fin. \<lbrace>valid_sched and simple_sched_action\<rbrace> finalise_cap cap fin \<lbrace>\<lambda>rv. valid_sched and simple_sched_action\<rbrace>
 5. \<And>s. \<lbrace>valid_sched and simple_sched_action\<rbrace> preemption_point \<lbrace>\<lambda>rv. valid_sched and simple_sched_action\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma rec_del_valid_sched[wp]:
  "\<lbrace>valid_sched and simple_sched_action\<rbrace> rec_del call \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (rule hoare_strengthen_post) apply (rule rec_del_valid_sched') apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and simple_sched_action\<rbrace> rec_del call \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>valid_sched and simple_sched_action\<rbrace> rec_del call \<lbrace>?Q\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> valid_sched s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (valid_sched and simple_sched_action) s \<Longrightarrow> valid_sched s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma rec_del_simple_sched_action[wp]:
  "\<lbrace>simple_sched_action\<rbrace> rec_del call \<lbrace>\<lambda>rv. simple_sched_action\<rbrace>" by (wp rec_del_preservation preemption_point_inv' | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>simple_sched_action\<rbrace> rec_del call \<lbrace>\<lambda>rv. simple_sched_action\<rbrace>
theory DetSchedSchedule_AI

lemma ethread_set_valid_etcbs[wp]:
  "\<lbrace>valid_etcbs\<rbrace> ethread_set f tptr \<lbrace>\<lambda>_. valid_etcbs\<rbrace>" apply (simp add: ethread_set_def set_eobject_def | wp)+ apply (clarsimp simp: valid_etcbs_def is_etcb_at_def get_etcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> ethread_set f tptr \<lbrace>\<lambda>_. valid_etcbs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_etcbs s \<Longrightarrow> (\<exists>y. get_etcb tptr s = Some y) \<longrightarrow> valid_etcbs_2 (\<lambda>a. if a = tptr then Some (f (the (get_etcb tptr s))) else ekheap s a) (kheap s) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma ethread_set_not_queued_valid_queues:
  "\<lbrace>valid_queues and not_queued tptr\<rbrace>
     ethread_set f tptr
   \<lbrace>\<lambda>_. valid_queues\<rbrace>" apply (simp add: ethread_set_def set_eobject_def not_queued_def | wp)+ apply (clarsimp simp: valid_queues_def is_etcb_at_def etcb_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues and not_queued tptr\<rbrace> ethread_set f tptr \<lbrace>\<lambda>_. valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_queues s \<and> (\<forall>d p. tptr \<notin> set (ready_queues s d p)) \<Longrightarrow> (\<exists>y. get_etcb tptr s = Some y) \<longrightarrow> valid_queues_2 (ready_queues s) (\<lambda>a. if a = tptr then Some (f (the (get_etcb tptr s))) else ekheap s a) (kheap s) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma ethread_set_weak_valid_sched_action[wp]:
  "\<lbrace>weak_valid_sched_action\<rbrace>
     ethread_set f tptr \<lbrace>\<lambda>_. weak_valid_sched_action\<rbrace>" apply (simp add: ethread_set_def set_eobject_def | wp)+ apply (clarsimp simp: weak_valid_sched_action_def is_etcb_at_def etcb_at_def get_etcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>weak_valid_sched_action\<rbrace> ethread_set f tptr \<lbrace>\<lambda>_. weak_valid_sched_action\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. weak_valid_sched_action s \<Longrightarrow> (\<exists>y. get_etcb tptr s = Some y) \<longrightarrow> weak_valid_sched_action_2 (scheduler_action s) (\<lambda>a. if a = tptr then Some (f (the (get_etcb tptr s))) else ekheap s a) (kheap s) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma ethread_set_not_domain_switch_in_cur_domain:
  "(\<And>x. tcb_domain (f x) = tcb_domain x)
  \<Longrightarrow> \<lbrace>switch_in_cur_domain\<rbrace>
     ethread_set f tptr \<lbrace>\<lambda>_. switch_in_cur_domain\<rbrace>" apply (simp add: ethread_set_def set_eobject_def | wp)+ apply (clarsimp simp: switch_in_cur_domain_def in_cur_domain_def etcb_at_def get_etcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. tcb_domain (f x) = tcb_domain x) \<Longrightarrow> \<lbrace>switch_in_cur_domain\<rbrace> ethread_set f tptr \<lbrace>\<lambda>_. switch_in_cur_domain\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>x. tcb_domain (f x) = tcb_domain x; switch_in_cur_domain s\<rbrakk> \<Longrightarrow> (\<exists>y. get_etcb tptr s = Some y) \<longrightarrow> switch_in_cur_domain_2 (scheduler_action s) (\<lambda>a. if a = tptr then Some (f (the (get_etcb tptr s))) else ekheap s a) (cur_domain s) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma ethread_set_not_domain_ct_in_cur_domain:
  "(\<And>x. tcb_domain (f x) = tcb_domain x)
  \<Longrightarrow> \<lbrace>ct_in_cur_domain\<rbrace>
     ethread_set f tptr \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace>" apply (simp add: ethread_set_def set_eobject_def | wp)+ apply (clarsimp simp: ct_in_cur_domain_def in_cur_domain_def etcb_at_def get_etcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. tcb_domain (f x) = tcb_domain x) \<Longrightarrow> \<lbrace>ct_in_cur_domain\<rbrace> ethread_set f tptr \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>x. tcb_domain (f x) = tcb_domain x; ct_in_cur_domain s\<rbrakk> \<Longrightarrow> (\<exists>y. get_etcb tptr s = Some y) \<longrightarrow> ct_in_cur_domain_2 (cur_thread s) (idle_thread s) (scheduler_action s) (cur_domain s) (\<lambda>a. if a = tptr then Some (f (the (get_etcb tptr s))) else ekheap s a) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma ethread_set_not_domain_valid_blocked:
  "(\<And>x. tcb_domain (f x) = tcb_domain x)
  \<Longrightarrow> \<lbrace>valid_blocked\<rbrace>
     ethread_set f tptr \<lbrace>\<lambda>_. valid_blocked\<rbrace>" apply (simp add: ethread_set_def set_eobject_def | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. tcb_domain (f x) = tcb_domain x) \<Longrightarrow> \<lbrace>valid_blocked\<rbrace> ethread_set f tptr \<lbrace>\<lambda>_. valid_blocked\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma ethread_set_not_domain_valid_blocked_except:
  "(\<And>x. tcb_domain (f x) = tcb_domain x)
  \<Longrightarrow> \<lbrace>valid_blocked_except ref\<rbrace>
     ethread_set f tptr \<lbrace>\<lambda>_. valid_blocked_except ref\<rbrace>" apply (simp add: ethread_set_def set_eobject_def | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. tcb_domain (f x) = tcb_domain x) \<Longrightarrow> \<lbrace>valid_blocked_except ref\<rbrace> ethread_set f tptr \<lbrace>\<lambda>_. valid_blocked_except ref\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma ethread_set_not_domain_valid_sched_action:
  "(\<And>x. tcb_domain (f x) = tcb_domain x)
  \<Longrightarrow> \<lbrace>valid_sched_action\<rbrace>
     ethread_set f tptr \<lbrace>\<lambda>_. valid_sched_action\<rbrace>" apply (simp add: valid_sched_action_def | wp ethread_set_not_domain_switch_in_cur_domain)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. tcb_domain (f x) = tcb_domain x) \<Longrightarrow> \<lbrace>valid_sched_action\<rbrace> ethread_set f tptr \<lbrace>\<lambda>_. valid_sched_action\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma ethread_set_valid_idle_etcb:
  "(\<And>x. tcb_domain (f x) = tcb_domain x)
  \<Longrightarrow> \<lbrace>valid_idle_etcb\<rbrace>
     ethread_set f tptr \<lbrace>\<lambda>_. valid_idle_etcb\<rbrace>" apply(simp add: ethread_set_def valid_idle_etcb_def set_eobject_def) apply wp apply(simp add: etcb_at_def get_etcb_def split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. tcb_domain (f x) = tcb_domain x) \<Longrightarrow> \<lbrace>valid_idle_etcb\<rbrace> ethread_set f tptr \<lbrace>\<lambda>_. valid_idle_etcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>x. tcb_domain (f x) = tcb_domain x) \<Longrightarrow> \<lbrace>etcb_at (\<lambda>etcb. tcb_domain etcb = default_domain) idle_thread_ptr\<rbrace> do tcb <- gets_the (get_etcb tptr);
es <- get;
put (ekheap_update (\<lambda>_. (ekheap es)(tptr \<mapsto> f tcb)) es)
od \<lbrace>\<lambda>_. etcb_at (\<lambda>etcb. tcb_domain etcb = default_domain) idle_thread_ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>x. tcb_domain (f x) = tcb_domain x; etcb_at (\<lambda>etcb. tcb_domain etcb = default_domain) idle_thread_ptr s\<rbrakk> \<Longrightarrow> get_etcb tptr s \<noteq> None \<longrightarrow> etcb_at (\<lambda>etcb. tcb_domain etcb = default_domain) idle_thread_ptr (ekheap_update (\<lambda>_. (ekheap s)(tptr \<mapsto> f (the (get_etcb tptr s)))) s) proof (prove)
goal:
No subgoals!