added simp lemma
authornipkow
Fri May 22 08:52:23 2020 +0200 (9 days ago)
changeset 718553e343c0c2138
parent 71854 6a51e64ba13d
child 71856 e9df7895e331
added simp lemma
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Thu May 21 20:00:09 2020 +0000
     1.2 +++ b/src/HOL/List.thy	Fri May 22 08:52:23 2020 +0200
     1.3 @@ -414,6 +414,9 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma strict_sorted_iff: "strict_sorted l \<longleftrightarrow> sorted l \<and> distinct l"
     1.8 +by (induction l) (use less_le in auto)
     1.9 +
    1.10  
    1.11  subsubsection \<open>List comprehension\<close>
    1.12  
    1.13 @@ -6049,6 +6052,10 @@
    1.14    case False thus ?thesis by simp
    1.15  qed
    1.16  
    1.17 +lemma length_sorted_list_of_set[simp]:
    1.18 +  "finite A \<Longrightarrow> length(sorted_list_of_set A) = card A"
    1.19 +by(simp flip: distinct_card)
    1.20 +
    1.21  lemmas sorted_list_of_set = set_sorted_list_of_set sorted_sorted_list_of_set distinct_sorted_list_of_set
    1.22  
    1.23  lemma sorted_list_of_set_sort_remdups [code]:
    1.24 @@ -6075,9 +6082,6 @@
    1.25    "sorted_list_of_set {m..<n} = [m..<n]"
    1.26  by (rule sorted_distinct_set_unique) simp_all
    1.27  
    1.28 -lemma strict_sorted_iff: "strict_sorted l \<longleftrightarrow> sorted l \<and> distinct l"
    1.29 -  by (induction l) (use less_le in auto)
    1.30 -
    1.31  lemma strict_sorted_list_of_set [simp]: "strict_sorted (sorted_list_of_set A)"
    1.32    by (simp add: strict_sorted_iff)
    1.33