theory PolicySystemSAC

lemma t_affects : "subjectAffects SACAuthGraph (partition_label T) = {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP}" apply (rule subset_antisym) defer 
  (* backward *)
   apply (rule subsetI, erule UnE) apply (auto simp:t_affects_ntfn123)[1] apply (erule insertE, simp only:, rule affects_lrefl) apply (erule insertE, simp only:, rule t_affects_sc) apply (erule insertE, simp only:, rule t_affects_rm) apply (erule insertE, simp only:, rule t_affects_r) apply (erule insertE, simp only:, rule t_affects_a) apply (erule insertE, simp only:, rule t_affects_bd, simp) apply (erule insertE, simp only:, rule t_affects_bd, simp) apply (erule insertE, simp only:, rule t_affects_c) apply (erule insertE, simp only:, rule t_affects_ep) apply simp 
  (* forward *)
   apply (rule subsetI, erule subjectAffects.induct) by (simp add:SACAuthGraph_def, blast?)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. subjectAffects SACAuthGraph (partition_label T) = {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP} proof (prove)
goal (2 subgoals):
 1. subjectAffects SACAuthGraph (partition_label T) \<subseteq> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP}
 2. {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP} \<subseteq> subjectAffects SACAuthGraph (partition_label T) proof (prove)
goal (2 subgoals):
 1. {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP} \<subseteq> subjectAffects SACAuthGraph (partition_label T)
 2. subjectAffects SACAuthGraph (partition_label T) \<subseteq> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP} proof (prove)
goal (2 subgoals):
 1. {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP} \<subseteq> subjectAffects SACAuthGraph (partition_label T)
 2. subjectAffects SACAuthGraph (partition_label T) \<subseteq> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP} proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label T)
 2. \<And>x. x \<in> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP} \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label T)
 3. subjectAffects SACAuthGraph (partition_label T) \<subseteq> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP} proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP} \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label T)
 2. subjectAffects SACAuthGraph (partition_label T) \<subseteq> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP} proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> {partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP} \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label T)
 2. subjectAffects SACAuthGraph (partition_label T) \<subseteq> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP} proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> {partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP} \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label T)
 2. subjectAffects SACAuthGraph (partition_label T) \<subseteq> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP} proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> {partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP} \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label T)
 2. subjectAffects SACAuthGraph (partition_label T) \<subseteq> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP} proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> {partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP} \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label T)
 2. subjectAffects SACAuthGraph (partition_label T) \<subseteq> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP} proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> {partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP} \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label T)
 2. subjectAffects SACAuthGraph (partition_label T) \<subseteq> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP} proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> {partition_label NicD, partition_label NicC, partition_label EP} \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label T)
 2. subjectAffects SACAuthGraph (partition_label T) \<subseteq> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP} proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> {partition_label NicC, partition_label EP} \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label T)
 2. subjectAffects SACAuthGraph (partition_label T) \<subseteq> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP} proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> {partition_label EP} \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label T)
 2. subjectAffects SACAuthGraph (partition_label T) \<subseteq> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP} proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> {} \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label T)
 2. subjectAffects SACAuthGraph (partition_label T) \<subseteq> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP} proof (prove)
goal (1 subgoal):
 1. subjectAffects SACAuthGraph (partition_label T) \<subseteq> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP} proof (prove)
goal (1 subgoal):
 1. subjectAffects SACAuthGraph (partition_label T) \<subseteq> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP} proof (prove)
goal (12 subgoals):
 1. \<And>x. partition_label T \<in> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP}
 2. \<And>x auth l'. \<lbrakk>(partition_label T, auth, l') \<in> SACAuthGraph; auth \<in> {Control, Write}\<rbrakk> \<Longrightarrow> l' \<in> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP}
 3. \<And>x auth l'. \<lbrakk>(partition_label T, auth, l') \<in> SACAuthGraph; auth \<in> {Receive, Notify, SyncSend, Call, Reset}\<rbrakk> \<Longrightarrow> l' \<in> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP}
 4. \<And>x auth ep l' l''. \<lbrakk>(partition_label T, auth, ep) \<in> SACAuthGraph; auth \<in> {SyncSend, Notify, Call}; (l', Receive, ep) \<in> SACAuthGraph; (l', Write, l'') \<in> SACAuthGraph\<rbrakk> \<Longrightarrow> l'' \<in> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP}
 5. \<And>x ep l'. \<lbrakk>(partition_label T, Receive, ep) \<in> SACAuthGraph; (l', SyncSend, ep) \<in> SACAuthGraph\<rbrakk> \<Longrightarrow> l' \<in> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP}
 6. \<And>x l'. (l', Reply, partition_label T) \<in> SACAuthGraph \<Longrightarrow> l' \<in> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP}
 7. \<And>x l' l''. \<lbrakk>(partition_label T, Reply, l') \<in> SACAuthGraph; (l', Write, l'') \<in> SACAuthGraph\<rbrakk> \<Longrightarrow> l'' \<in> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP}
 8. \<And>x l'. (partition_label T, DeleteDerived, l') \<in> SACAuthGraph \<Longrightarrow> l' \<in> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP}
 9. \<And>x l' l''. \<lbrakk>(partition_label T, DeleteDerived, l') \<in> SACAuthGraph; (l'', DeleteDerived, l') \<in> SACAuthGraph\<rbrakk> \<Longrightarrow> l'' \<in> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP}
 10. \<And>x ep l' auth l''. \<lbrakk>(partition_label T, Reset, ep) \<in> SACAuthGraph; (l', auth, ep) \<in> SACAuthGraph; auth \<in> {SyncSend, Receive}; (l', Write, l'') \<in> SACAuthGraph\<rbrakk> \<Longrightarrow> l'' \<in> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3} \<union> {partition_label T, partition_label SC, partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD, partition_label NicC, partition_label EP}
A total of 12 subgoals...