theory ArchRetype_AI

lemma glob_vs_refs_add_one':
  "glob_vs_refs (ArchObj (PageDirectory (pd(p := pde)))) =
   glob_vs_refs (ArchObj (PageDirectory pd))
   - Pair (VSRef (ucast p) (Some APageDirectory)) ` set_option (pde_ref (pd p))
   \<union> Pair (VSRef (ucast p) (Some APageDirectory)) ` set_option (pde_ref pde)" apply (simp add: glob_vs_refs_def) apply (rule set_eqI) apply clarsimp apply (rule iffI) apply (clarsimp del: disjCI dest!: graph_ofD split: if_split_asm) apply (rule disjI1) apply (rule conjI) apply (rule_tac x="(aa, ba)" in image_eqI) apply simp apply (simp add:  graph_of_def) apply clarsimp apply (erule disjE) apply (clarsimp dest!: graph_ofD) apply (rule_tac x="(aa,ba)" in image_eqI) apply simp apply (clarsimp simp: graph_of_def) apply clarsimp apply (rule_tac x="(p,x)" in image_eqI) apply simp apply (clarsimp simp: graph_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. glob_vs_refs (ArchObj (PageDirectory (pd(p := pde)))) = glob_vs_refs (ArchObj (PageDirectory pd)) - Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<union> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde) proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd(p := pde)) = (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd) - Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<union> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde) proof (prove)
goal (1 subgoal):
 1. \<And>x. (x \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd(p := pde))) = (x \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd) - Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<union> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. ((a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd(p := pde))) = ((a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd) \<and> (a, b) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<or> (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde)) proof (prove)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd(p := pde)) \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd) \<and> (a, b) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<or> (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde)
 2. \<And>a b. (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd) \<and> (a, b) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<or> (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde) \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd(p := pde)) proof (prove)
goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>aa \<noteq> p; pde_ref (pd aa) = Some ba\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd) \<and> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<or> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde)
 2. \<And>a b. (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd) \<and> (a, b) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<or> (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde) \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd(p := pde)) proof (prove)
goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>aa \<noteq> p; pde_ref (pd aa) = Some ba\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd) \<and> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p))
 2. \<And>a b. (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd) \<and> (a, b) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<or> (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde) \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd(p := pde)) proof (prove)
goal (3 subgoals):
 1. \<And>aa ba. \<lbrakk>aa \<noteq> p; pde_ref (pd aa) = Some ba\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd)
 2. \<And>aa ba. \<lbrakk>aa \<noteq> p; pde_ref (pd aa) = Some ba\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p))
 3. \<And>a b. (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd) \<and> (a, b) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<or> (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde) \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd(p := pde)) proof (prove)
goal (4 subgoals):
 1. \<And>aa ba. \<lbrakk>aa \<noteq> p; pde_ref (pd aa) = Some ba\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) = (case (aa, ba) of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x))
 2. \<And>aa ba. \<lbrakk>aa \<noteq> p; pde_ref (pd aa) = Some ba\<rbrakk> \<Longrightarrow> (aa, ba) \<in> graph_of (pde_ref \<circ> pd)
 3. \<And>aa ba. \<lbrakk>aa \<noteq> p; pde_ref (pd aa) = Some ba\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p))
 4. \<And>a b. (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd) \<and> (a, b) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<or> (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde) \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd(p := pde)) proof (prove)
goal (3 subgoals):
 1. \<And>aa ba. \<lbrakk>aa \<noteq> p; pde_ref (pd aa) = Some ba\<rbrakk> \<Longrightarrow> (aa, ba) \<in> graph_of (pde_ref \<circ> pd)
 2. \<And>aa ba. \<lbrakk>aa \<noteq> p; pde_ref (pd aa) = Some ba\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p))
 3. \<And>a b. (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd) \<and> (a, b) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<or> (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde) \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd(p := pde)) proof (prove)
goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>aa \<noteq> p; pde_ref (pd aa) = Some ba\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p))
 2. \<And>a b. (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd) \<and> (a, b) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<or> (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde) \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd(p := pde)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd) \<and> (a, b) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<or> (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde) \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd(p := pde)) proof (prove)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd) \<and> (a, b) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd(p := pde))
 2. \<And>a b. (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde) \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd(p := pde)) proof (prove)
goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>(VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)); pde_ref (pd aa) = Some ba\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd(p := pde))
 2. \<And>a b. (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde) \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd(p := pde)) proof (prove)
goal (3 subgoals):
 1. \<And>aa ba. \<lbrakk>(VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)); pde_ref (pd aa) = Some ba\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) = (case (aa, ba) of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x))
 2. \<And>aa ba. \<lbrakk>(VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)); pde_ref (pd aa) = Some ba\<rbrakk> \<Longrightarrow> (aa, ba) \<in> graph_of (pde_ref \<circ> pd(p := pde))
 3. \<And>a b. (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde) \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd(p := pde)) proof (prove)
goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>(VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<notin> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref (pd p)); pde_ref (pd aa) = Some ba\<rbrakk> \<Longrightarrow> (aa, ba) \<in> graph_of (pde_ref \<circ> pd(p := pde))
 2. \<And>a b. (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde) \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd(p := pde)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> Pair (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory)) ` set_option (pde_ref pde) \<Longrightarrow> (a, b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd(p := pde)) proof (prove)
goal (1 subgoal):
 1. \<And>x. pde_ref pde = Some x \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory), x) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` graph_of (pde_ref \<circ> pd(p := pde)) proof (prove)
goal (2 subgoals):
 1. \<And>x. pde_ref pde = Some x \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) p) (Some APageDirectory), x) = (case (p, x) of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x))
 2. \<And>x. pde_ref pde = Some x \<Longrightarrow> (p, x) \<in> graph_of (pde_ref \<circ> pd(p := pde)) proof (prove)
goal (1 subgoal):
 1. \<And>x. pde_ref pde = Some x \<Longrightarrow> (p, x) \<in> graph_of (pde_ref \<circ> pd(p := pde)) proof (prove)
goal:
No subgoals!