kings-crown/FVELER_Isabelle huggingface dataset:
theory PolicyExample

lemma subjectAffects_Low: "subjectAffects example_auth_graph2 (partition_label Low) = {partition_label Low,partition_label NTFN,partition_label SharedPage, partition_label High}" apply(rule equalityI) apply(rule subsetI) apply(erule subjectAffects.induct, fastforce+) apply(auto intro: affects_lrefl SharedPage_in_subjectAffects_Low NTFN_in_subjectAffects_Low High_in_subjectAffects_Low simp del: example_auth_graph2_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. subjectAffects example_auth_graph2 (partition_label Low) = {partition_label Low, partition_label NTFN, partition_label SharedPage, partition_label High} proof (prove)
goal (2 subgoals):
 1. subjectAffects example_auth_graph2 (partition_label Low) \<subseteq> {partition_label Low, partition_label NTFN, partition_label SharedPage, partition_label High}
 2. {partition_label Low, partition_label NTFN, partition_label SharedPage, partition_label High} \<subseteq> subjectAffects example_auth_graph2 (partition_label Low) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> subjectAffects example_auth_graph2 (partition_label Low) \<Longrightarrow> x \<in> {partition_label Low, partition_label NTFN, partition_label SharedPage, partition_label High}
 2. {partition_label Low, partition_label NTFN, partition_label SharedPage, partition_label High} \<subseteq> subjectAffects example_auth_graph2 (partition_label Low) proof (prove)
goal (1 subgoal):
 1. {partition_label Low, partition_label NTFN, partition_label SharedPage, partition_label High} \<subseteq> subjectAffects example_auth_graph2 (partition_label Low) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma subjectAffects_SharedPage: "subjectAffects example_auth_graph2 (partition_label SharedPage) = {partition_label SharedPage}" apply(rule equalityI) apply(rule subsetI) apply(erule subjectAffects.induct, fastforce+) apply(auto intro: affects_lrefl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. subjectAffects example_auth_graph2 (partition_label SharedPage) = {partition_label SharedPage} proof (prove)
goal (2 subgoals):
 1. subjectAffects example_auth_graph2 (partition_label SharedPage) \<subseteq> {partition_label SharedPage}
 2. {partition_label SharedPage} \<subseteq> subjectAffects example_auth_graph2 (partition_label SharedPage) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> subjectAffects example_auth_graph2 (partition_label SharedPage) \<Longrightarrow> x \<in> {partition_label SharedPage}
 2. {partition_label SharedPage} \<subseteq> subjectAffects example_auth_graph2 (partition_label SharedPage) proof (prove)
goal (1 subgoal):
 1. {partition_label SharedPage} \<subseteq> subjectAffects example_auth_graph2 (partition_label SharedPage) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma High_in_subjectAffects_NTFN:
  "partition_label High \<in> subjectAffects example_auth_graph2 (partition_label NTFN)" apply(rule affects_send[where ep="partition_label NTFN"]) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label High \<in> subjectAffects example_auth_graph2 (partition_label NTFN) proof (prove)
goal (4 subgoals):
 1. (partition_label NTFN, ?auth, partition_label NTFN) \<in> example_auth_graph2
 2. ?auth \<in> {SyncSend, Notify, Call}
 3. (?l', Receive, partition_label NTFN) \<in> example_auth_graph2
 4. (?l', Write, partition_label High) \<in> example_auth_graph2 proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma subjectAffects_NTFN: "subjectAffects example_auth_graph2 (partition_label NTFN) = {partition_label NTFN,partition_label High}" apply(rule equalityI) apply(rule subsetI) apply(erule subjectAffects.induct, fastforce+) apply(auto intro: affects_lrefl High_in_subjectAffects_NTFN simp del: example_auth_graph2_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. subjectAffects example_auth_graph2 (partition_label NTFN) = {partition_label NTFN, partition_label High} proof (prove)
goal (2 subgoals):
 1. subjectAffects example_auth_graph2 (partition_label NTFN) \<subseteq> {partition_label NTFN, partition_label High}
 2. {partition_label NTFN, partition_label High} \<subseteq> subjectAffects example_auth_graph2 (partition_label NTFN) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> subjectAffects example_auth_graph2 (partition_label NTFN) \<Longrightarrow> x \<in> {partition_label NTFN, partition_label High}
 2. {partition_label NTFN, partition_label High} \<subseteq> subjectAffects example_auth_graph2 (partition_label NTFN) proof (prove)
goal (1 subgoal):
 1. {partition_label NTFN, partition_label High} \<subseteq> subjectAffects example_auth_graph2 (partition_label NTFN) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma NTFN_in_subjectAffects_High:
  "partition_label NTFN \<in> subjectAffects example_auth_graph2 (partition_label High)" apply(fastforce intro: affects_ep) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label NTFN \<in> subjectAffects example_auth_graph2 (partition_label High) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma subjectAffects_High: "subjectAffects example_auth_graph2 (partition_label High) = {partition_label NTFN,partition_label High}" apply(rule equalityI) apply(rule subsetI) apply(erule subjectAffects.induct, fastforce+) apply(auto intro: affects_lrefl NTFN_in_subjectAffects_High simp del: example_auth_graph2_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. subjectAffects example_auth_graph2 (partition_label High) = {partition_label NTFN, partition_label High} proof (prove)
goal (2 subgoals):
 1. subjectAffects example_auth_graph2 (partition_label High) \<subseteq> {partition_label NTFN, partition_label High}
 2. {partition_label NTFN, partition_label High} \<subseteq> subjectAffects example_auth_graph2 (partition_label High) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> subjectAffects example_auth_graph2 (partition_label High) \<Longrightarrow> x \<in> {partition_label NTFN, partition_label High}
 2. {partition_label NTFN, partition_label High} \<subseteq> subjectAffects example_auth_graph2 (partition_label High) proof (prove)
goal (1 subgoal):
 1. {partition_label NTFN, partition_label High} \<subseteq> subjectAffects example_auth_graph2 (partition_label High) proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma partsSubjectAffects_Low: "partsSubjectAffects example_auth_graph2 Low = {Partition Low, Partition High, Partition SharedPage, Partition NTFN}" apply(auto simp: partsSubjectAffects_def image_def label_can_affect_partition_def subjectReads_2 subjectAffects_Low | case_tac xa, rename_tac xa)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partsSubjectAffects example_auth_graph2 Low = {Partition Low, Partition High, Partition SharedPage, Partition NTFN} proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma partsSubjectAffects_SharedPage: "partsSubjectAffects example_auth_graph2 SharedPage = {Partition SharedPage, Partition High, Partition Low, Partition NTFN}" apply(auto simp: partsSubjectAffects_def image_def label_can_affect_partition_def subjectReads_2 subjectAffects_SharedPage | rename_tac xa, case_tac xa)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partsSubjectAffects example_auth_graph2 SharedPage = {Partition SharedPage, Partition High, Partition Low, Partition NTFN} proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma partsSubjectAffects_NTFN: "partsSubjectAffects example_auth_graph2 NTFN = {Partition NTFN, Partition High}" apply(auto simp: partsSubjectAffects_def image_def label_can_affect_partition_def subjectReads_2 subjectAffects_NTFN | rename_tac xa, case_tac xa)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partsSubjectAffects example_auth_graph2 NTFN = {Partition NTFN, Partition High} proof (prove)
goal:
No subgoals!
theory PolicyExample

lemma partsSubjectAffects_High: "partsSubjectAffects example_auth_graph2 High = {Partition High, Partition NTFN}" apply(auto simp: partsSubjectAffects_def image_def label_can_affect_partition_def subjectReads_2 subjectAffects_High | rename_tac xa, case_tac xa)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partsSubjectAffects example_auth_graph2 High = {Partition High, Partition NTFN} proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma reads_all_rm_controlled_subjects : "\<lbrakk>partition_label RM \<in> subjectReads SACAuthGraph (partition_label x); l \<in> RMControls\<rbrakk> \<Longrightarrow> l \<in> subjectReads SACAuthGraph (partition_label x)" apply (simp only:RMControls_def) apply (erule insertE, rule_tac t="partition_label RM" in reads_read_thread_read_pages, simp, simp)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>partition_label RM \<in> subjectReads SACAuthGraph (partition_label x); l \<in> RMControls\<rbrakk> \<Longrightarrow> l \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>partition_label RM \<in> subjectReads SACAuthGraph (partition_label x); l \<in> {partition_label RM, partition_label R, partition_label NicA, partition_label NicB, partition_label NicD}\<rbrakk> \<Longrightarrow> l \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>partition_label RM \<in> subjectReads SACAuthGraph (partition_label x); l \<in> {}\<rbrakk> \<Longrightarrow> l \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma reads_ntfn3_via_r : "partition_label R \<in> subjectReads SACAuthGraph (partition_label x) \<Longrightarrow> partition_label NTFN3 \<in> subjectReads SACAuthGraph (partition_label x)" apply (rule_tac ep="partition_label NTFN3" and t="partition_label R" and auth="Receive" and auth'="Notify" and a="partition_label T" in reads_read_queued_thread_read_ep) apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label R \<in> subjectReads SACAuthGraph (partition_label x) \<Longrightarrow> partition_label NTFN3 \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (5 subgoals):
 1. partition_label R \<in> subjectReads SACAuthGraph (partition_label x) \<Longrightarrow> (partition_label T, Notify, partition_label NTFN3) \<in> SACAuthGraph
 2. partition_label R \<in> subjectReads SACAuthGraph (partition_label x) \<Longrightarrow> Notify \<in> {Notify, SyncSend, Reset}
 3. partition_label R \<in> subjectReads SACAuthGraph (partition_label x) \<Longrightarrow> (partition_label R, Receive, partition_label NTFN3) \<in> SACAuthGraph
 4. partition_label R \<in> subjectReads SACAuthGraph (partition_label x) \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 5. partition_label R \<in> subjectReads SACAuthGraph (partition_label x) \<Longrightarrow> partition_label R \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma reads_ntfn2_via_rm : "partition_label RM \<in> subjectReads SACAuthGraph (partition_label x) \<Longrightarrow> partition_label NTFN2 \<in> subjectReads SACAuthGraph (partition_label x)" apply (rule_tac ep="partition_label NTFN2" and t="partition_label RM" and auth="Receive" and auth'="Notify" and a="partition_label T" in reads_read_queued_thread_read_ep) apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label RM \<in> subjectReads SACAuthGraph (partition_label x) \<Longrightarrow> partition_label NTFN2 \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (5 subgoals):
 1. partition_label RM \<in> subjectReads SACAuthGraph (partition_label x) \<Longrightarrow> (partition_label T, Notify, partition_label NTFN2) \<in> SACAuthGraph
 2. partition_label RM \<in> subjectReads SACAuthGraph (partition_label x) \<Longrightarrow> Notify \<in> {Notify, SyncSend, Reset}
 3. partition_label RM \<in> subjectReads SACAuthGraph (partition_label x) \<Longrightarrow> (partition_label RM, Receive, partition_label NTFN2) \<in> SACAuthGraph
 4. partition_label RM \<in> subjectReads SACAuthGraph (partition_label x) \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 5. partition_label RM \<in> subjectReads SACAuthGraph (partition_label x) \<Longrightarrow> partition_label RM \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma reads_ntfn1_via_sc : "partition_label SC \<in> subjectReads SACAuthGraph (partition_label x) \<Longrightarrow> partition_label NTFN1 \<in> subjectReads SACAuthGraph (partition_label x)" apply (rule_tac ep="partition_label NTFN1" and t="partition_label SC" and auth="Receive" and auth'="Notify" and a="partition_label T" in reads_read_queued_thread_read_ep) apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label SC \<in> subjectReads SACAuthGraph (partition_label x) \<Longrightarrow> partition_label NTFN1 \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (5 subgoals):
 1. partition_label SC \<in> subjectReads SACAuthGraph (partition_label x) \<Longrightarrow> (partition_label T, Notify, partition_label NTFN1) \<in> SACAuthGraph
 2. partition_label SC \<in> subjectReads SACAuthGraph (partition_label x) \<Longrightarrow> Notify \<in> {Notify, SyncSend, Reset}
 3. partition_label SC \<in> subjectReads SACAuthGraph (partition_label x) \<Longrightarrow> (partition_label SC, Receive, partition_label NTFN1) \<in> SACAuthGraph
 4. partition_label SC \<in> subjectReads SACAuthGraph (partition_label x) \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 5. partition_label SC \<in> subjectReads SACAuthGraph (partition_label x) \<Longrightarrow> partition_label SC \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma reads_Control_rev':
  "(x,Control,y) \<in> aag \<Longrightarrow>
    x \<in> subjectReads (complete_AgentAuthGraph aag) y" apply(rule reads_read_page_read_thread) apply(rule reads_lrefl) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, Control, y) \<in> aag \<Longrightarrow> x \<in> subjectReads (complete_AgentAuthGraph aag) y proof (prove)
goal (2 subgoals):
 1. (x, Control, y) \<in> aag \<Longrightarrow> ?b \<in> subjectReads (complete_AgentAuthGraph aag) y
 2. (x, Control, y) \<in> aag \<Longrightarrow> (x, Write, ?b) \<in> complete_AgentAuthGraph aag proof (prove)
goal (1 subgoal):
 1. (x, Control, y) \<in> aag \<Longrightarrow> (x, Write, y) \<in> complete_AgentAuthGraph aag proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma reads_Control_rev:
  "(x,Control,y) \<in> SACGraph \<Longrightarrow>
   x \<in> subjectReads SACAuthGraph y" apply(subst SACAuthGraph_def) apply(erule reads_Control_rev') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, Control, y) \<in> SACGraph \<Longrightarrow> x \<in> subjectReads SACAuthGraph y proof (prove)
goal (1 subgoal):
 1. (x, Control, y) \<in> SACGraph \<Longrightarrow> x \<in> subjectReads (complete_AgentAuthGraph SACGraph) y proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma abdrm_reads_ep : "x \<in> {NicA, NicB, NicD, RM} \<Longrightarrow> partition_label EP \<in> subjectReads SACAuthGraph (partition_label x)" apply (rule_tac t = "partition_label RM" and a = "partition_label SC" and auth' = "SyncSend" and auth = "Receive" in reads_read_queued_thread_read_ep) apply (simp+)[4] apply safe apply(fastforce intro: reads_Control_rev simp del: complete_AgentAuthGraph_def) apply(fastforce intro: reads_Control_rev simp del: complete_AgentAuthGraph_def) apply(fastforce intro: reads_Control_rev simp del: complete_AgentAuthGraph_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> {NicA, NicB, NicD, RM} \<Longrightarrow> partition_label EP \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (5 subgoals):
 1. x \<in> {NicA, NicB, NicD, RM} \<Longrightarrow> (partition_label SC, SyncSend, partition_label EP) \<in> SACAuthGraph
 2. x \<in> {NicA, NicB, NicD, RM} \<Longrightarrow> SyncSend \<in> {Notify, SyncSend, Reset}
 3. x \<in> {NicA, NicB, NicD, RM} \<Longrightarrow> (partition_label RM, Receive, partition_label EP) \<in> SACAuthGraph
 4. x \<in> {NicA, NicB, NicD, RM} \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 5. x \<in> {NicA, NicB, NicD, RM} \<Longrightarrow> partition_label RM \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. x \<in> {NicA, NicB, NicD, RM} \<Longrightarrow> partition_label RM \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (3 subgoals):
 1. x = NicA \<Longrightarrow> partition_label RM \<in> subjectReads SACAuthGraph (partition_label NicA)
 2. x = NicB \<Longrightarrow> partition_label RM \<in> subjectReads SACAuthGraph (partition_label NicB)
 3. x = NicD \<Longrightarrow> partition_label RM \<in> subjectReads SACAuthGraph (partition_label NicD) proof (prove)
goal (2 subgoals):
 1. x = NicB \<Longrightarrow> partition_label RM \<in> subjectReads SACAuthGraph (partition_label NicB)
 2. x = NicD \<Longrightarrow> partition_label RM \<in> subjectReads SACAuthGraph (partition_label NicD) proof (prove)
goal (1 subgoal):
 1. x = NicD \<Longrightarrow> partition_label RM \<in> subjectReads SACAuthGraph (partition_label NicD) proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma abd_reads_rm : "x \<in> {NicA, NicB, NicD} \<Longrightarrow> partition_label RM \<in> subjectReads SACAuthGraph (partition_label x)" apply (rule reads_Control_rev) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> {NicA, NicB, NicD} \<Longrightarrow> partition_label RM \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (1 subgoal):
 1. x \<in> {NicA, NicB, NicD} \<Longrightarrow> (partition_label RM, Control, partition_label x) \<in> SACGraph proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma abd_reads_c : "x \<in> {NicA, NicB, NicD} \<Longrightarrow> partition_label NicC \<in> subjectReads SACAuthGraph (partition_label x)" apply (rule_tac t = "partition_label SC" in reads_read_thread_read_pages) apply (rule abdrm_reads_sc, simp, blast, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> {NicA, NicB, NicD} \<Longrightarrow> partition_label NicC \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (2 subgoals):
 1. x \<in> {NicA, NicB, NicD} \<Longrightarrow> partition_label SC \<in> subjectReads SACAuthGraph (partition_label x)
 2. x \<in> {NicA, NicB, NicD} \<Longrightarrow> (partition_label SC, Read, partition_label NicC) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma abd_reads_r : "x \<in> {NicA, NicB, NicD} \<Longrightarrow> partition_label R \<in> subjectReads SACAuthGraph (partition_label x)" apply (rule_tac p="partition_label R" and t="partition_label RM" in reads_read_thread_read_pages) apply (rule abd_reads_rm, simp, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> {NicA, NicB, NicD} \<Longrightarrow> partition_label R \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (2 subgoals):
 1. x \<in> {NicA, NicB, NicD} \<Longrightarrow> partition_label RM \<in> subjectReads SACAuthGraph (partition_label x)
 2. x \<in> {NicA, NicB, NicD} \<Longrightarrow> (partition_label RM, Read, partition_label R) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma abd_reads_ntfn3 : "x \<in> {NicA, NicB, NicD} \<Longrightarrow> partition_label NTFN3 \<in> subjectReads SACAuthGraph (partition_label x)" apply (rule_tac ep="partition_label NTFN3" and t="partition_label R" and auth="Receive" and auth'="Notify" and a="partition_label T" in reads_read_queued_thread_read_ep) apply (simp_all add: abd_reads_r del:SACAuthGraph_def, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> {NicA, NicB, NicD} \<Longrightarrow> partition_label NTFN3 \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal (5 subgoals):
 1. x \<in> {NicA, NicB, NicD} \<Longrightarrow> (partition_label T, Notify, partition_label NTFN3) \<in> SACAuthGraph
 2. x \<in> {NicA, NicB, NicD} \<Longrightarrow> Notify \<in> {Notify, SyncSend, Reset}
 3. x \<in> {NicA, NicB, NicD} \<Longrightarrow> (partition_label R, Receive, partition_label NTFN3) \<in> SACAuthGraph
 4. x \<in> {NicA, NicB, NicD} \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 5. x \<in> {NicA, NicB, NicD} \<Longrightarrow> partition_label R \<in> subjectReads SACAuthGraph (partition_label x) proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma c_reads_sc : "partition_label SC \<in> subjectReads SACAuthGraph (partition_label NicC)" apply (rule_tac b = "partition_label NicC" in reads_read_page_read_thread) apply (rule reads_lrefl) apply (simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label SC \<in> subjectReads SACAuthGraph (partition_label NicC) proof (prove)
goal (2 subgoals):
 1. partition_label NicC \<in> subjectReads SACAuthGraph (partition_label NicC)
 2. (partition_label SC, Write, partition_label NicC) \<in> SACAuthGraph proof (prove)
goal (1 subgoal):
 1. (partition_label SC, Write, partition_label NicC) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma c_reads_ep : "partition_label EP \<in> subjectReads SACAuthGraph (partition_label NicC)" apply (rule_tac a = "partition_label EP" and ep = "partition_label EP" and t = "partition_label SC" and auth = "SyncSend" and auth' = "Reset" in reads_read_queued_thread_read_ep) apply (simp,simp,simp,simp) apply (rule c_reads_sc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label EP \<in> subjectReads SACAuthGraph (partition_label NicC) proof (prove)
goal (5 subgoals):
 1. (partition_label EP, Reset, partition_label EP) \<in> SACAuthGraph
 2. Reset \<in> {Notify, SyncSend, Reset}
 3. (partition_label SC, SyncSend, partition_label EP) \<in> SACAuthGraph
 4. SyncSend \<in> {SyncSend, Receive}
 5. partition_label SC \<in> subjectReads SACAuthGraph (partition_label NicC) proof (prove)
goal (1 subgoal):
 1. partition_label SC \<in> subjectReads SACAuthGraph (partition_label NicC) proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma c_reads_rm : "partition_label RM \<in> subjectReads SACAuthGraph (partition_label NicC)" apply (rule_tac ep = "partition_label EP" in read_sync_ep_read_receivers) apply (rule c_reads_ep) apply (simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label RM \<in> subjectReads SACAuthGraph (partition_label NicC) proof (prove)
goal (2 subgoals):
 1. partition_label EP \<in> subjectReads SACAuthGraph (partition_label NicC)
 2. (partition_label RM, Receive, partition_label EP) \<in> SACAuthGraph proof (prove)
goal (1 subgoal):
 1. (partition_label RM, Receive, partition_label EP) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma c_reads_any_controlled_by_rm : "x \<in> {partition_label R, partition_label NicA, partition_label NicB, partition_label NicD} \<Longrightarrow> x \<in> subjectReads SACAuthGraph (partition_label NicC)" apply (rule_tac t = "partition_label RM" in reads_read_thread_read_pages) apply (rule c_reads_rm) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> {partition_label R, partition_label NicA, partition_label NicB, partition_label NicD} \<Longrightarrow> x \<in> subjectReads SACAuthGraph (partition_label NicC) proof (prove)
goal (2 subgoals):
 1. x \<in> {partition_label R, partition_label NicA, partition_label NicB, partition_label NicD} \<Longrightarrow> partition_label RM \<in> subjectReads SACAuthGraph (partition_label NicC)
 2. x \<in> {partition_label R, partition_label NicA, partition_label NicB, partition_label NicD} \<Longrightarrow> (partition_label RM, Read, x) \<in> SACAuthGraph proof (prove)
goal (1 subgoal):
 1. x \<in> {partition_label R, partition_label NicA, partition_label NicB, partition_label NicD} \<Longrightarrow> (partition_label RM, Read, x) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!