theory VSpace_R

lemma invalidate_tlb_by_asid_corres_ex:
  "corres dc
          (\<lambda>s. asid \<le> mask asid_bits \<and> asid \<noteq> 0
            \<and> valid_asid_map s \<and> valid_vspace_objs s
            \<and> pspace_aligned s \<and> pspace_distinct s
            \<and> unique_table_refs (caps_of_state s)
            \<and> valid_global_objs s \<and> valid_vs_lookup s
            \<and> valid_arch_state s \<and> (\<exists>pd. vspace_at_asid asid pd s))
          (pspace_aligned' and pspace_distinct' and no_0_obj')
          (invalidate_tlb_by_asid asid) (invalidateTLBByASID asid)" apply (rule corres_name_pre, clarsimp) apply (rule corres_guard_imp) apply (rule_tac pd=pd in invalidateTLBByASID_corres) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>s. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0 \<and> valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> unique_table_refs (caps_of_state s) \<and> valid_global_objs s \<and> valid_vs_lookup s \<and> valid_arch_state s \<and> (\<exists>pd. vspace_at_asid asid pd s)) (pspace_aligned' and pspace_distinct' and no_0_obj') (invalidate_tlb_by_asid asid) (invalidateTLBByASID asid) proof (prove)
goal (1 subgoal):
 1. \<And>s s' pd. \<lbrakk>(s, s') \<in> state_relation; asid \<le> mask local.asid_bits; pspace_aligned' s'; asid \<noteq> 0; pspace_distinct' s'; no_0_obj' s'; valid_asid_map s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; unique_table_refs (caps_of_state s); valid_global_objs s; valid_vs_lookup s; valid_arch_state s; vspace_at_asid asid pd s\<rbrakk> \<Longrightarrow> corres dc ((=) s) ((=) s') (invalidate_tlb_by_asid asid) (invalidateTLBByASID asid) proof (prove)
goal (3 subgoals):
 1. \<And>s s' pd. \<lbrakk>(s, s') \<in> state_relation; asid \<le> mask local.asid_bits; pspace_aligned' s'; asid \<noteq> 0; pspace_distinct' s'; no_0_obj' s'; valid_asid_map s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; unique_table_refs (caps_of_state s); valid_global_objs s; valid_vs_lookup s; valid_arch_state s; vspace_at_asid asid pd s\<rbrakk> \<Longrightarrow> corres dc (?Q15 s s' pd) (?Q'15 s s' pd) (invalidate_tlb_by_asid asid) (invalidateTLBByASID asid)
 2. \<And>s s' pd sa. \<lbrakk>(s, s') \<in> state_relation; asid \<le> mask local.asid_bits; pspace_aligned' s'; asid \<noteq> 0; pspace_distinct' s'; no_0_obj' s'; valid_asid_map s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; unique_table_refs (caps_of_state s); valid_global_objs s; valid_vs_lookup s; valid_arch_state s; vspace_at_asid asid pd s; s = sa\<rbrakk> \<Longrightarrow> ?Q15 s s' pd sa
 3. \<And>s s' pd sa. \<lbrakk>(s, s') \<in> state_relation; asid \<le> mask local.asid_bits; pspace_aligned' s'; asid \<noteq> 0; pspace_distinct' s'; no_0_obj' s'; valid_asid_map s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; unique_table_refs (caps_of_state s); valid_global_objs s; valid_vs_lookup s; valid_arch_state s; vspace_at_asid asid pd s; s' = sa\<rbrakk> \<Longrightarrow> ?Q'15 s s' pd sa proof (prove)
goal (2 subgoals):
 1. \<And>s s' pd sa. \<lbrakk>(s, s') \<in> state_relation; asid \<le> mask local.asid_bits; pspace_aligned' s'; asid \<noteq> 0; pspace_distinct' s'; no_0_obj' s'; valid_asid_map s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; unique_table_refs (caps_of_state s); valid_global_objs s; valid_vs_lookup s; valid_arch_state s; vspace_at_asid asid pd s; s = sa\<rbrakk> \<Longrightarrow> (K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd) sa
 2. \<And>s s' pd sa. \<lbrakk>(s, s') \<in> state_relation; asid \<le> mask local.asid_bits; pspace_aligned' s'; asid \<noteq> 0; pspace_distinct' s'; no_0_obj' s'; valid_asid_map s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; unique_table_refs (caps_of_state s); valid_global_objs s; valid_vs_lookup s; valid_arch_state s; vspace_at_asid asid pd s; s' = sa\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj') sa proof (prove)
goal:
No subgoals!