my_list_induction[X:TYPE] : THEORY
BEGIN
   less(l1,l2: list[X]) : bool = length(l1) < length(l2)

   less_wf: LEMMA well_founded?(less) % :-)

   list_length_induction :LEMMA % :-)
        (FORALL (p:pred[list[X]]):
            (FORALL (g:list[X]):
                (FORALL (s:list[X]):
                    less(s,g) IMPLIES p(s))
                        IMPLIES p(g))
            IMPLIES (FORALL (l:list[X]): p(l)))

END my_list_induction

my_list_props[X:TYPE] : THEORY
BEGIN
    occ(x:X,l:list[X]) : RECURSIVE nat =
      CASES l
        OF null   : 0 ,
        cons(y,l) : IF x=y THEN occ(x,l)+1 ELSE occ(x,l) ENDIF
      ENDCASES
    MEASURE length(l)

    occ_nth: LEMMA
       FORALL(l:list[X]): FORALL(x:X): occ(x,l) > 0 IMPLIES 
          EXISTS(i:nat): i<length(l) AND nth(l,i) = x

    nth_occ: LEMMA
       FORALL(l:list[X]): FORALL(i:nat): i<length(l) IMPLIES occ(nth(l,i),l) > 0 

    perm?( l1,l2 : list[X]) : bool = FORALL(x:X): occ(x,l1) = occ(x,l2)

    perm_null: LEMMA % :-)
       FORALL(l:list[X]): perm?(null, l) IMPLIES l = null

    perm_commutative: LEMMA % :-)
       FORALL(l1,l2: list[X]):perm?(l1,l2) IMPLIES perm?(l2,l1)

    append_occ: LEMMA % :-)
       FORALL( l1,l2:list[X] ): FORALL(x:X): occ(x,append(l1,l2)) = occ(x,l1)+occ(x,l2)

    length_append: LEMMA % :-)
 	   FORALL( l1,l2:list[X] ):length(append(l1,l2)) = length(l1) + length(l2)

    nth_append: LEMMA % :-( to be done
       FORALL( l1,l2:list[X] ): FORALL(i:nat): i < length(l1)+length(l2) IMPLIES
           nth(append(l1,l2),i) = IF i < length(l1) THEN nth(l1,i) ELSE nth(l2,i-length(l1)) ENDIF

END my_list_props


SPLIT : THEORY
BEGIN
    IMPORTING my_list_props

    split (m: nat, l : list[nat]) : RECURSIVE [list[nat], list[nat]] =
        CASES l OF
            null        : (null, null),
            cons(h,t)   : LET
                            (l,r) = split (m, t)
                          IN
                            IF h < m
                            THEN (cons(h,l),r)
                            ELSE (l,cons(h,r))
                            ENDIF
        ENDCASES
    MEASURE (length(l))

    split_length: LEMMA % :-)
       FORALL( m:nat, l:list[nat] ): LET s = split(m,l) IN length(l) = length(s`1) + length(s`2)

    split_occ: LEMMA % :-)
       FORALL( n: nat, l:list[nat] ): LET s = split(n, l) IN FORALL(x:nat):occ(x,l) = occ(x,s`1)+occ(x,s`2)

    upb( g:nat, l:list[nat] ): bool =
       FORALL(i:nat): i < length(l) IMPLIES nth(l,i) < g

    lwb( s:nat, l:list[nat] ): bool =
       FORALL(i:nat): i < length(l) IMPLIES NOT nth(l,i) < s

    split_lwb_upb: LEMMA % :-( to be done
       FORALL( m:nat, l:list[nat] ): LET s = split(m,l) IN upb(m,s`1) AND lwb(m,s`2)

END SPLIT

QS : THEORY
BEGIN
	IMPORTING SPLIT
    qs (l : list[nat]) : RECURSIVE list[nat] =
        CASES l OF
            null        : null,
            cons(h,t)   : LET
                            (l,r) = split (h, t)
                          IN
                            append(qs(l),cons(h,qs(r)))
        ENDCASES
    MEASURE (length(l))

END QS

SORTED: THEORY
BEGIN
    IMPORTING my_list_props[nat]
    IMPORTING SPLIT

    sorted?(l:list[nat]) : bool = 
        FORALL (i,j: nat): i < j AND j < length(l) IMPLIES nth(l,i) <= nth(l,j)

    sorted_append: LEMMA % :-( to be done
       FORALL( m:nat, l1,l2:list[nat] ): 
          sorted?(l1) AND sorted?(l2) and upb(m,l1) AND lwb(m,l2)
            IMPLIES sorted?(append(l1,l2))
END SORTED

QS_props : THEORY
BEGIN
    IMPORTING QS, SORTED
    IMPORTING my_list_props[nat], my_list_induction[nat]

    qs_perm: LEMMA % :-( to be done
       FORALL(l:list[nat]):perm?(qs(l),l)

    occ_upb: LEMMA % :-) 
        FORALL( n: nat, l:list[nat] ): upb(n,l) IMPLIES 
            (FORALL(x:nat):occ(x,l) > 0 IMPLIES x < n) 

    occ_lwb: LEMMA % :-)
        FORALL( n: nat, l:list[nat] ): lwb(n,l) IMPLIES 
            (FORALL(x:nat):occ(x,l) > 0 IMPLIES NOT x < n) 

    upb_perm: LEMMA % :-)
    	FORALL(l, lp: list[nat]): perm?(l,lp) IMPLIES
	        FORALL(n:nat): upb(n,l) IMPLIES upb(n,lp)

    lwb_perm: LEMMA % :-)
    	FORALL(l, lp: list[nat]): perm?(l,lp) IMPLIES
   	        FORALL(n:nat): lwb(n,l) IMPLIES lwb(n,lp)

    qs_sorted :LEMMA % :-( to be done
        FORALL (l:list[nat]): sorted?(qs(l))

%    tl : VAR list[nat]

%    test : LEMMA
%        qs ((:4,3,6,2,5:)) = tl


END QS_props