Hi J.J. :
First you have to choose how arrays are modelled, i.e., which HOL type
is going to be used to represent arrays. Choices:
- functions of type : num -> ty
- finite functions : num |-> ty
- lists : ty list
- finite products : ty['dim]
Summary of the read (A[i]) and write (A[i] := e) operations on array A:
A : num -> ty
read operation: A i
write operation: \j. if (i=j) then e else A j
Note: there is already a definition for update in combinTheory, using
an infix
(i =+ e) A = \j. if (i=j) then e else A(j)
A : num |-> ty (load finite_mapTheory)
read operation: A ' i
write : A |+ (i,e)
A : ty list
read operation: EL i list
write operation: not sure an indexed write for lists is defined in
HOL. If not, the
following is one version:
update (h::t) 0 e = e::t
update (h::t) n e = h::update t (n-1) e;
A : ty['dim] (load fcpTheory)
read operation: A ' i
write operation: (i :+ e) A
I hope this helps,
Konrad.
On Thu, Apr 11, 2013 at 6:10 AM, J. J. W. <[email protected]> wrote:
> Dear all,
>
> I would like to model the following:
>
> public replace_smaller(int[] A, int c, int d){
> if (A[d] < A[c]){
> A[c] = A[q]
> }
> return A;
> }
>
> and I would like to prove that the resulting array is just like the code.
>
> So I think I should define the following:
>
> val replace_smaller_def = Define `replace_smaller a b (\a. if (nth (a, p)
> < nth (a,q)) then ... else ...`;
>
> However I have no idea how to continue with this since, I have no idea how
> to access the array or anything like that.
>
> Can someone give me some advice?
>
> Kind regards,
>
> Jun Jie
>
>
> ------------------------------------------------------------------------------
> Precog is a next-generation analytics platform capable of advanced
> analytics on semi-structured data. The platform includes APIs for building
> apps and a phenomenal toolset for data science. Developers can use
> our toolset for easy data analysis & visualization. Get a free account!
> http://www2.precog.com/precogplatform/slashdotnewsletter
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
Precog is a next-generation analytics platform capable of advanced
analytics on semi-structured data. The platform includes APIs for building
apps and a phenomenal toolset for data science. Developers can use
our toolset for easy data analysis & visualization. Get a free account!
http://www2.precog.com/precogplatform/slashdotnewsletter
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
