theory PolicySystemSAC

lemma SAC_partsSubjectAffects_T : "(partsSubjectAffects SACAuthGraph T) = {Partition NTFN1, Partition NTFN2, Partition NTFN3} \<union> {Partition T, Partition SC, Partition RM, Partition R, Partition NicA, Partition NicB, Partition NicD, Partition NicC, Partition EP}" apply (rule equalityI) apply (rule subsetI) apply (simp add: partsSubjectAffects_def image_def label_can_affect_partition_def SAC_affects SAC_reads) apply (clarify) apply (case_tac xa, simp_all)[1] apply (rule subsetI) apply (simp add: partsSubjectAffects_def image_def label_can_affect_partition_def SAC_affects SAC_reads) apply (erule disjE, simp add: SAC_reads)  (* Do not collapse this in with a blast? because attempting blast takes too long *)
     apply ((erule disjE)?, simp add: SAC_reads, blast)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partsSubjectAffects SACAuthGraph T = {Partition NTFN1, Partition NTFN2, Partition NTFN3} \<union> {Partition T, Partition SC, Partition RM, Partition R, Partition NicA, Partition NicB, Partition NicD, Partition NicC, Partition EP} proof (prove)
goal (2 subgoals):
 1. partsSubjectAffects SACAuthGraph T \<subseteq> {Partition NTFN1, Partition NTFN2, Partition NTFN3} \<union> {Partition T, Partition SC, Partition RM, Partition R, Partition NicA, Partition NicB, Partition NicD, Partition NicC, Partition EP}
 2. {Partition NTFN1, Partition NTFN2, Partition NTFN3} \<union> {Partition T, Partition SC, Partition RM, Partition R, Partition NicA, Partition NicB, Partition NicD, Partition NicC, Partition EP} \<subseteq> partsSubjectAffects SACAuthGraph T proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> partsSubjectAffects SACAuthGraph T \<Longrightarrow> x \<in> {Partition NTFN1, Partition NTFN2, Partition NTFN3} \<union> {Partition T, Partition SC, Partition RM, Partition R, Partition NicA, Partition NicB, Partition NicD, Partition NicC, Partition EP}
 2. {Partition NTFN1, Partition NTFN2, Partition NTFN3} \<union> {Partition T, Partition SC, Partition RM, Partition R, Partition NicA, Partition NicB, Partition NicD, Partition NicC, Partition EP} \<subseteq> partsSubjectAffects SACAuthGraph T proof (prove)
goal (2 subgoals):
 1. \<And>x. \<exists>xa. (\<exists>d. (d = partition_label T \<or> d = partition_label SC \<or> d = partition_label RM \<or> d = partition_label R \<or> d = partition_label NicA \<or> d = partition_label NicB \<or> d = partition_label NicD \<or> d = partition_label NicC \<or> d = partition_label EP \<or> d = partition_label NTFN1 \<or> d = partition_label NTFN2 \<or> d = partition_label NTFN3) \<and> d \<in> subjectReads SACAuthGraph (partition_label xa)) \<and> x = Partition xa \<Longrightarrow> x = Partition T \<or> x = Partition SC \<or> x = Partition RM \<or> x = Partition R \<or> x = Partition NicA \<or> x = Partition NicB \<or> x = Partition NicD \<or> x = Partition NicC \<or> x = Partition EP \<or> x = Partition NTFN1 \<or> x = Partition NTFN2 \<or> x = Partition NTFN3
 2. {Partition NTFN1, Partition NTFN2, Partition NTFN3} \<union> {Partition T, Partition SC, Partition RM, Partition R, Partition NicA, Partition NicB, Partition NicD, Partition NicC, Partition EP} \<subseteq> partsSubjectAffects SACAuthGraph T proof (prove)
goal (2 subgoals):
 1. \<And>x xa d. \<lbrakk>d = partition_label T \<or> d = partition_label SC \<or> d = partition_label RM \<or> d = partition_label R \<or> d = partition_label NicA \<or> d = partition_label NicB \<or> d = partition_label NicD \<or> d = partition_label NicC \<or> d = partition_label EP \<or> d = partition_label NTFN1 \<or> d = partition_label NTFN2 \<or> d = partition_label NTFN3; d \<in> subjectReads SACAuthGraph (partition_label xa); xa \<noteq> T; xa \<noteq> SC; xa \<noteq> RM; xa \<noteq> R; xa \<noteq> NicA; xa \<noteq> NicB; xa \<noteq> NicD; xa \<noteq> NicC; xa \<noteq> EP; xa \<noteq> NTFN1; xa \<noteq> NTFN3\<rbrakk> \<Longrightarrow> xa = NTFN2
 2. {Partition NTFN1, Partition NTFN2, Partition NTFN3} \<union> {Partition T, Partition SC, Partition RM, Partition R, Partition NicA, Partition NicB, Partition NicD, Partition NicC, Partition EP} \<subseteq> partsSubjectAffects SACAuthGraph T proof (prove)
goal (1 subgoal):
 1. {Partition NTFN1, Partition NTFN2, Partition NTFN3} \<union> {Partition T, Partition SC, Partition RM, Partition R, Partition NicA, Partition NicB, Partition NicD, Partition NicC, Partition EP} \<subseteq> partsSubjectAffects SACAuthGraph T proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {Partition NTFN1, Partition NTFN2, Partition NTFN3} \<union> {Partition T, Partition SC, Partition RM, Partition R, Partition NicA, Partition NicB, Partition NicD, Partition NicC, Partition EP} \<Longrightarrow> x \<in> partsSubjectAffects SACAuthGraph T proof (prove)
goal (1 subgoal):
 1. \<And>x. x = Partition T \<or> x = Partition SC \<or> x = Partition RM \<or> x = Partition R \<or> x = Partition NicA \<or> x = Partition NicB \<or> x = Partition NicD \<or> x = Partition NicC \<or> x = Partition EP \<or> x = Partition NTFN1 \<or> x = Partition NTFN2 \<or> x = Partition NTFN3 \<Longrightarrow> \<exists>xa. (\<exists>d. (d = partition_label T \<or> d = partition_label SC \<or> d = partition_label RM \<or> d = partition_label R \<or> d = partition_label NicA \<or> d = partition_label NicB \<or> d = partition_label NicD \<or> d = partition_label NicC \<or> d = partition_label EP \<or> d = partition_label NTFN1 \<or> d = partition_label NTFN2 \<or> d = partition_label NTFN3) \<and> d \<in> subjectReads SACAuthGraph (partition_label xa)) \<and> x = Partition xa proof (prove)
goal (1 subgoal):
 1. \<And>x. x = Partition SC \<or> x = Partition RM \<or> x = Partition R \<or> x = Partition NicA \<or> x = Partition NicB \<or> x = Partition NicD \<or> x = Partition NicC \<or> x = Partition EP \<or> x = Partition NTFN1 \<or> x = Partition NTFN2 \<or> x = Partition NTFN3 \<Longrightarrow> \<exists>xa. (\<exists>d. (d = partition_label T \<or> d = partition_label SC \<or> d = partition_label RM \<or> d = partition_label R \<or> d = partition_label NicA \<or> d = partition_label NicB \<or> d = partition_label NicD \<or> d = partition_label NicC \<or> d = partition_label EP \<or> d = partition_label NTFN1 \<or> d = partition_label NTFN2 \<or> d = partition_label NTFN3) \<and> d \<in> subjectReads SACAuthGraph (partition_label xa)) \<and> x = Partition xa proof (prove)
goal (1 subgoal):
 1. \<And>x. x = Partition SC \<or> x = Partition RM \<or> x = Partition R \<or> x = Partition NicA \<or> x = Partition NicB \<or> x = Partition NicD \<or> x = Partition NicC \<or> x = Partition EP \<or> x = Partition NTFN1 \<or> x = Partition NTFN2 \<or> x = Partition NTFN3 \<Longrightarrow> \<exists>xa. (\<exists>d. (d = partition_label T \<or> d = partition_label SC \<or> d = partition_label RM \<or> d = partition_label R \<or> d = partition_label NicA \<or> d = partition_label NicB \<or> d = partition_label NicD \<or> d = partition_label NicC \<or> d = partition_label EP \<or> d = partition_label NTFN1 \<or> d = partition_label NTFN2 \<or> d = partition_label NTFN3) \<and> d \<in> subjectReads SACAuthGraph (partition_label xa)) \<and> x = Partition xa proof (prove)
goal:
No subgoals!