theory ADT_C

lemma cpspace_asidpool_relation_unique:
  assumes invs: "\<forall>x\<in>ran (map_to_asidpools ah). wf_asid_pool' x"
                "\<forall>x\<in>ran (map_to_asidpools ah'). wf_asid_pool' x"
  assumes rels: "cpspace_asidpool_relation ah ch"
                "cpspace_asidpool_relation ah' ch"
  shows   "map_to_asidpools ah' = map_to_asidpools ah" 
  (* FIXME: Should we generalize cmap_relation_unique, instead? *)
   using rels apply (clarsimp simp add: cmap_relation_def) apply (drule inj_image_inv[OF inj_Ptr])+ apply simp apply (rule ext) apply (case_tac "x:dom (map_to_asidpools ah)") apply (drule bspec, assumption)+ apply (simp add: dom_def Collect_eq, drule_tac x=x in spec) using invs apply (clarsimp simp: casid_pool_relation_def Let_def
                  split: asidpool.splits asid_pool_C.splits) apply (rename_tac "fun" array) apply (drule bspec, fastforce)+ apply (drule array_relation_to_map)+ apply (rule ext, rename_tac y) apply (drule_tac x=y in spec)+ apply clarsimp apply (case_tac "y\<le>2^asid_low_bits - 1", simp) apply (drule_tac s="option_to_ptr (fun y)" in sym) apply (simp add: option_to_ptr_def option_to_0_def ran_def
              split: option.splits) apply (simp add: atLeastAtMost_def atLeast_def atMost_def dom_def
                    Collect_mono2) apply (drule_tac x=y in spec)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_to_asidpools ah' = map_to_asidpools ah proof (prove)
goal (1 subgoal):
 1. map_to_asidpools ah' = map_to_asidpools ah proof (prove)
using this:
cmap_relation (map_to_asidpools ah) (clift ch) ap_Ptr casid_pool_relation
cmap_relation (map_to_asidpools ah') (clift ch) ap_Ptr casid_pool_relation

goal (1 subgoal):
 1. map_to_asidpools ah' = map_to_asidpools ah proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ap_Ptr ` dom (map_to_asidpools ah) = dom (clift ch); \<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah x)) (the (clift ch (ap_Ptr x))); ap_Ptr ` dom (map_to_asidpools ah') = dom (clift ch); \<forall>x\<in>dom (map_to_asidpools ah'). casid_pool_relation (the (map_to_asidpools ah' x)) (the (clift ch (ap_Ptr x)))\<rbrakk> \<Longrightarrow> map_to_asidpools ah' = map_to_asidpools ah proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah x)) (the (clift ch (ap_Ptr x))); \<forall>x\<in>dom (map_to_asidpools ah'). casid_pool_relation (the (map_to_asidpools ah' x)) (the (clift ch (ap_Ptr x))); inv ap_Ptr ` dom (clift ch) = dom (map_to_asidpools ah); inv ap_Ptr ` dom (clift ch) = dom (map_to_asidpools ah')\<rbrakk> \<Longrightarrow> map_to_asidpools ah' = map_to_asidpools ah proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah x)) (the (clift ch (ap_Ptr x))); \<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah' x)) (the (clift ch (ap_Ptr x))); dom (map_to_asidpools ah') = dom (map_to_asidpools ah); inv ap_Ptr ` dom (clift ch) = dom (map_to_asidpools ah)\<rbrakk> \<Longrightarrow> map_to_asidpools ah' = map_to_asidpools ah proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah x)) (the (clift ch (ap_Ptr x))); \<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah' x)) (the (clift ch (ap_Ptr x))); dom (map_to_asidpools ah') = dom (map_to_asidpools ah); inv ap_Ptr ` dom (clift ch) = dom (map_to_asidpools ah)\<rbrakk> \<Longrightarrow> map_to_asidpools ah' x = map_to_asidpools ah x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah x)) (the (clift ch (ap_Ptr x))); \<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah' x)) (the (clift ch (ap_Ptr x))); dom (map_to_asidpools ah') = dom (map_to_asidpools ah); inv ap_Ptr ` dom (clift ch) = dom (map_to_asidpools ah); x \<in> dom (map_to_asidpools ah)\<rbrakk> \<Longrightarrow> map_to_asidpools ah' x = map_to_asidpools ah x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah x)) (the (clift ch (ap_Ptr x))); \<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah' x)) (the (clift ch (ap_Ptr x))); dom (map_to_asidpools ah') = dom (map_to_asidpools ah); inv ap_Ptr ` dom (clift ch) = dom (map_to_asidpools ah); x \<notin> dom (map_to_asidpools ah)\<rbrakk> \<Longrightarrow> map_to_asidpools ah' x = map_to_asidpools ah x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>dom (map_to_asidpools ah') = dom (map_to_asidpools ah); inv ap_Ptr ` dom (clift ch) = dom (map_to_asidpools ah); x \<in> dom (map_to_asidpools ah); casid_pool_relation (the (map_to_asidpools ah x)) (the (clift ch (ap_Ptr x))); casid_pool_relation (the (map_to_asidpools ah' x)) (the (clift ch (ap_Ptr x)))\<rbrakk> \<Longrightarrow> map_to_asidpools ah' x = map_to_asidpools ah x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah x)) (the (clift ch (ap_Ptr x))); \<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah' x)) (the (clift ch (ap_Ptr x))); dom (map_to_asidpools ah') = dom (map_to_asidpools ah); inv ap_Ptr ` dom (clift ch) = dom (map_to_asidpools ah); x \<notin> dom (map_to_asidpools ah)\<rbrakk> \<Longrightarrow> map_to_asidpools ah' x = map_to_asidpools ah x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>inv ap_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_asidpools ah a = Some y}; \<exists>y. map_to_asidpools ah x = Some y; casid_pool_relation (the (map_to_asidpools ah x)) (the (clift ch (ap_Ptr x))); casid_pool_relation (the (map_to_asidpools ah' x)) (the (clift ch (ap_Ptr x))); (\<exists>y. map_to_asidpools ah' x = Some y) = (\<exists>y. map_to_asidpools ah x = Some y)\<rbrakk> \<Longrightarrow> map_to_asidpools ah' x = map_to_asidpools ah x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah x)) (the (clift ch (ap_Ptr x))); \<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah' x)) (the (clift ch (ap_Ptr x))); dom (map_to_asidpools ah') = dom (map_to_asidpools ah); inv ap_Ptr ` dom (clift ch) = dom (map_to_asidpools ah); x \<notin> dom (map_to_asidpools ah)\<rbrakk> \<Longrightarrow> map_to_asidpools ah' x = map_to_asidpools ah x proof (prove)
using this:
\<forall>x\<in>ran (map_to_asidpools ah). wf_asid_pool' x
\<forall>x\<in>ran (map_to_asidpools ah'). wf_asid_pool' x

goal (2 subgoals):
 1. \<And>x. \<lbrakk>inv ap_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_asidpools ah a = Some y}; \<exists>y. map_to_asidpools ah x = Some y; casid_pool_relation (the (map_to_asidpools ah x)) (the (clift ch (ap_Ptr x))); casid_pool_relation (the (map_to_asidpools ah' x)) (the (clift ch (ap_Ptr x))); (\<exists>y. map_to_asidpools ah' x = Some y) = (\<exists>y. map_to_asidpools ah x = Some y)\<rbrakk> \<Longrightarrow> map_to_asidpools ah' x = map_to_asidpools ah x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah x)) (the (clift ch (ap_Ptr x))); \<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah' x)) (the (clift ch (ap_Ptr x))); dom (map_to_asidpools ah') = dom (map_to_asidpools ah); inv ap_Ptr ` dom (clift ch) = dom (map_to_asidpools ah); x \<notin> dom (map_to_asidpools ah)\<rbrakk> \<Longrightarrow> map_to_asidpools ah' x = map_to_asidpools ah x proof (prove)
goal (2 subgoals):
 1. \<And>x xa xb xc. \<lbrakk>array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_low_bits - 1) xb xc; \<forall>x\<in>ran (map_to_asidpools ah). wf_asid_pool' x; \<forall>x\<in>ran (map_to_asidpools ah'). wf_asid_pool' x; inv ap_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_asidpools ah a = Some y}; map_to_asidpools ah' x = Some (asidpool.ASIDPool xb); map_to_asidpools ah x = Some (asidpool.ASIDPool xa); the (clift ch (ap_Ptr x)) = asid_pool_C.asid_pool_C xc; array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_low_bits - 1) xa xc\<rbrakk> \<Longrightarrow> xb = xa
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah x)) (the (clift ch (ap_Ptr x))); \<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah' x)) (the (clift ch (ap_Ptr x))); dom (map_to_asidpools ah') = dom (map_to_asidpools ah); inv ap_Ptr ` dom (clift ch) = dom (map_to_asidpools ah); x \<notin> dom (map_to_asidpools ah)\<rbrakk> \<Longrightarrow> map_to_asidpools ah' x = map_to_asidpools ah x proof (prove)
goal (2 subgoals):
 1. \<And>x xa fun array. \<lbrakk>array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_low_bits - 1) fun array; \<forall>x\<in>ran (map_to_asidpools ah). wf_asid_pool' x; \<forall>x\<in>ran (map_to_asidpools ah'). wf_asid_pool' x; inv ap_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_asidpools ah a = Some y}; map_to_asidpools ah' x = Some (asidpool.ASIDPool fun); map_to_asidpools ah x = Some (asidpool.ASIDPool xa); the (clift ch (ap_Ptr x)) = asid_pool_C.asid_pool_C array; array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_low_bits - 1) xa array\<rbrakk> \<Longrightarrow> fun = xa
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah x)) (the (clift ch (ap_Ptr x))); \<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah' x)) (the (clift ch (ap_Ptr x))); dom (map_to_asidpools ah') = dom (map_to_asidpools ah); inv ap_Ptr ` dom (clift ch) = dom (map_to_asidpools ah); x \<notin> dom (map_to_asidpools ah)\<rbrakk> \<Longrightarrow> map_to_asidpools ah' x = map_to_asidpools ah x proof (prove)
goal (2 subgoals):
 1. \<And>x xa fun array. \<lbrakk>array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_low_bits - 1) fun array; inv ap_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_asidpools ah a = Some y}; map_to_asidpools ah' x = Some (asidpool.ASIDPool fun); map_to_asidpools ah x = Some (asidpool.ASIDPool xa); the (clift ch (ap_Ptr x)) = asid_pool_C.asid_pool_C array; array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_low_bits - 1) xa array; wf_asid_pool' (asidpool.ASIDPool xa); wf_asid_pool' (asidpool.ASIDPool fun)\<rbrakk> \<Longrightarrow> fun = xa
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah x)) (the (clift ch (ap_Ptr x))); \<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah' x)) (the (clift ch (ap_Ptr x))); dom (map_to_asidpools ah') = dom (map_to_asidpools ah); inv ap_Ptr ` dom (clift ch) = dom (map_to_asidpools ah); x \<notin> dom (map_to_asidpools ah)\<rbrakk> \<Longrightarrow> map_to_asidpools ah' x = map_to_asidpools ah x proof (prove)
goal (2 subgoals):
 1. \<And>x xa fun array. \<lbrakk>inv ap_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_asidpools ah a = Some y}; map_to_asidpools ah' x = Some (asidpool.ASIDPool fun); map_to_asidpools ah x = Some (asidpool.ASIDPool xa); the (clift ch (ap_Ptr x)) = asid_pool_C.asid_pool_C array; wf_asid_pool' (asidpool.ASIDPool xa); wf_asid_pool' (asidpool.ASIDPool fun); \<forall>i\<le>2 ^ local.asid_low_bits - 1. ((=) \<circ> option_to_ptr) (fun i) (the (array_to_map (2 ^ local.asid_low_bits - 1) array i)); \<forall>i\<le>2 ^ local.asid_low_bits - 1. ((=) \<circ> option_to_ptr) (xa i) (the (array_to_map (2 ^ local.asid_low_bits - 1) array i))\<rbrakk> \<Longrightarrow> fun = xa
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah x)) (the (clift ch (ap_Ptr x))); \<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah' x)) (the (clift ch (ap_Ptr x))); dom (map_to_asidpools ah') = dom (map_to_asidpools ah); inv ap_Ptr ` dom (clift ch) = dom (map_to_asidpools ah); x \<notin> dom (map_to_asidpools ah)\<rbrakk> \<Longrightarrow> map_to_asidpools ah' x = map_to_asidpools ah x proof (prove)
goal (2 subgoals):
 1. \<And>x xa fun array y. \<lbrakk>inv ap_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_asidpools ah a = Some y}; map_to_asidpools ah' x = Some (asidpool.ASIDPool fun); map_to_asidpools ah x = Some (asidpool.ASIDPool xa); the (clift ch (ap_Ptr x)) = asid_pool_C.asid_pool_C array; wf_asid_pool' (asidpool.ASIDPool xa); wf_asid_pool' (asidpool.ASIDPool fun); \<forall>i\<le>2 ^ local.asid_low_bits - 1. ((=) \<circ> option_to_ptr) (fun i) (the (array_to_map (2 ^ local.asid_low_bits - 1) array i)); \<forall>i\<le>2 ^ local.asid_low_bits - 1. ((=) \<circ> option_to_ptr) (xa i) (the (array_to_map (2 ^ local.asid_low_bits - 1) array i))\<rbrakk> \<Longrightarrow> fun y = xa y
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah x)) (the (clift ch (ap_Ptr x))); \<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah' x)) (the (clift ch (ap_Ptr x))); dom (map_to_asidpools ah') = dom (map_to_asidpools ah); inv ap_Ptr ` dom (clift ch) = dom (map_to_asidpools ah); x \<notin> dom (map_to_asidpools ah)\<rbrakk> \<Longrightarrow> map_to_asidpools ah' x = map_to_asidpools ah x proof (prove)
goal (2 subgoals):
 1. \<And>x xa fun array y. \<lbrakk>inv ap_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_asidpools ah a = Some y}; map_to_asidpools ah' x = Some (asidpool.ASIDPool fun); map_to_asidpools ah x = Some (asidpool.ASIDPool xa); the (clift ch (ap_Ptr x)) = asid_pool_C.asid_pool_C array; wf_asid_pool' (asidpool.ASIDPool xa); wf_asid_pool' (asidpool.ASIDPool fun); y \<le> 2 ^ local.asid_low_bits - 1 \<longrightarrow> ((=) \<circ> option_to_ptr) (fun y) (the (array_to_map (2 ^ local.asid_low_bits - 1) array y)); y \<le> 2 ^ local.asid_low_bits - 1 \<longrightarrow> ((=) \<circ> option_to_ptr) (xa y) (the (array_to_map (2 ^ local.asid_low_bits - 1) array y))\<rbrakk> \<Longrightarrow> fun y = xa y
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah x)) (the (clift ch (ap_Ptr x))); \<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah' x)) (the (clift ch (ap_Ptr x))); dom (map_to_asidpools ah') = dom (map_to_asidpools ah); inv ap_Ptr ` dom (clift ch) = dom (map_to_asidpools ah); x \<notin> dom (map_to_asidpools ah)\<rbrakk> \<Longrightarrow> map_to_asidpools ah' x = map_to_asidpools ah x proof (prove)
goal (2 subgoals):
 1. \<And>x xa fun array y. \<lbrakk>inv ap_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_asidpools ah a = Some y}; map_to_asidpools ah' x = Some (asidpool.ASIDPool fun); map_to_asidpools ah x = Some (asidpool.ASIDPool xa); the (clift ch (ap_Ptr x)) = asid_pool_C.asid_pool_C array; y \<le> 2 ^ local.asid_low_bits - 1 \<longrightarrow> option_to_ptr (fun y) = the (array_to_map (2 ^ local.asid_low_bits - 1) array y); y \<le> 2 ^ local.asid_low_bits - 1 \<longrightarrow> option_to_ptr (xa y) = the (array_to_map (2 ^ local.asid_low_bits - 1) array y); dom xa \<subseteq> {0..2 ^ local.asid_low_bits - 1}; dom fun \<subseteq> {0..2 ^ local.asid_low_bits - 1}; 0 \<notin> ran xa; \<forall>x\<in>ran xa. is_aligned x pdBits; 0 \<notin> ran fun; \<forall>x\<in>ran fun. is_aligned x pdBits\<rbrakk> \<Longrightarrow> fun y = xa y
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah x)) (the (clift ch (ap_Ptr x))); \<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah' x)) (the (clift ch (ap_Ptr x))); dom (map_to_asidpools ah') = dom (map_to_asidpools ah); inv ap_Ptr ` dom (clift ch) = dom (map_to_asidpools ah); x \<notin> dom (map_to_asidpools ah)\<rbrakk> \<Longrightarrow> map_to_asidpools ah' x = map_to_asidpools ah x proof (prove)
goal (3 subgoals):
 1. \<And>x xa fun array y. \<lbrakk>inv ap_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_asidpools ah a = Some y}; map_to_asidpools ah' x = Some (asidpool.ASIDPool fun); map_to_asidpools ah x = Some (asidpool.ASIDPool xa); the (clift ch (ap_Ptr x)) = asid_pool_C.asid_pool_C array; option_to_ptr (fun y) = the (array_to_map (2 ^ local.asid_low_bits - 1) array y); option_to_ptr (xa y) = the (array_to_map (2 ^ local.asid_low_bits - 1) array y); dom xa \<subseteq> {0..2 ^ local.asid_low_bits - 1}; dom fun \<subseteq> {0..2 ^ local.asid_low_bits - 1}; 0 \<notin> ran xa; \<forall>x\<in>ran xa. is_aligned x pdBits; 0 \<notin> ran fun; \<forall>x\<in>ran fun. is_aligned x pdBits; y \<le> 2 ^ local.asid_low_bits - 1\<rbrakk> \<Longrightarrow> fun y = xa y
 2. \<And>x xa fun array y. \<lbrakk>inv ap_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_asidpools ah a = Some y}; map_to_asidpools ah' x = Some (asidpool.ASIDPool fun); map_to_asidpools ah x = Some (asidpool.ASIDPool xa); the (clift ch (ap_Ptr x)) = asid_pool_C.asid_pool_C array; y \<le> 2 ^ local.asid_low_bits - 1 \<longrightarrow> option_to_ptr (fun y) = the (array_to_map (2 ^ local.asid_low_bits - 1) array y); y \<le> 2 ^ local.asid_low_bits - 1 \<longrightarrow> option_to_ptr (xa y) = the (array_to_map (2 ^ local.asid_low_bits - 1) array y); dom xa \<subseteq> {0..2 ^ local.asid_low_bits - 1}; dom fun \<subseteq> {0..2 ^ local.asid_low_bits - 1}; 0 \<notin> ran xa; \<forall>x\<in>ran xa. is_aligned x pdBits; 0 \<notin> ran fun; \<forall>x\<in>ran fun. is_aligned x pdBits; \<not> y \<le> 2 ^ local.asid_low_bits - 1\<rbrakk> \<Longrightarrow> fun y = xa y
 3. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah x)) (the (clift ch (ap_Ptr x))); \<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah' x)) (the (clift ch (ap_Ptr x))); dom (map_to_asidpools ah') = dom (map_to_asidpools ah); inv ap_Ptr ` dom (clift ch) = dom (map_to_asidpools ah); x \<notin> dom (map_to_asidpools ah)\<rbrakk> \<Longrightarrow> map_to_asidpools ah' x = map_to_asidpools ah x proof (prove)
goal (3 subgoals):
 1. \<And>x xa fun array y. \<lbrakk>inv ap_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_asidpools ah a = Some y}; map_to_asidpools ah' x = Some (asidpool.ASIDPool fun); map_to_asidpools ah x = Some (asidpool.ASIDPool xa); the (clift ch (ap_Ptr x)) = asid_pool_C.asid_pool_C array; option_to_ptr (xa y) = the (array_to_map (2 ^ local.asid_low_bits - 1) array y); dom xa \<subseteq> {0..2 ^ local.asid_low_bits - 1}; dom fun \<subseteq> {0..2 ^ local.asid_low_bits - 1}; 0 \<notin> ran xa; \<forall>x\<in>ran xa. is_aligned x pdBits; 0 \<notin> ran fun; \<forall>x\<in>ran fun. is_aligned x pdBits; y \<le> 2 ^ local.asid_low_bits - 1; the (array_to_map (2 ^ local.asid_low_bits - 1) array y) = option_to_ptr (fun y)\<rbrakk> \<Longrightarrow> fun y = xa y
 2. \<And>x xa fun array y. \<lbrakk>inv ap_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_asidpools ah a = Some y}; map_to_asidpools ah' x = Some (asidpool.ASIDPool fun); map_to_asidpools ah x = Some (asidpool.ASIDPool xa); the (clift ch (ap_Ptr x)) = asid_pool_C.asid_pool_C array; y \<le> 2 ^ local.asid_low_bits - 1 \<longrightarrow> option_to_ptr (fun y) = the (array_to_map (2 ^ local.asid_low_bits - 1) array y); y \<le> 2 ^ local.asid_low_bits - 1 \<longrightarrow> option_to_ptr (xa y) = the (array_to_map (2 ^ local.asid_low_bits - 1) array y); dom xa \<subseteq> {0..2 ^ local.asid_low_bits - 1}; dom fun \<subseteq> {0..2 ^ local.asid_low_bits - 1}; 0 \<notin> ran xa; \<forall>x\<in>ran xa. is_aligned x pdBits; 0 \<notin> ran fun; \<forall>x\<in>ran fun. is_aligned x pdBits; \<not> y \<le> 2 ^ local.asid_low_bits - 1\<rbrakk> \<Longrightarrow> fun y = xa y
 3. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah x)) (the (clift ch (ap_Ptr x))); \<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah' x)) (the (clift ch (ap_Ptr x))); dom (map_to_asidpools ah') = dom (map_to_asidpools ah); inv ap_Ptr ` dom (clift ch) = dom (map_to_asidpools ah); x \<notin> dom (map_to_asidpools ah)\<rbrakk> \<Longrightarrow> map_to_asidpools ah' x = map_to_asidpools ah x proof (prove)
goal (2 subgoals):
 1. \<And>x xa fun array y. \<lbrakk>inv ap_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_asidpools ah a = Some y}; map_to_asidpools ah' x = Some (asidpool.ASIDPool fun); map_to_asidpools ah x = Some (asidpool.ASIDPool xa); the (clift ch (ap_Ptr x)) = asid_pool_C.asid_pool_C array; y \<le> 2 ^ local.asid_low_bits - 1 \<longrightarrow> option_to_ptr (fun y) = the (array_to_map (2 ^ local.asid_low_bits - 1) array y); y \<le> 2 ^ local.asid_low_bits - 1 \<longrightarrow> option_to_ptr (xa y) = the (array_to_map (2 ^ local.asid_low_bits - 1) array y); dom xa \<subseteq> {0..2 ^ local.asid_low_bits - 1}; dom fun \<subseteq> {0..2 ^ local.asid_low_bits - 1}; 0 \<notin> ran xa; \<forall>x\<in>ran xa. is_aligned x pdBits; 0 \<notin> ran fun; \<forall>x\<in>ran fun. is_aligned x pdBits; \<not> y \<le> 2 ^ local.asid_low_bits - 1\<rbrakk> \<Longrightarrow> fun y = xa y
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah x)) (the (clift ch (ap_Ptr x))); \<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah' x)) (the (clift ch (ap_Ptr x))); dom (map_to_asidpools ah') = dom (map_to_asidpools ah); inv ap_Ptr ` dom (clift ch) = dom (map_to_asidpools ah); x \<notin> dom (map_to_asidpools ah)\<rbrakk> \<Longrightarrow> map_to_asidpools ah' x = map_to_asidpools ah x proof (prove)
goal (2 subgoals):
 1. \<And>x xa fun array y. \<lbrakk>inv ap_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_asidpools ah a = Some y}; map_to_asidpools ah' x = Some (asidpool.ASIDPool fun); map_to_asidpools ah x = Some (asidpool.ASIDPool xa); the (clift ch (ap_Ptr x)) = asid_pool_C.asid_pool_C array; \<forall>x. (\<exists>y. xa x = Some y) \<longrightarrow> x \<le> 2 ^ local.asid_low_bits - 1; \<forall>x. (\<exists>y. fun x = Some y) \<longrightarrow> x \<le> 2 ^ local.asid_low_bits - 1; 0 \<notin> ran xa; \<forall>x\<in>ran xa. is_aligned x pdBits; 0 \<notin> ran fun; \<forall>x\<in>ran fun. is_aligned x pdBits; \<not> y \<le> 2 ^ local.asid_low_bits - 1\<rbrakk> \<Longrightarrow> fun y = xa y
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah x)) (the (clift ch (ap_Ptr x))); \<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah' x)) (the (clift ch (ap_Ptr x))); dom (map_to_asidpools ah') = dom (map_to_asidpools ah); inv ap_Ptr ` dom (clift ch) = dom (map_to_asidpools ah); x \<notin> dom (map_to_asidpools ah)\<rbrakk> \<Longrightarrow> map_to_asidpools ah' x = map_to_asidpools ah x proof (prove)
goal (2 subgoals):
 1. \<And>x xa fun array y. \<lbrakk>inv ap_Ptr ` {a. \<exists>y. clift ch a = Some y} = {a. \<exists>y. map_to_asidpools ah a = Some y}; map_to_asidpools ah' x = Some (asidpool.ASIDPool fun); map_to_asidpools ah x = Some (asidpool.ASIDPool xa); the (clift ch (ap_Ptr x)) = asid_pool_C.asid_pool_C array; 0 \<notin> ran xa; \<forall>x\<in>ran xa. is_aligned x pdBits; 0 \<notin> ran fun; \<forall>x\<in>ran fun. is_aligned x pdBits; \<not> y \<le> 2 ^ local.asid_low_bits - 1; (\<exists>ya. xa y = Some ya) \<longrightarrow> y \<le> 2 ^ local.asid_low_bits - 1; (\<exists>ya. fun y = Some ya) \<longrightarrow> y \<le> 2 ^ local.asid_low_bits - 1\<rbrakk> \<Longrightarrow> fun y = xa y
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah x)) (the (clift ch (ap_Ptr x))); \<forall>x\<in>dom (map_to_asidpools ah). casid_pool_relation (the (map_to_asidpools ah' x)) (the (clift ch (ap_Ptr x))); dom (map_to_asidpools ah') = dom (map_to_asidpools ah); inv ap_Ptr ` dom (clift ch) = dom (map_to_asidpools ah); x \<notin> dom (map_to_asidpools ah)\<rbrakk> \<Longrightarrow> map_to_asidpools ah' x = map_to_asidpools ah x proof (prove)
goal:
No subgoals!