diff -r f27ba31b7e96 -r 6f7b9039715f no_shm_selinux/File_renaming.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/no_shm_selinux/File_renaming.thy Tue Dec 17 13:30:21 2013 +0800 @@ -0,0 +1,221 @@ +theory File_renaming +imports Main OS_type_def My_list_prefix +begin + +fun parent :: "'a list \<Rightarrow> ('a list) option" +where + "parent [] = None" + | "parent (n#ns) = Some ns" + +definition file_after_rename :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" +where + "file_after_rename oldf newf f \<equiv> (if (oldf \<preceq> f) then ((f \<setminus> oldf) @ newf) else f)" + +definition file_before_rename :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" +where + "file_before_rename oldf newf f \<equiv> (if (newf \<preceq> f) then ((f \<setminus> newf) @ oldf) else f)" + +lemma list_diff_rev_prop0: "f \<setminus> f = []" +by (induct f, auto simp:list_diff_rev_def) + +lemma list_diff_rev_prop0': "f \<setminus> [] = f" +apply (simp add:list_diff_rev_def) +apply (induct f rule:rev_induct, simp+) +done + +lemma list_diff_rev_prop1_aux: "a # f\<^isub>3 \<setminus> f\<^isub>3 = [a]" +by (induct f\<^isub>3, auto simp:list_diff_rev_def) + +lemma list_diff_rev_prop1: "f @ f' \<setminus> f' = f" +apply (subgoal_tac "f @ f' \<setminus> [] @ f' = f \<setminus> []") +apply (simp add:list_diff_rev_prop0') +apply (simp only: list_diff_rev_ext_left[where ys = "[]"]) +done + +lemma list_diff_rev_prop2_aux: "f \<preceq> f' \<Longrightarrow> a # f' \<setminus> f = a # (f' \<setminus> f)" +apply (erule no_juniorE) +by (simp only:list_diff_rev_prop1 append_Cons[THEN sym]) + +lemma list_diff_rev_prop2: "f \<preceq> f' \<Longrightarrow> (f' \<setminus> f) @ f = f'" +apply (induct f', simp add:no_junior_def list_diff_rev_def) +apply (case_tac "f = a # f'", simp add:list_diff_rev_prop0) +apply (drule no_junior_noteq, simp) +by (simp add:list_diff_rev_prop2_aux) + +lemma file_renaming_prop0: + "file_after_rename f\<^isub>2 f\<^isub>3 f\<^isub>2 = f\<^isub>3" +apply (simp add:file_after_rename_def list_diff_rev_def) +apply (induct f\<^isub>2, auto) +done + +lemma file_renaming_prop0': + "file_before_rename f\<^isub>2 f\<^isub>3 f\<^isub>3 = f\<^isub>2" +apply (simp add:file_before_rename_def list_diff_rev_def) +apply (induct f\<^isub>3, auto) +done + +lemma file_renaming_prop1: + "f\<^isub>2 \<preceq> f \<Longrightarrow> f\<^isub>3 \<preceq> file_after_rename f\<^isub>2 f\<^isub>3 f " +by (simp add:file_after_rename_def) + +lemma file_renaming_prop1': + "f\<^isub>3 \<preceq> f \<Longrightarrow> f\<^isub>2 \<preceq> file_before_rename f\<^isub>2 f\<^isub>3 f" +by (simp add:file_before_rename_def) + +lemma file_renaming_prop1'': + "\<not> f\<^isub>3 \<preceq> file_after_rename f\<^isub>2 f\<^isub>3 f \<Longrightarrow> \<not> f\<^isub>2 \<preceq> f" +by (case_tac "f\<^isub>2 \<preceq> f", drule_tac f\<^isub>3 = f\<^isub>3 in file_renaming_prop1, simp+) + +lemma file_renaming_prop2: + "\<lbrakk>f\<^isub>2 \<preceq> f; f \<noteq> f\<^isub>2\<rbrakk> \<Longrightarrow> file_after_rename f\<^isub>2 f\<^isub>3 f \<noteq> f\<^isub>3" +apply (case_tac f, simp add:no_junior_def) +apply (auto simp add:file_after_rename_def list_diff_rev_prop1_aux) +apply (erule no_juniorE, simp add:list_diff_rev_prop1) +done + +lemma file_renaming_prop2': + "\<lbrakk>f\<^isub>3 \<preceq> f; f \<noteq> f\<^isub>3\<rbrakk> \<Longrightarrow> file_before_rename f\<^isub>2 f\<^isub>3 f \<noteq> f\<^isub>2" +apply (case_tac f, simp add:no_junior_def) +apply (auto simp add:file_before_rename_def list_diff_rev_prop1_aux) +apply (erule no_juniorE, simp add:list_diff_rev_prop1) +done + +lemma file_renaming_prop3: + "\<lbrakk>f\<^isub>2 \<preceq> f; f\<^isub>2 \<noteq> f\<rbrakk> \<Longrightarrow> f\<^isub>3 \<preceq> file_after_rename f\<^isub>2 f\<^isub>3 f \<and> f\<^isub>3 \<noteq> file_after_rename f\<^isub>2 f\<^isub>3 f" +apply (frule_tac f\<^isub>3 = f\<^isub>3 in file_renaming_prop1, simp) +by (drule_tac f\<^isub>3 = f\<^isub>3 in file_renaming_prop2, simp+) + +lemma file_renaming_prop3': + "\<lbrakk>f\<^isub>3 \<preceq> f; f\<^isub>3 \<noteq> f\<rbrakk> \<Longrightarrow> f\<^isub>2 \<preceq> file_before_rename f\<^isub>2 f\<^isub>3 f \<and> f\<^isub>2 \<noteq> file_before_rename f\<^isub>2 f\<^isub>3 f" +apply (frule_tac f\<^isub>2 = f\<^isub>2 in file_renaming_prop1', simp) +by (drule_tac f\<^isub>2 = f\<^isub>2 in file_renaming_prop2', simp+) + +lemma file_renaming_prop4: "\<not> f\<^isub>2 \<preceq> f \<Longrightarrow> file_after_rename f\<^isub>2 f\<^isub>3 f = f" +by (simp add:file_after_rename_def) + +lemma file_renaming_prop4': "\<not> f\<^isub>3 \<preceq> f \<Longrightarrow> file_before_rename f\<^isub>2 f\<^isub>3 f = f" +by (simp add:file_before_rename_def) + +lemma file_renaming_prop5: + "f\<^isub>2 \<preceq> f\<^isub>1 \<Longrightarrow> file_before_rename f\<^isub>2 f\<^isub>3 (file_after_rename f\<^isub>2 f\<^isub>3 f\<^isub>1) = f\<^isub>1" +apply (case_tac "f\<^isub>1 = f\<^isub>2") +apply (simp add:file_renaming_prop0 file_renaming_prop0') +apply (simp add:file_after_rename_def file_before_rename_def) +by (simp add:list_diff_rev_prop1 list_diff_rev_prop2) + +lemma file_renaming_prop5': + "f\<^isub>3 \<preceq> f\<^isub>1 \<Longrightarrow> file_after_rename f\<^isub>2 f\<^isub>3 (file_before_rename f\<^isub>2 f\<^isub>3 f\<^isub>1) = f\<^isub>1" +apply (case_tac "f\<^isub>1 = f\<^isub>3") +apply (simp add:file_renaming_prop0' file_renaming_prop0) +apply (simp add:file_after_rename_def file_before_rename_def) +by (simp add:list_diff_rev_prop1 list_diff_rev_prop2) + +lemma file_renaming_prop6: + "f\<^isub>2 \<preceq> f \<Longrightarrow> file_after_rename f\<^isub>2 f\<^isub>3 (a # f) = (a # (file_after_rename f\<^isub>2 f\<^isub>3 f))" +by (simp add:file_after_rename_def list_diff_rev_prop2_aux) + +lemma file_renaming_prop6': + "f\<^isub>3 \<preceq> f \<Longrightarrow> file_before_rename f\<^isub>2 f\<^isub>3 (a # f) = (a # (file_before_rename f\<^isub>2 f\<^isub>3 f))" +by (simp add:file_before_rename_def list_diff_rev_prop2_aux) + +lemma file_renaming_prop7: "file_after_rename f\<^isub>2 f\<^isub>3 (a # f\<^isub>2) = a # f\<^isub>3" +apply (auto simp:file_after_rename_def no_junior_def list_diff_rev_def) +by (induct f\<^isub>2, auto) + +lemma file_renaming_prop7': "file_before_rename f\<^isub>2 f\<^isub>3 (a # f\<^isub>3) = a # f\<^isub>2" +by (auto simp:file_before_rename_def no_junior_def list_diff_rev_prop1_aux) + +lemma file_renaming_prop8: "f\<^isub>2 \<preceq> f \<Longrightarrow> f\<^isub>3 \<preceq> (file_after_rename f\<^isub>2 f\<^isub>3 (a # f))" +by (simp add:file_after_rename_def no_junior_def) + +lemma file_renaming_prop8': "f\<^isub>3 \<preceq> f \<Longrightarrow> f\<^isub>2 \<preceq> (file_before_rename f\<^isub>2 f\<^isub>3 (a # f))" +by (simp add:file_before_rename_def no_junior_def) + +lemma no_junior_prop0: "f\<preceq> f' \<Longrightarrow> f \<preceq> (a # f')" +by (simp add:no_junior_def) + +lemma file_renaming_prop9: + "f\<^isub>2 \<preceq> f\<^isub>1 \<Longrightarrow> file_before_rename f\<^isub>2 f\<^isub>3 (file_after_rename f\<^isub>2 f\<^isub>3 (a # f\<^isub>1)) = (a # f\<^isub>1)" +by (drule_tac a = a in no_junior_prop0, simp add:file_renaming_prop5) + +lemma file_renaming_prop9': + "f\<^isub>3 \<preceq> f\<^isub>1 \<Longrightarrow> file_after_rename f\<^isub>2 f\<^isub>3 (file_before_rename f\<^isub>2 f\<^isub>3 (a # f\<^isub>1)) = (a # f\<^isub>1)" +by (drule_tac a = a in no_junior_prop0, simp add:file_renaming_prop5') + +lemma file_renaming_prop10: + "\<lbrakk>a # f\<^isub>1 = file_after_rename fx fy f\<^isub>1'; file_after_rename fx fy f\<^isub>1' \<noteq> fy; fx \<preceq> f\<^isub>1'\<rbrakk> \<Longrightarrow> a # (file_before_rename fx fy f\<^isub>1) = f\<^isub>1'" +apply (frule_tac f\<^isub>3 = fy in file_renaming_prop1) +apply (subgoal_tac "fy \<preceq> f\<^isub>1") defer apply (rotate_tac 3, erule no_juniorE, case_tac zs, simp+) +apply (drule_tac f = f\<^isub>1 and f\<^isub>2 = fx and f\<^isub>3 = fy and a = a in file_renaming_prop6') +by (drule_tac f\<^isub>1 = f\<^isub>1' and f\<^isub>3 = fy in file_renaming_prop5, simp) + +lemma file_renaming_prop11: + "\<lbrakk>f\<^isub>2 \<preceq> f; file_after_rename f\<^isub>2 f\<^isub>3 f = f'\<rbrakk> \<Longrightarrow> f = file_before_rename f\<^isub>2 f\<^isub>3 f'" +by (drule_tac f\<^isub>3 = f\<^isub>3 in file_renaming_prop5, simp) + +lemma file_renaming_prop11': + "\<lbrakk>f\<^isub>3 \<preceq> f; file_before_rename f\<^isub>2 f\<^isub>3 f = f'\<rbrakk> \<Longrightarrow> f = file_after_rename f\<^isub>2 f\<^isub>3 f'" +by (drule_tac f\<^isub>2 = f\<^isub>2 in file_renaming_prop5', simp) + +lemma file_renaming_prop12: + "\<lbrakk>\<not> f\<^isub>3 \<preceq> aa; f\<^isub>3 \<preceq> f; file_after_rename f\<^isub>2 f\<^isub>3 aa = f\<rbrakk> \<Longrightarrow> file_before_rename f\<^isub>2 f\<^isub>3 f = aa" +apply (simp add:file_after_rename_def file_before_rename_def split:if_splits) +by (auto, simp add:list_diff_rev_prop1 list_diff_rev_prop2) + +lemma file_renaming_prop12': + "\<lbrakk>\<not> f\<^isub>2 \<preceq> aa; f\<^isub>2 \<preceq> f; file_before_rename f\<^isub>2 f\<^isub>3 aa = f\<rbrakk> \<Longrightarrow> file_after_rename f\<^isub>2 f\<^isub>3 f = aa" +apply (simp add:file_after_rename_def file_before_rename_def split:if_splits) +by (auto, simp add:list_diff_rev_prop1 list_diff_rev_prop2) + + +lemma file_renaming_prop13: + "\<lbrakk>f\<^isub>3 \<preceq> f; file_before_rename f\<^isub>2 f\<^isub>3 f = f\<rbrakk> \<Longrightarrow> f\<^isub>2 \<preceq> f" +apply (simp add:file_before_rename_def) +apply (rule_tac zs = "f \<setminus> f\<^isub>3" in no_juniorI) +by simp + +(************ something *****************) + + +lemma parent_is_parent: "parent f = Some pf \<Longrightarrow> f \<noteq> pf" +by (case_tac f, auto) + +lemma parent_is_parent': "parent f = Some f \<Longrightarrow> false" +by (drule parent_is_parent, simp) + +lemma parent_is_parent'': "parent f \<noteq> Some f" +by (case_tac f, auto) + +lemma parent_is_parent3: "parent f = Some f' \<Longrightarrow> \<not> f \<preceq> f'" +by (case_tac f, auto elim:no_juniorE) + +lemma parent_is_ancen: "parent f = Some f' \<Longrightarrow> f' \<preceq> f" +by (case_tac f, auto simp:no_junior_def) + +lemma parent_is_ancen': "\<lbrakk>parent f = Some pf; f' \<preceq> pf\<rbrakk> \<Longrightarrow> f' \<preceq> f" +by (case_tac f, auto simp:no_junior_def) + +lemma parent_ancen: "\<lbrakk>parent f = Some pf; f' \<preceq> f; f \<noteq> f'\<rbrakk> \<Longrightarrow> f' \<preceq> pf" +apply (erule no_juniorE) +apply (case_tac zs, simp) +apply (rule_tac zs = list in no_juniorI) +by auto + +lemma parent_rename_ancen: "\<lbrakk>parent f = Some pf; f\<^isub>3 \<preceq> pf; f \<noteq> f\<^isub>3\<rbrakk> \<Longrightarrow> parent (file_before_rename f\<^isub>2 f\<^isub>3 f) = Some (file_before_rename f\<^isub>2 f\<^isub>3 pf)" +apply (simp add:file_before_rename_def) +apply (case_tac f, simp, simp) +by (drule_tac a = a in list_diff_rev_prop2_aux, simp) + +lemma no_junior_trans: "\<lbrakk>f \<preceq> f'; f' \<preceq> f''\<rbrakk> \<Longrightarrow> f \<preceq> f''" +by (auto elim:no_juniorE) + +lemma no_junior_conf: "\<lbrakk>a \<preceq> c; b \<preceq> c\<rbrakk> \<Longrightarrow> a \<preceq> b \<or> b \<preceq> a" +apply (simp add:no_junior_def) +apply (induct c, auto) +done + +lemma noJ_Anc: "x \<prec> y = (x \<preceq> y \<and> x \<noteq> y)" +apply (simp add: no_junior_expand) +by (auto simp:is_ancestor_def) + +end \ No newline at end of file