theory ArchTcb_AI

lemma checked_insert_is_derived: (* arch specific *)
  "\<lbrakk> same_object_as new_cap old_cap; is_cnode_or_valid_arch new_cap;
     obj_refs new_cap = obj_refs old_cap
         \<longrightarrow> table_cap_ref old_cap = table_cap_ref new_cap
            \<and> pt_pd_asid old_cap = pt_pd_asid new_cap\<rbrakk>
     \<Longrightarrow> is_derived m slot new_cap old_cap" apply (cases slot) apply (frule same_object_as_cap_master) apply (frule master_cap_obj_refs) apply (frule cap_master_eq_badge_none) apply (frule same_master_cap_same_types) apply (simp add: is_derived_def) apply clarsimp apply (auto simp: is_cap_simps cap_master_cap_def
                    is_cnode_or_valid_arch_def vs_cap_ref_def
                    table_cap_ref_def pt_pd_asid_def up_ucast_inj_eq
             split: cap.split_asm arch_cap.split_asm
                    option.split_asm)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>same_object_as new_cap old_cap; is_cnode_or_valid_arch new_cap; obj_refs new_cap = obj_refs old_cap \<longrightarrow> table_cap_ref old_cap = table_cap_ref new_cap \<and> pt_pd_asid old_cap = pt_pd_asid new_cap\<rbrakk> \<Longrightarrow> is_derived m slot new_cap old_cap proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>same_object_as new_cap old_cap; is_cnode_or_valid_arch new_cap; obj_refs new_cap = obj_refs old_cap \<longrightarrow> table_cap_ref old_cap = table_cap_ref new_cap \<and> pt_pd_asid old_cap = pt_pd_asid new_cap; slot = (a, b)\<rbrakk> \<Longrightarrow> is_derived m slot new_cap old_cap proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>same_object_as new_cap old_cap; is_cnode_or_valid_arch new_cap; obj_refs new_cap = obj_refs old_cap \<longrightarrow> table_cap_ref old_cap = table_cap_ref new_cap \<and> pt_pd_asid old_cap = pt_pd_asid new_cap; slot = (a, b); cap_master_cap new_cap = cap_master_cap old_cap\<rbrakk> \<Longrightarrow> is_derived m slot new_cap old_cap proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>same_object_as new_cap old_cap; is_cnode_or_valid_arch new_cap; obj_refs new_cap = obj_refs old_cap \<longrightarrow> table_cap_ref old_cap = table_cap_ref new_cap \<and> pt_pd_asid old_cap = pt_pd_asid new_cap; slot = (a, b); cap_master_cap new_cap = cap_master_cap old_cap; obj_refs new_cap = obj_refs old_cap\<rbrakk> \<Longrightarrow> is_derived m slot new_cap old_cap proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>same_object_as new_cap old_cap; is_cnode_or_valid_arch new_cap; obj_refs new_cap = obj_refs old_cap \<longrightarrow> table_cap_ref old_cap = table_cap_ref new_cap \<and> pt_pd_asid old_cap = pt_pd_asid new_cap; slot = (a, b); cap_master_cap new_cap = cap_master_cap old_cap; obj_refs new_cap = obj_refs old_cap; (cap_badge new_cap = None) = (cap_badge old_cap = None)\<rbrakk> \<Longrightarrow> is_derived m slot new_cap old_cap proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>same_object_as new_cap old_cap; is_cnode_or_valid_arch new_cap; obj_refs new_cap = obj_refs old_cap \<longrightarrow> table_cap_ref old_cap = table_cap_ref new_cap \<and> pt_pd_asid old_cap = pt_pd_asid new_cap; slot = (a, b); cap_master_cap new_cap = cap_master_cap old_cap; obj_refs new_cap = obj_refs old_cap; (cap_badge new_cap = None) = (cap_badge old_cap = None); is_pt_cap new_cap = is_pt_cap old_cap \<and> is_pd_cap new_cap = is_pd_cap old_cap\<rbrakk> \<Longrightarrow> is_derived m slot new_cap old_cap proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>same_object_as new_cap old_cap; is_cnode_or_valid_arch new_cap; table_cap_ref old_cap = table_cap_ref new_cap \<and> pt_pd_asid old_cap = pt_pd_asid new_cap; slot = (a, b); cap_master_cap new_cap = cap_master_cap old_cap; obj_refs new_cap = obj_refs old_cap; (cap_badge new_cap = None) = (cap_badge old_cap = None); is_pt_cap new_cap = is_pt_cap old_cap \<and> is_pd_cap new_cap = is_pd_cap old_cap\<rbrakk> \<Longrightarrow> (is_untyped_cap old_cap \<longrightarrow> new_cap \<noteq> NullCap \<and> \<not> is_zombie old_cap \<and> new_cap \<noteq> IRQControlCap \<and> descendants_of (a, b) m = {} \<and> is_master_reply_cap old_cap = is_reply_cap new_cap \<and> (is_pt_cap old_cap \<longrightarrow> cap_asid new_cap = cap_asid old_cap \<and> (\<exists>y. cap_asid new_cap = Some y)) \<and> (is_pd_cap old_cap \<longrightarrow> cap_asid new_cap = cap_asid old_cap \<and> (\<exists>y. cap_asid new_cap = Some y)) \<and> (vs_cap_ref new_cap = vs_cap_ref old_cap \<or> is_pg_cap old_cap) \<and> \<not> is_reply_cap old_cap \<and> \<not> is_master_reply_cap new_cap) \<and> (\<not> is_untyped_cap old_cap \<longrightarrow> new_cap \<noteq> NullCap \<and> \<not> is_zombie old_cap \<and> new_cap \<noteq> IRQControlCap \<and> (cap_badge old_cap, cap_badge new_cap) \<in> capBadge_ordering False \<and> is_master_reply_cap old_cap = is_reply_cap new_cap \<and> (is_pt_cap old_cap \<longrightarrow> cap_asid new_cap = cap_asid old_cap \<and> (\<exists>y. cap_asid new_cap = Some y)) \<and> (is_pd_cap old_cap \<longrightarrow> cap_asid new_cap = cap_asid old_cap \<and> (\<exists>y. cap_asid new_cap = Some y)) \<and> (vs_cap_ref new_cap = vs_cap_ref old_cap \<or> is_pg_cap old_cap) \<and> \<not> is_reply_cap old_cap \<and> \<not> is_master_reply_cap new_cap) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>same_object_as new_cap old_cap; is_cnode_or_valid_arch new_cap; slot = (a, b); cap_master_cap new_cap = cap_master_cap old_cap; obj_refs new_cap = obj_refs old_cap; (cap_badge new_cap = None) = (cap_badge old_cap = None); table_cap_ref old_cap = table_cap_ref new_cap; pt_pd_asid old_cap = pt_pd_asid new_cap; is_pt_cap new_cap = is_pt_cap old_cap; is_pd_cap new_cap = is_pd_cap old_cap\<rbrakk> \<Longrightarrow> (is_untyped_cap old_cap \<longrightarrow> new_cap \<noteq> NullCap \<and> \<not> is_zombie old_cap \<and> new_cap \<noteq> IRQControlCap \<and> descendants_of (a, b) m = {} \<and> is_master_reply_cap old_cap = is_reply_cap new_cap \<and> (is_pt_cap old_cap \<longrightarrow> cap_asid new_cap = cap_asid old_cap \<and> (\<exists>y. cap_asid new_cap = Some y)) \<and> (is_pd_cap old_cap \<longrightarrow> cap_asid new_cap = cap_asid old_cap \<and> (\<exists>y. cap_asid new_cap = Some y)) \<and> (vs_cap_ref new_cap = vs_cap_ref old_cap \<or> is_pg_cap old_cap) \<and> \<not> is_reply_cap old_cap \<and> \<not> is_master_reply_cap new_cap) \<and> (\<not> is_untyped_cap old_cap \<longrightarrow> new_cap \<noteq> NullCap \<and> \<not> is_zombie old_cap \<and> new_cap \<noteq> IRQControlCap \<and> (cap_badge old_cap, cap_badge new_cap) \<in> capBadge_ordering False \<and> is_master_reply_cap old_cap = is_reply_cap new_cap \<and> (is_pt_cap old_cap \<longrightarrow> cap_asid new_cap = cap_asid old_cap \<and> (\<exists>y. cap_asid new_cap = Some y)) \<and> (is_pd_cap old_cap \<longrightarrow> cap_asid new_cap = cap_asid old_cap \<and> (\<exists>y. cap_asid new_cap = Some y)) \<and> (vs_cap_ref new_cap = vs_cap_ref old_cap \<or> is_pg_cap old_cap) \<and> \<not> is_reply_cap old_cap \<and> \<not> is_master_reply_cap new_cap) proof (prove)
goal:
No subgoals!