theory PolicyExample

lemma subjectReads_CTR:
  "subjectReads example_auth_graph (partition_label CTR) = {partition_label CTR,partition_label C,partition_label EP, partition_label RM, partition_label NTFN1, partition_label NTFN2}" apply(clarsimp) apply(rule equalityI) apply(rule subsetI) apply(erule subjectReads.induct; auto) apply(auto simp: subjectReads_CTR'[simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. subjectReads example_auth_graph (partition_label CTR) = {partition_label CTR, partition_label C, partition_label EP, partition_label RM, partition_label NTFN1, partition_label NTFN2} proof (prove)
goal (1 subgoal):
 1. subjectReads (insert (partition_label T, Notify, partition_label NTFN1) (insert (partition_label CTR, Receive, partition_label NTFN1) (insert (partition_label C, Read, partition_label CTR) (insert (partition_label C, Write, partition_label CTR) (insert (partition_label CTR, Read, partition_label C) (insert (partition_label CTR, Write, partition_label C) (insert (partition_label CTR, SyncSend, partition_label EP) (insert (partition_label T, Notify, partition_label NTFN2) (insert (partition_label RM, Receive, partition_label NTFN2) (insert (partition_label RM, Receive, partition_label EP) {(a, b, y). a = y})))))))))) (partition_label CTR) = {partition_label CTR, partition_label C, partition_label EP, partition_label RM, partition_label NTFN1, partition_label NTFN2} proof (prove)
goal (2 subgoals):
 1. subjectReads (insert (partition_label T, Notify, partition_label NTFN1) (insert (partition_label CTR, Receive, partition_label NTFN1) (insert (partition_label C, Read, partition_label CTR) (insert (partition_label C, Write, partition_label CTR) (insert (partition_label CTR, Read, partition_label C) (insert (partition_label CTR, Write, partition_label C) (insert (partition_label CTR, SyncSend, partition_label EP) (insert (partition_label T, Notify, partition_label NTFN2) (insert (partition_label RM, Receive, partition_label NTFN2) (insert (partition_label RM, Receive, partition_label EP) {(a, b, y). a = y})))))))))) (partition_label CTR) \<subseteq> {partition_label CTR, partition_label C, partition_label EP, partition_label RM, partition_label NTFN1, partition_label NTFN2}
 2. {partition_label CTR, partition_label C, partition_label EP, partition_label RM, partition_label NTFN1, partition_label NTFN2} \<subseteq> subjectReads (insert (partition_label T, Notify, partition_label NTFN1) (insert (partition_label CTR, Receive, partition_label NTFN1) (insert (partition_label C, Read, partition_label CTR) (insert (partition_label C, Write, partition_label CTR) (insert (partition_label CTR, Read, partition_label C) (insert (partition_label CTR, Write, partition_label C) (insert (partition_label CTR, SyncSend, partition_label EP) (insert (partition_label T, Notify, partition_label NTFN2) (insert (partition_label RM, Receive, partition_label NTFN2) (insert (partition_label RM, Receive, partition_label EP) {(a, b, y). a = y})))))))))) (partition_label CTR) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> subjectReads (insert (partition_label T, Notify, partition_label NTFN1) (insert (partition_label CTR, Receive, partition_label NTFN1) (insert (partition_label C, Read, partition_label CTR) (insert (partition_label C, Write, partition_label CTR) (insert (partition_label CTR, Read, partition_label C) (insert (partition_label CTR, Write, partition_label C) (insert (partition_label CTR, SyncSend, partition_label EP) (insert (partition_label T, Notify, partition_label NTFN2) (insert (partition_label RM, Receive, partition_label NTFN2) (insert (partition_label RM, Receive, partition_label EP) {(a, b, y). a = y})))))))))) (partition_label CTR) \<Longrightarrow> x \<in> {partition_label CTR, partition_label C, partition_label EP, partition_label RM, partition_label NTFN1, partition_label NTFN2}
 2. {partition_label CTR, partition_label C, partition_label EP, partition_label RM, partition_label NTFN1, partition_label NTFN2} \<subseteq> subjectReads (insert (partition_label T, Notify, partition_label NTFN1) (insert (partition_label CTR, Receive, partition_label NTFN1) (insert (partition_label C, Read, partition_label CTR) (insert (partition_label C, Write, partition_label CTR) (insert (partition_label CTR, Read, partition_label C) (insert (partition_label CTR, Write, partition_label C) (insert (partition_label CTR, SyncSend, partition_label EP) (insert (partition_label T, Notify, partition_label NTFN2) (insert (partition_label RM, Receive, partition_label NTFN2) (insert (partition_label RM, Receive, partition_label EP) {(a, b, y). a = y})))))))))) (partition_label CTR) proof (prove)
goal (1 subgoal):
 1. {partition_label CTR, partition_label C, partition_label EP, partition_label RM, partition_label NTFN1, partition_label NTFN2} \<subseteq> subjectReads (insert (partition_label T, Notify, partition_label NTFN1) (insert (partition_label CTR, Receive, partition_label NTFN1) (insert (partition_label C, Read, partition_label CTR) (insert (partition_label C, Write, partition_label CTR) (insert (partition_label CTR, Read, partition_label C) (insert (partition_label CTR, Write, partition_label C) (insert (partition_label CTR, SyncSend, partition_label EP) (insert (partition_label T, Notify, partition_label NTFN2) (insert (partition_label RM, Receive, partition_label NTFN2) (insert (partition_label RM, Receive, partition_label EP) {(a, b, y). a = y})))))))))) (partition_label CTR) proof (prove)
goal:
No subgoals!