theory PolicySystemSAC

lemma SAC_policyFlows : "policyFlows SACAuthGraph = SACPolicyFlows" apply (rule subset_antisym) 
  (* forward *)
   apply (rule subsetI) apply clarify apply (erule policyFlows.cases) 
    (* subject case *)
     apply (clarsimp simp:SACPolicyFlows_def) apply (case_tac "d = Partition T") apply (case_tac l, auto simp:SAC_partsSubjectAffects_T SAC_partsSubjectAffects_exceptT)[1] apply (case_tac l, auto simp:SAC_partsSubjectAffects_T SAC_partsSubjectAffects_exceptT)[1] 
    (* scheduler case *)
     apply (simp add:SACPolicyFlows_def) 
  (* backward *)
   apply (rule subsetI) apply (clarsimp simp:SACPolicyFlows_def) apply (erule disjE) 
    (* scheduler flows to all *)
     apply (simp add:PSched_flows_to_all) 
    (* all subjects flow to all subjects *)
     apply (clarify, simp) apply (rule policy_affects) apply (case_tac l, case_tac[1-12] k, auto simp:SAC_partsSubjectAffects_T SAC_partsSubjectAffects_exceptT) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. policyFlows SACAuthGraph = SACPolicyFlows proof (prove)
goal (2 subgoals):
 1. policyFlows SACAuthGraph \<subseteq> SACPolicyFlows
 2. SACPolicyFlows \<subseteq> policyFlows SACAuthGraph proof (prove)
goal (2 subgoals):
 1. policyFlows SACAuthGraph \<subseteq> SACPolicyFlows
 2. SACPolicyFlows \<subseteq> policyFlows SACAuthGraph proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> policyFlows SACAuthGraph \<Longrightarrow> x \<in> SACPolicyFlows
 2. SACPolicyFlows \<subseteq> policyFlows SACAuthGraph proof (prove)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> policyFlows SACAuthGraph \<Longrightarrow> (a, b) \<in> SACPolicyFlows
 2. SACPolicyFlows \<subseteq> policyFlows SACAuthGraph proof (prove)
goal (3 subgoals):
 1. \<And>a b d l. \<lbrakk>a = Partition l; b = d; d \<in> partsSubjectAffects SACAuthGraph l\<rbrakk> \<Longrightarrow> (a, b) \<in> SACPolicyFlows
 2. \<And>a b d. \<lbrakk>a = PSched; b = d\<rbrakk> \<Longrightarrow> (a, b) \<in> SACPolicyFlows
 3. SACPolicyFlows \<subseteq> policyFlows SACAuthGraph proof (prove)
goal (3 subgoals):
 1. \<And>a b d l. \<lbrakk>a = Partition l; b = d; d \<in> partsSubjectAffects SACAuthGraph l\<rbrakk> \<Longrightarrow> (a, b) \<in> SACPolicyFlows
 2. \<And>a b d. \<lbrakk>a = PSched; b = d\<rbrakk> \<Longrightarrow> (a, b) \<in> SACPolicyFlows
 3. SACPolicyFlows \<subseteq> policyFlows SACAuthGraph proof (prove)
goal (3 subgoals):
 1. \<And>d l. d \<in> partsSubjectAffects SACAuthGraph l \<Longrightarrow> \<exists>k. d = Partition k \<and> (k = T \<longrightarrow> l = T)
 2. \<And>a b d. \<lbrakk>a = PSched; b = d\<rbrakk> \<Longrightarrow> (a, b) \<in> SACPolicyFlows
 3. SACPolicyFlows \<subseteq> policyFlows SACAuthGraph proof (prove)
goal (4 subgoals):
 1. \<And>d l. \<lbrakk>d \<in> partsSubjectAffects SACAuthGraph l; d = Partition T\<rbrakk> \<Longrightarrow> \<exists>k. d = Partition k \<and> (k = T \<longrightarrow> l = T)
 2. \<And>d l. \<lbrakk>d \<in> partsSubjectAffects SACAuthGraph l; d \<noteq> Partition T\<rbrakk> \<Longrightarrow> \<exists>k. d = Partition k \<and> (k = T \<longrightarrow> l = T)
 3. \<And>a b d. \<lbrakk>a = PSched; b = d\<rbrakk> \<Longrightarrow> (a, b) \<in> SACPolicyFlows
 4. SACPolicyFlows \<subseteq> policyFlows SACAuthGraph proof (prove)
goal (3 subgoals):
 1. \<And>d l. \<lbrakk>d \<in> partsSubjectAffects SACAuthGraph l; d \<noteq> Partition T\<rbrakk> \<Longrightarrow> \<exists>k. d = Partition k \<and> (k = T \<longrightarrow> l = T)
 2. \<And>a b d. \<lbrakk>a = PSched; b = d\<rbrakk> \<Longrightarrow> (a, b) \<in> SACPolicyFlows
 3. SACPolicyFlows \<subseteq> policyFlows SACAuthGraph proof (prove)
goal (2 subgoals):
 1. \<And>a b d. \<lbrakk>a = PSched; b = d\<rbrakk> \<Longrightarrow> (a, b) \<in> SACPolicyFlows
 2. SACPolicyFlows \<subseteq> policyFlows SACAuthGraph proof (prove)
goal (2 subgoals):
 1. \<And>a b d. \<lbrakk>a = PSched; b = d\<rbrakk> \<Longrightarrow> (a, b) \<in> SACPolicyFlows
 2. SACPolicyFlows \<subseteq> policyFlows SACAuthGraph proof (prove)
goal (1 subgoal):
 1. SACPolicyFlows \<subseteq> policyFlows SACAuthGraph proof (prove)
goal (1 subgoal):
 1. SACPolicyFlows \<subseteq> policyFlows SACAuthGraph proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> SACPolicyFlows \<Longrightarrow> x \<in> policyFlows SACAuthGraph proof (prove)
goal (1 subgoal):
 1. \<And>a b. a = PSched \<or> (\<exists>l. a = Partition l \<and> (\<exists>k. b = Partition k \<and> (k = T \<longrightarrow> l = T))) \<Longrightarrow> (a, b) \<in> policyFlows SACAuthGraph proof (prove)
goal (2 subgoals):
 1. \<And>a b. a = PSched \<Longrightarrow> (a, b) \<in> policyFlows SACAuthGraph
 2. \<And>a b. \<exists>l. a = Partition l \<and> (\<exists>k. b = Partition k \<and> (k = T \<longrightarrow> l = T)) \<Longrightarrow> (a, b) \<in> policyFlows SACAuthGraph proof (prove)
goal (2 subgoals):
 1. \<And>a b. a = PSched \<Longrightarrow> (a, b) \<in> policyFlows SACAuthGraph
 2. \<And>a b. \<exists>l. a = Partition l \<and> (\<exists>k. b = Partition k \<and> (k = T \<longrightarrow> l = T)) \<Longrightarrow> (a, b) \<in> policyFlows SACAuthGraph proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<exists>l. a = Partition l \<and> (\<exists>k. b = Partition k \<and> (k = T \<longrightarrow> l = T)) \<Longrightarrow> (a, b) \<in> policyFlows SACAuthGraph proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<exists>l. a = Partition l \<and> (\<exists>k. b = Partition k \<and> (k = T \<longrightarrow> l = T)) \<Longrightarrow> (a, b) \<in> policyFlows SACAuthGraph proof (prove)
goal (1 subgoal):
 1. \<And>l k. k = T \<longrightarrow> l = T \<Longrightarrow> (Partition l, Partition k) \<in> policyFlows SACAuthGraph proof (prove)
goal (1 subgoal):
 1. \<And>l k. k = T \<longrightarrow> l = T \<Longrightarrow> Partition k \<in> partsSubjectAffects SACAuthGraph l proof (prove)
goal:
No subgoals!