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