430 by (auto dest:parentf_has_dirtag)

   430 by (auto dest:parentf_has_dirtag)

   431 

   431 

   432 lemma parentf_is_dir: "\<lbrakk>parent f = Some pf; f \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> pf"

   432 lemma parentf_is_dir: "\<lbrakk>parent f = Some pf; f \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> pf"

   433 by (clarsimp simp:current_files_def parentf_is_dir')

   433 by (clarsimp simp:current_files_def parentf_is_dir')

   434 

   434 

   435 lemma ancenf_is_dir_aux: "\<forall> f. f \<preceq> f' \<and> f \<noteq> f' \<and> f' \<in> current_files \<tau> \<and> valid \<tau> \<longrightarrow> is_dir \<tau> f"

   438 lemma ancenf_is_dir_aux: "\<forall> f. f \<preceq> f' \<and> f \<noteq> f' \<and> f' \<in> current_files \<tau> \<and> valid \<tau> \<longrightarrow> is_dir \<tau> f"

   436 proof (induct f')

   439 proof (induct f')

   437   case Nil show ?case

   440   case Nil show ?case

   438     by (auto simp:current_files_def no_junior_def)

   441     by (auto simp:current_files_def no_junior_def)

   439 next 

   442 next