mv lemma
authornipkow
Sun May 13 13:43:34 2018 +0200 (12 months ago)
changeset 68160efce008331f6
parent 68159 620ca44d8b7d
child 68161 2053ff42214b
child 68163 b168f30e541f
mv lemma
src/HOL/Data_Structures/Sorting.thy
src/HOL/List.thy
     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)