Lem_sorting.thy

chapter {* Generated by Lem from sorting.lem. *}

theory "Lem_sorting" 

imports 
 	 Main
	 "Lem_bool" 
	 "Lem_basic_classes" 
	 "Lem_maybe" 
	 "Lem_list" 
	 "Lem_num" 
	 "Lem" 
	 "~~/src/HOL/Library/Permutation" 

begin 



(*open import Bool Basic_classes Maybe List Num*)

(*open import {isabelle} `~~/src/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 \<Rightarrow> 'a \<Rightarrow> bool)\<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 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
      )
    ))" 
declare isPermutationBy.simps [simp del]




(* ------------------------- *)
(* 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 \<Rightarrow> 'a \<Rightarrow> ordering)\<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool "  where 
     " predicate_of_ord f x y = (
  (case  f x y of
      LT => True
    | EQ => True
    | GT => False
  ))"



end