theory Finalise_IF

lemma ep_queues_are_invisible_or_eps_are_equal:
  "\<lbrakk> (pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag;
     ko_at (Endpoint ep) epptr s; ko_at (Endpoint ep') epptr s';
     reads_equiv aag s s'; affects_equiv aag l s s';
     valid_objs s; sym_refs (state_refs_of s); valid_objs s';
     sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s' \<rbrakk>
     \<Longrightarrow> (\<not> ep_queue_invisible aag l ep \<or> \<not> ep_queue_invisible aag l ep') \<longrightarrow> ep = ep'" apply (rule impI) apply (erule disjE) apply (blast intro!: ep_queues_are_invisible_or_eps_are_equal'[rule_format]) apply (rule sym) apply (erule ep_queues_are_invisible_or_eps_are_equal'[rule_format]) by (assumption | erule reads_equiv_sym | erule affects_equiv_sym)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint ep) epptr s; ko_at (Endpoint ep') epptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'\<rbrakk> \<Longrightarrow> \<not> ep_queue_invisible aag l ep \<or> \<not> ep_queue_invisible aag l ep' \<longrightarrow> ep = ep' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint ep) epptr s; ko_at (Endpoint ep') epptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ep_queue_invisible aag l ep \<or> \<not> ep_queue_invisible aag l ep'\<rbrakk> \<Longrightarrow> ep = ep' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint ep) epptr s; ko_at (Endpoint ep') epptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ep_queue_invisible aag l ep\<rbrakk> \<Longrightarrow> ep = ep'
 2. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint ep) epptr s; ko_at (Endpoint ep') epptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ep_queue_invisible aag l ep'\<rbrakk> \<Longrightarrow> ep = ep' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint ep) epptr s; ko_at (Endpoint ep') epptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ep_queue_invisible aag l ep'\<rbrakk> \<Longrightarrow> ep = ep' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ko_at (Endpoint ep) epptr s; ko_at (Endpoint ep') epptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ep_queue_invisible aag l ep'\<rbrakk> \<Longrightarrow> ep' = ep proof (prove)
goal (11 subgoals):
 1. \<lbrakk>ko_at (Endpoint ep) epptr s; ko_at (Endpoint ep') epptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ep_queue_invisible aag l ep'\<rbrakk> \<Longrightarrow> ko_at (Endpoint ep') epptr ?s10
 2. \<lbrakk>ko_at (Endpoint ep) epptr s; ko_at (Endpoint ep') epptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ep_queue_invisible aag l ep'\<rbrakk> \<Longrightarrow> ko_at (Endpoint ep) epptr ?s'10
 3. \<lbrakk>ko_at (Endpoint ep) epptr s; ko_at (Endpoint ep') epptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ep_queue_invisible aag l ep'\<rbrakk> \<Longrightarrow> reads_equiv aag ?s10 ?s'10
 4. \<lbrakk>ko_at (Endpoint ep) epptr s; ko_at (Endpoint ep') epptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ep_queue_invisible aag l ep'\<rbrakk> \<Longrightarrow> affects_equiv aag ?l10 ?s10 ?s'10
 5. \<lbrakk>ko_at (Endpoint ep) epptr s; ko_at (Endpoint ep') epptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ep_queue_invisible aag l ep'\<rbrakk> \<Longrightarrow> valid_objs ?s10
 6. \<lbrakk>ko_at (Endpoint ep) epptr s; ko_at (Endpoint ep') epptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ep_queue_invisible aag l ep'\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of ?s10)
 7. \<lbrakk>ko_at (Endpoint ep) epptr s; ko_at (Endpoint ep') epptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ep_queue_invisible aag l ep'\<rbrakk> \<Longrightarrow> valid_objs ?s'10
 8. \<lbrakk>ko_at (Endpoint ep) epptr s; ko_at (Endpoint ep') epptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ep_queue_invisible aag l ep'\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of ?s'10)
 9. \<lbrakk>ko_at (Endpoint ep) epptr s; ko_at (Endpoint ep') epptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ep_queue_invisible aag l ep'\<rbrakk> \<Longrightarrow> pas_refined aag ?s10
 10. \<lbrakk>ko_at (Endpoint ep) epptr s; ko_at (Endpoint ep') epptr s'; reads_equiv aag s s'; affects_equiv aag l s s'; valid_objs s; sym_refs (state_refs_of s); valid_objs s'; sym_refs (state_refs_of s'); pas_refined aag s; pas_refined aag s'; \<not> ep_queue_invisible aag l ep'\<rbrakk> \<Longrightarrow> pas_refined aag ?s'10
A total of 11 subgoals...