theory finite_static

imports Main rc_theory all_sobj_prop

begin

context tainting_s_complete begin

lemma tainted_s_subset_all_sobjs:

  "tainted_s \<subseteq> all_sobjs"

apply (rule subsetI, erule tainted_s.induct)

apply (auto intro:all_sobjs.intros)

apply (drule seeds_in_init)

apply (subgoal_tac "exists [] obj")

apply (frule obj2sobj_nil_init)

apply (drule all_sobjs_I)

apply (rule vs_nil, simp) 

apply (case_tac obj, simp+)

done

definition 

  "init_proc_opt \<equiv> {Some p | p. p \<in> init_processes} \<union> {None}"

lemma finite_init_proc_opt:

  "finite init_proc_opt"

unfolding init_proc_opt_def

apply (simp add: finite_Un)

apply (rule finite_imageI)

by (simp add:init_finite)

definition 

  "init_file_opt \<equiv> {Some f | f. f \<in> init_files} \<union> {None}"

lemma finite_init_file_opt:

  "finite init_file_opt"

unfolding init_file_opt_def

apply (simp add: finite_Un)

apply (rule finite_imageI)

by (simp add:init_finite)

definition 

  "init_ipc_opt \<equiv> {Some i | i. i \<in> init_processes} \<union> {None}"

lemma finite_init_ipc_opt:

  "finite init_ipc_opt"

unfolding init_ipc_opt_def

apply (simp add: finite_Un)

apply (rule finite_imageI)

by (simp add:init_finite)

lemma finite_t_client:

  "finite (UNIV :: t_client set)"

apply (subgoal_tac "UNIV = {Client1, Client2}")

apply (metis (full_types) finite.emptyI finite_insert)

apply auto

apply (case_tac x, simp+)

done

lemma finite_t_normal_role:

  "finite (UNIV :: t_normal_role set)"

proof-

  have p1: "finite {WebServer}" by simp

  have p2: "finite {WS c | c. c \<in> UNIV}" using finite_t_client by auto

  have p3: "finite {UpLoad c| c. c \<in> UNIV}" using finite_t_client by auto

  have p4: "finite {CGI c| c. c \<in> UNIV}" using finite_t_client by auto

  from p1 p2 p3 p4

  have p5: "finite ({WebServer} \<union> {WS c | c. c \<in> UNIV} \<union> {UpLoad c | c. c \<in> UNIV} \<union> {CGI c | c. c \<in> UNIV})" 

    by auto

  have p6: "(UNIV :: t_normal_role set) = ({WebServer} \<union> {WS c | c. c \<in> UNIV} \<union> 

     {UpLoad c | c. c \<in> UNIV} \<union> {CGI c | c. c \<in> UNIV})"

    apply (rule set_eqI, auto split:t_normal_role.splits)

    by (case_tac x, auto)

  show ?thesis by (simp only:p6 p5)

qed

lemma finite_t_role: "finite (UNIV :: t_role set)"

proof-

  have p1: "finite {NormalRole r | r. r \<in> UNIV}" using finite_t_normal_role by auto

  have p2: "finite {InheritParentRole, UseForcedRole, InheritUpMixed, InheritUserRole, InheritProcessRole}"

    by auto

  have p3: "UNIV = {InheritParentRole, UseForcedRole, InheritUpMixed, InheritUserRole, InheritProcessRole} \<union> 

    {NormalRole r | r. r \<in> UNIV}"

    apply (rule set_eqI, auto split:t_role.splits)

    by (case_tac x, auto)

  have p4: "finite ({InheritParentRole, UseForcedRole, InheritUpMixed, InheritUserRole, InheritProcessRole} \<union> 

    {NormalRole r | r. r \<in> UNIV})" using p1 p2 by auto

  show ?thesis by (simp only:p3 p4)

qed

lemma finite_t_normal_file_type: "finite (UNIV :: t_normal_file_type set)"

proof-

  have p1: "finite {WebData_file c | c. c \<in> UNIV}" using finite_t_client by auto

  have p2: "finite {CGI_P_file c | c. c \<in> UNIV}"  using finite_t_client by auto

  have p3: "finite {PrivateD_file c | c. c \<in> UNIV}" using finite_t_client by auto

  have p4: "finite {Executable_file, Root_file_type, WebServerLog_file}" by auto

  have p5: "finite ({WebData_file c | c. c \<in> UNIV} \<union> {CGI_P_file c | c. c \<in> UNIV} \<union> 

    {PrivateD_file c | c. c \<in> UNIV} \<union> {Executable_file, Root_file_type, WebServerLog_file})"

    using p1 p2 p3 p4 by auto

  have p6: "UNIV = ({WebData_file c | c. c \<in> UNIV} \<union> {CGI_P_file c | c. c \<in> UNIV} \<union> 

    {PrivateD_file c | c. c \<in> UNIV} \<union> {Executable_file, Root_file_type, WebServerLog_file})"

    apply (rule set_eqI, auto split:t_normal_file_type.splits)

    by (case_tac x, auto)

  show ?thesis by (simp only:p6 p5)

qed

lemma finite_t_rc_file_type: "finite (UNIV :: t_rc_file_type set)"

proof-

  have p1: "finite {NormalFile_type t | t. t \<in> UNIV}" using finite_t_normal_file_type by auto

  have p2: "finite ({InheritParent_file_type} \<union> {NormalFile_type t | t. t \<in> UNIV})"

    using p1 by auto

  have p3: "UNIV = ({InheritParent_file_type} \<union> {NormalFile_type t | t. t \<in> UNIV})"

    apply (rule set_eqI, auto split:t_rc_file_type.splits)

    by (case_tac x, auto)

  show ?thesis by (simp only:p3 p2)

qed

lemma finite_t_normal_proc_type: "finite (UNIV :: t_normal_proc_type set)"

proof-

  have p1: "finite {CGI_P_proc c | c. c \<in> UNIV}" using finite_t_client by auto

  have p2: "finite ({CGI_P_proc c | c. c \<in> UNIV} \<union> {WebServer_proc})" using p1 by auto

  have p3: "UNIV = ({CGI_P_proc c | c. c \<in> UNIV} \<union> {WebServer_proc})"

    apply (rule set_eqI, auto split:t_normal_proc_type.splits)

    by (case_tac x, auto)

  show ?thesis by (simp only:p3 p2)

qed

lemma finite_t_rc_proc_type: "finite (UNIV :: t_rc_proc_type set)"

proof-

  have p1: "finite {NormalProc_type t | t. t \<in> UNIV}" using finite_t_normal_proc_type by auto

  have p2: "finite ({NormalProc_type t | t. t \<in> UNIV} \<union> {InheritParent_proc_type, UseNewRoleType})"

    using p1 by auto

  have p3: "UNIV = ({NormalProc_type t | t. t \<in> UNIV} \<union> {InheritParent_proc_type, UseNewRoleType})"

    apply (rule set_eqI, auto split:t_rc_proc_type.splits)

    by (case_tac x, auto)

  show ?thesis by (simp only:p3 p2)

qed

lemma finite_t_normal_ipc_type : "finite (UNIV :: t_normal_ipc_type set)"

proof-

  have p1: "finite {WebIPC}" by auto

  have p2: "UNIV = {WebIPC}" apply auto by (case_tac x, auto)

  show ?thesis by (simp only:p1 p2)

qed

definition 

  "all_sps \<equiv> (UNIV ::t_normal_role set) \<times> (UNIV :: t_role set) \<times> (UNIV :: t_normal_proc_type set) \<times> init_users"

lemma finite_all_sps: "finite all_sps"

proof-

  have "finite ((UNIV :: t_normal_proc_type set) \<times> init_users)"

    using finite_t_normal_proc_type init_finite

    by (rule_tac finite_cartesian_product, auto)

  hence "finite ((UNIV :: t_role set) \<times> (UNIV :: t_normal_proc_type set) \<times> init_users)"

    using finite_t_role by (rule_tac finite_cartesian_product, auto)

  hence "finite ((UNIV::t_normal_role set) \<times> (UNIV::t_role set) \<times> (UNIV::t_normal_proc_type set) \<times> init_users)" 

    using finite_t_normal_role by (rule_tac finite_cartesian_product, auto)

  thus ?thesis by (simp only:all_sps_def)

qed

definition

   "all_SPs \<equiv> {SProc sp (Some p) | sp p. sp \<in> all_sps \<and> p \<in> init_processes} \<union> {SProc sp None | sp. sp \<in> all_sps}"

lemma finite_all_SPs: "finite all_SPs"

proof-

  have p1: "finite {SProc sp (Some p) | sp p. sp \<in> all_sps \<and> p \<in> init_processes}"

    using finite_all_sps init_finite by auto

  have p2: "finite {SProc sp None | sp. sp \<in> all_sps}"

    using finite_all_sps by auto

  have "finite ({SProc sp (Some p) | sp p. sp \<in> all_sps \<and> p \<in> init_processes} \<union> 

    {SProc sp None | sp. sp \<in> all_sps})"

    using p1 p2 by auto

  thus ?thesis by (simp only:all_SPs_def)

qed

definition

  "all_sfs \<equiv> (UNIV :: t_normal_file_type set) \<times> init_files"

lemma finite_all_sfs: "finite all_sfs"

proof-

  have "finite ((UNIV :: t_normal_file_type set) \<times> init_files)"

    using finite_t_normal_file_type init_finite

    by (rule_tac finite_cartesian_product, auto)

  thus ?thesis by (simp add:all_sfs_def)

qed

definition 

  "all_SFs \<equiv> {SFile sf (Some f) | sf f. sf \<in> all_sfs \<and> f \<in> init_files} \<union> {SFile sf None| sf. sf \<in> all_sfs}"

lemma finite_all_SFs: "finite all_SFs"

proof-

  have p1: "finite ({SFile sf (Some f) | sf f. sf \<in> all_sfs \<and> f \<in> init_files} \<union>

    {SFile sf None| sf. sf \<in> all_sfs})"

    using finite_all_sfs init_finite by auto

  thus ?thesis by (simp only:all_SFs_def)

qed

definition 

  "all_SIs \<equiv> {SIPC si (Some i)| si i. si \<in> UNIV \<and> i \<in> init_ipcs} \<union> {SIPC si None| si. si \<in> UNIV}"

lemma finite_all_SIs: "finite all_SIs"

proof-

  have "finite ({SIPC si (Some i)| si i. si \<in> UNIV \<and> i \<in> init_ipcs} \<union> {SIPC si None| si. si \<in> UNIV})"

    using finite_t_normal_ipc_type init_finite by auto

  thus ?thesis by (simp only:all_SIs_def)

qed

lemma all_sobjs_srf_init':

  "sobj \<in> all_sobjs \<Longrightarrow> \<forall> sf srf. sobj = SFile sf (Some srf) \<longrightarrow> srf \<in> init_files"

by (erule all_sobjs.induct, auto) 

lemma all_sobjs_srf_init:

  "SFile sf (Some srf) \<in> all_sobjs \<Longrightarrow> srf \<in> init_files"

by (auto dest!:all_sobjs_srf_init')

lemma all_sobjs_sd_init':

  "sobj \<in> all_sobjs \<Longrightarrow> \<forall> tf sd srf. sobj = SFile (tf, sd) srf \<longrightarrow> sd \<in> init_files"

by (erule all_sobjs.induct, auto) 

lemma all_sobjs_sd_init:

  "SFile (tf, sd) srf \<in> all_sobjs \<Longrightarrow> sd \<in> init_files"

by (auto dest!:all_sobjs_sd_init')

lemma all_sobjs_sri_init':

  "sobj \<in> all_sobjs \<Longrightarrow> \<forall> si sri. sobj = SIPC si (Some sri) \<longrightarrow> sri \<in> init_ipcs"

apply (erule all_sobjs.induct, auto) using init_ipc_has_type 

by (simp add:bidirect_in_init_def)

lemma all_sobjs_sri_init:

  "SIPC si (Some sri) \<in> all_sobjs \<Longrightarrow> sri \<in> init_ipcs"

by (auto dest!:all_sobjs_sri_init')

lemma all_sobjs_sru_init'[rule_format]:

  "sobj \<in> all_sobjs \<Longrightarrow> \<forall> r fr pt u srp. sobj = SProc (r,fr,pt,u) srp \<longrightarrow> u \<in> init_users"

using init_owner_valid

by (erule_tac all_sobjs.induct, auto) 

lemma all_sobjs_sru_init:

  "SProc (r,fr,pt,u) srp \<in> all_sobjs \<Longrightarrow> u \<in> init_users"

by (auto dest!:all_sobjs_sru_init')

lemma unknown_not_in_all_sobjs':

  "sobj \<in> all_sobjs \<Longrightarrow> sobj \<noteq> Unknown"

by (erule_tac all_sobjs.induct, auto) 

lemma unknown_not_in_all_sobjs:

  "Unknown \<in> all_sobjs \<Longrightarrow> False"

using unknown_not_in_all_sobjs' by auto

lemma finite_all_sobjs: "finite all_sobjs"

proof-

  have p1: "finite (all_SPs \<union> all_SFs \<union> all_SIs)"

    using finite_all_SPs finite_all_SFs finite_all_SIs by auto

  have p2: "all_sobjs \<subseteq> (all_SPs \<union> all_SFs \<union> all_SIs)"

    apply (rule subsetI)

    using all_sobjs_sd_init all_sobjs_sri_init all_sobjs_srf_init all_sobjs_srp_init 

      all_sobjs_sru_init unknown_not_in_all_sobjs

    by (case_tac x, auto simp:all_SPs_def all_SFs_def all_SIs_def all_sps_def all_sfs_def)

  show ?thesis 

    apply (rule_tac B = "(all_SPs \<union> all_SFs \<union> all_SIs)" in finite_subset)

    using p1 p2 by auto

qed

lemma finite_tainted_s:

  "finite tainted_s"

apply (rule_tac B = "all_sobjs" in finite_subset)

apply (rule tainted_s_subset_all_sobjs)

apply (rule finite_all_sobjs)

done

end

end