theory ADT_IF

lemma handle_event_domain_fields:
  notes hy_inv[wp del]
  shows "\<lbrace>domain_fields P and K (e \<noteq> Interrupt)\<rbrace>
         handle_event e
         \<lbrace>\<lambda>_. domain_fields P\<rbrace>" apply (rule hoare_gen_asm) apply (rule hoare_pre) apply (case_tac e) apply (rename_tac syscall) apply (case_tac syscall) apply (wp | simp add: handle_call_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. P (domain_time s) (domain_index s) (domain_list s)) and K (e \<noteq> Interrupt)\<rbrace> handle_event e \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>\<lambda>s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace> handle_event e \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>?Q2\<rbrace> handle_event e \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 2. \<And>s. \<lbrakk>e \<noteq> Interrupt; P (domain_time s) (domain_index s) (domain_list s)\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (7 subgoals):
 1. \<And>x1. \<lbrakk>e \<noteq> Interrupt; e = SyscallEvent x1\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> handle_event e \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 2. \<And>x2. \<lbrakk>e \<noteq> Interrupt; e = UnknownSyscall x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> handle_event e \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 3. \<And>x31 x32. \<lbrakk>e \<noteq> Interrupt; e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> handle_event e \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 4. \<lbrakk>e \<noteq> Interrupt; e = Interrupt\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> handle_event e \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 5. \<And>x5. \<lbrakk>e \<noteq> Interrupt; e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> handle_event e \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 6. \<And>x6. \<lbrakk>e \<noteq> Interrupt; e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> handle_event e \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 7. \<And>s. \<lbrakk>e \<noteq> Interrupt; P (domain_time s) (domain_index s) (domain_list s)\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (7 subgoals):
 1. \<And>syscall. \<lbrakk>e \<noteq> Interrupt; e = SyscallEvent syscall\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> handle_event e \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 2. \<And>x2. \<lbrakk>e \<noteq> Interrupt; e = UnknownSyscall x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> handle_event e \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 3. \<And>x31 x32. \<lbrakk>e \<noteq> Interrupt; e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> handle_event e \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 4. \<lbrakk>e \<noteq> Interrupt; e = Interrupt\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> handle_event e \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 5. \<And>x5. \<lbrakk>e \<noteq> Interrupt; e = VMFaultEvent x5\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> handle_event e \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 6. \<And>x6. \<lbrakk>e \<noteq> Interrupt; e = HypervisorEvent x6\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> handle_event e \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 7. \<And>s. \<lbrakk>e \<noteq> Interrupt; P (domain_time s) (domain_index s) (domain_list s)\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (14 subgoals):
 1. \<And>syscall. \<lbrakk>e \<noteq> Interrupt; e = SyscallEvent syscall; syscall = SysCall\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> handle_event e \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 2. \<And>syscall. \<lbrakk>e \<noteq> Interrupt; e = SyscallEvent syscall; syscall = SysReplyRecv\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> handle_event e \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 3. \<And>syscall. \<lbrakk>e \<noteq> Interrupt; e = SyscallEvent syscall; syscall = SysSend\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> handle_event e \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 4. \<And>syscall. \<lbrakk>e \<noteq> Interrupt; e = SyscallEvent syscall; syscall = SysNBSend\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> handle_event e \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 5. \<And>syscall. \<lbrakk>e \<noteq> Interrupt; e = SyscallEvent syscall; syscall = SysRecv\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> handle_event e \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 6. \<And>syscall. \<lbrakk>e \<noteq> Interrupt; e = SyscallEvent syscall; syscall = SysReply\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> handle_event e \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 7. \<And>syscall. \<lbrakk>e \<noteq> Interrupt; e = SyscallEvent syscall; syscall = SysYield\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> handle_event e \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 8. \<And>syscall. \<lbrakk>e \<noteq> Interrupt; e = SyscallEvent syscall; syscall = SysNBRecv\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> handle_event e \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 9. \<And>x2. \<lbrakk>e \<noteq> Interrupt; e = UnknownSyscall x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> handle_event e \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 10. \<And>x31 x32. \<lbrakk>e \<noteq> Interrupt; e = UserLevelFault x31 x32\<rbrakk> \<Longrightarrow> \<lbrace>?Q2\<rbrace> handle_event e \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace>
A total of 14 subgoals... proof (prove)
goal:
No subgoals!