theory ArchVSpace_AI

lemma valid_arch_state_unmap_strg:
  "valid_arch_state s \<longrightarrow>
   valid_arch_state(s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (arm_asid_table (arch_state s))(ptr := None)\<rparr>\<rparr>)" apply (clarsimp simp: valid_arch_state_def valid_asid_table_def) apply (rule conjI) apply (clarsimp simp add: ran_def) apply blast apply (clarsimp simp: inj_on_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_state s \<longrightarrow> valid_arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(ptr := None)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> (\<forall>p\<in>ran ((asid_table s)(ptr := None)). typ_at (AArch AASIDPool) p s) \<and> inj_on ((asid_table s)(ptr := None)) (dom (asid_table s) - {ptr}) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> \<forall>p\<in>ran ((asid_table s)(ptr := None)). typ_at (AArch AASIDPool) p s
 2. \<lbrakk>\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> inj_on ((asid_table s)(ptr := None)) (dom (asid_table s) - {ptr}) proof (prove)
goal (2 subgoals):
 1. \<And>p a. \<lbrakk>\<forall>p. (\<exists>a. asid_table s a = Some p) \<longrightarrow> typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); a \<noteq> ptr; asid_table s a = Some p\<rbrakk> \<Longrightarrow> typ_at (AArch AASIDPool) p s
 2. \<lbrakk>\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> inj_on ((asid_table s)(ptr := None)) (dom (asid_table s) - {ptr}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> inj_on ((asid_table s)(ptr := None)) (dom (asid_table s) - {ptr}) proof (prove)
goal:
No subgoals!