1586 

  1586 apply (rule impI)

  1587 apply (simp add:s2ss_def)

  1588 apply (tactic {*my_seteq_tac 1*})

  1589 apply (rule_tac x = obj in exI)

  1590 apply (simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits)

  1591 apply (simp add:co2sobj.simps)

  1592 apply (simp add:co2sobj.simps)

  1593 apply (tactic {*my_setiff_tac 1*})

  1594 apply (rule_tac x = obj in exI)

  1595 apply (subgoal_tac "alive (UnLink p f # s) obj")

  1596 apply (auto simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits)[1]

  1597 apply (auto simp add:co2sobj_unlink alive_simps split:t_object.splits)[1]

  1598 

  1599 apply (simp add:s2ss_def)

  1600 apply (tactic {*my_seteq_tac 1*})

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

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

  1603 apply (simp add:co2sobj.simps)

  1604 apply (simp add:co2sobj.simps)

  1605 apply (tactic {*my_setiff_tac 1*})

  1606 apply (case_tac "obj = O_file f")

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

  1608 apply (auto simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits)[1]

  1609 apply (rule_tac x =obj in exI)

  1610 apply (subgoal_tac "alive (UnLink p f # s) obj")

  1611 apply (auto simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits)[1]

  1612 apply (auto simp add:co2sobj_unlink alive_simps split:t_object.splits)[1]

  1613 

  1614 apply (simp add:s2ss_def)

  1615 apply (tactic {*my_seteq_tac 1*})

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

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

  1618 apply (simp add:co2sobj.simps)

  1619 apply (simp add:co2sobj.simps)

  1620 apply (tactic {*my_setiff_tac 1*})

  1621 apply (case_tac "obj = O_file f")

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

  1623 apply (auto simp add:co2sobj_unlink is_file_simps is_dir_simps same_inode_files_prop9 split:t_object.splits)[1]

  1624 apply (erule_tac obj = obj in co2sobj_some_caseD)

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

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

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

  1628 apply (simp add:alive_simps co2sobj.simps)

  1629 apply (rule conjI, rule notI, simp add:same_inode_files_prop9)

  1630 apply (rule impI, frule_tac f' = f' in cf2sfiles_unlink)

  1631 apply (simp add:current_files_simps is_file_simps is_file_in_current)

  1632 apply (simp add:tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop)

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

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

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

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

  1637 

  1638 apply (simp add:s2ss_def)

  1639 apply (tactic {*my_seteq_tac 1*})

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

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

  1642 apply (simp add:co2sobj.simps)

  1643 apply (simp add:co2sobj.simps)

  1644 apply (tactic {*my_setiff_tac 1*})

  1645 apply (case_tac "obj = O_file f")

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

  1647 apply (subgoal_tac "alive (UnLink p f # s) (O_file f')")

  1648 apply (frule same_inode_files_prop11, frule_tac f = f' in is_file_has_sfile', simp add:vd_cons, erule exE)

  1649 apply (frule_tac obj = "O_file f'" in co2sobj_unlink, simp)

  1650 apply (simp split:if_splits option.splits add:is_file_simps)

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

  1652 apply (auto split:t_sobject.splits)[1]

  1653 apply (simp add:is_file_simps same_inode_files_prop11)

  1654 apply (erule_tac obj = obj in co2sobj_some_caseD)

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

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

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

  1658 apply (subgoal_tac "alive (UnLink p f # s) (O_file f')")

  1659 apply (frule same_inode_files_prop11, frule_tac f = f' in is_file_has_sfile', simp add:vd_cons, erule exE)

  1660 apply (frule_tac obj = "O_file f'" in co2sobj_unlink, simp)

  1661 apply (simp split:if_splits option.splits add:is_file_simps)

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

  1663 apply (auto split:t_sobject.splits)[1]

  1664 apply (simp add:is_file_simps same_inode_files_prop11)

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

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

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

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

  1669 done

  1670 

  1671 definition del_s2ss_obj :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_object \<Rightarrow> t_sobject \<Rightarrow> t_static_state"

  1672 where

  1673   "del_s2ss_obj s ss obj sobj \<equiv> 

  1674      if (\<exists> obj'. alive s obj' \<and> obj' \<noteq> obj \<and> co2sobj s obj' = Some sobj)

  1675      then ss

  1676      else ss - {sobj}"

  1677 

  1678 lemma del_update_s2ss_obj:

  1679   "update_s2ss_obj s ss obj sobj sobj' = del_s2ss_obj s ss obj sobj \<union> {sobj'}"

  1680 by (auto simp:update_s2ss_obj_def del_s2ss_obj_def split:if_splits)

  1681 

  1682 lemma s2ss_rmdir: "valid (Rmdir p f # s) \<Longrightarrow> s2ss (Rmdir p f # s) = (

  1683   case (co2sobj s (O_dir f)) of

  1684     Some sdir \<Rightarrow> del_s2ss_obj s (s2ss s) (O_dir f) sdir

  1685   | _         \<Rightarrow> {})"

  1686 apply (frule vd_cons, frule vt_grant_os)

  1687 apply (clarsimp simp:dir_is_empty_def)

  1688 apply (frule is_dir_has_sdir', simp, erule exE)

  1689 apply (simp split:option.splits, rule conjI, rule impI, simp add:co2sobj.simps)

  1690 apply (rule allI, rule impI)

  1691 

  1692 apply (simp add:del_s2ss_obj_def)

  1693 apply (rule conjI|rule impI|erule exE|erule conjE)+

  1694 apply (simp add:s2ss_def)

  1695 apply (tactic {*my_seteq_tac 1*})

  1696 apply (rule_tac x = obj in exI)

  1697 apply (simp add:co2sobj_rmdir is_file_simps is_dir_simps alive_simps split:t_object.splits if_splits)

  1698 apply (tactic {*my_setiff_tac 1*})

  1699 apply (case_tac "obj = O_dir f")

  1700 apply (rule_tac x = obj' in exI)

  1701 apply (subgoal_tac "alive (Rmdir p f # s) obj'")

  1702 apply (auto simp add:co2sobj_rmdir is_file_simps is_dir_simps split:t_object.splits)[1]

  1703 apply (simp add:alive_rmdir)

  1704 apply (rule_tac x = obj in exI)

  1705 apply (subgoal_tac "alive (Rmdir p f # s) obj")

  1706 apply (auto simp add:co2sobj_rmdir is_file_simps is_dir_simps split:t_object.splits)[1]

  1707 apply (simp add:alive_rmdir)

  1708 

  1709 apply (rule conjI|rule impI|erule exE|erule conjE)+

  1710 apply (simp add:s2ss_def)

  1711 apply (tactic {*my_seteq_tac 1*})

  1712 apply simp

  1713 apply (case_tac "obj = O_dir f", simp add:alive_rmdir)

  1714 apply (rule conjI)

  1715 apply (rule_tac x = obj in exI, simp add:co2sobj_rmdir alive_rmdir)

  1716 apply (simp add:co2sobj_rmdir)

  1717 apply (simp add:alive_rmdir, erule_tac x = obj in allE, simp)

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

  1719 apply (case_tac "obj = O_dir f", simp)

  1720 apply (rule_tac x = obj in exI, simp add:co2sobj_rmdir alive_rmdir)

  1721 done

  1594   s2ss_readfile s2ss_writefile s2ss_closefd s2ss_unlink

  1729   s2ss_readfile s2ss_writefile s2ss_closefd s2ss_unlink s2ss_rmdir

  1595 

  1730