theory StoreWord_C

lemma projectKO_opt_retyp_same:
  assumes pko: "projectKO_opt ko = Some v"
  shows "projectKO_opt \<circ>\<^sub>m
    (\<lambda>x. if x \<in> set (new_cap_addrs sz ptr ko) then Some ko else ksPSpace \<sigma> x)
  =
  (\<lambda>x. if x \<in> set (new_cap_addrs sz ptr ko) then Some v else (projectKO_opt \<circ>\<^sub>m (ksPSpace \<sigma>)) x)"
  (is "?LHS = ?RHS") proof (rule ext) fix x show "?LHS x = ?RHS x" proof (cases "x \<in> set (new_cap_addrs sz ptr ko)") case True thus ?thesis using pko by simp next case False thus ?thesis by (simp add: map_comp_def) 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 sz ptr ko) then Some ko else ksPSpace \<sigma> x) = (\<lambda>x. if x \<in> set (new_cap_addrs sz ptr ko) then Some v else (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 sz ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (if x \<in> set (new_cap_addrs sz ptr ko) then Some v else (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 sz ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (if x \<in> set (new_cap_addrs sz ptr ko) then Some v else (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 sz ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (if x \<in> set (new_cap_addrs sz ptr ko) then Some v else (projectKO_opt \<circ>\<^sub>m ksPSpace \<sigma>) x) proof (state)
goal (2 subgoals):
 1. x \<in> set (new_cap_addrs sz ptr ko) \<Longrightarrow> (projectKO_opt \<circ>\<^sub>m (\<lambda>x. if x \<in> set (new_cap_addrs sz ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (if x \<in> set (new_cap_addrs sz ptr ko) then Some v else (projectKO_opt \<circ>\<^sub>m ksPSpace \<sigma>) x)
 2. x \<notin> set (new_cap_addrs sz ptr ko) \<Longrightarrow> (projectKO_opt \<circ>\<^sub>m (\<lambda>x. if x \<in> set (new_cap_addrs sz ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (if x \<in> set (new_cap_addrs sz ptr ko) then Some v else (projectKO_opt \<circ>\<^sub>m ksPSpace \<sigma>) x) proof (state)
this:
x \<in> set (new_cap_addrs sz ptr ko)

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

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

goal (1 subgoal):
 1. (projectKO_opt \<circ>\<^sub>m (\<lambda>x. if x \<in> set (new_cap_addrs sz ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (if x \<in> set (new_cap_addrs sz ptr ko) then Some v else (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 sz ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (if x \<in> set (new_cap_addrs sz ptr ko) then Some v else (projectKO_opt \<circ>\<^sub>m ksPSpace \<sigma>) x)

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

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

goal (1 subgoal):
 1. (projectKO_opt \<circ>\<^sub>m (\<lambda>x. if x \<in> set (new_cap_addrs sz ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (if x \<in> set (new_cap_addrs sz ptr ko) then Some v else (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 sz ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (if x \<in> set (new_cap_addrs sz ptr ko) then Some v else (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 sz ptr ko) then Some ko else ksPSpace \<sigma> x)) x = (if x \<in> set (new_cap_addrs sz ptr ko) then Some v else (projectKO_opt \<circ>\<^sub>m ksPSpace \<sigma>) x)

goal:
No subgoals!