add lemmas
authorAndreas Lochbihler
Tue Dec 01 12:28:02 2015 +0100 (2015-12-01)
changeset 6176513ca8f4f6907
parent 61764 ac6e5de1a50b
child 61766 507b39df1a57
add lemmas
src/HOL/Library/Transitive_Closure_Table.thy
     1.1 --- a/src/HOL/Library/Transitive_Closure_Table.thy	Tue Dec 01 12:27:16 2015 +0100
     1.2 +++ b/src/HOL/Library/Transitive_Closure_Table.thy	Tue Dec 01 12:28:02 2015 +0100
     1.3 @@ -207,4 +207,23 @@
     1.4  code_pred rtranclp
     1.5    using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce
     1.6  
     1.7 +lemma rtrancl_path_Range: "\<lbrakk> rtrancl_path R x xs y; z \<in> set xs \<rbrakk> \<Longrightarrow> RangeP R z"
     1.8 +by(induction rule: rtrancl_path.induct) auto
     1.9 +
    1.10 +lemma rtrancl_path_Range_end: "\<lbrakk> rtrancl_path R x xs y; xs \<noteq> [] \<rbrakk> \<Longrightarrow> RangeP R y"
    1.11 +by(induction rule: rtrancl_path.induct)(auto elim: rtrancl_path.cases)
    1.12 +
    1.13 +lemma rtrancl_path_nth:
    1.14 +  "\<lbrakk> rtrancl_path R x xs y; i < length xs \<rbrakk> \<Longrightarrow> R ((x # xs) ! i) (xs ! i)"
    1.15 +proof(induction arbitrary: i rule: rtrancl_path.induct)
    1.16 +  case step thus ?case by(cases i) simp_all
    1.17 +qed simp
    1.18 +
    1.19 +lemma rtrancl_path_last: "\<lbrakk> rtrancl_path R x xs y; xs \<noteq> [] \<rbrakk> \<Longrightarrow> last xs = y"
    1.20 +by(induction rule: rtrancl_path.induct)(auto elim: rtrancl_path.cases)
    1.21 +
    1.22 +lemma rtrancl_path_mono:
    1.23 +  "\<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"
    1.24 +by(induction rule: rtrancl_path.induct)(auto intro: rtrancl_path.intros)
    1.25 +
    1.26  end
    1.27 \ No newline at end of file