1 (*<*)

     2 theory Co2sobj_prop

     3 imports Main Flask Flask_type Static Static_type Sectxt_prop Init_prop Current_files_prop Current_sockets_prop

     4 begin

     5 (*<*)

     6 

     7 context tainting_s begin

     8 

     9 (************ simpset for cf2sfile ***************)

    10 

    11 declare get_parentfs_ctxts.simps [simp del]

    12 

    13 lemma cf2sfile_open_none:

    14   "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) f b = cf2sfile s f b"

    15 apply (frule vd_cons, frule vt_grant_os)

    16 apply (frule noroot_events)

    17 by (auto split:if_splits option.splits    dest!:current_has_sec'

    18           simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 

    19                get_parentfs_ctxts_simps)

    20 

    21 lemma cf2sfile_open_some1:

    22   "\<lbrakk>valid (Open p f flag fd (Some inum) # s); f' \<in> current_files s\<rbrakk>

    23    \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'"

    24 apply (frule vd_cons, frule vt_grant_os, frule noroot_events, rule ext)

    25 apply (induct f')

    26 apply (auto  split:if_splits option.splits    dest!:current_has_sec'

    27           simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 

    28                get_parentfs_ctxts_simps)

    29 done

    30 

    31 lemma cf2sfile_open_some2:

    32   "\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_file s f'\<rbrakk>

    33    \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' True = cf2sfile s f' True"

    34 apply (frule vd_cons, drule is_file_in_current)

    35 by (simp add:cf2sfile_open_some1)

    36 

    37 lemma cf2sfile_open_some3:

    38   "\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_dir s f'\<rbrakk>

    39    \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' False = cf2sfile s f' False"

    40 apply (frule vd_cons, drule is_dir_in_current)

    41 by (simp add:cf2sfile_open_some1)

    42 

    43 lemma cf2sfile_open_some:

    44   "valid (Open p f flag fd (Some inum) # s) \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f True = (

    45      case (parent f) of

    46        Some pf \<Rightarrow> (case (sectxt_of_obj (Open p f flag fd (Some inum) # s) (O_file f), sectxt_of_obj s (O_dir pf), 

    47                          get_parentfs_ctxts s pf) of

    48                     (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)

    49                   | _ \<Rightarrow> None)

    50      | None \<Rightarrow> None)"

    51 apply (frule vd_cons, frule vt_grant_os, frule noroot_events)

    52 apply (auto split:if_splits option.splits    dest!:current_has_sec'

    53           simp:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 

    54                get_parentfs_ctxts_simps)

    55 

    56 

    57 

    58 lemma cf2sfile_open:

    59   "valid (Open p f flag fd opt # s) \<Longrightarrow> cf2sfile (Open p f flag fd opt # s) = (\<lambda> f' b. 

    60      if (opt = None) then cf2sfile s f' b

    61      else if (f' = f \<and> b = True) 

    62      then (case (parent f) of

    63              Some pf \<Rightarrow> (case (sectxt_of_obj s (O_file f), sectxt_of_obj s (O_dir pf), 

    64                  get_parentfs_ctxts s pf) of

    65                           (Some sec, Some psec, Some asecs) \<Rightarrow>

    66                               Some (if (\<not> deleted (O_file f) s \<and> f \<in> init_files) 

    67                                     then Init f else Created, sec, Some psec, set asecs)

    68                         | _ \<Rightarrow> None)

    69            | None \<Rightarrow> None)

    70      else cf2sfile s f' b)"

    71 apply (frule vd_cons, frule vt_grant_os, rule ext, rule ext)

    72 apply (auto split:if_splits option.splits 

    73              simp:sectxt_of_obj_simps)

    74 

    75 

    76 

    77 

    78 

    79 

    80 

    81 

    82 

    83 

    84 

    85 

    86 lemma cf2sfile_keep_path: "\<lbrakk>f \<preceq> f'; \<tau> \<in> vt rc_cs\<rbrakk> \<Longrightarrow> cf2sfile \<tau> f \<preceq> cf2sfile \<tau> f'"

    87 apply (induct f', simp add:no_junior_def)

    88 apply (case_tac "f = a # f'", simp add:cf2sfile.simps)

    89 apply (drule no_junior_noteq, simp, simp add:cf2sfile.simps)

    90 done

    91 

    92 lemma ckp'_aux: "\<not> f \<preceq> a # f' \<Longrightarrow> \<not> f \<preceq> f'"

    93 by (auto simp:no_junior_def)

    94 

    95 lemma cf2sfile_keep_path': "\<lbrakk>\<not> f \<preceq> f'; \<tau> \<in> vt rc_cs; f \<in> current_files \<tau>; f' \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> \<not> cf2sfile \<tau> f \<preceq> cf2sfile \<tau> f'"

    96 apply (induct f', simp add:no_junior_def cf2sfile.simps, rule notI, drule cf2sfile_root_file, simp)

    97 apply (case_tac "f = a # f'", simp add:cf2sfile.simps)

    98 apply (rule notI)

    99 apply (frule ckp'_aux, simp, frule parentf_in_current', simp+)

   100 apply (case_tac "cf2sfile \<tau> f = cf2sfile \<tau> (a # f')", drule cf2sfile_inj, simp+)

   101 apply (simp add:cf2sfile.simps)

   102 by (drule no_junior_noteq, simp+)

   103 

   104 lemma cf2sfile_keep_path'': "\<lbrakk>cf2sfile \<tau> f \<preceq> cf2sfile \<tau> f'; \<tau> \<in> vt rc_cs; f \<in> current_files \<tau>; f' \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> f \<preceq> f'"

   105 using cf2sfile_keep_path'

   106 by (auto)

   107 

   108 lemma cf2sfile_open_some': "\<lbrakk>f \<in> current_files \<tau>; Open p f' flags fd (Some inum) # \<tau> \<in> vt rc_cs\<rbrakk> \<Longrightarrow> cf2sfile (Open p f' flags fd (Some inum) # \<tau>) f = cf2sfile \<tau> f"

   109 apply (frule vt_cons')

   110 apply (drule vt_grant_os)

   111 apply (induct f)

   112 apply (simp add:cf2sfile.simps)+

   113 apply (frule parentf_in_current', simp)

   114 apply (auto simp:os_grant.simps index_of_file.simps split:option.splits)

   115 done

   116 

   117 lemma cf2sfile_open_some: "\<lbrakk>Open p f flags fd (Some inum) # \<tau> \<in> vt rc_cs; parent f = Some pf\<rbrakk> 

   118                            \<Longrightarrow> cf2sfile (Open p f flags fd (Some inum) # \<tau>) f = (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf))"

   119 apply (case_tac f, simp)

   120 apply (frule vt_grant_os)

   121 apply (simp add:cf2sfile.simps os_grant.simps current_files_simps index_of_file.simps cf2sfile_open_some')

   122 done

   123 

   124 lemma cf2sfile_open_none: "cf2sfile (Open p f flags fd None # \<tau>) f' = cf2sfile \<tau> f'"

   125 apply (induct f')

   126 by (simp add:cf2sfile.simps index_of_file.simps split:option.splits nat.splits)+

   127 

   128 lemma cf2sfile_open: "\<lbrakk>Open p f flags fd opt # \<tau> \<in> vt rc_cs; f' \<in> current_files (Open p f flags fd opt # \<tau>)\<rbrakk> \<Longrightarrow> 

   129                        cf2sfile (Open p f flags fd opt # \<tau>) f' = (

   130                          if (opt = None) then cf2sfile \<tau> f'

   131                          else if (f' = f) then (case (parent f) of

   132                                                   Some pf \<Rightarrow> (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf))

   133                                                 | _       \<Rightarrow> [])

   134                               else cf2sfile \<tau> f'                                                          )"

   135 apply (frule vt_grant_os)

   136 by (auto simp:os_grant.simps current_files_simps intro:cf2sfile_open_none cf2sfile_open_some cf2sfile_open_some' split:if_splits option.splits)

   137 

   138 lemma cf2sfile_mkdir_some': "\<lbrakk>Mkdir p f' inum # \<tau> \<in> vt rc_cs; f \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> cf2sfile (Mkdir p f' inum # \<tau>) f = cf2sfile \<tau> f"

   139 apply (frule vt_cons', drule vt_grant_os)

   140 apply (induct f, (simp add:cf2sfile.simps)+)

   141 apply (frule parentf_in_current', simp)

   142 apply (auto simp:os_grant.simps index_of_file.simps split:option.splits)

   143 done

   144 

   145 lemma cf2sfile_mkdir_some: "\<lbrakk>Mkdir p f inum # \<tau> \<in> vt rc_cs; parent f = Some pf\<rbrakk>

   146                              \<Longrightarrow> cf2sfile (Mkdir p f inum # \<tau>) f = (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf))"

   147 apply (case_tac f, simp)

   148 apply (frule vt_grant_os)

   149 apply (simp add:cf2sfile.simps os_grant.simps current_files_simps index_of_file.simps cf2sfile_mkdir_some')

   150 done

   151 

   152 lemma cf2sfile_mkdir: "\<lbrakk>Mkdir p f inum # \<tau> \<in> vt rc_cs; f' \<in> current_files (Mkdir p f inum # \<tau>)\<rbrakk> \<Longrightarrow>

   153                         cf2sfile (Mkdir p f inum # \<tau>) f' = (

   154                           if (f' = f) then (case (parent f) of

   155                                               Some pf \<Rightarrow> (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf))

   156                                             | _       \<Rightarrow> [])

   157                           else cf2sfile \<tau> f'               ) "

   158 apply (frule vt_grant_os)

   159 by (auto simp:os_grant.simps current_files_simps intro:cf2sfile_mkdir_some cf2sfile_mkdir_some' split:if_splits option.splits)

   160 

   161 lemma cf2sfile_linkhard_none: "\<lbrakk>LinkHard p f\<^isub>1 f\<^isub>2 # \<tau> \<in> vt rc_cs; f \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> cf2sfile (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) f = cf2sfile \<tau> f"

   162 apply (frule vt_cons')

   163 apply (drule vt_grant_os)

   164 apply (induct f)

   165 apply (simp add:cf2sfile.simps)+

   166 apply (frule parentf_in_current', simp)

   167 apply (auto simp:os_grant.simps index_of_file.simps split:option.splits)

   168 done

   169 

   170 lemma cf2sfile_linkhard_some: 

   171   "\<lbrakk>LinkHard p f\<^isub>1 f\<^isub>2 # \<tau> \<in> vt rc_cs; parent f\<^isub>2 = Some pf\<^isub>2\<rbrakk> \<Longrightarrow> cf2sfile (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) f\<^isub>2 = (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>2))"

   172 apply (case_tac f\<^isub>2, simp)

   173 apply (frule vt_grant_os)

   174 apply (simp add:cf2sfile.simps os_grant.simps current_files_simps index_of_file.simps cf2sfile_linkhard_none)

   175 done

   176 

   177 lemma cf2sfile_linkhard: "\<lbrakk>LinkHard p f\<^isub>1 f\<^isub>2 # \<tau> \<in> vt rc_cs; f \<in> current_files (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>)\<rbrakk> \<Longrightarrow>

   178                            cf2sfile (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) f = (

   179                              if (f = f\<^isub>2) then (case (parent f\<^isub>2) of

   180                                                  Some pf\<^isub>2 \<Rightarrow> SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>2)

   181                                                | _        \<Rightarrow> [])

   182                              else cf2sfile \<tau> f                 )"

   183 apply (frule vt_grant_os)

   184 by (auto simp:os_grant.simps current_files_simps intro:cf2sfile_linkhard_none cf2sfile_linkhard_some split:if_splits option.splits)

   185 

   186 

   187 lemma no_junior_aux: "\<not> f\<^isub>2 \<preceq> a # f \<Longrightarrow> \<not> f\<^isub>2 \<preceq> f"

   188 by (auto simp:no_junior_def)

   189 

   190 lemma cf2sfile_rename_aux: "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; f \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> f \<noteq> f\<^isub>3 \<and> \<not> f\<^isub>3 \<preceq> f"

   191 apply (frule vt_grant_os, simp add:os_grant.simps, (erule exE|erule conjE)+)

   192 apply (rule conjI, rule notI, simp)

   193 apply (rule notI, drule vt_cons', simp add:ancenf_in_current)

   194 done

   195 

   196 lemma cf2sfile_rename'1: 

   197   "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; f \<in> current_files \<tau>; \<not> (f\<^isub>2 \<preceq> f)\<rbrakk> \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f = cf2sfile \<tau> f"

   198 apply (frule vt_cons',frule vt_grant_os,  induct f)

   199 apply (simp add:cf2sfile.simps)

   200 apply (frule parentf_in_current', simp, simp)

   201 apply (frule no_junior_aux, simp)

   202 apply (simp add:os_grant.simps, (erule exE|erule conjE)+)

   203 apply (drule cf2sfile_rename_aux, simp, erule conjE)

   204 apply (auto simp add:cf2sfile.simps index_of_file.simps split:option.splits nat.splits)

   205 done

   206 

   207 lemma cf2sfile_rename'2: 

   208   "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; \<not> (f\<^isub>3 \<preceq> f)\<rbrakk> \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f = cf2sfile \<tau> f"

   209 apply (frule vt_cons', induct f)

   210 by (auto simp add:index_of_file.simps cf2sfile.simps no_junior_def split:option.splits nat.splits)

   211 

   212 lemma cf2sfile_rename1:

   213   "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; parent f\<^isub>3 = Some pf\<^isub>3\<rbrakk> \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f\<^isub>3 = SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>3)"

   214 apply (case_tac f\<^isub>3, simp add:cf2sfile.simps)

   215 apply (auto dest!:cf2sfile_rename'2 simp add:no_junior_def cf2sfile.simps index_of_file.simps split:option.splits)

   216 done

   217 

   218 lemma index_of_file_rename1: "\<lbrakk>f\<^isub>2 \<preceq> f; f \<noteq> f\<^isub>2\<rbrakk> \<Longrightarrow> index_of_file (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) (file_after_rename f\<^isub>2 f\<^isub>3 f) = index_of_file \<tau> f"

   219 apply (clarsimp simp add:index_of_file.simps split:option.splits)

   220 by (frule_tac f\<^isub>3 = f\<^isub>3 in file_renaming_prop3, simp, erule conjE, simp add:file_renaming_prop5)

   221 

   222 lemma cf2sfile_rename2: "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; (file_before_rename f\<^isub>2 f\<^isub>3 f) \<in> current_files \<tau>; parent f\<^isub>3 = Some pf\<^isub>3; f\<^isub>3 \<preceq> f\<rbrakk> 

   223    \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f = file_after_rename (cf2sfile \<tau> f\<^isub>2) (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>3)) (cf2sfile \<tau> (file_before_rename f\<^isub>2 f\<^isub>3 f))"

   224 apply (induct f, simp add:no_junior_def)

   225 apply (case_tac "a # f = f\<^isub>3", simp)

   226 apply (drule cf2sfile_rename1, simp, simp add:file_renaming_prop0' file_renaming_prop0)

   227 

   228 apply (frule no_junior_noteq, simp, simp)

   229 apply (frule_tac file_renaming_prop1')

   230 apply (frule_tac f = f\<^isub>2 and \<tau> = \<tau> in cf2sfile_keep_path, simp add:vt_cons')

   231 apply (frule_tac f\<^isub>2 = f\<^isub>2 and a = a in file_renaming_prop8')

   232 apply (frule_tac f\<^isub>2 = f\<^isub>2 and a = a in file_renaming_prop6')

   233 apply (frule_tac f = "file_before_rename f\<^isub>2 f\<^isub>3 (a # f)" and \<tau> = \<tau> and f\<^isub>2 = f\<^isub>2 and f\<^isub>3 = f\<^isub>3 and p = p in index_of_file_rename1, simp add:file_before_rename_def)

   234 apply (drule_tac f\<^isub>3 = f\<^isub>3 and f\<^isub>1 = f and a = a and f\<^isub>2 = f\<^isub>2 in file_renaming_prop9', simp)

   235 apply (drule parentf_in_current', simp add:vt_cons')

   236 apply (simp add:cf2sfile.simps)

   237 apply (erule file_renaming_prop6[THEN sym])

   238 done

   239 

   240 lemma cf2sfile_rename2': "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; f \<in> current_files \<tau>; parent f\<^isub>3 = Some pf\<^isub>3; f\<^isub>2 \<preceq> f\<rbrakk> 

   241    \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) (file_after_rename f\<^isub>2 f\<^isub>3 f) = file_after_rename (cf2sfile \<tau> f\<^isub>2) (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>3)) (cf2sfile \<tau> f)"

   242 apply (frule_tac f\<^isub>3 = f\<^isub>3 in file_renaming_prop5)

   243 apply (frule_tac f\<^isub>3 = f\<^isub>3 in file_renaming_prop1)

   244 apply (drule_tac f = "file_after_rename f\<^isub>2 f\<^isub>3 f" in cf2sfile_rename2, simp+)

   245 done

   246 

   247 lemma cf2sfile_rename3: "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; f \<in> current_files \<tau>; parent f\<^isub>3 = Some pf\<^isub>3\<rbrakk> 

   248    \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) (file_after_rename f\<^isub>2 f\<^isub>3 f) = file_after_rename (cf2sfile \<tau> f\<^isub>2) (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>3)) (cf2sfile \<tau> f)"

   249 apply (case_tac "f\<^isub>2 \<preceq> f")

   250 apply (rule cf2sfile_rename2', simp+)

   251 apply (frule vt_grant_os)

   252 apply (frule_tac \<tau> = \<tau> in cf2sfile_keep_path', simp add:vt_cons', simp add:os_grant.simps, simp)

   253 apply (simp add:file_after_rename_def)

   254 by (rule cf2sfile_rename'1, simp+)

   255 

   256 lemma cf2sfile_rename: "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; f \<in> current_files (Rename p f\<^isub>2 f\<^isub>3 # \<tau>)\<rbrakk> \<Longrightarrow>

   257                          cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f = (

   258                            if (f\<^isub>3 \<preceq> f) then (case (parent f\<^isub>3) of 

   259                                                Some pf\<^isub>3 \<Rightarrow> file_after_rename (cf2sfile \<tau> f\<^isub>2) (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>3)) (cf2sfile \<tau> (file_before_rename f\<^isub>2 f\<^isub>3 f))

   260                                              | _        \<Rightarrow> [])

   261                            else cf2sfile \<tau> f               )"

   262 apply (frule vt_grant_os)

   263 apply (case_tac "f = f\<^isub>3", clarsimp simp:os_grant.simps, drule cf2sfile_rename1, simp+, simp add:file_renaming_prop0' file_renaming_prop0)

   264 

   265 apply (auto simp:os_grant.simps current_files_simps intro:cf2sfile_rename'2 cf2sfile_rename1 split:if_splits option.splits) 

   266 apply (rule cf2sfile_rename2, simp, drule rename_renaming_decom, simp+)

   267 apply (drule_tac f\<^isub>2 = f\<^isub>2 and f\<^isub>1 = f\<^isub>1 and f\<^isub>3 = f\<^isub>3 in file_renaming_prop5, simp+)

   268 done

   269 

   270 lemma cf2sfile_other: "\<lbrakk>

   271                         \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;

   272                         \<forall> p f im. e \<noteq> Mkdir p f im;

   273                         \<forall> p f\<^isub>1 f\<^isub>2. e \<noteq> LinkHard p f\<^isub>1 f\<^isub>2;

   274                         \<forall> p f\<^isub>2 f\<^isub>3. e \<noteq> Rename p f\<^isub>2 f\<^isub>3\<rbrakk> \<Longrightarrow> cf2sfile (e # \<tau>) f' = cf2sfile \<tau> f'"

   275 apply (induct f', simp add:cf2sfile.simps index_of_file.simps split:option.splits nat.splits)

   276 apply (case_tac e, auto simp add:cf2sfile.simps index_of_file.simps split:option.splits nat.splits)

   277 done

   278 

   279 lemmas cf2sfile_nil = init_cf2sfile

   280 

   281 lemma cf2sfile_nil': "f \<in> current_files [] \<Longrightarrow> cf2sfile [] f = map SInit f"

   282 by (simp add:cf2sfile_nil current_files_simps)

   283 

   284 lemmas cf2sfile_simps = cf2sfile_nil cf2sfile_nil' cf2sfile_open cf2sfile_mkdir cf2sfile_linkhard cf2sfile_rename cf2sfile_other

   285 

   286 lemmas cf2sfile_simpss = cf2sfile_nil cf2sfile_nil' cf2sfile_open_some' cf2sfile_open_some cf2sfile_open_none cf2sfile_open cf2sfile_mkdir_some' cf2sfile_mkdir_some

   287                          cf2sfile_mkdir cf2sfile_linkhard_none cf2sfile_linkhard_some cf2sfile_linkhard cf2sfile_rename'1 cf2sfile_rename'2 cf2sfile_rename1

   288                          cf2sfile_rename2 cf2sfile_rename2' cf2sfile_rename3 cf2sfile_rename cf2sfile_other

   289 

   290 lemma cf2sfile_open_some'_inum: "\<lbrakk>Open p f' flags fd (Some inum) # \<tau> \<in> vt rc_cs; inum_of_file \<tau> f = Some im\<rbrakk> \<Longrightarrow> cf2sfile (Open p f' flags fd (Some inum) # \<tau>) f = cf2sfile \<tau> f"

   291 by (simp add:cf2sfile_open_some' current_files_def)

   292 

   293 lemma cf2sfile_mkdir_some'_inum: "\<lbrakk>Mkdir p f' inum # \<tau> \<in> vt rc_cs; inum_of_file \<tau> f = Some im\<rbrakk> \<Longrightarrow> cf2sfile (Mkdir p f' inum # \<tau>) f = cf2sfile \<tau> f"

   294 by (simp add:cf2sfile_mkdir_some' current_files_def)

   295 

   296 lemma cf2sfile_linkhard_none_inum: "\<lbrakk>LinkHard p f\<^isub>1 f\<^isub>2 # \<tau> \<in> vt rc_cs; inum_of_file \<tau> f = Some im\<rbrakk> \<Longrightarrow> cf2sfile (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) f = cf2sfile \<tau> f"

   297 by (simp add:cf2sfile_linkhard_none current_files_def)

   298 

   299 lemma cf2sfile_rename'1_inum: 

   300   "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; inum_of_file \<tau> f = Some im ; \<not> (f\<^isub>2 \<preceq> f)\<rbrakk> \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f = cf2sfile \<tau> f"

   301 by (simp add:cf2sfile_rename'1 current_files_def)

   302 

   303 lemma cf2sfile_rename2_inum: "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; inum_of_file \<tau> (file_before_rename f\<^isub>2 f\<^isub>3 f) = Some im; parent f\<^isub>3 = Some pf\<^isub>3; f\<^isub>3 \<preceq> f\<rbrakk> 

   304    \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f = file_after_rename (cf2sfile \<tau> f\<^isub>2) (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>3)) (cf2sfile \<tau> (file_before_rename f\<^isub>2 f\<^isub>3 f))"

   305 by (simp add:cf2sfile_rename2 current_files_def)

   306 

   307 lemma cf2sfile_rename2'_inum: "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; inum_of_file \<tau> f = Some im; parent f\<^isub>3 = Some pf\<^isub>3; f\<^isub>2 \<preceq> f\<rbrakk> 

   308    \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) (file_after_rename f\<^isub>2 f\<^isub>3 f) = file_after_rename (cf2sfile \<tau> f\<^isub>2) (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>3)) (cf2sfile \<tau> f)"

   309 by (simp add:cf2sfile_rename2' current_files_def)

   310 

   311 lemma cf2sfile_rename3_inum: "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; inum_of_file \<tau> f = Some im; parent f\<^isub>3 = Some pf\<^isub>3\<rbrakk> 

   312    \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) (file_after_rename f\<^isub>2 f\<^isub>3 f) = file_after_rename (cf2sfile \<tau> f\<^isub>2) (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>3)) (cf2sfile \<tau> f)"

   313 by (simp add:cf2sfile_rename3 current_files_def)

   314 

   315 lemma cf2sfile_nil'_inum: "inum_of_file [] f = Some im \<Longrightarrow> cf2sfile [] f = map SInit f"

   316 by (simp add:cf2sfile_nil' current_files_def)

   317 

   318 lemmas cf2sfile_simps_inum = cf2sfile_nil cf2sfile_nil'_inum cf2sfile_open_some'_inum cf2sfile_open_some cf2sfile_open_none cf2sfile_open cf2sfile_mkdir_some'_inum cf2sfile_mkdir_some

   319                          cf2sfile_mkdir cf2sfile_linkhard_none_inum cf2sfile_linkhard_some cf2sfile_linkhard cf2sfile_rename'1_inum cf2sfile_rename'2 cf2sfile_rename1

   320                          cf2sfile_rename2_inum cf2sfile_rename2'_inum cf2sfile_rename3_inum cf2sfile_rename cf2sfile_other

   321 

   322 (*************** cp2sproc simpset *********************)

   323 

   324 lemma cp2sproc_nil: "p \<in> init_processes \<Longrightarrow> cp2sproc [] p = SInit p"

   325 by (simp add:cp2sproc_def index_of_proc.simps)

   326 

   327 lemma cp2sproc_nil': "p \<in> current_procs [] \<Longrightarrow> cp2sproc [] p = SInit p"

   328 by (simp add:cp2sproc_nil current_procs.simps)

   329 

   330 lemma cp2sproc_clone: "cp2sproc (Clone p p' # \<tau>) p'' = (

   331                          if (p'' = p') then SCrea (Suc (length \<tau>))

   332                          else cp2sproc \<tau> p''           )"

   333 by (auto simp:cp2sproc_def index_of_proc.simps d2s_aux.simps)

   334 

   335 lemma cp2sproc_other: "\<forall> p p'. e \<noteq> Clone p p' \<Longrightarrow> cp2sproc (e # \<tau>) p'' = cp2sproc \<tau> p''"

   336 apply (case_tac e)

   337 by (auto simp:cp2sproc_def index_of_proc.simps d2s_aux.simps)

   338 

   339 lemmas cp2sproc_simps = cp2sproc_nil cp2sproc_nil' cp2sproc_clone cp2sproc_other

   340 

   341 (******************** ch2sshm simpset **************************)

   342 

   343 lemma ch2sshm_nil: "h \<in> init_shms \<Longrightarrow> ch2sshm [] h = SInit h"

   344 by (simp add:ch2sshm_def index_of_shm.simps)

   345 

   346 lemma ch2sshm_nil': "h \<in> current_shms [] \<Longrightarrow> ch2sshm [] h = SInit h"

   347 by (simp add:ch2sshm_nil current_shms.simps)

   348 

   349 lemma ch2sshm_createshm: "ch2sshm (CreateShM p h # \<tau>) h' = (if (h' = h) then SCrea (Suc (length \<tau>)) else ch2sshm \<tau> h')"

   350 by (simp add:ch2sshm_def index_of_shm.simps d2s_aux.simps) 

   351 

   352 lemma ch2sshm_other: "\<forall> p h. e \<noteq> CreateShM p h \<Longrightarrow> ch2sshm (e # \<tau>) h' = ch2sshm \<tau> h'"

   353 apply (case_tac e)

   354 by (auto simp add:ch2sshm_def index_of_shm.simps d2s_aux.simps) 

   355 

   356 lemmas ch2sshm_simps = ch2sshm_nil ch2sshm_nil' ch2sshm_createshm ch2sshm_other

   357 

   358 (********************* cm2smsg simpset ***********************)

   359 

   360 lemma cm2smsg_nil: "m \<in> init_msgs \<Longrightarrow> cm2smsg [] m = SInit m"

   361 by (simp add:cm2smsg_def index_of_msg.simps)

   362 

   363 lemma cm2smsg_nil': "m \<in> current_msgs [] \<Longrightarrow> cm2smsg [] m = SInit m"

   364 by (simp add:cm2smsg_nil current_msgs.simps)

   365 

   366 lemma cm2smsg_createmsg: "cm2smsg (CreateMsg p m # \<tau>) m' = (if (m' = m) then SCrea (Suc (length \<tau>)) else cm2smsg \<tau> m')"

   367 by (simp add:cm2smsg_def index_of_msg.simps d2s_aux.simps)

   368 

   369 lemma cm2smsg_other: "\<forall> p m. e \<noteq> CreateMsg p m \<Longrightarrow> cm2smsg (e # \<tau>) m' = cm2smsg \<tau> m'"

   370 apply (case_tac e)

   371 by (auto simp:cm2smsg_def index_of_msg.simps d2s_aux.simps)

   372 

   373 lemmas cm2smsg_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other

   374 

   375 (********************** cfd2fd_s simpset ******************************)

   376 

   377 lemma cfd2fd_s_nil: "fd \<in> init_fds_of_proc p \<Longrightarrow> cfd2fd_s [] p fd = SInit fd"

   378 by (simp add:cfd2fd_s_def index_of_fd.simps)

   379 

   380 lemma cfd2fd_s_nil': "fd \<in> current_proc_fds [] p \<Longrightarrow> cfd2fd_s [] p fd = SInit fd"

   381 by (simp add:cfd2fd_s_nil current_proc_fds.simps)

   382 

   383 lemma cfd2fd_s_open: "cfd2fd_s (Open p f flags fd opt # \<tau>) p' fd' = (

   384                         if (p = p') then (if (fd = fd') then SCrea (Suc (length \<tau>)) 

   385                                           else cfd2fd_s \<tau> p' fd')

   386                         else cfd2fd_s \<tau> p' fd'                      )"

   387 by (simp add:cfd2fd_s_def index_of_fd.simps d2s_aux.simps)

   388 

   389 lemma cfd2fd_s_createsock: "cfd2fd_s (CreateSock p af st fd im # \<tau>) p' fd' = (

   390                               if (p = p') then (if (fd = fd') then SCrea (Suc (length \<tau>)) 

   391                                           else cfd2fd_s \<tau> p' fd')

   392                               else cfd2fd_s \<tau> p' fd'                         )"

   393 by (simp add:cfd2fd_s_def index_of_fd.simps d2s_aux.simps)

   394 

   395 lemma cfd2fd_s_accept: "cfd2fd_s (Accept p fd addr port fd' im # \<tau>) p' fd'' = (

   396                           if (p' = p) then (if (fd'' = fd') then SCrea (Suc (length \<tau>))

   397                                             else cfd2fd_s \<tau> p' fd'')

   398                           else cfd2fd_s \<tau> p' fd''                             )"

   399 by (simp add:cfd2fd_s_def index_of_fd.simps d2s_aux.simps)

   400 

   401 lemma cfd2fd_s_clone: "cfd2fd_s (Clone p p' # \<tau>) p'' fd = (if (p'' = p') then cfd2fd_s \<tau> p fd else cfd2fd_s \<tau> p'' fd)"

   402 by (simp add:cfd2fd_s_def index_of_fd.simps d2s_aux.simps)

   403 

   404 lemma cfd2fd_s_other: "\<lbrakk>\<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;

   405                         \<forall> p af st fd im. e \<noteq> CreateSock p af st fd im;

   406                         \<forall> p fd addr port fd' im. e \<noteq> Accept p fd addr port fd' im;

   407                         \<forall> p p'. e \<noteq> Clone p p'\<rbrakk> \<Longrightarrow> cfd2fd_s (e # \<tau>) p'' fd'' = cfd2fd_s \<tau> p'' fd''"

   408 by (case_tac e, auto simp:cfd2fd_s_def index_of_fd.simps d2s_aux.simps)

   409 

   410 lemmas cfd2fd_s_simps = cfd2fd_s_nil cfd2fd_s_nil' cfd2fd_s_open cfd2fd_s_createsock cfd2fd_s_accept cfd2fd_s_clone cfd2fd_s_other

   411 

   412 (************* cim2im_s simpset **************************)

   413 

   414 (* no such lemma

   415 lemma cim2im_s_nil: "init_itag_of_inum im = Some tag \<Longrightarrow> cim2im_s [] im = SInit im"

   416 by (simp add:cim2im_s_def)

   417 *)

   418 

   419 lemma cim2im_s_open: "cim2im_s (Open p f flags fd (Some im) # \<tau>) im' = (if (im' = im) then SCrea (Suc (length \<tau>)) else cim2im_s \<tau> im')"

   420 by (simp add:cim2im_s_def)

   421 

   422 lemma cim2im_s_open': "cim2im_s (Open p f flags fd None # \<tau>) im = cim2im_s \<tau> im"

   423 by (simp add:cim2im_s_def)

   424 

   425 lemma cim2im_s_mkdir: "cim2im_s (Mkdir p f im # \<tau>) im' = (if (im' = im) then SCrea (Suc (length \<tau>)) else cim2im_s \<tau> im')"

   426 by (simp add:cim2im_s_def)

   427 

   428 lemma cim2im_s_createsock: "cim2im_s (CreateSock p sf st fd im # \<tau>) im' = (if (im' = im) then SCrea (Suc (length \<tau>)) else cim2im_s \<tau> im')"

   429 by (simp add:cim2im_s_def)

   430 

   431 lemma cim2im_s_accept: "cim2im_s (Accept p fd addr port fd' im # \<tau>) im' = (if (im' = im) then SCrea (Suc (length \<tau>)) else cim2im_s \<tau> im')"

   432 by (simp add:cim2im_s_def)

   433 

   434 lemma cim2im_s_other: "\<lbrakk>\<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;

   435                         \<forall> p f im. e \<noteq> Mkdir p f im;

   436                         \<forall> p sf st fd im. e \<noteq> CreateSock p sf st fd im;

   437                         \<forall> p fd addr port fd' im. e \<noteq> Accept p fd addr port fd' im\<rbrakk> \<Longrightarrow> cim2im_s (e # \<tau>) im = cim2im_s \<tau> im"

   438 by (case_tac e, auto simp:cim2im_s_def)

   439 

   440 lemmas cim2im_s_simps = cim2im_s_open cim2im_s_open' cim2im_s_mkdir cim2im_s_createsock cim2im_s_accept cim2im_s_other

   441 

   442 

   443 lemma cig2ig_s_simp: "cig2ig_s (e # \<tau>) tag = cig2ig_s \<tau> tag"

   444 apply (case_tac tag)

   445 by auto

   446 

   447 (******************* cobj2sobj no Suc (length \<tau>) ***********************)

   448 

   449 lemma cf2sfile_le_len: "\<lbrakk>cf2sfile \<tau> f = SCrea (Suc (length \<tau>)) # spf; f \<in> current_files \<tau>; \<tau> \<in> vt rc_cs\<rbrakk> \<Longrightarrow> False"

   450 apply (case_tac f, (simp add:cf2sfile.simps d2s_aux.simps)+)

   451 apply (case_tac "index_of_file \<tau> (a # list)", (simp add:d2s_aux.simps)+)

   452 by (drule index_of_file_le_length', simp+)

   453 

   454 lemma cf2sfile_le_len': "\<lbrakk>SCrea (Suc (length \<tau>)) # spf \<preceq> cf2sfile \<tau> f; f \<in> current_files \<tau>; \<tau> \<in> vt rc_cs\<rbrakk> \<Longrightarrow> False"

   455 apply (induct f)

   456 apply (simp add:no_junior_def cf2sfile.simps d2s_aux.simps)

   457 apply (case_tac "cf2sfile \<tau> (a # f) = SCrea (Suc (length \<tau>)) # spf") 

   458 apply (drule_tac f = "a # f" in cf2sfile_le_len, simp+)

   459 apply (simp only:cf2sfile.simps d2s_aux.simps)

   460 apply (drule_tac no_junior_noteq, simp+)

   461 apply (rule impI, erule impE, simp+)

   462 apply (drule parentf_in_current', simp+)

   463 done

   464 

   465 lemma cp2sproc_le_len: "cp2sproc \<tau> p = SCrea (Suc (length \<tau>)) \<Longrightarrow> False"

   466 apply (simp add:cp2sproc_def, case_tac "index_of_proc \<tau> p")

   467 apply (simp add:d2s_aux.simps)+

   468 by (drule index_of_proc_le_length', simp)

   469 

   470 lemma ch2sshm_le_len: "ch2sshm \<tau> h = SCrea (Suc (length \<tau>)) \<Longrightarrow> False"

   471 apply (simp add:ch2sshm_def, case_tac "index_of_shm \<tau> h")

   472 apply (simp add:d2s_aux.simps)+

   473 by (drule index_of_shm_le_length', simp)

   474 

   475 lemma cm2smsg_le_len: "cm2smsg \<tau> m = SCrea (Suc (length \<tau>)) \<Longrightarrow> False"

   476 apply (simp add:cm2smsg_def, case_tac "index_of_msg \<tau> m")

   477 apply (simp add:d2s_aux.simps)+

   478 by (drule index_of_msg_le_length', simp)

   479 

   480 lemma cim2im_s_le_len: "cim2im_s \<tau> im = SCrea (Suc (length \<tau>)) \<Longrightarrow> False"

   481 apply (simp add:cim2im_s_def, case_tac "inum2ind \<tau> im")

   482 apply (simp add:d2s_aux.simps)+

   483 by (drule inum2ind_le_length', simp)

   484 

   485 lemma cfd2fd_s_le_len: "cfd2fd_s \<tau> p fd = SCrea (Suc (length \<tau>)) \<Longrightarrow> False"

   486 apply (simp add:cfd2fd_s_def, case_tac "index_of_fd \<tau> p fd")

   487 apply (simp add:d2s_aux.simps)+

   488 by (drule index_of_fd_le_length', simp)

   489 

   490 end

   491 

   492 (*<*)

   493 end

   494 (*>*)