theory PasUpdates

lemma pas_refined_pasSubject_update':
  "\<lbrakk> pas_refined aag s; pas_wellformed (aag\<lparr>pasSubject := x\<rparr>) \<rbrakk>
     \<Longrightarrow> pas_refined (aag\<lparr>pasSubject := x\<rparr>) s" apply (subst pas_refined_def) apply (safe del: subsetI) apply (simp add: irq_map_wellformed_pasSubject_update pas_refined_def) apply (simp add: tcb_domain_map_wellformed_pasSubject_update pas_refined_def) apply (clarsimp simp: pas_refined_def) apply (clarsimp simp: pas_refined_def state_asids_to_policy_pasSubject_update) apply (fastforce simp: pas_refined_def state_irqs_to_policy_pasSubject_update) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; pas_wellformed (aag\<lparr>pasSubject := x\<rparr>)\<rbrakk> \<Longrightarrow> pas_refined (aag\<lparr>pasSubject := x\<rparr>) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; pas_wellformed (aag\<lparr>pasSubject := x\<rparr>)\<rbrakk> \<Longrightarrow> pas_wellformed (aag\<lparr>pasSubject := x\<rparr>) \<and> irq_map_wellformed (aag\<lparr>pasSubject := x\<rparr>) s \<and> tcb_domain_map_wellformed (aag\<lparr>pasSubject := x\<rparr>) s \<and> state_objs_in_policy (aag\<lparr>pasSubject := x\<rparr>) s \<and> state_asids_to_policy (aag\<lparr>pasSubject := x\<rparr>) s \<subseteq> pasPolicy (aag\<lparr>pasSubject := x\<rparr>) \<and> state_irqs_to_policy (aag\<lparr>pasSubject := x\<rparr>) s \<subseteq> pasPolicy (aag\<lparr>pasSubject := x\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>pas_refined aag s; pas_wellformed (aag\<lparr>pasSubject := x\<rparr>)\<rbrakk> \<Longrightarrow> irq_map_wellformed (aag\<lparr>pasSubject := x\<rparr>) s
 2. \<lbrakk>pas_refined aag s; pas_wellformed (aag\<lparr>pasSubject := x\<rparr>)\<rbrakk> \<Longrightarrow> tcb_domain_map_wellformed (aag\<lparr>pasSubject := x\<rparr>) s
 3. \<lbrakk>pas_refined aag s; pas_wellformed (aag\<lparr>pasSubject := x\<rparr>)\<rbrakk> \<Longrightarrow> state_objs_in_policy (aag\<lparr>pasSubject := x\<rparr>) s
 4. \<lbrakk>pas_refined aag s; pas_wellformed (aag\<lparr>pasSubject := x\<rparr>)\<rbrakk> \<Longrightarrow> state_asids_to_policy (aag\<lparr>pasSubject := x\<rparr>) s \<subseteq> pasPolicy (aag\<lparr>pasSubject := x\<rparr>)
 5. \<lbrakk>pas_refined aag s; pas_wellformed (aag\<lparr>pasSubject := x\<rparr>)\<rbrakk> \<Longrightarrow> state_irqs_to_policy (aag\<lparr>pasSubject := x\<rparr>) s \<subseteq> pasPolicy (aag\<lparr>pasSubject := x\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>pas_refined aag s; pas_wellformed (aag\<lparr>pasSubject := x\<rparr>)\<rbrakk> \<Longrightarrow> tcb_domain_map_wellformed (aag\<lparr>pasSubject := x\<rparr>) s
 2. \<lbrakk>pas_refined aag s; pas_wellformed (aag\<lparr>pasSubject := x\<rparr>)\<rbrakk> \<Longrightarrow> state_objs_in_policy (aag\<lparr>pasSubject := x\<rparr>) s
 3. \<lbrakk>pas_refined aag s; pas_wellformed (aag\<lparr>pasSubject := x\<rparr>)\<rbrakk> \<Longrightarrow> state_asids_to_policy (aag\<lparr>pasSubject := x\<rparr>) s \<subseteq> pasPolicy (aag\<lparr>pasSubject := x\<rparr>)
 4. \<lbrakk>pas_refined aag s; pas_wellformed (aag\<lparr>pasSubject := x\<rparr>)\<rbrakk> \<Longrightarrow> state_irqs_to_policy (aag\<lparr>pasSubject := x\<rparr>) s \<subseteq> pasPolicy (aag\<lparr>pasSubject := x\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pas_refined aag s; pas_wellformed (aag\<lparr>pasSubject := x\<rparr>)\<rbrakk> \<Longrightarrow> state_objs_in_policy (aag\<lparr>pasSubject := x\<rparr>) s
 2. \<lbrakk>pas_refined aag s; pas_wellformed (aag\<lparr>pasSubject := x\<rparr>)\<rbrakk> \<Longrightarrow> state_asids_to_policy (aag\<lparr>pasSubject := x\<rparr>) s \<subseteq> pasPolicy (aag\<lparr>pasSubject := x\<rparr>)
 3. \<lbrakk>pas_refined aag s; pas_wellformed (aag\<lparr>pasSubject := x\<rparr>)\<rbrakk> \<Longrightarrow> state_irqs_to_policy (aag\<lparr>pasSubject := x\<rparr>) s \<subseteq> pasPolicy (aag\<lparr>pasSubject := x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_refined aag s; pas_wellformed (aag\<lparr>pasSubject := x\<rparr>)\<rbrakk> \<Longrightarrow> state_asids_to_policy (aag\<lparr>pasSubject := x\<rparr>) s \<subseteq> pasPolicy (aag\<lparr>pasSubject := x\<rparr>)
 2. \<lbrakk>pas_refined aag s; pas_wellformed (aag\<lparr>pasSubject := x\<rparr>)\<rbrakk> \<Longrightarrow> state_irqs_to_policy (aag\<lparr>pasSubject := x\<rparr>) s \<subseteq> pasPolicy (aag\<lparr>pasSubject := x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; pas_wellformed (aag\<lparr>pasSubject := x\<rparr>)\<rbrakk> \<Longrightarrow> state_irqs_to_policy (aag\<lparr>pasSubject := x\<rparr>) s \<subseteq> pasPolicy (aag\<lparr>pasSubject := x\<rparr>) proof (prove)
goal:
No subgoals!