theory ExampleSystemPolicyFlows

lemma Sys3UT3Affects_correct_bw : "x \<in> Sys3Affects \<Longrightarrow> x \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel (UT3))" apply (simp add:Sys3AuthGraph_def Sys3AuthGraph_aux_def complete_AuthGraph_def Sys3Affects_def) apply (erule disjE) 
   (* UT3 affects UT3 *)
    apply (simp add:affects_lrefl) 
  (* UT3 affects EP3 *)
   apply (erule disjE) apply (rule_tac auth=SyncSend in affects_ep) apply simp apply (simp add:insertI1) 
  (* UT3 affects T3 *)
   apply (rule_tac auth=SyncSend and l' = "OrdinaryLabel (T3)" and ep="OrdinaryLabel (EP3)" in affects_send) apply (simp_all add:insertI1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> Sys3Affects \<Longrightarrow> x \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel UT3) proof (prove)
goal (1 subgoal):
 1. x = OrdinaryLabel UT3 \<or> x = OrdinaryLabel EP3 \<or> x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectAffects (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 UT3) proof (prove)
goal (2 subgoals):
 1. x = OrdinaryLabel UT3 \<Longrightarrow> x \<in> subjectAffects (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 UT3)
 2. x = OrdinaryLabel EP3 \<or> x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectAffects (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 UT3) proof (prove)
goal (2 subgoals):
 1. x = OrdinaryLabel UT3 \<Longrightarrow> x \<in> subjectAffects (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 UT3)
 2. x = OrdinaryLabel EP3 \<or> x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectAffects (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 UT3) proof (prove)
goal (1 subgoal):
 1. x = OrdinaryLabel EP3 \<or> x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectAffects (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 UT3) proof (prove)
goal (1 subgoal):
 1. x = OrdinaryLabel EP3 \<or> x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectAffects (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 UT3) proof (prove)
goal (2 subgoals):
 1. x = OrdinaryLabel EP3 \<Longrightarrow> x \<in> subjectAffects (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 UT3)
 2. x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectAffects (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 UT3) proof (prove)
goal (3 subgoals):
 1. x = OrdinaryLabel EP3 \<Longrightarrow> (OrdinaryLabel UT3, SyncSend, 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> SyncSend \<in> {Receive, Notify, SyncSend, Call, Reset}
 3. x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectAffects (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 UT3) proof (prove)
goal (2 subgoals):
 1. x = OrdinaryLabel EP3 \<Longrightarrow> SyncSend \<in> {Receive, Notify, SyncSend, Call, Reset}
 2. x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectAffects (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 UT3) proof (prove)
goal (1 subgoal):
 1. x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectAffects (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 UT3) proof (prove)
goal (1 subgoal):
 1. x = OrdinaryLabel T3 \<Longrightarrow> x \<in> subjectAffects (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 UT3) proof (prove)
goal (4 subgoals):
 1. x = OrdinaryLabel T3 \<Longrightarrow> (OrdinaryLabel UT3, 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 T3 \<Longrightarrow> SyncSend \<in> {SyncSend, Notify, Call}
 3. x = OrdinaryLabel T3 \<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})))
 4. x = OrdinaryLabel T3 \<Longrightarrow> (OrdinaryLabel T3, Write, 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}))) proof (prove)
goal:
No subgoals!