Just to add to Konrad’s e-mail. There is a list “write" operation in listTheory — it is defined as follows:
(∀e n. LUPDATE e n [] = []) ∧ (∀e x l. LUPDATE e 0 (x::l) = e::l) ∧ ∀e n x l. LUPDATE e (SUC n) (x::l) = x::LUPDATE e n l Other representation choices include: - functions of type : ‘a word -> ty - partial functions : ‘a word |-> ty This could make sense if your “int” type is actually a machine word, e.g. ``:word32`` in HOL. Anthony On 11 Apr 2013, at 18:12, Konrad Slind <[email protected]> wrote: > 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 ------------------------------------------------------------------------------ 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
