theory Invariants_AI

lemma cte_wp_at_cases:
  "cte_wp_at P t s = ((\<exists>sz fun cap. kheap s (fst t) = Some (CNode sz fun) \<and>
                                    well_formed_cnode_n sz fun \<and>
                                    fun (snd t) = Some cap \<and> P cap) \<or>
                      (\<exists>tcb get set restr. kheap s (fst t) = Some (TCB tcb) \<and>
                             tcb_cap_cases (snd t) = Some (get, set, restr) \<and>
                             P (get tcb)))" apply (cases t) apply (cases "kheap s (fst t)") apply (simp add: cte_wp_at_def get_cap_def
                    get_object_def gets_def get_def return_def assert_def
                    fail_def bind_def) apply (simp add: cte_wp_at_def get_cap_def tcb_cnode_map_def bind_def
                   get_object_def assert_opt_def return_def gets_def get_def
                   assert_def fail_def dom_def
              split: if_split_asm kernel_object.splits
                     option.splits) apply (simp add: tcb_cap_cases_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at P t s = ((\<exists>sz fun cap. kheap s (fst t) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun (snd t) = Some cap \<and> P cap) \<or> (\<exists>tcb get set restr. kheap s (fst t) = Some (TCB tcb) \<and> tcb_cap_cases (snd t) = Some (get, set, restr) \<and> P (get tcb))) proof (prove)
goal (1 subgoal):
 1. \<And>a b. t = (a, b) \<Longrightarrow> cte_wp_at P t s = ((\<exists>sz fun cap. kheap s (fst t) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun (snd t) = Some cap \<and> P cap) \<or> (\<exists>tcb get set restr. kheap s (fst t) = Some (TCB tcb) \<and> tcb_cap_cases (snd t) = Some (get, set, restr) \<and> P (get tcb))) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>t = (a, b); kheap s (fst t) = None\<rbrakk> \<Longrightarrow> cte_wp_at P t s = ((\<exists>sz fun cap. kheap s (fst t) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun (snd t) = Some cap \<and> P cap) \<or> (\<exists>tcb get set restr. kheap s (fst t) = Some (TCB tcb) \<and> tcb_cap_cases (snd t) = Some (get, set, restr) \<and> P (get tcb)))
 2. \<And>a b aa. \<lbrakk>t = (a, b); kheap s (fst t) = Some aa\<rbrakk> \<Longrightarrow> cte_wp_at P t s = ((\<exists>sz fun cap. kheap s (fst t) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun (snd t) = Some cap \<and> P cap) \<or> (\<exists>tcb get set restr. kheap s (fst t) = Some (TCB tcb) \<and> tcb_cap_cases (snd t) = Some (get, set, restr) \<and> P (get tcb))) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa. \<lbrakk>t = (a, b); kheap s (fst t) = Some aa\<rbrakk> \<Longrightarrow> cte_wp_at P t s = ((\<exists>sz fun cap. kheap s (fst t) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun (snd t) = Some cap \<and> P cap) \<or> (\<exists>tcb get set restr. kheap s (fst t) = Some (TCB tcb) \<and> tcb_cap_cases (snd t) = Some (get, set, restr) \<and> P (get tcb))) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa. \<lbrakk>t = (a, b); kheap s a = Some aa\<rbrakk> \<Longrightarrow> b \<noteq> tcb_cnode_index 4 \<longrightarrow> b \<noteq> tcb_cnode_index 3 \<longrightarrow> b \<noteq> tcb_cnode_index 2 \<longrightarrow> b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> b \<noteq> tcb_cnode_index 0 \<longrightarrow> (\<forall>x2. aa = TCB x2 \<longrightarrow> (\<forall>get. (\<forall>set restr. tcb_cap_cases b \<noteq> Some (get, set, restr)) \<or> \<not> P (get x2))) proof (prove)
goal:
No subgoals!