author | Andreas Lochbihler |

Tue Dec 01 12:27:16 2015 +0100 (2015-12-01) | |

changeset 61764 | ac6e5de1a50b |

parent 61759 | 49353865e539 |

child 61765 | 13ca8f4f6907 |

strengthen lemma

1.1 --- a/src/HOL/Library/Transitive_Closure_Table.thy Mon Nov 30 19:12:08 2015 +0100 1.2 +++ b/src/HOL/Library/Transitive_Closure_Table.thy Tue Dec 01 12:27:16 2015 +0100 1.3 @@ -93,14 +93,14 @@ 1.4 1.5 lemma rtrancl_path_distinct: 1.6 assumes xy: "rtrancl_path r x xs y" 1.7 - obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" 1.8 + obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" and "set xs' \<subseteq> set xs" 1.9 using xy 1.10 proof (induct xs rule: measure_induct_rule [of length]) 1.11 case (less xs) 1.12 show ?case 1.13 proof (cases "distinct (x # xs)") 1.14 case True 1.15 - with \<open>rtrancl_path r x xs y\<close> show ?thesis by (rule less) 1.16 + with \<open>rtrancl_path r x xs y\<close> show ?thesis by (rule less) simp 1.17 next 1.18 case False 1.19 then have "\<exists>as bs cs a. x # xs = as @ [a] @ bs @ [a] @ cs" 1.20 @@ -112,11 +112,11 @@ 1.21 case Nil 1.22 with xxs have x: "x = a" and xs: "xs = bs @ a # cs" 1.23 by auto 1.24 - from x xs \<open>rtrancl_path r x xs y\<close> have cs: "rtrancl_path r x cs y" 1.25 + from x xs \<open>rtrancl_path r x xs y\<close> have cs: "rtrancl_path r x cs y" "set cs \<subseteq> set xs" 1.26 by (auto elim: rtrancl_path_appendE) 1.27 from xs have "length cs < length xs" by simp 1.28 then show ?thesis 1.29 - by (rule less(1)) (iprover intro: cs less(2))+ 1.30 + by (rule less(1))(blast intro: cs less(2) order_trans del: subsetI)+ 1.31 next 1.32 case (Cons d ds) 1.33 with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)" 1.34 @@ -127,9 +127,10 @@ 1.35 from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE) 1.36 with xa have xy: "rtrancl_path r x ((ds @ [a]) @ cs) y" 1.37 by (rule rtrancl_path_trans) 1.38 + from xs have set: "set ((ds @ [a]) @ cs) \<subseteq> set xs" by auto 1.39 from xs have "length ((ds @ [a]) @ cs) < length xs" by simp 1.40 then show ?thesis 1.41 - by (rule less(1)) (iprover intro: xy less(2))+ 1.42 + by (rule less(1))(blast intro: xy less(2) set[THEN subsetD])+ 1.43 qed 1.44 qed 1.45 qed