|
1 theory File_renaming |
|
2 imports Main OS_type_def My_list_prefix |
|
3 begin |
|
4 |
|
5 fun parent :: "'a list \<Rightarrow> ('a list) option" |
|
6 where |
|
7 "parent [] = None" |
|
8 | "parent (n#ns) = Some ns" |
|
9 |
|
10 definition file_after_rename :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
11 where |
|
12 "file_after_rename oldf newf f \<equiv> (if (oldf \<preceq> f) then ((f \<setminus> oldf) @ newf) else f)" |
|
13 |
|
14 definition file_before_rename :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
15 where |
|
16 "file_before_rename oldf newf f \<equiv> (if (newf \<preceq> f) then ((f \<setminus> newf) @ oldf) else f)" |
|
17 |
|
18 lemma list_diff_rev_prop0: "f \<setminus> f = []" |
|
19 by (induct f, auto simp:list_diff_rev_def) |
|
20 |
|
21 lemma list_diff_rev_prop0': "f \<setminus> [] = f" |
|
22 apply (simp add:list_diff_rev_def) |
|
23 apply (induct f rule:rev_induct, simp+) |
|
24 done |
|
25 |
|
26 lemma list_diff_rev_prop1_aux: "a # f\<^isub>3 \<setminus> f\<^isub>3 = [a]" |
|
27 by (induct f\<^isub>3, auto simp:list_diff_rev_def) |
|
28 |
|
29 lemma list_diff_rev_prop1: "f @ f' \<setminus> f' = f" |
|
30 apply (subgoal_tac "f @ f' \<setminus> [] @ f' = f \<setminus> []") |
|
31 apply (simp add:list_diff_rev_prop0') |
|
32 apply (simp only: list_diff_rev_ext_left[where ys = "[]"]) |
|
33 done |
|
34 |
|
35 lemma list_diff_rev_prop2_aux: "f \<preceq> f' \<Longrightarrow> a # f' \<setminus> f = a # (f' \<setminus> f)" |
|
36 apply (erule no_juniorE) |
|
37 by (simp only:list_diff_rev_prop1 append_Cons[THEN sym]) |
|
38 |
|
39 lemma list_diff_rev_prop2: "f \<preceq> f' \<Longrightarrow> (f' \<setminus> f) @ f = f'" |
|
40 apply (induct f', simp add:no_junior_def list_diff_rev_def) |
|
41 apply (case_tac "f = a # f'", simp add:list_diff_rev_prop0) |
|
42 apply (drule no_junior_noteq, simp) |
|
43 by (simp add:list_diff_rev_prop2_aux) |
|
44 |
|
45 lemma file_renaming_prop0: |
|
46 "file_after_rename f\<^isub>2 f\<^isub>3 f\<^isub>2 = f\<^isub>3" |
|
47 apply (simp add:file_after_rename_def list_diff_rev_def) |
|
48 apply (induct f\<^isub>2, auto) |
|
49 done |
|
50 |
|
51 lemma file_renaming_prop0': |
|
52 "file_before_rename f\<^isub>2 f\<^isub>3 f\<^isub>3 = f\<^isub>2" |
|
53 apply (simp add:file_before_rename_def list_diff_rev_def) |
|
54 apply (induct f\<^isub>3, auto) |
|
55 done |
|
56 |
|
57 lemma file_renaming_prop1: |
|
58 "f\<^isub>2 \<preceq> f \<Longrightarrow> f\<^isub>3 \<preceq> file_after_rename f\<^isub>2 f\<^isub>3 f " |
|
59 by (simp add:file_after_rename_def) |
|
60 |
|
61 lemma file_renaming_prop1': |
|
62 "f\<^isub>3 \<preceq> f \<Longrightarrow> f\<^isub>2 \<preceq> file_before_rename f\<^isub>2 f\<^isub>3 f" |
|
63 by (simp add:file_before_rename_def) |
|
64 |
|
65 lemma file_renaming_prop1'': |
|
66 "\<not> f\<^isub>3 \<preceq> file_after_rename f\<^isub>2 f\<^isub>3 f \<Longrightarrow> \<not> f\<^isub>2 \<preceq> f" |
|
67 by (case_tac "f\<^isub>2 \<preceq> f", drule_tac f\<^isub>3 = f\<^isub>3 in file_renaming_prop1, simp+) |
|
68 |
|
69 lemma file_renaming_prop2: |
|
70 "\<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" |
|
71 apply (case_tac f, simp add:no_junior_def) |
|
72 apply (auto simp add:file_after_rename_def list_diff_rev_prop1_aux) |
|
73 apply (erule no_juniorE, simp add:list_diff_rev_prop1) |
|
74 done |
|
75 |
|
76 lemma file_renaming_prop2': |
|
77 "\<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" |
|
78 apply (case_tac f, simp add:no_junior_def) |
|
79 apply (auto simp add:file_before_rename_def list_diff_rev_prop1_aux) |
|
80 apply (erule no_juniorE, simp add:list_diff_rev_prop1) |
|
81 done |
|
82 |
|
83 lemma file_renaming_prop3: |
|
84 "\<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" |
|
85 apply (frule_tac f\<^isub>3 = f\<^isub>3 in file_renaming_prop1, simp) |
|
86 by (drule_tac f\<^isub>3 = f\<^isub>3 in file_renaming_prop2, simp+) |
|
87 |
|
88 lemma file_renaming_prop3': |
|
89 "\<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" |
|
90 apply (frule_tac f\<^isub>2 = f\<^isub>2 in file_renaming_prop1', simp) |
|
91 by (drule_tac f\<^isub>2 = f\<^isub>2 in file_renaming_prop2', simp+) |
|
92 |
|
93 lemma file_renaming_prop4: "\<not> f\<^isub>2 \<preceq> f \<Longrightarrow> file_after_rename f\<^isub>2 f\<^isub>3 f = f" |
|
94 by (simp add:file_after_rename_def) |
|
95 |
|
96 lemma file_renaming_prop4': "\<not> f\<^isub>3 \<preceq> f \<Longrightarrow> file_before_rename f\<^isub>2 f\<^isub>3 f = f" |
|
97 by (simp add:file_before_rename_def) |
|
98 |
|
99 lemma file_renaming_prop5: |
|
100 "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" |
|
101 apply (case_tac "f\<^isub>1 = f\<^isub>2") |
|
102 apply (simp add:file_renaming_prop0 file_renaming_prop0') |
|
103 apply (simp add:file_after_rename_def file_before_rename_def) |
|
104 by (simp add:list_diff_rev_prop1 list_diff_rev_prop2) |
|
105 |
|
106 lemma file_renaming_prop5': |
|
107 "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" |
|
108 apply (case_tac "f\<^isub>1 = f\<^isub>3") |
|
109 apply (simp add:file_renaming_prop0' file_renaming_prop0) |
|
110 apply (simp add:file_after_rename_def file_before_rename_def) |
|
111 by (simp add:list_diff_rev_prop1 list_diff_rev_prop2) |
|
112 |
|
113 lemma file_renaming_prop6: |
|
114 "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))" |
|
115 by (simp add:file_after_rename_def list_diff_rev_prop2_aux) |
|
116 |
|
117 lemma file_renaming_prop6': |
|
118 "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))" |
|
119 by (simp add:file_before_rename_def list_diff_rev_prop2_aux) |
|
120 |
|
121 lemma file_renaming_prop7: "file_after_rename f\<^isub>2 f\<^isub>3 (a # f\<^isub>2) = a # f\<^isub>3" |
|
122 apply (auto simp:file_after_rename_def no_junior_def list_diff_rev_def) |
|
123 by (induct f\<^isub>2, auto) |
|
124 |
|
125 lemma file_renaming_prop7': "file_before_rename f\<^isub>2 f\<^isub>3 (a # f\<^isub>3) = a # f\<^isub>2" |
|
126 by (auto simp:file_before_rename_def no_junior_def list_diff_rev_prop1_aux) |
|
127 |
|
128 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))" |
|
129 by (simp add:file_after_rename_def no_junior_def) |
|
130 |
|
131 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))" |
|
132 by (simp add:file_before_rename_def no_junior_def) |
|
133 |
|
134 lemma no_junior_prop0: "f\<preceq> f' \<Longrightarrow> f \<preceq> (a # f')" |
|
135 by (simp add:no_junior_def) |
|
136 |
|
137 lemma file_renaming_prop9: |
|
138 "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)" |
|
139 by (drule_tac a = a in no_junior_prop0, simp add:file_renaming_prop5) |
|
140 |
|
141 lemma file_renaming_prop9': |
|
142 "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)" |
|
143 by (drule_tac a = a in no_junior_prop0, simp add:file_renaming_prop5') |
|
144 |
|
145 lemma file_renaming_prop10: |
|
146 "\<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'" |
|
147 apply (frule_tac f\<^isub>3 = fy in file_renaming_prop1) |
|
148 apply (subgoal_tac "fy \<preceq> f\<^isub>1") defer apply (rotate_tac 3, erule no_juniorE, case_tac zs, simp+) |
|
149 apply (drule_tac f = f\<^isub>1 and f\<^isub>2 = fx and f\<^isub>3 = fy and a = a in file_renaming_prop6') |
|
150 by (drule_tac f\<^isub>1 = f\<^isub>1' and f\<^isub>3 = fy in file_renaming_prop5, simp) |
|
151 |
|
152 lemma file_renaming_prop11: |
|
153 "\<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'" |
|
154 by (drule_tac f\<^isub>3 = f\<^isub>3 in file_renaming_prop5, simp) |
|
155 |
|
156 lemma file_renaming_prop11': |
|
157 "\<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'" |
|
158 by (drule_tac f\<^isub>2 = f\<^isub>2 in file_renaming_prop5', simp) |
|
159 |
|
160 lemma file_renaming_prop12: |
|
161 "\<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" |
|
162 apply (simp add:file_after_rename_def file_before_rename_def split:if_splits) |
|
163 by (auto, simp add:list_diff_rev_prop1 list_diff_rev_prop2) |
|
164 |
|
165 lemma file_renaming_prop12': |
|
166 "\<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" |
|
167 apply (simp add:file_after_rename_def file_before_rename_def split:if_splits) |
|
168 by (auto, simp add:list_diff_rev_prop1 list_diff_rev_prop2) |
|
169 |
|
170 |
|
171 lemma file_renaming_prop13: |
|
172 "\<lbrakk>f\<^isub>3 \<preceq> f; file_before_rename f\<^isub>2 f\<^isub>3 f = f\<rbrakk> \<Longrightarrow> f\<^isub>2 \<preceq> f" |
|
173 apply (simp add:file_before_rename_def) |
|
174 apply (rule_tac zs = "f \<setminus> f\<^isub>3" in no_juniorI) |
|
175 by simp |
|
176 |
|
177 (************ something *****************) |
|
178 |
|
179 |
|
180 lemma parent_is_parent: "parent f = Some pf \<Longrightarrow> f \<noteq> pf" |
|
181 by (case_tac f, auto) |
|
182 |
|
183 lemma parent_is_parent': "parent f = Some f \<Longrightarrow> false" |
|
184 by (drule parent_is_parent, simp) |
|
185 |
|
186 lemma parent_is_parent'': "parent f \<noteq> Some f" |
|
187 by (case_tac f, auto) |
|
188 |
|
189 lemma parent_is_parent3: "parent f = Some f' \<Longrightarrow> \<not> f \<preceq> f'" |
|
190 by (case_tac f, auto elim:no_juniorE) |
|
191 |
|
192 lemma parent_is_ancen: "parent f = Some f' \<Longrightarrow> f' \<preceq> f" |
|
193 by (case_tac f, auto simp:no_junior_def) |
|
194 |
|
195 lemma parent_is_ancen': "\<lbrakk>parent f = Some pf; f' \<preceq> pf\<rbrakk> \<Longrightarrow> f' \<preceq> f" |
|
196 by (case_tac f, auto simp:no_junior_def) |
|
197 |
|
198 lemma parent_ancen: "\<lbrakk>parent f = Some pf; f' \<preceq> f; f \<noteq> f'\<rbrakk> \<Longrightarrow> f' \<preceq> pf" |
|
199 apply (erule no_juniorE) |
|
200 apply (case_tac zs, simp) |
|
201 apply (rule_tac zs = list in no_juniorI) |
|
202 by auto |
|
203 |
|
204 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)" |
|
205 apply (simp add:file_before_rename_def) |
|
206 apply (case_tac f, simp, simp) |
|
207 by (drule_tac a = a in list_diff_rev_prop2_aux, simp) |
|
208 |
|
209 lemma no_junior_trans: "\<lbrakk>f \<preceq> f'; f' \<preceq> f''\<rbrakk> \<Longrightarrow> f \<preceq> f''" |
|
210 by (auto elim:no_juniorE) |
|
211 |
|
212 lemma no_junior_conf: "\<lbrakk>a \<preceq> c; b \<preceq> c\<rbrakk> \<Longrightarrow> a \<preceq> b \<or> b \<preceq> a" |
|
213 apply (simp add:no_junior_def) |
|
214 apply (induct c, auto) |
|
215 done |
|
216 |
|
217 lemma noJ_Anc: "x \<prec> y = (x \<preceq> y \<and> x \<noteq> y)" |
|
218 apply (simp add: no_junior_expand) |
|
219 by (auto simp:is_ancestor_def) |
|
220 |
|
221 end |