theory CSpace_AI

lemma set_cap_mdb_cte_at:
  "\<lbrace>\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and>
        (dest \<in> dom (cdt s)\<union> ran (cdt s) \<longrightarrow> P new_cap)\<rbrace>
   set_cap new_cap dest
   \<lbrace>\<lambda>xc s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s)\<rbrace>" apply (clarsimp simp:mdb_cte_at_def cte_wp_at_caps_of_state valid_def) apply (simp add:mdb_set_cap) apply (intro conjI) apply (erule use_valid[OF _ set_cap_caps_of_state]) apply simp apply (rule impI) apply (erule_tac P = "x\<in> ran G" for x G in mp) apply (rule ranI,simp) apply (erule use_valid[OF _ set_cap_caps_of_state]) apply (drule spec)+ apply (drule_tac P = "cdt x y = z" for x y z in mp) apply simp+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> (dest \<in> dom (cdt s) \<union> ran (cdt s) \<longrightarrow> P new_cap)\<rbrace> set_cap new_cap dest \<lbrace>\<lambda>xc s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b a ba aa bb. \<lbrakk>((), b) \<in> fst (set_cap new_cap dest s); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> P cap) \<and> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> P cap); dest \<in> dom (cdt s) \<longrightarrow> P new_cap; dest \<in> ran (cdt s) \<longrightarrow> P new_cap; cdt b (aa, bb) = Some (a, ba)\<rbrakk> \<Longrightarrow> (\<exists>cap. caps_of_state b (a, ba) = Some cap \<and> P cap) \<and> (\<exists>cap. caps_of_state b (aa, bb) = Some cap \<and> P cap) proof (prove)
goal (1 subgoal):
 1. \<And>s b a ba aa bb. \<lbrakk>((), b) \<in> fst (set_cap new_cap dest s); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> P cap) \<and> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> P cap); dest \<in> dom (cdt s) \<longrightarrow> P new_cap; dest \<in> ran (cdt s) \<longrightarrow> P new_cap; cdt s (aa, bb) = Some (a, ba)\<rbrakk> \<Longrightarrow> (\<exists>cap. caps_of_state b (a, ba) = Some cap \<and> P cap) \<and> (\<exists>cap. caps_of_state b (aa, bb) = Some cap \<and> P cap) proof (prove)
goal (2 subgoals):
 1. \<And>s b a ba aa bb. \<lbrakk>((), b) \<in> fst (set_cap new_cap dest s); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> P cap) \<and> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> P cap); dest \<in> dom (cdt s) \<longrightarrow> P new_cap; dest \<in> ran (cdt s) \<longrightarrow> P new_cap; cdt s (aa, bb) = Some (a, ba)\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state b (a, ba) = Some cap \<and> P cap
 2. \<And>s b a ba aa bb. \<lbrakk>((), b) \<in> fst (set_cap new_cap dest s); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> P cap) \<and> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> P cap); dest \<in> dom (cdt s) \<longrightarrow> P new_cap; dest \<in> ran (cdt s) \<longrightarrow> P new_cap; cdt s (aa, bb) = Some (a, ba)\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state b (aa, bb) = Some cap \<and> P cap proof (prove)
goal (2 subgoals):
 1. \<And>s b a ba aa bb. \<lbrakk>\<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> P cap) \<and> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> P cap); dest \<in> dom (cdt s) \<longrightarrow> P new_cap; dest \<in> ran (cdt s) \<longrightarrow> P new_cap; cdt s (aa, bb) = Some (a, ba)\<rbrakk> \<Longrightarrow> \<exists>cap. ((caps_of_state s)(dest \<mapsto> new_cap)) (a, ba) = Some cap \<and> P cap
 2. \<And>s b a ba aa bb. \<lbrakk>((), b) \<in> fst (set_cap new_cap dest s); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> P cap) \<and> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> P cap); dest \<in> dom (cdt s) \<longrightarrow> P new_cap; dest \<in> ran (cdt s) \<longrightarrow> P new_cap; cdt s (aa, bb) = Some (a, ba)\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state b (aa, bb) = Some cap \<and> P cap proof (prove)
goal (2 subgoals):
 1. \<And>s a ba aa bb. \<lbrakk>\<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> P cap) \<and> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> P cap); dest \<in> dom (cdt s) \<longrightarrow> P new_cap; dest \<in> ran (cdt s) \<longrightarrow> P new_cap; cdt s (aa, bb) = Some (a, ba)\<rbrakk> \<Longrightarrow> (a, ba) = dest \<longrightarrow> P new_cap
 2. \<And>s b a ba aa bb. \<lbrakk>((), b) \<in> fst (set_cap new_cap dest s); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> P cap) \<and> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> P cap); dest \<in> dom (cdt s) \<longrightarrow> P new_cap; dest \<in> ran (cdt s) \<longrightarrow> P new_cap; cdt s (aa, bb) = Some (a, ba)\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state b (aa, bb) = Some cap \<and> P cap proof (prove)
goal (2 subgoals):
 1. \<And>s a ba aa bb. \<lbrakk>\<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> P cap) \<and> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> P cap); dest \<in> dom (cdt s) \<longrightarrow> P new_cap; dest \<in> ran (cdt s) \<longrightarrow> P new_cap; cdt s (aa, bb) = Some (a, ba); (a, ba) = dest\<rbrakk> \<Longrightarrow> P new_cap
 2. \<And>s b a ba aa bb. \<lbrakk>((), b) \<in> fst (set_cap new_cap dest s); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> P cap) \<and> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> P cap); dest \<in> dom (cdt s) \<longrightarrow> P new_cap; dest \<in> ran (cdt s) \<longrightarrow> P new_cap; cdt s (aa, bb) = Some (a, ba)\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state b (aa, bb) = Some cap \<and> P cap proof (prove)
goal (2 subgoals):
 1. \<And>s a ba aa bb. \<lbrakk>\<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> P cap) \<and> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> P cap); dest \<in> dom (cdt s) \<longrightarrow> P new_cap; cdt s (aa, bb) = Some (a, ba); (a, ba) = dest\<rbrakk> \<Longrightarrow> dest \<in> ran (cdt s)
 2. \<And>s b a ba aa bb. \<lbrakk>((), b) \<in> fst (set_cap new_cap dest s); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> P cap) \<and> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> P cap); dest \<in> dom (cdt s) \<longrightarrow> P new_cap; dest \<in> ran (cdt s) \<longrightarrow> P new_cap; cdt s (aa, bb) = Some (a, ba)\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state b (aa, bb) = Some cap \<and> P cap proof (prove)
goal (1 subgoal):
 1. \<And>s b a ba aa bb. \<lbrakk>((), b) \<in> fst (set_cap new_cap dest s); \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> P cap) \<and> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> P cap); dest \<in> dom (cdt s) \<longrightarrow> P new_cap; dest \<in> ran (cdt s) \<longrightarrow> P new_cap; cdt s (aa, bb) = Some (a, ba)\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state b (aa, bb) = Some cap \<and> P cap proof (prove)
goal (1 subgoal):
 1. \<And>s b a ba aa bb. \<lbrakk>\<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> P cap) \<and> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> P cap); dest \<in> dom (cdt s) \<longrightarrow> P new_cap; dest \<in> ran (cdt s) \<longrightarrow> P new_cap; cdt s (aa, bb) = Some (a, ba)\<rbrakk> \<Longrightarrow> \<exists>cap. ((caps_of_state s)(dest \<mapsto> new_cap)) (aa, bb) = Some cap \<and> P cap proof (prove)
goal (1 subgoal):
 1. \<And>s b a ba aa bb. \<lbrakk>dest \<in> dom (cdt s) \<longrightarrow> P new_cap; dest \<in> ran (cdt s) \<longrightarrow> P new_cap; cdt s (aa, bb) = Some (a, ba); cdt s (?a46 s b a ba aa bb, ?b48 s b a ba aa bb) = Some (?a42 s b a ba aa bb, ?b44 s b a ba aa bb) \<longrightarrow> (\<exists>cap. caps_of_state s (?a42 s b a ba aa bb, ?b44 s b a ba aa bb) = Some cap \<and> P cap) \<and> (\<exists>cap. caps_of_state s (?a46 s b a ba aa bb, ?b48 s b a ba aa bb) = Some cap \<and> P cap)\<rbrakk> \<Longrightarrow> \<exists>cap. ((caps_of_state s)(dest \<mapsto> new_cap)) (aa, bb) = Some cap \<and> P cap proof (prove)
goal (2 subgoals):
 1. \<And>s b a ba aa bb. \<lbrakk>dest \<in> dom (cdt s) \<longrightarrow> P new_cap; dest \<in> ran (cdt s) \<longrightarrow> P new_cap; cdt s (aa, bb) = Some (a, ba)\<rbrakk> \<Longrightarrow> cdt s (?a46 s b a ba aa bb, ?b48 s b a ba aa bb) = Some (?a42 s b a ba aa bb, ?b44 s b a ba aa bb)
 2. \<And>s b a ba aa bb. \<lbrakk>dest \<in> dom (cdt s) \<longrightarrow> P new_cap; dest \<in> ran (cdt s) \<longrightarrow> P new_cap; cdt s (aa, bb) = Some (a, ba); (\<exists>cap. caps_of_state s (?a42 s b a ba aa bb, ?b44 s b a ba aa bb) = Some cap \<and> P cap) \<and> (\<exists>cap. caps_of_state s (?a46 s b a ba aa bb, ?b48 s b a ba aa bb) = Some cap \<and> P cap)\<rbrakk> \<Longrightarrow> \<exists>cap. ((caps_of_state s)(dest \<mapsto> new_cap)) (aa, bb) = Some cap \<and> P cap proof (prove)
goal (1 subgoal):
 1. \<And>s a ba aa bb. \<lbrakk>dest \<in> dom (cdt s) \<longrightarrow> P new_cap; dest \<in> ran (cdt s) \<longrightarrow> P new_cap; cdt s (aa, bb) = Some (a, ba); (\<exists>cap. caps_of_state s (a, ba) = Some cap \<and> P cap) \<and> (\<exists>cap. caps_of_state s (aa, bb) = Some cap \<and> P cap)\<rbrakk> \<Longrightarrow> (aa, bb) = dest \<longrightarrow> P new_cap proof (prove)
goal:
No subgoals!