theory PolicyExample

lemma "policyFlows example_auth_graph2 = example_policy2" apply(rule equalityI) apply(rule subsetI) apply(clarsimp simp: example_policy2_def) apply(erule policyFlows.cases) apply(case_tac l; auto simp: partsSubjectAffects2) apply assumption apply(rule subsetI) apply(clarsimp simp: example_policy2_def) apply(elim disjE) apply(fastforce simp: partsSubjectAffects2 intro: policy_affects)+ apply(fastforce intro: policy_scheduler) apply(fastforce intro: policyFlows_refl refl_onD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. policyFlows example_auth_graph2 = example_policy2 proof (prove)
goal (2 subgoals):
 1. policyFlows example_auth_graph2 \<subseteq> example_policy2
 2. example_policy2 \<subseteq> policyFlows example_auth_graph2 proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> policyFlows example_auth_graph2 \<Longrightarrow> x \<in> example_policy2
 2. example_policy2 \<subseteq> policyFlows example_auth_graph2 proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> policyFlows example_auth_graph2; a = Partition High \<longrightarrow> b \<noteq> Partition NTFN; a = Partition NTFN \<longrightarrow> b \<noteq> Partition High; a = Partition SharedPage \<longrightarrow> b \<noteq> Partition High; a = Partition SharedPage \<longrightarrow> b \<noteq> Partition Low; a = Partition SharedPage \<longrightarrow> b \<noteq> Partition NTFN; a = Partition Low \<longrightarrow> b \<noteq> Partition NTFN; a = Partition Low \<longrightarrow> b \<noteq> Partition SharedPage; a = Partition Low \<longrightarrow> b \<noteq> Partition High; a \<noteq> b\<rbrakk> \<Longrightarrow> a = PSched
 2. example_policy2 \<subseteq> policyFlows example_auth_graph2 proof (prove)
goal (3 subgoals):
 1. \<And>a b d l. \<lbrakk>a = Partition High \<longrightarrow> b \<noteq> Partition NTFN; a = Partition NTFN \<longrightarrow> b \<noteq> Partition High; a = Partition SharedPage \<longrightarrow> b \<noteq> Partition High; a = Partition SharedPage \<longrightarrow> b \<noteq> Partition Low; a = Partition SharedPage \<longrightarrow> b \<noteq> Partition NTFN; a = Partition Low \<longrightarrow> b \<noteq> Partition NTFN; a = Partition Low \<longrightarrow> b \<noteq> Partition SharedPage; a = Partition Low \<longrightarrow> b \<noteq> Partition High; a \<noteq> b; a = Partition l; b = d; d \<in> partsSubjectAffects example_auth_graph2 l\<rbrakk> \<Longrightarrow> a = PSched
 2. \<And>a b d. \<lbrakk>a = Partition High \<longrightarrow> b \<noteq> Partition NTFN; a = Partition NTFN \<longrightarrow> b \<noteq> Partition High; a = Partition SharedPage \<longrightarrow> b \<noteq> Partition High; a = Partition SharedPage \<longrightarrow> b \<noteq> Partition Low; a = Partition SharedPage \<longrightarrow> b \<noteq> Partition NTFN; a = Partition Low \<longrightarrow> b \<noteq> Partition NTFN; a = Partition Low \<longrightarrow> b \<noteq> Partition SharedPage; a = Partition Low \<longrightarrow> b \<noteq> Partition High; a \<noteq> b; a = PSched; b = d\<rbrakk> \<Longrightarrow> a = PSched
 3. example_policy2 \<subseteq> policyFlows example_auth_graph2 proof (prove)
goal (2 subgoals):
 1. \<And>a b d. \<lbrakk>a = Partition High \<longrightarrow> b \<noteq> Partition NTFN; a = Partition NTFN \<longrightarrow> b \<noteq> Partition High; a = Partition SharedPage \<longrightarrow> b \<noteq> Partition High; a = Partition SharedPage \<longrightarrow> b \<noteq> Partition Low; a = Partition SharedPage \<longrightarrow> b \<noteq> Partition NTFN; a = Partition Low \<longrightarrow> b \<noteq> Partition NTFN; a = Partition Low \<longrightarrow> b \<noteq> Partition SharedPage; a = Partition Low \<longrightarrow> b \<noteq> Partition High; a \<noteq> b; a = PSched; b = d\<rbrakk> \<Longrightarrow> a = PSched
 2. example_policy2 \<subseteq> policyFlows example_auth_graph2 proof (prove)
goal (1 subgoal):
 1. example_policy2 \<subseteq> policyFlows example_auth_graph2 proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> example_policy2 \<Longrightarrow> x \<in> policyFlows example_auth_graph2 proof (prove)
goal (1 subgoal):
 1. \<And>a b. a = Partition High \<and> b = Partition NTFN \<or> a = Partition NTFN \<and> b = Partition High \<or> a = Partition SharedPage \<and> b = Partition High \<or> a = Partition SharedPage \<and> b = Partition Low \<or> a = Partition SharedPage \<and> b = Partition NTFN \<or> a = Partition Low \<and> b = Partition NTFN \<or> a = Partition Low \<and> b = Partition SharedPage \<or> a = Partition Low \<and> b = Partition High \<or> a = PSched \<or> a = b \<Longrightarrow> (a, b) \<in> policyFlows example_auth_graph2 proof (prove)
goal (10 subgoals):
 1. \<And>a b. a = Partition High \<and> b = Partition NTFN \<Longrightarrow> (a, b) \<in> policyFlows example_auth_graph2
 2. \<And>a b. a = Partition NTFN \<and> b = Partition High \<Longrightarrow> (a, b) \<in> policyFlows example_auth_graph2
 3. \<And>a b. a = Partition SharedPage \<and> b = Partition High \<Longrightarrow> (a, b) \<in> policyFlows example_auth_graph2
 4. \<And>a b. a = Partition SharedPage \<and> b = Partition Low \<Longrightarrow> (a, b) \<in> policyFlows example_auth_graph2
 5. \<And>a b. a = Partition SharedPage \<and> b = Partition NTFN \<Longrightarrow> (a, b) \<in> policyFlows example_auth_graph2
 6. \<And>a b. a = Partition Low \<and> b = Partition NTFN \<Longrightarrow> (a, b) \<in> policyFlows example_auth_graph2
 7. \<And>a b. a = Partition Low \<and> b = Partition SharedPage \<Longrightarrow> (a, b) \<in> policyFlows example_auth_graph2
 8. \<And>a b. a = Partition Low \<and> b = Partition High \<Longrightarrow> (a, b) \<in> policyFlows example_auth_graph2
 9. \<And>a b. a = PSched \<Longrightarrow> (a, b) \<in> policyFlows example_auth_graph2
 10. \<And>a b. a = b \<Longrightarrow> (a, b) \<in> policyFlows example_auth_graph2 proof (prove)
goal (2 subgoals):
 1. \<And>a b. a = PSched \<Longrightarrow> (a, b) \<in> policyFlows example_auth_graph2
 2. \<And>a b. a = b \<Longrightarrow> (a, b) \<in> policyFlows example_auth_graph2 proof (prove)
goal (1 subgoal):
 1. \<And>a b. a = b \<Longrightarrow> (a, b) \<in> policyFlows example_auth_graph2 proof (prove)
goal:
No subgoals!