theory ArchNoninterference

lemma inte_obj_arch:
  assumes inte_obj: "(integrity_obj_atomic aag activate subjects l)\<^sup>*\<^sup>* ko ko'"
  assumes "ko = Some (ArchObj ao)"
  assumes "ko \<noteq> ko'"
  shows "integrity_obj_atomic aag activate subjects l ko ko'" proof (cases "l \<in> subjects") case True then show ?thesis by (fastforce intro: integrity_obj_atomic.intros) next case False note l = this have "\<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow>
              ko \<noteq> ko' \<longrightarrow>
              integrity_obj_atomic aag activate subjects l ko ko'" using inte_obj proof (induct rule: rtranclp_induct) case base then show ?case by clarsimp next case (step y z) have "\<exists>ao'. ko' = Some (ArchObj ao')" using False inte_obj assms by (auto elim!: rtranclp_induct integrity_obj_atomic.cases) then show ?case using step.hyps by (fastforce intro: troa_arch arch_troa_asidpool_clear integrity_obj_atomic.intros
                    elim!: integrity_obj_atomic.cases arch_integrity_obj_atomic.cases) qed then show ?thesis using assms by fastforce qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. integrity_obj_atomic aag activate subjects l ko ko' proof (state)
goal (2 subgoals):
 1. l \<in> subjects \<Longrightarrow> integrity_obj_atomic aag activate subjects l ko ko'
 2. l \<notin> subjects \<Longrightarrow> integrity_obj_atomic aag activate subjects l ko ko' proof (state)
this:
l \<in> subjects

goal (2 subgoals):
 1. l \<in> subjects \<Longrightarrow> integrity_obj_atomic aag activate subjects l ko ko'
 2. l \<notin> subjects \<Longrightarrow> integrity_obj_atomic aag activate subjects l ko ko' proof (chain)
picking this:
l \<in> subjects proof (prove)
using this:
l \<in> subjects

goal (1 subgoal):
 1. integrity_obj_atomic aag activate subjects l ko ko' proof (state)
this:
integrity_obj_atomic aag activate subjects l ko ko'

goal (1 subgoal):
 1. l \<notin> subjects \<Longrightarrow> integrity_obj_atomic aag activate subjects l ko ko' proof (state)
goal (1 subgoal):
 1. l \<notin> subjects \<Longrightarrow> integrity_obj_atomic aag activate subjects l ko ko' proof (state)
this:
l \<notin> subjects

goal (1 subgoal):
 1. l \<notin> subjects \<Longrightarrow> integrity_obj_atomic aag activate subjects l ko ko' proof (state)
this:
l \<notin> subjects

goal (1 subgoal):
 1. l \<notin> subjects \<Longrightarrow> integrity_obj_atomic aag activate subjects l ko ko' proof (prove)
goal (1 subgoal):
 1. \<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> ko' \<longrightarrow> integrity_obj_atomic aag activate subjects l ko ko' proof (prove)
using this:
(integrity_obj_atomic aag activate subjects l)\<^sup>*\<^sup>* ko ko'

goal (1 subgoal):
 1. \<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> ko' \<longrightarrow> integrity_obj_atomic aag activate subjects l ko ko' proof (state)
goal (2 subgoals):
 1. \<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> ko \<longrightarrow> integrity_obj_atomic aag activate subjects l ko ko
 2. \<And>y z. \<lbrakk>(integrity_obj_atomic aag activate subjects l)\<^sup>*\<^sup>* ko y; integrity_obj_atomic aag activate subjects l y z; \<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> y \<longrightarrow> integrity_obj_atomic aag activate subjects l ko y\<rbrakk> \<Longrightarrow> \<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> z \<longrightarrow> integrity_obj_atomic aag activate subjects l ko z proof (state)
this:


goal (2 subgoals):
 1. \<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> ko \<longrightarrow> integrity_obj_atomic aag activate subjects l ko ko
 2. \<And>y z. \<lbrakk>(integrity_obj_atomic aag activate subjects l)\<^sup>*\<^sup>* ko y; integrity_obj_atomic aag activate subjects l y z; \<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> y \<longrightarrow> integrity_obj_atomic aag activate subjects l ko y\<rbrakk> \<Longrightarrow> \<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> z \<longrightarrow> integrity_obj_atomic aag activate subjects l ko z proof (chain)
picking this:
 proof (prove)
goal (1 subgoal):
 1. \<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> ko \<longrightarrow> integrity_obj_atomic aag activate subjects l ko ko proof (state)
this:
\<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> ko \<longrightarrow> integrity_obj_atomic aag activate subjects l ko ko

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(integrity_obj_atomic aag activate subjects l)\<^sup>*\<^sup>* ko y; integrity_obj_atomic aag activate subjects l y z; \<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> y \<longrightarrow> integrity_obj_atomic aag activate subjects l ko y\<rbrakk> \<Longrightarrow> \<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> z \<longrightarrow> integrity_obj_atomic aag activate subjects l ko z proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(integrity_obj_atomic aag activate subjects l)\<^sup>*\<^sup>* ko y; integrity_obj_atomic aag activate subjects l y z; \<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> y \<longrightarrow> integrity_obj_atomic aag activate subjects l ko y\<rbrakk> \<Longrightarrow> \<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> z \<longrightarrow> integrity_obj_atomic aag activate subjects l ko z proof (state)
this:
(integrity_obj_atomic aag activate subjects l)\<^sup>*\<^sup>* ko y
integrity_obj_atomic aag activate subjects l y z
\<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> y \<longrightarrow> integrity_obj_atomic aag activate subjects l ko y

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(integrity_obj_atomic aag activate subjects l)\<^sup>*\<^sup>* ko y; integrity_obj_atomic aag activate subjects l y z; \<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> y \<longrightarrow> integrity_obj_atomic aag activate subjects l ko y\<rbrakk> \<Longrightarrow> \<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> z \<longrightarrow> integrity_obj_atomic aag activate subjects l ko z proof (prove)
goal (1 subgoal):
 1. \<exists>ao'. ko' = Some (ArchObj ao') proof (prove)
using this:
l \<notin> subjects
(integrity_obj_atomic aag activate subjects l)\<^sup>*\<^sup>* ko ko'
(integrity_obj_atomic aag activate subjects l)\<^sup>*\<^sup>* ko ko'
ko = Some (ArchObj ao)
ko \<noteq> ko'

goal (1 subgoal):
 1. \<exists>ao'. ko' = Some (ArchObj ao') proof (state)
this:
\<exists>ao'. ko' = Some (ArchObj ao')

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(integrity_obj_atomic aag activate subjects l)\<^sup>*\<^sup>* ko y; integrity_obj_atomic aag activate subjects l y z; \<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> y \<longrightarrow> integrity_obj_atomic aag activate subjects l ko y\<rbrakk> \<Longrightarrow> \<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> z \<longrightarrow> integrity_obj_atomic aag activate subjects l ko z proof (chain)
picking this:
\<exists>ao'. ko' = Some (ArchObj ao') proof (prove)
using this:
\<exists>ao'. ko' = Some (ArchObj ao')

goal (1 subgoal):
 1. \<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> z \<longrightarrow> integrity_obj_atomic aag activate subjects l ko z proof (prove)
using this:
\<exists>ao'. ko' = Some (ArchObj ao')
(integrity_obj_atomic aag activate subjects l)\<^sup>*\<^sup>* ko y
integrity_obj_atomic aag activate subjects l y z
\<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> y \<longrightarrow> integrity_obj_atomic aag activate subjects l ko y

goal (1 subgoal):
 1. \<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> z \<longrightarrow> integrity_obj_atomic aag activate subjects l ko z proof (state)
this:
\<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> z \<longrightarrow> integrity_obj_atomic aag activate subjects l ko z

goal:
No subgoals! proof (state)
this:
\<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> ko' \<longrightarrow> integrity_obj_atomic aag activate subjects l ko ko'

goal (1 subgoal):
 1. l \<notin> subjects \<Longrightarrow> integrity_obj_atomic aag activate subjects l ko ko' proof (chain)
picking this:
\<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> ko' \<longrightarrow> integrity_obj_atomic aag activate subjects l ko ko' proof (prove)
using this:
\<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> ko' \<longrightarrow> integrity_obj_atomic aag activate subjects l ko ko'

goal (1 subgoal):
 1. integrity_obj_atomic aag activate subjects l ko ko' proof (prove)
using this:
\<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow> ko \<noteq> ko' \<longrightarrow> integrity_obj_atomic aag activate subjects l ko ko'
(integrity_obj_atomic aag activate subjects l)\<^sup>*\<^sup>* ko ko'
ko = Some (ArchObj ao)
ko \<noteq> ko'

goal (1 subgoal):
 1. integrity_obj_atomic aag activate subjects l ko ko' proof (state)
this:
integrity_obj_atomic aag activate subjects l ko ko'

goal:
No subgoals!