theory ArchVSpace_AI

lemma new_lookups_rtrancl:
  "new_lookups^* = Id \<union> new_lookups" using ap pd apply - apply (rule set_eqI) apply clarsimp apply (rule iffI) apply (erule rtrancl_induct2) apply clarsimp apply (clarsimp del: disjCI) apply (erule disjE) apply clarsimp apply (thin_tac "x \<in> R^*" for x R) apply (subgoal_tac "False", simp+) apply (clarsimp simp: new_lookups_def) apply (erule disjE, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. new_lookups\<^sup>* = Id \<union> new_lookups proof (prove)
using this:
kheap s ap = Some (ArchObj (ASIDPool pool))
kheap s pdp = Some (ArchObj (PageDirectory pd))

goal (1 subgoal):
 1. new_lookups\<^sup>* = Id \<union> new_lookups proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); kheap s pdp = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> new_lookups\<^sup>* = Id \<union> new_lookups proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); kheap s pdp = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (x \<in> new_lookups\<^sup>*) = (x \<in> Id \<union> new_lookups) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); kheap s pdp = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (((a, b), aa, ba) \<in> new_lookups\<^sup>*) = (a = aa \<and> b = ba \<or> ((a, b), aa, ba) \<in> new_lookups) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); kheap s pdp = Some (ArchObj (PageDirectory pd)); ((a, b), aa, ba) \<in> new_lookups\<^sup>*\<rbrakk> \<Longrightarrow> a = aa \<and> b = ba \<or> ((a, b), aa, ba) \<in> new_lookups
 2. \<And>a b aa ba. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); kheap s pdp = Some (ArchObj (PageDirectory pd)); a = aa \<and> b = ba \<or> ((a, b), aa, ba) \<in> new_lookups\<rbrakk> \<Longrightarrow> ((a, b), aa, ba) \<in> new_lookups\<^sup>* proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); kheap s pdp = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> a = a \<and> b = b \<or> ((a, b), a, b) \<in> new_lookups
 2. \<And>a b aa ba ab bb ac bc. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); kheap s pdp = Some (ArchObj (PageDirectory pd)); ((a, b), ab, bb) \<in> new_lookups\<^sup>*; ((ab, bb), ac, bc) \<in> new_lookups; a = ab \<and> b = bb \<or> ((a, b), ab, bb) \<in> new_lookups\<rbrakk> \<Longrightarrow> a = ac \<and> b = bc \<or> ((a, b), ac, bc) \<in> new_lookups
 3. \<And>a b aa ba. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); kheap s pdp = Some (ArchObj (PageDirectory pd)); a = aa \<and> b = ba \<or> ((a, b), aa, ba) \<in> new_lookups\<rbrakk> \<Longrightarrow> ((a, b), aa, ba) \<in> new_lookups\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); kheap s pdp = Some (ArchObj (PageDirectory pd)); ((a, b), ab, bb) \<in> new_lookups\<^sup>*; ((ab, bb), ac, bc) \<in> new_lookups; a = ab \<and> b = bb \<or> ((a, b), ab, bb) \<in> new_lookups\<rbrakk> \<Longrightarrow> a = ac \<and> b = bc \<or> ((a, b), ac, bc) \<in> new_lookups
 2. \<And>a b aa ba. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); kheap s pdp = Some (ArchObj (PageDirectory pd)); a = aa \<and> b = ba \<or> ((a, b), aa, ba) \<in> new_lookups\<rbrakk> \<Longrightarrow> ((a, b), aa, ba) \<in> new_lookups\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a b ab bb ac bc. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); kheap s pdp = Some (ArchObj (PageDirectory pd)); ((a, b), ab, bb) \<in> new_lookups\<^sup>*; ((ab, bb), ac, bc) \<in> new_lookups; a = ab \<and> b = bb \<or> ((a, b), ab, bb) \<in> new_lookups\<rbrakk> \<Longrightarrow> a = ac \<and> b = bc \<or> ((a, b), ac, bc) \<in> new_lookups
 2. \<And>a b aa ba. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); kheap s pdp = Some (ArchObj (PageDirectory pd)); a = aa \<and> b = ba \<or> ((a, b), aa, ba) \<in> new_lookups\<rbrakk> \<Longrightarrow> ((a, b), aa, ba) \<in> new_lookups\<^sup>* proof (prove)
goal (3 subgoals):
 1. \<And>a b ab bb ac bc. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); kheap s pdp = Some (ArchObj (PageDirectory pd)); ((a, b), ab, bb) \<in> new_lookups\<^sup>*; ((ab, bb), ac, bc) \<in> new_lookups; a = ab \<and> b = bb\<rbrakk> \<Longrightarrow> a = ac \<and> b = bc \<or> ((a, b), ac, bc) \<in> new_lookups
 2. \<And>a b ab bb ac bc. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); kheap s pdp = Some (ArchObj (PageDirectory pd)); ((a, b), ab, bb) \<in> new_lookups\<^sup>*; ((ab, bb), ac, bc) \<in> new_lookups; ((a, b), ab, bb) \<in> new_lookups\<rbrakk> \<Longrightarrow> a = ac \<and> b = bc \<or> ((a, b), ac, bc) \<in> new_lookups
 3. \<And>a b aa ba. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); kheap s pdp = Some (ArchObj (PageDirectory pd)); a = aa \<and> b = ba \<or> ((a, b), aa, ba) \<in> new_lookups\<rbrakk> \<Longrightarrow> ((a, b), aa, ba) \<in> new_lookups\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a b ab bb ac bc. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); kheap s pdp = Some (ArchObj (PageDirectory pd)); ((a, b), ab, bb) \<in> new_lookups\<^sup>*; ((ab, bb), ac, bc) \<in> new_lookups; ((a, b), ab, bb) \<in> new_lookups\<rbrakk> \<Longrightarrow> a = ac \<and> b = bc \<or> ((a, b), ac, bc) \<in> new_lookups
 2. \<And>a b aa ba. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); kheap s pdp = Some (ArchObj (PageDirectory pd)); a = aa \<and> b = ba \<or> ((a, b), aa, ba) \<in> new_lookups\<rbrakk> \<Longrightarrow> ((a, b), aa, ba) \<in> new_lookups\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a b ab bb ac bc. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); kheap s pdp = Some (ArchObj (PageDirectory pd)); ((ab, bb), ac, bc) \<in> new_lookups; ((a, b), ab, bb) \<in> new_lookups\<rbrakk> \<Longrightarrow> a = ac \<and> b = bc \<or> ((a, b), ac, bc) \<in> new_lookups
 2. \<And>a b aa ba. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); kheap s pdp = Some (ArchObj (PageDirectory pd)); a = aa \<and> b = ba \<or> ((a, b), aa, ba) \<in> new_lookups\<rbrakk> \<Longrightarrow> ((a, b), aa, ba) \<in> new_lookups\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>a b ab bb ac bc. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); kheap s pdp = Some (ArchObj (PageDirectory pd)); ((ab, bb), ac, bc) \<in> new_lookups; ((a, b), ab, bb) \<in> new_lookups\<rbrakk> \<Longrightarrow> False
 2. \<And>a b aa ba. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); kheap s pdp = Some (ArchObj (PageDirectory pd)); a = aa \<and> b = ba \<or> ((a, b), aa, ba) \<in> new_lookups\<rbrakk> \<Longrightarrow> ((a, b), aa, ba) \<in> new_lookups\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>kheap s ap = Some (ArchObj (ASIDPool pool)); kheap s pdp = Some (ArchObj (PageDirectory pd)); a = aa \<and> b = ba \<or> ((a, b), aa, ba) \<in> new_lookups\<rbrakk> \<Longrightarrow> ((a, b), aa, ba) \<in> new_lookups\<^sup>* proof (prove)
goal:
No subgoals!