Co2sobj_prop.thy
changeset 7 f27882976251
parent 6 8779d321cc2e
child 8 289a30c4cfb7
equal deleted inserted replaced
6:8779d321cc2e 7:f27882976251
     5 (*<*)
     5 (*<*)
     6 
     6 
     7 context tainting_s begin
     7 context tainting_s begin
     8 
     8 
     9 (************ simpset for cf2sfile ***************)
     9 (************ simpset for cf2sfile ***************)
    10 
       
    11 declare get_parentfs_ctxts.simps [simp del]
       
    12 
    10 
    13 lemma sroot_only:
    11 lemma sroot_only:
    14   "cf2sfile s [] = Some sroot"
    12   "cf2sfile s [] = Some sroot"
    15 by (simp add:cf2sfile_def)
    13 by (simp add:cf2sfile_def)
    16 
    14 
    69 apply (frule is_dir_in_current, frule is_dir_not_file)
    67 apply (frule is_dir_in_current, frule is_dir_not_file)
    70 apply (drule current_file_has_sfile, simp)
    68 apply (drule current_file_has_sfile, simp)
    71 apply (auto simp:cf2sfile_def split:if_splits option.splits)
    69 apply (auto simp:cf2sfile_def split:if_splits option.splits)
    72 done
    70 done
    73 
    71 
       
    72 lemma sroot_set:
       
    73   "valid s \<Longrightarrow> \<exists> sec. sroot = (Init [], sec, None, {}) \<and> sectxt_of_obj s (O_dir []) = Some sec"
       
    74 apply (frule root_is_dir)
       
    75 apply (drule is_dir_has_sec, simp)
       
    76 apply (auto simp:sroot_def sec_of_root_def sectxt_of_obj_def type_of_obj.simps 
       
    77                  root_type_remains root_user_remains
       
    78            dest!:root_has_type' root_has_user' root_has_init_type' root_has_init_user'
       
    79            split:option.splits)
       
    80 done
       
    81 
       
    82 lemma cf2sfile_path_file:
       
    83   "\<lbrakk>is_file s (f # pf); valid s\<rbrakk>
       
    84    \<Longrightarrow> cf2sfile s (f # pf) = (
       
    85      case (cf2sfile s pf) of
       
    86        Some (pfi, pfsec, psec, asecs) \<Rightarrow> 
       
    87           (case (sectxt_of_obj s (O_file (f # pf))) of
       
    88               Some fsec \<Rightarrow> Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)
       
    89                                 else Created, fsec, Some pfsec, asecs \<union> {pfsec})
       
    90            | None \<Rightarrow> None)
       
    91      | _ \<Rightarrow> None)"
       
    92 apply (frule is_file_in_current, drule parentf_is_dir'', simp)
       
    93 apply (frule is_dir_has_sfile, simp, frule is_file_has_sfile, simp)
       
    94 apply (frule sroot_set)
       
    95 apply (case_tac pf, (clarsimp simp:get_parentfs_ctxts'_def sectxt_of_pf_def)+) 
       
    96 done
       
    97 
       
    98 lemma cf2sfile_path_dir:
       
    99   "\<lbrakk>is_dir s (f # pf); valid s\<rbrakk>
       
   100    \<Longrightarrow> cf2sfile s (f # pf) = (
       
   101      case (cf2sfile s pf) of
       
   102        Some (pfi, pfsec, psec, asecs) \<Rightarrow> 
       
   103           (case (sectxt_of_obj s (O_dir (f # pf))) of
       
   104               Some fsec \<Rightarrow> Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)
       
   105                                 else Created, fsec, Some pfsec, asecs \<union> {pfsec})
       
   106            | None \<Rightarrow> None)
       
   107      | _ \<Rightarrow> None)"
       
   108 apply (frule is_dir_in_current, drule parentf_is_dir'', simp)
       
   109 apply (frule_tac f = "f # pf" in is_dir_has_sfile, simp)
       
   110 apply (frule_tac f = "pf" in is_dir_has_sfile, simp)
       
   111 apply (frule sroot_set)
       
   112 apply (case_tac pf, (clarsimp simp:get_parentfs_ctxts'_def sectxt_of_pf_def)+) 
       
   113 done  
       
   114 
    74 lemma cf2sfile_path:
   115 lemma cf2sfile_path:
    75   "\<lbrakk>f # pf \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) = (
   116   "\<lbrakk>f # pf \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) = (
    76      case (cf2sfile s pf) of
   117      case (cf2sfile s pf) of
    77        Some (pfi, pfsec, psec, asecs) \<Rightarrow> (if (is_file s (f # pf))
   118        Some (pfi, pfsec, psec, asecs) \<Rightarrow> (if (is_file s (f # pf))
    78          then (case (sectxt_of_obj s (O_file (f # pf))) of
   119          then (case (sectxt_of_obj s (O_file (f # pf))) of
    79                  Some fsec \<Rightarrow> Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)
   120                  Some fsec \<Rightarrow> Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)
    80                                    else Created, fsec, Some pfsec, asecs \<union> {pfsec})
   121                                    else Created, fsec, Some pfsec, asecs \<union> {pfsec})
    81                | None \<Rightarrow> None)
   122                | None \<Rightarrow> None)
    82          else (case (sectxt_of_obj s (O_dir (f # pf))) of
   123          else (case (sectxt_of_obj s (O_dir (f # pf))) of
    83                  Some fsec \<Rightarrow> Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)
   124                  Some fsec \<Rightarrow> Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)
    84                                    else Created, fsec, Some pfsec, asecs \<union> {pfsec})
   125                                    else Created, fsec, Some pfsec, asecs \<union> {pfsec})
    85                | None \<Rightarrow> None)           )
   126                | None \<Rightarrow> None)           )
    86      | None \<Rightarrow> None)"
   127      | None \<Rightarrow> None)"
       
   128 apply (drule is_file_or_dir, simp)
       
   129 apply (erule disjE)
       
   130 apply (frule cf2sfile_path_file, simp) defer
       
   131 apply (frule cf2sfile_path_dir, simp, drule is_dir_not_file)
       
   132 apply (auto split:option.splits)
       
   133 done
       
   134 
       
   135 
       
   136 
       
   137 apply simp
       
   138 
       
   139 thm cf2sfile_def
       
   140 apply (simp (no_asm_simp))
       
   141 apply simp
       
   142 apply (frule cf2sfile_path_file, simp)
       
   143 apply (simp add: cf2sfile_path_file)
       
   144 apply auto
       
   145 apply (simp only:cf2sfile_path_file)
       
   146 by (simp add:cf2sfile_path_file cf2sfile_path_dir)
    87 apply (frule parentf_is_dir'', simp)
   147 apply (frule parentf_is_dir'', simp)
    88 apply (frule parentf_in_current', simp)
       
    89 apply (frule is_file_or_dir, simp)
   148 apply (frule is_file_or_dir, simp)
    90 apply (frule_tac f = pf in current_file_has_sfile, simp, erule exE)
   149 apply (frule sroot_set, erule disjE)
    91 apply (auto dest!:is_file_has_sec' is_dir_has_sec' get_pfs_secs_prop
   150 apply (frule is_dir_has_sfile, simp, frule is_file_has_sfile, simp)
    92             simp:cf2sfile_def split:option.splits if_splits)
   151 apply (case_tac pf, clarsimp)
       
   152 apply (auto dest!:is_file_has_sec' is_dir_has_sec' get_pfs_secs_prop simp:cf2sfile_def get_parentfs_ctxts.simps
       
   153             simp:get_parentfs_ctxts'_def sectxt_of_pf_def split:option.splits if_splits)[1]
       
   154 apply (auto dest!:is_file_has_sec' is_dir_has_sec' get_pfs_secs_prop 
       
   155             simp:get_parentfs_ctxts'_def sectxt_of_pf_def split:option.splits if_splits)[1]
    93 apply (case_tac "is_file s (f # pf)")
   156 apply (case_tac "is_file s (f # pf)")
    94 apply (frule is_file_has_sec, simp)
   157 apply (frule is_file_has_sec, simp)
    95 apply (frule is_dir_has_sec, simp)
   158 apply (frule is_dir_has_sec, simp)
    96 apply (frule is_dir_not_file)
   159 apply (frule is_dir_not_file)
    97 apply (erule exE)+
   160 apply (erule exE)+