theory Invariants_AI

lemma valid_mdb_eqI:
  assumes "valid_mdb s"
  assumes c: "\<And>p P. cte_wp_at P p s = cte_wp_at P p s'"
  assumes "cdt s = cdt s'"
  assumes "is_original_cap s = is_original_cap s'"
  shows "valid_mdb s'" using assms apply (simp add: valid_mdb_def) apply (rule conjI) apply (force simp add: valid_mdb_def swp_def mdb_cte_at_def) apply (clarsimp simp add: cte_wp_caps_of_lift [OF c] valid_arch_mdb_eqI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_mdb s' proof (prove)
using this:
valid_mdb s
cte_wp_at ?P ?p s = cte_wp_at ?P ?p s'
cdt s = cdt s'
is_original_cap s = is_original_cap s'

goal (1 subgoal):
 1. valid_mdb s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s') \<and> untyped_mdb (cdt s') (caps_of_state s) \<and> descendants_inc (cdt s') (caps_of_state s) \<and> no_mloop (cdt s') \<and> untyped_inc (cdt s') (caps_of_state s) \<and> ut_revocable (is_original_cap s') (caps_of_state s) \<and> irq_revocable (is_original_cap s') (caps_of_state s) \<and> reply_master_revocable (is_original_cap s') (caps_of_state s) \<and> reply_mdb (cdt s') (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s') (caps_of_state s); \<And>P p. cte_wp_at P p s = cte_wp_at P p s'; cdt s = cdt s'; is_original_cap s = is_original_cap s'\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s') (cdt s') \<and> untyped_mdb (cdt s') (caps_of_state s') \<and> descendants_inc (cdt s') (caps_of_state s') \<and> untyped_inc (cdt s') (caps_of_state s') \<and> ut_revocable (is_original_cap s') (caps_of_state s') \<and> irq_revocable (is_original_cap s') (caps_of_state s') \<and> reply_master_revocable (is_original_cap s') (caps_of_state s') \<and> reply_mdb (cdt s') (caps_of_state s') \<and> valid_arch_mdb (is_original_cap s') (caps_of_state s') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s') \<and> untyped_mdb (cdt s') (caps_of_state s) \<and> descendants_inc (cdt s') (caps_of_state s) \<and> no_mloop (cdt s') \<and> untyped_inc (cdt s') (caps_of_state s) \<and> ut_revocable (is_original_cap s') (caps_of_state s) \<and> irq_revocable (is_original_cap s') (caps_of_state s) \<and> reply_master_revocable (is_original_cap s') (caps_of_state s) \<and> reply_mdb (cdt s') (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s') (caps_of_state s); \<And>P p. cte_wp_at P p s = cte_wp_at P p s'; cdt s = cdt s'; is_original_cap s = is_original_cap s'\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s') (cdt s')
 2. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s') \<and> untyped_mdb (cdt s') (caps_of_state s) \<and> descendants_inc (cdt s') (caps_of_state s) \<and> no_mloop (cdt s') \<and> untyped_inc (cdt s') (caps_of_state s) \<and> ut_revocable (is_original_cap s') (caps_of_state s) \<and> irq_revocable (is_original_cap s') (caps_of_state s) \<and> reply_master_revocable (is_original_cap s') (caps_of_state s) \<and> reply_mdb (cdt s') (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s') (caps_of_state s); \<And>P p. cte_wp_at P p s = cte_wp_at P p s'; cdt s = cdt s'; is_original_cap s = is_original_cap s'\<rbrakk> \<Longrightarrow> untyped_mdb (cdt s') (caps_of_state s') \<and> descendants_inc (cdt s') (caps_of_state s') \<and> untyped_inc (cdt s') (caps_of_state s') \<and> ut_revocable (is_original_cap s') (caps_of_state s') \<and> irq_revocable (is_original_cap s') (caps_of_state s') \<and> reply_master_revocable (is_original_cap s') (caps_of_state s') \<and> reply_mdb (cdt s') (caps_of_state s') \<and> valid_arch_mdb (is_original_cap s') (caps_of_state s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s') \<and> untyped_mdb (cdt s') (caps_of_state s) \<and> descendants_inc (cdt s') (caps_of_state s) \<and> no_mloop (cdt s') \<and> untyped_inc (cdt s') (caps_of_state s) \<and> ut_revocable (is_original_cap s') (caps_of_state s) \<and> irq_revocable (is_original_cap s') (caps_of_state s) \<and> reply_master_revocable (is_original_cap s') (caps_of_state s) \<and> reply_mdb (cdt s') (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s') (caps_of_state s); \<And>P p. cte_wp_at P p s = cte_wp_at P p s'; cdt s = cdt s'; is_original_cap s = is_original_cap s'\<rbrakk> \<Longrightarrow> untyped_mdb (cdt s') (caps_of_state s') \<and> descendants_inc (cdt s') (caps_of_state s') \<and> untyped_inc (cdt s') (caps_of_state s') \<and> ut_revocable (is_original_cap s') (caps_of_state s') \<and> irq_revocable (is_original_cap s') (caps_of_state s') \<and> reply_master_revocable (is_original_cap s') (caps_of_state s') \<and> reply_mdb (cdt s') (caps_of_state s') \<and> valid_arch_mdb (is_original_cap s') (caps_of_state s') proof (prove)
goal:
No subgoals!