theory PolicySystemSAC

lemma ntfn123_reads : "l \<in> {NTFN1, NTFN2, NTFN3} \<Longrightarrow> subjectReads SACAuthGraph (partition_label l) = {partition_label NicB, partition_label RM, partition_label R, partition_label NicA, partition_label NicD, partition_label EP, partition_label SC, partition_label NicC, partition_label NTFN1, partition_label NTFN2, partition_label NTFN3}" apply (rule subset_antisym) defer 
  (* backward *)
   apply (rule subsetI) apply (erule_tac a=x in insertE, rule reads_all_rm_controlled_subjects, rule ntfn123_reads_rm, simp, simp) apply (erule_tac a=x in insertE, simp only:, rule ntfn123_reads_rm, simp) apply (erule_tac a=x in insertE, rule reads_all_rm_controlled_subjects, rule ntfn123_reads_rm, simp, simp) apply (erule_tac a=x in insertE, rule reads_all_rm_controlled_subjects, rule ntfn123_reads_rm, simp, simp) apply (erule_tac a=x in insertE, rule reads_all_rm_controlled_subjects, rule ntfn123_reads_rm, simp, simp) apply (erule_tac a=x in insertE, simp only:, rule ntfn123_reads_ep, simp) apply (erule_tac a=x in insertE, simp only:, rule ntfn123_reads_sc, simp) apply (erule_tac a=x in insertE, simp only:, rule ntfn123_reads_c, simp) apply (auto simp:ntfn123_reads_ntfn123)[1] 
  (* forward *)
   apply (rule subsetI) apply (erule subjectReads.induct) by (simp add:SACAuthGraph_def, blast?)+

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