1459 lemma alive_co2sobj_unlink:

  1460   "\<lbrakk>alive s obj; valid (UnLink p f # s); obj \<noteq> O_file f\<rbrakk>

  1461    \<Longrightarrow> alive (UnLink p f # s) obj"

  1462 by (auto simp add:alive_simps split:t_object.splits)

  1463 

  1464 lemma s2ss_unlink:

  1465   "valid (UnLink p f # s) \<Longrightarrow> s2ss (UnLink p f # s) = (

  1466      if (proc_fd_of_file s f = {}) 

  1467      then (case (cf2sfile s f) of 

  1468              Some sf \<Rightarrow> del_s2ss_file s (s2ss s) f sf

  1469            | _       \<Rightarrow> {})

  1470      else s2ss s)"

  1471 apply (frule vd_cons, frule vt_grant_os, clarsimp split:if_splits)

  1472 apply (frule is_file_has_sfile', simp, erule exE, simp)

  1473 apply (rule conjI, rule impI)

  1474 apply (simp add:update_s2ss_sfile_def del_s2ss_file_def)

  1475 apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+ defer

  1476 apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+ 

  1477 

  1478 apply (simp add:s2ss_def)

  1479 apply (tactic {*my_seteq_tac 1*})

  1480 apply (case_tac "obj = O_file f", simp add:is_file_simps)

  1481 apply simp

  1482 apply (rule conjI)

  1483 apply (rule_tac x = obj in exI,simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits)

  1484 apply (simp add:co2sobj.simps)

  1485 apply (simp add:co2sobj.simps)

  1486 apply (rule notI, simp, frule_tac obj = obj in co2sobj_sfile_imp, erule exE, simp)

  1487 apply (frule_tac obj = obj in co2sobj_unlink, simp)

  1488 apply (erule_tac x = fa in allE, simp add:is_file_simps)

  1489 apply (simp add:co2sobj.simps tainted_eq_Tainted)

  1490 apply (tactic {*my_setiff_tac 1*})

  1491 apply (case_tac "obj = O_file f", simp add:co2sobj.simps tainted_eq_Tainted)

  1492 apply (frule_tac alive_co2sobj_unlink, simp, simp)

  1493 apply (frule_tac obj = obj in co2sobj_unlink, simp)

  1494 apply (rule_tac x = obj in exI)

  1495 apply (simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)

  1496 

  1497 apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+  defer

  1498 

  1499 apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+ 

  1500 apply (simp add:s2ss_def)

  1501 apply (tactic {*my_seteq_tac 1*})

  1502 apply (case_tac "obj = O_file f", simp add:alive_simps)

  1503 apply (erule_tac obj = obj in co2sobj_some_caseD)

  1504 apply (rule disjI2, simp, rule_tac x = obj in exI)

  1505 apply (simp add:co2sobj_unlink)

  1506 apply (case_tac "fa \<in> same_inode_files s f")

  1507 apply (rule disjI1)

  1508 apply (simp add:co2sobj_unlink)

  1509 apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop split:if_splits)

  1510 apply (erule bexE, erule_tac x = f'' in ballE, simp, simp)

  1511 apply (rule disjI2, simp, rule_tac x = obj in exI)

  1512 apply (simp add:co2sobj_unlink is_file_simps)

  1513 apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_unlink)

  1514 apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps)

  1515 apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_unlink)

  1516 apply (tactic {*my_setiff_tac 1*})

  1517 apply (drule same_inode_files_prop10, simp, erule exE, erule conjE)

  1518 apply (rule_tac x = "O_file f'a" in exI, simp add:is_file_simps)

  1519 apply (frule_tac obj = "O_file f'a" in co2sobj_unlink, simp add:same_inode_files_prop11 is_file_simps)

  1520 apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop 

  1521   is_file_simps same_inode_files_prop11 split:if_splits)

  1522 apply (rule impI, erule bexE, erule_tac x = f'' in ballE, simp, simp)

  1523 apply (erule bexE, erule_tac x = f'' in ballE, simp, simp)

  1524 

  1525 apply (tactic {*my_setiff_tac 1*})

  1526 apply (case_tac "f' = f", simp add:same_inode_files_prop9) 

  1527 apply (case_tac "obj= O_file f")

  1528 apply (rule_tac x = "O_file f'" in exI, simp add:is_file_simps)

  1529 apply (frule_tac f' = f' in cf2sfiles_unlink, simp add:current_files_simps is_file_in_current)

  1530 apply (simp add:co2sobj.simps tainted_eq_Tainted)

  1531 apply (erule_tac obj = obj in co2sobj_some_caseD)

  1532 apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)

  1533 apply (case_tac "fa \<in> same_inode_files s f")

  1534 apply (rule_tac x = "O_file f'" in exI)

  1535 apply (frule_tac f' = f' in cf2sfiles_unlink, simp add:current_files_simps is_file_in_current)

  1536 apply (simp add:co2sobj.simps tainted_eq_Tainted is_file_simps cf2sfiles_prop same_inodes_Tainted)

  1537 apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps)

  1538 apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)

  1539 apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps)

  1540 apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)

  1541 

  1542 apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+  defer

  1543 

  1544 apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+ 

  1545 apply (simp add:s2ss_def)

  1546 apply (tactic {*my_seteq_tac 1*})

  1547 apply (case_tac "obj = O_file f", simp add:alive_simps, simp)

  1548 apply (erule_tac obj = obj in co2sobj_some_caseD)

  1549 apply (rule disjI2, rule conjI, simp, rule_tac x = obj in exI)

  1550 apply (simp add:co2sobj_unlink)

  1551 apply (rule notI, simp add:co2sobj.simps split:option.splits)

  1552 apply (case_tac "fa \<in> same_inode_files s f")

  1553 apply (rule disjI1)

  1554 apply (simp add:co2sobj_unlink)

  1555 apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop split:if_splits)

  1556 apply (erule bexE, erule_tac x = f'' in ballE, simp, simp)

  1557 apply (rule disjI2, rule conjI, simp, rule_tac x = obj in exI)

  1558 apply (simp add:co2sobj_unlink is_file_simps)

  1559 apply (rule notI, simp add:co2sobj_unlink tainted_eq_Tainted)

  1560 apply (erule_tac x = fa in allE, simp add:co2sobj.simps is_file_simps tainted_eq_Tainted)

  1561 apply (rule disjI2, rule conjI, simp, rule_tac x = obj in exI, simp add:co2sobj_unlink)

  1562 apply (rule notI, simp add:co2sobj.simps split:option.splits)

  1563 apply (rule disjI2, rule conjI, simp, rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps)

  1564 apply (rule notI, simp add:co2sobj.simps split:option.splits)

  1565 apply (rule disjI2, rule conjI, simp, rule_tac x = obj in exI, simp add:co2sobj_unlink)

  1566 apply (rule notI, simp add:co2sobj.simps split:option.splits)

  1567 apply (tactic {*my_setiff_tac 1*})

  1568 apply (drule same_inode_files_prop10, simp, erule exE, erule conjE)

  1569 apply (rule_tac x = "O_file f'" in exI, simp add:is_file_simps)

  1570 apply (frule_tac obj = "O_file f'" in co2sobj_unlink, simp add:same_inode_files_prop11 is_file_simps)

  1571 apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop 

  1572   is_file_simps same_inode_files_prop11 split:if_splits)

  1573 apply (rule impI, erule bexE, erule_tac x = f'' in ballE, simp, simp)

  1574 apply (erule bexE, erule_tac x = f'' in ballE, simp, simp)

  1575 apply (tactic {*my_setiff_tac 1*}, simp)

  1576 apply (case_tac "obj = O_file f", simp add:co2sobj.simps tainted_eq_Tainted)

  1577 apply (erule_tac obj = obj in co2sobj_some_caseD)

  1578 apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)

  1579 apply (case_tac "fa \<in> same_inode_files s f")

  1580 apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_Tainted tainted_eq_Tainted)

  1581 apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps)

  1582 apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)

  1583 apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps)

  1584 apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)

  1585 

  1586 

  1587 

  1588