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