Mercurial Mercurial > hg > rc / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
finite_static.thy
changeset 1 dcde836219bc 
--- /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 \<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
\ No newline at end of file
rc