theory PolicySystemSAC

lemma SAC_partsSubjectAffects_exceptT : "x \<noteq> T \<Longrightarrow> partsSubjectAffects SACAuthGraph x = SACFlowDoms" apply (rule equalityI) defer apply (rule subsetI) apply (simp add:partsSubjectAffects_def image_def label_can_affect_partition_def) apply (case_tac x) apply ((erule disjE, clarify, simp add:SAC_affects SAC_reads, blast?)+, simp add:SAC_affects SAC_reads, blast?)+ apply (rule subsetI) apply (simp add:partsSubjectAffects_def image_def label_can_affect_partition_def) apply (clarify) apply (case_tac x) apply (case_tac[!] xaa) apply (auto simp: SAC_affects SAC_reads) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<noteq> T \<Longrightarrow> partsSubjectAffects SACAuthGraph x = SACFlowDoms proof (prove)
goal (2 subgoals):
 1. x \<noteq> T \<Longrightarrow> partsSubjectAffects SACAuthGraph x \<subseteq> SACFlowDoms
 2. x \<noteq> T \<Longrightarrow> SACFlowDoms \<subseteq> partsSubjectAffects SACAuthGraph x proof (prove)
goal (2 subgoals):
 1. x \<noteq> T \<Longrightarrow> SACFlowDoms \<subseteq> partsSubjectAffects SACAuthGraph x
 2. x \<noteq> T \<Longrightarrow> partsSubjectAffects SACAuthGraph x \<subseteq> SACFlowDoms proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<noteq> T; xa \<in> SACFlowDoms\<rbrakk> \<Longrightarrow> xa \<in> partsSubjectAffects SACAuthGraph x
 2. x \<noteq> T \<Longrightarrow> partsSubjectAffects SACAuthGraph x \<subseteq> SACFlowDoms proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<noteq> T; xa = Partition EP \<or> xa = Partition SC \<or> xa = Partition NicC \<or> xa = Partition RM \<or> xa = Partition R \<or> xa = Partition NicA \<or> xa = Partition NicB \<or> xa = Partition NicD \<or> xa = Partition NTFN1 \<or> xa = Partition NTFN2 \<or> xa = Partition NTFN3\<rbrakk> \<Longrightarrow> \<exists>xb. (\<exists>d. d \<in> subjectAffects SACAuthGraph (partition_label x) \<and> d \<in> subjectReads SACAuthGraph (partition_label xb)) \<and> xa = Partition xb
 2. x \<noteq> T \<Longrightarrow> partsSubjectAffects SACAuthGraph x \<subseteq> SACFlowDoms proof (prove)
goal (13 subgoals):
 1. \<And>xa. \<lbrakk>x \<noteq> T; xa = Partition EP \<or> xa = Partition SC \<or> xa = Partition NicC \<or> xa = Partition RM \<or> xa = Partition R \<or> xa = Partition NicA \<or> xa = Partition NicB \<or> xa = Partition NicD \<or> xa = Partition NTFN1 \<or> xa = Partition NTFN2 \<or> xa = Partition NTFN3; x = NicA\<rbrakk> \<Longrightarrow> \<exists>xb. (\<exists>d. d \<in> subjectAffects SACAuthGraph (partition_label x) \<and> d \<in> subjectReads SACAuthGraph (partition_label xb)) \<and> xa = Partition xb
 2. \<And>xa. \<lbrakk>x \<noteq> T; xa = Partition EP \<or> xa = Partition SC \<or> xa = Partition NicC \<or> xa = Partition RM \<or> xa = Partition R \<or> xa = Partition NicA \<or> xa = Partition NicB \<or> xa = Partition NicD \<or> xa = Partition NTFN1 \<or> xa = Partition NTFN2 \<or> xa = Partition NTFN3; x = NicB\<rbrakk> \<Longrightarrow> \<exists>xb. (\<exists>d. d \<in> subjectAffects SACAuthGraph (partition_label x) \<and> d \<in> subjectReads SACAuthGraph (partition_label xb)) \<and> xa = Partition xb
 3. \<And>xa. \<lbrakk>x \<noteq> T; xa = Partition EP \<or> xa = Partition SC \<or> xa = Partition NicC \<or> xa = Partition RM \<or> xa = Partition R \<or> xa = Partition NicA \<or> xa = Partition NicB \<or> xa = Partition NicD \<or> xa = Partition NTFN1 \<or> xa = Partition NTFN2 \<or> xa = Partition NTFN3; x = NicC\<rbrakk> \<Longrightarrow> \<exists>xb. (\<exists>d. d \<in> subjectAffects SACAuthGraph (partition_label x) \<and> d \<in> subjectReads SACAuthGraph (partition_label xb)) \<and> xa = Partition xb
 4. \<And>xa. \<lbrakk>x \<noteq> T; xa = Partition EP \<or> xa = Partition SC \<or> xa = Partition NicC \<or> xa = Partition RM \<or> xa = Partition R \<or> xa = Partition NicA \<or> xa = Partition NicB \<or> xa = Partition NicD \<or> xa = Partition NTFN1 \<or> xa = Partition NTFN2 \<or> xa = Partition NTFN3; x = NicD\<rbrakk> \<Longrightarrow> \<exists>xb. (\<exists>d. d \<in> subjectAffects SACAuthGraph (partition_label x) \<and> d \<in> subjectReads SACAuthGraph (partition_label xb)) \<and> xa = Partition xb
 5. \<And>xa. \<lbrakk>x \<noteq> T; xa = Partition EP \<or> xa = Partition SC \<or> xa = Partition NicC \<or> xa = Partition RM \<or> xa = Partition R \<or> xa = Partition NicA \<or> xa = Partition NicB \<or> xa = Partition NicD \<or> xa = Partition NTFN1 \<or> xa = Partition NTFN2 \<or> xa = Partition NTFN3; x = R\<rbrakk> \<Longrightarrow> \<exists>xb. (\<exists>d. d \<in> subjectAffects SACAuthGraph (partition_label x) \<and> d \<in> subjectReads SACAuthGraph (partition_label xb)) \<and> xa = Partition xb
 6. \<And>xa. \<lbrakk>x \<noteq> T; xa = Partition EP \<or> xa = Partition SC \<or> xa = Partition NicC \<or> xa = Partition RM \<or> xa = Partition R \<or> xa = Partition NicA \<or> xa = Partition NicB \<or> xa = Partition NicD \<or> xa = Partition NTFN1 \<or> xa = Partition NTFN2 \<or> xa = Partition NTFN3; x = RM\<rbrakk> \<Longrightarrow> \<exists>xb. (\<exists>d. d \<in> subjectAffects SACAuthGraph (partition_label x) \<and> d \<in> subjectReads SACAuthGraph (partition_label xb)) \<and> xa = Partition xb
 7. \<And>xa. \<lbrakk>x \<noteq> T; xa = Partition EP \<or> xa = Partition SC \<or> xa = Partition NicC \<or> xa = Partition RM \<or> xa = Partition R \<or> xa = Partition NicA \<or> xa = Partition NicB \<or> xa = Partition NicD \<or> xa = Partition NTFN1 \<or> xa = Partition NTFN2 \<or> xa = Partition NTFN3; x = SC\<rbrakk> \<Longrightarrow> \<exists>xb. (\<exists>d. d \<in> subjectAffects SACAuthGraph (partition_label x) \<and> d \<in> subjectReads SACAuthGraph (partition_label xb)) \<and> xa = Partition xb
 8. \<And>xa. \<lbrakk>x \<noteq> T; xa = Partition EP \<or> xa = Partition SC \<or> xa = Partition NicC \<or> xa = Partition RM \<or> xa = Partition R \<or> xa = Partition NicA \<or> xa = Partition NicB \<or> xa = Partition NicD \<or> xa = Partition NTFN1 \<or> xa = Partition NTFN2 \<or> xa = Partition NTFN3; x = EP\<rbrakk> \<Longrightarrow> \<exists>xb. (\<exists>d. d \<in> subjectAffects SACAuthGraph (partition_label x) \<and> d \<in> subjectReads SACAuthGraph (partition_label xb)) \<and> xa = Partition xb
 9. \<And>xa. \<lbrakk>x \<noteq> T; xa = Partition EP \<or> xa = Partition SC \<or> xa = Partition NicC \<or> xa = Partition RM \<or> xa = Partition R \<or> xa = Partition NicA \<or> xa = Partition NicB \<or> xa = Partition NicD \<or> xa = Partition NTFN1 \<or> xa = Partition NTFN2 \<or> xa = Partition NTFN3; x = T\<rbrakk> \<Longrightarrow> \<exists>xb. (\<exists>d. d \<in> subjectAffects SACAuthGraph (partition_label x) \<and> d \<in> subjectReads SACAuthGraph (partition_label xb)) \<and> xa = Partition xb
 10. \<And>xa. \<lbrakk>x \<noteq> T; xa = Partition EP \<or> xa = Partition SC \<or> xa = Partition NicC \<or> xa = Partition RM \<or> xa = Partition R \<or> xa = Partition NicA \<or> xa = Partition NicB \<or> xa = Partition NicD \<or> xa = Partition NTFN1 \<or> xa = Partition NTFN2 \<or> xa = Partition NTFN3; x = NTFN1\<rbrakk> \<Longrightarrow> \<exists>xb. (\<exists>d. d \<in> subjectAffects SACAuthGraph (partition_label x) \<and> d \<in> subjectReads SACAuthGraph (partition_label xb)) \<and> xa = Partition xb
A total of 13 subgoals... proof (prove)
goal (1 subgoal):
 1. x \<noteq> T \<Longrightarrow> partsSubjectAffects SACAuthGraph x \<subseteq> SACFlowDoms proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<noteq> T; xa \<in> partsSubjectAffects SACAuthGraph x\<rbrakk> \<Longrightarrow> xa \<in> SACFlowDoms proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<noteq> T; \<exists>xb. (\<exists>d. d \<in> subjectAffects SACAuthGraph (partition_label x) \<and> d \<in> subjectReads SACAuthGraph (partition_label xb)) \<and> xa = Partition xb\<rbrakk> \<Longrightarrow> xa = Partition EP \<or> xa = Partition SC \<or> xa = Partition NicC \<or> xa = Partition RM \<or> xa = Partition R \<or> xa = Partition NicA \<or> xa = Partition NicB \<or> xa = Partition NicD \<or> xa = Partition NTFN1 \<or> xa = Partition NTFN2 \<or> xa = Partition NTFN3 proof (prove)
goal (1 subgoal):
 1. \<And>xa xaa d. \<lbrakk>x \<noteq> T; d \<in> subjectAffects SACAuthGraph (partition_label x); d \<in> subjectReads SACAuthGraph (partition_label xaa); xaa \<noteq> EP; xaa \<noteq> SC; xaa \<noteq> NicC; xaa \<noteq> RM; xaa \<noteq> R; xaa \<noteq> NicA; xaa \<noteq> NicB; xaa \<noteq> NicD; xaa \<noteq> NTFN1; xaa \<noteq> NTFN3\<rbrakk> \<Longrightarrow> xaa = NTFN2 proof (prove)
goal (12 subgoals):
 1. \<And>xa xaa d. \<lbrakk>x \<noteq> T; d \<in> subjectAffects SACAuthGraph (partition_label x); d \<in> subjectReads SACAuthGraph (partition_label xaa); xaa \<noteq> EP; xaa \<noteq> SC; xaa \<noteq> NicC; xaa \<noteq> RM; xaa \<noteq> R; xaa \<noteq> NicA; xaa \<noteq> NicB; xaa \<noteq> NicD; xaa \<noteq> NTFN1; xaa \<noteq> NTFN3; x = NicA\<rbrakk> \<Longrightarrow> xaa = NTFN2
 2. \<And>xa xaa d. \<lbrakk>x \<noteq> T; d \<in> subjectAffects SACAuthGraph (partition_label x); d \<in> subjectReads SACAuthGraph (partition_label xaa); xaa \<noteq> EP; xaa \<noteq> SC; xaa \<noteq> NicC; xaa \<noteq> RM; xaa \<noteq> R; xaa \<noteq> NicA; xaa \<noteq> NicB; xaa \<noteq> NicD; xaa \<noteq> NTFN1; xaa \<noteq> NTFN3; x = NicB\<rbrakk> \<Longrightarrow> xaa = NTFN2
 3. \<And>xa xaa d. \<lbrakk>x \<noteq> T; d \<in> subjectAffects SACAuthGraph (partition_label x); d \<in> subjectReads SACAuthGraph (partition_label xaa); xaa \<noteq> EP; xaa \<noteq> SC; xaa \<noteq> NicC; xaa \<noteq> RM; xaa \<noteq> R; xaa \<noteq> NicA; xaa \<noteq> NicB; xaa \<noteq> NicD; xaa \<noteq> NTFN1; xaa \<noteq> NTFN3; x = NicC\<rbrakk> \<Longrightarrow> xaa = NTFN2
 4. \<And>xa xaa d. \<lbrakk>x \<noteq> T; d \<in> subjectAffects SACAuthGraph (partition_label x); d \<in> subjectReads SACAuthGraph (partition_label xaa); xaa \<noteq> EP; xaa \<noteq> SC; xaa \<noteq> NicC; xaa \<noteq> RM; xaa \<noteq> R; xaa \<noteq> NicA; xaa \<noteq> NicB; xaa \<noteq> NicD; xaa \<noteq> NTFN1; xaa \<noteq> NTFN3; x = NicD\<rbrakk> \<Longrightarrow> xaa = NTFN2
 5. \<And>xa xaa d. \<lbrakk>x \<noteq> T; d \<in> subjectAffects SACAuthGraph (partition_label x); d \<in> subjectReads SACAuthGraph (partition_label xaa); xaa \<noteq> EP; xaa \<noteq> SC; xaa \<noteq> NicC; xaa \<noteq> RM; xaa \<noteq> R; xaa \<noteq> NicA; xaa \<noteq> NicB; xaa \<noteq> NicD; xaa \<noteq> NTFN1; xaa \<noteq> NTFN3; x = R\<rbrakk> \<Longrightarrow> xaa = NTFN2
 6. \<And>xa xaa d. \<lbrakk>x \<noteq> T; d \<in> subjectAffects SACAuthGraph (partition_label x); d \<in> subjectReads SACAuthGraph (partition_label xaa); xaa \<noteq> EP; xaa \<noteq> SC; xaa \<noteq> NicC; xaa \<noteq> RM; xaa \<noteq> R; xaa \<noteq> NicA; xaa \<noteq> NicB; xaa \<noteq> NicD; xaa \<noteq> NTFN1; xaa \<noteq> NTFN3; x = RM\<rbrakk> \<Longrightarrow> xaa = NTFN2
 7. \<And>xa xaa d. \<lbrakk>x \<noteq> T; d \<in> subjectAffects SACAuthGraph (partition_label x); d \<in> subjectReads SACAuthGraph (partition_label xaa); xaa \<noteq> EP; xaa \<noteq> SC; xaa \<noteq> NicC; xaa \<noteq> RM; xaa \<noteq> R; xaa \<noteq> NicA; xaa \<noteq> NicB; xaa \<noteq> NicD; xaa \<noteq> NTFN1; xaa \<noteq> NTFN3; x = SC\<rbrakk> \<Longrightarrow> xaa = NTFN2
 8. \<And>xa xaa d. \<lbrakk>x \<noteq> T; d \<in> subjectAffects SACAuthGraph (partition_label x); d \<in> subjectReads SACAuthGraph (partition_label xaa); xaa \<noteq> EP; xaa \<noteq> SC; xaa \<noteq> NicC; xaa \<noteq> RM; xaa \<noteq> R; xaa \<noteq> NicA; xaa \<noteq> NicB; xaa \<noteq> NicD; xaa \<noteq> NTFN1; xaa \<noteq> NTFN3; x = EP\<rbrakk> \<Longrightarrow> xaa = NTFN2
 9. \<And>xa xaa d. \<lbrakk>x \<noteq> T; d \<in> subjectAffects SACAuthGraph (partition_label x); d \<in> subjectReads SACAuthGraph (partition_label xaa); xaa \<noteq> EP; xaa \<noteq> SC; xaa \<noteq> NicC; xaa \<noteq> RM; xaa \<noteq> R; xaa \<noteq> NicA; xaa \<noteq> NicB; xaa \<noteq> NicD; xaa \<noteq> NTFN1; xaa \<noteq> NTFN3; x = T\<rbrakk> \<Longrightarrow> xaa = NTFN2
 10. \<And>xa xaa d. \<lbrakk>x \<noteq> T; d \<in> subjectAffects SACAuthGraph (partition_label x); d \<in> subjectReads SACAuthGraph (partition_label xaa); xaa \<noteq> EP; xaa \<noteq> SC; xaa \<noteq> NicC; xaa \<noteq> RM; xaa \<noteq> R; xaa \<noteq> NicA; xaa \<noteq> NicB; xaa \<noteq> NicD; xaa \<noteq> NTFN1; xaa \<noteq> NTFN3; x = NTFN1\<rbrakk> \<Longrightarrow> xaa = NTFN2
A total of 12 subgoals... proof (prove)
goal (144 subgoals):
 1. \<And>xa xaa d. \<lbrakk>x \<noteq> T; d \<in> subjectAffects SACAuthGraph (partition_label x); d \<in> subjectReads SACAuthGraph (partition_label xaa); xaa \<noteq> EP; xaa \<noteq> SC; xaa \<noteq> NicC; xaa \<noteq> RM; xaa \<noteq> R; xaa \<noteq> NicA; xaa \<noteq> NicB; xaa \<noteq> NicD; xaa \<noteq> NTFN1; xaa \<noteq> NTFN3; x = NicA; xaa = NicA\<rbrakk> \<Longrightarrow> xaa = NTFN2
 2. \<And>xa xaa d. \<lbrakk>x \<noteq> T; d \<in> subjectAffects SACAuthGraph (partition_label x); d \<in> subjectReads SACAuthGraph (partition_label xaa); xaa \<noteq> EP; xaa \<noteq> SC; xaa \<noteq> NicC; xaa \<noteq> RM; xaa \<noteq> R; xaa \<noteq> NicA; xaa \<noteq> NicB; xaa \<noteq> NicD; xaa \<noteq> NTFN1; xaa \<noteq> NTFN3; x = NicA; xaa = NicB\<rbrakk> \<Longrightarrow> xaa = NTFN2
 3. \<And>xa xaa d. \<lbrakk>x \<noteq> T; d \<in> subjectAffects SACAuthGraph (partition_label x); d \<in> subjectReads SACAuthGraph (partition_label xaa); xaa \<noteq> EP; xaa \<noteq> SC; xaa \<noteq> NicC; xaa \<noteq> RM; xaa \<noteq> R; xaa \<noteq> NicA; xaa \<noteq> NicB; xaa \<noteq> NicD; xaa \<noteq> NTFN1; xaa \<noteq> NTFN3; x = NicA; xaa = NicC\<rbrakk> \<Longrightarrow> xaa = NTFN2
 4. \<And>xa xaa d. \<lbrakk>x \<noteq> T; d \<in> subjectAffects SACAuthGraph (partition_label x); d \<in> subjectReads SACAuthGraph (partition_label xaa); xaa \<noteq> EP; xaa \<noteq> SC; xaa \<noteq> NicC; xaa \<noteq> RM; xaa \<noteq> R; xaa \<noteq> NicA; xaa \<noteq> NicB; xaa \<noteq> NicD; xaa \<noteq> NTFN1; xaa \<noteq> NTFN3; x = NicA; xaa = NicD\<rbrakk> \<Longrightarrow> xaa = NTFN2
 5. \<And>xa xaa d. \<lbrakk>x \<noteq> T; d \<in> subjectAffects SACAuthGraph (partition_label x); d \<in> subjectReads SACAuthGraph (partition_label xaa); xaa \<noteq> EP; xaa \<noteq> SC; xaa \<noteq> NicC; xaa \<noteq> RM; xaa \<noteq> R; xaa \<noteq> NicA; xaa \<noteq> NicB; xaa \<noteq> NicD; xaa \<noteq> NTFN1; xaa \<noteq> NTFN3; x = NicA; xaa = R\<rbrakk> \<Longrightarrow> xaa = NTFN2
 6. \<And>xa xaa d. \<lbrakk>x \<noteq> T; d \<in> subjectAffects SACAuthGraph (partition_label x); d \<in> subjectReads SACAuthGraph (partition_label xaa); xaa \<noteq> EP; xaa \<noteq> SC; xaa \<noteq> NicC; xaa \<noteq> RM; xaa \<noteq> R; xaa \<noteq> NicA; xaa \<noteq> NicB; xaa \<noteq> NicD; xaa \<noteq> NTFN1; xaa \<noteq> NTFN3; x = NicA; xaa = RM\<rbrakk> \<Longrightarrow> xaa = NTFN2
 7. \<And>xa xaa d. \<lbrakk>x \<noteq> T; d \<in> subjectAffects SACAuthGraph (partition_label x); d \<in> subjectReads SACAuthGraph (partition_label xaa); xaa \<noteq> EP; xaa \<noteq> SC; xaa \<noteq> NicC; xaa \<noteq> RM; xaa \<noteq> R; xaa \<noteq> NicA; xaa \<noteq> NicB; xaa \<noteq> NicD; xaa \<noteq> NTFN1; xaa \<noteq> NTFN3; x = NicA; xaa = SC\<rbrakk> \<Longrightarrow> xaa = NTFN2
 8. \<And>xa xaa d. \<lbrakk>x \<noteq> T; d \<in> subjectAffects SACAuthGraph (partition_label x); d \<in> subjectReads SACAuthGraph (partition_label xaa); xaa \<noteq> EP; xaa \<noteq> SC; xaa \<noteq> NicC; xaa \<noteq> RM; xaa \<noteq> R; xaa \<noteq> NicA; xaa \<noteq> NicB; xaa \<noteq> NicD; xaa \<noteq> NTFN1; xaa \<noteq> NTFN3; x = NicA; xaa = EP\<rbrakk> \<Longrightarrow> xaa = NTFN2
 9. \<And>xa xaa d. \<lbrakk>x \<noteq> T; d \<in> subjectAffects SACAuthGraph (partition_label x); d \<in> subjectReads SACAuthGraph (partition_label xaa); xaa \<noteq> EP; xaa \<noteq> SC; xaa \<noteq> NicC; xaa \<noteq> RM; xaa \<noteq> R; xaa \<noteq> NicA; xaa \<noteq> NicB; xaa \<noteq> NicD; xaa \<noteq> NTFN1; xaa \<noteq> NTFN3; x = NicA; xaa = T\<rbrakk> \<Longrightarrow> xaa = NTFN2
 10. \<And>xa xaa d. \<lbrakk>x \<noteq> T; d \<in> subjectAffects SACAuthGraph (partition_label x); d \<in> subjectReads SACAuthGraph (partition_label xaa); xaa \<noteq> EP; xaa \<noteq> SC; xaa \<noteq> NicC; xaa \<noteq> RM; xaa \<noteq> R; xaa \<noteq> NicA; xaa \<noteq> NicB; xaa \<noteq> NicD; xaa \<noteq> NTFN1; xaa \<noteq> NTFN3; x = NicA; xaa = NTFN1\<rbrakk> \<Longrightarrow> xaa = NTFN2
A total of 144 subgoals... proof (prove)
goal:
No subgoals!