Re: [Hol-info] Matrix transposition in HOL

[Lockwood M. <loc...@ec...>]

Changing your definition around just a little to have only one clause
seems to make it quite easy to prove termination - it may be all you
needed to hear was to use "WF_REL_TAC `measure (LENGTH o HD)`. In detail
(which doubtless could be slicked up further -- I used bare HOL, and
very old-fashioned tactics):

app load ["Defn", "TotalDefn", "listTheory"];

open Defn TotalDefn;
open listTheory;

val TRANSPOSE_DEF = Hol_defn "TRANSPOSE"
  `TRANSPOSE (ROWS:'a list list) =
    if NULL ROWS then []
    else if NULL (HD ROWS) then []
         else  (MAP HD ROWS) :: (TRANSPOSE (MAP TL ROWS))`;

 (* tgoal TRANSPOSE_DEF; or, more compactly: *)

val (traspose_def, traspose_induction) = tprove (TRANSPOSE_DEF,
WF_REL_TAC `measure (LENGTH o HD)`
THEN INDUCT_THEN list_INDUCT (fn th => ALL_TAC) THENL
[REWRITE_TAC [NULL_DEF]
,GEN_TAC THEN REWRITE_TAC [NULL_DEF, HD, MAP]
 THEN DISJ_CASES_THEN MP_TAC (ISPEC (Term`h:'a list`) list_CASES) THENL
 [DISCH_TAC THEN ASM_REWRITE_TAC [NULL]
 ,STRIP_TAC THEN ASM_REWRITE_TAC [LENGTH, TL,
prim_recTheory.LESS_SUC_REFL]
]]);

Best wishes,

Lockwood
|- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |-
Lockwood Morris  loc...@ec...  (315)443-3046  Rm. 1-236 CST
Emeritus Professor  Dept. of EECS  Syracuse University  Syracuse NY
On Mon, 26 Sep 2005, Ashish Darbari wrote:

> I'm trying to define a transpose function for a matrix, represented as
> a list of list in HOL. One possibility is the following text book definition
>
> val TRANSPOSE_DEF = Hol_defn "TRANSPOSE" `(TRANSPOSE ([]::n) = [])
>     /\ (TRANSPOSE ROWS = (MAP HD ROWS) :: (TRANSPOSE (MAP TL ROWS)))`;
>
> I tried to define it using "Define" in HOL, and clearly I can't since the
> termination condition is unknown to HOL. So when I use Hol_defn to do
> this I need to come up with a decent termination predicate that I can
> supply to the WF_REL_TAC. What is that predicate going to be?  I tried
> a few things but didn't go very far with all the steps of the
> subsequent proof. Can anyone provide some useful insights?
>
> Thanks
> Ashish
>
>
>
>
> -------------------------------------------------------
> SF.Net email is sponsored by:
> Tame your development challenges with Apache's Geronimo App Server. Download
> it for free - -and be entered to win a 42" plasma tv or your very own
> Sony(tm)PSP.  Click here to play: http://sourceforge.net/geronimo.php
> _______________________________________________
> hol-info mailing list
> hol...@li...
> https://lists.sourceforge.net/lists/listinfo/hol-info
>