1256 apply (rule disjI2, rule conjI, rule disjI2, rule_tac x = obj in exI) |
1256 apply (rule disjI2, rule conjI, rule disjI2, rule_tac x = obj in exI) |
1257 apply (frule_tac obj = obj in co2sobj_closefd, simp) |
1257 apply (frule_tac obj = obj in co2sobj_closefd, simp) |
1258 apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] |
1258 apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] |
1259 apply (rule notI, simp add:co2sobj.simps split:option.splits) |
1259 apply (rule notI, simp add:co2sobj.simps split:option.splits) |
1260 apply (case_tac "f = a", simp add:alive_simps) |
1260 apply (case_tac "f = a", simp add:alive_simps) |
1261 apply (case_tac "f \<in> same_inode_files s a", rule disjI2) |
1261 apply (case_tac "f \<in> same_inode_files s a", rule disjI1) |
1262 apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits) |
1262 apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits) |
1263 apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop) |
1263 apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop) |
1264 |
|
1265 |
|
1266 apply (erule bexE, erule conjE) |
1264 apply (erule bexE, erule conjE) |
1267 apply (rule conjI, rule_tac x = "O_file f''" in exI) |
1265 apply (erule_tac x = f'' in ballE, simp, simp) |
1268 apply (simp add:same_inode_files_prop11 co2sobj.simps tainted_eq_Tainted cf2sfiles_prop same_inodes_Tainted) |
1266 apply (rule disjI2, rule conjI, rule disjI2, rule_tac x = obj in exI) |
|
1267 apply (simp add:is_file_simps co2sobj_closefd tainted_eq_Tainted) |
|
1268 apply (rule notI, simp add:co2sobj_closefd) |
|
1269 apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps tainted_eq_Tainted) |
|
1270 apply (rule disjI2, rule conjI, rule disjI2, rule_tac x = obj in exI) |
|
1271 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) |
|
1272 apply (rule notI, simp add:co2sobj.simps split:option.splits) |
|
1273 apply (rule disjI2, rule conjI, rule disjI2, rule_tac x = obj in exI) |
|
1274 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) |
|
1275 apply (rule notI, simp add:co2sobj.simps split:option.splits) |
|
1276 apply (rule disjI2, rule conjI, rule disjI2, rule_tac x = obj in exI) |
|
1277 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) |
|
1278 apply (rule notI, simp add:co2sobj.simps split:option.splits) |
|
1279 apply (rule impI, rule conjI, rule impI) |
|
1280 |
|
1281 apply (erule_tac obj = obj in co2sobj_some_caseD) |
|
1282 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted) |
1269 apply (rule notI, simp) |
1283 apply (rule notI, simp) |
1270 apply (rule disjI2, rule conjI, rule_tac x = obj in exI) |
1284 apply (rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI) |
1271 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) |
1285 apply (frule_tac obj = obj in co2sobj_closefd, simp) |
|
1286 apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] |
|
1287 apply (erule_tac x = obj in allE, simp add:co2sobj_closefd) |
|
1288 apply (rule notI, simp add:co2sobj.simps split:option.splits) |
|
1289 apply (case_tac "f = a", simp add:alive_simps) |
|
1290 apply (case_tac "f \<in> same_inode_files s a", rule conjI, rule disjI2, rule conjI) |
|
1291 apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits) |
|
1292 apply (simp add:co2sobj.simps) |
1272 apply (rule notI, simp add:co2sobj.simps) |
1293 apply (rule notI, simp add:co2sobj.simps) |
1273 apply (rule disjI2, rule conjI, rule_tac x = obj in exI) |
1294 apply (rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI) |
1274 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) |
1295 apply (simp add:is_file_simps co2sobj_closefd tainted_eq_Tainted) |
|
1296 apply (rule notI, simp add:co2sobj.simps) |
|
1297 apply (rule notI, simp add:co2sobj_closefd tainted_eq_Tainted) |
|
1298 apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps tainted_eq_Tainted) |
|
1299 apply (rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI) |
|
1300 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) |
|
1301 apply (rule notI, simp add:co2sobj.simps split:option.splits)+ |
|
1302 apply (rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI) |
|
1303 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) |
|
1304 apply (rule notI, simp add:co2sobj.simps split:option.splits)+ |
|
1305 apply (rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI) |
|
1306 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) |
|
1307 apply (rule notI, simp add:co2sobj.simps split:option.splits)+ |
|
1308 apply (rule impI) |
|
1309 apply (erule_tac obj = obj in co2sobj_some_caseD) |
|
1310 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted) |
|
1311 apply (rule disjI2, rule notI, simp) |
|
1312 apply (rule disjI2, rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI) |
|
1313 apply (frule_tac obj = obj in co2sobj_closefd, simp) |
|
1314 apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] |
|
1315 apply (erule_tac x = obj in allE, simp add:co2sobj_closefd) |
1275 apply (rule notI, simp add:co2sobj.simps split:option.splits) |
1316 apply (rule notI, simp add:co2sobj.simps split:option.splits) |
1276 apply (rule disjI2, rule conjI, rule_tac x = obj in exI) |
1317 apply (case_tac "f = a", simp add:alive_simps) |
1277 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) |
1318 apply (case_tac "f \<in> same_inode_files s a", rule disjI1) |
1278 apply (rule notI, simp add:co2sobj.simps split:option.splits) |
1319 apply (simp add:co2sobj_closefd split:if_splits option.splits t_sobject.splits) |
1279 apply (rule disjI2, rule conjI, rule_tac x = obj in exI) |
1320 apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_Tainted tainted_eq_Tainted) |
1280 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) |
1321 apply (erule bexE, erule conjE, erule_tac x = "f''" in ballE, simp, simp) |
1281 apply (rule notI, simp add:co2sobj.simps split:option.splits) |
1322 apply (rule disjI2, rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI) |
1282 |
1323 apply (simp add:is_file_simps co2sobj_closefd tainted_eq_Tainted) |
1283 apply (erule bexE, erule conjE) |
1324 apply (rule notI, simp add:co2sobj.simps) |
1284 apply (simp add:update_s2ss_obj_def split:if_splits) |
1325 apply (rule notI, simp add:co2sobj_closefd tainted_eq_Tainted) |
1285 apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted) |
1326 apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps tainted_eq_Tainted) |
|
1327 apply (rule disjI2, rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI) |
|
1328 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) |
|
1329 apply (rule notI, simp add:co2sobj.simps split:option.splits)+ |
|
1330 apply (rule disjI2, rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI) |
|
1331 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) |
|
1332 apply (rule notI, simp add:co2sobj.simps split:option.splits)+ |
|
1333 apply (rule disjI2, rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI) |
|
1334 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) |
|
1335 apply (rule notI, simp add:co2sobj.simps split:option.splits)+ |
|
1336 |
|
1337 apply (simp add:update_s2ss_sfile_def update_s2ss_obj_def split:if_splits) |
|
1338 apply (erule conjE, erule disjE) |
|
1339 apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted) |
|
1340 apply (erule exE, erule conjE) |
|
1341 apply (case_tac "obj = O_file a", simp add:co2sobj.simps tainted_eq_Tainted) |
|
1342 apply (case_tac "obj = O_proc p") |
|
1343 apply (rule_tac x = obj' in exI, frule_tac obj = obj' in co2sobj_sproc_imp, erule exE) |
|
1344 apply (frule_tac obj = obj' in alive_co2sobj_closefd3, simp+) |
|
1345 apply (simp add:co2sobj_closefd) |
|
1346 apply (simp add:co2sobj.simps tainted_eq_Tainted) |
|
1347 apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+) |
|
1348 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd) |
|
1349 apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] |
|
1350 apply (erule conjE|erule exE|erule disjE)+ |
|
1351 apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted) |
|
1352 apply (erule conjE, erule exE, erule conjE) |
|
1353 apply (case_tac "obj = O_file a", simp add:co2sobj.simps tainted_eq_Tainted) |
|
1354 apply (case_tac "obj = O_proc p") |
|
1355 apply (simp add:co2sobj.simps tainted_eq_Tainted) |
|
1356 apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+) |
|
1357 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd) |
|
1358 apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] |
|
1359 apply (erule conjE|erule exE|erule disjE)+ |
|
1360 apply (drule same_inode_files_prop10, simp add:file_of_pfd_is_file, erule exE, erule conjE) |
|
1361 apply (rule_tac x = "O_file f'" in exI) |
|
1362 apply (frule same_inode_files_prop11) |
|
1363 apply (frule_tac obj = "O_file f'" in co2sobj_closefd) |
|
1364 apply (simp add:alive_simps)+ |
|
1365 apply (frule_tac f = "f'" in is_file_has_sfile', simp, erule exE) |
|
1366 apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted split:if_splits) |
|
1367 apply (rule impI, erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp) |
|
1368 apply (erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp) |
|
1369 apply (erule conjE, erule disjE) |
|
1370 apply (rule_tac x = "O_proc p" in exI) |
|
1371 apply (simp add:co2sobj.simps tainted_eq_Tainted) |
1286 apply (erule exE, erule conjE) |
1372 apply (erule exE, erule conjE) |
1287 apply (case_tac "obj = O_proc p") |
1373 apply (case_tac "obj = O_proc p") |
1288 apply (rule_tac x = obj' in exI) |
1374 apply (rule_tac x = "obj'" in exI, simp, frule_tac obj = obj' in co2sobj_sproc_imp, erule exE) |
1289 apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd) |
1375 apply (frule_tac obj = obj' in alive_co2sobj_closefd3, simp+) |
|
1376 apply (simp add:co2sobj_closefd tainted_eq_Tainted) |
1290 apply (simp add:co2sobj.simps tainted_eq_Tainted) |
1377 apply (simp add:co2sobj.simps tainted_eq_Tainted) |
1291 apply (case_tac "obj = O_file a") |
1378 apply (case_tac "obj = O_file a", simp add:co2sobj.simps tainted_eq_Tainted) |
|
1379 apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+) |
|
1380 apply (erule_tac obj = obj in co2sobj_some_caseD) |
|
1381 apply (rule_tac x = obj in exI) |
|
1382 apply (simp add:co2sobj_closefd) |
|
1383 apply (case_tac "f = a", simp add:alive_simps) |
|
1384 apply (case_tac "f \<in> same_inode_files s a") |
|
1385 apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted) |
|
1386 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd) |
|
1387 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd) |
|
1388 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd) |
|
1389 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd) |
|
1390 apply (erule disjE) |
|
1391 apply (drule same_inode_files_prop10, simp add:file_of_pfd_is_file, erule exE, erule conjE) |
1292 apply (rule_tac x = "O_file f'" in exI) |
1392 apply (rule_tac x = "O_file f'" in exI) |
1293 apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps same_inode_files_prop11) |
1393 apply (frule same_inode_files_prop11) |
1294 apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits) |
1394 apply (frule_tac obj = "O_file f'" in co2sobj_closefd) |
1295 apply (rule conjI) |
1395 apply (simp add:alive_simps)+ |
1296 apply (rule impI) |
1396 apply (frule_tac f = "f'" in is_file_has_sfile', simp, erule exE) |
1297 apply (rule_tac x = f' in ballE, simp, simp, simp) |
1397 apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted split:if_splits) |
1298 apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_Tainted) |
1398 apply (rule impI, erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp) |
1299 apply (rule_tac x = obj in exI) |
1399 apply (erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp) |
1300 apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+) |
1400 apply (erule conjE, erule disjE) |
1301 apply (frule_tac obj = obj in co2sobj_closefd, simp) |
1401 apply (rule_tac x = "O_proc p" in exI) |
1302 apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] |
1402 apply (simp add:co2sobj.simps tainted_eq_Tainted) |
1303 apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted) |
|
1304 apply (erule conjE, erule exE, erule conjE) |
1403 apply (erule conjE, erule exE, erule conjE) |
1305 apply (case_tac "obj = O_proc p") |
1404 apply (case_tac "obj = O_proc p", simp add:co2sobj.simps tainted_eq_Tainted) |
1306 apply (simp add:co2sobj.simps tainted_eq_Tainted) |
1405 apply (case_tac "obj = O_file a", simp add:co2sobj.simps tainted_eq_Tainted) |
1307 apply (case_tac "obj = O_file a") |
1406 apply (erule_tac obj = obj in co2sobj_some_caseD) |
1308 apply (rule_tac x = "O_file f'" in exI) |
1407 apply (rule_tac x = obj in exI) |
1309 apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps same_inode_files_prop11) |
1408 apply (simp add:co2sobj_closefd) |
1310 apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits) |
1409 apply (case_tac "f \<in> same_inode_files s a") |
1311 apply (rule conjI) |
1410 apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted) |
1312 apply (rule impI) |
1411 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd is_file_simps) |
1313 apply (rule_tac x = f' in ballE, simp, simp, simp) |
1412 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd) |
1314 apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_Tainted) |
1413 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd is_dir_simps) |
1315 apply (rule_tac x = obj in exI) |
1414 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd) |
1316 apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+) |
1415 |
1317 apply (frule_tac obj = obj in co2sobj_closefd, simp) |
|
1318 apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] |
|
1319 |
|
1320 |
|
1321 |
|
1322 |
|
1323 |
|
1324 apply |
|
1325 |
|
1326 defer |
|
1327 apply (rule impI) |
1416 apply (rule impI) |
1328 apply (simp add:update_s2ss_obj_def) |
1417 apply (simp add:update_s2ss_obj_def) |
1329 apply (rule conjI, rule impI, erule exE, erule conjE) |
1418 apply (rule conjI, rule impI, erule exE, erule conjE) |
1330 apply (simp add:s2ss_def) |
1419 apply (simp add:s2ss_def) |
1331 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE) |
1420 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE) |