1(* Author: Tobias Nipkow *) 2 3section \<open>Lists Sorted wrt $<$\<close> 4 5theory Sorted_Less 6imports Less_False 7begin 8 9hide_const sorted 10 11text \<open>Is a list sorted without duplicates, i.e., wrt @{text"<"}?.\<close> 12 13abbreviation sorted :: "'a::linorder list \<Rightarrow> bool" where 14"sorted \<equiv> sorted_wrt (<)" 15 16lemmas sorted_wrt_Cons = sorted_wrt.simps(2) 17 18text \<open>The definition of @{const sorted_wrt} relates each element to all the elements after it. 19This causes a blowup of the formulas. Thus we simplify matters by only comparing adjacent elements.\<close> 20 21declare 22 sorted_wrt.simps(2)[simp del] 23 sorted_wrt1[simp] sorted_wrt2[OF transp_less, simp] 24 25lemma sorted_cons: "sorted (x#xs) \<Longrightarrow> sorted xs" 26by(simp add: sorted_wrt_Cons) 27 28lemma sorted_cons': "ASSUMPTION (sorted (x#xs)) \<Longrightarrow> sorted xs" 29by(rule ASSUMPTION_D [THEN sorted_cons]) 30 31lemma sorted_snoc: "sorted (xs @ [y]) \<Longrightarrow> sorted xs" 32by(simp add: sorted_wrt_append) 33 34lemma sorted_snoc': "ASSUMPTION (sorted (xs @ [y])) \<Longrightarrow> sorted xs" 35by(rule ASSUMPTION_D [THEN sorted_snoc]) 36 37lemma sorted_mid_iff: 38 "sorted(xs @ y # ys) = (sorted(xs @ [y]) \<and> sorted(y # ys))" 39by(fastforce simp add: sorted_wrt_Cons sorted_wrt_append) 40 41lemma sorted_mid_iff2: 42 "sorted(x # xs @ y # ys) = 43 (sorted(x # xs) \<and> x < y \<and> sorted(xs @ [y]) \<and> sorted(y # ys))" 44by(fastforce simp add: sorted_wrt_Cons sorted_wrt_append) 45 46lemma sorted_mid_iff': "NO_MATCH [] ys \<Longrightarrow> 47 sorted(xs @ y # ys) = (sorted(xs @ [y]) \<and> sorted(y # ys))" 48by(rule sorted_mid_iff) 49 50lemmas sorted_lems = sorted_mid_iff' sorted_mid_iff2 sorted_cons' sorted_snoc' 51 52text\<open>Splay trees need two additional @{const sorted} lemmas:\<close> 53 54lemma sorted_snoc_le: 55 "ASSUMPTION(sorted(xs @ [x])) \<Longrightarrow> x \<le> y \<Longrightarrow> sorted (xs @ [y])" 56by (auto simp add: sorted_wrt_append ASSUMPTION_def) 57 58lemma sorted_Cons_le: 59 "ASSUMPTION(sorted(x # xs)) \<Longrightarrow> y \<le> x \<Longrightarrow> sorted (y # xs)" 60by (auto simp add: sorted_wrt_Cons ASSUMPTION_def) 61 62end 63