Hi Ayesha, | 0 [`1 <= i`] | 1 [`i <= dimindex (:N)`] | 2 [`~(i' <= dimindex (:N))`] | 3 [`1 <= i'`] | 4 [`i' <= dimindex (:N+P)`] | | `sum (1..dimindex (:M)) (\k. C$i$k * B$k$(i' - dimindex (:N))) = | (lambda j. sum (1..dimindex (:M)) (\k. C$i$k * B$k$j))$(i' - dimindex (:N))`
As you probably know, you would want to use LAMBDA_BETA here to reduce the right-hand side, but it needs you to establish bounds on the argument. Maybe the simplest way is first to do: e(IMP_REWRITE_TAC[LAMBDA_BETA]);; which will reduce your goal purely to the bound. A more low-level variant is: e(CONV_TAC SYM_CONV THEN MATCH_MP_TAC LAMBDA_BETA);; Otherwise you could first establish that same bound (say with ASM_ARITH_TAC), put it in the assumptions, then use simply ASM_SIMP_TAC[LAMBDA_BETA]]. Unfortunately though, I think you will probably want to restate your goal using the special type constructor "finite_sum" rather than the simple disjoint sum "+". The former is a "finite-forcing" variant that works better with using types as indices and gives you the simple rewrite DIMINDEX_FINITE_SUM: # DIMINDEX_FINITE_SUM;; val it : thm = |- dimindex (:(M,N)finite_sum) = dimindex (:M) + dimindex (:N) Otherwise you'll need to add a condition that M and N are finite, which is a bit more messy still. John. ------------------------------------------------------------------------------ Mobile security can be enabling, not merely restricting. Employees who bring their own devices (BYOD) to work are irked by the imposition of MDM restrictions. Mobile Device Manager Plus allows you to control only the apps on BYO-devices by containerizing them, leaving personal data untouched! https://ad.doubleclick.net/ddm/clk/304595813;131938128;j _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
