theory KHeap_R

lemma typ_at'_valid_obj'_lift:
  assumes P: "\<And>P T p. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>"
  notes [wp] = hoare_vcg_all_lift hoare_vcg_imp_lift hoare_vcg_const_Ball_lift typ_at_lifts [OF P]
  shows      "\<lbrace>\<lambda>s. valid_obj' obj s\<rbrace> f \<lbrace>\<lambda>rv s. valid_obj' obj s\<rbrace>" apply (cases obj; simp add: valid_obj'_def hoare_TrueI) apply (rename_tac endpoint) apply (case_tac endpoint; simp add: valid_ep'_def, wp) apply (rename_tac notification) apply (case_tac "ntfnObj notification";
             simp add: valid_ntfn'_def valid_bound_tcb'_def split: option.splits,
             (wpsimp|rule conjI)+) apply (rename_tac tcb) apply (case_tac "tcbState tcb";
           simp add: valid_tcb'_def valid_tcb_state'_def split_def valid_bound_ntfn'_def
              split: option.splits,
           wpsimp) apply (wpsimp simp: valid_cte'_def) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object; wpsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_obj' obj\<rbrace> f \<lbrace>\<lambda>rv. valid_obj' obj\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x1. obj = KOEndpoint x1 \<Longrightarrow> \<lbrace>valid_ep' x1\<rbrace> f \<lbrace>\<lambda>rv. valid_ep' x1\<rbrace>
 2. \<And>x2. obj = KONotification x2 \<Longrightarrow> \<lbrace>valid_ntfn' x2\<rbrace> f \<lbrace>\<lambda>rv. valid_ntfn' x2\<rbrace>
 3. \<And>x6. obj = KOTCB x6 \<Longrightarrow> \<lbrace>valid_tcb' x6\<rbrace> f \<lbrace>\<lambda>rv. valid_tcb' x6\<rbrace>
 4. \<And>x7. obj = KOCTE x7 \<Longrightarrow> \<lbrace>valid_cte' x7\<rbrace> f \<lbrace>\<lambda>rv. valid_cte' x7\<rbrace>
 5. \<And>x8. obj = KOArch x8 \<Longrightarrow> \<lbrace>valid_arch_obj' x8\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_obj' x8\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>endpoint. obj = KOEndpoint endpoint \<Longrightarrow> \<lbrace>valid_ep' endpoint\<rbrace> f \<lbrace>\<lambda>rv. valid_ep' endpoint\<rbrace>
 2. \<And>x2. obj = KONotification x2 \<Longrightarrow> \<lbrace>valid_ntfn' x2\<rbrace> f \<lbrace>\<lambda>rv. valid_ntfn' x2\<rbrace>
 3. \<And>x6. obj = KOTCB x6 \<Longrightarrow> \<lbrace>valid_tcb' x6\<rbrace> f \<lbrace>\<lambda>rv. valid_tcb' x6\<rbrace>
 4. \<And>x7. obj = KOCTE x7 \<Longrightarrow> \<lbrace>valid_cte' x7\<rbrace> f \<lbrace>\<lambda>rv. valid_cte' x7\<rbrace>
 5. \<And>x8. obj = KOArch x8 \<Longrightarrow> \<lbrace>valid_arch_obj' x8\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_obj' x8\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x2. obj = KONotification x2 \<Longrightarrow> \<lbrace>valid_ntfn' x2\<rbrace> f \<lbrace>\<lambda>rv. valid_ntfn' x2\<rbrace>
 2. \<And>x6. obj = KOTCB x6 \<Longrightarrow> \<lbrace>valid_tcb' x6\<rbrace> f \<lbrace>\<lambda>rv. valid_tcb' x6\<rbrace>
 3. \<And>x7. obj = KOCTE x7 \<Longrightarrow> \<lbrace>valid_cte' x7\<rbrace> f \<lbrace>\<lambda>rv. valid_cte' x7\<rbrace>
 4. \<And>x8. obj = KOArch x8 \<Longrightarrow> \<lbrace>valid_arch_obj' x8\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_obj' x8\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>notification. obj = KONotification notification \<Longrightarrow> \<lbrace>valid_ntfn' notification\<rbrace> f \<lbrace>\<lambda>rv. valid_ntfn' notification\<rbrace>
 2. \<And>x6. obj = KOTCB x6 \<Longrightarrow> \<lbrace>valid_tcb' x6\<rbrace> f \<lbrace>\<lambda>rv. valid_tcb' x6\<rbrace>
 3. \<And>x7. obj = KOCTE x7 \<Longrightarrow> \<lbrace>valid_cte' x7\<rbrace> f \<lbrace>\<lambda>rv. valid_cte' x7\<rbrace>
 4. \<And>x8. obj = KOArch x8 \<Longrightarrow> \<lbrace>valid_arch_obj' x8\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_obj' x8\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x6. obj = KOTCB x6 \<Longrightarrow> \<lbrace>valid_tcb' x6\<rbrace> f \<lbrace>\<lambda>rv. valid_tcb' x6\<rbrace>
 2. \<And>x7. obj = KOCTE x7 \<Longrightarrow> \<lbrace>valid_cte' x7\<rbrace> f \<lbrace>\<lambda>rv. valid_cte' x7\<rbrace>
 3. \<And>x8. obj = KOArch x8 \<Longrightarrow> \<lbrace>valid_arch_obj' x8\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_obj' x8\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. obj = KOTCB tcb \<Longrightarrow> \<lbrace>valid_tcb' tcb\<rbrace> f \<lbrace>\<lambda>rv. valid_tcb' tcb\<rbrace>
 2. \<And>x7. obj = KOCTE x7 \<Longrightarrow> \<lbrace>valid_cte' x7\<rbrace> f \<lbrace>\<lambda>rv. valid_cte' x7\<rbrace>
 3. \<And>x8. obj = KOArch x8 \<Longrightarrow> \<lbrace>valid_arch_obj' x8\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_obj' x8\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x7. obj = KOCTE x7 \<Longrightarrow> \<lbrace>valid_cte' x7\<rbrace> f \<lbrace>\<lambda>rv. valid_cte' x7\<rbrace>
 2. \<And>x8. obj = KOArch x8 \<Longrightarrow> \<lbrace>valid_arch_obj' x8\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_obj' x8\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x8. obj = KOArch x8 \<Longrightarrow> \<lbrace>valid_arch_obj' x8\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_obj' x8\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>arch_kernel_object. obj = KOArch arch_kernel_object \<Longrightarrow> \<lbrace>valid_arch_obj' arch_kernel_object\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_obj' arch_kernel_object\<rbrace> proof (prove)
goal:
No subgoals!