Sorting.hascasl revision c6b11bbe64a712a10d5d9e58152a7dba35edd056
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder free type Nat ::= 0 | Succ(prec:Nat)
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder pred __<=__ : Nat*Nat
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder forall x,y:Nat
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder . not Succ(x) <= 0
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski . Succ(x)<=Succ(y) <=> x<=y
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian Maeder pred __<=__ : Nat * Nat
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski forall x,y,z : Nat
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski . x <= x %(reflexive)%
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder . x <= z if x <= y /\ y <= z %(transitive)%
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder . x = y if x <= y /\ y <= x %(antisymmetric)%
0095c7efbddd0ffeed6aaf8ec015346be161d819Till Mossakowski . x <= y \/ y <= x %(dichotomous)%
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder . x = y => x <= y
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski free type List[Nat] ::= Nil | Cons(head:Nat; tail:List[Nat])
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder pred elem : Nat * List[Nat]
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder forall x,y:Nat; l:List[Nat]
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder . not elem (x,Nil)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski . elem(x,Cons(y,l)) <=> x=y \/ elem(x,l)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder preds is_ordered : List[Nat];
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski permutation : List[Nat] * List[Nat]
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski vars x,y:Nat; L,L1,L2:List[Nat]
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski . is_ordered(Nil)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski . is_ordered(Cons(x,Nil))
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski . is_ordered(Cons(x,(Cons(y,L)))) <=> x<=y /\ is_ordered(Cons(y,L))
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski . permutation(L1,L2) <=> (forall x:Nat . elem(x,L1) <=> elem(x,L2))
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder op sorter : List[Nat]->List[Nat]
cf31aaf25d0fe96b0578755e7ee18b732e337343Christian Maeder var L:List[Nat]
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder . is_ordered(sorter(L))
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder . permutation(L,sorter(L))
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski ops insert : Nat*List[Nat] -> List[Nat];
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski insert_sort : List[Nat]->List[Nat]
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski vars x,y:Nat; L:List[Nat]
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski . insert(x,Nil) = Cons(x,Nil)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder . insert(x,Cons(y,L)) = Cons(x,insert(y,L)) when x<=y else Cons(y,insert(x,L))
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski . insert_sort(Nil) = Nil
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder . insert_sort(Cons(x,L)) = insert(x,insert_sort(L))