--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/File_renaming.thy	Fri May 03 08:20:21 2013 +0100
@@ -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