equal
deleted
inserted
replaced
189 "\<lbrakk> T\<in>Reach E; R<length E \<rbrakk> \<Longrightarrow> Reach(E[R:=(fst(E!R),T)]) \<subseteq> Reach E" |
189 "\<lbrakk> T\<in>Reach E; R<length E \<rbrakk> \<Longrightarrow> Reach(E[R:=(fst(E!R),T)]) \<subseteq> Reach E" |
190 apply (unfold Reach_def) |
190 apply (unfold Reach_def) |
191 apply clarify |
191 apply clarify |
192 apply simp |
192 apply simp |
193 apply(case_tac "\<exists>i<length path - 1. (fst(E!R),T)=(path!(Suc i),path!i)") |
193 apply(case_tac "\<exists>i<length path - 1. (fst(E!R),T)=(path!(Suc i),path!i)") |
194 --\<open>the changed edge is part of the path\<close> |
194 \<comment>\<open>the changed edge is part of the path\<close> |
195 apply(erule exE) |
195 apply(erule exE) |
196 apply(drule_tac P = "\<lambda>i. i<length path - 1 \<and> (fst(E!R),T)=(path!Suc i,path!i)" in Ex_first_occurrence) |
196 apply(drule_tac P = "\<lambda>i. i<length path - 1 \<and> (fst(E!R),T)=(path!Suc i,path!i)" in Ex_first_occurrence) |
197 apply clarify |
197 apply clarify |
198 apply(erule disjE) |
198 apply(erule disjE) |
199 --\<open>T is NOT a root\<close> |
199 \<comment>\<open>T is NOT a root\<close> |
200 apply clarify |
200 apply clarify |
201 apply(rule_tac x = "(take m path)@patha" in exI) |
201 apply(rule_tac x = "(take m path)@patha" in exI) |
202 apply(subgoal_tac "\<not>(length path\<le>m)") |
202 apply(subgoal_tac "\<not>(length path\<le>m)") |
203 prefer 2 apply arith |
203 prefer 2 apply arith |
204 apply(simp) |
204 apply(simp) |
238 apply(rotate_tac -4) |
238 apply(rotate_tac -4) |
239 apply(erule_tac x = "i - m" in allE) |
239 apply(erule_tac x = "i - m" in allE) |
240 apply(subgoal_tac "Suc (i - m)=(Suc i - m)" ) |
240 apply(subgoal_tac "Suc (i - m)=(Suc i - m)" ) |
241 prefer 2 apply arith |
241 prefer 2 apply arith |
242 apply simp |
242 apply simp |
243 --\<open>T is a root\<close> |
243 \<comment>\<open>T is a root\<close> |
244 apply(case_tac "m=0") |
244 apply(case_tac "m=0") |
245 apply force |
245 apply force |
246 apply(rule_tac x = "take (Suc m) path" in exI) |
246 apply(rule_tac x = "take (Suc m) path" in exI) |
247 apply(subgoal_tac "\<not>(length path\<le>Suc m)" ) |
247 apply(subgoal_tac "\<not>(length path\<le>Suc m)" ) |
248 prefer 2 apply arith |
248 prefer 2 apply arith |
251 apply simp |
251 apply simp |
252 apply clarify |
252 apply clarify |
253 apply(case_tac "R=j") |
253 apply(case_tac "R=j") |
254 apply(force simp add: nth_list_update) |
254 apply(force simp add: nth_list_update) |
255 apply(force simp add: nth_list_update) |
255 apply(force simp add: nth_list_update) |
256 --\<open>the changed edge is not part of the path\<close> |
256 \<comment>\<open>the changed edge is not part of the path\<close> |
257 apply(rule_tac x = "path" in exI) |
257 apply(rule_tac x = "path" in exI) |
258 apply simp |
258 apply simp |
259 apply clarify |
259 apply clarify |
260 apply(erule_tac x = "i" in allE) |
260 apply(erule_tac x = "i" in allE) |
261 apply clarify |
261 apply clarify |
274 apply (unfold Reach_def) |
274 apply (unfold Reach_def) |
275 apply simp |
275 apply simp |
276 apply(erule disjE) |
276 apply(erule disjE) |
277 prefer 2 apply force |
277 prefer 2 apply force |
278 apply clarify |
278 apply clarify |
279 --\<open>there exist a black node in the path to T\<close> |
279 \<comment>\<open>there exist a black node in the path to T\<close> |
280 apply(case_tac "\<exists>m<length path. M!(path!m)=Black") |
280 apply(case_tac "\<exists>m<length path. M!(path!m)=Black") |
281 apply(erule exE) |
281 apply(erule exE) |
282 apply(drule_tac P = "\<lambda>m. m<length path \<and> M!(path!m)=Black" in Ex_first_occurrence) |
282 apply(drule_tac P = "\<lambda>m. m<length path \<and> M!(path!m)=Black" in Ex_first_occurrence) |
283 apply clarify |
283 apply clarify |
284 apply(case_tac "ma") |
284 apply(case_tac "ma") |
316 apply (unfold Reach_def) |
316 apply (unfold Reach_def) |
317 apply simp |
317 apply simp |
318 apply(erule disjE) |
318 apply(erule disjE) |
319 prefer 2 apply force |
319 prefer 2 apply force |
320 apply clarify |
320 apply clarify |
321 --\<open>there exist a black node in the path to T\<close> |
321 \<comment>\<open>there exist a black node in the path to T\<close> |
322 apply(case_tac "\<exists>m<length path. M!(path!m)=Black") |
322 apply(case_tac "\<exists>m<length path. M!(path!m)=Black") |
323 apply(erule exE) |
323 apply(erule exE) |
324 apply(drule_tac P = "\<lambda>m. m<length path \<and> M!(path!m)=Black" in Ex_first_occurrence) |
324 apply(drule_tac P = "\<lambda>m. m<length path \<and> M!(path!m)=Black" in Ex_first_occurrence) |
325 apply clarify |
325 apply clarify |
326 apply(case_tac "ma") |
326 apply(case_tac "ma") |