kings-crown/FVELER_Isabelle huggingface dataset:
theory PolicySystemSAC

lemma ntfn13_reads_ntfn2 : "l \<in> {NTFN1, NTFN3} \<Longrightarrow> partition_label NTFN2 \<in> subjectReads SACAuthGraph (partition_label l)" apply (rule_tac t="partition_label RM" and auth="Receive" and auth'="Reset" and a="partition_label NTFN2" in reads_read_queued_thread_read_ep) apply (simp, simp, simp, simp) apply (erule insertE, simp only:, rule ntfn1_reads_rm, erule insertE, simp only:, rule ntfn3_reads_rm, simp) done

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

lemma ntfn12_reads_ntfn3 : "l \<in> {NTFN1, NTFN2} \<Longrightarrow> partition_label NTFN3 \<in> subjectReads SACAuthGraph (partition_label l)" apply (rule_tac t="partition_label R" and auth="Receive" and auth'="Reset" and a="partition_label NTFN3" in reads_read_queued_thread_read_ep) apply (simp, simp, simp, simp) apply (erule insertE, simp only:, rule reads_all_rm_controlled_subjects, rule ntfn1_reads_rm, simp, erule insertE, simp only:, rule reads_all_rm_controlled_subjects, rule ntfn2_reads_rm, simp_all) done

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

lemma ntfn23_reads_ntfn1 : "l \<in> {NTFN2, NTFN3} \<Longrightarrow> partition_label NTFN1 \<in> subjectReads SACAuthGraph (partition_label l)" apply (rule_tac t="partition_label SC" and auth="Receive" and auth'="Reset" and a="partition_label NTFN1" in reads_read_queued_thread_read_ep) apply (simp, simp, simp, simp) apply (erule insertE, simp only:, rule ntfn2_reads_sc, erule insertE, simp only:, rule ntfn3_reads_sc, simp) done

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

lemma ntfn123_reads_rm : "l \<in> {NTFN1, NTFN2, NTFN3} \<Longrightarrow> partition_label RM \<in> subjectReads SACAuthGraph (partition_label l)" by (auto simp:ntfn1_reads_rm ntfn2_reads_rm ntfn3_reads_rm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. l \<in> {NTFN1, NTFN2, NTFN3} \<Longrightarrow> partition_label RM \<in> subjectReads SACAuthGraph (partition_label l)
theory PolicySystemSAC

lemma ntfn123_reads_sc : "l \<in> {NTFN1, NTFN2, NTFN3} \<Longrightarrow> partition_label SC \<in> subjectReads SACAuthGraph (partition_label l)" by (auto simp:ntfn1_reads_sc ntfn2_reads_sc ntfn3_reads_sc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. l \<in> {NTFN1, NTFN2, NTFN3} \<Longrightarrow> partition_label SC \<in> subjectReads SACAuthGraph (partition_label l)
theory PolicySystemSAC

lemma ntfn123_reads_ep : "l \<in> {NTFN1, NTFN2, NTFN3} \<Longrightarrow> partition_label EP \<in> subjectReads SACAuthGraph (partition_label l)" by (auto simp:ntfn1_reads_ep ntfn2_reads_ep ntfn3_reads_ep)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. l \<in> {NTFN1, NTFN2, NTFN3} \<Longrightarrow> partition_label EP \<in> subjectReads SACAuthGraph (partition_label l)
theory PolicySystemSAC

lemma ntfn123_reads_ntfn123 : "\<lbrakk>l \<in> {NTFN1, NTFN2, NTFN3}; x \<in> {NTFN1, NTFN2, NTFN3}\<rbrakk> \<Longrightarrow> partition_label l \<in> subjectReads SACAuthGraph (partition_label x)" by (auto simp:ntfn12_reads_ntfn3 ntfn13_reads_ntfn2 ntfn23_reads_ntfn1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>l \<in> {NTFN1, NTFN2, NTFN3}; x \<in> {NTFN1, NTFN2, NTFN3}\<rbrakk> \<Longrightarrow> partition_label l \<in> subjectReads SACAuthGraph (partition_label x)
theory PolicySystemSAC

lemma ntfn1_affects_sc : "partition_label SC \<in> subjectAffects SACAuthGraph (partition_label NTFN1)" apply (rule_tac l''="partition_label SC" and l'="partition_label SC" and ep="partition_label NTFN1" and auth="Notify" and l="partition_label NTFN1" in affects_send) apply (simp_all add:SACAuthGraph_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label SC \<in> subjectAffects SACAuthGraph (partition_label NTFN1) proof (prove)
goal (4 subgoals):
 1. (partition_label NTFN1, Notify, partition_label NTFN1) \<in> SACAuthGraph
 2. Notify \<in> {SyncSend, Notify, Call}
 3. (partition_label SC, Receive, partition_label NTFN1) \<in> SACAuthGraph
 4. (partition_label SC, Write, partition_label SC) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma ntfn1_affects_c : "partition_label NicC \<in> subjectAffects SACAuthGraph (partition_label NTFN1)" apply (rule_tac l'="partition_label SC" and ep="partition_label NTFN1" and l="partition_label NTFN1" and auth="Notify" in affects_send) apply (simp_all add:SACAuthGraph_def) done

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

lemma ntfn2_affects_rm : "partition_label RM \<in> subjectAffects SACAuthGraph (partition_label NTFN2)" apply (rule_tac l'="partition_label RM" and ep="partition_label NTFN2" and auth="Notify" and l="partition_label NTFN2" in affects_send) apply (simp_all add:SACAuthGraph_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label RM \<in> subjectAffects SACAuthGraph (partition_label NTFN2) proof (prove)
goal (4 subgoals):
 1. (partition_label NTFN2, Notify, partition_label NTFN2) \<in> SACAuthGraph
 2. Notify \<in> {SyncSend, Notify, Call}
 3. (partition_label RM, Receive, partition_label NTFN2) \<in> SACAuthGraph
 4. (partition_label RM, Write, partition_label RM) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma ntfn2_affects_ep : "partition_label EP \<in> subjectAffects SACAuthGraph (partition_label NTFN2)" apply (rule affects_ep_bound_trans) by (auto simp: SACAuthGraph_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label EP \<in> subjectAffects SACAuthGraph (partition_label NTFN2) proof (prove)
goal (1 subgoal):
 1. \<exists>tcb ntfn. (tcb, Receive, ntfn) \<in> SACAuthGraph \<and> (tcb, Receive, partition_label EP) \<in> SACAuthGraph \<and> (partition_label NTFN2, Notify, ntfn) \<in> SACAuthGraph
theory PolicySystemSAC

lemma ntfn2_affects_rm_controls : "x \<in> RMControls \<Longrightarrow> x \<in> subjectAffects SACAuthGraph (partition_label NTFN2)" apply (rule_tac l="partition_label NTFN2" and ep="partition_label NTFN2" and auth="SyncSend" and l'="partition_label RM" in affects_send) apply (simp_all add:SACAuthGraph_def) done

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

lemma ntfn3_affects_r : "partition_label R \<in> subjectAffects SACAuthGraph (partition_label NTFN3)" apply (rule_tac l'="partition_label R" and ep="partition_label NTFN3" and auth="Notify" and l="partition_label NTFN3" in affects_send) apply (simp_all add:SACAuthGraph_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label R \<in> subjectAffects SACAuthGraph (partition_label NTFN3) proof (prove)
goal (4 subgoals):
 1. (partition_label NTFN3, Notify, partition_label NTFN3) \<in> SACAuthGraph
 2. Notify \<in> {SyncSend, Notify, Call}
 3. (partition_label R, Receive, partition_label NTFN3) \<in> SACAuthGraph
 4. (partition_label R, Write, partition_label R) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma t_reads : "subjectReads SACAuthGraph (partition_label T) = {partition_label T}" apply (rule subset_antisym) defer apply (rule subsetI, erule insertE, simp only:, rule reads_lrefl, simp) apply (rule subsetI, erule subjectReads.induct) apply (simp add:SACAuthGraph_def, blast?)+ done

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

lemma t_affects_ntfn123 : "l \<in> {NTFN1, NTFN2, NTFN3} \<Longrightarrow>  partition_label l \<in> subjectAffects SACAuthGraph (partition_label T)" apply (rule_tac auth="Notify" in affects_ep) apply (simp_all add:SACAuthGraph_def, blast) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. l \<in> {NTFN1, NTFN2, NTFN3} \<Longrightarrow> partition_label l \<in> subjectAffects SACAuthGraph (partition_label T) proof (prove)
goal (2 subgoals):
 1. l \<in> {NTFN1, NTFN2, NTFN3} \<Longrightarrow> (partition_label T, Notify, partition_label l) \<in> SACAuthGraph
 2. l \<in> {NTFN1, NTFN2, NTFN3} \<Longrightarrow> Notify \<in> {Receive, Notify, SyncSend, Call, Reset} proof (prove)
goal:
No subgoals!
theory PolicySystemSAC

lemma t_affects_sc : "partition_label SC \<in> subjectAffects SACAuthGraph (partition_label T)" apply (rule_tac l''="partition_label SC" and l'="partition_label SC" and ep="partition_label NTFN1" and auth="Notify" and l="partition_label T" in affects_send) apply (simp_all add:SACAuthGraph_def) done

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

lemma t_affects_rm : "partition_label RM \<in> subjectAffects SACAuthGraph (partition_label T)" apply (rule_tac l''="partition_label RM" and l'="partition_label RM" and ep="partition_label NTFN2" and auth="Notify" and l="partition_label T" in affects_send) apply (simp_all add:SACAuthGraph_def) done

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

lemma t_affects_r : "partition_label R \<in> subjectAffects SACAuthGraph (partition_label T)" apply (rule_tac l''="partition_label R" and l'="partition_label R" and ep="partition_label NTFN3" and auth="Notify" and l="partition_label T" in affects_send) apply (simp_all add:SACAuthGraph_def) done

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

lemma t_affects_ep : "partition_label EP \<in> subjectAffects SACAuthGraph (partition_label T)" apply (rule affects_ep_bound_trans) by (auto simp: SACAuthGraph_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partition_label EP \<in> subjectAffects SACAuthGraph (partition_label T) proof (prove)
goal (1 subgoal):
 1. \<exists>tcb ntfn. (tcb, Receive, ntfn) \<in> SACAuthGraph \<and> (tcb, Receive, partition_label EP) \<in> SACAuthGraph \<and> (partition_label T, Notify, ntfn) \<in> SACAuthGraph
theory PolicySystemSAC

lemma t_affects_c : "partition_label NicC \<in> subjectAffects SACAuthGraph (partition_label T)" apply (rule_tac l''="partition_label NicC" and l'="partition_label SC" and ep="partition_label NTFN1" and auth="Notify" and l="partition_label T" in affects_send) apply (simp_all add:SACAuthGraph_def) done

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

lemma t_affects_a : "partition_label NicA \<in> subjectAffects SACAuthGraph (partition_label T)" apply (rule_tac l''="partition_label NicA" and l'="partition_label RM" and ep="partition_label NTFN2" and auth="Notify" and l="partition_label T" in affects_send) apply (simp_all add:SACAuthGraph_def) done

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

lemma t_affects_bd : "l \<in> {NicB, NicD} \<Longrightarrow> partition_label l \<in> subjectAffects SACAuthGraph (partition_label T)" apply (rule_tac l'="partition_label R" and ep="partition_label NTFN3" and auth="Notify" and l="partition_label T" in affects_send) apply (simp_all add:SACAuthGraph_def, blast) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. l \<in> {NicB, NicD} \<Longrightarrow> partition_label l \<in> subjectAffects SACAuthGraph (partition_label T) proof (prove)
goal (4 subgoals):
 1. l \<in> {NicB, NicD} \<Longrightarrow> (partition_label T, Notify, partition_label NTFN3) \<in> SACAuthGraph
 2. l \<in> {NicB, NicD} \<Longrightarrow> Notify \<in> {SyncSend, Notify, Call}
 3. l \<in> {NicB, NicD} \<Longrightarrow> (partition_label R, Receive, partition_label NTFN3) \<in> SACAuthGraph
 4. l \<in> {NicB, NicD} \<Longrightarrow> (partition_label R, Write, partition_label l) \<in> SACAuthGraph proof (prove)
goal:
No subgoals!
theory ExampleSystemPolicyFlows

lemma Sys3Reads_correct_fw : "\<lbrakk>x \<in> subjectReads Sys3AuthGraph (OrdinaryLabel (l)); l \<in> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> x \<in> Sys3Reads" apply (induct x rule:subjectReads.induct) apply (auto simp:Sys3AuthGraph_def Sys3AuthGraph_aux_def complete_AuthGraph_def Sys3Reads_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> subjectReads Sys3AuthGraph (OrdinaryLabel l); l \<in> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> x \<in> Sys3Reads proof (prove)
goal (13 subgoals):
 1. \<And>l'. \<lbrakk>(OrdinaryLabel l, Read, l') \<in> Sys3AuthGraph; l \<in> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> l' \<in> Sys3Reads
 2. l \<in> {T3, UT3, EP3} \<Longrightarrow> OrdinaryLabel l \<in> Sys3Reads
 3. \<And>auth ep. \<lbrakk>(OrdinaryLabel l, auth, ep) \<in> Sys3AuthGraph; auth \<in> {SyncSend, Receive}; l \<in> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> ep \<in> Sys3Reads
 4. \<And>a auth' ep t auth. \<lbrakk>(a, auth', ep) \<in> Sys3AuthGraph; auth' \<in> {Notify, SyncSend, Reset}; (t, auth, ep) \<in> Sys3AuthGraph; auth \<in> {SyncSend, Receive}; t \<in> subjectReads Sys3AuthGraph (OrdinaryLabel l); l \<in> {T3, UT3, EP3} \<Longrightarrow> t \<in> Sys3Reads; l \<in> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> ep \<in> Sys3Reads
 5. \<And>b t. \<lbrakk>b \<in> subjectReads Sys3AuthGraph (OrdinaryLabel l); l \<in> {T3, UT3, EP3} \<Longrightarrow> b \<in> Sys3Reads; (t, Write, b) \<in> Sys3AuthGraph; l \<in> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> t \<in> Sys3Reads
 6. \<And>t p. \<lbrakk>t \<in> subjectReads Sys3AuthGraph (OrdinaryLabel l); l \<in> {T3, UT3, EP3} \<Longrightarrow> t \<in> Sys3Reads; (t, Read, p) \<in> Sys3AuthGraph; l \<in> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> p \<in> Sys3Reads
 7. \<And>ep b. \<lbrakk>ep \<in> subjectReads Sys3AuthGraph (OrdinaryLabel l); l \<in> {T3, UT3, EP3} \<Longrightarrow> ep \<in> Sys3Reads; (b, SyncSend, ep) \<in> Sys3AuthGraph; l \<in> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> b \<in> Sys3Reads
 8. \<And>ep b. \<lbrakk>ep \<in> subjectReads Sys3AuthGraph (OrdinaryLabel l); l \<in> {T3, UT3, EP3} \<Longrightarrow> ep \<in> Sys3Reads; (b, Call, ep) \<in> Sys3AuthGraph; l \<in> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> b \<in> Sys3Reads
 9. \<And>ep b. \<lbrakk>ep \<in> subjectReads Sys3AuthGraph (OrdinaryLabel l); l \<in> {T3, UT3, EP3} \<Longrightarrow> ep \<in> Sys3Reads; (b, Receive, ep) \<in> Sys3AuthGraph; l \<in> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> b \<in> Sys3Reads
 10. \<And>t' t. \<lbrakk>t' \<in> subjectReads Sys3AuthGraph (OrdinaryLabel l); l \<in> {T3, UT3, EP3} \<Longrightarrow> t' \<in> Sys3Reads; (t, Reply, t') \<in> Sys3AuthGraph; l \<in> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> t \<in> Sys3Reads
A total of 13 subgoals... proof (prove)
goal:
No subgoals!