equal
deleted
inserted
replaced
81 apply (drule nn_notin_aux) |
81 apply (drule nn_notin_aux) |
82 apply auto |
82 apply auto |
83 done |
83 done |
84 |
84 |
85 lemma ncf_notin_curf_general: |
85 lemma ncf_notin_curf_general: |
86 assumes vd: "valid \<tau>" and fin_fs: "finite fs" |
86 assumes fin_fs: "finite fs" |
87 shows "new_childf_general f \<tau> fs \<notin> (current_files \<tau> \<union> fs)" |
87 shows "new_childf_general f fs \<notin> fs" |
88 proof- |
88 proof- |
89 from vd fin_fs have "finite (current_files \<tau> \<union> fs)" |
89 have a1: "Suc (Max (fname_length_set {fn. fn # f \<in> fs})) \<notin> |
90 by (auto dest:finite_cf) |
90 fname_length_set {fn. fn # f \<in> fs}" |
91 hence a1: "Suc (Max (fname_length_set {fn. fn # f \<in> (current_files \<tau> \<union> fs)})) \<notin> |
91 using fin_fs |
92 fname_length_set {fn. fn # f \<in> (current_files \<tau> \<union> fs)}" |
|
93 by (erule_tac ncf_notin_curf_aux) |
92 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 |
93 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}" |
94 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) |
95 by (auto simp:fname_length_set_def) |
97 show ?thesis |
96 show ?thesis |
102 using a1 by auto |
101 using a1 by auto |
103 qed |
102 qed |
104 |
103 |
105 lemma ncf_notin_curf: |
104 lemma ncf_notin_curf: |
106 "valid \<tau> \<Longrightarrow> new_childf f \<tau> \<notin> (current_files \<tau>)" |
105 "valid \<tau> \<Longrightarrow> new_childf f \<tau> \<notin> (current_files \<tau>)" |
107 apply (drule_tac fs = "{}" in ncf_notin_curf_general) |
106 apply (drule finite_cf) |
108 apply (simp) |
107 apply (drule_tac fs = "current_files \<tau>" in ncf_notin_curf_general) |
109 apply (simp add:new_childf_def) |
108 apply (simp add:new_childf_def) |
110 done |
109 done |
111 |
110 |
112 lemma ncf_parent_general: "valid \<tau> \<Longrightarrow> parent (new_childf_general f \<tau> fs) = Some f" |
111 lemma ncf_parent_general: "valid \<tau> \<Longrightarrow> parent (new_childf_general f fs) = Some f" |
113 by (simp add:new_childf_general_def) |
112 by (simp add:new_childf_general_def) |
114 |
113 |
115 lemma ncf_parent: "valid \<tau> \<Longrightarrow> parent (new_childf f \<tau>) = Some f" |
114 lemma ncf_parent: "valid \<tau> \<Longrightarrow> parent (new_childf f \<tau>) = Some f" |
116 by (simp add:new_childf_def ncf_parent_general) |
115 by (simp add:new_childf_def ncf_parent_general) |
117 |
116 |