theory PolicySystemSAC

lemma abd_affects : "x \<in> {NicA, NicB, NicD} \<Longrightarrow> subjectAffects SACAuthGraph (partition_label x) = partition_label ` abd_affects_set" apply (rule subset_antisym) defer apply (rule abd_affects_bw) apply (simp) apply (rule subsetI) apply (erule subjectAffects.induct) by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> {NicA, NicB, NicD} \<Longrightarrow> subjectAffects SACAuthGraph (partition_label x) = partition_label ` abd_affects_set proof (prove)
goal (2 subgoals):
 1. x \<in> {NicA, NicB, NicD} \<Longrightarrow> subjectAffects SACAuthGraph (partition_label x) \<subseteq> partition_label ` abd_affects_set
 2. x \<in> {NicA, NicB, NicD} \<Longrightarrow> partition_label ` abd_affects_set \<subseteq> subjectAffects SACAuthGraph (partition_label x) proof (prove)
goal (2 subgoals):
 1. x \<in> {NicA, NicB, NicD} \<Longrightarrow> partition_label ` abd_affects_set \<subseteq> subjectAffects SACAuthGraph (partition_label x)
 2. x \<in> {NicA, NicB, NicD} \<Longrightarrow> subjectAffects SACAuthGraph (partition_label x) \<subseteq> partition_label ` abd_affects_set proof (prove)
goal (2 subgoals):
 1. x \<in> {NicA, NicB, NicD} \<Longrightarrow> x \<in> {NicA, NicB, NicD}
 2. x \<in> {NicA, NicB, NicD} \<Longrightarrow> subjectAffects SACAuthGraph (partition_label x) \<subseteq> partition_label ` abd_affects_set proof (prove)
goal (1 subgoal):
 1. x \<in> {NicA, NicB, NicD} \<Longrightarrow> subjectAffects SACAuthGraph (partition_label x) \<subseteq> partition_label ` abd_affects_set proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; xa \<in> subjectAffects SACAuthGraph (partition_label x)\<rbrakk> \<Longrightarrow> xa \<in> partition_label ` abd_affects_set proof (prove)
goal (12 subgoals):
 1. \<And>xa. x \<in> {NicA, NicB, NicD} \<Longrightarrow> partition_label x \<in> partition_label ` abd_affects_set
 2. \<And>xa auth l'. \<lbrakk>x \<in> {NicA, NicB, NicD}; (partition_label x, auth, l') \<in> SACAuthGraph; auth \<in> {Control, Write}\<rbrakk> \<Longrightarrow> l' \<in> partition_label ` abd_affects_set
 3. \<And>xa auth l'. \<lbrakk>x \<in> {NicA, NicB, NicD}; (partition_label x, auth, l') \<in> SACAuthGraph; auth \<in> {Receive, Notify, SyncSend, Call, Reset}\<rbrakk> \<Longrightarrow> l' \<in> partition_label ` abd_affects_set
 4. \<And>xa auth ep l' l''. \<lbrakk>x \<in> {NicA, NicB, NicD}; (partition_label x, 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 ` abd_affects_set
 5. \<And>xa ep l'. \<lbrakk>x \<in> {NicA, NicB, NicD}; (partition_label x, Receive, ep) \<in> SACAuthGraph; (l', SyncSend, ep) \<in> SACAuthGraph\<rbrakk> \<Longrightarrow> l' \<in> partition_label ` abd_affects_set
 6. \<And>xa l'. \<lbrakk>x \<in> {NicA, NicB, NicD}; (l', Reply, partition_label x) \<in> SACAuthGraph\<rbrakk> \<Longrightarrow> l' \<in> partition_label ` abd_affects_set
 7. \<And>xa l' l''. \<lbrakk>x \<in> {NicA, NicB, NicD}; (partition_label x, Reply, l') \<in> SACAuthGraph; (l', Write, l'') \<in> SACAuthGraph\<rbrakk> \<Longrightarrow> l'' \<in> partition_label ` abd_affects_set
 8. \<And>xa l'. \<lbrakk>x \<in> {NicA, NicB, NicD}; (partition_label x, DeleteDerived, l') \<in> SACAuthGraph\<rbrakk> \<Longrightarrow> l' \<in> partition_label ` abd_affects_set
 9. \<And>xa l' l''. \<lbrakk>x \<in> {NicA, NicB, NicD}; (partition_label x, DeleteDerived, l') \<in> SACAuthGraph; (l'', DeleteDerived, l') \<in> SACAuthGraph\<rbrakk> \<Longrightarrow> l'' \<in> partition_label ` abd_affects_set
 10. \<And>xa ep l' auth l''. \<lbrakk>x \<in> {NicA, NicB, NicD}; (partition_label x, Reset, ep) \<in> SACAuthGraph; (l', auth, ep) \<in> SACAuthGraph; auth \<in> {SyncSend, Receive}; (l', Write, l'') \<in> SACAuthGraph\<rbrakk> \<Longrightarrow> l'' \<in> partition_label ` abd_affects_set
A total of 12 subgoals...