theory PolicySystemSAC

lemma abd_reads_all_bw : "x \<in> {NicA, NicB, NicD} \<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 x)" apply (rule subsetI) 
  (* refl cases *)
   apply (case_tac "partition_label x = xa") apply simp 
  (* non refl cases *)
   apply (case_tac "xa \<in> RMControls") apply (rule reads_all_rm_controlled_subjects, rule abd_reads_rm, simp, simp) apply (erule_tac a = xa in insertE, simp) apply (erule_tac a = xa in insertE, simp only:, rule abd_reads_rm, simp) apply (erule_tac a = xa in insertE, simp) apply (erule_tac a = xa in insertE, simp) apply (erule_tac a = xa in insertE, simp) apply (erule_tac a = xa in insertE, simp only:, rule abdrm_reads_ep, simp, blast) apply (erule_tac a = xa in insertE, simp only:, rule abdrm_reads_sc, simp, blast) apply (erule_tac a = xa in insertE, simp only:, rule abd_reads_c, simp) apply (erule_tac a = xa in insertE, simp only:, rule reads_ntfn1_via_sc, rule abdrm_reads_sc, simp, blast) apply (erule_tac a = xa in insertE, simp only:, rule reads_ntfn2_via_rm, rule abd_reads_rm, simp) apply (erule_tac a = xa in insertE, simp only:, rule reads_ntfn3_via_r, rule abd_reads_r, simp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> {NicA, NicB, NicD} \<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 x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; xa \<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> xa \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; xa \<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> xa \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; xa \<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}; partition_label x = xa\<rbrakk> \<Longrightarrow> xa \<in> subjectReads SACAuthGraph (partition_label x)
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; xa \<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}; partition_label x \<noteq> xa\<rbrakk> \<Longrightarrow> xa \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; xa \<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}; partition_label x \<noteq> xa\<rbrakk> \<Longrightarrow> xa \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; xa \<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}; partition_label x \<noteq> xa\<rbrakk> \<Longrightarrow> xa \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; xa \<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}; partition_label x \<noteq> xa; xa \<in> RMControls\<rbrakk> \<Longrightarrow> xa \<in> subjectReads SACAuthGraph (partition_label x)
 2. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; xa \<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}; partition_label x \<noteq> xa; xa \<notin> RMControls\<rbrakk> \<Longrightarrow> xa \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; xa \<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}; partition_label x \<noteq> xa; xa \<notin> RMControls\<rbrakk> \<Longrightarrow> xa \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<notin> RMControls; xa \<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> xa \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<notin> RMControls; xa \<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> xa \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<notin> RMControls; xa \<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> xa \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<notin> RMControls; xa \<in> {partition_label NicD, partition_label EP, partition_label SC, partition_label NicC, partition_label NTFN1, partition_label NTFN2, partition_label NTFN3}\<rbrakk> \<Longrightarrow> xa \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<notin> RMControls; xa \<in> {partition_label EP, partition_label SC, partition_label NicC, partition_label NTFN1, partition_label NTFN2, partition_label NTFN3}\<rbrakk> \<Longrightarrow> xa \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<notin> RMControls; xa \<in> {partition_label SC, partition_label NicC, partition_label NTFN1, partition_label NTFN2, partition_label NTFN3}\<rbrakk> \<Longrightarrow> xa \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<notin> RMControls; xa \<in> {partition_label NicC, partition_label NTFN1, partition_label NTFN2, partition_label NTFN3}\<rbrakk> \<Longrightarrow> xa \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<notin> RMControls; xa \<in> {partition_label NTFN1, partition_label NTFN2, partition_label NTFN3}\<rbrakk> \<Longrightarrow> xa \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<notin> RMControls; xa \<in> {partition_label NTFN2, partition_label NTFN3}\<rbrakk> \<Longrightarrow> xa \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<notin> RMControls; xa \<in> {partition_label NTFN3}\<rbrakk> \<Longrightarrow> xa \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<in> {NicA, NicB, NicD}; partition_label x \<noteq> xa; xa \<notin> RMControls; xa \<in> {}\<rbrakk> \<Longrightarrow> xa \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal:
No subgoals!