theory VSpace_C

lemma asid_map_pd_to_hwasids_clear:
  "\<lbrakk> pd \<notin> ran (option_map snd \<circ> m |` (- {asid}));
         \<forall>hw_asid pd'. m asid = Some (hw_asid, pd') \<longrightarrow> pd' = pd \<rbrakk> \<Longrightarrow>
   asid_map_pd_to_hwasids (m (asid := None))
        = (asid_map_pd_to_hwasids m) (pd := {})" apply (rule ext, rule set_eqI) apply (simp add: asid_map_pd_to_hwasids_def split: if_split) apply (intro conjI impI) apply (clarsimp elim!: ranE split: if_split_asm) apply (erule notE, rule ranI, simp add: restrict_map_def) apply (subst if_P, assumption) apply simp apply (simp add: ran_def split: if_split) apply (rule iffI) apply fastforce apply (erule exEI) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pd \<notin> ran (map_option snd \<circ> m|\<^bsub>(- {asid})\<^esub>); \<forall>hw_asid pd'. m asid = Some (hw_asid, pd') \<longrightarrow> pd' = pd\<rbrakk> \<Longrightarrow> asid_map_pd_to_hwasids (m(asid := None)) = (asid_map_pd_to_hwasids m)(pd := {}) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>pd \<notin> ran (map_option snd \<circ> m|\<^bsub>(- {asid})\<^esub>); \<forall>hw_asid pd'. m asid = Some (hw_asid, pd') \<longrightarrow> pd' = pd\<rbrakk> \<Longrightarrow> (xa \<in> asid_map_pd_to_hwasids (m(asid := None)) x) = (xa \<in> ((asid_map_pd_to_hwasids m)(pd := {})) x) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>pd \<notin> ran (map_option snd \<circ> m|\<^bsub>(- {asid})\<^esub>); \<forall>hw_asid pd'. m asid = Some (hw_asid, pd') \<longrightarrow> pd' = pd\<rbrakk> \<Longrightarrow> (x = pd \<longrightarrow> (xa, pd) \<notin> ran (m(asid := None))) \<and> (x \<noteq> pd \<longrightarrow> ((xa, x) \<in> ran (m(asid := None))) = ((xa, x) \<in> ran m)) proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>pd \<notin> ran (map_option snd \<circ> m|\<^bsub>(- {asid})\<^esub>); \<forall>hw_asid pd'. m asid = Some (hw_asid, pd') \<longrightarrow> pd' = pd; x = pd\<rbrakk> \<Longrightarrow> (xa, pd) \<notin> ran (m(asid := None))
 2. \<And>x xa. \<lbrakk>pd \<notin> ran (map_option snd \<circ> m|\<^bsub>(- {asid})\<^esub>); \<forall>hw_asid pd'. m asid = Some (hw_asid, pd') \<longrightarrow> pd' = pd; x \<noteq> pd\<rbrakk> \<Longrightarrow> ((xa, x) \<in> ran (m(asid := None))) = ((xa, x) \<in> ran m) proof (prove)
goal (2 subgoals):
 1. \<And>xa xb. \<lbrakk>pd \<notin> ran (map_option snd \<circ> m|\<^bsub>(- {asid})\<^esub>); \<forall>hw_asid pd'. m asid = Some (hw_asid, pd') \<longrightarrow> pd' = pd; xb \<noteq> asid; m xb = Some (xa, pd)\<rbrakk> \<Longrightarrow> False
 2. \<And>x xa. \<lbrakk>pd \<notin> ran (map_option snd \<circ> m|\<^bsub>(- {asid})\<^esub>); \<forall>hw_asid pd'. m asid = Some (hw_asid, pd') \<longrightarrow> pd' = pd; x \<noteq> pd\<rbrakk> \<Longrightarrow> ((xa, x) \<in> ran (m(asid := None))) = ((xa, x) \<in> ran m) proof (prove)
goal (2 subgoals):
 1. \<And>xa xb. \<lbrakk>\<forall>hw_asid pd'. m asid = Some (hw_asid, pd') \<longrightarrow> pd' = pd; xb \<noteq> asid; m xb = Some (xa, pd)\<rbrakk> \<Longrightarrow> \<exists>a. (if ?a29 xa xb \<noteq> asid then m (?a29 xa xb) else None) = Some (a, pd)
 2. \<And>x xa. \<lbrakk>pd \<notin> ran (map_option snd \<circ> m|\<^bsub>(- {asid})\<^esub>); \<forall>hw_asid pd'. m asid = Some (hw_asid, pd') \<longrightarrow> pd' = pd; x \<noteq> pd\<rbrakk> \<Longrightarrow> ((xa, x) \<in> ran (m(asid := None))) = ((xa, x) \<in> ran m) proof (prove)
goal (2 subgoals):
 1. \<And>xa xb. \<lbrakk>\<forall>hw_asid pd'. m asid = Some (hw_asid, pd') \<longrightarrow> pd' = pd; xb \<noteq> asid; m xb = Some (xa, pd)\<rbrakk> \<Longrightarrow> \<exists>a. m xb = Some (a, pd)
 2. \<And>x xa. \<lbrakk>pd \<notin> ran (map_option snd \<circ> m|\<^bsub>(- {asid})\<^esub>); \<forall>hw_asid pd'. m asid = Some (hw_asid, pd') \<longrightarrow> pd' = pd; x \<noteq> pd\<rbrakk> \<Longrightarrow> ((xa, x) \<in> ran (m(asid := None))) = ((xa, x) \<in> ran m) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>pd \<notin> ran (map_option snd \<circ> m|\<^bsub>(- {asid})\<^esub>); \<forall>hw_asid pd'. m asid = Some (hw_asid, pd') \<longrightarrow> pd' = pd; x \<noteq> pd\<rbrakk> \<Longrightarrow> ((xa, x) \<in> ran (m(asid := None))) = ((xa, x) \<in> ran m) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<forall>a aa. (m|\<^bsub>(- {asid})\<^esub>) a \<noteq> Some (aa, pd); \<forall>hw_asid pd'. m asid = Some (hw_asid, pd') \<longrightarrow> pd' = pd; x \<noteq> pd\<rbrakk> \<Longrightarrow> (\<exists>a. a \<noteq> asid \<and> (a \<noteq> asid \<longrightarrow> m a = Some (xa, x))) = (\<exists>a. m a = Some (xa, x)) proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>\<forall>a aa. (m|\<^bsub>(- {asid})\<^esub>) a \<noteq> Some (aa, pd); \<forall>hw_asid pd'. m asid = Some (hw_asid, pd') \<longrightarrow> pd' = pd; x \<noteq> pd; \<exists>a. a \<noteq> asid \<and> (a \<noteq> asid \<longrightarrow> m a = Some (xa, x))\<rbrakk> \<Longrightarrow> \<exists>a. m a = Some (xa, x)
 2. \<And>x xa. \<lbrakk>\<forall>a aa. (m|\<^bsub>(- {asid})\<^esub>) a \<noteq> Some (aa, pd); \<forall>hw_asid pd'. m asid = Some (hw_asid, pd') \<longrightarrow> pd' = pd; x \<noteq> pd; \<exists>a. m a = Some (xa, x)\<rbrakk> \<Longrightarrow> \<exists>a. a \<noteq> asid \<and> (a \<noteq> asid \<longrightarrow> m a = Some (xa, x)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<forall>a aa. (m|\<^bsub>(- {asid})\<^esub>) a \<noteq> Some (aa, pd); \<forall>hw_asid pd'. m asid = Some (hw_asid, pd') \<longrightarrow> pd' = pd; x \<noteq> pd; \<exists>a. m a = Some (xa, x)\<rbrakk> \<Longrightarrow> \<exists>a. a \<noteq> asid \<and> (a \<noteq> asid \<longrightarrow> m a = Some (xa, x)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>\<forall>a aa. (m|\<^bsub>(- {asid})\<^esub>) a \<noteq> Some (aa, pd); \<forall>hw_asid pd'. m asid = Some (hw_asid, pd') \<longrightarrow> pd' = pd; x \<noteq> pd; m xb = Some (xa, x)\<rbrakk> \<Longrightarrow> xb \<noteq> asid \<and> (xb \<noteq> asid \<longrightarrow> m xb = Some (xa, x)) proof (prove)
goal:
No subgoals!