346 (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss <=[r] ts) \<and> |
346 (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss <=[r] ts) \<and> |
347 (\<forall>p\<in>w. p < n)" and |
347 (\<forall>p\<in>w. p < n)" and |
348 r = "{(ss',ss) . ss <[r] ss'} <*lex*> finite_psubset" |
348 r = "{(ss',ss) . ss <[r] ss'} <*lex*> finite_psubset" |
349 in while_rule) |
349 in while_rule) |
350 |
350 |
351 \<comment> "Invariant holds initially:" |
351 \<comment> \<open>Invariant holds initially:\<close> |
352 apply (simp add:stables_def) |
352 apply (simp add:stables_def) |
353 |
353 |
354 \<comment> "Invariant is preserved:" |
354 \<comment> \<open>Invariant is preserved:\<close> |
355 apply(simp add: stables_def split_paired_all) |
355 apply(simp add: stables_def split_paired_all) |
356 apply(rename_tac ss w) |
356 apply(rename_tac ss w) |
357 apply(subgoal_tac "(SOME p. p \<in> w) \<in> w") |
357 apply(subgoal_tac "(SOME p. p \<in> w) \<in> w") |
358 prefer 2 apply (fast intro: someI) |
358 prefer 2 apply (fast intro: someI) |
359 apply(subgoal_tac "\<forall>(q,t) \<in> set (step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w))). q < length ss \<and> t \<in> A") |
359 apply(subgoal_tac "\<forall>(q,t) \<in> set (step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w))). q < length ss \<and> t \<in> A") |
391 apply clarsimp |
391 apply clarsimp |
392 apply (blast intro!: merges_bounded_lemma) |
392 apply (blast intro!: merges_bounded_lemma) |
393 apply (blast dest!: boundedD) |
393 apply (blast dest!: boundedD) |
394 |
394 |
395 |
395 |
396 \<comment> "Postcondition holds upon termination:" |
396 \<comment> \<open>Postcondition holds upon termination:\<close> |
397 apply(clarsimp simp add: stables_def split_paired_all) |
397 apply(clarsimp simp add: stables_def split_paired_all) |
398 |
398 |
399 \<comment> "Well-foundedness of the termination relation:" |
399 \<comment> \<open>Well-foundedness of the termination relation:\<close> |
400 apply (rule wf_lex_prod) |
400 apply (rule wf_lex_prod) |
401 apply (insert orderI [THEN acc_le_listI]) |
401 apply (insert orderI [THEN acc_le_listI]) |
402 apply (simp add: acc_def lesssub_def wfP_wf_eq [symmetric]) |
402 apply (simp add: acc_def lesssub_def wfP_wf_eq [symmetric]) |
403 apply (rule wf_finite_psubset) |
403 apply (rule wf_finite_psubset) |
404 |
404 |
405 \<comment> "Loop decreases along termination relation:" |
405 \<comment> \<open>Loop decreases along termination relation:\<close> |
406 apply(simp add: stables_def split_paired_all) |
406 apply(simp add: stables_def split_paired_all) |
407 apply(rename_tac ss w) |
407 apply(rename_tac ss w) |
408 apply(subgoal_tac "(SOME p. p \<in> w) \<in> w") |
408 apply(subgoal_tac "(SOME p. p \<in> w) \<in> w") |
409 prefer 2 apply (fast intro: someI) |
409 prefer 2 apply (fast intro: someI) |
410 apply(subgoal_tac "\<forall>(q,t) \<in> set (step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w))). q < length ss \<and> t \<in> A") |
410 apply(subgoal_tac "\<forall>(q,t) \<in> set (step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w))). q < length ss \<and> t \<in> A") |