diff -r b992684e9ff6 -r dcde836219bc os_rc.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/os_rc.thy	Fri Apr 12 10:43:11 2013 +0100
@@ -0,0 +1,376 @@
+theory os_rc 
+imports Main rc_theory 
+begin
+
+(****** below context is for lemmas of OS and RC ******)
+context rc_basic begin
+
+inductive_cases vs_step': "valid (e # \<tau>)" 
+
+lemma valid_cons:
+  "valid (e # \<tau>) \<Longrightarrow> valid \<tau>"
+by (drule vs_step', auto)
+
+lemma valid_os: 
+  "valid (e # \<tau>) \<Longrightarrow> os_grant \<tau> e"
+by (drule vs_step', auto)
+
+lemma valid_rc:
+  "valid (e # \<tau>) \<Longrightarrow> rc_grant \<tau> e"
+by (drule vs_step', auto)
+
+lemma vs_history:
+  "\<lbrakk>s \<preceq> s'; valid s'\<rbrakk> \<Longrightarrow> valid s"
+apply (induct s', simp add:no_junior_def)
+apply (case_tac "s = a # s'", simp)
+apply (drule no_junior_noteq, simp)
+by (drule valid_cons)
+
+lemma parent_file_in_current: 
+  "\<lbrakk>parent f = Some pf; f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> pf \<in> current_files s"
+apply (induct s)
+apply (simp add:parent_file_in_init)
+apply (frule valid_cons, frule valid_rc, frule valid_os)
+apply (case_tac a, auto split:option.splits)
+apply (case_tac f, simp+)
+done
+
+lemma parent_file_in_current': 
+  "\<lbrakk>fn # pf \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> pf \<in> current_files s"
+by (auto intro!:parent_file_in_current[where pf = pf])
+
+lemma parent_file_in_init': 
+  "fn # pf \<in> init_files \<Longrightarrow> pf \<in> init_files"
+by (auto intro!:parent_file_in_init[where pf = pf])
+
+lemma ancient_file_in_current:
+  "\<lbrakk>f \<in> current_files s; valid s; af \<preceq> f\<rbrakk> \<Longrightarrow> af \<in> current_files s"
+apply (induct f)
+apply (simp add:no_junior_def)
+apply (case_tac "af = a # f", simp)
+apply (drule no_junior_noteq, simp)
+apply (drule parent_file_in_current', simp+)
+done
+
+lemma cannot_del_root:
+  "\<lbrakk>valid (DeleteFile p [] # s); f \<noteq> []; f \<in> current_files s\<rbrakk> \<Longrightarrow> False"
+apply (frule valid_cons, frule valid_os)
+apply (case_tac f rule:rev_cases, simp)
+apply (drule_tac af = "[y]" in ancient_file_in_current, simp+)
+done
+
+lemma init_file_initialrole_imp_some: "\<exists> r. init_file_initialrole f = Some r"
+by (case_tac f, auto split:option.splits)
+
+lemma file_has_initialrole: "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> (\<exists> r. initialrole s f = Some r)"
+apply (induct s arbitrary:f) 
+apply (simp, rule init_file_initialrole_imp_some)
+apply (frule valid_cons, frule valid_os, case_tac a)
+apply (auto split:if_splits option.splits)
+done
+
+lemma file_has_initialrole':
+  "\<lbrakk>initialrole s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"
+by (rule notI, auto dest:file_has_initialrole)
+
+lemma file_has_effinitialrole: 
+  "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> \<exists> r. effinitialrole s f = Some r"
+apply (induct f)
+apply (auto simp:effinitialrole_def dest:file_has_initialrole parent_file_in_current')
+done
+
+lemma file_has_effinitialrole':
+  "\<lbrakk>effinitialrole s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"
+by (rule notI, auto dest:file_has_effinitialrole)
+
+lemma init_file_forcedrole_imp_some: "\<exists> r. init_file_forcedrole f = Some r"
+by (case_tac f, auto split:option.splits)
+
+lemma file_has_forcedrole: "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> (\<exists> r. forcedrole s f = Some r)"
+apply (induct s arbitrary:f) 
+apply (simp add:init_file_forcedrole_imp_some)
+apply (frule valid_cons, frule valid_os, case_tac a, auto)
+done
+
+lemma file_has_forcedrole':
+  "\<lbrakk>forcedrole s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"
+by (rule notI, auto dest:file_has_forcedrole)
+
+lemma file_has_effforcedrole: 
+  "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> \<exists> r. effforcedrole s f = Some r"
+apply (induct f)
+apply (auto simp:effforcedrole_def dest:file_has_forcedrole parent_file_in_current')
+done
+
+lemma file_has_effforcedrole':
+  "\<lbrakk>effforcedrole s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"
+by (rule notI, auto dest:file_has_effforcedrole)
+
+lemma current_proc_has_forcedrole:
+  "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> r. proc_forcedrole s p = Some r"
+apply (induct s arbitrary:p) using init_proc_has_frole
+apply (simp add:bidirect_in_init_def)
+apply (frule valid_cons, frule valid_os, case_tac a)
+apply (auto split:if_splits option.splits intro:file_has_effforcedrole)
+done
+
+lemma current_proc_has_forcedrole':
+  "\<lbrakk>proc_forcedrole s p = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s"
+by (rule notI, auto dest:current_proc_has_forcedrole)
+
+lemma current_proc_has_owner: "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> u. owner s p = Some u"
+apply (induct s arbitrary:p) using init_proc_has_owner
+apply (simp add:bidirect_in_init_def)
+apply (frule valid_cons, frule valid_os, case_tac a, auto)
+done
+
+lemma current_proc_has_owner':
+  "\<lbrakk>owner s p = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s"
+by (rule notI, auto dest:current_proc_has_owner)
+
+(*
+lemma effinitial_normal_intro: 
+  "\<lbrakk>f \<in> current_files \<tau>; valid \<tau>; effinitialrole \<tau> f \<noteq> Some UseForcedRole\<rbrakk> \<Longrightarrow> \<exists>nr. effinitialrole \<tau> f = Some (NormalRole nr)"
+apply (drule file_has_effinitialrole, simp)
+apply (erule exE, frule effinitialrole_valid, simp)
+done
+
+lemma effforced_normal_intro: 
+  "\<lbrakk>f \<in> current_files \<tau>; valid \<tau>; effforcedrole \<tau> f \<noteq> Some InheritUserRole; effforcedrole \<tau> f \<noteq> Some InheritProcessRole; effforcedrole \<tau> f \<noteq> Some InheritUpMixed\<rbrakk> 
+  \<Longrightarrow> \<exists>nr. effforcedrole \<tau> f = Some (NormalRole nr)"
+apply (drule file_has_effforcedrole, simp)
+apply (erule exE, frule effforcedrole_valid, simp)
+done
+*)
+
+lemma owner_in_users: "\<lbrakk>owner s p = Some u; valid s\<rbrakk> \<Longrightarrow> u \<in> init_users"
+apply (induct s arbitrary:p) defer
+apply (frule valid_cons, frule valid_os, case_tac a)
+apply (auto split:if_splits option.splits intro!:init_owner_valid)
+done
+
+lemma user_has_normalrole: 
+  "u \<in> init_users \<Longrightarrow> \<exists> nr. defrole u = Some nr" using init_user_has_role
+by (auto simp:bidirect_in_init_def)
+
+lemma user_has_normalrole':
+  "defrole u = None \<Longrightarrow> u \<notin> init_users"
+by (rule notI, auto dest:user_has_normalrole)
+
+lemma current_proc_has_role: 
+  "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> nr. currentrole s p = Some nr"
+apply (induct s arbitrary:p) using init_proc_has_role
+apply (simp add:bidirect_in_init_def)
+apply (frule valid_cons, frule valid_os, case_tac a)
+apply (auto simp:map_comp_def split:if_splits option.splits t_role.splits
+           dest!:current_proc_has_owner' user_has_normalrole' current_proc_has_forcedrole'
+                 file_has_forcedrole' file_has_effforcedrole' 
+                 file_has_initialrole' file_has_effinitialrole'
+           intro:user_has_normalrole
+            dest:owner_in_users effinitialrole_valid effforcedrole_valid proc_forcedrole_valid)
+done
+
+lemma current_file_has_type: 
+  "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_file s f = Some t"
+apply (induct s)
+apply (simp split:option.splits)
+apply (frule valid_cons, frule valid_os, case_tac a)
+apply (auto split:option.splits intro:current_proc_has_role)
+done
+
+lemma init_file_has_etype: "f \<in> init_files \<Longrightarrow> \<exists> nt. etype_aux init_file_type_aux f = Some nt"
+apply (induct f) defer
+apply (frule parent_file_in_init') 
+apply (auto split:option.splits t_rc_file_type.splits)
+done
+
+lemma current_file_has_etype[rule_format]:
+  "f \<in> current_files s \<Longrightarrow> valid s \<longrightarrow> (\<exists> nt. etype_of_file s f = Some nt)"
+apply (induct f)
+apply (auto simp:etype_of_file_def dest:current_file_has_type parent_file_in_current'
+           split:option.splits t_rc_file_type.splits)
+done
+
+lemma current_file_has_etype':
+  "\<lbrakk>etype_of_file s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"
+by (rule notI, auto dest:current_file_has_etype)
+
+(*** etype_of_file simpset ***)
+
+lemma etype_aux_prop:
+  "\<forall> x. x \<preceq> f \<longrightarrow> func' x = func x \<Longrightarrow> etype_aux func f = etype_aux func' f"
+apply (induct f)
+by (auto split:t_rc_file_type.splits option.splits)
+
+lemma etype_aux_prop1:
+  "func' = func ((a#f) := b) \<Longrightarrow> etype_aux func f = etype_aux func' f"
+by (rule etype_aux_prop, auto simp:no_junior_def)
+
+lemma etype_aux_prop1':
+  "etype_aux func f = x \<Longrightarrow> etype_aux (func ((a#f) := b)) f = x"
+apply (subgoal_tac "etype_aux func f = etype_aux (func ((a#f) := b)) f")
+apply (simp, rule etype_aux_prop1, simp)
+done
+
+lemma etype_aux_prop2:
+  "\<lbrakk>f \<in> current_files s; f' \<notin> current_files s; valid s\<rbrakk> \<Longrightarrow>
+  etype_aux (func (f' := b)) f = etype_aux func f"
+apply (rule etype_aux_prop)
+by (auto dest:ancient_file_in_current)
+
+lemma etype_aux_prop3:
+  "parent f = Some pf 
+   \<Longrightarrow> etype_aux (func (f := Some InheritParent_file_type)) f = etype_aux func pf"
+apply (case_tac f, simp+)
+by (rule etype_aux_prop, simp add:no_junior_def)
+
+lemma etype_aux_prop4:
+  "etype_aux (func (f := Some (NormalFile_type t))) f = Some t"
+by (case_tac f, auto)
+
+lemma etype_of_file_delete:
+  "\<lbrakk>valid (DeleteFile p f # s); f' \<in> current_files s\<rbrakk>
+   \<Longrightarrow> etype_of_file (DeleteFile p f # s) f' = etype_of_file s f'"
+apply (frule valid_cons, frule valid_os)
+apply (simp add:etype_of_file_def)
+done
+
+lemma current_proc_has_type: 
+  "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> nt. type_of_process s p = Some nt"
+apply (induct s arbitrary:p) using init_proc_has_type
+apply (simp add:bidirect_in_init_def)
+
+apply (frule valid_cons, frule valid_os, case_tac a)
+
+apply (subgoal_tac "nat1 \<in> current_procs (a # s)") prefer 2 apply simp
+apply (drule_tac p = nat1 in current_proc_has_role, simp, erule exE)
+
+apply (auto simp:pct_def pot_def pet_def dest:current_proc_has_role 
+           split:option.splits t_rc_proc_type.splits 
+           dest!:default_process_create_type_valid default_process_chown_type_valid 
+                 default_process_execute_type_valid)
+done
+
+lemma current_ipc_has_type: 
+  "\<lbrakk>i \<in> current_ipcs s; valid s\<rbrakk> \<Longrightarrow> \<exists> nt. type_of_ipc s i = Some nt"
+apply (induct s) using init_ipc_has_type
+apply (simp add:bidirect_in_init_def)
+
+apply (frule valid_cons, frule valid_os, case_tac a)
+apply (auto dest:current_proc_has_role)
+done
+
+(*** finite current_*  ***)
+
+lemma finite_cf: "finite (current_files s)"
+apply (induct s) defer apply (case_tac a)
+using init_finite by auto
+
+lemma finite_cp: "finite (current_procs s)"
+apply (induct s) defer apply (case_tac a)
+using init_finite by auto
+
+lemma finite_ci: "finite (current_ipcs s)"
+apply (induct s) defer apply (case_tac a)
+using init_finite by auto
+
+(*** properties of new-proc new-ipc ... ***)
+
+lemma nn_notin_aux: "finite s \<Longrightarrow> \<forall> a \<in> s. Max s \<ge> a "
+apply (erule finite.induct, simp)
+apply (rule ballI)
+apply (case_tac "aa = a", simp+)
+done
+
+lemma nn_notin: "finite s \<Longrightarrow> next_nat s \<notin> s"
+apply (drule nn_notin_aux)
+apply (simp add:next_nat_def)
+by (auto)
+
+lemma np_notin_curp: "new_proc \<tau> \<notin> current_procs \<tau>" using finite_cp
+by (simp add:new_proc_def nn_notin)
+
+lemma np_notin_curp': "new_proc \<tau> \<in> current_procs \<tau> \<Longrightarrow> False"
+by (simp add:np_notin_curp)
+
+lemma ni_notin_curi: "new_ipc \<tau> \<notin> current_ipcs \<tau>" using finite_ci
+by (simp add:new_ipc_def nn_notin)
+
+lemma ni_notin_curi': "new_ipc \<tau> \<in> current_ipcs \<tau> \<Longrightarrow> False"
+by (simp add:ni_notin_curi)
+
+end
+
+context tainting_s_complete begin
+
+lemma init_notin_curf_deleted:
+  "\<lbrakk>f \<notin> current_files s; f \<in> init_files\<rbrakk> \<Longrightarrow> deleted (File f) s"
+by (induct s, simp, case_tac a, auto)
+
+lemma init_notin_curi_deleted:
+  "\<lbrakk>i \<notin> current_ipcs s; i \<in> init_ipcs\<rbrakk> \<Longrightarrow> deleted (IPC i) s"
+by (induct s, simp, case_tac a, auto)
+
+lemma init_notin_curp_deleted:
+  "\<lbrakk>p \<notin> current_procs s; p \<in> init_processes\<rbrakk> \<Longrightarrow> deleted (Proc p) s"
+by (induct s, simp, case_tac a, auto)
+  
+lemma ni_init_deled: "new_ipc s \<in> init_ipcs \<Longrightarrow> deleted (IPC (new_ipc s)) s"
+using ni_notin_curi[where \<tau> = s]
+by (drule_tac init_notin_curi_deleted, simp+)
+
+lemma np_init_deled: "new_proc s \<in> init_processes \<Longrightarrow> deleted (Proc (new_proc s)) s"
+using np_notin_curp[where \<tau> = s]
+by (drule_tac init_notin_curp_deleted, simp+)
+
+lemma source_dir_in_init: "source_dir s f = Some sd \<Longrightarrow> sd \<in> init_files"
+by (induct f, auto split:if_splits)
+
+lemma source_proc_in_init:
+  "\<lbrakk>source_proc s p = Some p'; p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> p' \<in> init_processes"
+apply (induct s arbitrary:p, simp split:if_splits)
+apply (frule valid_os, frule valid_cons, case_tac a)
+by (auto simp:np_notin_curp split:if_splits)
+
+end
+
+context tainting_s_sound begin
+
+lemma len_fname_all: "length (fname_all_a len) = len"
+by (induct len, auto simp:fname_all_a.simps)
+
+lemma ncf_notin_curf: "new_childf f s \<notin> current_files s"
+apply (simp add:new_childf_def next_fname_def all_fname_under_dir_def)
+apply (rule notI)
+apply (subgoal_tac "(CHR ''a'' # fname_all_a (Max (fname_length_set {fn. fn # f \<in> current_files s}))) \<in> {fn. fn # f \<in> current_files s}")
+defer apply simp
+apply (subgoal_tac "length (CHR ''a'' # fname_all_a (Max (fname_length_set {fn. fn # f \<in> current_files s}))) \<in> fname_length_set {fn. fn # f \<in> current_files s}")
+defer apply (auto simp:fname_length_set_def image_def)[1]
+apply (subgoal_tac "finite (fname_length_set {fn. fn # f \<in> current_files s})")  
+defer
+apply (simp add:fname_length_set_def) 
+apply (rule finite_imageI) using finite_cf[where s = s]
+apply (drule_tac h = "\<lambda> f'. case f' of [] \<Rightarrow> '''' | fn # pf' \<Rightarrow> if (pf' = f) then fn else ''''" in finite_imageI)
+apply (rule_tac B = "(list_case [] (\<lambda>fn pf'. if pf' = f then fn else []) ` current_files s)" in finite_subset)
+unfolding image_def
+apply(auto)[1]
+apply (rule_tac x = "x # f" in bexI, simp+)
+apply (drule_tac s = "(fname_length_set {fn. fn # f \<in> current_files s})" in nn_notin_aux)
+apply (erule_tac x = "length (CHR ''a'' # fname_all_a (Max (fname_length_set {fn. fn # f \<in> current_files s})))" in ballE)
+apply (simp add:len_fname_all, simp)
+done
+
+lemma ncf_parent: "parent (new_childf f \<tau>) = Some f"
+by (simp add:new_childf_def)
+
+lemma clone_event_no_limit: 
+  "\<lbrakk>p \<in> current_procs \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> valid (Clone p (new_proc \<tau>) # \<tau>)"
+apply (rule vs_step)
+apply (auto intro:clone_no_limit split:option.splits
+            dest:current_proc_has_role current_proc_has_type)
+done 
+
+
+end
+
+end
\ No newline at end of file