theory Finalise_AI

lemma unbind_notification_not_bound:
  "\<lbrace>\<lambda>s. obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = Some tcbptr) ntfnptr s
      \<and> valid_objs s \<and> sym_refs (state_refs_of s)\<rbrace>
     unbind_notification tcbptr
   \<lbrace>\<lambda>_. obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None) ntfnptr\<rbrace>" apply (simp add: unbind_notification_def) apply (rule hoare_pre) apply (rule hoare_seq_ext[OF _ gbn_wp[where P="\<lambda>ptr _. ptr = (Some ntfnptr)"]]) apply (rule hoare_gen_asm[where P'=\<top>, simplified]) apply (wp sbn_obj_at_impossible simple_obj_set_prop_at | wpc | simp)+ apply (clarsimp simp: obj_at_def) apply (rule valid_objsE, simp+) apply (drule_tac P="(=) (Some ntfnptr)" in ntfn_bound_tcb_at, simp+) apply (auto simp: obj_at_def valid_obj_def is_tcb valid_ntfn_def pred_tcb_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = Some tcbptr) ntfnptr s \<and> valid_objs s \<and> sym_refs (state_refs_of s)\<rbrace> unbind_notification tcbptr \<lbrace>\<lambda>_. obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None) ntfnptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = Some tcbptr) ntfnptr s \<and> valid_objs s \<and> sym_refs (state_refs_of s)\<rbrace> do ntfnptr <- get_bound_notification tcbptr;
case ntfnptr of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
do_unbind_notification ntfnptr' ntfn tcbptr
od
od \<lbrace>\<lambda>_. obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None) ntfnptr\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do ntfnptr <- get_bound_notification tcbptr;
case ntfnptr of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
do_unbind_notification ntfnptr' ntfn tcbptr
od
od \<lbrace>\<lambda>_. obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None) ntfnptr\<rbrace>
 2. \<And>s. obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = Some tcbptr) ntfnptr s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>ntfnptra. \<lbrace>\<lambda>_. ntfnptra = Some ntfnptr\<rbrace> case ntfnptra of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
do_unbind_notification ntfnptr' ntfn tcbptr
od \<lbrace>\<lambda>_. obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None) ntfnptr\<rbrace>
 2. \<And>s. obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = Some tcbptr) ntfnptr s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<Longrightarrow> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_bound_notification tcb = Some ntfnptr) tcbptr s proof (prove)
goal (2 subgoals):
 1. \<And>ntfnptra. ntfnptra = Some ntfnptr \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case ntfnptra of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
do_unbind_notification ntfnptr' ntfn tcbptr
od \<lbrace>\<lambda>_. obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None) ntfnptr\<rbrace>
 2. \<And>s. obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = Some tcbptr) ntfnptr s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<Longrightarrow> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_bound_notification tcb = Some ntfnptr) tcbptr s proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = Some tcbptr) ntfnptr s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<Longrightarrow> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_bound_notification tcb = Some ntfnptr) tcbptr s proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn. \<lbrakk>valid_objs s; sym_refs (state_refs_of s); kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some tcbptr\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s tcbptr = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> tcb_bound_notification tcb = Some ntfnptr) proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn. \<lbrakk>valid_objs s; sym_refs (state_refs_of s); kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some tcbptr; valid_obj ntfnptr (Notification ntfn) s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s tcbptr = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> tcb_bound_notification tcb = Some ntfnptr) proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn. \<lbrakk>valid_objs s; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some tcbptr; valid_obj ntfnptr (Notification ntfn) s; bound_tcb_at ((=) (Some ntfnptr)) tcbptr s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s tcbptr = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> tcb_bound_notification tcb = Some ntfnptr) proof (prove)
goal:
No subgoals!