Theory Lem_sorting

chapter ‹Generated by Lem from ‹sorting.lem›.›

theory "Lem_sorting" 

imports
  Main
  "Lem_bool"
  "Lem_basic_classes"
  "Lem_maybe"
  "Lem_list"
  "Lem_num"
  "Lem"
  "HOL-Combinatorics.List_Permutation"

begin 



― ‹‹open import Bool Basic_classes Maybe List Num››

― ‹‹open import {isabelle} `HOL-Library.Permutation`››
― ‹‹open import {coq} `Coq.Lists.List`››
― ‹‹open import {hol} `sortingTheory` `permLib`››
― ‹‹open import {isabelle} `$LIB_DIR/Lem`››

― ‹‹ ------------------------- ››
― ‹‹ permutations              ››
― ‹‹ ------------------------- ››

― ‹‹val isPermutation : forall 'a. Eq 'a => list 'a -> list 'a -> bool››
― ‹‹val isPermutationBy : forall 'a. ('a -> 'a -> bool) -> list 'a -> list 'a -> bool››

fun  isPermutationBy  :: "('a ⇒ 'a ⇒ bool)⇒ 'a list ⇒ 'a list ⇒ bool "  where 
     " isPermutationBy eq ([]) l2 = ( (l2 = []))"
|" isPermutationBy eq (x # xs) l2 = ( (
      (case  delete_first (eq x) l2 of
          None => False
        | Some ys => isPermutationBy eq xs ys
      )
    ))"




― ‹‹ ------------------------- ››
― ‹‹ isSorted                  ››
― ‹‹ ------------------------- ››

― ‹‹ isSortedBy R l 
   checks, whether the list l is sorted by ordering R. 
   R should represent an order, i.e. it should be transitive.
   Different backends defined "isSorted" slightly differently. However,
   the definitions coincide for transitive R. Therefore there is the
   following restriction:

   WARNING: Use isSorted and isSortedBy only with transitive relations!
››

― ‹‹val isSorted : forall 'a. Ord 'a => list 'a -> bool››
― ‹‹val isSortedBy : forall 'a. ('a -> 'a -> bool) -> list 'a -> bool››

― ‹‹ DPM: rejigged the definition with a nested match to get past Coq's termination checker. ››
― ‹‹let rec isSortedBy cmp l=  match l with
  | [] -> true
  | x1 :: xs ->
    match xs with
      | [] -> true
      | x2 :: _ -> (cmp x1 x2 && isSortedBy cmp xs)
    end
end››


― ‹‹ ----------------------- ››
― ‹‹ insertion sort          ››
― ‹‹ ----------------------- ›› 

― ‹‹val insert : forall 'a. Ord 'a => 'a -> list 'a -> list 'a››
― ‹‹val insertBy : forall 'a. ('a -> 'a -> bool) -> 'a -> list 'a -> list 'a››

― ‹‹val insertSort: forall 'a. Ord 'a => list 'a -> list 'a››
― ‹‹val insertSortBy: forall 'a. ('a -> 'a -> bool) -> list 'a -> list 'a››

― ‹‹let rec insertBy cmp e l=  match l with
  | [] -> [e]
  | x :: xs -> if cmp x e then x :: (insertBy cmp e xs) else (e :: x :: xs)
end››

― ‹‹let insertSortBy cmp l=  List.foldl (fun l e -> insertBy cmp e l) [] l››


― ‹‹ ----------------------- ››
― ‹‹ general sorting         ››
― ‹‹ ----------------------- ›› 

― ‹‹val sort: forall 'a. Ord 'a => list 'a -> list 'a››
― ‹‹val sortBy: forall 'a. ('a -> 'a -> bool) -> list 'a -> list 'a››
― ‹‹val sortByOrd: forall 'a. ('a -> 'a -> ordering) -> list 'a -> list 'a››

― ‹‹val predicate_of_ord : forall 'a. ('a -> 'a -> ordering) -> 'a -> 'a -> bool››
definition predicate_of_ord  :: "('a ⇒ 'a ⇒ ordering)⇒ 'a ⇒ 'a ⇒ bool "  where 
     " predicate_of_ord f x y = (
  (case  f x y of
      LT => True
    | EQ => True
    | GT => False
  ))"



end