theory ExampleSystemPolicyFlows

lemma Sys3T3Reads_correct_bw : "x \<in> Sys3Reads \<Longrightarrow> x \<in> subjectReads Sys3AuthGraph (OrdinaryLabel (T3))" apply (simp add: Sys3AuthGraph_def Sys3AuthGraph_aux_def complete_AuthGraph_def Sys3Reads_def) apply (erule disjE) 
   (* T3 reads UT3 *)
    apply (rule_tac ep = "OrdinaryLabel (EP3)" in read_sync_ep_read_senders) apply (rule_tac auth = Receive in reads_ep) apply (simp) apply (simp add:insertI1) apply (simp add: insertI1) 
  (* T3 reads EP3 *)
   apply (erule disjE) apply (rule_tac auth = Receive in reads_ep) apply (simp) apply (simp add:insertI1) 
  (* T3 reads T3 *)
   apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> Sys3Reads \<Longrightarrow> x \<in> subjectReads Sys3AuthGraph (OrdinaryLabel T3) proof (prove)
goal (1 subgoal):
 1. x = OrdinaryLabel UT3 \<or> x = OrdinaryLabel EP3 \<or> x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel T3) proof (prove)
goal (2 subgoals):
 1. x = OrdinaryLabel UT3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel T3)
 2. x = OrdinaryLabel EP3 \<or> x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel T3) proof (prove)
goal (2 subgoals):
 1. x = OrdinaryLabel UT3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel T3)
 2. x = OrdinaryLabel EP3 \<or> x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel T3) proof (prove)
goal (3 subgoals):
 1. x = OrdinaryLabel UT3 \<Longrightarrow> OrdinaryLabel EP3 \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel T3)
 2. x = OrdinaryLabel UT3 \<Longrightarrow> (x, SyncSend, OrdinaryLabel EP3) \<in> insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))
 3. x = OrdinaryLabel EP3 \<or> x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel T3) proof (prove)
goal (4 subgoals):
 1. x = OrdinaryLabel UT3 \<Longrightarrow> (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) \<in> insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))
 2. x = OrdinaryLabel UT3 \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 3. x = OrdinaryLabel UT3 \<Longrightarrow> (x, SyncSend, OrdinaryLabel EP3) \<in> insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))
 4. x = OrdinaryLabel EP3 \<or> x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel T3) proof (prove)
goal (3 subgoals):
 1. x = OrdinaryLabel UT3 \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 2. x = OrdinaryLabel UT3 \<Longrightarrow> (x, SyncSend, OrdinaryLabel EP3) \<in> insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))
 3. x = OrdinaryLabel EP3 \<or> x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel T3) proof (prove)
goal (2 subgoals):
 1. x = OrdinaryLabel UT3 \<Longrightarrow> (x, SyncSend, OrdinaryLabel EP3) \<in> insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))
 2. x = OrdinaryLabel EP3 \<or> x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel T3) proof (prove)
goal (1 subgoal):
 1. x = OrdinaryLabel EP3 \<or> x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel T3) proof (prove)
goal (1 subgoal):
 1. x = OrdinaryLabel EP3 \<or> x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel T3) proof (prove)
goal (2 subgoals):
 1. x = OrdinaryLabel EP3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel T3)
 2. x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel T3) proof (prove)
goal (3 subgoals):
 1. x = OrdinaryLabel EP3 \<Longrightarrow> (OrdinaryLabel T3, Receive, x) \<in> insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))
 2. x = OrdinaryLabel EP3 \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 3. x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel T3) proof (prove)
goal (2 subgoals):
 1. x = OrdinaryLabel EP3 \<Longrightarrow> Receive \<in> {SyncSend, Receive}
 2. x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel T3) proof (prove)
goal (1 subgoal):
 1. x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel T3) proof (prove)
goal (1 subgoal):
 1. x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectReads (insert (OrdinaryLabel UT3, SyncSend, OrdinaryLabel EP3) (insert (OrdinaryLabel UT3, Reset, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Receive, OrdinaryLabel EP3) (insert (OrdinaryLabel T3, Reset, OrdinaryLabel EP3) {(l, a, l) |a l. l = OrdinaryLabel T3 \<or> l = OrdinaryLabel UT3})))) (OrdinaryLabel T3) proof (prove)
goal:
No subgoals!