equal
deleted
inserted
replaced
4969 by(induction xs)(auto) |
4969 by(induction xs)(auto) |
4970 |
4970 |
4971 lemma sorted_wrt01: "length xs \<le> 1 \<Longrightarrow> sorted_wrt P xs" |
4971 lemma sorted_wrt01: "length xs \<le> 1 \<Longrightarrow> sorted_wrt P xs" |
4972 by(auto simp: le_Suc_eq length_Suc_conv) |
4972 by(auto simp: le_Suc_eq length_Suc_conv) |
4973 |
4973 |
|
4974 lemma sorted_wrt_iff_nth_Suc: |
|
4975 "sorted_wrt P xs = (\<forall>i j. i < j \<longrightarrow> j < length xs \<longrightarrow> P (xs ! i) (xs ! j))" |
|
4976 apply(induction xs) |
|
4977 apply simp |
|
4978 apply(force simp: in_set_conv_nth nth_Cons split: nat.split) |
|
4979 done |
|
4980 |
|
4981 lemma sorted_wrt_nth_less: |
|
4982 "\<lbrakk> sorted_wrt P xs; i < j; j < length xs \<rbrakk> \<Longrightarrow> P (xs ! i) (xs ! j)" |
|
4983 by(auto simp: sorted_wrt_iff_nth_Suc) |
|
4984 |
4974 text \<open>Strictly Ascending Sequences of Natural Numbers\<close> |
4985 text \<open>Strictly Ascending Sequences of Natural Numbers\<close> |
4975 |
4986 |
4976 lemma sorted_wrt_upt[simp]: "sorted_wrt (<) [m..<n]" |
4987 lemma sorted_wrt_upt[simp]: "sorted_wrt (<) [m..<n]" |
4977 by(induction n) (auto simp: sorted_wrt_append) |
4988 by(induction n) (auto simp: sorted_wrt_append) |
4978 |
4989 |