theory PolicyExample

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

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