theory VSpace_C

lemma asid_map_pd_to_hwasids_update:
  "\<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 \<mapsto> (hw_asid, pd)))
        = (asid_map_pd_to_hwasids m) (pd := {hw_asid})" apply (rule ext, rule set_eqI) apply (simp add: asid_map_pd_to_hwasids_def split: if_split) apply (intro conjI impI) apply (rule iffI) apply (rule ccontr, 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 (fastforce split: if_split) 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 \<mapsto> (hw_asid, pd))) = (asid_map_pd_to_hwasids m)(pd := {hw_asid}) 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 \<mapsto> (hw_asid, pd))) x) = (xa \<in> ((asid_map_pd_to_hwasids m)(pd := {hw_asid})) 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) \<in> ran (m(asid \<mapsto> (hw_asid, pd)))) = (xa = hw_asid)) \<and> (x \<noteq> pd \<longrightarrow> ((xa, x) \<in> ran (m(asid \<mapsto> (hw_asid, pd)))) = ((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) \<in> ran (m(asid \<mapsto> (hw_asid, pd)))) = (xa = hw_asid)
 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 \<mapsto> (hw_asid, pd)))) = ((xa, x) \<in> ran m) proof (prove)
goal (3 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; (xa, pd) \<in> ran (m(asid \<mapsto> (hw_asid, pd)))\<rbrakk> \<Longrightarrow> xa = hw_asid
 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 = pd; xa = hw_asid\<rbrakk> \<Longrightarrow> (xa, pd) \<in> ran (m(asid \<mapsto> (hw_asid, pd)))
 3. \<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 \<mapsto> (hw_asid, pd)))) = ((xa, x) \<in> ran m) proof (prove)
goal (3 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; xa \<noteq> hw_asid; 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 = pd; xa = hw_asid\<rbrakk> \<Longrightarrow> (xa, pd) \<in> ran (m(asid \<mapsto> (hw_asid, pd)))
 3. \<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 \<mapsto> (hw_asid, pd)))) = ((xa, x) \<in> ran m) proof (prove)
goal (3 subgoals):
 1. \<And>xa xb. \<lbrakk>\<forall>hw_asid pd'. m asid = Some (hw_asid, pd') \<longrightarrow> pd' = pd; xa \<noteq> hw_asid; xb \<noteq> asid; m xb = Some (xa, pd)\<rbrakk> \<Longrightarrow> \<exists>a. (if ?a33 xa xb \<noteq> asid then m (?a33 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 = pd; xa = hw_asid\<rbrakk> \<Longrightarrow> (xa, pd) \<in> ran (m(asid \<mapsto> (hw_asid, pd)))
 3. \<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 \<mapsto> (hw_asid, pd)))) = ((xa, x) \<in> ran m) proof (prove)
goal (3 subgoals):
 1. \<And>xa xb. \<lbrakk>\<forall>hw_asid pd'. m asid = Some (hw_asid, pd') \<longrightarrow> pd' = pd; xa \<noteq> hw_asid; 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 = pd; xa = hw_asid\<rbrakk> \<Longrightarrow> (xa, pd) \<in> ran (m(asid \<mapsto> (hw_asid, pd)))
 3. \<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 \<mapsto> (hw_asid, pd)))) = ((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; xa = hw_asid\<rbrakk> \<Longrightarrow> (xa, pd) \<in> ran (m(asid \<mapsto> (hw_asid, 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 \<mapsto> (hw_asid, pd)))) = ((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 \<mapsto> (hw_asid, pd)))) = ((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!