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

author | Andreas Lochbihler |

Tue, 01 Dec 2015 12:28:02 +0100 | |

changeset 61765 | 13ca8f4f6907 |

parent 61764 | ac6e5de1a50b |

child 61766 | 507b39df1a57 |

add lemmas

--- a/src/HOL/Library/Transitive_Closure_Table.thy Tue Dec 01 12:27:16 2015 +0100 +++ b/src/HOL/Library/Transitive_Closure_Table.thy Tue Dec 01 12:28:02 2015 +0100 @@ -207,4 +207,23 @@ code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce +lemma rtrancl_path_Range: "\<lbrakk> rtrancl_path R x xs y; z \<in> set xs \<rbrakk> \<Longrightarrow> RangeP R z" +by(induction rule: rtrancl_path.induct) auto + +lemma rtrancl_path_Range_end: "\<lbrakk> rtrancl_path R x xs y; xs \<noteq> [] \<rbrakk> \<Longrightarrow> RangeP R y" +by(induction rule: rtrancl_path.induct)(auto elim: rtrancl_path.cases) + +lemma rtrancl_path_nth: + "\<lbrakk> rtrancl_path R x xs y; i < length xs \<rbrakk> \<Longrightarrow> R ((x # xs) ! i) (xs ! i)" +proof(induction arbitrary: i rule: rtrancl_path.induct) + case step thus ?case by(cases i) simp_all +qed simp + +lemma rtrancl_path_last: "\<lbrakk> rtrancl_path R x xs y; xs \<noteq> [] \<rbrakk> \<Longrightarrow> last xs = y" +by(induction rule: rtrancl_path.induct)(auto elim: rtrancl_path.cases) + +lemma rtrancl_path_mono: + "\<lbrakk> rtrancl_path R x p y; \<And>x y. R x y \<Longrightarrow> S x y \<rbrakk> \<Longrightarrow> rtrancl_path S x p y" +by(induction rule: rtrancl_path.induct)(auto intro: rtrancl_path.intros) + end \ No newline at end of file