61 by (drule nim_notin_curim, simp) |
61 by (drule nim_notin_curim, simp) |
62 |
62 |
63 lemma len_fname_all: "length (fname_all_a len) = len" |
63 lemma len_fname_all: "length (fname_all_a len) = len" |
64 by (induct len, auto simp:fname_all_a.simps) |
64 by (induct len, auto simp:fname_all_a.simps) |
65 |
65 |
66 lemma ncf_notin_curf: "valid \<tau> \<Longrightarrow> new_childf f \<tau> \<notin> current_files \<tau>" |
66 lemma finite_fs_fnames: |
67 apply (drule finite_cf) |
67 "finite (fs::t_file set) \<Longrightarrow> finite {fn. fn # f \<in> fs}" |
68 apply (simp add:new_childf_def next_fname_def all_fname_under_dir_def) |
68 thm finite_imageI |
69 apply (rule notI) |
|
70 apply (subgoal_tac "(CHR ''a'' # fname_all_a (Max (fname_length_set {fn. fn # f \<in> current_files \<tau>}))) \<in> {fn. fn # f \<in> current_files \<tau>}") |
|
71 defer apply simp |
|
72 apply (subgoal_tac "length (CHR ''a'' # fname_all_a (Max (fname_length_set {fn. fn # f \<in> current_files \<tau>}))) \<in> fname_length_set {fn. fn # f \<in> current_files \<tau>}") |
|
73 defer apply (auto simp:fname_length_set_def image_def)[1] |
|
74 apply (subgoal_tac "finite (fname_length_set {fn. fn # f \<in> current_files \<tau>})") |
|
75 defer |
|
76 apply (simp add:fname_length_set_def) |
|
77 apply (rule finite_imageI) |
|
78 apply (drule_tac h = "\<lambda> f'. case f' of [] \<Rightarrow> '''' | fn # pf' \<Rightarrow> if (pf' = f) then fn else ''''" in finite_imageI) |
69 apply (drule_tac h = "\<lambda> f'. case f' of [] \<Rightarrow> '''' | fn # pf' \<Rightarrow> if (pf' = f) then fn else ''''" in finite_imageI) |
79 apply (rule_tac B = "(list_case [] (\<lambda>fn pf'. if pf' = f then fn else []) ` current_files \<tau>)" in finite_subset) |
70 apply (rule_tac B = "(list_case [] (\<lambda>fn pf'. if pf' = f then fn else []) ` fs)" in finite_subset) |
80 unfolding image_def |
71 unfolding image_def |
81 apply (clarsimp split:if_splits) |
72 apply (clarsimp split:if_splits) |
82 apply (rule_tac x = "x # f" in bexI, simp+) |
73 apply (rule_tac x = "x # f" in bexI, simp+) |
83 |
|
84 apply (drule_tac s = "(fname_length_set {fn. fn # f \<in> current_files \<tau>})" in nn_notin_aux) |
|
85 apply (erule_tac x = "length (CHR ''a'' # fname_all_a (Max (fname_length_set {fn. fn # f \<in> current_files \<tau>})))" in ballE) |
|
86 apply (simp add:len_fname_all, simp) |
|
87 done |
74 done |
88 |
75 |
|
76 lemma ncf_notin_curf_aux: |
|
77 "finite (fs::t_file set) \<Longrightarrow> Suc (Max (fname_length_set {fn. fn # f \<in> fs})) \<notin> fname_length_set {fn. fn # f \<in> fs}" |
|
78 apply (drule_tac f = f in finite_fs_fnames) |
|
79 apply (drule_tac h = length in finite_imageI) |
|
80 apply (simp add:fname_length_set_def) |
|
81 apply (drule nn_notin_aux) |
|
82 apply auto |
|
83 done |
|
84 |
|
85 lemma ncf_notin_curf_general: |
|
86 assumes vd: "valid \<tau>" and fin_fs: "finite fs" |
|
87 shows "new_childf_general f \<tau> fs \<notin> (current_files \<tau> \<union> fs)" |
|
88 proof- |
|
89 from vd fin_fs have "finite (current_files \<tau> \<union> fs)" |
|
90 by (auto dest:finite_cf) |
|
91 hence a1: "Suc (Max (fname_length_set {fn. fn # f \<in> (current_files \<tau> \<union> fs)})) \<notin> |
|
92 fname_length_set {fn. fn # f \<in> (current_files \<tau> \<union> fs)}" |
|
93 by (erule_tac ncf_notin_curf_aux) |
|
94 have a2: "\<And> f pf fs. f # pf \<in> fs \<Longrightarrow> f \<in> {fn. fn # pf \<in> fs}" by auto |
|
95 have a3: "\<And> f pf fs. f \<in> {fn. fn # pf \<in> fs} \<Longrightarrow> length f \<in> fname_length_set {fn. fn # pf \<in> fs}" |
|
96 by (auto simp:fname_length_set_def) |
|
97 show ?thesis |
|
98 apply (simp only:new_childf_general_def next_fname_def all_fname_under_dir_def) |
|
99 apply (rule notI) |
|
100 apply (drule a2, drule a3) |
|
101 apply (simp only:len_fname_all) |
|
102 using a1 by auto |
|
103 qed |
|
104 |
|
105 lemma ncf_notin_curf: |
|
106 "valid \<tau> \<Longrightarrow> new_childf f \<tau> \<notin> (current_files \<tau>)" |
|
107 apply (drule_tac fs = "{}" in ncf_notin_curf_general) |
|
108 apply (simp) |
|
109 apply (simp add:new_childf_def) |
|
110 done |
|
111 |
|
112 lemma ncf_parent_general: "valid \<tau> \<Longrightarrow> parent (new_childf_general f \<tau> fs) = Some f" |
|
113 by (simp add:new_childf_general_def) |
|
114 |
89 lemma ncf_parent: "valid \<tau> \<Longrightarrow> parent (new_childf f \<tau>) = Some f" |
115 lemma ncf_parent: "valid \<tau> \<Longrightarrow> parent (new_childf f \<tau>) = Some f" |
90 by (simp add:new_childf_def) |
116 by (simp add:new_childf_def ncf_parent_general) |
91 |
117 |
92 end |
118 end |
93 |
119 |
94 end |
120 end |