theory CSpace_R

lemma untyped_ranges_zero_delta:
  assumes urz: "untyped_ranges_zero' s"
    and other: "\<forall>p. p \<notin> set xs \<longrightarrow> cps' p = cteCaps_of s p"
     and vmdb: "valid_mdb' s"
     and vobj: "valid_objs' s"
       and eq: "ran (restrict_map (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) (set xs))
           \<subseteq> gsUntypedZeroRanges s
        \<Longrightarrow> utr' = ((gsUntypedZeroRanges s - ran (restrict_map (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) (set xs)))
                \<union> ran (restrict_map (untypedZeroRange \<circ>\<^sub>m cps') (set xs)))"
  notes Collect_const[simp del]
  shows "untyped_ranges_zero_inv cps' utr'" apply (subst eq) apply (clarsimp simp: urz[unfolded untyped_ranges_zero_inv_def]) apply (fastforce simp: map_comp_Some_iff restrict_map_Some_iff elim!: ranE)[1] apply (simp add: untyped_ranges_zero_inv_def urz[unfolded untyped_ranges_zero_inv_def]) apply (rule sym, rule trans, rule_tac P="\<lambda>x. x \<in> set xs"
        and m="untypedZeroRange \<circ>\<^sub>m cteCaps_of s" in ran_split_eq) apply (rule_tac B="dom (untypedZeroRange \<circ>\<^sub>m (\<lambda>cp. if valid_cap' cp s
      then Some cp else None) \<circ>\<^sub>m cteCaps_of s)" in subset_inj_on[rotated]) apply (clarsimp simp: map_comp_Some_iff cteCaps_of_def) apply (case_tac "the (ctes_of s x)", clarsimp) apply (frule ctes_of_valid_cap'[OF _ vobj]) apply blast apply (cut_tac vmdb) apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def) apply (clarsimp intro!: inj_onI simp: map_comp_Some_iff
                     split: if_split_asm) apply (drule(1) untypedZeroRange_to_usableCapRange)+ apply (clarsimp) apply (drule(2) usableUntypedRange_uniq, (simp add: valid_capAligned)+) apply (simp add: map_comp_def other) apply (simp add: restrict_map_is_map_comp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_ranges_zero_inv cps' utr' proof (prove)
goal (2 subgoals):
 1. ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set xs) \<subseteq> gsUntypedZeroRanges s
 2. untyped_ranges_zero_inv cps' (gsUntypedZeroRanges s - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set xs) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` set xs)) proof (prove)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set xs) \<Longrightarrow> (a, b) \<in> ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s)
 2. untyped_ranges_zero_inv cps' (gsUntypedZeroRanges s - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set xs) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` set xs)) proof (prove)
goal (1 subgoal):
 1. untyped_ranges_zero_inv cps' (gsUntypedZeroRanges s - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set xs) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` set xs)) proof (prove)
goal (1 subgoal):
 1. ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set xs) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` set xs) = ran (untypedZeroRange \<circ>\<^sub>m cps') proof (prove)
goal (3 subgoals):
 1. inj_on (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) (dom (untypedZeroRange \<circ>\<^sub>m cteCaps_of s))
 2. \<forall>x. x \<notin> set xs \<longrightarrow> (untypedZeroRange \<circ>\<^sub>m cps') x = (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) x
 3. ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` {x. x \<in> set xs}) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` {x. x \<in> set xs}) = ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set xs) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` set xs) proof (prove)
goal (4 subgoals):
 1. dom (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) \<subseteq> dom (untypedZeroRange \<circ>\<^sub>m (\<lambda>cp. if valid_cap' cp s then Some cp else None) \<circ>\<^sub>m cteCaps_of s)
 2. inj_on (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) (dom (untypedZeroRange \<circ>\<^sub>m (\<lambda>cp. if valid_cap' cp s then Some cp else None) \<circ>\<^sub>m cteCaps_of s))
 3. \<forall>x. x \<notin> set xs \<longrightarrow> (untypedZeroRange \<circ>\<^sub>m cps') x = (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) x
 4. ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` {x. x \<in> set xs}) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` {x. x \<in> set xs}) = ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set xs) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` set xs) proof (prove)
goal (4 subgoals):
 1. \<And>x a b z. \<lbrakk>untypedZeroRange (cteCap z) = Some (a, b); ctes_of s x = Some z\<rbrakk> \<Longrightarrow> \<exists>a b k'. (valid_cap' k' s \<longrightarrow> cteCap z = k' \<and> untypedZeroRange k' = Some (a, b)) \<and> valid_cap' k' s
 2. inj_on (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) (dom (untypedZeroRange \<circ>\<^sub>m (\<lambda>cp. if valid_cap' cp s then Some cp else None) \<circ>\<^sub>m cteCaps_of s))
 3. \<forall>x. x \<notin> set xs \<longrightarrow> (untypedZeroRange \<circ>\<^sub>m cps') x = (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) x
 4. ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` {x. x \<in> set xs}) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` {x. x \<in> set xs}) = ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set xs) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` set xs) proof (prove)
goal (4 subgoals):
 1. \<And>x a b x1 x2. \<lbrakk>untypedZeroRange x1 = Some (a, b); ctes_of s x = Some (CTE x1 x2)\<rbrakk> \<Longrightarrow> \<exists>a b k'. (valid_cap' k' s \<longrightarrow> x1 = k' \<and> untypedZeroRange k' = Some (a, b)) \<and> valid_cap' k' s
 2. inj_on (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) (dom (untypedZeroRange \<circ>\<^sub>m (\<lambda>cp. if valid_cap' cp s then Some cp else None) \<circ>\<^sub>m cteCaps_of s))
 3. \<forall>x. x \<notin> set xs \<longrightarrow> (untypedZeroRange \<circ>\<^sub>m cps') x = (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) x
 4. ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` {x. x \<in> set xs}) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` {x. x \<in> set xs}) = ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set xs) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` set xs) proof (prove)
goal (4 subgoals):
 1. \<And>x a b x1 x2. \<lbrakk>untypedZeroRange x1 = Some (a, b); ctes_of s x = Some (CTE x1 x2); valid_cap' x1 s\<rbrakk> \<Longrightarrow> \<exists>a b k'. (valid_cap' k' s \<longrightarrow> x1 = k' \<and> untypedZeroRange k' = Some (a, b)) \<and> valid_cap' k' s
 2. inj_on (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) (dom (untypedZeroRange \<circ>\<^sub>m (\<lambda>cp. if valid_cap' cp s then Some cp else None) \<circ>\<^sub>m cteCaps_of s))
 3. \<forall>x. x \<notin> set xs \<longrightarrow> (untypedZeroRange \<circ>\<^sub>m cps') x = (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) x
 4. ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` {x. x \<in> set xs}) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` {x. x \<in> set xs}) = ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set xs) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` set xs) proof (prove)
goal (3 subgoals):
 1. inj_on (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) (dom (untypedZeroRange \<circ>\<^sub>m (\<lambda>cp. if valid_cap' cp s then Some cp else None) \<circ>\<^sub>m cteCaps_of s))
 2. \<forall>x. x \<notin> set xs \<longrightarrow> (untypedZeroRange \<circ>\<^sub>m cps') x = (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) x
 3. ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` {x. x \<in> set xs}) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` {x. x \<in> set xs}) = ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set xs) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` set xs) proof (prove)
goal (3 subgoals):
 1. valid_mdb' s \<Longrightarrow> inj_on (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) (dom (untypedZeroRange \<circ>\<^sub>m (\<lambda>cp. if valid_cap' cp s then Some cp else None) \<circ>\<^sub>m cteCaps_of s))
 2. \<forall>x. x \<notin> set xs \<longrightarrow> (untypedZeroRange \<circ>\<^sub>m cps') x = (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) x
 3. ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` {x. x \<in> set xs}) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` {x. x \<in> set xs}) = ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set xs) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` set xs) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> inj_on (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) (dom (untypedZeroRange \<circ>\<^sub>m (\<lambda>cp. if valid_cap' cp s then Some cp else None) \<circ>\<^sub>m cteCaps_of s))
 2. \<forall>x. x \<notin> set xs \<longrightarrow> (untypedZeroRange \<circ>\<^sub>m cps') x = (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) x
 3. ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` {x. x \<in> set xs}) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` {x. x \<in> set xs}) = ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set xs) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` set xs) proof (prove)
goal (3 subgoals):
 1. \<And>x y b aa k' k'b. \<lbrakk>untypedZeroRange k'b = Some (aa, b); valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); cteCaps_of s y = Some k'b; valid_cap' k'b s; valid_cap' k' s; cteCaps_of s x = Some k'; untypedZeroRange k' = Some (aa, b)\<rbrakk> \<Longrightarrow> x = y
 2. \<forall>x. x \<notin> set xs \<longrightarrow> (untypedZeroRange \<circ>\<^sub>m cps') x = (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) x
 3. ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` {x. x \<in> set xs}) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` {x. x \<in> set xs}) = ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set xs) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` set xs) proof (prove)
goal (3 subgoals):
 1. \<And>x y b aa k' k'b. \<lbrakk>valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); cteCaps_of s y = Some k'b; valid_cap' k'b s; valid_cap' k' s; cteCaps_of s x = Some k'; isUntypedCap k'b \<and> usableUntypedRange k'b = {aa..b} \<and> aa \<le> b; isUntypedCap k' \<and> usableUntypedRange k' = {aa..b} \<and> aa \<le> b\<rbrakk> \<Longrightarrow> x = y
 2. \<forall>x. x \<notin> set xs \<longrightarrow> (untypedZeroRange \<circ>\<^sub>m cps') x = (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) x
 3. ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` {x. x \<in> set xs}) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` {x. x \<in> set xs}) = ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set xs) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` set xs) proof (prove)
goal (3 subgoals):
 1. \<And>x y b aa k' k'b. \<lbrakk>valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); cteCaps_of s y = Some k'b; valid_cap' k'b s; valid_cap' k' s; cteCaps_of s x = Some k'; isUntypedCap k'b; usableUntypedRange k'b = {aa..b}; isUntypedCap k'; usableUntypedRange k' = {aa..b}; aa \<le> b\<rbrakk> \<Longrightarrow> x = y
 2. \<forall>x. x \<notin> set xs \<longrightarrow> (untypedZeroRange \<circ>\<^sub>m cps') x = (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) x
 3. ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` {x. x \<in> set xs}) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` {x. x \<in> set xs}) = ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set xs) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` set xs) proof (prove)
goal (2 subgoals):
 1. \<forall>x. x \<notin> set xs \<longrightarrow> (untypedZeroRange \<circ>\<^sub>m cps') x = (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) x
 2. ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` {x. x \<in> set xs}) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` {x. x \<in> set xs}) = ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set xs) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` set xs) proof (prove)
goal (1 subgoal):
 1. ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` {x. x \<in> set xs}) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` {x. x \<in> set xs}) = ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set xs) \<union> ran ((untypedZeroRange \<circ>\<^sub>m cps') |` set xs) proof (prove)
goal:
No subgoals!