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