summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | Andreas Lochbihler |

Tue, 01 Dec 2015 12:27:16 +0100 | |

changeset 61764 | ac6e5de1a50b |

parent 61759 | 49353865e539 |

child 61765 | 13ca8f4f6907 |

strengthen lemma

--- a/src/HOL/Library/Transitive_Closure_Table.thy Mon Nov 30 19:12:08 2015 +0100 +++ b/src/HOL/Library/Transitive_Closure_Table.thy Tue Dec 01 12:27:16 2015 +0100 @@ -93,14 +93,14 @@ lemma rtrancl_path_distinct: assumes xy: "rtrancl_path r x xs y" - obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" + obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" and "set xs' \<subseteq> set xs" using xy proof (induct xs rule: measure_induct_rule [of length]) case (less xs) show ?case proof (cases "distinct (x # xs)") case True - with \<open>rtrancl_path r x xs y\<close> show ?thesis by (rule less) + with \<open>rtrancl_path r x xs y\<close> show ?thesis by (rule less) simp next case False then have "\<exists>as bs cs a. x # xs = as @ [a] @ bs @ [a] @ cs" @@ -112,11 +112,11 @@ case Nil with xxs have x: "x = a" and xs: "xs = bs @ a # cs" by auto - from x xs \<open>rtrancl_path r x xs y\<close> have cs: "rtrancl_path r x cs y" + from x xs \<open>rtrancl_path r x xs y\<close> have cs: "rtrancl_path r x cs y" "set cs \<subseteq> set xs" by (auto elim: rtrancl_path_appendE) from xs have "length cs < length xs" by simp then show ?thesis - by (rule less(1)) (iprover intro: cs less(2))+ + by (rule less(1))(blast intro: cs less(2) order_trans del: subsetI)+ next case (Cons d ds) with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)" @@ -127,9 +127,10 @@ from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE) with xa have xy: "rtrancl_path r x ((ds @ [a]) @ cs) y" by (rule rtrancl_path_trans) + from xs have set: "set ((ds @ [a]) @ cs) \<subseteq> set xs" by auto from xs have "length ((ds @ [a]) @ cs) < length xs" by simp then show ?thesis - by (rule less(1)) (iprover intro: xy less(2))+ + by (rule less(1))(blast intro: xy less(2) set[THEN subsetD])+ qed qed qed