kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchDetSchedSchedule_AI

lemma switch_to_idle_thread_ct_not_in_q [wp, DetSchedSchedule_AI_assms]:
  "\<lbrace>valid_queues and valid_idle\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>_. ct_not_in_q\<rbrace>" apply (simp add: switch_to_idle_thread_def) apply wp apply (simp add: arch_switch_to_idle_thread_def) apply wp+ apply (fastforce simp: valid_queues_def ct_not_in_q_def not_queued_def
                         valid_idle_def pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues and valid_idle\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>_. ct_not_in_q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues and valid_idle\<rbrace> do thread <- gets idle_thread;
y <- arch_switch_to_idle_thread;
modify (cur_thread_update (\<lambda>_. thread))
od \<lbrace>\<lambda>_. ct_not_in_q\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>thread. \<lbrace>?B1 thread\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>y s. ct_not_in_q (s\<lparr>cur_thread := thread\<rparr>)\<rbrace>
 2. \<lbrace>?Q\<rbrace> gets idle_thread \<lbrace>?B1\<rbrace>
 3. \<And>s. (valid_queues and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>thread. \<lbrace>?B1 thread\<rbrace> gets idle_thread >>= set_vm_root \<lbrace>\<lambda>y s. ct_not_in_q_2 (ready_queues s) (scheduler_action s) thread\<rbrace>
 2. \<lbrace>?Q\<rbrace> gets idle_thread \<lbrace>?B1\<rbrace>
 3. \<And>s. (valid_queues and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_queues and valid_idle) s \<Longrightarrow> ct_not_in_q_2 (ready_queues s) (scheduler_action s) (idle_thread s) proof (prove)
goal:
No subgoals!
theory ArchDetSchedSchedule_AI

lemma switch_to_idle_thread_valid_sched_action [wp, DetSchedSchedule_AI_assms]:
  "\<lbrace>valid_sched_action and valid_idle\<rbrace>
     switch_to_idle_thread
   \<lbrace>\<lambda>_. valid_sched_action\<rbrace>" apply (simp add: switch_to_idle_thread_def) apply wp apply (simp add: arch_switch_to_idle_thread_def do_machine_op_def split_def) apply wp+ apply (clarsimp simp: valid_sched_action_def valid_idle_def is_activatable_def
                        pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched_action and valid_idle\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>_. valid_sched_action\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched_action and valid_idle\<rbrace> do thread <- gets idle_thread;
y <- arch_switch_to_idle_thread;
modify (cur_thread_update (\<lambda>_. thread))
od \<lbrace>\<lambda>_. valid_sched_action\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>thread. \<lbrace>?B1 thread\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>y s. valid_sched_action (s\<lparr>cur_thread := thread\<rparr>)\<rbrace>
 2. \<lbrace>?Q\<rbrace> gets idle_thread \<lbrace>?B1\<rbrace>
 3. \<And>s. (valid_sched_action and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>thread. \<lbrace>?B1 thread\<rbrace> gets idle_thread >>= set_vm_root \<lbrace>\<lambda>y s. valid_sched_action_2 (scheduler_action s) (ekheap s) (kheap s) thread (cur_domain s)\<rbrace>
 2. \<lbrace>?Q\<rbrace> gets idle_thread \<lbrace>?B1\<rbrace>
 3. \<And>s. (valid_sched_action and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_sched_action and valid_idle) s \<Longrightarrow> valid_sched_action_2 (scheduler_action s) (ekheap s) (kheap s) (idle_thread s) (cur_domain s) proof (prove)
goal:
No subgoals!
theory ArchDetSchedSchedule_AI

lemma switch_to_idle_thread_ct_in_cur_domain [wp, DetSchedSchedule_AI_assms]:
  "\<lbrace>\<top>\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace>" by (simp add: switch_to_idle_thread_def arch_switch_to_idle_thread_def do_machine_op_def
                split_def
      | wp
      | simp add: ct_in_cur_domain_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace>
theory ArchDetSchedSchedule_AI

lemma set_vm_root_valid_blocked_ct_in_q [wp]:
  "\<lbrace>valid_blocked and ct_in_q\<rbrace> set_vm_root p \<lbrace>\<lambda>_. valid_blocked and ct_in_q\<rbrace>" by (wp | wpc | auto)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked and ct_in_q\<rbrace> set_vm_root p \<lbrace>\<lambda>_. valid_blocked and ct_in_q\<rbrace>
theory ArchDetSchedSchedule_AI

lemma arch_switch_to_thread_valid_blocked [wp, DetSchedSchedule_AI_assms]:
  "\<lbrace>valid_blocked and ct_in_q\<rbrace> arch_switch_to_thread thread \<lbrace>\<lambda>_. valid_blocked and ct_in_q\<rbrace>" apply (simp add: arch_switch_to_thread_def) apply (rule hoare_seq_ext)+ apply (rule do_machine_op_valid_blocked) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked and ct_in_q\<rbrace> arch_switch_to_thread thread \<lbrace>\<lambda>_. valid_blocked and ct_in_q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked and ct_in_q\<rbrace> do y <- set_vm_root thread;
do_machine_op clearExMonitor
od \<lbrace>\<lambda>_. valid_blocked and ct_in_q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrace>?B y\<rbrace> do_machine_op clearExMonitor \<lbrace>\<lambda>_. valid_blocked and ct_in_q\<rbrace>
 2. \<lbrace>valid_blocked and ct_in_q\<rbrace> set_vm_root thread \<lbrace>?B\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked and ct_in_q\<rbrace> set_vm_root thread \<lbrace>\<lambda>y. valid_blocked and ct_in_q\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchDetSchedSchedule_AI

lemma switch_to_idle_thread_valid_blocked [wp, DetSchedSchedule_AI_assms]:
  "\<lbrace>valid_blocked and ct_in_q\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>rv. valid_blocked\<rbrace>" apply (simp add: switch_to_idle_thread_def arch_switch_to_idle_thread_def do_machine_op_def | wp | wpc)+ apply clarsimp apply (drule(1) ct_in_q_valid_blocked_ct_upd) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked and ct_in_q\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>rv. valid_blocked\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_blocked s \<and> ct_in_q s \<Longrightarrow> valid_blocked_2 (ready_queues s) (kheap s) (scheduler_action s) (idle_thread s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_blocked s; ct_in_q s\<rbrakk> \<Longrightarrow> valid_blocked_2 (ready_queues s) (kheap s) (scheduler_action s) (idle_thread s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_blocked s; valid_blocked (s\<lparr>cur_thread := ?thread15 s\<rparr>)\<rbrakk> \<Longrightarrow> valid_blocked_2 (ready_queues s) (kheap s) (scheduler_action s) (idle_thread s) proof (prove)
goal:
No subgoals!
theory ArchDetSchedSchedule_AI

lemma astit_st_tcb_at[wp]:
  "\<lbrace>st_tcb_at P t\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>" apply (simp add: arch_switch_to_idle_thread_def) by (wpsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at P t\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at P t\<rbrace> gets idle_thread >>= set_vm_root \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>
theory ArchDetSchedSchedule_AI

lemma stit_activatable' [DetSchedSchedule_AI_assms]:
  "\<lbrace>valid_idle\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>rv . ct_in_state activatable\<rbrace>" apply (simp add: switch_to_idle_thread_def ct_in_state_def do_machine_op_def split_def) apply wpsimp apply (clarsimp simp: valid_idle_def ct_in_state_def pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>rv. ct_in_state activatable\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle\<rbrace> do thread <- gets idle_thread;
y <- arch_switch_to_idle_thread;
modify (cur_thread_update (\<lambda>_. thread))
od \<lbrace>\<lambda>rv s. st_tcb_at activatable (cur_thread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_idle s \<Longrightarrow> st_tcb_at activatable (idle_thread s) s proof (prove)
goal:
No subgoals!
theory ArchDetSchedSchedule_AI

lemma switch_to_idle_thread_cur_thread_idle_thread [wp, DetSchedSchedule_AI_assms]:
  "\<lbrace>\<top>\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>_ s. cur_thread s = idle_thread s\<rbrace>" by (wp | simp add:switch_to_idle_thread_def arch_switch_to_idle_thread_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>_ s. cur_thread s = idle_thread s\<rbrace>
theory ArchDetSchedSchedule_AI

lemma set_pd_valid_etcbs[wp]:
  "\<lbrace>valid_etcbs\<rbrace> set_pd ptr pd \<lbrace>\<lambda>rv. valid_etcbs\<rbrace>" by (wp hoare_drop_imps valid_etcbs_lift | simp add: set_pd_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> set_pd ptr pd \<lbrace>\<lambda>rv. valid_etcbs\<rbrace>
theory ArchDetSchedSchedule_AI

lemma set_pt_valid_etcbs[wp]:
  "\<lbrace>valid_etcbs\<rbrace> set_pt ptr pt \<lbrace>\<lambda>rv. valid_etcbs\<rbrace>" by (wp hoare_drop_imps valid_etcbs_lift | simp add: set_pt_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> set_pt ptr pt \<lbrace>\<lambda>rv. valid_etcbs\<rbrace>
theory ArchDetSchedSchedule_AI

lemma set_asid_pool_valid_etcbs[wp]:
  "\<lbrace>valid_etcbs\<rbrace> set_asid_pool ptr pool \<lbrace>\<lambda>rv. valid_etcbs\<rbrace>" by (wp hoare_drop_imps valid_etcbs_lift | simp add: set_asid_pool_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> set_asid_pool ptr pool \<lbrace>\<lambda>rv. valid_etcbs\<rbrace>
theory ArchDetSchedSchedule_AI

lemma set_pt_valid_sched[wp]:
  "\<lbrace>valid_sched\<rbrace> set_pt ptr pt \<lbrace>\<lambda>rv. valid_sched\<rbrace>" by (wp hoare_drop_imps valid_sched_lift | simp add: set_pt_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> set_pt ptr pt \<lbrace>\<lambda>rv. valid_sched\<rbrace>
theory ArchDetSchedSchedule_AI

lemma set_pd_valid_sched[wp]:
  "\<lbrace>valid_sched\<rbrace> set_pd ptr pd \<lbrace>\<lambda>rv. valid_sched\<rbrace>" by (wp hoare_drop_imps valid_sched_lift | simp add: set_pd_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> set_pd ptr pd \<lbrace>\<lambda>rv. valid_sched\<rbrace>
theory ArchDetSchedSchedule_AI

lemma set_asid_pool_valid_sched[wp]:
  "\<lbrace>valid_sched\<rbrace> set_asid_pool ptr pool \<lbrace>\<lambda>rv. valid_sched\<rbrace>" by (wp hoare_drop_imps valid_sched_lift | simp add: set_asid_pool_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> set_asid_pool ptr pool \<lbrace>\<lambda>rv. valid_sched\<rbrace>
theory ArchDetSchedSchedule_AI

lemma activate_thread_valid_sched [DetSchedSchedule_AI_assms]:
  "\<lbrace>valid_sched\<rbrace> activate_thread \<lbrace>\<lambda>_. valid_sched\<rbrace>" apply (simp add: activate_thread_def) apply (wp set_thread_state_runnable_valid_sched gts_wp | wpc | simp add: arch_activate_idle_thread_def)+ apply (force elim: st_tcb_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> activate_thread \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> do thread <- gets cur_thread;
state <- get_thread_state thread;
case state of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user thread getRestartPC;
as_user thread $ setNextPC pc;
set_thread_state thread Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread thread | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_sched s \<Longrightarrow> st_tcb_at ((=) Restart) (cur_thread s) s \<longrightarrow> st_tcb_at runnable (cur_thread s) s proof (prove)
goal:
No subgoals!
theory ArchDetSchedSchedule_AI

lemma arch_perform_invocation_valid_sched [wp, DetSchedSchedule_AI_assms]:
  "\<lbrace>invs and valid_sched and ct_active and valid_arch_inv a\<rbrace>
     arch_perform_invocation a
   \<lbrace>\<lambda>_.valid_sched\<rbrace>" apply (cases a, simp_all add: arch_perform_invocation_def) apply (wp perform_asid_control_invocation_valid_sched | wpc |
            simp add: valid_arch_inv_def invs_valid_idle)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_sched and ct_active and valid_arch_inv a\<rbrace> arch_perform_invocation a \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x1. a = InvokePageTable x1 \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and valid_arch_inv (InvokePageTable x1)\<rbrace> liftE (do y <- perform_page_table_invocation x1;
return []
od) \<lbrace>\<lambda>_. valid_sched\<rbrace>
 2. \<And>x2. a = InvokePageDirectory x2 \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and valid_arch_inv (InvokePageDirectory x2)\<rbrace> liftE (do y <- perform_page_directory_invocation x2;
return []
od) \<lbrace>\<lambda>_. valid_sched\<rbrace>
 3. \<And>x3. a = InvokePage x3 \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and valid_arch_inv (InvokePage x3)\<rbrace> liftE (perform_page_invocation x3) \<lbrace>\<lambda>_. valid_sched\<rbrace>
 4. \<And>x4. a = InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and valid_arch_inv (InvokeASIDControl x4)\<rbrace> liftE (do y <- perform_asid_control_invocation x4;
return []
od) \<lbrace>\<lambda>_. valid_sched\<rbrace>
 5. \<And>x5. a = InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs and valid_sched and ct_active and valid_arch_inv (InvokeASIDPool x5)\<rbrace> liftE (do y <- perform_asid_pool_invocation x5;
return []
od) \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchDetSchedSchedule_AI

lemma hvmf_st_tcb_at [wp, DetSchedSchedule_AI_assms]:
  "\<lbrace>st_tcb_at P t' \<rbrace> handle_vm_fault t w \<lbrace>\<lambda>rv. st_tcb_at P t' \<rbrace>" by (cases w, simp_all) ((wp | simp)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at P t'\<rbrace> handle_vm_fault t w \<lbrace>\<lambda>rv. st_tcb_at P t'\<rbrace>
theory ArchDetSchedSchedule_AI

lemma handle_vm_fault_st_tcb_cur_thread [wp, DetSchedSchedule_AI_assms]:
  "\<lbrace> \<lambda>s. st_tcb_at P (cur_thread s) s \<rbrace> handle_vm_fault t f \<lbrace>\<lambda>_ s. st_tcb_at P (cur_thread s) s \<rbrace>" apply (fold ct_in_state_def) apply (rule ct_in_state_thread_state_lift) apply (cases f) apply (wp|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. st_tcb_at P (cur_thread s) s\<rbrace> handle_vm_fault t f \<lbrace>\<lambda>_ s. st_tcb_at P (cur_thread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_state P\<rbrace> handle_vm_fault t f \<lbrace>\<lambda>_. ct_in_state P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> handle_vm_fault t f \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace>
 2. \<And>ta. \<lbrace>st_tcb_at P ta\<rbrace> handle_vm_fault t f \<lbrace>\<lambda>_. st_tcb_at P ta\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>P. f = ARMDataAbort \<Longrightarrow> \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> handle_vm_fault t f \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace>
 2. \<And>P. f = ARMPrefetchAbort \<Longrightarrow> \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> handle_vm_fault t f \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace>
 3. \<And>ta. \<lbrace>st_tcb_at P ta\<rbrace> handle_vm_fault t f \<lbrace>\<lambda>_. st_tcb_at P ta\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchDetSchedSchedule_AI

lemma arch_post_modify_registers_not_idle_thread[DetSchedSchedule_AI_assms]:
  "\<lbrace>\<lambda>s::det_ext state. t \<noteq> idle_thread s\<rbrace> arch_post_modify_registers c t \<lbrace>\<lambda>_ s. t \<noteq> idle_thread s\<rbrace>" by (wpsimp simp: arch_post_modify_registers_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. t \<noteq> idle_thread s\<rbrace> arch_post_modify_registers c t \<lbrace>\<lambda>_ s. t \<noteq> idle_thread s\<rbrace>
theory ArchDetSchedSchedule_AI

lemma handle_reserved_irq_valid_sched:
  "\<lbrace>valid_sched and invs and (\<lambda>s. irq \<in> non_kernel_IRQs \<longrightarrow>  scheduler_act_sane s \<and> ct_not_queued s)\<rbrace>
  handle_reserved_irq irq \<lbrace>\<lambda>rv. valid_sched\<rbrace>" unfolding handle_reserved_irq_def by (wpsimp simp: non_kernel_IRQs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and invs and (\<lambda>s. irq \<in> non_kernel_IRQs \<longrightarrow> scheduler_act_sane s \<and> ct_not_queued s)\<rbrace> handle_reserved_irq irq \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and invs and (\<lambda>s. irq \<in> non_kernel_IRQs \<longrightarrow> scheduler_act_sane s \<and> ct_not_queued s)\<rbrace> return () \<lbrace>\<lambda>rv. valid_sched\<rbrace>
theory Corres_Cases

lemma corres_case_helperI:
  "corres_case_helper (P, P') (P, P') R \<Longrightarrow> R" by (simp add: corres_case_helper_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_case_helper (P, P') (P, P') R \<Longrightarrow> R
theory Corres_Cases

lemma corres_case_conj_process:
  "\<lbrakk> corres_case_helper (P, P') (A, A') R; corres_case_helper (P, P') (B, B') S \<rbrakk>
   \<Longrightarrow> corres_case_helper (P, P') (\<lambda>s. A s \<and> B s, \<lambda>s. A' s \<and> B' s) (R \<and> S)" by (clarsimp simp add: corres_case_helper_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_case_helper (P, P') (A, A') R; corres_case_helper (P, P') (B, B') S\<rbrakk> \<Longrightarrow> corres_case_helper (P, P') (\<lambda>s. A s \<and> B s, \<lambda>s. A' s \<and> B' s) (R \<and> S)
theory Corres_Cases

lemma corres_case_all_process:
  "\<lbrakk> \<And>x. corres_case_helper (P, P') (Q x, Q' x) (R x) \<rbrakk>
   \<Longrightarrow> corres_case_helper (P, P') (\<lambda>s. \<forall>x. Q x s, \<lambda>s. \<forall>x. Q' x s) (\<forall>x. R x)" by (clarsimp simp: corres_case_helper_def subset_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. corres_case_helper (P, P') (Q x, Q' x) (R x)) \<Longrightarrow> corres_case_helper (P, P') (\<lambda>s. \<forall>x. Q x s, \<lambda>s. \<forall>x. Q' x s) (\<forall>x. R x)
theory Corres_Cases

lemma corres_case_all_process_weak:
  "\<lbrakk> \<And>x. corres_case_helper (P, P') (Q x, Q') (R x) \<rbrakk>
   \<Longrightarrow> corres_case_helper (P, P') (\<lambda>s. \<forall>x. Q x s, Q') (\<forall>x. R x)" by (clarsimp simp: corres_case_helper_def subset_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. corres_case_helper (P, P') (Q x, Q') (R x)) \<Longrightarrow> corres_case_helper (P, P') (\<lambda>s. \<forall>x. Q x s, Q') (\<forall>x. R x)
theory Corres_Cases

lemma corres_case_imp_process_weak:
  "\<lbrakk> S \<Longrightarrow> corres_case_helper (P, P') (Q, Q') R \<rbrakk>
   \<Longrightarrow> corres_case_helper (P, P') (\<lambda>s. S \<longrightarrow> Q s, Q') (S \<longrightarrow> R)" by (clarsimp simp add: corres_case_helper_def subset_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (S \<Longrightarrow> corres_case_helper (P, P') (Q, Q') R) \<Longrightarrow> corres_case_helper (P, P') (\<lambda>s. S \<longrightarrow> Q s, Q') (S \<longrightarrow> R)
theory Corres_Cases

lemma corres_case_helper_corres_left:
  "corres_underlying sr nf nf' r Q Q' f f' \<Longrightarrow>
    corres_case_helper (P, P') (Q, Q') (corres_underlying sr nf nf' r P P' f f')" by (auto simp: corres_case_helper_def elim!: corres_guard_imp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r Q Q' f f' \<Longrightarrow> corres_case_helper (P, P') (Q, Q') (corres_underlying sr nf nf' r P P' f f')
theory Corres_Cases

lemma corres_case_helper_corres_right:
  "corres_underlying sr nf nf' r Q' Q f f' \<Longrightarrow>
    corres_case_helper (P, P') (Q, Q') (corres_underlying sr nf nf' r P' P f f')" by (auto simp: corres_case_helper_def elim!: corres_guard_imp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r Q' Q f f' \<Longrightarrow> corres_case_helper (P, P') (Q, Q') (corres_underlying sr nf nf' r P' P f f')
theory Corres_Cases

lemma "corres_underlying srel nf nf' rrel G G' ((case x of None \<Rightarrow> a | Some y \<Rightarrow> b y) >>=E g) m" apply corres_cases oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying srel nf nf' rrel G G' ((case x of None \<Rightarrow> a | Some y \<Rightarrow> b y) >>=E g) m proof (prove)
goal (4 subgoals):
 1. x = None \<Longrightarrow> corres_underlying srel nf nf' rrel ?Q38 ?Q'40 (a >>=E g) m
 2. \<And>x2. x = Some x2 \<Longrightarrow> corres_underlying srel nf nf' rrel (?Q39 x2) (?Q'41 x2) (b x2 >>=E g) m
 3. \<And>s s'. \<lbrakk>G s; G' s'; (s, s') \<in> srel\<rbrakk> \<Longrightarrow> (x = None \<longrightarrow> ?Q38 s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?Q39 xa s)
 4. \<And>s s'. \<lbrakk>G s; G' s'; (s, s') \<in> srel\<rbrakk> \<Longrightarrow> (x = None \<longrightarrow> ?Q'40 s') \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?Q'41 xa s')
theory Corres_Cases

lemma "corres_underlying srel nf nf' rrel G G' m (case x of None \<Rightarrow> a | Some y \<Rightarrow> b y)" apply corres_cases oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying srel nf nf' rrel G G' m (case x of None \<Rightarrow> a | Some y \<Rightarrow> b y) proof (prove)
goal (4 subgoals):
 1. x = None \<Longrightarrow> corres_underlying srel nf nf' rrel ?Q'38 ?Q40 m a
 2. \<And>x2. x = Some x2 \<Longrightarrow> corres_underlying srel nf nf' rrel (?Q'39 x2) (?Q41 x2) m (b x2)
 3. \<And>s s'. \<lbrakk>G s; G' s'; (s, s') \<in> srel\<rbrakk> \<Longrightarrow> (x = None \<longrightarrow> ?Q'38 s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?Q'39 xa s)
 4. \<And>s s'. \<lbrakk>G s; G' s'; (s, s') \<in> srel\<rbrakk> \<Longrightarrow> (x = None \<longrightarrow> ?Q40 s') \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?Q41 xa s')
theory Corres_Cases

lemma "corres_underlying srel nf nf' rrel G G' m ((case x of None \<Rightarrow> a | Some y \<Rightarrow> b y) >>= g)" apply corres_cases oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying srel nf nf' rrel G G' m ((case x of None \<Rightarrow> a | Some y \<Rightarrow> b y) >>= g) proof (prove)
goal (4 subgoals):
 1. x = None \<Longrightarrow> corres_underlying srel nf nf' rrel ?Q'38 ?Q40 m (a >>= g)
 2. \<And>x2. x = Some x2 \<Longrightarrow> corres_underlying srel nf nf' rrel (?Q'39 x2) (?Q41 x2) m (b x2 >>= g)
 3. \<And>s s'. \<lbrakk>G s; G' s'; (s, s') \<in> srel\<rbrakk> \<Longrightarrow> (x = None \<longrightarrow> ?Q'38 s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?Q'39 xa s)
 4. \<And>s s'. \<lbrakk>G s; G' s'; (s, s') \<in> srel\<rbrakk> \<Longrightarrow> (x = None \<longrightarrow> ?Q40 s') \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?Q41 xa s')