theory Noninterference

lemma do_user_op_if_reads_respects_g:
  "reads_respects_g aag l (pas_refined aag and valid_vspace_objs_if and einvs and
                           is_subject aag \<circ> cur_thread and det_inv InUserMode tc and ct_running)
                    (do_user_op_if utf tc)" apply (rule equiv_valid_guard_imp) apply (rule do_user_op_reads_respects_g[where P="\<lambda>tc. einvs and
               det_inv InUserMode tc and ct_running"]) using utf_det apply fastforce apply simp apply (rule ct_running_not_idle) apply simp apply (simp add: invs_valid_idle) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (pas_refined aag and valid_vspace_objs_if and einvs and is_subject aag \<circ> cur_thread and det_inv InUserMode tc and ct_running) (do_user_op_if utf tc) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ?Q (do_user_op_if utf tc)
 2. \<And>s. (pas_refined aag and valid_vspace_objs_if and einvs and is_subject aag \<circ> cur_thread and det_inv InUserMode tc and ct_running) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<forall>pl pr pxn tc ms s. (einvs and det_inv InUserMode tc and ct_running) s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>x. utf (cur_thread s) pl pr pxn (tc, ms) = {x})
 2. \<And>s. (pas_refined aag and valid_vspace_objs_if and einvs and is_subject aag \<circ> cur_thread and det_inv InUserMode tc and ct_running) s \<Longrightarrow> (pas_refined aag and invs and valid_vspace_objs_if and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and (einvs and det_inv InUserMode tc and ct_running)) s proof (prove)
using this:
\<forall>pl pr pxn tc ms s. det_inv InUserMode tc s \<and> einvs s \<and> context_matches_state pl pr pxn ms s \<and> ct_running s \<longrightarrow> (\<exists>x. utf (cur_thread s) pl pr pxn (tc, ms) = {x})

goal (2 subgoals):
 1. \<forall>pl pr pxn tc ms s. (einvs and det_inv InUserMode tc and ct_running) s \<and> context_matches_state pl pr pxn ms s \<longrightarrow> (\<exists>x. utf (cur_thread s) pl pr pxn (tc, ms) = {x})
 2. \<And>s. (pas_refined aag and valid_vspace_objs_if and einvs and is_subject aag \<circ> cur_thread and det_inv InUserMode tc and ct_running) s \<Longrightarrow> (pas_refined aag and invs and valid_vspace_objs_if and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and (einvs and det_inv InUserMode tc and ct_running)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and valid_vspace_objs_if and einvs and is_subject aag \<circ> cur_thread and det_inv InUserMode tc and ct_running) s \<Longrightarrow> (pas_refined aag and invs and valid_vspace_objs_if and is_subject aag \<circ> cur_thread and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and (einvs and det_inv InUserMode tc and ct_running)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. pas_refined aag s \<and> valid_vspace_objs_if s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> is_subject aag (cur_thread s) \<and> det_inv InUserMode tc s \<and> ct_running s \<Longrightarrow> cur_thread s \<noteq> idle_thread s proof (prove)
goal (2 subgoals):
 1. \<And>s. pas_refined aag s \<and> valid_vspace_objs_if s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> is_subject aag (cur_thread s) \<and> det_inv InUserMode tc s \<and> ct_running s \<Longrightarrow> ct_running s
 2. \<And>s. pas_refined aag s \<and> valid_vspace_objs_if s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> is_subject aag (cur_thread s) \<and> det_inv InUserMode tc s \<and> ct_running s \<Longrightarrow> valid_idle s proof (prove)
goal (1 subgoal):
 1. \<And>s. pas_refined aag s \<and> valid_vspace_objs_if s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> is_subject aag (cur_thread s) \<and> det_inv InUserMode tc s \<and> ct_running s \<Longrightarrow> valid_idle s proof (prove)
goal:
No subgoals!