Hi Michael,
A more generic version of this theorem is already there in HOL Light's
vectors library, which I am copying here.
let VEC_COMPONENT = prove
(`!k i. (vec k :real^N)$i = &k`,
REPEAT GEN_TAC THEN
SUBGOAL_THEN `?k. 1 <= k /\ k <= dimindex(:N) /\ !z:real^N. z$i = z$k`
CHOOSE_TAC THENL
[REWRITE_TAC[FINITE_INDEX_INRANGE];
ASM_SIMP_TAC[vec; CART_EQ; LAMBDA_BETA]]);;
I hope, this would work for you.
On Sat, Jan 13, 2018 at 5:32 AM, Michael Beeson <profbee...@gmail.com>
wrote:
> g `vec 0 $1 = &0`;;
>
>
> # e (REWRITE_TAC[vec]);;
>
> val it : goalstack = 1 subgoal (1 total)
>
>
> `(lambda i. &0)$1 = &0`
>
>
> # e (REWRITE_TAC[lambda]);;
>
> val it : goalstack = 1 subgoal (1 total)
>
>
> `(@f. !i. 1 <= i /\ i <= dimindex (:?224242) ==> f$i = &0)$1 = &0`
>
>
> But
>
>
> e (MESON_TAC[LE_REFL; DIMINDEX_GE_1]);;
>
>
> does not work as hoped, and I can't figure out how to
>
> get rid of @.
>
>
> Also, I'd like to prove vec 0 $2 = &0, but that
>
> would only work for vectors with dimindex at least 2, and
>
> I don't even know how to write that theorem.
>
>
>
>
>
>
> ------------------------------------------------------------
> ------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Adnan Rashid
PhD Candidate
School of Electrical Engineering and Computer Science
NUST, Sector H-12, Islamabad, Pakistan
Voice: +92 51 90852086
Web: save.seecs.nust.edu.pk/adnanrashid/
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
