1873 apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard) |
1873 apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard) |
1874 apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard) |
1874 apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard) |
1875 apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard) |
1875 apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard) |
1876 done |
1876 done |
1877 |
1877 |
1878 lemma has_same_inode_prop3: |
1878 lemma same_inode_files_prop12: |
1879 "is_file s f \<Longrightarrow> has_same_inode s f f" |
1879 "is_file s f \<Longrightarrow> f \<in> same_inode_files s f " |
1880 by (auto simp:is_file_def has_same_inode_def split:option.splits) |
1880 by (auto simp:is_file_def same_inode_files_def split:option.splits) |
1881 |
1881 |
1882 definition update_s2ss_sfile_tainted:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> bool \<Rightarrow> t_static_state" |
1882 definition update_s2ss_sfile_tainted:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> bool \<Rightarrow> t_static_state" |
1883 where |
1883 where |
1884 "update_s2ss_sfile_tainted s ss f tag \<equiv> |
1884 "update_s2ss_sfile_tainted s ss f tag \<equiv> |
1885 if (\<exists> f'. is_file s f' \<and> f' \<notin> same_inode_files s f \<and> |
1885 if (\<exists> f'. is_file s f' \<and> f' \<notin> same_inode_files s f \<and> |
1898 apply (simp add:update_s2ss_sfile_tainted_def) |
1898 apply (simp add:update_s2ss_sfile_tainted_def) |
1899 apply (rule conjI|rule impI|erule exE|erule conjE)+ |
1899 apply (rule conjI|rule impI|erule exE|erule conjE)+ |
1900 apply (simp add:s2ss_def) |
1900 apply (simp add:s2ss_def) |
1901 apply (tactic {*my_seteq_tac 1*}) |
1901 apply (tactic {*my_seteq_tac 1*}) |
1902 apply (case_tac "obj = O_file f") |
1902 apply (case_tac "obj = O_file f") |
1903 apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted has_same_inode_prop3 cf2sfiles_other) |
1903 apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted same_inode_files_prop12 cf2sfiles_other) |
1904 apply (erule_tac obj = obj in co2sobj_some_caseD) |
1904 apply (erule_tac obj = obj in co2sobj_some_caseD) |
1905 apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_truncate alive_simps) |
1905 apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_truncate alive_simps) |
1906 apply (case_tac "fa \<in> same_inode_files s f") |
1906 apply (case_tac "fa \<in> same_inode_files s f") |
1907 apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted cf2sfiles_prop cf2sfiles_other) |
1907 apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted cf2sfiles_prop cf2sfiles_other) |
1908 apply (simp add:same_inode_files_prop7) |
|
1909 apply (rule disjI2, simp, rule_tac x = obj in exI) |
1908 apply (rule disjI2, simp, rule_tac x = obj in exI) |
1910 apply (simp add:co2sobj_truncate is_file_simps) |
1909 apply (simp add:co2sobj_truncate is_file_simps) |
1911 apply (rule disjI2, simp, rule_tac x = obj in exI) |
1910 apply (rule disjI2, simp, rule_tac x = obj in exI) |
1912 apply (simp add:co2sobj_truncate) |
1911 apply (simp add:co2sobj_truncate) |
1913 apply (rule disjI2, simp, rule_tac x = obj in exI) |
1912 apply (rule disjI2, simp, rule_tac x = obj in exI) |
1914 apply (simp add:co2sobj_truncate is_dir_simps) |
1913 apply (simp add:co2sobj_truncate is_dir_simps) |
1915 apply (rule disjI2, simp, rule_tac x = obj in exI) |
1914 apply (rule disjI2, simp, rule_tac x = obj in exI) |
1916 apply (simp add:co2sobj_truncate) |
1915 apply (simp add:co2sobj_truncate) |
1917 apply (tactic {*my_setiff_tac 1*}) |
1916 apply (tactic {*my_setiff_tac 1*}) |
1918 apply (rule_tac x = "O_file f" in exI) |
1917 apply (rule_tac x = "O_file f" in exI) |
1919 apply (simp add:co2sobj.simps is_file_simps tainted_eq_Tainted cf2sfiles_other has_same_inode_prop3) |
1918 apply (simp add:co2sobj.simps is_file_simps tainted_eq_Tainted cf2sfiles_other same_inode_files_prop12) |
1920 apply (tactic {*my_setiff_tac 1*}) |
1919 apply (tactic {*my_setiff_tac 1*}) |
1921 apply (erule_tac obj = obj in co2sobj_some_caseD) |
1920 apply (erule_tac obj = obj in co2sobj_some_caseD) |
1922 apply (rule_tac x = obj in exI, simp add:co2sobj_truncate) |
1921 apply (rule_tac x = obj in exI, simp add:co2sobj_truncate) |
1923 apply (case_tac "fa \<in> same_inode_files s f") |
1922 apply (case_tac "fa \<in> same_inode_files s f") |
1924 apply (rule_tac x = "O_file f'" in exI) |
1923 apply (rule_tac x = "O_file f'" in exI) |
1931 |
1930 |
1932 apply (rule conjI|rule impI|erule exE|erule conjE)+ |
1931 apply (rule conjI|rule impI|erule exE|erule conjE)+ |
1933 apply (simp add:s2ss_def) |
1932 apply (simp add:s2ss_def) |
1934 apply (tactic {*my_seteq_tac 1*}) |
1933 apply (tactic {*my_seteq_tac 1*}) |
1935 apply (case_tac "obj = O_file f") |
1934 apply (case_tac "obj = O_file f") |
1936 apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted has_same_inode_prop3 cf2sfiles_other) |
1935 apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted same_inode_files_prop12 cf2sfiles_other) |
1937 apply (erule_tac obj = obj in co2sobj_some_caseD) |
1936 apply (erule_tac obj = obj in co2sobj_some_caseD) |
1938 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_truncate alive_simps) |
1937 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_truncate alive_simps) |
1939 apply (rule notI, simp add:co2sobj.simps split:option.splits) |
1938 apply (rule notI, simp add:co2sobj.simps split:option.splits) |
1940 apply (case_tac "fa \<in> same_inode_files s f") |
1939 apply (case_tac "fa \<in> same_inode_files s f") |
1941 apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted cf2sfiles_prop cf2sfiles_other) |
1940 apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted cf2sfiles_prop cf2sfiles_other) |
1942 apply (simp add:same_inode_files_prop7) |
|
1943 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI) |
1941 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI) |
1944 apply (simp add:co2sobj_truncate is_file_simps) |
1942 apply (simp add:co2sobj_truncate is_file_simps) |
1945 apply (rule notI, simp add:co2sobj_truncate is_file_simps) |
1943 apply (rule notI, simp add:co2sobj_truncate is_file_simps) |
1946 apply (erule_tac x = fa in allE) |
1944 apply (erule_tac x = fa in allE) |
1947 apply (simp add:co2sobj.simps) |
1945 apply (simp add:co2sobj.simps) |
1954 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI) |
1952 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI) |
1955 apply (simp add:co2sobj_truncate) |
1953 apply (simp add:co2sobj_truncate) |
1956 apply (rule notI, simp add:co2sobj.simps split:option.splits) |
1954 apply (rule notI, simp add:co2sobj.simps split:option.splits) |
1957 apply (tactic {*my_setiff_tac 1*}) |
1955 apply (tactic {*my_setiff_tac 1*}) |
1958 apply (rule_tac x = "O_file f" in exI) |
1956 apply (rule_tac x = "O_file f" in exI) |
1959 apply (simp add:co2sobj.simps is_file_simps tainted_eq_Tainted cf2sfiles_other has_same_inode_prop3) |
1957 apply (simp add:co2sobj.simps is_file_simps tainted_eq_Tainted cf2sfiles_other same_inode_files_prop12) |
1960 apply (tactic {*my_setiff_tac 1*}) |
1958 apply (tactic {*my_setiff_tac 1*}) |
1961 apply (erule_tac obj = obj in co2sobj_some_caseD) |
1959 apply (erule_tac obj = obj in co2sobj_some_caseD) |
1962 apply (rule_tac x = obj in exI, simp add:co2sobj_truncate) |
1960 apply (rule_tac x = obj in exI, simp add:co2sobj_truncate) |
1963 apply (case_tac "fa \<in> same_inode_files s f") |
1961 apply (case_tac "fa \<in> same_inode_files s f") |
1964 apply (simp add:co2sobj.simps same_inodes_Tainted tainted_eq_Tainted cf2sfiles_prop) |
1962 apply (simp add:co2sobj.simps same_inodes_Tainted tainted_eq_Tainted cf2sfiles_prop) |