theory Retype_C

lemma projectKO_opt_retyp_other:
  assumes cover: "range_cover ptr sz (objBitsKO ko) n"
  assumes pal: "pspace_aligned' \<sigma>"
  assumes pno: "pspace_no_overlap' ptr sz \<sigma>"
  and  ko_def: "ko \<equiv> x"
  and  pko: "\<forall>v. (projectKO_opt x :: ('a :: pre_storable) option) \<noteq> Some v"
  shows "projectKO_opt \<circ>\<^sub>m
    (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x)
  = (projectKO_opt \<circ>\<^sub>m (ksPSpace \<sigma>) :: word32 \<Rightarrow> ('a :: pre_storable) option)" (is "?LHS = ?RHS") proof (rule ext) fix x show "?LHS x = ?RHS x" proof (cases "x \<in> set (new_cap_addrs n ptr ko)") case False thus ?thesis by (simp add: map_comp_def) next case True hence "ksPSpace \<sigma> x = None" apply - apply (cut_tac no_overlap_new_cap_addrs_disjoint [OF cover pal pno]) apply (rule ccontr) apply (clarsimp,drule domI[where a = x]) apply blast done thus ?thesis using True pko ko_def by simp qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. projectKO_opt \<circ>\<^sub>m (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x) = projectKO_opt \<circ>\<^sub>m ksPSpace \<sigma> proof (state)
goal (1 subgoal):
 1. \<And>x. (projectKO_opt \<circ>\<^sub>m (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (projectKO_opt \<circ>\<^sub>m ksPSpace \<sigma>) x proof (state)
goal (1 subgoal):
 1. \<And>x. (projectKO_opt \<circ>\<^sub>m (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (projectKO_opt \<circ>\<^sub>m ksPSpace \<sigma>) x proof (prove)
goal (1 subgoal):
 1. (projectKO_opt \<circ>\<^sub>m (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (projectKO_opt \<circ>\<^sub>m ksPSpace \<sigma>) x proof (state)
goal (2 subgoals):
 1. x \<in> set (new_cap_addrs n ptr ko) \<Longrightarrow> (projectKO_opt \<circ>\<^sub>m (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (projectKO_opt \<circ>\<^sub>m ksPSpace \<sigma>) x
 2. x \<notin> set (new_cap_addrs n ptr ko) \<Longrightarrow> (projectKO_opt \<circ>\<^sub>m (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (projectKO_opt \<circ>\<^sub>m ksPSpace \<sigma>) x proof (state)
this:
x \<notin> set (new_cap_addrs n ptr ko)

goal (2 subgoals):
 1. x \<in> set (new_cap_addrs n ptr ko) \<Longrightarrow> (projectKO_opt \<circ>\<^sub>m (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (projectKO_opt \<circ>\<^sub>m ksPSpace \<sigma>) x
 2. x \<notin> set (new_cap_addrs n ptr ko) \<Longrightarrow> (projectKO_opt \<circ>\<^sub>m (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (projectKO_opt \<circ>\<^sub>m ksPSpace \<sigma>) x proof (prove)
using this:
x \<notin> set (new_cap_addrs n ptr ko)

goal (1 subgoal):
 1. (projectKO_opt \<circ>\<^sub>m (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (projectKO_opt \<circ>\<^sub>m ksPSpace \<sigma>) x proof (state)
this:
(projectKO_opt \<circ>\<^sub>m (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (projectKO_opt \<circ>\<^sub>m ksPSpace \<sigma>) x

goal (1 subgoal):
 1. x \<in> set (new_cap_addrs n ptr ko) \<Longrightarrow> (projectKO_opt \<circ>\<^sub>m (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (projectKO_opt \<circ>\<^sub>m ksPSpace \<sigma>) x proof (state)
goal (1 subgoal):
 1. x \<in> set (new_cap_addrs n ptr ko) \<Longrightarrow> (projectKO_opt \<circ>\<^sub>m (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (projectKO_opt \<circ>\<^sub>m ksPSpace \<sigma>) x proof (state)
this:
x \<in> set (new_cap_addrs n ptr ko)

goal (1 subgoal):
 1. x \<in> set (new_cap_addrs n ptr ko) \<Longrightarrow> (projectKO_opt \<circ>\<^sub>m (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (projectKO_opt \<circ>\<^sub>m ksPSpace \<sigma>) x proof (prove)
using this:
x \<in> set (new_cap_addrs n ptr ko)

goal (1 subgoal):
 1. ksPSpace \<sigma> x = None proof (prove)
goal (1 subgoal):
 1. x \<in> set (new_cap_addrs n ptr ko) \<Longrightarrow> ksPSpace \<sigma> x = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set (new_cap_addrs n ptr ko); set (new_cap_addrs n ptr ko) \<inter> dom (ksPSpace \<sigma>) = {}\<rbrakk> \<Longrightarrow> ksPSpace \<sigma> x = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set (new_cap_addrs n ptr ko); set (new_cap_addrs n ptr ko) \<inter> dom (ksPSpace \<sigma>) = {}; ksPSpace \<sigma> x \<noteq> None\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>x \<in> set (new_cap_addrs n ptr ko); set (new_cap_addrs n ptr ko) \<inter> dom (ksPSpace \<sigma>) = {}; x \<in> dom (ksPSpace \<sigma>)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
ksPSpace \<sigma> x = None

goal (1 subgoal):
 1. x \<in> set (new_cap_addrs n ptr ko) \<Longrightarrow> (projectKO_opt \<circ>\<^sub>m (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (projectKO_opt \<circ>\<^sub>m ksPSpace \<sigma>) x proof (prove)
using this:
ksPSpace \<sigma> x = None

goal (1 subgoal):
 1. (projectKO_opt \<circ>\<^sub>m (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (projectKO_opt \<circ>\<^sub>m ksPSpace \<sigma>) x proof (prove)
using this:
ksPSpace \<sigma> x = None
x \<in> set (new_cap_addrs n ptr ko)
\<forall>v. projectKO_opt x \<noteq> Some v
ko \<equiv> x

goal (1 subgoal):
 1. (projectKO_opt \<circ>\<^sub>m (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (projectKO_opt \<circ>\<^sub>m ksPSpace \<sigma>) x proof (state)
this:
(projectKO_opt \<circ>\<^sub>m (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (projectKO_opt \<circ>\<^sub>m ksPSpace \<sigma>) x

goal:
No subgoals! proof (state)
this:
(projectKO_opt \<circ>\<^sub>m (\<lambda>x. if x \<in> set (new_cap_addrs n ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (projectKO_opt \<circ>\<^sub>m ksPSpace \<sigma>) x

goal:
No subgoals!