= y) xs`
Thank you very much! I will try my proofs again.
Regards,
Liu
-Original Messages-
From:michael.norr...@data61.csiro.au
Sent Time:2017-12-04 13:35:21 (Monday)
To: 2015200...@mail.buct.edu.cn
Cc: hol-info@lists.sourceforge.net
Subject: Re: [Hol-info] Proof about sorting
.
Michael
From: Liu Gengyang <2015200...@mail.buct.edu.cn>
Date: Monday, 4 December 2017 at 14:38
To: "Norrish, Michael (Data61, Acton)" <michael.norr...@data61.csiro.au>
Cc: hol4_QA <hol-info@lists.sourceforge.net>
Subject: Re: Re: [Hol-info] Proof about sorting
H
ay)
To: 2015200...@mail.buct.edu.cn, hol-info@lists.sourceforge.net
Cc:
Subject: Re: [Hol-info] Proof about sorting
There are proofs that quick-sort and merge-sort are correct in the distribution
already. Perhaps looking at these examples in src/sort will give you some
clues.
Michael
From: Liu Gengyang
You might like to try the following
(1) a predicate sorted, to mean each list member is <= the next one
(2) a lemma that inserting an element into a sorted list gives a sorted list
Jeremy
On 04/12/17 12:58, Liu Gengyang wrote:
Hi,
Recently I am meeting a problem, it has been confusing me a
;hol-info@lists.sourceforge.net>
Subject: [Hol-info] Proof about sorting
Hi,
Recently I am meeting a problem, it has been confusing me a few days, seeking
for help.
I defined a sorting predicate mySort:
val insert_def = Define `
(insert x [] = [x]) /\
(insert x (h::t) = if x <= h
Hi,
Recently I am meeting a problem, it has been confusing me a few days, seeking
for help.
I defined a sorting predicate mySort:
val insert_def = Define `
(insert x [] = [x]) /\
(insert x (h::t) = if x <= h
then (x::h::t)
else (h::(insert x t)))`;
val
