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