theory ArchAcc_AI

lemma simpler_set_pt_def:
  "set_pt p pt =
   (\<lambda>s. if \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) then
           ({((), s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)}, False)
        else ({}, True))" apply (rule ext) apply (clarsimp simp: set_pt_def set_object_def get_object_def assert_def
                        put_def get_def simpler_gets_def bind_def return_def fail_def) apply (rule conjI) apply (clarsimp simp: set_pt_def set_object_def get_object_def assert_def
                         put_def get_def simpler_gets_def bind_def
                         return_def fail_def a_type_def
                  split: kernel_object.splits
                         arch_kernel_obj.splits) using a_type_def aa_type_APageTableE apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_pt p pt = (\<lambda>s. if \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) then ({((), s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)}, False) else ({}, True)) proof (prove)
goal (1 subgoal):
 1. \<And>s. set_pt p pt s = (if \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) then ({((), s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)}, False) else ({}, True)) proof (prove)
goal (1 subgoal):
 1. \<And>s. (a_type (the (kheap s p)) = a_type (ArchObj (PageTable pt)) \<longrightarrow> (\<exists>y. kheap s p = Some y) \<longrightarrow> (\<exists>pt. kheap s p = Some (ArchObj (PageTable pt)))) \<and> (a_type (the (kheap s p)) \<noteq> a_type (ArchObj (PageTable pt)) \<longrightarrow> (\<exists>y. kheap s p = Some y) \<longrightarrow> (\<forall>pt. kheap s p \<noteq> Some (ArchObj (PageTable pt)))) proof (prove)
goal (2 subgoals):
 1. \<And>s. a_type (the (kheap s p)) = a_type (ArchObj (PageTable pt)) \<longrightarrow> (\<exists>y. kheap s p = Some y) \<longrightarrow> (\<exists>pt. kheap s p = Some (ArchObj (PageTable pt)))
 2. \<And>s. a_type (the (kheap s p)) \<noteq> a_type (ArchObj (PageTable pt)) \<longrightarrow> (\<exists>y. kheap s p = Some y) \<longrightarrow> (\<forall>pt. kheap s p \<noteq> Some (ArchObj (PageTable pt))) proof (prove)
goal (1 subgoal):
 1. \<And>s. a_type (the (kheap s p)) \<noteq> a_type (ArchObj (PageTable pt)) \<longrightarrow> (\<exists>y. kheap s p = Some y) \<longrightarrow> (\<forall>pt. kheap s p \<noteq> Some (ArchObj (PageTable pt))) proof (prove)
using this:
a_type ?ob \<equiv> case ?ob of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)
\<lbrakk>a_type ?ko = AArch APageTable; \<And>pt. ?ko = ArchObj (PageTable pt) \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R

goal (1 subgoal):
 1. \<And>s. a_type (the (kheap s p)) \<noteq> a_type (ArchObj (PageTable pt)) \<longrightarrow> (\<exists>y. kheap s p = Some y) \<longrightarrow> (\<forall>pt. kheap s p \<noteq> Some (ArchObj (PageTable pt))) proof (prove)
goal:
No subgoals!