theory Invariants_AI

lemma cte_at_typ:
  "cte_at p = (\<lambda>s. typ_at (ACapTable (length (snd p))) (fst p) s
                \<or> (typ_at ATCB (fst p) s \<and> snd p \<in> dom tcb_cap_cases))" apply (rule ext) apply (simp add: cte_at_cases obj_at_def) apply (rule arg_cong2[where f="(\<or>)"]) apply (safe, simp_all add: a_type_def DomainI) apply (clarsimp simp add: a_type_def well_formed_cnode_n_def length_set_helper) apply (drule_tac m="fun" in domI) apply simp apply (case_tac ko, simp_all) apply (simp add: well_formed_cnode_n_def length_set_helper split: if_split_asm) apply (case_tac ko, simp_all split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at (\<lambda>_. True) p = (\<lambda>s. typ_at (ACapTable (length (snd p))) (fst p) s \<or> typ_at ATCB (fst p) s \<and> snd p \<in> dom tcb_cap_cases) proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at (\<lambda>_. True) p s = (typ_at (ACapTable (length (snd p))) (fst p) s \<or> typ_at ATCB (fst p) s \<and> snd p \<in> dom tcb_cap_cases) proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<exists>sz fun. kheap s (fst p) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> snd p \<in> dom fun) \<or> (\<exists>tcb. kheap s (fst p) = Some (TCB tcb)) \<and> snd p \<in> dom tcb_cap_cases) = ((\<exists>ko. kheap s (fst p) = Some ko \<and> a_type ko = ACapTable (length (snd p))) \<or> (\<exists>ko. kheap s (fst p) = Some ko \<and> a_type ko = ATCB) \<and> snd p \<in> dom tcb_cap_cases) proof (prove)
goal (2 subgoals):
 1. \<And>s. (\<exists>sz fun. kheap s (fst p) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> snd p \<in> dom fun) = (\<exists>ko. kheap s (fst p) = Some ko \<and> a_type ko = ACapTable (length (snd p)))
 2. \<And>s. ((\<exists>tcb. kheap s (fst p) = Some (TCB tcb)) \<and> snd p \<in> dom tcb_cap_cases) = ((\<exists>ko. kheap s (fst p) = Some ko \<and> a_type ko = ATCB) \<and> snd p \<in> dom tcb_cap_cases) proof (prove)
goal (3 subgoals):
 1. \<And>s sz fun y. \<lbrakk>kheap s (fst p) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd p) = Some y\<rbrakk> \<Longrightarrow> sz = length (snd p)
 2. \<And>s ko. \<lbrakk>kheap s (fst p) = Some ko; (case ko 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 (aa_type ao)) = ACapTable (length (snd p))\<rbrakk> \<Longrightarrow> \<exists>sz fun. ko = CNode sz fun \<and> well_formed_cnode_n sz fun \<and> snd p \<in> dom fun
 3. \<And>s ko a aa b. \<lbrakk>tcb_cap_cases (snd p) = Some (a, aa, b); kheap s (fst p) = Some ko; (case ko 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 (aa_type ao)) = ATCB\<rbrakk> \<Longrightarrow> \<exists>tcb. ko = TCB tcb proof (prove)
goal (3 subgoals):
 1. \<And>s sz fun y. \<lbrakk>kheap s (fst p) = Some (CNode sz fun); dom fun = {x. length x = sz}; fun (snd p) = Some y\<rbrakk> \<Longrightarrow> sz = length (snd p)
 2. \<And>s ko. \<lbrakk>kheap s (fst p) = Some ko; (case ko 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 (aa_type ao)) = ACapTable (length (snd p))\<rbrakk> \<Longrightarrow> \<exists>sz fun. ko = CNode sz fun \<and> well_formed_cnode_n sz fun \<and> snd p \<in> dom fun
 3. \<And>s ko a aa b. \<lbrakk>tcb_cap_cases (snd p) = Some (a, aa, b); kheap s (fst p) = Some ko; (case ko 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 (aa_type ao)) = ATCB\<rbrakk> \<Longrightarrow> \<exists>tcb. ko = TCB tcb proof (prove)
goal (3 subgoals):
 1. \<And>s sz fun y. \<lbrakk>kheap s (fst p) = Some (CNode sz fun); dom fun = {x. length x = sz}; snd p \<in> dom fun\<rbrakk> \<Longrightarrow> sz = length (snd p)
 2. \<And>s ko. \<lbrakk>kheap s (fst p) = Some ko; (case ko 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 (aa_type ao)) = ACapTable (length (snd p))\<rbrakk> \<Longrightarrow> \<exists>sz fun. ko = CNode sz fun \<and> well_formed_cnode_n sz fun \<and> snd p \<in> dom fun
 3. \<And>s ko a aa b. \<lbrakk>tcb_cap_cases (snd p) = Some (a, aa, b); kheap s (fst p) = Some ko; (case ko 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 (aa_type ao)) = ATCB\<rbrakk> \<Longrightarrow> \<exists>tcb. ko = TCB tcb proof (prove)
goal (2 subgoals):
 1. \<And>s ko. \<lbrakk>kheap s (fst p) = Some ko; (case ko 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 (aa_type ao)) = ACapTable (length (snd p))\<rbrakk> \<Longrightarrow> \<exists>sz fun. ko = CNode sz fun \<and> well_formed_cnode_n sz fun \<and> snd p \<in> dom fun
 2. \<And>s ko a aa b. \<lbrakk>tcb_cap_cases (snd p) = Some (a, aa, b); kheap s (fst p) = Some ko; (case ko 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 (aa_type ao)) = ATCB\<rbrakk> \<Longrightarrow> \<exists>tcb. ko = TCB tcb proof (prove)
goal (2 subgoals):
 1. \<And>s ko x11 x12. \<lbrakk>kheap s (fst p) = Some (CNode x11 x12); (if well_formed_cnode_n x11 x12 then ACapTable x11 else AGarbage (cte_level_bits + x11)) = ACapTable (length (snd p)); ko = CNode x11 x12\<rbrakk> \<Longrightarrow> well_formed_cnode_n x11 x12 \<and> snd p \<in> dom x12
 2. \<And>s ko a aa b. \<lbrakk>tcb_cap_cases (snd p) = Some (a, aa, b); kheap s (fst p) = Some ko; (case ko 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 (aa_type ao)) = ATCB\<rbrakk> \<Longrightarrow> \<exists>tcb. ko = TCB tcb proof (prove)
goal (1 subgoal):
 1. \<And>s ko a aa b. \<lbrakk>tcb_cap_cases (snd p) = Some (a, aa, b); kheap s (fst p) = Some ko; (case ko 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 (aa_type ao)) = ATCB\<rbrakk> \<Longrightarrow> \<exists>tcb. ko = TCB tcb proof (prove)
goal:
No subgoals!