author nipkow Sun May 13 13:43:34 2018 +0200 (12 months ago) changeset 68160 efce008331f6 parent 68159 620ca44d8b7d child 68161 2053ff42214b child 68163 b168f30e541f
mv lemma
 src/HOL/Data_Structures/Sorting.thy file | annotate | diff | revisions src/HOL/List.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Data_Structures/Sorting.thy	Sun May 13 13:15:50 2018 +0200
1.2 +++ b/src/HOL/Data_Structures/Sorting.thy	Sun May 13 13:43:34 2018 +0200
1.3 @@ -1,28 +1,15 @@
1.4  (* Author: Tobias Nipkow *)
1.5
1.6 -(* FIXME adjust List.sorted to work like below; [code] is different! *)
1.7 -
1.8  theory Sorting
1.9  imports
1.10    Complex_Main
1.11    "HOL-Library.Multiset"
1.12  begin
1.13
1.14 -hide_const List.sorted List.insort
1.15 +hide_const List.insort
1.16
1.17  declare Let_def [simp]
1.18
1.19 -fun sorted :: "'a::linorder list \<Rightarrow> bool" where
1.20 -"sorted [] = True" |
1.21 -"sorted (x # xs) = ((\<forall>y\<in>set xs. x \<le> y) & sorted xs)"
1.22 -
1.23 -lemma sorted_append:
1.24 -  "sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
1.25 -by (induct xs) (auto)
1.26 -
1.27 -lemma sorted01: "length xs \<le> 1 \<Longrightarrow> sorted xs"
1.28 -by(auto simp: le_Suc_eq length_Suc_conv)
1.29 -
1.30
1.31  subsection "Insertion Sort"
1.32
```
```     2.1 --- a/src/HOL/List.thy	Sun May 13 13:15:50 2018 +0200
2.2 +++ b/src/HOL/List.thy	Sun May 13 13:43:34 2018 +0200
2.3 @@ -5021,6 +5021,9 @@
2.4
2.5  lemmas [code] = sorted.simps(1) sorted2_simps
2.6
2.7 +lemma sorted01: "length xs \<le> 1 \<Longrightarrow> sorted xs"
2.8 +by (simp add: sorted_sorted_wrt sorted_wrt01)
2.9 +
2.10  lemma sorted_tl:
2.11    "sorted xs \<Longrightarrow> sorted (tl xs)"
2.12  by (cases xs) (simp_all)
```