theory ArchArch_IF

lemma arch_perform_invocation_reads_respects_g:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows "reads_respects_g aag l (ct_active and authorised_arch_inv aag ai and valid_arch_inv ai
                                           and authorised_for_globals_arch_inv ai and invs
                                           and pas_refined aag and is_subject aag \<circ> cur_thread)
                          (arch_perform_invocation ai)" apply (rule equiv_valid_guard_imp) apply (rule reads_respects_g) apply (rule arch_perform_invocation_reads_respects[OF domains_distinct]) apply (rule doesnt_touch_globalsI) apply (wp arch_perform_invocation_globals_equiv) apply (simp add: invs_valid_vs_lookup invs_def valid_state_def valid_pspace_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (ct_active and authorised_arch_inv aag ai and valid_arch_inv ai and authorised_for_globals_arch_inv ai and invs and pas_refined aag and is_subject aag \<circ> cur_thread) (arch_perform_invocation ai) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?Q (arch_perform_invocation ai)
 2. \<And>s. (ct_active and authorised_arch_inv aag ai and valid_arch_inv ai and authorised_for_globals_arch_inv ai and invs and pas_refined aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. reads_respects aag l ?P3 (arch_perform_invocation ai)
 2. doesnt_touch_globals ?Q3 (arch_perform_invocation ai)
 3. \<And>s. (ct_active and authorised_arch_inv aag ai and valid_arch_inv ai and authorised_for_globals_arch_inv ai and invs and pas_refined aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> (?P3 and ?Q3) s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q3 (arch_perform_invocation ai)
 2. \<And>s. (ct_active and authorised_arch_inv aag ai and valid_arch_inv ai and authorised_for_globals_arch_inv ai and invs and pas_refined aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and authorised_arch_inv aag ai and valid_arch_inv ai and is_subject aag \<circ> cur_thread and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>globals_equiv st and ?Q3\<rbrace> arch_perform_invocation ai \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. (ct_active and authorised_arch_inv aag ai and valid_arch_inv ai and authorised_for_globals_arch_inv ai and invs and pas_refined aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and authorised_arch_inv aag ai and valid_arch_inv ai and is_subject aag \<circ> cur_thread and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<And>st s. (globals_equiv st and ?Q3) s \<Longrightarrow> (globals_equiv st and invs and ct_active and valid_arch_inv ai and authorised_for_globals_arch_inv ai) s
 2. \<And>s. (ct_active and authorised_arch_inv aag ai and valid_arch_inv ai and authorised_for_globals_arch_inv ai and invs and pas_refined aag and is_subject aag \<circ> cur_thread) s \<Longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and authorised_arch_inv aag ai and valid_arch_inv ai and is_subject aag \<circ> cur_thread and ?Q3) s proof (prove)
goal:
No subgoals!