theory ArchFinalise_AI

lemma no_cap_to_obj_with_diff_ref_finalI_ARCH[Finalise_AI_asms]:
  "\<lbrakk> cte_wp_at ((=) cap) p s; is_final_cap' cap s;
            obj_refs cap' = obj_refs cap \<rbrakk>
      \<Longrightarrow> no_cap_to_obj_with_diff_ref cap' {p} s" apply (case_tac "obj_refs cap = {}") apply (case_tac "cap_irqs cap = {}") apply (case_tac "arch_gen_refs cap = {}") apply (simp add: is_final_cap'_def) apply (case_tac cap, simp_all add: gen_obj_refs_def) apply ((clarsimp simp add: no_cap_to_obj_with_diff_ref_def
                              cte_wp_at_caps_of_state
                              vs_cap_ref_def
                       dest!: obj_ref_none_no_asid[rule_format])+)[2] apply (clarsimp simp: no_cap_to_obj_with_diff_ref_def
                        is_final_cap'_def2
              simp del: split_paired_All) apply (frule_tac x=p in spec) apply (drule_tac x="(a, b)" in spec) apply (clarsimp simp: cte_wp_at_caps_of_state
                        gen_obj_refs_Int) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) cap) p s; is_final_cap' cap s; obj_refs cap' = obj_refs cap\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap' {p} s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cte_wp_at ((=) cap) p s; is_final_cap' cap s; obj_refs cap' = obj_refs cap; obj_refs cap = {}\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap' {p} s
 2. \<lbrakk>cte_wp_at ((=) cap) p s; is_final_cap' cap s; obj_refs cap' = obj_refs cap; obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap' {p} s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cte_wp_at ((=) cap) p s; is_final_cap' cap s; obj_refs cap' = obj_refs cap; obj_refs cap = {}; cap_irqs cap = {}\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap' {p} s
 2. \<lbrakk>cte_wp_at ((=) cap) p s; is_final_cap' cap s; obj_refs cap' = obj_refs cap; obj_refs cap = {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap' {p} s
 3. \<lbrakk>cte_wp_at ((=) cap) p s; is_final_cap' cap s; obj_refs cap' = obj_refs cap; obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap' {p} s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>cte_wp_at ((=) cap) p s; is_final_cap' cap s; obj_refs cap' = obj_refs cap; obj_refs cap = {}; cap_irqs cap = {}; arch_gen_refs cap = {}\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap' {p} s
 2. \<lbrakk>cte_wp_at ((=) cap) p s; is_final_cap' cap s; obj_refs cap' = obj_refs cap; obj_refs cap = {}; cap_irqs cap = {}; arch_gen_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap' {p} s
 3. \<lbrakk>cte_wp_at ((=) cap) p s; is_final_cap' cap s; obj_refs cap' = obj_refs cap; obj_refs cap = {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap' {p} s
 4. \<lbrakk>cte_wp_at ((=) cap) p s; is_final_cap' cap s; obj_refs cap' = obj_refs cap; obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap' {p} s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>cte_wp_at ((=) cap) p s; \<exists>a b. {cref. \<exists>cap'. fst (get_cap cref s) = {(cap', s)} \<and> gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}} = {(a, b)}; obj_refs cap' = {}; obj_refs cap = {}; cap_irqs cap = {}; arch_gen_refs cap = {}\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap' {p} s
 2. \<lbrakk>cte_wp_at ((=) cap) p s; is_final_cap' cap s; obj_refs cap' = obj_refs cap; obj_refs cap = {}; cap_irqs cap = {}; arch_gen_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap' {p} s
 3. \<lbrakk>cte_wp_at ((=) cap) p s; is_final_cap' cap s; obj_refs cap' = obj_refs cap; obj_refs cap = {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap' {p} s
 4. \<lbrakk>cte_wp_at ((=) cap) p s; is_final_cap' cap s; obj_refs cap' = obj_refs cap; obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap' {p} s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cte_wp_at ((=) cap) p s; is_final_cap' cap s; obj_refs cap' = {}; obj_refs cap = {}; cap_irqs cap = {}; arch_gen_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap' {p} s
 2. \<lbrakk>cte_wp_at ((=) cap) p s; is_final_cap' cap s; obj_refs cap' = {}; obj_refs cap = {}; cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap' {p} s
 3. \<lbrakk>cte_wp_at ((=) cap) p s; is_final_cap' cap s; obj_refs cap' = obj_refs cap; obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap' {p} s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) cap) p s; is_final_cap' cap s; obj_refs cap' = obj_refs cap; obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap' {p} s proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>cte_wp_at ((=) cap) p s; obj_refs cap' = obj_refs cap; obj_refs cap \<noteq> {}; \<forall>cref'. cte_wp_at (\<lambda>c. gen_obj_refs cap \<inter> gen_obj_refs c \<noteq> {}) cref' s = (cref' = (aa, ba)); (a, b) \<noteq> p; cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap') (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>cte_wp_at ((=) cap) p s; obj_refs cap' = obj_refs cap; obj_refs cap \<noteq> {}; \<forall>cref'. cte_wp_at (\<lambda>c. gen_obj_refs cap \<inter> gen_obj_refs c \<noteq> {}) cref' s = (cref' = (aa, ba)); (a, b) \<noteq> p; cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap') (a, b) s; cte_wp_at (\<lambda>c. gen_obj_refs cap \<inter> gen_obj_refs c \<noteq> {}) p s = (p = (aa, ba))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>cte_wp_at ((=) cap) p s; obj_refs cap' = obj_refs cap; obj_refs cap \<noteq> {}; (a, b) \<noteq> p; cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap \<and> table_cap_ref c \<noteq> table_cap_ref cap') (a, b) s; cte_wp_at (\<lambda>c. gen_obj_refs cap \<inter> gen_obj_refs c \<noteq> {}) p s = (p = (aa, ba)); cte_wp_at (\<lambda>c. gen_obj_refs cap \<inter> gen_obj_refs c \<noteq> {}) (a, b) s = ((a, b) = (aa, ba))\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!