1
+ − 1
theory all_sobj_prop
+ − 2
imports Main rc_theory os_rc obj2sobj_prop deleted_prop sound_defs_prop source_prop
+ − 3
begin
+ − 4
+ − 5
context tainting_s_complete begin
+ − 6
+ − 7
lemma initf_has_effinitialrole:
+ − 8
"f \<in> init_files ==> \<exists> r. effinitialrole [] f = Some r"
+ − 9
by (rule_tac f = f in file_has_effinitialrole, simp, simp add:vs_nil)
+ − 10
+ − 11
lemma initf_has_effforcedrole:
+ − 12
"f \<in> init_files ==> \<exists> r. effforcedrole [] f = Some r"
+ − 13
by (rule_tac f = f in file_has_effforcedrole, simp, simp add:vs_nil)
+ − 14
+ − 15
lemma efffrole_sdir_some:
+ − 16
"sd \<in> init_files ==> \<exists> r. erole_functor init_file_forcedrole InheritUpMixed sd = Some r"
+ − 17
apply (frule_tac s = "[]" in undel_initf_keeps_efrole, simp, simp add:vs_nil)
+ − 18
by (drule initf_has_effforcedrole, simp)
+ − 19
+ − 20
lemma efffrole_sdir_some':
+ − 21
"erole_functor init_file_forcedrole InheritUpMixed sd = None ==> sd \<notin> init_files"
+ − 22
by (rule notI, auto dest!:efffrole_sdir_some)
+ − 23
+ − 24
lemma effirole_sdir_some:
+ − 25
"sd \<in> init_files ==> \<exists> r. erole_functor init_file_initialrole UseForcedRole sd = Some r"
+ − 26
apply (frule_tac s = "[]" in undel_initf_keeps_eirole, simp, simp add:vs_nil)
+ − 27
by (drule initf_has_effinitialrole, simp)
+ − 28
+ − 29
lemma effirole_sdir_some':
+ − 30
"erole_functor init_file_initialrole UseForcedRole sd = None ==> sd \<notin> init_files"
+ − 31
by (rule notI, auto dest:effirole_sdir_some)
+ − 32
+ − 33
lemma erole_func_irole_simp:
+ − 34
"erole_functor init_file_initialrole UseForcedRole sd = effinitialrole [] sd"
+ − 35
by (simp add:effinitialrole_def)
+ − 36
+ − 37
lemma erole_func_frole_simp:
+ − 38
"erole_functor init_file_forcedrole InheritUpMixed sd = effforcedrole [] sd"
+ − 39
by (simp add:effforcedrole_def)
+ − 40
+ − 41
lemma init_effforcedrole_valid: "erole_functor init_file_forcedrole InheritUpMixed sd = Some r \<Longrightarrow> r = InheritUserRole \<or> r = InheritProcessRole \<or> r = InheritUpMixed \<or> (\<exists> nr. r = NormalRole nr)"
+ − 42
by (simp add:erole_func_frole_simp, erule effforcedrole_valid)
+ − 43
+ − 44
lemma init_effinitialrole_valid: "erole_functor init_file_initialrole UseForcedRole sd = Some r \<Longrightarrow> r = UseForcedRole \<or> (\<exists> nr. r = NormalRole nr)"
+ − 45
by (simp add:erole_func_irole_simp, erule effinitialrole_valid)
+ − 46
+ − 47
lemma exec_role_some:
+ − 48
"[|sd \<in> init_files; u \<in> init_users|] ==> \<exists> r'. exec_role_aux r sd u = Some r'"
+ − 49
by (auto simp:exec_role_aux_def split:option.splits t_role.splits
+ − 50
dest!:effirole_sdir_some' efffrole_sdir_some'
+ − 51
dest:init_effforcedrole_valid init_effinitialrole_valid
+ − 52
intro:effirole_sdir_some efffrole_sdir_some user_has_normalrole)
+ − 53
+ − 54
lemma chown_role_some:
+ − 55
"u \<in> init_users ==> \<exists> r'. chown_role_aux r fr u = Some r'"
+ − 56
by (auto simp:chown_role_aux_def split:option.splits t_role.splits
+ − 57
dest!:effirole_sdir_some' efffrole_sdir_some'
+ − 58
dest:init_effforcedrole_valid init_effinitialrole_valid
+ − 59
intro:effirole_sdir_some efffrole_sdir_some user_has_normalrole)
+ − 60
+ − 61
declare obj2sobj.simps [simp del]
+ − 62
+ − 63
lemma all_sobjs_I:
+ − 64
assumes ex: "exists s obj"
+ − 65
and vd: "valid s"
+ − 66
shows "obj2sobj s obj \<in> all_sobjs"
+ − 67
using ex vd
+ − 68
proof (induct s arbitrary:obj)
+ − 69
case Nil
+ − 70
assume ex:"exists [] obj"
+ − 71
show ?case
+ − 72
proof (cases obj)
+ − 73
case (Proc p) assume prem: "obj = Proc p"
+ − 74
with ex have initp:"p \<in> init_processes" by simp
+ − 75
from initp obtain r where "init_currentrole p = Some r"
+ − 76
using init_proc_has_role by (auto simp:bidirect_in_init_def)
+ − 77
moreover from initp obtain t where "init_process_type p = Some t"
+ − 78
using init_proc_has_type by (auto simp:bidirect_in_init_def)
+ − 79
moreover from initp obtain fr where "init_proc_forcedrole p = Some fr"
+ − 80
using init_proc_has_frole by (auto simp:bidirect_in_init_def)
+ − 81
moreover from initp obtain u where "init_owner p = Some u"
+ − 82
using init_proc_has_owner by (auto simp:bidirect_in_init_def)
+ − 83
ultimately have "obj2sobj [] (Proc p) \<in> all_sobjs"
+ − 84
using initp by (auto intro!:ap_init simp:obj2sobj.simps)
+ − 85
with prem show ?thesis by simp
+ − 86
next
+ − 87
case (File f) assume prem: "obj = File f"
+ − 88
with ex have initf: "f \<in> init_files" by simp
+ − 89
from initf obtain t where "etype_aux init_file_type_aux f = Some t"
+ − 90
using init_file_has_etype by auto
+ − 91
moreover from initf have "source_dir [] f = Some f"
+ − 92
by (simp add:source_dir_of_init')
+ − 93
ultimately have "obj2sobj [] (File f) \<in> all_sobjs"
+ − 94
using initf by (auto simp:etype_of_file_def obj2sobj.simps intro!:af_init)
+ − 95
with prem show ?thesis by simp
+ − 96
next
+ − 97
case (IPC i) assume prem: "obj = IPC i"
+ − 98
with ex have initi: "i \<in> init_ipcs" by simp
+ − 99
from initi obtain t where "init_ipc_type i = Some t"
+ − 100
using init_ipc_has_type by (auto simp:bidirect_in_init_def)
+ − 101
hence "obj2sobj [] (IPC i) \<in> all_sobjs"
+ − 102
using initi by (auto intro!:ai_init simp:obj2sobj.simps)
+ − 103
with prem show ?thesis by simp
+ − 104
qed
+ − 105
next
+ − 106
case (Cons e s)
+ − 107
assume prem: "\<And> obj. \<lbrakk>exists s obj; valid s\<rbrakk> \<Longrightarrow> obj2sobj s obj \<in> all_sobjs"
+ − 108
and ex_cons: "exists (e # s) obj" and vs_cons: "valid (e # s)"
+ − 109
have vs: "valid s" and rc: "rc_grant s e" and os: "os_grant s e"
+ − 110
using vs_cons by (auto intro:valid_cons valid_os valid_rc)
+ − 111
from prem and vs have prem': "\<And> obj. exists s obj \<Longrightarrow> obj2sobj s obj \<in> all_sobjs" by simp
+ − 112
show ?case
+ − 113
proof (cases e)
+ − 114
case (ChangeOwner p u)
+ − 115
assume ev: "e = ChangeOwner p u"
+ − 116
show ?thesis
+ − 117
proof (cases "obj = Proc p")
+ − 118
case True
+ − 119
have curp: "p \<in> current_procs s" and exp: "exists s (Proc p)" using os ev by auto
+ − 120
from curp obtain r fr t u' srp where sp: "obj2sobj s (Proc p) = SProc (r,fr,t,u') (Some srp)"
+ − 121
using vs apply (drule_tac current_proc_has_sobj, simp) by blast
+ − 122
hence sp_in: "SProc (r,fr,t,u') (Some srp) \<in> all_sobjs" using prem' exp by metis
+ − 123
have comp: "(r, Proc_type t, CHANGE_OWNER) \<in> compatible" using sp ev rc
+ − 124
by (auto simp:obj2sobj.simps split:option.splits)
+ − 125
from os ev have uinit: "u \<in> init_users" by simp
+ − 126
then obtain nr where chown: "chown_role_aux r fr u = Some nr"
+ − 127
by (auto dest:chown_role_some)
+ − 128
hence nsp_in:"obj2sobj (e#s) (Proc p) = SProc (nr,fr,chown_type_aux r nr t, u) (Some srp)"
+ − 129
using sp ev os
+ − 130
by (auto split:option.splits t_role.splits
+ − 131
simp del:currentrole.simps type_of_process.simps
+ − 132
simp add:chown_role_aux_valid chown_type_aux_valid obj2sobj.simps)
+ − 133
thus ?thesis using True ev os rc sp_in sp
+ − 134
by (auto simp:chown comp intro!:ap_chown[where u'=u'])
+ − 135
next
+ − 136
case False
+ − 137
hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons
+ − 138
by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps
+ − 139
split:option.splits t_role.splits)
+ − 140
thus ?thesis using False prem' ex_cons ev by (case_tac obj, auto)
+ − 141
qed
+ − 142
next
+ − 143
case (Clone p p')
+ − 144
assume ev: "e = Clone p p'"
+ − 145
show ?thesis
+ − 146
proof (cases "obj = Proc p'")
+ − 147
case True
+ − 148
from ev os have exp: "exists s (Proc p)" by (simp add:os_grant.simps)
+ − 149
from exp obtain r fr pt u sp where sproc: "cp2sproc s p = Some (r, fr, pt, u)"
+ − 150
and srp: "source_proc s p = Some sp" using vs
+ − 151
apply (simp del:cp2sproc.simps)
+ − 152
by (frule current_proc_has_sproc, simp, frule current_proc_has_srp, simp, blast)
+ − 153
hence SP: "SProc (r,fr,pt,u) (Some sp) \<in> all_sobjs" using exp prem'[where obj = "Proc p"] vs
+ − 154
by (auto split:option.splits simp add:obj2sobj.simps)
+ − 155
have "obj2sobj (e # s) (Proc p') = SProc (r,fr,clone_type_aux r pt, u) (Some sp)"
+ − 156
using ev sproc srp vs_cons
+ − 157
by (simp add:obj2sobj.simps cp2sproc_clone del:cp2sproc.simps)
+ − 158
thus ?thesis using True SP by (simp add:ap_clone)
+ − 159
next
+ − 160
case False
+ − 161
hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons
+ − 162
by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps
+ − 163
split:option.splits t_role.splits)
+ − 164
thus ?thesis using False prem' ex_cons ev by (case_tac obj, auto)
+ − 165
qed
+ − 166
next
+ − 167
case (Execute p f)
+ − 168
assume ev: "e = Execute p f"
+ − 169
show ?thesis
+ − 170
proof (cases "obj = Proc p")
+ − 171
case True
+ − 172
from ev os have exp: "exists s (Proc p)" and exf: "exists s (File f)" by auto
+ − 173
from exp obtain r fr pt u sp where sproc: "cp2sproc s p = Some (r, fr, pt, u)"
+ − 174
and srp: "source_proc s p = Some sp" using vs
+ − 175
apply (simp del:cp2sproc.simps)
+ − 176
by (frule current_proc_has_sproc, simp, frule current_proc_has_srp, simp, blast)
+ − 177
hence SP: "SProc (r,fr,pt,u) (Some sp) \<in> all_sobjs" using exp prem'[where obj = "Proc p"] vs
+ − 178
by (auto split:option.splits simp add:obj2sobj.simps)
+ − 179
from exf obtain sd t where srdir: "source_dir s f = Some sd" and
+ − 180
etype: "etype_of_file s f = Some t" using vs
+ − 181
by (simp, drule_tac current_file_has_sd, auto dest:current_file_has_etype)
+ − 182
then obtain srf where SF: "SFile (t, sd) srf \<in> all_sobjs"
+ − 183
using exf prem'[where obj = "File f"] vs
+ − 184
by (auto split:option.splits if_splits simp:obj2sobj.simps dest:current_file_has_etype)
+ − 185
from sproc srdir have "u \<in> init_users" and "sd \<in> init_files" using vs
+ − 186
by (auto intro:source_dir_in_init owner_in_users split:option.splits)
+ − 187
then obtain nr where "exec_role_aux r sd u = Some nr" by (auto dest:exec_role_some)
+ − 188
+ − 189
hence "obj2sobj (e # s) (Proc p) \<in> all_sobjs" using ev vs_cons srdir sproc srp
+ − 190
apply (auto simp:obj2sobj.simps cp2sproc_simps source_proc.simps
+ − 191
intro:source_dir_in_init simp del:cp2sproc.simps
+ − 192
split:option.splits dest!:efffrole_sdir_some')
+ − 193
apply (rule ap_exec) using SF SP rc ev etype by (auto split:option.splits)
+ − 194
with True show ?thesis by simp
+ − 195
next
+ − 196
case False
+ − 197
hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons
+ − 198
by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps
+ − 199
split:option.splits t_role.splits)
+ − 200
thus ?thesis using False prem' ex_cons ev by (case_tac obj, auto)
+ − 201
qed
+ − 202
next
+ − 203
case (CreateFile p f)
+ − 204
assume ev: "e = CreateFile p f"
+ − 205
show ?thesis
+ − 206
proof (cases "obj = File f")
+ − 207
case True
+ − 208
from os ev obtain pf where expf: "exists s (File pf)" and parent:"parent f = Some pf" by auto
+ − 209
from expf obtain pft sd srpf where SF: "SFile (pft, sd) srpf \<in> all_sobjs"
+ − 210
and eptype: "etype_of_file s pf = Some pft" and srpf: "source_dir s pf = Some sd"
+ − 211
using prem'[where obj = "File pf"] vs
+ − 212
by (auto split:option.splits if_splits simp:obj2sobj.simps
+ − 213
dest:current_file_has_etype current_file_has_sd)
+ − 214
from os ev have exp: "exists s (Proc p)" by simp
+ − 215
then obtain r pt fr u srp where SP: "SProc (r, fr, pt, u) srp \<in> all_sobjs"
+ − 216
and sproc: "cp2sproc s p = Some (r, fr, pt, u)"
+ − 217
using prem'[where obj = "Proc p"] vs
+ − 218
by (auto split:option.splits if_splits simp:obj2sobj.simps
+ − 219
dest:current_proc_has_sproc)
+ − 220
have "obj2sobj (e # s) (File f) \<in> all_sobjs" using ev vs_cons sproc srpf parent os
+ − 221
apply (auto simp:obj2sobj.simps source_dir_simps init_notin_curf_deleted
+ − 222
split:option.splits dest!:current_file_has_etype')
+ − 223
apply (case_tac "default_fd_create_type r")
+ − 224
using SF SP rc ev eptype sproc
+ − 225
apply (rule_tac sf = srpf in af_cfd', auto simp:etype_of_file_def etype_aux_prop3) [1]
+ − 226
using SF SP rc ev eptype sproc
+ − 227
apply (rule_tac sf = srpf in af_cfd)
+ − 228
apply (auto simp:etype_of_file_def etype_aux_prop4)
+ − 229
done
+ − 230
with True show ?thesis by simp
+ − 231
next
+ − 232
case False
+ − 233
hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs
+ − 234
by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps etype_aux_prop2
+ − 235
split:option.splits t_role.splits )
+ − 236
thus ?thesis using False prem' ex_cons ev by (case_tac obj, auto)
+ − 237
qed
+ − 238
next
+ − 239
case (CreateIPC p i)
+ − 240
assume ev: "e = CreateIPC p i"
+ − 241
show ?thesis
+ − 242
proof (cases "obj = IPC i")
+ − 243
case True
+ − 244
from os ev have exp: "exists s (Proc p)" by simp
+ − 245
then obtain r pt fr u srp where SP: "SProc (r, fr, pt, u) srp \<in> all_sobjs"
+ − 246
and sproc: "cp2sproc s p = Some (r, fr, pt, u)"
+ − 247
using prem'[where obj = "Proc p"] vs
+ − 248
by (auto split:option.splits if_splits simp:obj2sobj.simps
+ − 249
dest:current_proc_has_sproc)
+ − 250
have "obj2sobj (e # s) (IPC i) \<in> all_sobjs" using ev vs_cons sproc os
+ − 251
apply (auto simp:obj2sobj.simps ni_init_deled split:option.splits)
+ − 252
apply (rule ai_cipc) using SP sproc rc ev by auto
+ − 253
with True show ?thesis by simp
+ − 254
next
+ − 255
case False
+ − 256
hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs
+ − 257
by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps
+ − 258
split:option.splits t_role.splits )
+ − 259
thus ?thesis using False prem' ex_cons ev by (case_tac obj, auto)
+ − 260
qed
+ − 261
next
+ − 262
case (ChangeRole p r')
+ − 263
assume ev: "e = ChangeRole p r'"
+ − 264
show ?thesis
+ − 265
proof (cases "obj = Proc p")
+ − 266
case True
+ − 267
from os ev have exp: "exists s (Proc p)" by simp
+ − 268
then obtain r pt fr u srp where SP: "SProc (r, fr, pt, u) srp \<in> all_sobjs"
+ − 269
and sproc: "cp2sproc s p = Some (r, fr, pt, u)" and srproc: "source_proc s p = srp"
+ − 270
using prem'[where obj = "Proc p"] vs
+ − 271
by (auto split:option.splits if_splits simp:obj2sobj.simps
+ − 272
dest:current_proc_has_sproc)
+ − 273
have "obj2sobj (e # s) (Proc p) \<in> all_sobjs" using ev vs_cons sproc os
+ − 274
apply (auto simp:obj2sobj.simps ni_init_deled split:option.splits)
+ − 275
apply (rule ap_crole) using SP sproc rc ev srproc by auto
+ − 276
with True show ?thesis by simp
+ − 277
next
+ − 278
case False
+ − 279
hence "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs
+ − 280
by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps
+ − 281
split:option.splits t_role.splits )
+ − 282
thus ?thesis using False prem' ex_cons ev by (case_tac obj, auto)
+ − 283
qed
+ − 284
next
+ − 285
case (ReadFile p f)
+ − 286
assume ev: "e = ReadFile p f"
+ − 287
have "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs
+ − 288
by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps
+ − 289
split:option.splits t_role.splits)
+ − 290
moreover have "exists s obj" using ev ex_cons
+ − 291
by (case_tac obj, auto)
+ − 292
ultimately show ?thesis using prem[where obj = obj] vs by simp
+ − 293
next
+ − 294
case (WriteFile p f)
+ − 295
assume ev: "e = WriteFile p f"
+ − 296
have "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs
+ − 297
by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps
+ − 298
split:option.splits t_role.splits)
+ − 299
moreover have "exists s obj" using ev ex_cons
+ − 300
by (case_tac obj, auto)
+ − 301
ultimately show ?thesis using prem[where obj = obj] vs by simp
+ − 302
next
+ − 303
case (Send p i)
+ − 304
assume ev: "e = Send p i"
+ − 305
have "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs
+ − 306
by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps
+ − 307
split:option.splits t_role.splits)
+ − 308
moreover have "exists s obj" using ev ex_cons
+ − 309
by (case_tac obj, auto)
+ − 310
ultimately show ?thesis using prem[where obj = obj] vs by simp
+ − 311
next
+ − 312
case (Recv p i)
+ − 313
assume ev: "e = Recv p i"
+ − 314
have "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs
+ − 315
by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps
+ − 316
split:option.splits t_role.splits)
+ − 317
moreover have "exists s obj" using ev ex_cons
+ − 318
by (case_tac obj, auto)
+ − 319
ultimately show ?thesis using prem[where obj = obj] vs by simp
+ − 320
next
+ − 321
case (Kill p p')
+ − 322
assume ev: "e = Kill p p'"
+ − 323
have "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs
+ − 324
by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps
+ − 325
split:option.splits t_role.splits)
+ − 326
thus ?thesis using prem[where obj = obj] vs ex_cons ev
+ − 327
by (case_tac obj, auto)
+ − 328
next
+ − 329
case (DeleteFile p f')
+ − 330
assume ev: "e = DeleteFile p f'"
+ − 331
have "obj2sobj (e#s) obj = obj2sobj s obj"
+ − 332
proof-
+ − 333
have "\<And> f. obj = File f ==> obj2sobj (e#s) (File f) = obj2sobj s (File f)"
+ − 334
using ev vs os ex_cons vs_cons
+ − 335
by (auto simp:obj2sobj.simps etype_of_file_delete source_dir_simps
+ − 336
split:option.splits t_role.splits if_splits
+ − 337
dest!:current_file_has_etype' current_file_has_sd'
+ − 338
dest:source_dir_prop)
+ − 339
moreover have "\<forall> f. obj \<noteq> File f ==> obj2sobj (e#s) obj = obj2sobj s obj"
+ − 340
using ev vs_cons ex_cons os vs
+ − 341
by (case_tac obj, auto simp:obj2sobj.simps split:option.splits)
+ − 342
ultimately show ?thesis by auto
+ − 343
qed
+ − 344
thus ?thesis using prem[where obj = obj] vs ex_cons ev
+ − 345
by (case_tac obj, auto)
+ − 346
next
+ − 347
case (DeleteIPC p i)
+ − 348
assume ev: "e = DeleteIPC p i"
+ − 349
have "obj2sobj (e#s) obj = obj2sobj s obj" using ev vs_cons ex_cons os vs
+ − 350
by (case_tac obj, auto simp:obj2sobj.simps etype_of_file_def source_dir_simps
+ − 351
split:option.splits t_role.splits)
+ − 352
thus ?thesis using prem[where obj = obj] vs ex_cons ev
+ − 353
by (case_tac obj, auto)
+ − 354
qed
+ − 355
qed
+ − 356
+ − 357
declare obj2sobj.simps [simp add]
+ − 358
+ − 359
lemma seeds_in_all_sobjs:
+ − 360
assumes seed: "obj \<in> seeds" shows "init_obj2sobj obj \<in> all_sobjs"
+ − 361
proof (cases obj)
+ − 362
case (Proc p)
+ − 363
assume p0: "obj = Proc p" (*?*)
+ − 364
from seed p0 have pinit: "p \<in> init_processes" by (drule_tac seeds_in_init, simp)
+ − 365
from pinit obtain r where "init_currentrole p = Some r"
+ − 366
using init_proc_has_role by (auto simp:bidirect_in_init_def)
+ − 367
moreover from pinit obtain fr where "init_proc_forcedrole p = Some fr"
+ − 368
using init_proc_has_frole by (auto simp:bidirect_in_init_def)
+ − 369
moreover from pinit obtain pt where "init_process_type p = Some pt"
+ − 370
using init_proc_has_type by (auto simp:bidirect_in_init_def)
+ − 371
moreover from pinit obtain u where "init_owner p = Some u"
+ − 372
using init_proc_has_owner by (auto simp:bidirect_in_init_def)
+ − 373
ultimately show ?thesis using p0 by (auto intro:ap_init)
+ − 374
next
+ − 375
case (File f)
+ − 376
assume p0: "obj = File f" (*?*)
+ − 377
from seed p0 have finit: "f \<in> init_files" by (drule_tac seeds_in_init, simp)
+ − 378
then obtain t where "etype_aux init_file_type_aux f = Some t"
+ − 379
by (auto dest:init_file_has_etype)
+ − 380
with finit p0 show ?thesis by (auto intro:af_init)
+ − 381
next
+ − 382
case (IPC i)
+ − 383
assume p0: "obj = IPC i" (*?*)
+ − 384
from seed p0 have iinit: "i \<in> init_ipcs" by (drule_tac seeds_in_init, simp)
+ − 385
then obtain t where "init_ipc_type i = Some t" using init_ipc_has_type
+ − 386
by (auto simp:bidirect_in_init_def)
+ − 387
with iinit p0 show ?thesis by (auto intro:ai_init)
+ − 388
qed
+ − 389
+ − 390
lemma tainted_s_in_all_sobjs:
+ − 391
"sobj \<in> tainted_s \<Longrightarrow> sobj \<in> all_sobjs"
+ − 392
apply (erule tainted_s.induct)
+ − 393
apply (erule seeds_in_all_sobjs)
+ − 394
apply (auto intro:ap_crole ap_exec ap_chown ai_cipc af_cfd af_cfd' ap_clone)
+ − 395
done
+ − 396
+ − 397
end
+ − 398
+ − 399
context tainting_s_sound begin
+ − 400
+ − 401
(*** all_sobjs' equal with all_sobjs in the view of soundness ***)
+ − 402
+ − 403
lemma all_sobjs'_eq1: "sobj \<in> all_sobjs \<Longrightarrow> sobj \<in> all_sobjs'"
+ − 404
apply (erule all_sobjs.induct)
+ − 405
apply (auto intro:af'_init af'_cfd af'_cfd' ai'_init ai'_cipc ap'_init ap'_crole ap'_exec ap'_chown)
+ − 406
by (simp add:clone_type_aux_def clone_type_unchange)
+ − 407
+ − 408
lemma all_sobjs'_eq2: "sobj \<in> all_sobjs' \<Longrightarrow> sobj \<in> all_sobjs"
+ − 409
apply (erule all_sobjs'.induct)
+ − 410
by (auto intro:af_init af_cfd af_cfd' ai_init ai_cipc ap_init ap_crole ap_exec ap_chown)
+ − 411
+ − 412
lemma all_sobjs'_eq: "(sobj \<in> all_sobjs) = (sobj \<in> all_sobjs')"
+ − 413
by (auto intro:iffI all_sobjs'_eq1 all_sobjs'_eq2)
+ − 414
+ − 415
(************************ all_sobjs Elim Rules ********************)
+ − 416
+ − 417
declare obj2sobj.simps [simp del]
+ − 418
declare cp2sproc.simps [simp del]
+ − 419
+ − 420
lemma all_sobjs_E0_aux[rule_format]:
+ − 421
"sobj \<in> all_sobjs' \<Longrightarrow> (\<forall> s' obj' sobj'. valid s' \<and> obj2sobj s' obj' = sobj' \<and> exists s' obj' \<and> sobj' \<noteq> Unknown \<and> no_del_event s' \<and> initp_intact s' \<longrightarrow> (\<exists> s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and> obj2sobj (s @ s') obj = sobj \<and> exists (s @ s') obj))"
+ − 422
proof (induct rule:all_sobjs'.induct)
+ − 423
case (af'_init f t) show ?case
+ − 424
proof (rule allI|rule impI|erule conjE)+
+ − 425
fix s' obj' sobj'
+ − 426
assume vss': "valid s'" and sobjs': "obj2sobj s' obj' = sobj'"
+ − 427
and nodels': "no_del_event s'"and intacts':"initp_intact s'"
+ − 428
and exso': "exists s' obj'"
+ − 429
from nodels' af'_init(1) have exf: "f \<in> current_files s'"
+ − 430
by (drule_tac obj = "File f" in nodel_imp_exists, simp+)
+ − 431
have "obj2sobj s' (File f) = SFile (t, f) (Some f)"
+ − 432
proof-
+ − 433
have "obj2sobj [] (File f) = SFile (t, f) (Some f)" using af'_init
+ − 434
by (auto simp:etype_of_file_def source_dir_of_init' obj2sobj.simps
+ − 435
split:option.splits)
+ − 436
thus ?thesis using vss' exf nodels' af'_init(1)
+ − 437
by (drule_tac obj2sobj_file_remains_app', auto)
+ − 438
qed
+ − 439
thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 440
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and>
+ − 441
obj2sobj (s @ s') obj = SFile (t, f) (Some f) \<and> exists (s @ s') obj"
+ − 442
apply (rule_tac x = "[]" in exI, rule_tac x = "File f" in exI)
+ − 443
by (simp add:vss' sobjs' nodels' intacts' exf exso')
+ − 444
qed
+ − 445
next
+ − 446
case (af'_cfd t sd srf r fr pt u srp t')
+ − 447
show ?case
+ − 448
proof (rule allI|rule impI|erule conjE)+
+ − 449
fix s' obj' sobj'
+ − 450
assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'"
+ − 451
and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and exobj':"exists s' obj'"
+ − 452
with af'_cfd(1,2) obtain sa pf where
+ − 453
"valid (sa@s')" and "obj2sobj (sa@s') obj'=sobj' \<and> no_del_event (sa@s')" and
+ − 454
"exists (sa@s') obj'" and "initp_intact (sa@s')" and
+ − 455
SFa: "obj2sobj (sa@s') (File pf) = SFile (t, sd) srf" and
+ − 456
exfa: "pf \<in> current_files (sa@s')"
+ − 457
apply (erule_tac x = s' in allE, erule_tac x = obj' in allE, auto)
+ − 458
by (frule obj2sobj_file, auto)
+ − 459
with af'_cfd(3,4) notUkn obtain sb p where
+ − 460
SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) srp" and
+ − 461
expab: "exists (sb@sa@s') (Proc p)" and vsab: "valid (sb@sa@s')" and
+ − 462
soab: "obj2sobj (sb@sa@s') obj' = sobj'" and
+ − 463
exsoab: "exists (sb@sa@s') obj'" and
+ − 464
intactab: "initp_intact (sb@sa@s')" and
+ − 465
nodelab: "no_del_event (sb@sa@s')"
+ − 466
by (blast dest:obj2sobj_proc intro:nodel_exists_remains)
+ − 467
from exfa nodelab have exf:"pf \<in> current_files (sb@sa@s')"
+ − 468
apply (drule_tac obj = "File pf" in nodel_imp_un_deleted)
+ − 469
by (drule_tac s' = "sb" in not_deleted_imp_exists', auto)
+ − 470
from SFa vsab exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File pf) = SFile (t,sd) srf"
+ − 471
by (rule_tac s = "sa@s'" in obj2sobj_file_remains_app', simp_all)
+ − 472
obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)"
+ − 473
and tau: "\<tau>=sb@sa@s'" by auto
+ − 474
+ − 475
have valid: "valid (e # \<tau>)"
+ − 476
proof-
+ − 477
have "os_grant \<tau> e"
+ − 478
using ev tau expab exf by (simp add:ncf_notin_curf ncf_parent)
+ − 479
moreover have "rc_grant \<tau> e"
+ − 480
using ev tau af'_cfd(5,6,7) SPab SFab
+ − 481
by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps
+ − 482
split:if_splits option.splits t_rc_file_type.splits)
+ − 483
ultimately show ?thesis using vsab tau
+ − 484
by (rule_tac vs_step, simp+)
+ − 485
qed moreover
+ − 486
have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover
+ − 487
have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau
+ − 488
by (case_tac obj', simp+) moreover
+ − 489
have "obj2sobj (e#\<tau>) obj' = sobj'"
+ − 490
proof-
+ − 491
have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 492
using soab tau valid notUkn nodel ev exsoab
+ − 493
by (auto intro!:obj2sobj_file_remains' simp:ncf_notin_curf)
+ − 494
moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 495
using soab tau valid notUkn nodel ev exsoab
+ − 496
by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf)
+ − 497
moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 498
using soab tau valid notUkn nodel ev exsoab
+ − 499
by (auto simp:obj2sobj.simps cp2sproc_simps
+ − 500
simp del:cp2sproc.simps split:option.splits)
+ − 501
ultimately show ?thesis by (case_tac obj', auto)
+ − 502
qed moreover
+ − 503
have "initp_intact (e#\<tau>)" using intactab tau ev valid nodel
+ − 504
by (simp_all add:initp_intact_I_others) moreover
+ − 505
have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t', sd) None"
+ − 506
proof-
+ − 507
have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t'"
+ − 508
using ev tau SFab SPab af'_cfd(5)
+ − 509
by (auto simp:obj2sobj.simps cp2sproc.simps etype_of_file_def
+ − 510
split:option.splits if_splits intro!:etype_aux_prop4)
+ − 511
moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd"
+ − 512
using ev tau SFab SPab valid ncf_parent
+ − 513
by (auto simp:source_dir_simps obj2sobj.simps
+ − 514
split:if_splits option.splits)
+ − 515
ultimately show ?thesis using nodel ncf_notin_curf[where s = \<tau>]
+ − 516
nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>]
+ − 517
by (auto simp:obj2sobj.simps dest:no_del_event_cons_D)
+ − 518
qed
+ − 519
ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 520
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and>
+ − 521
obj2sobj (s @ s') obj = SFile (t', sd) None \<and> exists (s @ s') obj "
+ − 522
using tau ev
+ − 523
by (rule_tac x = "e#sb@sa" in exI, rule_tac x = "File (new_childf pf \<tau>)" in exI, simp+)
+ − 524
qed
+ − 525
next
+ − 526
case (af'_cfd' t sd srf r fr pt u srp)
+ − 527
show ?case
+ − 528
proof (rule allI|rule impI|erule conjE)+
+ − 529
fix s' obj' sobj'
+ − 530
assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'"
+ − 531
and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and exobj':"exists s' obj'"
+ − 532
with af'_cfd'(1,2) obtain sa pf where
+ − 533
"valid (sa@s')" and "obj2sobj (sa@s') obj'=sobj' \<and> no_del_event (sa@s')" and
+ − 534
"exists (sa@s') obj'" and "initp_intact (sa@s')" and
+ − 535
SFa: "obj2sobj (sa@s') (File pf) = SFile (t, sd) srf" and
+ − 536
exfa: "pf \<in> current_files (sa@s')"
+ − 537
apply (erule_tac x = s' in allE, erule_tac x = obj' in allE, auto)
+ − 538
by (frule obj2sobj_file, auto)
+ − 539
with af'_cfd'(3,4) notUkn obtain sb p where
+ − 540
SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) srp" and
+ − 541
expab: "exists (sb@sa@s') (Proc p)" and vsab: "valid (sb@sa@s')" and
+ − 542
soab: "obj2sobj (sb@sa@s') obj' = sobj'" and
+ − 543
exsoab: "exists (sb@sa@s') obj'" and
+ − 544
intactab: "initp_intact (sb@sa@s')" and
+ − 545
nodelab: "no_del_event (sb@sa@s')"
+ − 546
by (blast dest:obj2sobj_proc intro:nodel_exists_remains)
+ − 547
from exfa nodelab have exf:"pf \<in> current_files (sb@sa@s')"
+ − 548
apply (drule_tac obj = "File pf" in nodel_imp_un_deleted)
+ − 549
by (drule_tac s' = "sb" in not_deleted_imp_exists', auto)
+ − 550
from SFa vsab exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File pf) = SFile (t,sd) srf"
+ − 551
by (rule_tac s = "sa@s'" in obj2sobj_file_remains_app', simp_all)
+ − 552
obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)"
+ − 553
and tau: "\<tau>=sb@sa@s'" by auto
+ − 554
+ − 555
have valid: "valid (e # \<tau>)"
+ − 556
proof-
+ − 557
have "os_grant \<tau> e"
+ − 558
using ev tau expab exf by (simp add:ncf_notin_curf ncf_parent)
+ − 559
moreover have "rc_grant \<tau> e"
+ − 560
using ev tau af'_cfd'(5,6) SPab SFab
+ − 561
by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps
+ − 562
split:if_splits option.splits t_rc_file_type.splits)
+ − 563
ultimately show ?thesis using vsab tau
+ − 564
by (rule_tac vs_step, simp+)
+ − 565
qed moreover
+ − 566
have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover
+ − 567
have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau
+ − 568
by (case_tac obj', simp+) moreover
+ − 569
have "obj2sobj (e#\<tau>) obj' = sobj'"
+ − 570
proof-
+ − 571
have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 572
using soab tau valid notUkn nodel ev exsoab
+ − 573
by (auto intro!:obj2sobj_file_remains' simp:ncf_notin_curf)
+ − 574
moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 575
using soab tau valid notUkn nodel ev exsoab
+ − 576
by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf)
+ − 577
moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 578
using soab tau valid notUkn nodel ev exsoab
+ − 579
by (auto simp:obj2sobj.simps cp2sproc_simps
+ − 580
simp del:cp2sproc.simps split:option.splits)
+ − 581
ultimately show ?thesis by (case_tac obj', auto)
+ − 582
qed moreover
+ − 583
have "initp_intact (e#\<tau>)" using intactab tau ev valid nodel
+ − 584
by (simp add:initp_intact_I_others) moreover
+ − 585
have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t, sd) None"
+ − 586
proof-
+ − 587
have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t"
+ − 588
proof-
+ − 589
have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = etype_of_file \<tau> pf"
+ − 590
using ev tau SPab af'_cfd'(5)
+ − 591
by (auto simp:obj2sobj.simps ncf_parent etype_of_file_def cp2sproc.simps
+ − 592
split:option.splits intro!:etype_aux_prop3)
+ − 593
thus ?thesis using SFab tau ev
+ − 594
by (auto simp:obj2sobj.simps split:option.splits if_splits)
+ − 595
qed
+ − 596
moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd"
+ − 597
using ev tau SFab SPab valid ncf_parent
+ − 598
by (auto simp:source_dir_simps obj2sobj.simps
+ − 599
split:if_splits option.splits)
+ − 600
ultimately show ?thesis using nodel ncf_notin_curf[where s = \<tau>]
+ − 601
nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>]
+ − 602
by (auto simp:obj2sobj.simps dest:no_del_event_cons_D)
+ − 603
qed
+ − 604
ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 605
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and>
+ − 606
obj2sobj (s @ s') obj = SFile (t, sd) None \<and> exists (s @ s') obj"
+ − 607
using tau ev
+ − 608
by (rule_tac x = "e#sb@sa" in exI, rule_tac x = "File (new_childf pf \<tau>)" in exI, simp+)
+ − 609
qed
+ − 610
next
+ − 611
case (ai'_init i t)
+ − 612
hence initi: "i \<in> init_ipcs" using init_ipc_has_type
+ − 613
by (simp add:bidirect_in_init_def)
+ − 614
show ?case
+ − 615
proof (rule allI|rule impI|erule conjE)+
+ − 616
fix s' obj' sobj'
+ − 617
assume vss': "valid s'" and sobjs': "obj2sobj s' obj' = sobj'"
+ − 618
and nodels': "no_del_event s'"and intacts':"initp_intact s'"
+ − 619
and exso': "exists s' obj'"
+ − 620
from nodels' initi have exi: "i \<in> current_ipcs s'"
+ − 621
by (drule_tac obj = "IPC i" in nodel_imp_exists, simp+)
+ − 622
have "obj2sobj s' (IPC i) = SIPC t (Some i)"
+ − 623
proof-
+ − 624
have "obj2sobj [] (IPC i) = SIPC t (Some i)"
+ − 625
using ai'_init initi by (auto simp:obj2sobj.simps)
+ − 626
thus ?thesis using vss' exi nodels' initi
+ − 627
by (drule_tac obj2sobj_ipc_remains'', auto simp:obj2sobj.simps)
+ − 628
qed
+ − 629
thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 630
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and>
+ − 631
obj2sobj (s @ s') obj = SIPC t (Some i) \<and> exists (s @ s') obj"
+ − 632
apply (rule_tac x = "[]" in exI, rule_tac x = "IPC i" in exI)
+ − 633
by (simp add:vss' sobjs' nodels' exi exso' intacts' del:obj2sobj.simps)
+ − 634
qed
+ − 635
next
+ − 636
case (ai'_cipc r fr pt u srp)
+ − 637
show ?case
+ − 638
proof (rule allI|rule impI|erule conjE)+
+ − 639
fix s' obj' sobj'
+ − 640
assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'"
+ − 641
and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and exobj':"exists s' obj'"
+ − 642
with ai'_cipc(1,2) notUkn obtain s p where
+ − 643
SPab: "obj2sobj (s@s') (Proc p) = SProc (r,fr,pt,u) srp" and
+ − 644
expab: "exists (s@s') (Proc p)" and vsab: "valid (s@s')" and
+ − 645
soab: "obj2sobj (s@s') obj' = sobj'" and
+ − 646
exsoab: "exists (s@s') obj'" and
+ − 647
intactab: "initp_intact (s@s')" and
+ − 648
nodelab: "no_del_event (s@s')"
+ − 649
by (blast dest:obj2sobj_proc intro:nodel_exists_remains)
+ − 650
obtain e \<tau> where ev: "e = CreateIPC p (new_ipc \<tau>)" and tau: "\<tau>=s@s'" by auto
+ − 651
+ − 652
have valid: "valid (e # \<tau>)"
+ − 653
proof-
+ − 654
have "os_grant \<tau> e"
+ − 655
using ev tau expab by (simp)
+ − 656
moreover have "rc_grant \<tau> e"
+ − 657
using ev tau ai'_cipc(3) SPab
+ − 658
by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
+ − 659
ultimately show ?thesis using vsab tau
+ − 660
by (rule_tac vs_step, simp+)
+ − 661
qed moreover
+ − 662
have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover
+ − 663
have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau
+ − 664
by (case_tac obj', simp+) moreover
+ − 665
have "obj2sobj (e#\<tau>) obj' = sobj'"
+ − 666
proof-
+ − 667
have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 668
using soab tau valid notUkn nodel ev exsoab
+ − 669
by (auto intro!:obj2sobj_file_remains' simp:ncf_notin_curf)
+ − 670
moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 671
using soab tau valid notUkn nodel ev exsoab
+ − 672
by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf)
+ − 673
moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 674
using soab tau valid notUkn nodel ev exsoab
+ − 675
by (auto simp:obj2sobj.simps cp2sproc_simps
+ − 676
simp del:cp2sproc.simps split:option.splits)
+ − 677
ultimately show ?thesis by (case_tac obj', auto)
+ − 678
qed moreover
+ − 679
have "initp_intact (e#\<tau>)" using intactab tau ev valid nodel
+ − 680
by (simp add:initp_intact_I_others) moreover
+ − 681
have "obj2sobj (e#\<tau>) (IPC (new_ipc \<tau>)) = SIPC (default_ipc_create_type r) None"
+ − 682
using ev tau SPab nodel
+ − 683
nodel_imp_exists[where obj = "IPC (new_ipc \<tau>)" and s =\<tau>]
+ − 684
by (auto simp:obj2sobj.simps ni_notin_curi cp2sproc.simps
+ − 685
split:option.splits dest:no_del_event_cons_D)
+ − 686
ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 687
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and>
+ − 688
obj2sobj (s @ s') obj = SIPC (default_ipc_create_type r) None \<and> exists (s @ s') obj"
+ − 689
using tau ev
+ − 690
by (rule_tac x = "e#s" in exI, rule_tac x = "IPC (new_ipc \<tau>)" in exI, simp+)
+ − 691
qed
+ − 692
next
+ − 693
case (ap'_init p r fr t u)
+ − 694
hence initp: "p \<in> init_processes" using init_proc_has_role
+ − 695
by (simp add:bidirect_in_init_def)
+ − 696
show ?case
+ − 697
proof (rule allI|rule impI|erule conjE)+
+ − 698
fix s' obj' sobj'
+ − 699
assume VSs': "valid s'" and SOs': "obj2sobj s' obj' = sobj'"
+ − 700
and Nodels': "no_del_event s'"and Intacts':"initp_intact s'"
+ − 701
and exso': "exists s' obj'"
+ − 702
from Nodels' initp have exp: "p \<in> current_procs s'"
+ − 703
apply (drule_tac obj = "Proc p" in nodel_imp_un_deleted)
+ − 704
by (drule not_deleted_imp_exists, simp+)
+ − 705
with Intacts' initp ap'_init have "obj2sobj s' (Proc p) = SProc (r, fr, t, u) (Some p)"
+ − 706
by (auto simp:initp_intact_def split:option.splits)
+ − 707
thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 708
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and>
+ − 709
obj2sobj (s @ s') obj = SProc (r, fr, t, u) (Some p) \<and> exists (s @ s') obj"
+ − 710
apply (rule_tac x = "[]" in exI, rule_tac x = "Proc p" in exI)
+ − 711
by (simp add:VSs' SOs' Nodels' exp exso' initp intact_imp_butp Intacts'
+ − 712
del:obj2sobj.simps)
+ − 713
qed
+ − 714
next
+ − 715
case (ap'_crole r fr t u srp r')
+ − 716
show ?case
+ − 717
proof (rule allI|rule impI|erule conjE)+
+ − 718
fix s' obj' sobj'
+ − 719
assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'"
+ − 720
and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'"
+ − 721
with ap'_crole(1,2) obtain s p where
+ − 722
VSab: "valid (s@s')" and SOab': "obj2sobj (s@s') obj' = sobj'"
+ − 723
and nodelab: "no_del_event (s@s')"
+ − 724
and intactab: "initp_intact (s@s')"
+ − 725
and SPab: "obj2sobj (s@s') (Proc p) = SProc (r, fr, t, u) srp"
+ − 726
and exp:"exists (s@s') (Proc p)" and exobj'ab:"exists (s@s') obj'"
+ − 727
by (blast dest:obj2sobj_proc intro:nodel_exists_remains)
+ − 728
obtain e \<tau> where ev: "e = ChangeRole (new_proc (s@s')) r'"
+ − 729
and tau: "\<tau> = Clone p (new_proc (s@s'))#s@s'" by auto
+ − 730
hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit)
+ − 731
+ − 732
have valid: "valid (e#\<tau>)"
+ − 733
proof-
+ − 734
have "os_grant \<tau> e"
+ − 735
using ev tau exp by (simp)
+ − 736
moreover have "rc_grant \<tau> e"
+ − 737
using ev tau ap'_crole(3) SPab
+ − 738
by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
+ − 739
ultimately show ?thesis using vs_tau
+ − 740
by (erule_tac vs_step, simp+)
+ − 741
qed moreover
+ − 742
have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover
+ − 743
have "initp_intact (e#\<tau>)" using tau ev intactab valid
+ − 744
by (simp add:initp_intact_I_crole) moreover
+ − 745
have exobj': "exists (e#\<tau>) obj'" using exobj'ab valid ev tau
+ − 746
by (case_tac obj', simp+) moreover
+ − 747
have "obj2sobj (e#\<tau>) obj' = sobj'"
+ − 748
proof-
+ − 749
have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 750
using SOab' tau ev valid notUkn nodel exobj'
+ − 751
obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]
+ − 752
by (auto)
+ − 753
moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 754
using SOab' tau ev valid notUkn nodel exobj'
+ − 755
obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]
+ − 756
by auto
+ − 757
moreover have "\<And> p'. obj' = Proc p' \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 758
apply (case_tac "p' = new_proc (s @ s')")
+ − 759
using vs_tau exobj'ab tau
+ − 760
apply (simp, drule_tac valid_os, simp add:np_notin_curp)
+ − 761
using tau ev SOab' valid notUkn vs_tau
+ − 762
by (auto simp:obj2sobj.simps cp2sproc_simps split:option.splits)
+ − 763
ultimately show ?thesis by (case_tac obj', auto)
+ − 764
qed moreover
+ − 765
have "obj2sobj (e#\<tau>) (Proc (new_proc (s@s'))) = SProc (r', fr, t, u) srp"
+ − 766
using SPab tau vs_tau ev valid
+ − 767
by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:cp2sproc.simps
+ − 768
split:option.splits) moreover
+ − 769
have "exists (e#\<tau>) (Proc p)" using exp tau ev by simp
+ − 770
ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 771
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and>
+ − 772
obj2sobj (s @ s') obj = SProc (r', fr, t, u) srp \<and> exists (s @ s') obj"
+ − 773
using ev tau
+ − 774
apply (rule_tac x = "e # Clone p (new_proc (s @ s')) # s" in exI)
+ − 775
by (rule_tac x = "Proc (new_proc (s@s'))" in exI, auto)
+ − 776
qed
+ − 777
next
+ − 778
case (ap'_chown r fr t u srp u' nr)
+ − 779
show ?case
+ − 780
proof (rule allI|rule impI|erule conjE)+
+ − 781
fix s' obj' sobj'
+ − 782
assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'"
+ − 783
and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'"
+ − 784
with ap'_chown(1,2) obtain s p where
+ − 785
VSab: "valid (s@s')" and SOab': "obj2sobj (s@s') obj' = sobj'"
+ − 786
and nodelab: "no_del_event (s@s')" and intactab: "initp_intact (s@s')"
+ − 787
and SPab: "obj2sobj (s@s') (Proc p) = SProc (r, fr, t, u) srp"
+ − 788
and exp:"exists (s@s') (Proc p)" and exobj'ab:"exists (s@s') obj'"
+ − 789
by (blast dest:obj2sobj_proc intro:nodel_exists_remains)
+ − 790
obtain e \<tau> where ev: "e = ChangeOwner (new_proc (s@s')) u'"
+ − 791
and tau: "\<tau> = Clone p (new_proc (s@s'))#s@s'" by auto
+ − 792
hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit)
+ − 793
+ − 794
have valid: "valid (e#\<tau>)"
+ − 795
proof-
+ − 796
have "os_grant \<tau> e"
+ − 797
using ev tau exp ap'_chown(3) by (simp)
+ − 798
moreover have "rc_grant \<tau> e"
+ − 799
using ev tau ap'_chown(5) SPab
+ − 800
by (auto simp:cp2sproc.simps obj2sobj.simps pct_def clone_type_unchange
+ − 801
split:option.splits t_rc_proc_type.splits)
+ − 802
(* here is another place of no_limit of clone event assumption *)
+ − 803
ultimately show ?thesis using vs_tau
+ − 804
by (erule_tac vs_step, simp+)
+ − 805
qed moreover
+ − 806
have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover
+ − 807
have "initp_intact (e#\<tau>)" using intactab tau ev valid
+ − 808
by (simp add:initp_intact_I_chown) moreover
+ − 809
have exobj': "exists (e#\<tau>) obj'" using exobj'ab valid ev tau
+ − 810
by (case_tac obj', simp+) moreover
+ − 811
have "obj2sobj (e#\<tau>) obj' = sobj'"
+ − 812
proof-
+ − 813
have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 814
using SOab' tau ev valid notUkn nodel exobj'
+ − 815
obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]
+ − 816
by (auto)
+ − 817
moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 818
using SOab' tau ev valid notUkn nodel exobj'
+ − 819
obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]
+ − 820
by auto
+ − 821
moreover have "\<And> p'. obj' = Proc p' \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 822
apply (case_tac "p' = new_proc (s @ s')")
+ − 823
using vs_tau exobj'ab tau
+ − 824
apply (simp, drule_tac valid_os, simp add:np_notin_curp)
+ − 825
using tau ev SOab' valid notUkn vs_tau
+ − 826
by (auto simp:obj2sobj.simps cp2sproc_simps' split:option.splits)
+ − 827
ultimately show ?thesis by (case_tac obj', auto)
+ − 828
qed moreover
+ − 829
have "obj2sobj (e#\<tau>) (Proc (new_proc (s@s'))) =
+ − 830
SProc (nr,fr,chown_type_aux r nr t,u') srp"
+ − 831
using SPab tau vs_tau ev valid ap'_chown(4)
+ − 832
by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:cp2sproc.simps
+ − 833
split:option.splits) moreover
+ − 834
have "exists (e#\<tau>) (Proc p)" using exp tau ev by simp moreover
+ − 835
ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 836
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and>
+ − 837
obj2sobj (s @ s') obj = SProc (nr,fr,chown_type_aux r nr t,u') srp \<and>
+ − 838
exists (s @ s') obj"
+ − 839
using ev tau
+ − 840
apply (rule_tac x = "e # Clone p (new_proc (s @ s')) # s" in exI)
+ − 841
by (rule_tac x = "Proc (new_proc (s@s'))" in exI, auto)
+ − 842
qed
+ − 843
next
+ − 844
case (ap'_exec r fr pt u sp t sd sf r' fr')
+ − 845
show ?case
+ − 846
proof (rule allI|rule impI|erule conjE)+
+ − 847
fix s' obj' sobj'
+ − 848
assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'"
+ − 849
and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'"
+ − 850
with ap'_exec(3,4) obtain sa f where
+ − 851
SFa: "obj2sobj (sa @ s') (File f) = SFile (t, sd) sf" and
+ − 852
Exfa: "exists (sa @ s') (File f)" and
+ − 853
butsa: "initp_intact (sa @ s')" and
+ − 854
othersa:"valid (sa @ s') \<and> obj2sobj (sa @ s') obj' = sobj' \<and>
+ − 855
exists (sa @s') obj' \<and> no_del_event (sa @ s')"
+ − 856
by (blast dest:obj2sobj_file intro:nodel_exists_remains)
+ − 857
with ap'_exec(1,2) notUkn obtain sb p where
+ − 858
VSab: "valid (sb@sa@s')" and SOab': "obj2sobj (sb@sa@s') obj' = sobj'"
+ − 859
and nodelab: "no_del_event (sb@sa@s')"
+ − 860
and intactab: "initp_intact (sb@sa@s')"
+ − 861
and SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r, fr, pt, u) sp"
+ − 862
and exp:"exists (sb@sa@s') (Proc p)" and exobj'ab:"exists (sb@sa@s') obj'"
+ − 863
by (blast dest:obj2sobj_proc intro:nodel_exists_remains)
+ − 864
obtain e \<tau> where ev: "e = Execute (new_proc (sb@sa@s')) f"
+ − 865
and tau: "\<tau> = Clone p (new_proc (sb@sa@s'))#sb@sa@s'" by auto
+ − 866
hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit)
+ − 867
from Exfa nodelab have exf:"f \<in> current_files (sb@sa@s')"
+ − 868
apply (drule_tac obj = "File f" in nodel_imp_un_deleted)
+ − 869
by (drule_tac s' = "sb" in not_deleted_imp_exists', auto)
+ − 870
from SFa VSab Exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File f) = SFile (t,sd) sf"
+ − 871
by (rule_tac s = "sa@s'" in obj2sobj_file_remains'', simp_all)
+ − 872
+ − 873
have valid: "valid (e#\<tau>)"
+ − 874
proof-
+ − 875
have "os_grant \<tau> e"
+ − 876
using ev tau exp by (simp add:exf)
+ − 877
moreover have "rc_grant \<tau> e"
+ − 878
using ev tau ap'_exec(5) SPab SFab
+ − 879
by (auto simp:etype_of_file_def cp2sproc.simps obj2sobj.simps
+ − 880
split:if_splits option.splits)
+ − 881
ultimately show ?thesis using vs_tau
+ − 882
by (erule_tac vs_step, simp+)
+ − 883
qed moreover
+ − 884
have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover
+ − 885
have "initp_intact (e#\<tau>)" using tau ev intactab valid
+ − 886
by (simp add:initp_intact_I_exec) moreover
+ − 887
have exobj': "exists (e#\<tau>) obj'" using exobj'ab valid ev tau
+ − 888
by (case_tac obj', simp+) moreover
+ − 889
have "obj2sobj (e#\<tau>) obj' = sobj'"
+ − 890
proof-
+ − 891
have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 892
using SOab' tau ev valid notUkn nodel exobj'
+ − 893
obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (sb @ sa @ s'))]"]
+ − 894
by (auto simp del:obj2sobj.simps)
+ − 895
moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 896
using SOab' tau ev valid notUkn nodel exobj'
+ − 897
obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (sb @ sa @ s'))]"]
+ − 898
by (auto simp del:obj2sobj.simps)
+ − 899
moreover have "\<And> p'. obj' = Proc p' \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 900
apply (case_tac "p' = new_proc (sb @ sa @ s')")
+ − 901
using vs_tau exobj'ab tau
+ − 902
apply (simp, drule_tac valid_os, simp add:np_notin_curp)
+ − 903
using tau ev SOab' valid notUkn vs_tau
+ − 904
by (auto simp:obj2sobj.simps cp2sproc_simps' split:option.splits)
+ − 905
ultimately show ?thesis by (case_tac obj', auto)
+ − 906
qed moreover
+ − 907
have "obj2sobj (e#\<tau>) (Proc (new_proc (sb @ sa @ s'))) =
+ − 908
SProc (r',fr',exec_type_aux r pt, u) sp"
+ − 909
proof-
+ − 910
have "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) sp" using SPab tau vs_tau
+ − 911
by (auto split:option.splits simp:cp2sproc_simps' obj2sobj.simps)
+ − 912
hence "obj2sobj \<tau> (Proc (new_proc (sb@sa@s'))) = SProc (r,fr,pt,u) sp" using tau
+ − 913
by (auto simp:obj2sobj.simps cp2sproc.simps pct_def clone_type_unchange
+ − 914
split:option.splits)
+ − 915
moreover have "source_dir \<tau> f = Some sd" using vs_tau SFab tau
+ − 916
by (auto simp:source_dir_simps obj2sobj.simps split:option.splits if_splits)
+ − 917
ultimately show ?thesis using valid ev ap'_exec(6,7)
+ − 918
by (auto simp:cp2sproc_exec obj2sobj.simps split:option.splits)
+ − 919
qed
+ − 920
ultimately
+ − 921
show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 922
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact (s @ s') \<and>
+ − 923
obj2sobj (s @ s') obj = SProc (r', fr', exec_type_aux r pt, u) sp \<and>
+ − 924
exists (s @ s') obj"
+ − 925
using ev tau
+ − 926
apply (rule_tac x = "e#Clone p (new_proc (sb @ sa @ s')) #sb@sa" in exI)
+ − 927
by (rule_tac x = "Proc (new_proc (sb @ sa @ s'))" in exI, auto)
+ − 928
qed
+ − 929
qed
+ − 930
+ − 931
(* this is for ts2t createfile case ... *)
+ − 932
lemma all_sobjs_E0:
+ − 933
"\<lbrakk>sobj \<in> all_sobjs'; valid s'; obj2sobj s' obj' = sobj'; exists s' obj'; sobj' \<noteq> Unknown;
+ − 934
no_del_event s'; initp_intact s'\<rbrakk>
+ − 935
\<Longrightarrow> \<exists> s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s@s') obj \<and>
+ − 936
no_del_event (s @ s') \<and> initp_intact (s @ s') \<and>
+ − 937
obj2sobj (s @ s') obj = sobj \<and> exists (s @ s') obj"
+ − 938
by (drule all_sobjs_E0_aux, auto)
+ − 939
+ − 940
lemma all_sobjs_E1_aux[rule_format]:
+ − 941
"sobj \<in> all_sobjs' \<Longrightarrow> (\<forall> s' obj' sobj'. valid s' \<and> obj2sobj s' obj' = sobj' \<and> exists s' obj' \<and> sobj' \<noteq> Unknown \<and> no_del_event s' \<and> initp_intact_but s' sobj' \<longrightarrow> (\<exists> s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and> obj2sobj (s @ s') obj = sobj \<and> exists (s @ s') obj))"
+ − 942
proof (induct rule:all_sobjs'.induct)
+ − 943
case (af'_init f t) show ?case
+ − 944
proof (rule allI|rule impI|erule conjE)+
+ − 945
fix s' obj' sobj'
+ − 946
assume vss': "valid s'" and sobjs': "obj2sobj s' obj' = sobj'"
+ − 947
and nodels': "no_del_event s'"and intacts':"initp_intact_but s' sobj'"
+ − 948
and exso': "exists s' obj'"
+ − 949
from nodels' af'_init(1) have exf: "f \<in> current_files s'"
+ − 950
by (drule_tac obj = "File f" in nodel_imp_exists, simp+)
+ − 951
have "obj2sobj s' (File f) = SFile (t, f) (Some f)"
+ − 952
proof-
+ − 953
have "obj2sobj [] (File f) = SFile (t, f) (Some f)" using af'_init
+ − 954
by (auto simp:etype_of_file_def source_dir_of_init' obj2sobj.simps
+ − 955
split:option.splits)
+ − 956
thus ?thesis using vss' exf nodels' af'_init(1)
+ − 957
by (drule_tac obj2sobj_file_remains_app', auto)
+ − 958
qed
+ − 959
thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 960
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and>
+ − 961
obj2sobj (s @ s') obj = SFile (t, f) (Some f) \<and> exists (s @ s') obj"
+ − 962
apply (rule_tac x = "[]" in exI, rule_tac x = "File f" in exI)
+ − 963
by (simp add:vss' sobjs' nodels' intacts' exf exso')
+ − 964
qed
+ − 965
next
+ − 966
case (af'_cfd t sd srf r fr pt u srp t')
+ − 967
show ?case
+ − 968
proof (rule allI|rule impI|erule conjE)+
+ − 969
fix s' obj' sobj'
+ − 970
assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'"
+ − 971
and "initp_intact_but s' sobj'" and notUkn: "sobj' \<noteq> Unknown"
+ − 972
and exobj':"exists s' obj'"
+ − 973
with af'_cfd(1,2) obtain sa pf where
+ − 974
"valid (sa@s')" and "obj2sobj (sa@s') obj'=sobj' \<and> no_del_event (sa@s')" and
+ − 975
"exists (sa@s') obj'" and "initp_intact_but (sa@s') sobj'" and
+ − 976
SFa: "obj2sobj (sa@s') (File pf) = SFile (t, sd) srf" and
+ − 977
exfa: "pf \<in> current_files (sa@s')"
+ − 978
apply (erule_tac x = s' in allE, erule_tac x = obj' in allE, auto)
+ − 979
by (frule obj2sobj_file, auto)
+ − 980
with af'_cfd(3,4) notUkn obtain sb p where
+ − 981
SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) srp" and
+ − 982
expab: "exists (sb@sa@s') (Proc p)" and vsab: "valid (sb@sa@s')" and
+ − 983
soab: "obj2sobj (sb@sa@s') obj' = sobj'" and
+ − 984
exsoab: "exists (sb@sa@s') obj'" and
+ − 985
intactab: "initp_intact_but (sb@sa@s') sobj'" and
+ − 986
nodelab: "no_del_event (sb@sa@s')"
+ − 987
by (blast dest:obj2sobj_proc intro:nodel_exists_remains)
+ − 988
from exfa nodelab have exf:"pf \<in> current_files (sb@sa@s')"
+ − 989
apply (drule_tac obj = "File pf" in nodel_imp_un_deleted)
+ − 990
by (drule_tac s' = "sb" in not_deleted_imp_exists', auto)
+ − 991
from SFa vsab exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File pf) = SFile (t,sd) srf"
+ − 992
by (rule_tac s = "sa@s'" in obj2sobj_file_remains_app', simp_all)
+ − 993
obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)"
+ − 994
and tau: "\<tau>=sb@sa@s'" by auto
+ − 995
+ − 996
have valid: "valid (e # \<tau>)"
+ − 997
proof-
+ − 998
have "os_grant \<tau> e"
+ − 999
using ev tau expab exf by (simp add:ncf_notin_curf ncf_parent)
+ − 1000
moreover have "rc_grant \<tau> e"
+ − 1001
using ev tau af'_cfd(5,6,7) SPab SFab
+ − 1002
by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps
+ − 1003
split:if_splits option.splits t_rc_file_type.splits)
+ − 1004
ultimately show ?thesis using vsab tau
+ − 1005
by (rule_tac vs_step, simp+)
+ − 1006
qed moreover
+ − 1007
have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover
+ − 1008
have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau
+ − 1009
by (case_tac obj', simp+) moreover
+ − 1010
have "obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1011
proof-
+ − 1012
have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1013
using soab tau valid notUkn nodel ev exsoab
+ − 1014
by (auto intro!:obj2sobj_file_remains' simp:ncf_notin_curf)
+ − 1015
moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1016
using soab tau valid notUkn nodel ev exsoab
+ − 1017
by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf)
+ − 1018
moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1019
using soab tau valid notUkn nodel ev exsoab
+ − 1020
by (auto simp:obj2sobj.simps cp2sproc_simps'
+ − 1021
simp del:cp2sproc.simps split:option.splits)
+ − 1022
ultimately show ?thesis by (case_tac obj', auto)
+ − 1023
qed moreover
+ − 1024
have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t', sd) None"
+ − 1025
proof-
+ − 1026
have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t'"
+ − 1027
using ev tau SFab SPab af'_cfd(5)
+ − 1028
by (auto simp:obj2sobj.simps cp2sproc.simps etype_of_file_def
+ − 1029
split:option.splits if_splits intro!:etype_aux_prop4)
+ − 1030
moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd"
+ − 1031
using ev tau SFab SPab valid ncf_parent
+ − 1032
by (auto simp:source_dir_simps obj2sobj.simps
+ − 1033
split:if_splits option.splits)
+ − 1034
ultimately show ?thesis using nodel ncf_notin_curf[where s = \<tau>]
+ − 1035
nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>]
+ − 1036
by (auto simp:obj2sobj.simps dest:no_del_event_cons_D)
+ − 1037
qed moreover
+ − 1038
have "initp_intact_but (e#\<tau>) sobj'" using intactab tau ev valid nodel
+ − 1039
apply (case_tac sobj', case_tac option)
+ − 1040
by (simp_all add:initp_intact_butp_I_others initp_intact_I_others)
+ − 1041
ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 1042
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and>
+ − 1043
obj2sobj (s @ s') obj = SFile (t', sd) None \<and> exists (s @ s') obj "
+ − 1044
using tau ev
+ − 1045
apply (rule_tac x = "e#sb@sa" in exI)
+ − 1046
by (rule_tac x = "File (new_childf pf \<tau>)" in exI, auto)
+ − 1047
qed
+ − 1048
next
+ − 1049
case (af'_cfd' t sd srf r fr pt u srp)
+ − 1050
show ?case
+ − 1051
proof (rule allI|rule impI|erule conjE)+
+ − 1052
fix s' obj' sobj'
+ − 1053
assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'"
+ − 1054
and "initp_intact_but s' sobj'" and notUkn: "sobj' \<noteq> Unknown"
+ − 1055
and exobj':"exists s' obj'"
+ − 1056
with af'_cfd'(1,2) obtain sa pf where
+ − 1057
"valid (sa@s')" and "obj2sobj (sa@s') obj'=sobj' \<and> no_del_event (sa@s')" and
+ − 1058
"exists (sa@s') obj'" and "initp_intact_but (sa@s') sobj'" and
+ − 1059
SFa: "obj2sobj (sa@s') (File pf) = SFile (t, sd) srf" and
+ − 1060
exfa: "pf \<in> current_files (sa@s')"
+ − 1061
apply (erule_tac x = s' in allE, erule_tac x = obj' in allE, auto)
+ − 1062
by (frule obj2sobj_file, auto)
+ − 1063
with af'_cfd'(3,4) notUkn obtain sb p where
+ − 1064
SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) srp" and
+ − 1065
expab: "exists (sb@sa@s') (Proc p)" and vsab: "valid (sb@sa@s')" and
+ − 1066
soab: "obj2sobj (sb@sa@s') obj' = sobj'" and
+ − 1067
exsoab: "exists (sb@sa@s') obj'" and
+ − 1068
intactab: "initp_intact_but (sb@sa@s') sobj'" and
+ − 1069
nodelab: "no_del_event (sb@sa@s')"
+ − 1070
by (blast dest:obj2sobj_proc intro:nodel_exists_remains)
+ − 1071
from exfa nodelab have exf:"pf \<in> current_files (sb@sa@s')"
+ − 1072
apply (drule_tac obj = "File pf" in nodel_imp_un_deleted)
+ − 1073
by (drule_tac s' = "sb" in not_deleted_imp_exists', auto)
+ − 1074
from SFa vsab exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File pf) = SFile (t,sd) srf"
+ − 1075
by (rule_tac s = "sa@s'" in obj2sobj_file_remains_app', simp_all)
+ − 1076
obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)"
+ − 1077
and tau: "\<tau>=sb@sa@s'" by auto
+ − 1078
+ − 1079
have valid: "valid (e # \<tau>)"
+ − 1080
proof-
+ − 1081
have "os_grant \<tau> e"
+ − 1082
using ev tau expab exf by (simp add:ncf_notin_curf ncf_parent)
+ − 1083
moreover have "rc_grant \<tau> e"
+ − 1084
using ev tau af'_cfd'(5,6) SPab SFab
+ − 1085
by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps
+ − 1086
split:if_splits option.splits t_rc_file_type.splits)
+ − 1087
ultimately show ?thesis using vsab tau
+ − 1088
by (rule_tac vs_step, simp+)
+ − 1089
qed moreover
+ − 1090
have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover
+ − 1091
have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau
+ − 1092
by (case_tac obj', simp+) moreover
+ − 1093
have "obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1094
proof-
+ − 1095
have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1096
using soab tau valid notUkn nodel ev exsoab
+ − 1097
by (auto intro!:obj2sobj_file_remains' simp:ncf_notin_curf)
+ − 1098
moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1099
using soab tau valid notUkn nodel ev exsoab
+ − 1100
by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf)
+ − 1101
moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1102
using soab tau valid notUkn nodel ev exsoab
+ − 1103
by (auto simp:obj2sobj.simps cp2sproc_simps'
+ − 1104
simp del:cp2sproc.simps split:option.splits)
+ − 1105
ultimately show ?thesis by (case_tac obj', auto)
+ − 1106
qed moreover
+ − 1107
have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t, sd) None"
+ − 1108
proof-
+ − 1109
have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t"
+ − 1110
proof-
+ − 1111
have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = etype_of_file \<tau> pf"
+ − 1112
using ev tau SPab af'_cfd'(5)
+ − 1113
by (auto simp:obj2sobj.simps cp2sproc.simps ncf_parent etype_of_file_def
+ − 1114
split:option.splits intro!:etype_aux_prop3)
+ − 1115
thus ?thesis using SFab tau ev
+ − 1116
by (auto simp:obj2sobj.simps split:option.splits if_splits)
+ − 1117
qed
+ − 1118
moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd"
+ − 1119
using ev tau SFab SPab valid ncf_parent
+ − 1120
by (auto simp:source_dir_simps obj2sobj.simps
+ − 1121
split:if_splits option.splits)
+ − 1122
ultimately show ?thesis using nodel ncf_notin_curf[where s = \<tau>]
+ − 1123
nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>]
+ − 1124
by (auto simp:obj2sobj.simps dest:no_del_event_cons_D)
+ − 1125
qed moreover
+ − 1126
have "initp_intact_but (e#\<tau>) sobj'" using intactab tau ev valid nodel
+ − 1127
apply (case_tac sobj', case_tac option)
+ − 1128
by (simp_all add:initp_intact_butp_I_others initp_intact_I_others)
+ − 1129
ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 1130
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and>
+ − 1131
obj2sobj (s @ s') obj = SFile (t, sd) None \<and> exists (s @ s') obj"
+ − 1132
using tau ev
+ − 1133
apply (rule_tac x = "e#sb@sa" in exI)
+ − 1134
by (rule_tac x = "File (new_childf pf \<tau>)" in exI, auto)
+ − 1135
qed
+ − 1136
next
+ − 1137
case (ai'_init i t)
+ − 1138
hence initi: "i \<in> init_ipcs" using init_ipc_has_type
+ − 1139
by (simp add:bidirect_in_init_def)
+ − 1140
show ?case
+ − 1141
proof (rule allI|rule impI|erule conjE)+
+ − 1142
fix s' obj' sobj'
+ − 1143
assume vss': "valid s'" and sobjs': "obj2sobj s' obj' = sobj'"
+ − 1144
and nodels': "no_del_event s'"and intacts':"initp_intact_but s' sobj'"
+ − 1145
and exso': "exists s' obj'"
+ − 1146
from nodels' initi have exi: "i \<in> current_ipcs s'"
+ − 1147
by (drule_tac obj = "IPC i" in nodel_imp_exists, simp+)
+ − 1148
have "obj2sobj s' (IPC i) = SIPC t (Some i)"
+ − 1149
proof-
+ − 1150
have "obj2sobj [] (IPC i) = SIPC t (Some i)"
+ − 1151
using ai'_init initi by (auto simp:obj2sobj.simps)
+ − 1152
thus ?thesis using vss' exi nodels' initi
+ − 1153
by (drule_tac obj2sobj_ipc_remains'', auto simp:obj2sobj.simps)
+ − 1154
qed
+ − 1155
thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 1156
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and>
+ − 1157
obj2sobj (s @ s') obj = SIPC t (Some i) \<and> exists (s @ s') obj"
+ − 1158
apply (rule_tac x = "[]" in exI, rule_tac x = "IPC i" in exI)
+ − 1159
by (simp add:vss' sobjs' nodels' exi exso' intacts' del:obj2sobj.simps)
+ − 1160
qed
+ − 1161
next
+ − 1162
case (ai'_cipc r fr pt u srp)
+ − 1163
show ?case
+ − 1164
proof (rule allI|rule impI|erule conjE)+
+ − 1165
fix s' obj' sobj'
+ − 1166
assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'"
+ − 1167
and "initp_intact_but s' sobj'" and notUkn: "sobj' \<noteq> Unknown"
+ − 1168
and exobj':"exists s' obj'"
+ − 1169
with ai'_cipc(1,2) notUkn obtain s p where
+ − 1170
SPab: "obj2sobj (s@s') (Proc p) = SProc (r,fr,pt,u) srp" and
+ − 1171
expab: "exists (s@s') (Proc p)" and vsab: "valid (s@s')" and
+ − 1172
soab: "obj2sobj (s@s') obj' = sobj'" and
+ − 1173
exsoab: "exists (s@s') obj'" and
+ − 1174
intactab: "initp_intact_but (s@s') sobj'" and
+ − 1175
nodelab: "no_del_event (s@s')"
+ − 1176
by (blast dest:obj2sobj_proc intro:nodel_exists_remains)
+ − 1177
obtain e \<tau> where ev: "e = CreateIPC p (new_ipc \<tau>)" and tau: "\<tau>=s@s'" by auto
+ − 1178
+ − 1179
have valid: "valid (e # \<tau>)"
+ − 1180
proof-
+ − 1181
have "os_grant \<tau> e"
+ − 1182
using ev tau expab by (simp)
+ − 1183
moreover have "rc_grant \<tau> e"
+ − 1184
using ev tau ai'_cipc(3) SPab
+ − 1185
by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
+ − 1186
ultimately show ?thesis using vsab tau
+ − 1187
by (rule_tac vs_step, simp+)
+ − 1188
qed moreover
+ − 1189
have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover
+ − 1190
have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau
+ − 1191
by (case_tac obj', simp+) moreover
+ − 1192
have "obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1193
proof-
+ − 1194
have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1195
using soab tau valid notUkn nodel ev exsoab
+ − 1196
by (auto intro!:obj2sobj_file_remains' simp:ncf_notin_curf)
+ − 1197
moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1198
using soab tau valid notUkn nodel ev exsoab
+ − 1199
by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf)
+ − 1200
moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1201
using soab tau valid notUkn nodel ev exsoab
+ − 1202
by (auto simp:obj2sobj.simps cp2sproc_simps'
+ − 1203
simp del:cp2sproc.simps split:option.splits)
+ − 1204
ultimately show ?thesis by (case_tac obj', auto)
+ − 1205
qed moreover
+ − 1206
have "obj2sobj (e#\<tau>) (IPC (new_ipc \<tau>)) = SIPC (default_ipc_create_type r) None"
+ − 1207
using ev tau SPab nodel
+ − 1208
nodel_imp_exists[where obj = "IPC (new_ipc \<tau>)" and s =\<tau>]
+ − 1209
by (auto simp:obj2sobj.simps ni_notin_curi cp2sproc.simps
+ − 1210
split:option.splits dest:no_del_event_cons_D) moreover
+ − 1211
have "initp_intact_but (e#\<tau>) sobj'" using intactab tau ev valid nodel
+ − 1212
apply (case_tac sobj', case_tac option)
+ − 1213
by (simp_all add:initp_intact_butp_I_others initp_intact_I_others)
+ − 1214
ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 1215
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and>
+ − 1216
obj2sobj (s @ s') obj = SIPC (default_ipc_create_type r) None \<and> exists (s @ s') obj"
+ − 1217
using tau ev
+ − 1218
by (rule_tac x = "e#s" in exI, rule_tac x = "IPC (new_ipc \<tau>)" in exI, auto)
+ − 1219
qed
+ − 1220
next
+ − 1221
case (ap'_init p r fr t u) (* the big difference from other elims is in this case *)
+ − 1222
hence initp: "p \<in> init_processes" using init_proc_has_role
+ − 1223
by (simp add:bidirect_in_init_def)
+ − 1224
show ?case
+ − 1225
proof (rule allI|rule impI|erule conjE)+
+ − 1226
fix s' obj' sobj'
+ − 1227
assume VSs': "valid s'" and SOs': "obj2sobj s' obj' = sobj'"
+ − 1228
and Nodels': "no_del_event s'"and Intacts':"initp_intact_but s' sobj'"
+ − 1229
and exso': "exists s' obj'" and notUkn: "sobj' \<noteq> Unknown"
+ − 1230
from Nodels' initp have exp: "p \<in> current_procs s'"
+ − 1231
by (drule_tac obj = "Proc p" in nodel_imp_exists, simp+)
+ − 1232
have "\<exists> p'. obj2sobj s' (Proc p') = SProc (r,fr,t,u) (Some p) \<and> p' \<in> current_procs s'"
+ − 1233
proof (cases sobj')
+ − 1234
case (SProc sp srp)
+ − 1235
show ?thesis
+ − 1236
proof (cases srp)
+ − 1237
case None
+ − 1238
with SProc Intacts' have "initp_intact s'" by simp
+ − 1239
thus ?thesis using initp ap'_init
+ − 1240
apply (rule_tac x = p in exI)
+ − 1241
by (auto simp:initp_intact_def exp split:option.splits)
+ − 1242
next
+ − 1243
case (Some p')
+ − 1244
show ?thesis
+ − 1245
proof (cases "p' = p")
+ − 1246
case True
+ − 1247
with Intacts' SProc Some have "initp_alter s' p"
+ − 1248
by (simp add:initp_intact_butp_def)
+ − 1249
then obtain pa where "pa \<in> current_procs s'"
+ − 1250
and "obj2sobj s' (Proc pa) = init_obj2sobj (Proc p)"
+ − 1251
by (auto simp only:initp_alter_def)
+ − 1252
thus ?thesis using ap'_init initp
+ − 1253
by (rule_tac x = pa in exI, auto)
+ − 1254
next
+ − 1255
case False
+ − 1256
with Intacts' SProc Some initp
+ − 1257
have "obj2sobj s' (Proc p) = init_obj2sobj (Proc p)"
+ − 1258
apply (simp only:initp_intact_butp_def initp_intact_but.simps)
+ − 1259
by (erule conjE, erule_tac x = p in allE, simp)
+ − 1260
thus ?thesis using ap'_init exp
+ − 1261
by (rule_tac x = p in exI, auto split:option.splits)
+ − 1262
qed
+ − 1263
qed
+ − 1264
next
+ − 1265
case (SFile sf srf)
+ − 1266
thus ?thesis using ap'_init exp Intacts' initp
+ − 1267
by (rule_tac x = p in exI, auto split:option.splits simp:initp_intact_def)
+ − 1268
next
+ − 1269
case (SIPC si sri)
+ − 1270
thus ?thesis using ap'_init exp Intacts' initp
+ − 1271
by (rule_tac x = p in exI, auto split:option.splits simp:initp_intact_def)
+ − 1272
next
+ − 1273
case Unknown
+ − 1274
thus ?thesis using notUkn by simp
+ − 1275
qed
+ − 1276
then obtain p' where "obj2sobj s' (Proc p') = SProc (r, fr, t, u) (Some p)"
+ − 1277
and "p' \<in> current_procs s'" by blast
+ − 1278
thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 1279
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and>
+ − 1280
obj2sobj (s @ s') obj = SProc (r, fr, t, u) (Some p) \<and> exists (s @ s') obj"
+ − 1281
apply (rule_tac x = "[]" in exI, rule_tac x = "Proc p'" in exI)
+ − 1282
by (simp add:VSs' SOs' Nodels' exp exso' Intacts')
+ − 1283
qed
+ − 1284
next
+ − 1285
case (ap'_crole r fr t u srp r')
+ − 1286
show ?case
+ − 1287
proof (rule allI|rule impI|erule conjE)+
+ − 1288
fix s' obj' sobj'
+ − 1289
assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'"
+ − 1290
and "initp_intact_but s' sobj'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'"
+ − 1291
with ap'_crole(1,2) obtain s p where
+ − 1292
VSab: "valid (s@s')" and SOab': "obj2sobj (s@s') obj' = sobj'"
+ − 1293
and nodelab: "no_del_event (s@s')"
+ − 1294
and intactab: "initp_intact_but (s@s') sobj'"
+ − 1295
and SPab: "obj2sobj (s@s') (Proc p) = SProc (r, fr, t, u) srp"
+ − 1296
and exp:"exists (s@s') (Proc p)" and exobj'ab:"exists (s@s') obj'"
+ − 1297
by (blast dest:obj2sobj_proc intro:nodel_exists_remains)
+ − 1298
obtain e \<tau> where ev: "e = ChangeRole (new_proc (s@s')) r'"
+ − 1299
and tau: "\<tau> = Clone p (new_proc (s@s'))#s@s'" by auto
+ − 1300
hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit)
+ − 1301
have np_not_initp: "new_proc (s@s') \<notin> init_processes" using nodelab
+ − 1302
apply (rule_tac notI, drule_tac obj = "Proc (new_proc (s@s'))" in nodel_imp_exists)
+ − 1303
by (auto simp:np_notin_curp)
+ − 1304
+ − 1305
have valid: "valid (e#\<tau>)"
+ − 1306
proof-
+ − 1307
have "os_grant \<tau> e"
+ − 1308
using ev tau exp by (simp)
+ − 1309
moreover have "rc_grant \<tau> e"
+ − 1310
using ev tau ap'_crole(3) SPab
+ − 1311
by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
+ − 1312
ultimately show ?thesis using vs_tau
+ − 1313
by (erule_tac vs_step, simp+)
+ − 1314
qed moreover
+ − 1315
have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover
+ − 1316
have "initp_intact_but (e#\<tau>) sobj'"
+ − 1317
proof (cases sobj')
+ − 1318
case (SProc sp srp)
+ − 1319
show ?thesis
+ − 1320
proof (cases srp)
+ − 1321
case (Some p')
+ − 1322
with SOab' exobj'ab VSab intactab notUkn SProc
+ − 1323
have butp: "p' \<in> init_processes \<and> initp_intact_butp (s@s') p'"
+ − 1324
by (case_tac obj', auto intro:source_proc_in_init simp:obj2sobj.simps
+ − 1325
split:if_splits option.splits)
+ − 1326
then obtain p'' where exp': "p'' \<in> current_procs (s@s')" and
+ − 1327
SP': "obj2sobj (s@s') (Proc p'') = init_obj2sobj (Proc p')"
+ − 1328
by (auto simp:initp_alter_def initp_intact_butp_def)
+ − 1329
hence "initp_alter (e#\<tau>) p'" using tau ev notUkn nodel
+ − 1330
apply (simp add:initp_alter_def del:init_obj2sobj.simps)
+ − 1331
apply (rule_tac x = p'' in exI, rule conjI, simp)
+ − 1332
apply (subgoal_tac "p'' \<noteq> new_proc (s @s')")
+ − 1333
apply (auto simp:obj2sobj.simps cp2sproc.simps
+ − 1334
simp del:init_obj2sobj.simps split:option.splits)[1]
+ − 1335
by (rule notI, simp add:np_notin_curp)
+ − 1336
thus ?thesis using SProc Some intactab tau ev valid vs_tau np_not_initp
+ − 1337
apply (simp add:initp_intact_butp_def del:init_obj2sobj.simps)
+ − 1338
apply (rule impI|rule allI|rule conjI|erule conjE)+
+ − 1339
apply (erule_tac x = pa in allE)
+ − 1340
by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:init_obj2sobj.simps
+ − 1341
split:option.splits)
+ − 1342
next
+ − 1343
case None
+ − 1344
with intactab SProc
+ − 1345
have "initp_intact (s@s')" by simp
+ − 1346
hence "initp_intact (e#\<tau>)" using tau ev valid
+ − 1347
by (simp add:initp_intact_I_crole)
+ − 1348
thus ?thesis using SProc None by simp
+ − 1349
qed
+ − 1350
next
+ − 1351
case (SFile sf srf)
+ − 1352
with intactab SFile
+ − 1353
have "initp_intact (s@s')" by simp
+ − 1354
hence "initp_intact (e#\<tau>)" using tau ev valid
+ − 1355
by (simp add:initp_intact_I_crole)
+ − 1356
thus ?thesis using SFile by simp
+ − 1357
next
+ − 1358
case (SIPC si sri)
+ − 1359
with intactab SIPC
+ − 1360
have "initp_intact (s@s')" by simp
+ − 1361
hence "initp_intact (e#\<tau>)" using tau ev valid
+ − 1362
by (simp add:initp_intact_I_crole)
+ − 1363
thus ?thesis using SIPC by simp
+ − 1364
next
+ − 1365
case Unknown
+ − 1366
with notUkn show ?thesis by simp
+ − 1367
qed moreover
+ − 1368
have exobj': "exists (e#\<tau>) obj'" using exobj'ab valid ev tau
+ − 1369
by (case_tac obj', simp+) moreover
+ − 1370
have "obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1371
proof-
+ − 1372
have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1373
using SOab' tau ev valid notUkn nodel exobj'
+ − 1374
obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]
+ − 1375
by (auto)
+ − 1376
moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1377
using SOab' tau ev valid notUkn nodel exobj'
+ − 1378
obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]
+ − 1379
by auto
+ − 1380
moreover have "\<And> p'. obj' = Proc p' \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1381
apply (case_tac "p' = new_proc (s @ s')")
+ − 1382
using vs_tau exobj'ab tau
+ − 1383
apply (simp, drule_tac valid_os, simp add:np_notin_curp)
+ − 1384
using tau ev SOab' valid notUkn vs_tau
+ − 1385
by (auto simp:obj2sobj.simps cp2sproc_simps' split:option.splits)
+ − 1386
ultimately show ?thesis by (case_tac obj', auto)
+ − 1387
qed moreover
+ − 1388
have "obj2sobj (e#\<tau>) (Proc (new_proc (s@s'))) = SProc (r', fr, t, u) srp"
+ − 1389
using SPab tau vs_tau ev valid
+ − 1390
by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:cp2sproc.simps
+ − 1391
split:option.splits) moreover
+ − 1392
have "exists (e#\<tau>) (Proc p)" using exp tau ev by simp
+ − 1393
ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 1394
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and>
+ − 1395
obj2sobj (s @ s') obj = SProc (r', fr, t, u) srp \<and> exists (s @ s') obj"
+ − 1396
using ev tau
+ − 1397
apply (rule_tac x = "e # Clone p (new_proc (s @ s')) # s" in exI)
+ − 1398
by (rule_tac x = "Proc (new_proc (s@s'))" in exI, auto)
+ − 1399
qed
+ − 1400
next
+ − 1401
case (ap'_chown r fr t u srp u' nr)
+ − 1402
show ?case
+ − 1403
proof (rule allI|rule impI|erule conjE)+
+ − 1404
fix s' obj' sobj'
+ − 1405
assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'"
+ − 1406
and "initp_intact_but s' sobj'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'"
+ − 1407
with ap'_chown(1,2) obtain s p where
+ − 1408
VSab: "valid (s@s')" and SOab': "obj2sobj (s@s') obj' = sobj'"
+ − 1409
and nodelab: "no_del_event (s@s')" and intactab: "initp_intact_but (s@s') sobj'"
+ − 1410
and SPab: "obj2sobj (s@s') (Proc p) = SProc (r, fr, t, u) srp"
+ − 1411
and exp:"exists (s@s') (Proc p)" and exobj'ab:"exists (s@s') obj'"
+ − 1412
by (blast dest:obj2sobj_proc intro:nodel_exists_remains)
+ − 1413
obtain e \<tau> where ev: "e = ChangeOwner (new_proc (s@s')) u'"
+ − 1414
and tau: "\<tau> = Clone p (new_proc (s@s'))#s@s'" by auto
+ − 1415
hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit)
+ − 1416
have np_not_initp: "new_proc (s@s') \<notin> init_processes" using nodelab
+ − 1417
apply (rule_tac notI, drule_tac obj = "Proc (new_proc (s@s'))" in nodel_imp_exists)
+ − 1418
by (auto simp:np_notin_curp)
+ − 1419
+ − 1420
have valid: "valid (e#\<tau>)"
+ − 1421
proof-
+ − 1422
have "os_grant \<tau> e"
+ − 1423
using ev tau exp ap'_chown(3) by (simp)
+ − 1424
moreover have "rc_grant \<tau> e"
+ − 1425
using ev tau ap'_chown(5) SPab
+ − 1426
by (auto simp:cp2sproc.simps obj2sobj.simps pct_def clone_type_unchange
+ − 1427
split:option.splits t_rc_proc_type.splits)
+ − 1428
(* here is another place of no_limit of clone event assumption *)
+ − 1429
ultimately show ?thesis using vs_tau
+ − 1430
by (erule_tac vs_step, simp+)
+ − 1431
qed moreover
+ − 1432
have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover
+ − 1433
have "initp_intact_but (e#\<tau>) sobj'"
+ − 1434
proof (cases sobj')
+ − 1435
case (SProc sp srp)
+ − 1436
show ?thesis
+ − 1437
proof (cases srp)
+ − 1438
case (Some p')
+ − 1439
with SOab' exobj'ab VSab intactab notUkn SProc
+ − 1440
have butp: "p' \<in> init_processes \<and> initp_intact_butp (s@s') p'"
+ − 1441
by (case_tac obj', auto intro:source_proc_in_init simp:obj2sobj.simps
+ − 1442
split:if_splits option.splits)
+ − 1443
then obtain p'' where exp': "p'' \<in> current_procs (s@s')" and
+ − 1444
SP': "obj2sobj (s@s') (Proc p'') = init_obj2sobj (Proc p')"
+ − 1445
by (auto simp:initp_alter_def initp_intact_butp_def)
+ − 1446
hence "initp_alter (e#\<tau>) p'" using tau ev notUkn nodel
+ − 1447
apply (simp add:initp_alter_def del:init_obj2sobj.simps)
+ − 1448
apply (rule_tac x = p'' in exI, rule conjI, simp)
+ − 1449
apply (subgoal_tac "p'' \<noteq> new_proc (s @s')")
+ − 1450
apply (auto simp:obj2sobj.simps cp2sproc.simps
+ − 1451
simp del:init_obj2sobj.simps split:option.splits)[1]
+ − 1452
by (rule notI, simp add:np_notin_curp)
+ − 1453
thus ?thesis using SProc Some intactab tau ev valid vs_tau np_not_initp
+ − 1454
apply (simp add:initp_intact_butp_def del:init_obj2sobj.simps)
+ − 1455
apply (rule impI|rule allI|rule conjI|erule conjE)+
+ − 1456
apply (erule_tac x = pa in allE)
+ − 1457
by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:init_obj2sobj.simps
+ − 1458
split:option.splits)
+ − 1459
next
+ − 1460
case None
+ − 1461
with intactab SProc
+ − 1462
have "initp_intact (s@s')" by simp
+ − 1463
hence "initp_intact (e#\<tau>)" using tau ev valid
+ − 1464
by (simp add:initp_intact_I_chown)
+ − 1465
thus ?thesis using SProc None by simp
+ − 1466
qed
+ − 1467
next
+ − 1468
case (SFile sf srf)
+ − 1469
with intactab SFile
+ − 1470
have "initp_intact (s@s')" by simp
+ − 1471
hence "initp_intact (e#\<tau>)" using tau ev valid
+ − 1472
by (simp add:initp_intact_I_chown)
+ − 1473
thus ?thesis using SFile by simp
+ − 1474
next
+ − 1475
case (SIPC si sri)
+ − 1476
with intactab SIPC
+ − 1477
have "initp_intact (s@s')" by simp
+ − 1478
hence "initp_intact (e#\<tau>)" using tau ev valid
+ − 1479
by (simp add:initp_intact_I_chown)
+ − 1480
thus ?thesis using SIPC by simp
+ − 1481
next
+ − 1482
case Unknown
+ − 1483
with notUkn show ?thesis by simp
+ − 1484
qed moreover
+ − 1485
have exobj': "exists (e#\<tau>) obj'" using exobj'ab valid ev tau
+ − 1486
by (case_tac obj', simp+) moreover
+ − 1487
have "obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1488
proof-
+ − 1489
have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1490
using SOab' tau ev valid notUkn nodel exobj'
+ − 1491
obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]
+ − 1492
by (auto)
+ − 1493
moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1494
using SOab' tau ev valid notUkn nodel exobj'
+ − 1495
obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]
+ − 1496
by auto
+ − 1497
moreover have "\<And> p'. obj' = Proc p' \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1498
apply (case_tac "p' = new_proc (s @ s')")
+ − 1499
using vs_tau exobj'ab tau
+ − 1500
apply (simp, drule_tac valid_os, simp add:np_notin_curp)
+ − 1501
using tau ev SOab' valid notUkn vs_tau
+ − 1502
by (auto simp:obj2sobj.simps cp2sproc_simps' split:option.splits)
+ − 1503
ultimately show ?thesis by (case_tac obj', auto)
+ − 1504
qed moreover
+ − 1505
have "obj2sobj (e#\<tau>) (Proc (new_proc (s@s'))) =
+ − 1506
SProc (nr,fr,chown_type_aux r nr t,u') srp"
+ − 1507
using SPab tau vs_tau ev valid ap'_chown(4)
+ − 1508
by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:cp2sproc.simps
+ − 1509
split:option.splits) moreover
+ − 1510
have "exists (e#\<tau>) (Proc p)" using exp tau ev by simp moreover
+ − 1511
ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 1512
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and>
+ − 1513
obj2sobj (s @ s') obj = SProc (nr,fr,chown_type_aux r nr t,u') srp \<and>
+ − 1514
exists (s @ s') obj"
+ − 1515
using ev tau
+ − 1516
apply (rule_tac x = "e # Clone p (new_proc (s @ s')) # s" in exI)
+ − 1517
by (rule_tac x = "Proc (new_proc (s@s'))" in exI, auto)
+ − 1518
qed
+ − 1519
next
+ − 1520
case (ap'_exec r fr pt u sp t sd sf r' fr')
+ − 1521
show ?case
+ − 1522
proof (rule allI|rule impI|erule conjE)+
+ − 1523
fix s' obj' sobj'
+ − 1524
assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'"
+ − 1525
and "initp_intact_but s' sobj'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'"
+ − 1526
with ap'_exec(3,4) obtain sa f where
+ − 1527
SFa: "obj2sobj (sa @ s') (File f) = SFile (t, sd) sf" and
+ − 1528
Exfa: "exists (sa @ s') (File f)" and
+ − 1529
butsa: "initp_intact_but (sa @ s') sobj'" and
+ − 1530
othersa:"valid (sa @ s') \<and> obj2sobj (sa @ s') obj' = sobj' \<and>
+ − 1531
exists (sa @s') obj' \<and> no_del_event (sa @ s')"
+ − 1532
by (blast dest:obj2sobj_file intro:nodel_exists_remains)
+ − 1533
with ap'_exec(1,2) notUkn obtain sb p where
+ − 1534
VSab: "valid (sb@sa@s')" and SOab': "obj2sobj (sb@sa@s') obj' = sobj'"
+ − 1535
and nodelab: "no_del_event (sb@sa@s')"
+ − 1536
and intactab: "initp_intact_but (sb@sa@s') sobj'"
+ − 1537
and SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r, fr, pt, u) sp"
+ − 1538
and exp:"exists (sb@sa@s') (Proc p)" and exobj'ab:"exists (sb@sa@s') obj'"
+ − 1539
by (blast dest:obj2sobj_proc intro:nodel_exists_remains)
+ − 1540
obtain e \<tau> where ev: "e = Execute (new_proc (sb@sa@s')) f"
+ − 1541
and tau: "\<tau> = Clone p (new_proc (sb@sa@s'))#sb@sa@s'" by auto
+ − 1542
hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit)
+ − 1543
from Exfa nodelab have exf:"f \<in> current_files (sb@sa@s')"
+ − 1544
apply (drule_tac obj = "File f" in nodel_imp_un_deleted)
+ − 1545
by (drule_tac s' = "sb" in not_deleted_imp_exists', auto)
+ − 1546
from SFa VSab Exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File f) = SFile (t,sd) sf"
+ − 1547
by (rule_tac s = "sa@s'" in obj2sobj_file_remains'', simp_all)
+ − 1548
have np_not_initp: "new_proc (sb@sa@s') \<notin> init_processes" using nodelab
+ − 1549
apply (rule_tac notI, drule_tac obj = "Proc (new_proc (sb@sa@s'))" in nodel_imp_exists)
+ − 1550
by (auto simp:np_notin_curp)
+ − 1551
+ − 1552
have valid: "valid (e#\<tau>)"
+ − 1553
proof-
+ − 1554
have "os_grant \<tau> e"
+ − 1555
using ev tau exp by (simp add:exf)
+ − 1556
moreover have "rc_grant \<tau> e"
+ − 1557
using ev tau ap'_exec(5) SPab SFab
+ − 1558
by (auto simp:etype_of_file_def cp2sproc.simps obj2sobj.simps
+ − 1559
split:if_splits option.splits)
+ − 1560
ultimately show ?thesis using vs_tau
+ − 1561
by (erule_tac vs_step, simp+)
+ − 1562
qed moreover
+ − 1563
have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover
+ − 1564
have "initp_intact_but (e#\<tau>) sobj'"
+ − 1565
proof (cases sobj')
+ − 1566
case (SProc sp srp)
+ − 1567
show ?thesis
+ − 1568
proof (cases srp)
+ − 1569
case (Some p')
+ − 1570
with SOab' exobj'ab VSab intactab notUkn SProc
+ − 1571
have butp: "p' \<in> init_processes \<and> initp_intact_butp (sb@sa@s') p'"
+ − 1572
by (case_tac obj', auto intro:source_proc_in_init simp:obj2sobj.simps
+ − 1573
split:if_splits option.splits)
+ − 1574
then obtain p'' where exp': "p'' \<in> current_procs (sb@sa@s')" and
+ − 1575
SP': "obj2sobj (sb@sa@s') (Proc p'') = init_obj2sobj (Proc p')"
+ − 1576
by (auto simp:initp_alter_def initp_intact_butp_def)
+ − 1577
hence "initp_alter (e#\<tau>) p'" using tau ev notUkn nodel
+ − 1578
apply (simp add:initp_alter_def del:init_obj2sobj.simps)
+ − 1579
apply (rule_tac x = p'' in exI, rule conjI, simp)
+ − 1580
apply (subgoal_tac "p'' \<noteq> new_proc (sb@sa@s')")
+ − 1581
apply (auto simp:obj2sobj.simps cp2sproc.simps
+ − 1582
simp del:init_obj2sobj.simps split:option.splits)[1]
+ − 1583
by (rule notI, simp add:np_notin_curp)
+ − 1584
thus ?thesis using SProc Some intactab tau ev valid vs_tau np_not_initp
+ − 1585
apply (simp add:initp_intact_butp_def del:init_obj2sobj.simps)
+ − 1586
apply (rule impI|rule allI|rule conjI|erule conjE)+
+ − 1587
apply (erule_tac x = pa in allE)
+ − 1588
by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:init_obj2sobj.simps
+ − 1589
split:option.splits)
+ − 1590
next
+ − 1591
case None
+ − 1592
with intactab SProc
+ − 1593
have "initp_intact (sb@sa@s')" by simp
+ − 1594
hence "initp_intact (e#\<tau>)" using tau ev valid
+ − 1595
by (simp add:initp_intact_I_exec)
+ − 1596
thus ?thesis using SProc None by simp
+ − 1597
qed
+ − 1598
next
+ − 1599
case (SFile sf srf)
+ − 1600
with intactab SFile
+ − 1601
have "initp_intact (sb@sa@s')" by simp
+ − 1602
hence "initp_intact (e#\<tau>)" using tau ev valid
+ − 1603
by (simp add:initp_intact_I_exec)
+ − 1604
thus ?thesis using SFile by simp
+ − 1605
next
+ − 1606
case (SIPC si sri)
+ − 1607
with intactab SIPC
+ − 1608
have "initp_intact (sb@sa@s')" by simp
+ − 1609
hence "initp_intact (e#\<tau>)" using tau ev valid
+ − 1610
by (simp add:initp_intact_I_exec)
+ − 1611
thus ?thesis using SIPC by simp
+ − 1612
next
+ − 1613
case Unknown
+ − 1614
with notUkn show ?thesis by simp
+ − 1615
qed moreover
+ − 1616
have exobj': "exists (e#\<tau>) obj'" using exobj'ab valid ev tau
+ − 1617
by (case_tac obj', simp+) moreover
+ − 1618
have "obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1619
proof-
+ − 1620
have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1621
using SOab' tau ev valid notUkn nodel exobj'
+ − 1622
obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (sb @ sa @ s'))]"]
+ − 1623
by (auto simp del:obj2sobj.simps)
+ − 1624
moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1625
using SOab' tau ev valid notUkn nodel exobj'
+ − 1626
obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (sb @ sa @ s'))]"]
+ − 1627
by (auto simp del:obj2sobj.simps)
+ − 1628
moreover have "\<And> p'. obj' = Proc p' \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1629
apply (case_tac "p' = new_proc (sb @ sa @ s')")
+ − 1630
using vs_tau exobj'ab tau
+ − 1631
apply (simp, drule_tac valid_os, simp add:np_notin_curp)
+ − 1632
using tau ev SOab' valid notUkn vs_tau
+ − 1633
by (auto simp:obj2sobj.simps cp2sproc_simps' split:option.splits)
+ − 1634
ultimately show ?thesis by (case_tac obj', auto)
+ − 1635
qed moreover
+ − 1636
have "obj2sobj (e#\<tau>) (Proc (new_proc (sb @ sa @ s'))) =
+ − 1637
SProc (r',fr',exec_type_aux r pt, u) sp"
+ − 1638
proof-
+ − 1639
have "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) sp" using SPab tau vs_tau
+ − 1640
by (auto split:option.splits simp:cp2sproc_simps' obj2sobj.simps)
+ − 1641
hence "obj2sobj \<tau> (Proc (new_proc (sb@sa@s'))) = SProc (r,fr,pt,u) sp" using tau
+ − 1642
by (auto simp:obj2sobj.simps cp2sproc.simps pct_def clone_type_unchange
+ − 1643
split:option.splits)
+ − 1644
moreover have "source_dir \<tau> f = Some sd" using vs_tau SFab tau
+ − 1645
by (auto simp:source_dir_simps obj2sobj.simps split:option.splits if_splits)
+ − 1646
ultimately show ?thesis using valid ev ap'_exec(6,7)
+ − 1647
by (auto simp:cp2sproc_exec obj2sobj.simps split:option.splits)
+ − 1648
qed
+ − 1649
ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 1650
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and>
+ − 1651
obj2sobj (s @ s') obj = SProc (r', fr', exec_type_aux r pt, u) sp \<and>
+ − 1652
exists (s @ s') obj"
+ − 1653
using ev tau
+ − 1654
apply (rule_tac x = "e#Clone p (new_proc (sb @ sa @ s')) #sb@sa" in exI)
+ − 1655
by (rule_tac x = "Proc (new_proc (sb @ sa @ s'))" in exI, auto)
+ − 1656
qed
+ − 1657
qed
+ − 1658
+ − 1659
(* this is for all_sobjs_E2 *)
+ − 1660
lemma all_sobjs_E1:
+ − 1661
"\<lbrakk>sobj \<in> all_sobjs'; valid s'; obj2sobj s' obj' = sobj'; exists s' obj'; sobj' \<noteq> Unknown;
+ − 1662
no_del_event s'; initp_intact_but s' sobj'\<rbrakk>
+ − 1663
\<Longrightarrow> \<exists> s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s@s') obj \<and>
+ − 1664
no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj' \<and>
+ − 1665
obj2sobj (s @ s') obj = sobj \<and> exists (s @ s') obj"
+ − 1666
by (drule all_sobjs_E1_aux, auto)
+ − 1667
+ − 1668
+ − 1669
lemma all_sobjs_E2_aux[rule_format]:
+ − 1670
"sobj \<in> all_sobjs' \<Longrightarrow> (\<forall> s' obj' sobj'. valid s' \<and> obj2sobj s' obj' = sobj' \<and> exists s' obj' \<and> sobj' \<noteq> Unknown \<and> not_both_sproc sobj sobj' \<and> no_del_event s' \<and> initp_intact s' \<longrightarrow> (\<exists> s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s @ s') obj' \<and> no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj \<and> obj2sobj (s @ s') obj = sobj \<and> exists (s @ s') obj \<and> sobj_source_eq_obj sobj obj))"
+ − 1671
proof (induct rule:all_sobjs'.induct)
+ − 1672
case (af'_init f t) show ?case
+ − 1673
proof (rule allI|rule impI|erule conjE)+
+ − 1674
fix s' obj' sobj'
+ − 1675
assume vss': "valid s'" and sobjs': "obj2sobj s' obj' = sobj'"
+ − 1676
and nodels': "no_del_event s'"and intacts':"initp_intact s'"
+ − 1677
and notboth: "not_both_sproc (SFile (t, f) (Some f)) sobj'"
+ − 1678
and exso': "exists s' obj'"
+ − 1679
from nodels' af'_init(1) have exf: "f \<in> current_files s'"
+ − 1680
by (drule_tac obj = "File f" in nodel_imp_exists, simp+)
+ − 1681
have "obj2sobj s' (File f) = SFile (t, f) (Some f)"
+ − 1682
proof-
+ − 1683
have "obj2sobj [] (File f) = SFile (t, f) (Some f)" using af'_init
+ − 1684
by (auto simp:etype_of_file_def source_dir_of_init' obj2sobj.simps
+ − 1685
split:option.splits)
+ − 1686
thus ?thesis using vss' exf nodels' af'_init(1)
+ − 1687
by (drule_tac obj2sobj_file_remains_app', auto)
+ − 1688
qed
+ − 1689
thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 1690
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and>
+ − 1691
initp_intact_but (s @ s') (SFile (t, f) (Some f)) \<and>
+ − 1692
obj2sobj (s @ s') obj = SFile (t, f) (Some f) \<and>
+ − 1693
exists (s @ s') obj \<and> sobj_source_eq_obj (SFile (t, f) (Some f)) obj"
+ − 1694
apply (rule_tac x = "[]" in exI, rule_tac x = "File f" in exI)
+ − 1695
by (simp add:vss' sobjs' nodels' intacts' exf exso')
+ − 1696
qed
+ − 1697
next
+ − 1698
case (af'_cfd t sd srf r fr pt u srp t')
+ − 1699
show ?case
+ − 1700
proof (rule allI|rule impI|erule conjE)+
+ − 1701
fix s' obj' sobj'
+ − 1702
assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'"
+ − 1703
and Both:"not_both_sproc (SFile (t', sd) None) sobj'"
+ − 1704
and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown"
+ − 1705
and exobj':"exists s' obj'"
+ − 1706
with af'_cfd(1,2) obtain sa pf where
+ − 1707
"valid (sa@s')" and "obj2sobj (sa@s') obj'=sobj' \<and> no_del_event (sa@s')" and
+ − 1708
"exists (sa@s') obj'" and "initp_intact (sa@s')" and
+ − 1709
SFa: "obj2sobj (sa@s') (File pf) = SFile (t, sd) srf" and
+ − 1710
exfa: "pf \<in> current_files (sa@s')"
+ − 1711
apply (drule_tac sf' = "(t, sd)" and srf' = srf in not_both_I_file)
+ − 1712
apply (erule_tac x = s' in allE, erule_tac x = obj' in allE, auto)
+ − 1713
by (frule obj2sobj_file, auto)
+ − 1714
with af'_cfd(3) notUkn obtain sb p where
+ − 1715
SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) srp" and
+ − 1716
expab: "exists (sb@sa@s') (Proc p)" and vsab: "valid (sb@sa@s')" and
+ − 1717
soab: "obj2sobj (sb@sa@s') obj' = sobj'" and
+ − 1718
exsoab: "exists (sb@sa@s') obj'" and
+ − 1719
intactab: "initp_intact (sb@sa@s')" and
+ − 1720
nodelab: "no_del_event (sb@sa@s')"
+ − 1721
apply (drule_tac s'= "sa@s'" and obj' = obj' in all_sobjs_E0, auto)
+ − 1722
apply (frule obj2sobj_proc, erule exE)
+ − 1723
by (auto intro:nodel_exists_remains)
+ − 1724
from exfa nodelab have exf:"pf \<in> current_files (sb@sa@s')"
+ − 1725
apply (drule_tac obj = "File pf" in nodel_imp_un_deleted)
+ − 1726
by (drule_tac s' = "sb" in not_deleted_imp_exists', auto)
+ − 1727
from SFa vsab exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File pf) = SFile (t,sd) srf"
+ − 1728
by (rule_tac s = "sa@s'" in obj2sobj_file_remains_app', simp_all)
+ − 1729
obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)"
+ − 1730
and tau: "\<tau>=sb@sa@s'" by auto
+ − 1731
+ − 1732
have valid: "valid (e # \<tau>)"
+ − 1733
proof-
+ − 1734
have "os_grant \<tau> e"
+ − 1735
using ev tau expab exf by (simp add:ncf_notin_curf ncf_parent)
+ − 1736
moreover have "rc_grant \<tau> e"
+ − 1737
using ev tau af'_cfd(5,6,7) SPab SFab
+ − 1738
by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps
+ − 1739
split:if_splits option.splits t_rc_file_type.splits)
+ − 1740
ultimately show ?thesis using vsab tau
+ − 1741
by (rule_tac vs_step, simp+)
+ − 1742
qed moreover
+ − 1743
have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover
+ − 1744
have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau
+ − 1745
by (case_tac obj', simp+) moreover
+ − 1746
have "obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1747
proof-
+ − 1748
have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1749
using soab tau valid notUkn nodel ev exsoab
+ − 1750
by (auto intro!:obj2sobj_file_remains' simp:ncf_notin_curf)
+ − 1751
moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1752
using soab tau valid notUkn nodel ev exsoab
+ − 1753
by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf)
+ − 1754
moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1755
using soab tau valid notUkn nodel ev exsoab
+ − 1756
by (auto simp:obj2sobj.simps cp2sproc_simps'
+ − 1757
simp del:cp2sproc.simps split:option.splits)
+ − 1758
ultimately show ?thesis by (case_tac obj', auto)
+ − 1759
qed moreover
+ − 1760
have "initp_intact (e#\<tau>)" using intactab tau ev valid nodel
+ − 1761
by (simp add:initp_intact_I_others) moreover
+ − 1762
have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t', sd) None"
+ − 1763
proof-
+ − 1764
have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t'"
+ − 1765
using ev tau SFab SPab af'_cfd(5)
+ − 1766
by (auto simp:obj2sobj.simps etype_of_file_def cp2sproc.simps
+ − 1767
split:option.splits if_splits intro!:etype_aux_prop4)
+ − 1768
moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd"
+ − 1769
using ev tau SFab SPab valid ncf_parent
+ − 1770
by (auto simp:source_dir_simps obj2sobj.simps
+ − 1771
split:if_splits option.splits)
+ − 1772
ultimately show ?thesis using nodel ncf_notin_curf[where s = \<tau>]
+ − 1773
nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>]
+ − 1774
by (auto simp:obj2sobj.simps dest:no_del_event_cons_D)
+ − 1775
qed
+ − 1776
ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 1777
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and>
+ − 1778
initp_intact_but (s @ s') (SFile (t', sd) None) \<and>
+ − 1779
obj2sobj (s @ s') obj = SFile (t', sd) None \<and>
+ − 1780
exists (s @ s') obj \<and> sobj_source_eq_obj (SFile (t', sd) None) obj"
+ − 1781
using tau ev
+ − 1782
apply (rule_tac x = "e#sb@sa" in exI)
+ − 1783
by (rule_tac x = "File (new_childf pf \<tau>)" in exI, auto)
+ − 1784
qed
+ − 1785
next
+ − 1786
case (af'_cfd' t sd srf r fr pt u srp)
+ − 1787
show ?case
+ − 1788
proof (rule allI|rule impI|erule conjE)+
+ − 1789
fix s' obj' sobj'
+ − 1790
assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'"
+ − 1791
and Both:"not_both_sproc (SFile (t, sd) None) sobj'"
+ − 1792
and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown"
+ − 1793
and exobj':"exists s' obj'"
+ − 1794
with af'_cfd'(1,2) obtain sa pf where
+ − 1795
"valid (sa@s')" and "obj2sobj (sa@s') obj'=sobj' \<and> no_del_event (sa@s')" and
+ − 1796
"exists (sa@s') obj'" and "initp_intact (sa@s')" and
+ − 1797
SFa: "obj2sobj (sa@s') (File pf) = SFile (t, sd) srf" and
+ − 1798
exfa: "pf \<in> current_files (sa@s')"
+ − 1799
apply (drule_tac sf' = "(t, sd)" and srf' = srf in not_both_I_file)
+ − 1800
apply (erule_tac x = s' in allE, erule_tac x = obj' in allE, auto)
+ − 1801
by (frule obj2sobj_file, auto)
+ − 1802
with af'_cfd'(3) notUkn obtain sb p where
+ − 1803
SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r,fr,pt,u) srp" and
+ − 1804
expab: "exists (sb@sa@s') (Proc p)" and vsab: "valid (sb@sa@s')" and
+ − 1805
soab: "obj2sobj (sb@sa@s') obj' = sobj'" and
+ − 1806
exsoab: "exists (sb@sa@s') obj'" and
+ − 1807
intactab: "initp_intact (sb@sa@s')" and
+ − 1808
nodelab: "no_del_event (sb@sa@s')"
+ − 1809
apply (drule_tac s'= "sa@s'" and obj' = obj' in all_sobjs_E0, auto)
+ − 1810
apply (frule obj2sobj_proc, erule exE)
+ − 1811
by (auto intro:nodel_exists_remains)
+ − 1812
from exfa nodelab have exf:"pf \<in> current_files (sb@sa@s')"
+ − 1813
apply (drule_tac obj = "File pf" in nodel_imp_un_deleted)
+ − 1814
by (drule_tac s' = "sb" in not_deleted_imp_exists', auto)
+ − 1815
from SFa vsab exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File pf) = SFile (t,sd) srf"
+ − 1816
by (rule_tac s = "sa@s'" in obj2sobj_file_remains_app', simp_all)
+ − 1817
obtain e \<tau> where ev: "e = CreateFile p (new_childf pf \<tau>)"
+ − 1818
and tau: "\<tau>=sb@sa@s'" by auto
+ − 1819
+ − 1820
have valid: "valid (e # \<tau>)"
+ − 1821
proof-
+ − 1822
have "os_grant \<tau> e"
+ − 1823
using ev tau expab exf by (simp add:ncf_notin_curf ncf_parent)
+ − 1824
moreover have "rc_grant \<tau> e"
+ − 1825
using ev tau af'_cfd'(5,6) SPab SFab
+ − 1826
by (auto simp:etype_of_file_def cp2sproc.simps ncf_parent obj2sobj.simps
+ − 1827
split:if_splits option.splits t_rc_file_type.splits)
+ − 1828
ultimately show ?thesis using vsab tau
+ − 1829
by (rule_tac vs_step, simp+)
+ − 1830
qed moreover
+ − 1831
have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover
+ − 1832
have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau
+ − 1833
by (case_tac obj', simp+) moreover
+ − 1834
have "obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1835
proof-
+ − 1836
have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1837
using soab tau valid notUkn nodel ev exsoab
+ − 1838
by (auto intro!:obj2sobj_file_remains' simp:ncf_notin_curf)
+ − 1839
moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1840
using soab tau valid notUkn nodel ev exsoab
+ − 1841
by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf)
+ − 1842
moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1843
using soab tau valid notUkn nodel ev exsoab
+ − 1844
by (auto simp:obj2sobj.simps cp2sproc_simps'
+ − 1845
simp del:cp2sproc.simps split:option.splits)
+ − 1846
ultimately show ?thesis by (case_tac obj', auto)
+ − 1847
qed moreover
+ − 1848
have "initp_intact (e#\<tau>)" using intactab tau ev valid nodel
+ − 1849
by (simp add:initp_intact_I_others) moreover
+ − 1850
have "obj2sobj (e#\<tau>) (File (new_childf pf \<tau>)) = SFile (t, sd) None"
+ − 1851
proof-
+ − 1852
have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = Some t"
+ − 1853
proof-
+ − 1854
have "etype_of_file (e#\<tau>) (new_childf pf \<tau>) = etype_of_file \<tau> pf"
+ − 1855
using ev tau SPab af'_cfd'(5)
+ − 1856
by (auto simp:obj2sobj.simps cp2sproc.simps ncf_parent etype_of_file_def
+ − 1857
split:option.splits intro!:etype_aux_prop3)
+ − 1858
thus ?thesis using SFab tau ev
+ − 1859
by (auto simp:obj2sobj.simps split:option.splits if_splits)
+ − 1860
qed
+ − 1861
moreover have "source_dir (e#\<tau>) (new_childf pf \<tau>) = Some sd"
+ − 1862
using ev tau SFab SPab valid ncf_parent
+ − 1863
by (auto simp:source_dir_simps obj2sobj.simps
+ − 1864
split:if_splits option.splits)
+ − 1865
ultimately show ?thesis using nodel ncf_notin_curf[where s = \<tau>]
+ − 1866
nodel_imp_exists[where obj = "File (new_childf pf \<tau>)" and s =\<tau>]
+ − 1867
by (auto simp:obj2sobj.simps dest:no_del_event_cons_D)
+ − 1868
qed
+ − 1869
ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 1870
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and>
+ − 1871
initp_intact_but (s @ s') (SFile (t, sd) None) \<and>
+ − 1872
obj2sobj (s @ s') obj = SFile (t, sd) None \<and>
+ − 1873
exists (s @ s') obj \<and> sobj_source_eq_obj (SFile (t, sd) None) obj"
+ − 1874
using tau ev
+ − 1875
apply (rule_tac x = "e#sb@sa" in exI)
+ − 1876
by (rule_tac x = "File (new_childf pf \<tau>)" in exI, auto)
+ − 1877
qed
+ − 1878
next
+ − 1879
case (ai'_init i t)
+ − 1880
hence initi: "i \<in> init_ipcs" using init_ipc_has_type
+ − 1881
by (simp add:bidirect_in_init_def)
+ − 1882
show ?case
+ − 1883
proof (rule allI|rule impI|erule conjE)+
+ − 1884
fix s' obj' sobj'
+ − 1885
assume vss': "valid s'" and sobjs': "obj2sobj s' obj' = sobj'"
+ − 1886
and nodels': "no_del_event s'"and intacts':"initp_intact s'"
+ − 1887
and notboth: "not_both_sproc (SIPC t (Some i)) sobj'"
+ − 1888
and exso': "exists s' obj'"
+ − 1889
from nodels' initi have exi: "i \<in> current_ipcs s'"
+ − 1890
by (drule_tac obj = "IPC i" in nodel_imp_exists, simp+)
+ − 1891
have "obj2sobj s' (IPC i) = SIPC t (Some i)"
+ − 1892
proof-
+ − 1893
have "obj2sobj [] (IPC i) = SIPC t (Some i)"
+ − 1894
using ai'_init initi by (auto simp:obj2sobj.simps)
+ − 1895
thus ?thesis using vss' exi nodels' initi
+ − 1896
by (drule_tac obj2sobj_ipc_remains'', auto simp:obj2sobj.simps)
+ − 1897
qed
+ − 1898
thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 1899
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and>
+ − 1900
initp_intact_but (s @ s') (SIPC t (Some i)) \<and>
+ − 1901
obj2sobj (s @ s') obj = SIPC t (Some i) \<and>
+ − 1902
exists (s @ s') obj \<and> sobj_source_eq_obj (SIPC t (Some i)) obj"
+ − 1903
apply (rule_tac x = "[]" in exI, rule_tac x = "IPC i" in exI)
+ − 1904
by (simp add:vss' sobjs' nodels' intacts' exi exso' del:obj2sobj.simps)
+ − 1905
qed
+ − 1906
next
+ − 1907
case (ai'_cipc r fr pt u srp)
+ − 1908
show ?case
+ − 1909
proof (rule allI|rule impI|erule conjE)+
+ − 1910
fix s' obj' sobj'
+ − 1911
assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'"
+ − 1912
and Both:"not_both_sproc (SIPC (default_ipc_create_type r) None) sobj'"
+ − 1913
and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown"
+ − 1914
and exobj':"exists s' obj'"
+ − 1915
with ai'_cipc(1) notUkn obtain s p where
+ − 1916
SPab: "obj2sobj (s@s') (Proc p) = SProc (r,fr,pt,u) srp" and
+ − 1917
expab: "exists (s@s') (Proc p)" and vsab: "valid (s@s')" and
+ − 1918
soab: "obj2sobj (s@s') obj' = sobj'" and
+ − 1919
exsoab: "exists (s@s') obj'" and
+ − 1920
intactab: "initp_intact (s@s')" and
+ − 1921
nodelab: "no_del_event (s@s')"
+ − 1922
apply (drule_tac s'= "s'" and obj' = obj' in all_sobjs_E0, auto)
+ − 1923
apply (frule obj2sobj_proc, erule exE)
+ − 1924
by (auto intro:nodel_exists_remains)
+ − 1925
obtain e \<tau> where ev: "e = CreateIPC p (new_ipc \<tau>)" and tau: "\<tau>=s@s'" by auto
+ − 1926
+ − 1927
have valid: "valid (e # \<tau>)"
+ − 1928
proof-
+ − 1929
have "os_grant \<tau> e"
+ − 1930
using ev tau expab by (simp)
+ − 1931
moreover have "rc_grant \<tau> e"
+ − 1932
using ev tau ai'_cipc(3) SPab
+ − 1933
by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
+ − 1934
ultimately show ?thesis using vsab tau
+ − 1935
by (rule_tac vs_step, simp+)
+ − 1936
qed moreover
+ − 1937
have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover
+ − 1938
have exobj': "exists (e#\<tau>) obj'" using exsoab valid ev tau
+ − 1939
by (case_tac obj', simp+) moreover
+ − 1940
have "obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1941
proof-
+ − 1942
have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1943
using soab tau valid notUkn nodel ev exsoab
+ − 1944
by (auto intro!:obj2sobj_file_remains' simp:ncf_notin_curf)
+ − 1945
moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1946
using soab tau valid notUkn nodel ev exsoab
+ − 1947
by (auto intro!:obj2sobj_ipc_remains' simp:ncf_notin_curf)
+ − 1948
moreover have "\<And> p. obj' = Proc p \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 1949
using soab tau valid notUkn nodel ev exsoab
+ − 1950
by (auto simp:obj2sobj.simps cp2sproc_simps'
+ − 1951
simp del:cp2sproc.simps split:option.splits)
+ − 1952
ultimately show ?thesis by (case_tac obj', auto)
+ − 1953
qed moreover
+ − 1954
have "initp_intact (e#\<tau>)" using intactab tau ev valid nodel
+ − 1955
by (simp add:initp_intact_I_others) moreover
+ − 1956
have "obj2sobj (e#\<tau>) (IPC (new_ipc \<tau>)) = SIPC (default_ipc_create_type r) None"
+ − 1957
using ev tau SPab nodel
+ − 1958
nodel_imp_exists[where obj = "IPC (new_ipc \<tau>)" and s =\<tau>]
+ − 1959
by (auto simp:obj2sobj.simps ni_notin_curi cp2sproc.simps
+ − 1960
split:option.splits dest:no_del_event_cons_D)
+ − 1961
ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 1962
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and>
+ − 1963
initp_intact_but (s @ s') (SIPC (default_ipc_create_type r) None) \<and>
+ − 1964
obj2sobj (s @ s') obj = SIPC (default_ipc_create_type r) None \<and>
+ − 1965
exists (s @ s') obj \<and> sobj_source_eq_obj (SIPC (default_ipc_create_type r) None) obj"
+ − 1966
using tau ev
+ − 1967
by (rule_tac x = "e#s" in exI, rule_tac x = "IPC (new_ipc \<tau>)" in exI, auto)
+ − 1968
qed
+ − 1969
next
+ − 1970
case (ap'_init p r fr t u)
+ − 1971
hence initp: "p \<in> init_processes" using init_proc_has_role
+ − 1972
by (simp add:bidirect_in_init_def)
+ − 1973
show ?case
+ − 1974
proof (rule allI|rule impI|erule conjE)+
+ − 1975
fix s' obj' sobj'
+ − 1976
assume VSs': "valid s'" and SOs': "obj2sobj s' obj' = sobj'"
+ − 1977
and Nodels': "no_del_event s'"and Intacts':"initp_intact s'"
+ − 1978
and notboth: "not_both_sproc (SProc (r,fr,t,u) (Some p)) sobj'"
+ − 1979
and exso': "exists s' obj'"
+ − 1980
from Nodels' initp have exp: "p \<in> current_procs s'"
+ − 1981
apply (drule_tac obj = "Proc p" in nodel_imp_un_deleted)
+ − 1982
by (drule not_deleted_imp_exists, simp+)
+ − 1983
with Intacts' initp ap'_init
+ − 1984
have "obj2sobj s' (Proc p) = SProc (r, fr, t, u) (Some p)"
+ − 1985
by (auto simp:initp_intact_def split:option.splits)
+ − 1986
thus "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 1987
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and>
+ − 1988
initp_intact_but (s @ s') (SProc (r, fr, t, u) (Some p)) \<and>
+ − 1989
obj2sobj (s @ s') obj = SProc (r, fr, t, u) (Some p) \<and>
+ − 1990
exists (s @ s') obj \<and>
+ − 1991
sobj_source_eq_obj (SProc (r, fr, t, u) (Some p)) obj"
+ − 1992
apply (rule_tac x = "[]" in exI, rule_tac x = "Proc p" in exI)
+ − 1993
by (simp add:VSs' SOs' Nodels' Intacts' initp intact_imp_butp exp exso'
+ − 1994
del:obj2sobj.simps)
+ − 1995
qed
+ − 1996
next
+ − 1997
case (ap'_crole r fr t u srp r')
+ − 1998
show ?case
+ − 1999
proof (rule allI|rule impI|erule conjE)+
+ − 2000
fix s' obj' sobj'
+ − 2001
assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'"
+ − 2002
and Both:"not_both_sproc (SProc (r', fr, t, u) srp) sobj'"
+ − 2003
and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'"
+ − 2004
with ap'_crole(1,2) obtain s p where
+ − 2005
VSab: "valid (s@s')" and SOab': "obj2sobj (s@s') obj' = sobj'"
+ − 2006
and nodelab: "no_del_event (s@s')"
+ − 2007
and butab: "initp_intact_but (s@s') (SProc (r, fr, t, u) srp)"
+ − 2008
and SPab: "obj2sobj (s@s') (Proc p) = SProc (r, fr, t, u) srp"
+ − 2009
and exp:"exists (s@s') (Proc p)" and exobj':"exists (s@s') obj'"
+ − 2010
and sreq: "sobj_source_eq_obj (SProc (r, fr, t, u) srp) (Proc p)"
+ − 2011
by (blast dest:not_both_I obj2sobj_proc intro:nodel_exists_remains)
+ − 2012
from VSab SPab sreq exp have srpeq: "srp = Some p"
+ − 2013
by (simp add:proc_source_eq_prop)
+ − 2014
with exp VSab SPab have initp: "p \<in> init_processes"
+ − 2015
by (auto dest:source_proc_in_init simp:obj2sobj.simps split:option.splits)
+ − 2016
obtain e \<tau> where ev: "e = ChangeRole p r'"
+ − 2017
and tau: "\<tau> = Clone p (new_proc (s@s'))#s@s'" by auto
+ − 2018
hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit)
+ − 2019
+ − 2020
have valid: "valid (e#\<tau>)"
+ − 2021
proof-
+ − 2022
have "os_grant \<tau> e"
+ − 2023
using ev tau exp by (simp)
+ − 2024
moreover have "rc_grant \<tau> e"
+ − 2025
using ev tau ap'_crole(3) SPab
+ − 2026
by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
+ − 2027
ultimately show ?thesis using vs_tau
+ − 2028
by (erule_tac vs_step, simp+)
+ − 2029
qed moreover
+ − 2030
have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover
+ − 2031
have "initp_intact_but (e#\<tau>) (SProc (r', fr, t, u) srp)"
+ − 2032
using butab tau ev valid initp srpeq nodel
+ − 2033
by (simp add:initp_intact_butp_I_crole) moreover
+ − 2034
have exobj': "exists (e#\<tau>) obj'" using exobj' valid ev tau
+ − 2035
by (case_tac obj', simp+) moreover
+ − 2036
have "obj2sobj (e#\<tau>) obj' = sobj'"
+ − 2037
proof-
+ − 2038
have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 2039
using SOab' tau ev valid notUkn nodel exobj'
+ − 2040
obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]
+ − 2041
by (auto)
+ − 2042
moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 2043
using SOab' tau ev valid notUkn nodel exobj'
+ − 2044
obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]
+ − 2045
by auto
+ − 2046
moreover have "\<And> p. obj' = Proc p \<Longrightarrow>False"
+ − 2047
using Both SOab' notUkn
+ − 2048
by (simp del:obj2sobj.simps, drule_tac obj2sobj_proc', auto)
+ − 2049
ultimately show ?thesis by (case_tac obj', auto)
+ − 2050
qed moreover
+ − 2051
have "obj2sobj (e#\<tau>) (Proc p) = SProc (r', fr, t, u) srp"
+ − 2052
using SPab tau vs_tau ev valid
+ − 2053
by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:cp2sproc.simps
+ − 2054
split:option.splits) moreover
+ − 2055
have "exists (e#\<tau>) (Proc p)" using exp tau ev by simp moreover
+ − 2056
have "sobj_source_eq_obj (SProc (r', fr, t, u) srp) (Proc p)"
+ − 2057
using sreq by (case_tac srp, simp+)
+ − 2058
ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 2059
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and>
+ − 2060
initp_intact_but (s @ s') (SProc (r', fr, t, u) srp) \<and>
+ − 2061
obj2sobj (s @ s') obj = SProc (r', fr, t, u) srp \<and>
+ − 2062
exists (s @ s') obj \<and> sobj_source_eq_obj (SProc (r', fr, t, u) srp) obj"
+ − 2063
using ev tau
+ − 2064
apply (rule_tac x = "e # Clone p (new_proc (s @ s')) # s" in exI)
+ − 2065
by (rule_tac x = "Proc p" in exI, auto)
+ − 2066
qed
+ − 2067
next
+ − 2068
case (ap'_chown r fr t u srp u' nr)
+ − 2069
show ?case
+ − 2070
proof (rule allI|rule impI|erule conjE)+
+ − 2071
fix s' obj' sobj'
+ − 2072
assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'"
+ − 2073
and Both:"not_both_sproc (SProc (nr,fr,chown_type_aux r nr t,u') srp) sobj'"
+ − 2074
and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'"
+ − 2075
with ap'_chown(1,2) obtain s p where
+ − 2076
VSab: "valid (s@s')" and SOab': "obj2sobj (s@s') obj' = sobj'"
+ − 2077
and nodelab: "no_del_event (s@s')"
+ − 2078
and butab: "initp_intact_but (s@s') (SProc (r, fr, t, u) srp)"
+ − 2079
and SPab: "obj2sobj (s@s') (Proc p) = SProc (r, fr, t, u) srp"
+ − 2080
and exp:"exists (s@s') (Proc p)" and exobj':"exists (s@s') obj'"
+ − 2081
and sreq: "sobj_source_eq_obj (SProc (r, fr, t, u) srp) (Proc p)"
+ − 2082
by (blast dest:not_both_I obj2sobj_proc intro:nodel_exists_remains)
+ − 2083
from VSab SPab sreq exp have srpeq: "srp = Some p"
+ − 2084
by (simp add:proc_source_eq_prop)
+ − 2085
with exp VSab SPab have initp: "p \<in> init_processes"
+ − 2086
by (auto dest:source_proc_in_init simp:obj2sobj.simps split:option.splits)
+ − 2087
obtain e \<tau> where ev: "e = ChangeOwner p u'"
+ − 2088
and tau: "\<tau> = Clone p (new_proc (s@s'))#s@s'" by auto
+ − 2089
hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit)
+ − 2090
+ − 2091
have valid: "valid (e#\<tau>)"
+ − 2092
proof-
+ − 2093
have "os_grant \<tau> e"
+ − 2094
using ev tau exp ap'_chown(3) by (simp)
+ − 2095
moreover have "rc_grant \<tau> e"
+ − 2096
using ev tau ap'_chown(5) SPab
+ − 2097
by (auto simp:cp2sproc.simps obj2sobj.simps pct_def clone_type_unchange
+ − 2098
split:option.splits t_rc_proc_type.splits)
+ − 2099
(* here is another place of no_limit of clone event assumption *)
+ − 2100
ultimately show ?thesis using vs_tau
+ − 2101
by (erule_tac vs_step, simp+)
+ − 2102
qed moreover
+ − 2103
have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover
+ − 2104
have "initp_intact_but (e#\<tau>) (SProc (nr,fr,chown_type_aux r nr t,u') srp)"
+ − 2105
using butab tau ev valid initp srpeq nodel
+ − 2106
by (simp add:initp_intact_butp_I_chown) moreover
+ − 2107
have exobj': "exists (e#\<tau>) obj'" using exobj' valid ev tau
+ − 2108
by (case_tac obj', simp+) moreover
+ − 2109
have "obj2sobj (e#\<tau>) obj' = sobj'"
+ − 2110
proof-
+ − 2111
have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 2112
using SOab' tau ev valid notUkn nodel exobj'
+ − 2113
obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]
+ − 2114
by (auto)
+ − 2115
moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 2116
using SOab' tau ev valid notUkn nodel exobj'
+ − 2117
obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (s @ s'))]"]
+ − 2118
by auto
+ − 2119
moreover have "\<And> p. obj' = Proc p \<Longrightarrow>False"
+ − 2120
using Both SOab' notUkn
+ − 2121
by (simp del:obj2sobj.simps, drule_tac obj2sobj_proc', auto)
+ − 2122
ultimately show ?thesis by (case_tac obj', auto)
+ − 2123
qed moreover
+ − 2124
have "obj2sobj (e#\<tau>) (Proc p) = SProc (nr,fr,chown_type_aux r nr t,u') srp"
+ − 2125
using SPab tau vs_tau ev valid ap'_chown(4)
+ − 2126
by (auto simp:obj2sobj.simps cp2sproc_simps' simp del:cp2sproc.simps
+ − 2127
split:option.splits) moreover
+ − 2128
have "exists (e#\<tau>) (Proc p)" using exp tau ev by simp moreover
+ − 2129
have "sobj_source_eq_obj (SProc (nr,fr,chown_type_aux r nr t,u') srp) (Proc p)"
+ − 2130
using sreq by (case_tac srp, simp+)
+ − 2131
ultimately show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 2132
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and>
+ − 2133
initp_intact_but (s @ s') (SProc (nr,fr,chown_type_aux r nr t,u') srp) \<and>
+ − 2134
obj2sobj (s @ s') obj = SProc (nr,fr,chown_type_aux r nr t,u') srp \<and>
+ − 2135
exists (s @ s') obj \<and> sobj_source_eq_obj (SProc (nr,fr,chown_type_aux r nr t,u') srp) obj"
+ − 2136
using ev tau
+ − 2137
apply (rule_tac x = "e # Clone p (new_proc (s @ s')) # s" in exI)
+ − 2138
by (rule_tac x = "Proc p" in exI, auto)
+ − 2139
qed
+ − 2140
next
+ − 2141
case (ap'_exec r fr pt u sp t sd sf r' fr')
+ − 2142
show ?case
+ − 2143
proof (rule allI|rule impI|erule conjE)+
+ − 2144
fix s' obj' sobj'
+ − 2145
assume "valid s'" and "obj2sobj s' obj' = sobj'" and "no_del_event s'"
+ − 2146
and Both:"not_both_sproc (SProc (r', fr', exec_type_aux r pt, u) sp) sobj'"
+ − 2147
and "initp_intact s'" and notUkn: "sobj' \<noteq> Unknown" and "exists s' obj'"
+ − 2148
with ap'_exec(3,4) obtain sa f where
+ − 2149
SFa: "obj2sobj (sa @ s') (File f) = SFile (t, sd) sf" and
+ − 2150
Exfa: "exists (sa @ s') (File f)" and
+ − 2151
buta: "initp_intact (sa @ s')" and
+ − 2152
othersa:"valid (sa @ s') \<and> obj2sobj (sa @ s') obj' = sobj' \<and> exists (sa @s') obj' \<and>
+ − 2153
no_del_event (sa @ s') \<and> sobj_source_eq_obj (SFile (t, sd) sf) (File f)"
+ − 2154
apply (simp only:not_both_sproc.simps)
+ − 2155
apply (erule_tac x = s' in allE, erule_tac x = obj' in allE)
+ − 2156
apply (erule_tac x = sobj' in allE, auto)
+ − 2157
by (frule obj2sobj_file, auto intro:nodel_exists_remains)
+ − 2158
with SFa Exfa othersa ap'_exec(1,2) Both notUkn obtain sb p where
+ − 2159
VSab: "valid (sb@sa@s')" and SOab': "obj2sobj (sb@sa@s') obj' = sobj'"
+ − 2160
and nodelab: "no_del_event (sb@sa@s')"
+ − 2161
and butab: "initp_intact_but (sb@sa@s') (SProc (r, fr, pt, u) sp)"
+ − 2162
and SPab: "obj2sobj (sb@sa@s') (Proc p) = SProc (r, fr, pt, u) sp"
+ − 2163
and exp:"exists (sb@sa@s') (Proc p)" and exobj':"exists (sb@sa@s') obj'"
+ − 2164
and sreq: "sobj_source_eq_obj (SProc (r, fr, pt, u) sp) (Proc p)"
+ − 2165
by (blast dest:not_both_I obj2sobj_proc intro:nodel_exists_remains)
+ − 2166
from VSab SPab sreq exp have srpeq: "sp = Some p" by (simp add:proc_source_eq_prop)
+ − 2167
with exp VSab SPab have initp: "p \<in> init_processes"
+ − 2168
by (auto dest:source_proc_in_init simp:obj2sobj.simps split:option.splits)
+ − 2169
obtain e \<tau> where ev: "e = Execute p f"
+ − 2170
and tau: "\<tau> = Clone p (new_proc (sb@sa@s'))#sb@sa@s'" by auto
+ − 2171
hence vs_tau:"valid \<tau>" using exp VSab by (auto intro:clone_event_no_limit)
+ − 2172
from Exfa nodelab have exf:"f \<in> current_files (sb@sa@s')"
+ − 2173
apply (drule_tac obj = "File f" in nodel_imp_un_deleted)
+ − 2174
by (drule_tac s' = "sb" in not_deleted_imp_exists', auto)
+ − 2175
from SFa VSab Exfa nodelab have SFab: "obj2sobj (sb@sa@s') (File f) = SFile (t,sd) sf"
+ − 2176
by (rule_tac s = "sa@s'" in obj2sobj_file_remains'', simp_all)
+ − 2177
+ − 2178
have valid: "valid (e#\<tau>)"
+ − 2179
proof-
+ − 2180
have "os_grant \<tau> e"
+ − 2181
using ev tau exp by (simp add:exf)
+ − 2182
moreover have "rc_grant \<tau> e"
+ − 2183
using ev tau ap'_exec(5) SPab SFab
+ − 2184
by (auto simp:etype_of_file_def cp2sproc.simps obj2sobj.simps
+ − 2185
split:if_splits option.splits)
+ − 2186
ultimately show ?thesis using vs_tau
+ − 2187
by (erule_tac vs_step, simp+)
+ − 2188
qed moreover
+ − 2189
have nodel: "no_del_event (e#\<tau>)" using nodelab tau ev by simp moreover
+ − 2190
have "initp_intact_but (e#\<tau>) (SProc (r', fr', exec_type_aux r pt, u) sp)"
+ − 2191
using butab tau ev valid initp srpeq nodel
+ − 2192
by (simp add:initp_intact_butp_I_exec) moreover
+ − 2193
have exobj': "exists (e#\<tau>) obj'" using exobj' valid ev tau
+ − 2194
by (case_tac obj', simp+) moreover
+ − 2195
have "obj2sobj (e#\<tau>) obj' = sobj'"
+ − 2196
proof-
+ − 2197
have "\<And> f. obj' = File f \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 2198
using SOab' tau ev valid notUkn nodel exobj'
+ − 2199
obj2sobj_file_remains''[where s'="[e,Clone p (new_proc (sb @ sa @ s'))]"]
+ − 2200
by (auto simp del:obj2sobj.simps)
+ − 2201
moreover have "\<And> i. obj' = IPC i \<Longrightarrow> obj2sobj (e#\<tau>) obj' = sobj'"
+ − 2202
using SOab' tau ev valid notUkn nodel exobj'
+ − 2203
obj2sobj_ipc_remains''[where s'="[e,Clone p (new_proc (sb @ sa @ s'))]"]
+ − 2204
by (auto simp del:obj2sobj.simps)
+ − 2205
moreover have "\<And> p. obj' = Proc p \<Longrightarrow>False"
+ − 2206
using Both SOab' notUkn
+ − 2207
by (simp del:obj2sobj.simps, drule_tac obj2sobj_proc', auto)
+ − 2208
ultimately show ?thesis by (case_tac obj', auto)
+ − 2209
qed moreover
+ − 2210
have "obj2sobj (e#\<tau>) (Proc p) = SProc (r',fr',exec_type_aux r pt, u) sp"
+ − 2211
proof-
+ − 2212
have "obj2sobj \<tau> (Proc p) = SProc (r,fr,pt,u) sp" using SPab tau vs_tau
+ − 2213
by (auto split:option.splits simp:cp2sproc_simps' obj2sobj.simps)
+ − 2214
moreover have "source_dir \<tau> f = Some sd" using vs_tau SFab tau
+ − 2215
by (auto simp:source_dir_simps obj2sobj.simps split:option.splits if_splits)
+ − 2216
ultimately show ?thesis using valid ev ap'_exec(6,7)
+ − 2217
by (auto simp:cp2sproc_exec obj2sobj.simps split:option.splits)
+ − 2218
qed moreover
+ − 2219
have "exists (e#\<tau>) (Proc p)" using exp tau ev by simp moreover
+ − 2220
have "sobj_source_eq_obj (SProc (r',fr',exec_type_aux r pt,u) sp) (Proc p)"
+ − 2221
using sreq by (case_tac sp, simp+)
+ − 2222
ultimately
+ − 2223
show "\<exists>s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and>
+ − 2224
exists (s @ s') obj' \<and> no_del_event (s @ s') \<and>
+ − 2225
initp_intact_but (s @ s') (SProc (r', fr', exec_type_aux r pt, u) sp) \<and>
+ − 2226
obj2sobj (s @ s') obj = SProc (r', fr', exec_type_aux r pt, u) sp \<and>
+ − 2227
exists (s @ s') obj \<and>
+ − 2228
sobj_source_eq_obj (SProc (r', fr', exec_type_aux r pt, u) sp) obj"
+ − 2229
using ev tau
+ − 2230
apply (rule_tac x = "e#Clone p (new_proc (sb @ sa @ s')) #sb@sa" in exI)
+ − 2231
by (rule_tac x = "Proc p" in exI, auto)
+ − 2232
qed
+ − 2233
qed
+ − 2234
+ − 2235
lemma all_sobjs_E2:
+ − 2236
"\<lbrakk>sobj \<in> all_sobjs'; valid s'; obj2sobj s' obj' = sobj'; exists s' obj'; sobj' \<noteq> Unknown;
+ − 2237
not_both_sproc sobj sobj'; no_del_event s'; initp_intact s'\<rbrakk>
+ − 2238
\<Longrightarrow> \<exists> s obj. valid (s @ s') \<and> obj2sobj (s @ s') obj' = sobj' \<and> exists (s@s') obj \<and>
+ − 2239
no_del_event (s @ s') \<and> initp_intact_but (s @ s') sobj \<and>
+ − 2240
obj2sobj (s @ s') obj = sobj \<and> exists (s @ s') obj \<and>
+ − 2241
sobj_source_eq_obj sobj obj"
+ − 2242
by (drule all_sobjs_E2_aux, auto)
+ − 2243
+ − 2244
end
+ − 2245
+ − 2246
end