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

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 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 split:if_splits)

end

context tainting_s_sound begin

(*** 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)

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 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!:np_notin_curp'
            dest:current_proc_has_role current_proc_has_type)
done 


end

end