src/HOL/List.thy
changeset 66442 050bc74d55ed
parent 66441 b9468503742a
child 66508 5df7a346f07b
equal deleted inserted replaced
66441:b9468503742a 66442:050bc74d55ed
  4884   case 3 thus ?case
  4884   case 3 thus ?case
  4885     by(simp add: sorted_wrt_append sorted_wrt_Cons assms)
  4885     by(simp add: sorted_wrt_append sorted_wrt_Cons assms)
  4886       (meson assms transpD)
  4886       (meson assms transpD)
  4887 qed simp_all
  4887 qed simp_all
  4888 
  4888 
       
  4889 lemma sorted_wrt_mono:
       
  4890   "(\<And>x y. P x y \<Longrightarrow> Q x y) \<Longrightarrow> sorted_wrt P xs \<Longrightarrow> sorted_wrt Q xs"
       
  4891 by(induction xs rule: sorted_wrt_induct)(auto)
       
  4892 
  4889 text \<open>Strictly Ascending Sequences of Natural Numbers\<close>    
  4893 text \<open>Strictly Ascending Sequences of Natural Numbers\<close>    
  4890 
  4894 
  4891 lemma sorted_wrt_upt[simp]: "sorted_wrt (op <) [0..<n]"
  4895 lemma sorted_wrt_upt[simp]: "sorted_wrt (op <) [0..<n]"
  4892 by(induction n) (auto simp: sorted_wrt_append)
  4896 by(induction n) (auto simp: sorted_wrt_append)
  4893 
  4897