diff -r b992684e9ff6 -r dcde836219bc finite_static.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/finite_static.thy Fri Apr 12 10:43:11 2013 +0100 @@ -0,0 +1,270 @@ +theory finite_static +imports Main rc_theory all_sobj_prop +begin + +context tainting_s_complete begin + +lemma tainted_s_subset_all_sobjs: + "tainted_s \ 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 \ {Some p | p. p \ init_processes} \ {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 \ {Some f | f. f \ init_files} \ {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 \ {Some i | i. i \ init_processes} \ {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 \ UNIV}" using finite_t_client by auto + have p3: "finite {UpLoad c| c. c \ UNIV}" using finite_t_client by auto + have p4: "finite {CGI c| c. c \ UNIV}" using finite_t_client by auto + from p1 p2 p3 p4 + have p5: "finite ({WebServer} \ {WS c | c. c \ UNIV} \ {UpLoad c | c. c \ UNIV} \ {CGI c | c. c \ UNIV})" + by auto + have p6: "(UNIV :: t_normal_role set) = ({WebServer} \ {WS c | c. c \ UNIV} \ + {UpLoad c | c. c \ UNIV} \ {CGI c | c. c \ 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 \ 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} \ + {NormalRole r | r. r \ UNIV}" + apply (rule set_eqI, auto split:t_role.splits) + by (case_tac x, auto) + have p4: "finite ({InheritParentRole, UseForcedRole, InheritUpMixed, InheritUserRole, InheritProcessRole} \ + {NormalRole r | r. r \ 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 \ UNIV}" using finite_t_client by auto + have p2: "finite {CGI_P_file c | c. c \ UNIV}" using finite_t_client by auto + have p3: "finite {PrivateD_file c | c. c \ 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 \ UNIV} \ {CGI_P_file c | c. c \ UNIV} \ + {PrivateD_file c | c. c \ UNIV} \ {Executable_file, Root_file_type, WebServerLog_file})" + using p1 p2 p3 p4 by auto + have p6: "UNIV = ({WebData_file c | c. c \ UNIV} \ {CGI_P_file c | c. c \ UNIV} \ + {PrivateD_file c | c. c \ UNIV} \ {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 \ UNIV}" using finite_t_normal_file_type by auto + have p2: "finite ({InheritParent_file_type} \ {NormalFile_type t | t. t \ UNIV})" + using p1 by auto + have p3: "UNIV = ({InheritParent_file_type} \ {NormalFile_type t | t. t \ 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 \ UNIV}" using finite_t_client by auto + have p2: "finite ({CGI_P_proc c | c. c \ UNIV} \ {WebServer_proc})" using p1 by auto + have p3: "UNIV = ({CGI_P_proc c | c. c \ UNIV} \ {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 \ UNIV}" using finite_t_normal_proc_type by auto + have p2: "finite ({NormalProc_type t | t. t \ UNIV} \ {InheritParent_proc_type, UseNewRoleType})" + using p1 by auto + have p3: "UNIV = ({NormalProc_type t | t. t \ UNIV} \ {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 \ (UNIV ::t_normal_role set) \ (UNIV :: t_role set) \ (UNIV :: t_normal_proc_type set) \ init_users" + +lemma finite_all_sps: "finite all_sps" +proof- + have "finite ((UNIV :: t_normal_proc_type set) \ init_users)" + using finite_t_normal_proc_type init_finite + by (rule_tac finite_cartesian_product, auto) + hence "finite ((UNIV :: t_role set) \ (UNIV :: t_normal_proc_type set) \ init_users)" + using finite_t_role by (rule_tac finite_cartesian_product, auto) + hence "finite ((UNIV::t_normal_role set) \ (UNIV::t_role set) \ (UNIV::t_normal_proc_type set) \ 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 \ {SProc sp (Some p) | sp p. sp \ all_sps \ p \ init_processes} \ {SProc sp None | sp. sp \ all_sps}" + +lemma finite_all_SPs: "finite all_SPs" +proof- + have p1: "finite {SProc sp (Some p) | sp p. sp \ all_sps \ p \ init_processes}" + using finite_all_sps init_finite by auto + have p2: "finite {SProc sp None | sp. sp \ all_sps}" + using finite_all_sps by auto + have "finite ({SProc sp (Some p) | sp p. sp \ all_sps \ p \ init_processes} \ + {SProc sp None | sp. sp \ all_sps})" + using p1 p2 by auto + thus ?thesis by (simp only:all_SPs_def) +qed + +definition + "all_sfs \ (UNIV :: t_normal_file_type set) \ init_files" + +lemma finite_all_sfs: "finite all_sfs" +proof- + have "finite ((UNIV :: t_normal_file_type set) \ 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 \ {SFile sf (Some f) | sf f. sf \ all_sfs \ f \ init_files} \ {SFile sf None| sf. sf \ all_sfs}" + +lemma finite_all_SFs: "finite all_SFs" +proof- + have p1: "finite ({SFile sf (Some f) | sf f. sf \ all_sfs \ f \ init_files} \ + {SFile sf None| sf. sf \ all_sfs})" + using finite_all_sfs init_finite by auto + thus ?thesis by (simp only:all_SFs_def) +qed + +definition + "all_SIs \ {SIPC si (Some i)| si i. si \ UNIV \ i \ init_ipcs} \ {SIPC si None| si. si \ UNIV}" + +lemma finite_all_SIs: "finite all_SIs" +proof- + have "finite ({SIPC si (Some i)| si i. si \ UNIV \ i \ init_ipcs} \ {SIPC si None| si. si \ 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 \ all_sobjs \ \ sf srf. sobj = SFile sf (Some srf) \ srf \ init_files" +by (erule all_sobjs.induct, auto) + +lemma all_sobjs_srf_init: + "SFile sf (Some srf) \ all_sobjs \ srf \ init_files" +by (auto dest!:all_sobjs_srf_init') + +lemma all_sobjs_sd_init': + "sobj \ all_sobjs \ \ tf sd srf. sobj = SFile (tf, sd) srf \ sd \ init_files" +by (erule all_sobjs.induct, auto) + +lemma all_sobjs_sd_init: + "SFile (tf, sd) srf \ all_sobjs \ sd \ init_files" +by (auto dest!:all_sobjs_sd_init') + +lemma all_sobjs_sri_init': + "sobj \ all_sobjs \ \ si sri. sobj = SIPC si (Some sri) \ sri \ 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) \ all_sobjs \ sri \ init_ipcs" +by (auto dest!:all_sobjs_sri_init') + +lemma all_sobjs_sru_init'[rule_format]: + "sobj \ all_sobjs \ \ r fr pt u srp. sobj = SProc (r,fr,pt,u) srp \ u \ init_users" +using init_owner_valid +by (erule_tac all_sobjs.induct, auto) + +lemma all_sobjs_sru_init: + "SProc (r,fr,pt,u) srp \ all_sobjs \ u \ init_users" +by (auto dest!:all_sobjs_sru_init') + +lemma unknown_not_in_all_sobjs': + "sobj \ all_sobjs \ sobj \ Unknown" +by (erule_tac all_sobjs.induct, auto) + +lemma unknown_not_in_all_sobjs: + "Unknown \ all_sobjs \ False" +using unknown_not_in_all_sobjs' by auto + +lemma finite_all_sobjs: "finite all_sobjs" +proof- + have p1: "finite (all_SPs \ all_SFs \ all_SIs)" + using finite_all_SPs finite_all_SFs finite_all_SIs by auto + have p2: "all_sobjs \ (all_SPs \ all_SFs \ 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 \ all_SFs \ 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 \ No newline at end of file