1
|
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 |