Hi,
I'm not entirely sure I understand what you're trying to define. If
you're just after the matrix that is matrix A with row i and column j
removed then you could define this as follows:
val dsyz_matrix = Define`
dszy_matrix (A:('n,'n) matrix) (i:num) (j:num) : ('n sub1,'n sub1)
matrix =
FCP x y. let xi = if x < i then x else x + 1
and yj = if y < j then y else y + 1
in A ' xi ' yj`;
The "size" of ``:'n sub1`` is one less than the size of ``:'n``.
Although note that ``dimindex(:1 sub1) = 1``, since all type must have
at least one element. One disadvantage of this sort of definition is
that you can't really do arithmetic on types, e.g. ``:'a sub1 + 1`` is
not the same as ``:'a``. This could lead to unexpected type errors.
To get around this you may need to define a casting function, e.g.
something like
val cast_matrix = Define`
cast_matrix pad (A:('a,'b) matrix) : ('m,'n) matrix =
FCP x y. if x < dimindex (:'a) /\ y < dimindex (:'b) then
A ' x ' y
else
pad`;
Note that if ``dimindex (:'a) = dimindex (:'m)`` and ``dimindex (:'b)
= dimindex (:'n)`` then effectively this will be an identity map.
Note that this requirement comes from a fundamental limitation of
HOL's simple, polymorphic type system. Systems with dependent types
(such as Coq and PVS) are better equipped for doing this sort of
reasoning, with the caveat that type checking is more complicated (not
always fully automatic) in these systems.
Anthony
On 26 Nov 2010, at 07:35, anythingroom wrote:
> hi everyone,
>
>
> I want to define a submatrix Mij is formed by throwing away row i
> and column j :
>
> The initial matrix of order n, this splitting gives n smaller matrix
> of order n-1.
>
>
> I define the definition of submatrix as follow:
>
>
> val dsyz_matrix = Define`dszy_matrix (A:('n,'n) matrix) (r:num)
> (c:num) =
>
> (\i j. (FCP x y. if (i < r /\ j < c) then (A %% x %% y) else
>
> if (i < r /\ j > c) then (A %% x %% (y + 1)) else
>
> if(i > r /\ j > c) then (A %% (x + 1) %% (y + 1)) else
>
> (A %% (x + 1) %% y)))`;
>
>
> And the result is like this:
>
> val dsyz_matrix =
> |- !(A :('n, 'n) matrix) (r :num) (c :num).
> (dszy_matrix A r c :num -> num -> ('a, 'b) matrix) =
> (\(i :num) (j :num).
> FCP (x :num) (y :num).
> (if i < r /\ j < c then
> A %% x %% y
> else
> (if i < r /\ j > c then
> A %% x %% (y + (1 :num))
> else
> (if i > r /\ j > c then
> A %% (x + (1 :num)) %% (y + (1 :num))
> else
> A %% (x + (1 :num)) %% y)))) : thm
>
>
> But the submatrix of order is not n – 1.
>
> How can I correct the definition that limit the order n – 1 of
> submatrix? Could anybody give me some hints about it?
>
>
> I appreciate your help.
>
>
> Best wishes,
>
>
> Amy
>
>
>
> 网易163/126邮箱百分百兼容iphone ipad邮件收发
> ------------------------------------------------------------------------------
> Increase Visibility of Your 3D Game App & Earn a Chance To Win $500!
> Tap into the largest installed PC base & get more eyes on your game by
> optimizing for Intel(R) Graphics Technology. Get started today with
> the
> Intel(R) Software Partner Program. Five $500 cash prizes are up for
> grabs.
> http://p.sf.net/sfu/intelisp-dev2dev_______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Increase Visibility of Your 3D Game App & Earn a Chance To Win $500!
Tap into the largest installed PC base & get more eyes on your game by
optimizing for Intel(R) Graphics Technology. Get started today with the
Intel(R) Software Partner Program. Five $500 cash prizes are up for grabs.
http://p.sf.net/sfu/intelisp-dev2dev
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
