File_renaming.thy
author chunhan
Thu, 16 May 2013 15:18:44 +0800
changeset 8 289a30c4cfb7
parent 1 7d9c0ed02b56
permissions -rwxr-xr-x
find bugs in deleted & inum_of_file

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