kings-crown/FVELER_Isabelle huggingface dataset:
theory BCorres2_AI

lemma cte_wp_at[wp]: "I (\<lambda>s. P (cte_wp_at P' p s))" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace> f \<lbrace>\<lambda>_ s. P (cte_wp_at P' p s)\<rbrace>
theory BCorres2_AI

lemma no_cap_to_obj_dr_emp[wp]: "I (no_cap_to_obj_dr_emp x)" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_cap_to_obj_dr_emp x\<rbrace> f \<lbrace>\<lambda>_. no_cap_to_obj_dr_emp x\<rbrace>
theory BCorres2_AI

lemma valid_vs_lookup[wp]: "I (valid_vs_lookup)" proof goal_cases interpret Arch . case 1 show ?case by (rule lift_inv, simp) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vs_lookup\<rbrace> f \<lbrace>\<lambda>_. valid_vs_lookup\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>valid_vs_lookup\<rbrace> f \<lbrace>\<lambda>_. valid_vs_lookup\<rbrace> proof (prove)
goal:
No subgoals! proof (state)
goal (1 subgoal):
 1. \<lbrace>valid_vs_lookup\<rbrace> f \<lbrace>\<lambda>_. valid_vs_lookup\<rbrace> proof (state)
this:


goal (1 subgoal):
 1. \<lbrace>valid_vs_lookup\<rbrace> f \<lbrace>\<lambda>_. valid_vs_lookup\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vs_lookup\<rbrace> f \<lbrace>\<lambda>_. valid_vs_lookup\<rbrace> proof (state)
this:
\<lbrace>valid_vs_lookup\<rbrace> f \<lbrace>\<lambda>_. valid_vs_lookup\<rbrace>

goal:
No subgoals!
theory BCorres2_AI

lemma typ_at[wp]: "I (\<lambda>s. P (typ_at T p s))" by (rule lift_inv,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace>
theory BCorres2_AI

lemma all_but_exst_update[simp]:
  "all_but_exst P (trans_state f s) = all_but_exst P s" apply (simp add: all_but_exst_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. all_but_exst P (trans_state f s) = all_but_exst P s proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma cap_delete_bcorres'[wp]:
  assumes finalise_cap_bcorres[wp]:
    "\<And>r ra. bcorres (finalise_cap r ra :: 'a::state_ext state \<Rightarrow> _) (finalise_cap r ra)"
  shows "bcorres (cap_delete slot :: 'a state \<Rightarrow> _) (cap_delete slot)" unfolding cap_delete_def apply wp apply (simp add: returnOk_bcorres_underlying) apply (wp rec_del_bcorres) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (cap_delete slot) (cap_delete slot) proof (prove)
goal (1 subgoal):
 1. bcorres (doE rec_del (CTEDeleteCall slot True);
returnOk ()
odE) (doE rec_del (CTEDeleteCall slot True);
returnOk ()
odE) proof (prove)
goal (2 subgoals):
 1. \<And>r. bcorres (K_bind (returnOk ()) r) (K_bind (returnOk ()) r)
 2. bcorres (rec_del (CTEDeleteCall slot True)) (rec_del (CTEDeleteCall slot True)) proof (prove)
goal (1 subgoal):
 1. bcorres (rec_del (CTEDeleteCall slot True)) (rec_del (CTEDeleteCall slot True)) proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma check_cap_at_bcorres[wp]: "bcorres f f' \<Longrightarrow> bcorres (check_cap_at a b f) (check_cap_at a b f')" apply (simp add: check_cap_at_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres f f' \<Longrightarrow> bcorres (check_cap_at a b f) (check_cap_at a b f') proof (prove)
goal (1 subgoal):
 1. bcorres f f' \<Longrightarrow> bcorres (do cap' <- get_cap b;
when (same_object_as a cap') f
od) (do cap' <- get_cap b;
when (same_object_as a cap') f'
od) proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma invoke_domain_bcorres[wp]: "bcorres (invoke_domain t d) (invoke_domain t d)" by (simp add: invoke_domain_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (invoke_domain t d) (invoke_domain t d)
theory BCorres2_AI

lemma truncate_state_detype[simp]: "truncate_state (detype x s) = detype x (truncate_state s)" apply (simp add: detype_def trans_state_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. truncate_state (detype x s) = detype x (truncate_state s) proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma resolve_address_bits_bcorres[wp]: "bcorres (resolve_address_bits a) (resolve_address_bits a)" apply (simp add: resolve_address_bits_def) apply (rule use_sbcorres_underlying) apply (rule resolve_address_bits'_sbcorres) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (resolve_address_bits a) (resolve_address_bits a) proof (prove)
goal (1 subgoal):
 1. bcorres (resolve_address_bits' TYPE('a) a) (resolve_address_bits' TYPE(unit) a) proof (prove)
goal (1 subgoal):
 1. \<And>s. s_bcorres (resolve_address_bits' TYPE('a) a) (resolve_address_bits' TYPE(unit) a) s proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma bcorres_cap_fault_on_failure[wp]: "bcorres f f' \<Longrightarrow> bcorres (cap_fault_on_failure a b f) (cap_fault_on_failure a b f')" apply (simp add: cap_fault_on_failure_def) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres f f' \<Longrightarrow> bcorres (cap_fault_on_failure a b f) (cap_fault_on_failure a b f') proof (prove)
goal (1 subgoal):
 1. bcorres f f' \<Longrightarrow> bcorres (f <handle2> throwError \<circ> CapFault a b) (f' <handle2> throwError \<circ> CapFault a b) proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma lookup_error_on_failure_bcorres[wp]: "bcorres b b' \<Longrightarrow> bcorres (lookup_error_on_failure a b) (lookup_error_on_failure a b')" apply (simp add: lookup_error_on_failure_def) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres b b' \<Longrightarrow> bcorres (lookup_error_on_failure a b) (lookup_error_on_failure a b') proof (prove)
goal (1 subgoal):
 1. bcorres b b' \<Longrightarrow> bcorres (b <handle2> throwError \<circ> FailedLookup a) (b' <handle2> throwError \<circ> FailedLookup a) proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma empty_on_failure_bcorres[wp]: "bcorres f f' \<Longrightarrow> bcorres (empty_on_failure f) (empty_on_failure f')" apply (simp add: empty_on_failure_def) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres f f' \<Longrightarrow> bcorres (empty_on_failure f) (empty_on_failure f') proof (prove)
goal (1 subgoal):
 1. bcorres f f' \<Longrightarrow> bcorres (f <catch> (\<lambda>x. return [])) (f' <catch> (\<lambda>x. return [])) proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma unify_failure_bcorres[wp]: "bcorres f f' \<Longrightarrow> bcorres (unify_failure f) (unify_failure f')" apply (simp add: unify_failure_def) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres f f' \<Longrightarrow> bcorres (unify_failure f) (unify_failure f') proof (prove)
goal (1 subgoal):
 1. bcorres f f' \<Longrightarrow> bcorres (f <handle2> (\<lambda>x. throwError ())) (f' <handle2> (\<lambda>x. throwError ())) proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma const_on_failure_bcorres[wp]: "bcorres f f' \<Longrightarrow> bcorres (const_on_failure c f) (const_on_failure c f')" apply (simp add: const_on_failure_def) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres f f' \<Longrightarrow> bcorres (const_on_failure c f) (const_on_failure c f') proof (prove)
goal (1 subgoal):
 1. bcorres f f' \<Longrightarrow> bcorres (f <catch> (\<lambda>x. return c)) (f' <catch> (\<lambda>x. return c)) proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma get_receive_slots_bcorres[wp]: "bcorres (get_receive_slots a b) (get_receive_slots a b)" by (cases b; wpsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (get_receive_slots a b) (get_receive_slots a b)
theory BCorres2_AI

lemma (in BCorres2_AI) make_fault_msg_bcorres[wp]:
  "bcorres (make_fault_msg a b :: 'a state \<Rightarrow> _) (make_fault_msg a b)" apply (cases a) apply (wp | wpc | simp | intro impI conjI allI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (make_fault_msg a b) (make_fault_msg a b) proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12 x13. a = CapFault x11 x12 x13 \<Longrightarrow> bcorres (make_fault_msg a b) (make_fault_msg a b)
 2. \<And>x2. a = UnknownSyscallException x2 \<Longrightarrow> bcorres (make_fault_msg a b) (make_fault_msg a b)
 3. \<And>x31 x32. a = UserException x31 x32 \<Longrightarrow> bcorres (make_fault_msg a b) (make_fault_msg a b)
 4. \<And>x4. a = ArchFault x4 \<Longrightarrow> bcorres (make_fault_msg a b) (make_fault_msg a b) proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma (in BCorres2_AI) handle_fault_reply_bcorres[wp]:
  "bcorres (handle_fault_reply a b c d :: 'a state \<Rightarrow> _) (handle_fault_reply a b c d)" apply (cases a) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (handle_fault_reply a b c d) (handle_fault_reply a b c d) proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12 x13. a = CapFault x11 x12 x13 \<Longrightarrow> bcorres (handle_fault_reply a b c d) (handle_fault_reply a b c d)
 2. \<And>x2. a = UnknownSyscallException x2 \<Longrightarrow> bcorres (handle_fault_reply a b c d) (handle_fault_reply a b c d)
 3. \<And>x31 x32. a = UserException x31 x32 \<Longrightarrow> bcorres (handle_fault_reply a b c d) (handle_fault_reply a b c d)
 4. \<And>x4. a = ArchFault x4 \<Longrightarrow> bcorres (handle_fault_reply a b c d) (handle_fault_reply a b c d) proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma decode_read_registers_bcorres[wp]: "bcorres (decode_read_registers a (cap.ThreadCap b)) (decode_read_registers a (cap.ThreadCap b))" apply (simp add: decode_read_registers_def) apply (wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (decode_read_registers a (ThreadCap b)) (decode_read_registers a (ThreadCap b)) proof (prove)
goal (1 subgoal):
 1. bcorres (case a of [] \<Rightarrow> throwError TruncatedMessage | [flags] \<Rightarrow> throwError TruncatedMessage | flags # n # x \<Rightarrow> doE range_check n 1 $ word_of_nat (length frameRegisters + length gpRegisters);
p <- case ThreadCap b of ThreadCap p \<Rightarrow> returnOk p;
self <- liftE $ gets cur_thread;
whenE (p = self) $ throwError IllegalOperation;
returnOk $ ReadRegisters p (flags !! 0) n ArchDefaultExtraRegisters
odE) (case a of [] \<Rightarrow> throwError TruncatedMessage | [flags] \<Rightarrow> throwError TruncatedMessage | flags # n # x \<Rightarrow> doE range_check n 1 $ word_of_nat (length frameRegisters + length gpRegisters);
p <- case ThreadCap b of ThreadCap p \<Rightarrow> returnOk p;
self <- liftE $ gets cur_thread;
whenE (p = self) $ throwError IllegalOperation;
returnOk $ ReadRegisters p (flags !! 0) n ArchDefaultExtraRegisters
odE) proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma decode_write_registers_bcorres[wp]: "bcorres (decode_write_registers a (cap.ThreadCap b)) (decode_write_registers a (cap.ThreadCap b))" apply (simp add: decode_write_registers_def) apply (wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (decode_write_registers a (ThreadCap b)) (decode_write_registers a (ThreadCap b)) proof (prove)
goal (1 subgoal):
 1. bcorres (case a of [] \<Rightarrow> throwError TruncatedMessage | [flags] \<Rightarrow> throwError TruncatedMessage | flags # n # values \<Rightarrow> doE whenE (length values < unat n) $ throwError TruncatedMessage;
p <- case ThreadCap b of ThreadCap p \<Rightarrow> returnOk p;
self <- liftE $ gets cur_thread;
whenE (p = self) $ throwError IllegalOperation;
returnOk $ WriteRegisters p (flags !! 0) (take (unat n) values) ArchDefaultExtraRegisters
odE) (case a of [] \<Rightarrow> throwError TruncatedMessage | [flags] \<Rightarrow> throwError TruncatedMessage | flags # n # values \<Rightarrow> doE whenE (length values < unat n) $ throwError TruncatedMessage;
p <- case ThreadCap b of ThreadCap p \<Rightarrow> returnOk p;
self <- liftE $ gets cur_thread;
whenE (p = self) $ throwError IllegalOperation;
returnOk $ WriteRegisters p (flags !! 0) (take (unat n) values) ArchDefaultExtraRegisters
odE) proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma decode_copy_registers_bcorres[wp]: "bcorres (decode_copy_registers a (cap.ThreadCap b) e) (decode_copy_registers a (cap.ThreadCap b) e)" apply (simp add: decode_copy_registers_def) apply (wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (decode_copy_registers a (ThreadCap b) e) (decode_copy_registers a (ThreadCap b) e) proof (prove)
goal (1 subgoal):
 1. bcorres (case a of [] \<Rightarrow> throwError TruncatedMessage | flags # x \<Rightarrow> doE suspend_source <- returnOk (flags !! 0);
resume_target <- returnOk (flags !! 1);
transfer_frame <- returnOk (flags !! 2);
transfer_integer <- returnOk (flags !! 3);
whenE (e = []) $ throwError TruncatedMessage;
src_tcb <- case e of [] \<Rightarrow> throwError $ InvalidCapability 1 | ThreadCap p # x \<Rightarrow> returnOk p | _ # x \<Rightarrow> throwError $ InvalidCapability 1;
p <- case ThreadCap b of ThreadCap p \<Rightarrow> returnOk p;
returnOk $ CopyRegisters p src_tcb suspend_source resume_target transfer_frame transfer_integer ArchDefaultExtraRegisters
odE) (case a of [] \<Rightarrow> throwError TruncatedMessage | flags # x \<Rightarrow> doE suspend_source <- returnOk (flags !! 0);
resume_target <- returnOk (flags !! 1);
transfer_frame <- returnOk (flags !! 2);
transfer_integer <- returnOk (flags !! 3);
whenE (e = []) $ throwError TruncatedMessage;
src_tcb <- case e of [] \<Rightarrow> throwError $ InvalidCapability 1 | ThreadCap p # x \<Rightarrow> returnOk p | _ # x \<Rightarrow> throwError $ InvalidCapability 1;
p <- case ThreadCap b of ThreadCap p \<Rightarrow> returnOk p;
returnOk $ CopyRegisters p src_tcb suspend_source resume_target transfer_frame transfer_integer ArchDefaultExtraRegisters
odE) proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma alternative_first:"x \<in> fst (f s) \<Longrightarrow> x \<in> fst ((f \<sqinter> g) s)" by (simp add: alternative_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> fst (f s) \<Longrightarrow> x \<in> fst ((f \<sqinter> g) s)
theory BCorres2_AI

lemma alternative_second:"x \<in> fst (g s) \<Longrightarrow> x \<in> fst ((f \<sqinter> g) s)" by (simp add: alternative_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> fst (g s) \<Longrightarrow> x \<in> fst ((f \<sqinter> g) s)
theory BCorres2_AI

lemma bcorres_underlying_dest: "bcorres_underlying l f k \<Longrightarrow> ((),s') \<in> fst (f s) \<Longrightarrow>
       ((),l s') \<in> fst (k (l s))" apply (clarsimp simp add: bcorres_underlying_def s_bcorres_underlying_def) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bcorres_underlying l f k; ((), s') \<in> fst (f s)\<rbrakk> \<Longrightarrow> ((), l s') \<in> fst (k (l s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. (\<lambda>x. case x of (x, y) \<Rightarrow> ((), l y)) ` fst (f s) \<subseteq> fst (k (l s)); ((), s') \<in> fst (f s)\<rbrakk> \<Longrightarrow> ((), l s') \<in> fst (k (l s)) proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma trans_state_twice[simp]: "trans_state (\<lambda>_. e) (trans_state f s) = trans_state (\<lambda>_. e) s" by (rule trans_state_update'')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. trans_state (\<lambda>_. e) (trans_state f s) = trans_state (\<lambda>_. e) s
theory BCorres2_AI

lemma guarded_sub_switch: "((),x) \<in> fst (guarded_switch_to word s) \<Longrightarrow>
       ((),x) \<in> fst (switch_to_thread word s)
       \<and> (\<exists>y. get_tcb word s = Some y \<and> runnable (tcb_state y))" apply (clarsimp simp add: guarded_switch_to_def bind_def
                            get_thread_state_def
                            thread_get_def
                            in_monad) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((), x) \<in> fst (guarded_switch_to word s) \<Longrightarrow> ((), x) \<in> fst (switch_to_thread word s) \<and> (\<exists>y. get_tcb word s = Some y \<and> runnable (tcb_state y)) proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma truncate_state_updates[simp]:
  "truncate_state (scheduler_action_update f s) = truncate_state s"
  "truncate_state (ready_queues_update g s) = truncate_state s" by (rule trans_state_update'')+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. truncate_state (scheduler_action_update f s) = truncate_state s &&& truncate_state (ready_queues_update g s) = truncate_state s
theory BCorres2_AI

lemma get_before_assert_opt:
  "do s \<leftarrow> assert_opt x; s' \<leftarrow> get; f s s' od
    = do s' \<leftarrow> get; s \<leftarrow> assert_opt x; f s s' od" apply (cases x, simp_all add: assert_opt_def) apply (simp add: ext exec_get) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do s <- assert_opt x;
get >>= f s
od = do s' <- get;
s <- assert_opt x;
f s s'
od proof (prove)
goal (1 subgoal):
 1. x = None \<Longrightarrow> fail = do s' <- get;
fail
od proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma s_bcorres_get_left:
  "(s_bcorres_underlying t (get >>= f) g s)
    = (s_bcorres_underlying t (f s) g s)" by (simp add: s_bcorres_underlying_def exec_get)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s_bcorres_underlying t (get >>= f) g s = s_bcorres_underlying t (f s) g s
theory BCorres2_AI

lemma get_outside_alternative:
  "alternative (get >>= f) g
    = do s \<leftarrow> get; alternative (f s) g od" by (simp add: alternative_def exec_get fun_eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (get >>= f \<sqinter> g) = do s <- get;
f s \<sqinter> g
od
theory BCorres2_AI

lemma switch_thread_bcorreses:
  "bcorres (switch_to_idle_thread :: 'a state \<Rightarrow> _) switch_to_idle_thread"
  "bcorres (switch_to_thread t :: 'a state \<Rightarrow> _) (switch_to_thread t)" apply (simp_all add: switch_to_idle_thread_def switch_to_thread_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres switch_to_idle_thread switch_to_idle_thread &&& bcorres (switch_to_thread t) (switch_to_thread t) proof (prove)
goal (2 subgoals):
 1. bcorres (do thread <- gets idle_thread;
y <- arch_switch_to_idle_thread;
modify (cur_thread_update (\<lambda>_. thread))
od) (do thread <- gets idle_thread;
y <- arch_switch_to_idle_thread;
modify (cur_thread_update (\<lambda>_. thread))
od)
 2. bcorres (do state <- get;
y <- assert (\<exists>y. get_tcb t state = Some y);
y <- arch_switch_to_thread t;
y <- do_extended_op (tcb_sched_action tcb_sched_dequeue t);
modify (cur_thread_update (\<lambda>_. t))
od) (do state <- get;
y <- assert (\<exists>y. get_tcb t state = Some y);
y <- arch_switch_to_thread t;
y <- do_extended_op (tcb_sched_action tcb_sched_dequeue t);
modify (cur_thread_update (\<lambda>_. t))
od) proof (prove)
goal:
No subgoals!
theory BCorres2_AI

lemma tcb_sched_action_bcorres:
  "bcorres (tcb_sched_action a b) (return ())" by (clarsimp simp: bcorres_underlying_def s_bcorres_underlying_def return_def
              dest!: tcb_sched_action_extended.ex_st)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (tcb_sched_action a b) (return ())
theory BCorres2_AI

lemma if_s_bcorres_underlying[wp]:
  "(P \<Longrightarrow> s_bcorres_underlying t f f' s) \<Longrightarrow> (\<not>P \<Longrightarrow> s_bcorres_underlying t g g' s)
  \<Longrightarrow> s_bcorres_underlying t (if P then f else g) (if P then f' else g') s" by (simp add: return_s_bcorres_underlying)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<Longrightarrow> s_bcorres_underlying t f f' s; \<not> P \<Longrightarrow> s_bcorres_underlying t g g' s\<rbrakk> \<Longrightarrow> s_bcorres_underlying t (if P then f else g) (if P then f' else g') s
theory BCorres2_AI

lemma schedule_choose_new_thread_bcorres1:
  "BCorres2_AI TYPE(det_ext) \<Longrightarrow> bcorres schedule_choose_new_thread schedule" unfolding schedule_choose_new_thread_def apply (clarsimp simp: bcorres_underlying_def) apply (simp add: schedule_det_ext_ext_def s_bcorres_get_left
                   gets_def get_thread_state_def thread_get_def gets_the_def
                   bind_assoc get_before_assert_opt ethread_get_def schedule_switch_thread_fastfail_def
                   when_def) apply (rule conjI; clarsimp) apply (rule s_bcorres_underlying_split[where g'="\<lambda>_. return ()",
                  OF _ choose_thread_bcorres, simplified]
               s_bcorres_underlying_split[where f'="return ()", simplified]
         | fastforce simp: s_bcorres_underlying_def set_scheduler_action_def
                           when_def exec_gets simpler_modify_def return_def
                           next_domain_def Let_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. BCorres2_AI TYPE(det_ext) \<Longrightarrow> bcorres schedule_choose_new_thread schedule proof (prove)
goal (1 subgoal):
 1. BCorres2_AI TYPE(det_ext) \<Longrightarrow> bcorres (do dom_time <- gets domain_time;
when (dom_time = 0) next_domain;
choose_thread;
set_scheduler_action resume_cur_thread
od) schedule proof (prove)
goal (1 subgoal):
 1. \<And>s. BCorres2_AI TYPE(det_ext) \<Longrightarrow> s_bcorres (do dom_time <- gets domain_time;
y <- when (dom_time = 0) next_domain;
y <- choose_thread;
set_scheduler_action resume_cur_thread
od) schedule s proof (prove)
goal (1 subgoal):
 1. \<And>s. BCorres2_AI TYPE(det_ext) \<Longrightarrow> (domain_time s = 0 \<longrightarrow> s_bcorres (do y <- next_domain;
y <- choose_thread;
set_scheduler_action resume_cur_thread
od) schedule s) \<and> (domain_time s \<noteq> 0 \<longrightarrow> s_bcorres (do y <- choose_thread;
set_scheduler_action resume_cur_thread
od) schedule s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>BCorres2_AI TYPE(det_ext); domain_time s = 0\<rbrakk> \<Longrightarrow> s_bcorres (do y <- next_domain;
y <- choose_thread;
set_scheduler_action resume_cur_thread
od) schedule s
 2. \<And>s. \<lbrakk>BCorres2_AI TYPE(det_ext); domain_time s \<noteq> 0\<rbrakk> \<Longrightarrow> s_bcorres (do y <- choose_thread;
set_scheduler_action resume_cur_thread
od) schedule s proof (prove)
goal:
No subgoals!
theory ArchBCorres2_AI

lemma invoke_irq_control_bcorres[wp]: "bcorres (invoke_irq_control a) (invoke_irq_control a)" apply (cases a) apply wpsimp apply (rename_tac acap) apply (case_tac acap) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (invoke_irq_control a) (invoke_irq_control a) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13. a = IRQControl x11 x12 x13 \<Longrightarrow> bcorres (invoke_irq_control a) (invoke_irq_control a)
 2. \<And>x2. a = ArchIRQControl x2 \<Longrightarrow> bcorres (invoke_irq_control a) (invoke_irq_control a) proof (prove)
goal (1 subgoal):
 1. \<And>x2. a = ArchIRQControl x2 \<Longrightarrow> bcorres (invoke_irq_control a) (invoke_irq_control a) proof (prove)
goal (1 subgoal):
 1. \<And>acap. a = ArchIRQControl acap \<Longrightarrow> bcorres (invoke_irq_control a) (invoke_irq_control a) proof (prove)
goal (1 subgoal):
 1. \<And>acap x1 x2 x3 x4. \<lbrakk>a = ArchIRQControl acap; acap = ArchIRQControlIssue x1 x2 x3 x4\<rbrakk> \<Longrightarrow> bcorres (invoke_irq_control a) (invoke_irq_control a) proof (prove)
goal:
No subgoals!
theory ArchBCorres2_AI

lemma invoke_irq_handler_bcorres[wp]: "bcorres (invoke_irq_handler a) (invoke_irq_handler a)" apply (cases a) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (invoke_irq_handler a) (invoke_irq_handler a) proof (prove)
goal (3 subgoals):
 1. \<And>x1. a = ACKIrq x1 \<Longrightarrow> bcorres (invoke_irq_handler a) (invoke_irq_handler a)
 2. \<And>x21 x22 x23. a = SetIRQHandler x21 x22 x23 \<Longrightarrow> bcorres (invoke_irq_handler a) (invoke_irq_handler a)
 3. \<And>x3. a = ClearIRQHandler x3 \<Longrightarrow> bcorres (invoke_irq_handler a) (invoke_irq_handler a) proof (prove)
goal:
No subgoals!