equal
deleted
inserted
replaced
350 apply (subgoal_tac "finite (fname_length_set {fn. fn # f \<in> current_files s})") |
350 apply (subgoal_tac "finite (fname_length_set {fn. fn # f \<in> current_files s})") |
351 defer |
351 defer |
352 apply (simp add:fname_length_set_def) |
352 apply (simp add:fname_length_set_def) |
353 apply (rule finite_imageI) using finite_cf[where s = s] |
353 apply (rule finite_imageI) using finite_cf[where s = s] |
354 apply (drule_tac h = "\<lambda> f'. case f' of [] \<Rightarrow> '''' | fn # pf' \<Rightarrow> if (pf' = f) then fn else ''''" in finite_imageI) |
354 apply (drule_tac h = "\<lambda> f'. case f' of [] \<Rightarrow> '''' | fn # pf' \<Rightarrow> if (pf' = f) then fn else ''''" in finite_imageI) |
355 apply (rule_tac B = "(list_case [] (\<lambda>fn pf'. if pf' = f then fn else []) ` current_files s)" in finite_subset) |
355 apply (rule_tac B = "(case_list [] (\<lambda>fn pf'. if pf' = f then fn else []) ` current_files s)" in finite_subset) |
356 unfolding image_def |
356 unfolding image_def |
357 apply(auto)[1] |
357 apply(auto)[1] |
358 apply (rule_tac x = "x # f" in bexI, simp+) |
358 apply (rule_tac x = "x # f" in bexI, simp+) |
359 apply (drule_tac s = "(fname_length_set {fn. fn # f \<in> current_files s})" in nn_notin_aux) |
359 apply (drule_tac s = "(fname_length_set {fn. fn # f \<in> current_files s})" in nn_notin_aux) |
360 apply (erule_tac x = "length (CHR ''a'' # fname_all_a (Max (fname_length_set {fn. fn # f \<in> current_files s})))" in ballE) |
360 apply (erule_tac x = "length (CHR ''a'' # fname_all_a (Max (fname_length_set {fn. fn # f \<in> current_files s})))" in ballE) |