theory finite_staticimports Main rc_theory all_sobj_propbegincontext tainting_s_complete beginlemma 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+)donedefinition "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_defapply (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_defapply (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_defapply (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 autoapply (case_tac x, simp+)donelemma 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)qedlemma 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)qedlemma 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)qedlemma 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)qedlemma 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)qedlemma 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)qedlemma 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)qeddefinition "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)qeddefinition "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)qeddefinition "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)qeddefinition "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)qeddefinition "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)qedlemma 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_validby (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 autolemma 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 autoqedlemma 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)doneendend