theory ExampleSystemPolicyFlows

lemma Sys3_policyFlows_correct_bw : "(a,b) \<in> Sys3PolicyFlows \<Longrightarrow> (a,b) \<in> policyFlows Sys3AuthGraph" apply (simp add:Sys3PolicyFlows_def) 
  (* All UT3/T3 cases *)
   apply (erule disjE, simp, rule policy_affects, simp add: partsSubjectAffects_def label_can_affect_partition_def, rule imageI, simp add: Sys3Affects_correct Sys3Reads_correct Sys3Affects_def Sys3Reads_def, blast)+ 
  (* All EP3 cases *)
   apply (erule disjE,simp, rule policy_affects, simp add: partsSubjectAffects_def label_can_affect_partition_def, rule imageI, simp add: Sys3EP3Affects_correct Sys3Reads_correct Sys3Reads_def Sys3EP3Affects_def)+ 
   (* IRQ3 case *)
    apply (rule_tac x = "OrdinaryLabel (IRQ3)" in exI) apply (rule conjI) apply (rule affects_lrefl) apply (rule reads_lrefl) 
  (* All PSched cases *)
   apply (erule disjE, simp add: PSched_flows_to_all)+ apply (simp add: PSched_flows_to_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> Sys3PolicyFlows \<Longrightarrow> (a, b) \<in> policyFlows Sys3AuthGraph proof (prove)
goal (1 subgoal):
 1. a = Partition UT3 \<and> b = Partition UT3 \<or> a = Partition UT3 \<and> b = Partition EP3 \<or> a = Partition UT3 \<and> b = Partition T3 \<or> a = Partition T3 \<and> b = Partition T3 \<or> a = Partition T3 \<and> b = Partition UT3 \<or> a = Partition T3 \<and> b = Partition EP3 \<or> a = Partition EP3 \<and> b = Partition UT3 \<or> a = Partition EP3 \<and> b = Partition EP3 \<or> a = Partition EP3 \<and> b = Partition T3 \<or> a = Partition IRQ3 \<and> b = Partition IRQ3 \<or> a = PSched \<and> b = Partition EP3 \<or> a = PSched \<and> b = Partition UT3 \<or> a = PSched \<and> b = Partition T3 \<or> a = PSched \<and> b = Partition IRQ3 \<or> a = PSched \<and> b = PSched \<Longrightarrow> (a, b) \<in> policyFlows Sys3AuthGraph proof (prove)
goal (1 subgoal):
 1. a = Partition UT3 \<and> b = Partition UT3 \<or> a = Partition UT3 \<and> b = Partition EP3 \<or> a = Partition UT3 \<and> b = Partition T3 \<or> a = Partition T3 \<and> b = Partition T3 \<or> a = Partition T3 \<and> b = Partition UT3 \<or> a = Partition T3 \<and> b = Partition EP3 \<or> a = Partition EP3 \<and> b = Partition UT3 \<or> a = Partition EP3 \<and> b = Partition EP3 \<or> a = Partition EP3 \<and> b = Partition T3 \<or> a = Partition IRQ3 \<and> b = Partition IRQ3 \<or> a = PSched \<and> b = Partition EP3 \<or> a = PSched \<and> b = Partition UT3 \<or> a = PSched \<and> b = Partition T3 \<or> a = PSched \<and> b = Partition IRQ3 \<or> a = PSched \<and> b = PSched \<Longrightarrow> (a, b) \<in> policyFlows Sys3AuthGraph proof (prove)
goal (1 subgoal):
 1. a = Partition EP3 \<and> b = Partition UT3 \<or> a = Partition EP3 \<and> b = Partition EP3 \<or> a = Partition EP3 \<and> b = Partition T3 \<or> a = Partition IRQ3 \<and> b = Partition IRQ3 \<or> a = PSched \<and> b = Partition EP3 \<or> a = PSched \<and> b = Partition UT3 \<or> a = PSched \<and> b = Partition T3 \<or> a = PSched \<and> b = Partition IRQ3 \<or> a = PSched \<and> b = PSched \<Longrightarrow> (a, b) \<in> policyFlows Sys3AuthGraph proof (prove)
goal (1 subgoal):
 1. a = Partition EP3 \<and> b = Partition UT3 \<or> a = Partition EP3 \<and> b = Partition EP3 \<or> a = Partition EP3 \<and> b = Partition T3 \<or> a = Partition IRQ3 \<and> b = Partition IRQ3 \<or> a = PSched \<and> b = Partition EP3 \<or> a = PSched \<and> b = Partition UT3 \<or> a = PSched \<and> b = Partition T3 \<or> a = PSched \<and> b = Partition IRQ3 \<or> a = PSched \<and> b = PSched \<Longrightarrow> (a, b) \<in> policyFlows Sys3AuthGraph proof (prove)
goal (2 subgoals):
 1. a = Partition IRQ3 \<and> b = Partition IRQ3 \<Longrightarrow> \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel IRQ3) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel IRQ3)
 2. a = PSched \<and> b = Partition EP3 \<or> a = PSched \<and> b = Partition UT3 \<or> a = PSched \<and> b = Partition T3 \<or> a = PSched \<and> b = Partition IRQ3 \<or> a = PSched \<and> b = PSched \<Longrightarrow> (a, b) \<in> policyFlows Sys3AuthGraph proof (prove)
goal (2 subgoals):
 1. a = Partition IRQ3 \<and> b = Partition IRQ3 \<Longrightarrow> \<exists>d. d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel IRQ3) \<and> d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel IRQ3)
 2. a = PSched \<and> b = Partition EP3 \<or> a = PSched \<and> b = Partition UT3 \<or> a = PSched \<and> b = Partition T3 \<or> a = PSched \<and> b = Partition IRQ3 \<or> a = PSched \<and> b = PSched \<Longrightarrow> (a, b) \<in> policyFlows Sys3AuthGraph proof (prove)
goal (2 subgoals):
 1. a = Partition IRQ3 \<and> b = Partition IRQ3 \<Longrightarrow> OrdinaryLabel IRQ3 \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel IRQ3) \<and> OrdinaryLabel IRQ3 \<in> subjectReads Sys3AuthGraph (OrdinaryLabel IRQ3)
 2. a = PSched \<and> b = Partition EP3 \<or> a = PSched \<and> b = Partition UT3 \<or> a = PSched \<and> b = Partition T3 \<or> a = PSched \<and> b = Partition IRQ3 \<or> a = PSched \<and> b = PSched \<Longrightarrow> (a, b) \<in> policyFlows Sys3AuthGraph proof (prove)
goal (3 subgoals):
 1. a = Partition IRQ3 \<and> b = Partition IRQ3 \<Longrightarrow> OrdinaryLabel IRQ3 \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel IRQ3)
 2. a = Partition IRQ3 \<and> b = Partition IRQ3 \<Longrightarrow> OrdinaryLabel IRQ3 \<in> subjectReads Sys3AuthGraph (OrdinaryLabel IRQ3)
 3. a = PSched \<and> b = Partition EP3 \<or> a = PSched \<and> b = Partition UT3 \<or> a = PSched \<and> b = Partition T3 \<or> a = PSched \<and> b = Partition IRQ3 \<or> a = PSched \<and> b = PSched \<Longrightarrow> (a, b) \<in> policyFlows Sys3AuthGraph proof (prove)
goal (2 subgoals):
 1. a = Partition IRQ3 \<and> b = Partition IRQ3 \<Longrightarrow> OrdinaryLabel IRQ3 \<in> subjectReads Sys3AuthGraph (OrdinaryLabel IRQ3)
 2. a = PSched \<and> b = Partition EP3 \<or> a = PSched \<and> b = Partition UT3 \<or> a = PSched \<and> b = Partition T3 \<or> a = PSched \<and> b = Partition IRQ3 \<or> a = PSched \<and> b = PSched \<Longrightarrow> (a, b) \<in> policyFlows Sys3AuthGraph proof (prove)
goal (1 subgoal):
 1. a = PSched \<and> b = Partition EP3 \<or> a = PSched \<and> b = Partition UT3 \<or> a = PSched \<and> b = Partition T3 \<or> a = PSched \<and> b = Partition IRQ3 \<or> a = PSched \<and> b = PSched \<Longrightarrow> (a, b) \<in> policyFlows Sys3AuthGraph proof (prove)
goal (1 subgoal):
 1. a = PSched \<and> b = Partition EP3 \<or> a = PSched \<and> b = Partition UT3 \<or> a = PSched \<and> b = Partition T3 \<or> a = PSched \<and> b = Partition IRQ3 \<or> a = PSched \<and> b = PSched \<Longrightarrow> (a, b) \<in> policyFlows Sys3AuthGraph proof (prove)
goal (1 subgoal):
 1. a = PSched \<and> b = PSched \<Longrightarrow> (a, b) \<in> policyFlows Sys3AuthGraph proof (prove)
goal:
No subgoals!