(`!(s:stable_sy) (s1:stable_sy) (s2:stable_sy) (s3:stable_sy) (l:real^(M,3)finite_product)
(l1:real^(P,3)finite_product) (l2:real^(N,3)finite_product).
s=(\i. ((1+i):num MOD k))
/\
s1=(\i. ((1+i):num MOD p))
/\
s3=(\i. ((1+i):num MOD (k-p+2)))
/\ (
(\x. if x=0 then 0 else (p-2+x) MOD k) s2 s3
/\
s))
/\ (!i j. {i MOD k ,j MOD k}
[REPEAT STRIP_TAC
THEN MRESA1_TAC
DIMINDEX_GE_1`(:M)`
THEN MRESA1_TAC
DIMINDEX_GE_1`(:P)`
THEN MRESA1_TAC
DIMINDEX_GE_1`(:N)`
THEN MP_TAC(ARITH_RULE`1<= k-p /\ 1<=p /\ 1<=k ==> 2< k-p+2 /\ 1<= k-p+2 /\ (k - p + 2) - 1=k - p + 1 /\ ~(k=0)/\ p-1< k/\ p< k /\ ~(p=0)
/\ ~(k-p+2=0)/\ 1< k-p+2/\ p<= k /\ p<=p `)
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL
IK_SY)[`s:stable_sy`;`k:num`]
THEN MRESA_TAC (GEN_ALL
IK_SY)[`s1:stable_sy`;`p:num`]
THEN MRESA_TAC (GEN_ALL
IK_SY)[`s3:stable_sy`;`k-p+2:num`]
THEN MRESA1_TAC (GEN_ALL
K_SY_LE2)`s:stable_sy`
THEN MRESA1_TAC (GEN_ALL
K_SY_LE2)`s1:stable_sy`
THEN MRESA_TAC (GEN_ALL
COVER_NOT_EAR_SY)[`0`;`p-1`;`s:stable_sy`]
THEN MRESA1_TAC
sigma_sy`s:stable_sy`
THEN MRESA_TAC (GEN_ALL
DIAGONAL_SY)[`0:num`;`p-1`;`s:stable_sy`]
THEN DISJ_CASES_TAC(SET_RULE`{0,p-1}
IN J_SY (s1:stable_sy)\/ ~({0,p-1}
IN J_SY (s1:stable_sy))`);
FIND_ASSUM MP_TAC `
COVER_SY 0 (p - 1) s s1 (s2:stable_sy)`
THEN REWRITE_TAC[
COVER_SY;
COVER3_SY;
COVER6_SY]
THEN RESA_TAC;
ASM_REWRITE_TAC[
d_fun]
THEN MRESA1_TAC
sigma_sy`s1:stable_sy`
THEN FIND_ASSUM MP_TAC`
SCHANGE (\x. if x=0 then 0 else (p-2+x) MOD k) s2 (s3:stable_sy)`
THEN REWRITE_TAC[
SCHANGE]
THEN RESA_TAC
THEN SUBGOAL_THEN`{0,1}
IN J_SY (s3:stable_sy)`ASSUME_TAC;
REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC
th[`0`;`1`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM
th;ARITH_RULE`A+0=A/\ ~(1=0)`])
THEN MP_TAC(ARITH_RULE`2<p ==> p-2+1 =p-1`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`p-1:num`;`k:num`];
MRESA_TAC (GEN_ALL
IN_J_IMP_IN_J1_SY)[`p:num`;`s1:stable_sy`]
THEN SUBGOAL_THEN`(k-p+2,1)
IN J1_SY (s3:stable_sy)`ASSUME_TAC;
REWRITE_TAC[
J1_SY;
IN_ELIM_THM]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN ASM_REWRITE_TAC[
IN_NUMSEG]
THEN STRIP_TAC
THEN STRIP_TAC
THEN EXISTS_TAC`k-p+2`
THEN ASM_REWRITE_TAC[]
THEN MRESAL_TAC MOD_MULT[`k-p+2:num`;`1:num`][ARITH_RULE`p*1=p/\1+0=1/\ SUC 0=1 /\ k - p + 2 <= k - p + 2`]
THEN MRESA_TAC
MOD_LT[`1:num`;`k-p+2:num`];
MRESAL_TAC
SUM_DELETE[`(\x. cstab -
norm (
row (
FST x) (vecmats
l1) -
row (
SND x) (vecmats (l1:real^(P,3)finite_product))))`;`
J1_SY (s1:stable_sy)`;`p-1,p`][
FINITE_J1_SY;REAL_ARITH`A=B-C<=> B=A+C`]
THEN MRESAL_TAC
SUM_DELETE[`(\x. cstab -
norm (
row (
FST x) (vecmats l2) -
row (
SND x) (vecmats (l2:real^(N,3)finite_product))))`;`
J1_SY (s3:stable_sy)`;`k-p+2,1`][
FINITE_J1_SY;REAL_ARITH`A=B-C<=> B=A+C`]
THEN SUBGOAL_THEN`
J1_SY s1
DELETE (p-1,p)
DELETE (p,1)
SUBSET J1_SY (s:stable_sy)` ASSUME_TAC;
ASM_REWRITE_TAC[
SUBSET;
J1_SY;
IN_ELIM_THM;
DELETE;
IN_NUMSEG]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[
PAIR_EQ;]
THEN MP_TAC(ARITH_RULE`i<=p ==> i=p \/ i< p:num`)
THEN RESA_TAC;
MRESAL_TAC MOD_MULT[`p:num`;`1:num`][ARITH_RULE`p*1=p /\ SUC 0=1`];
MP_TAC(ARITH_RULE`i<p /\ 2<p ==> i=p-1 \/ i< p-1:num`)
THEN RESA_TAC;
MP_TAC(ARITH_RULE`2<p ==> SUC(p-1)=p /\ p-1<p`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`p-1:num`;`p:num`];
STRIP_TAC
THEN STRIP_TAC
THEN EXISTS_TAC`i:num`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`i<p-1 /\ p < k /\ 2<p ==> i< k /\ i<=k:num /\ 1+i<k/\ 1+i< p/\ ~(i=1+i)/\ ~(i=p-1)/\ ~(p=2)`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`i:num`;`p:num`]
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[
th] THEN REPEAT STRIP_TAC)
THEN MRESA_TAC
MOD_LT[`i:num`;`k:num`]
THEN MRESA_TAC
MOD_LT[`1+i:num`;`k:num`]
THEN MRESA_TAC
MOD_LT[`1+i:num`;`p:num`]
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[SYM
th] )
THEN FIND_ASSUM MP_TAC`
J_SY s1
SUBSET J_SY (s:stable_sy)
UNION {{0, p - 1}}`
THEN REWRITE_TAC[
SUBSET;
UNION;
IN_ELIM_THM;
IN_SING]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC
th`{i,(1+i) MOD p}`)
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
MOD_LT[`1+i:num`;`p:num`]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`{i, 1 + i} = {0, p - 1} /\ ~(i=1+i) /\ ~(i=p-1) ==> i=0 /\ 1+i= p-1`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+0=p-1<=> p=2`];
SUBGOAL_THEN`
IMAGE (\(x,y). (p - 2 + x), (p - 2 + y)) (
J1_SY s3
DELETE (k-p+2,1))
SUBSET J1_SY (s:stable_sy)` ASSUME_TAC;
ASM_REWRITE_TAC[
J1_SY;
IMAGE;
DELETE;
SUBSET;
IN_ELIM_THM;
IN_NUMSEG]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[
PAIR_EQ;]
THEN MP_TAC(ARITH_RULE`i<=k-p+2 ==> i=k-p+2 \/ i< k-p+2:num`)
THEN RESA_TAC;
MRESAL_TAC MOD_MULT[`k-p+2:num`;`1:num`][ARITH_RULE`p*1=p /\ SUC 0=1`];
MP_TAC(ARITH_RULE`i<k-p+2 /\ 2<k-p+2 ==> i=k-p+1 \/ i< k-p+1:num`)
THEN RESA_TAC;
POP_ASSUM (fun th-> SUBST_ALL_TAC(
th))
THEN RESA_TAC
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`2<p /\ 2< k-p+2 /\ 2< k ==> p-2+k-p+1=k-1/\ SUC(k-p+1)=k-p+2 /\ k-p+1<k-p+2/\ p - 2 + k - p + 2=k/\ 1<=k-1 /\ k-1<=k/\ k-1<k/\ 1+k-1=k /\ SUC(k-1)=k/\ 1 + k - p + 1= k - p + 2 /\ ~(k-p+1=0)`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`k-p+1:num`;`k-p+2:num`]
THEN MRESA_TAC
MOD_LT[`k-1:num`;`k:num`]
THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`p*1=p /\ SUC 0=1`]
THEN EXISTS_TAC`k-1`
THEN ASM_REWRITE_TAC[]
THEN FIND_ASSUM MP_TAC`{(k - p + 1) MOD (k - p + 2), (
f_sy s2 o
(\x. if x = 0
then 0
else (p - 2 + x) MOD k))
((k - p + 1) MOD (k - p + 2))}
IN
J_SY (s3:stable_sy)`
THEN FIND_ASSUM(fun th-> REWRITE_TAC[SYM
th])`(\i. (1 + i) MOD (k - p + 2)) =
f_sy (s2:stable_sy) o (\x. if x = 0 then 0 else (p - 2 + x) MOD k)`
THEN ASM_REWRITE_TAC[]
THEN MRESAL_TAC MOD_MULT[`k-p+2:num`;`1:num`][ARITH_RULE`p*1=p /\ SUC 0=1`]
THEN STRIP_TAC
THEN FIND_ASSUM (fun th-> MP_TAC( ISPECL [`k-p+1`;`0`]
th))`!p' q.
{(if p' = 0 then 0 else (p - 2 + p') MOD k), (if q = 0
then 0
else (p - 2 + q) MOD
k)}
IN
J_SY s2 <=>
{p', q}
IN J_SY (s3:stable_sy)`
THEN POP_ASSUM (fun th-> REWRITE_TAC[
th;ARITH_RULE`0=0`])
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN FIND_ASSUM MP_TAC`
J_SY s2
SUBSET J_SY (s:stable_sy)
UNION {{0, p - 1}}`
THEN REWRITE_TAC[
SUBSET;
UNION;
IN_ELIM_THM;
IN_SING]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC
th`{k-1,0}`);
POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`1<=k-p /\2<p==> ~(k-1=p-1) /\ ~(0= p-1)`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`~(k-1=p-1) /\ ~(0= p-1)==> ~(p-1
IN {k-1,0})`)
THEN ASM_REWRITE_TAC[]
THEN SET_TAC[];
STRIP_TAC
THEN STRIP_TAC
THEN EXISTS_TAC`p-2+i:num`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`i<k - p + 1 /\ 2<p /\ 1<=i==> p-2+i< k/\ p-2+i<=k /\ 1<=p-2+i/\ 1+p-2+i<k /\ 1+i< k-p+2/\ p-2+1+i<k`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`p-2+1+i:num`;`k:num`]
THEN MRESA_TAC
MOD_LT[`p-2+i:num`;`k:num`]
THEN MP_TAC(ARITH_RULE`i<k - p + 1 /\ 2<p /\ 1<=i==> ~(i=0)/\ ~(1+i=0)`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`1+i:num`;`k-p+2:num`]
THEN MRESA_TAC
MOD_LT[`i:num`;`k-p+2:num`]
THEN REWRITE_TAC[ARITH_RULE`SUC (p - 2 + i)= p - 2 + SUC i`]
THEN MRESA_TAC
MOD_LT[`1+p-2+i:num`;`k:num`]
THEN FIND_ASSUM (fun th-> MP_TAC( ISPECL [`i MOD (k - p + 2)`;`(
f_sy (s2:stable_sy) o (\x. if x = 0 then 0 else (p - 2 + x) MOD k))
(i MOD (k - p + 2))`]
th))`!p' q.
{(if p' = 0 then 0 else (p - 2 + p') MOD k), (if q = 0
then 0
else (p - 2 + q) MOD
k)}
IN
J_SY s2 <=>
{p', q}
IN J_SY (s3:stable_sy)`
THEN FIND_ASSUM(fun th-> REWRITE_TAC[
th])`{i MOD (k - p + 2), (
f_sy s2 o (\x. if x = 0 then 0 else (p - 2 + x) MOD k))
(i MOD (k - p + 2))}
IN
J_SY (s3:stable_sy)`
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[
th])
THEN FIND_ASSUM(fun th-> REWRITE_TAC[SYM
th])`(\i. (1 + i) MOD (k - p + 2)) =
f_sy (s2:stable_sy) o (\x. if x = 0 then 0 else (p - 2 + x) MOD k)`
THEN POP_ASSUM(fun th-> REWRITE_TAC[
th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[
th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[
th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[
th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[
th])
THEN STRIP_TAC
THEN FIND_ASSUM MP_TAC`
J_SY s2
SUBSET J_SY (s:stable_sy)
UNION {{0, p - 1}}`
THEN REWRITE_TAC[
SUBSET;
UNION;
IN_ELIM_THM;
IN_SING]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC
th`{p-2+i,p-2+1+i}`);
ASM_REWRITE_TAC[ARITH_RULE`1+p-2+i= p-2+1+i`];
MP_TAC(SET_RULE`{p - 2 + i, p - 2 + 1 + i} = {0, p - 1} ==> (p-2+i=0) \/ (p-2+1+i=0)`)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`1<=i /\ 2< p==> ~(p-2+i=0) /\ ~(p-2+1+i=0)`)
THEN ASM_REWRITE_TAC[];
MRESAL_TAC
FINITE_DELETE_IMP[`
J1_SY (s1:stable_sy)`;`p-1,p`][
FINITE_J1_SY]
THEN MRESAL_TAC
FINITE_DELETE_IMP[`
J1_SY (s3:stable_sy)`;`k-p+2,1`][
FINITE_J1_SY]
THEN DISJ_CASES_TAC(SET_RULE`
ear_sy s3 \/ ~(
ear_sy (s3:stable_sy))`);
ASM_REWRITE_TAC[
sigma_sy]
THEN MATCH_MP_TAC(REAL_ARITH`
d_sy s <=
d_sy s1 +
d_sy s3
/\
&0<=
sum (
J1_SY s)
(\x. cstab -
norm (
row (
FST x) (vecmats l) -
row (
SND x) (vecmats l)))
/\
&0<=
sum (
J1_SY s1
DELETE (p - 1,p))
(\x. cstab -
norm (
row (
FST x) (vecmats
l1) -
row (
SND x) (vecmats
l1)))
/\ &0<= cstab -
norm (
row (p - 1) (vecmats
l1) -
row p (vecmats
l1))
/\
&0<=
sum (
J1_SY s3
DELETE (k - p + 2,1))
(\x. cstab -
norm (
row (
FST x) (vecmats l2) -
row (
SND x) (vecmats l2)))
/\ &0<= cstab -
norm (
row (k - p + 2) (vecmats l2) -
row 1 (vecmats l2))
==>
d_sy s +
#0.1 *
-- &1 *
sum (
J1_SY s)
(\x. cstab -
norm (
row (
FST x) (vecmats l) -
row (
SND x) (vecmats l))) <=
(
d_sy s1 +
#0.1 *
&1 *
(
sum (
J1_SY s1
DELETE (p - 1,p))
(\x. cstab -
norm (
row (
FST x) (vecmats
l1) -
row (
SND x) (vecmats
l1))) +
cstab -
norm (
row (p - 1) (vecmats
l1) -
row p (vecmats
l1)))) +
d_sy s3 +
#0.1 *
&1 *
(
sum (
J1_SY (s3:stable_sy)
DELETE (k - p + 2,1))
(\x. cstab -
norm (
row (
FST x) (vecmats l2) -
row (
SND x) (vecmats l2))) +
cstab -
norm (
row (k - p + 2) (vecmats l2) -
row 1 (vecmats l2)))`)
THEN RESA_TAC;
FIND_ASSUM MP_TAC `
COVER2_SY s s1 (s2:stable_sy)`
THEN REWRITE_TAC[
COVER2_SY]
THEN RESA_TAC;
STRIP_TAC;
MATCH_MP_TAC
SUM_POS_LE
THEN REWRITE_TAC[
FINITE_J1_SY]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[
J1_SY;
IN_ELIM_THM;
IN_NUMSEG]
THEN STRIP_TAC
THEN MRESA_TAC (GEN_ALL
B_SY_LE_CSTAB)[`i:num`;`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`;]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
STRIP_TAC;
MATCH_MP_TAC
SUM_POS_LE
THEN ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN DISJ_CASES_TAC(SET_RULE`x=p:num,1 \/ ~(x=p:num,1 )`);
ASM_REWRITE_TAC[]
THEN EXPAND_TAC"l1"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN SUBGOAL_THEN`1<= p/\ p<=
dimindex(:P)==>
row p ((pmat1 (vecmats l)):real^3^P) =
row k (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
ASSUME_TAC(ARITH_RULE`p<=p /\ ~(p<p:num) `)
THEN ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
POP_ASSUM MP_TAC
THEN ASSUME_TAC(ARITH_RULE`p<=p /\ ~(p<p:num) `)
THEN RESA_TAC
THEN SUBGOAL_THEN`
row 1 ((pmat1 (vecmats l)):real^3^P) =
row 1 (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`2<p==> 1<=1 /\ 1<p `)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
ASM_REWRITE_TAC[]
THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`p*1=p`]
THEN MRESAL_TAC (GEN_ALL
B_SY_LE_CSTAB)[`k:num`;`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`;][ARITH_RULE`SUC 0=1`]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
SUBGOAL_THEN`x
IN J1_SY (s1:stable_sy)
DELETE (p - 1,p)
DELETE (p,1)` ASSUME_TAC;
POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[
IN_ELIM_THM;
DELETE]
THEN SET_TAC[];
MP_TAC(SET_RULE`x
IN J1_SY s1
DELETE (p - 1,p)
DELETE (p,1)
/\
J1_SY s1
DELETE (p - 1,p)
DELETE (p,1)
SUBSET J1_SY s
==> x
IN J1_SY (s:stable_sy)`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"THY")
THEN DISCH_THEN(LABEL_TAC"THY1")
THEN REPEAT STRIP_TAC
THEN REMOVE_THEN"THY" MP_TAC
THEN REWRITE_TAC[
J1_SY;
DELETE;
IN_ELIM_THM;
IN_NUMSEG]
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REMOVE_THEN"THY1" MP_TAC
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`i<=p==> i=p \/ i<p:num`)
THEN RESA_TAC;
MRESAL_TAC MOD_MULT[`p:num`;`1:num`][ARITH_RULE`p*1=p/\ SUC 0=1`];
MP_TAC(ARITH_RULE`i< p /\ 2<p ==> i=p -1 \/ SUC i<p:num`)
THEN RESA_TAC;
MP_TAC(ARITH_RULE`2<p ==> p-1< p /\ SUC (p-1)=p`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`p-1:num`;`p:num`];
RESA_TAC
THEN RESA_TAC
THEN EXPAND_TAC"l1"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN MRESA_TAC
MOD_LT[`i:num`;`p:num`]
THEN SUBGOAL_THEN`
row i ((pmat1 (vecmats l)):real^3^P) =
row i (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`
row (SUC i) ((pmat1 (vecmats l)):real^3^P) =
row (SUC i) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`SUC i < p==> 1<= SUC i /\ SUC i <= p`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[
J1_SY;
IN_ELIM_THM;
IN_NUMSEG]
THEN STRIP_TAC
THEN MP_TAC(ARITH_RULE`SUC i < p /\ 1<=k-p ==> i <= k/\ i<k`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`i:num`;`k:num`]
THEN MRESA_TAC (GEN_ALL
B_SY_LE_CSTAB)[`i:num`;`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`;]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
STRIP_TAC;
SUBGOAL_THEN`1<= p/\ p<=
dimindex(:P)==>
row p ((pmat1 (vecmats l)):real^3^P) =
row k (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
ASSUME_TAC(ARITH_RULE`p<=p /\ ~(p<p:num) `)
THEN ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`p <= p`]
THEN EXPAND_TAC"l1"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN RESA_TAC
THEN SUBGOAL_THEN`
row (p-1) ((pmat1 (vecmats l)):real^3^P) =
row (p-1) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`2< p ==> p-1 <= p /\ 1<= p-1/\ p-1<p`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
ASM_REWRITE_TAC[]
THEN FIND_ASSUM (fun th-> MP_TAC(ISPECL [`p-1`;`k:num`]
th) )`!i j.
{i MOD k, j MOD k}
IN J_SY s
UNION {{0, p - 1}}
==>
norm (
row i (vecmats l) -
row j (vecmats (l:real^(M,3)finite_product))) <= cstab`
THEN REWRITE_TAC[
IN_ELIM_THM;
UNION;
IN_SING]
THEN MRESA_TAC
MOD_LT[`p-1:num`;`k:num`]
THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`p*1=p/\ SUC 0=1`;SET_RULE`{p-1,0}={0,p-1}`]
THEN REAL_ARITH_TAC;
STRIP_TAC;
MATCH_MP_TAC
SUM_POS_LE
THEN ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN DISJ_CASES_TAC(SET_RULE`x=k-p+1,k-p+2 \/ ~(x=k-p+1,k-p+2 )`);
ASM_REWRITE_TAC[]
THEN EXPAND_TAC"l2"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN SUBGOAL_THEN`
row (k-p+1) ((pmat2 (vecmats l)):real^3^N) =
row (k-1) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p ==> k-p+1<=k-p+2 /\ 1<= k-p+1 /\ k - (k - p + 2) + k - p + 1= k-1`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`
row (k-p+2) ((pmat2 (vecmats l)):real^3^N) =
row k (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p ==> k-p+2<=k-p+2 /\ 1<= k-p+2 /\ k - (k - p + 2) + k - p + 2= k`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE` 2<k ==> 1<=k-1 /\ k-1<= k /\ SUC (k - 1)= k /\ k-1<k`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`k-1:num`;`k:num`]
THEN MRESAL_TAC (GEN_ALL
B_SY_LE_CSTAB)[`k-1:num`;`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`;][ARITH_RULE`SUC 0=1`]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"THY")
THEN DISCH_THEN(LABEL_TAC"THY1")
THEN REMOVE_THEN"THY" MP_TAC
THEN REWRITE_TAC[
J1_SY;
DELETE;
IN_ELIM_THM;
IN_NUMSEG]
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REMOVE_THEN"THY1" MP_TAC
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`i<=k-p+2==> i=k-p+2 \/ i<k-p+2:num`)
THEN RESA_TAC;
MRESAL_TAC MOD_MULT[`k-p+2:num`;`1:num`][ARITH_RULE`p*1=p/\ SUC 0=1`];
MP_TAC(ARITH_RULE`i< k-p+2 /\ 2<p ==> i=k-p +1 \/ i< k-p+1:num`)
THEN RESA_TAC;
MP_TAC(ARITH_RULE`2<p /\ 1<= k-p ==> k-p+1< k-p+2 /\ SUC (k-p+1)=k-p+2`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`k-p+1:num`;`k-p+2:num`];
RESA_TAC
THEN RESA_TAC
THEN EXPAND_TAC"l2"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN MRESA_TAC
MOD_LT[`i:num`;`k-p+2:num`]
THEN SUBGOAL_THEN`
row i ((pmat2 (vecmats l)):real^3^N) =
row (p-2+i) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p ==> k - (k - p + 2) + i= p-2+i`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`
row (SUC i) ((pmat2 (vecmats l)):real^3^N) =
row (p-2+ SUC i) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p/\ i< k-p+1 ==> k - (k - p + 2) + SUC i= p-2+SUC i/\ 1<= SUC i /\ SUC i<= k-p+2`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE` i< k-p+1 /\ 2< p /\ 1<= k-p ==> 1<=p-2+i /\ p-2+i <= k /\ SUC (p-2+i)= p-2+ SUC i /\ p-2+i<k`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`p-2+i:num`;`k:num`]
THEN MRESAL_TAC (GEN_ALL
B_SY_LE_CSTAB)[`p-2+i:num`;`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`;][ARITH_RULE`SUC 0=1`]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
SUBGOAL_THEN`
row (k-p+2) ((pmat2 (vecmats l)):real^3^N) =
row k (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p ==> k-p+2<=k-p+2 /\ 1<= k-p+2 /\ k - (k - p + 2) + k - p + 2= k`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`
row 1 ((pmat2 (vecmats l)):real^3^N) =
row (p-1) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p ==> k - (k - p + 2) + 1= p-1/\ 1<=1 /\ 1<=k-p+2`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
EXPAND_TAC"l2"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN ASM_REWRITE_TAC[]
THEN FIND_ASSUM (fun th-> MP_TAC(ISPECL [`k:num`;`p-1:num`]
th) )`!i j.
{i MOD k, j MOD k}
IN J_SY s
UNION {{0, p - 1}}
==>
norm (
row i (vecmats l) -
row j (vecmats (l:real^(M,3)finite_product))) <= cstab`
THEN REWRITE_TAC[
IN_ELIM_THM;
UNION;
IN_SING]
THEN MRESA_TAC
MOD_LT[`p-1:num`;`k:num`]
THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`p*1=p/\ SUC 0=1`;SET_RULE`{p-1,0}={0,p-1}`]
THEN REAL_ARITH_TAC;
ASM_REWRITE_TAC[
sigma_sy]
THEN SUBGOAL_THEN `cstab -
norm (
row (p - 1) (vecmats (l1:real^(P,3)finite_product)) -
row p (vecmats
l1)) =cstab -
norm (
row (k-p + 2) (vecmats (l2:real^(N,3)finite_product)) -
row 1 (vecmats l2))` ASSUME_TAC;
REWRITE_TAC[REAL_ARITH`A-B=A-C<=> B=C`]
THEN EXPAND_TAC"l1"
THEN EXPAND_TAC"l2"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN SUBGOAL_THEN`
row 1 ((pmat2 (vecmats l)):real^3^N) =
row (p-1) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p ==> k - (k - p + 2) + 1= p-1/\ 1<=1 /\ 1<=k-p+2`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`
row (k-p+2) ((pmat2 (vecmats l)):real^3^N) =
row k (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p ==> k-p+2<=k-p+2 /\ 1<= k-p+2 /\ k - (k - p + 2) + k - p + 2= k`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`
row (p-1) ((pmat1 (vecmats l)):real^3^P) =
row (p-1) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`2< p ==> p-1 <= p /\ 1<= p-1/\ p-1<p`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`1<= p/\ p<=
dimindex(:P)==>
row p ((pmat1 (vecmats l)):real^3^P) =
row k (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
ASSUME_TAC(ARITH_RULE`p<=p /\ ~(p<p:num) `)
THEN ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`p <= p`]
THEN RESA_TAC
THEN SIMP_TAC[
NORM_SUB];
ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`(!x y.
x
IN J1_SY s3
DELETE (k - p + 2,1) /\
y
IN J1_SY (s3:stable_sy)
DELETE (k - p + 2,1) /\
(\(x,y). p - 2 + x,p - 2 + y) x = (\(x,y). p - 2 + x,p - 2 + y) y
==> x = y)`ASSUME_TAC;
REWRITE_TAC[
J1_SY;
DELETE;
IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[
PAIR_EQ;ARITH_RULE`p-2+B=p-2+C<=> B=C`];
SUBGOAL_THEN`!x. x
IN (
J1_SY (s3:stable_sy)
DELETE (k - p + 2,1))
==>
((\x. cstab -
norm (
row (
FST x) (vecmats (l:real^(M,3)finite_product)) -
row (
SND x) (vecmats l))) o
(\(x,y). p - 2 + x,p - 2 + y)) x
= (\x. cstab -
norm (
row (
FST x) (vecmats (l2:real^(N,3)finite_product)) -
row (
SND x) (vecmats l2))) x`
ASSUME_TAC;
ASM_REWRITE_TAC[
J1_SY;
DELETE;
IN_ELIM_THM;
o_DEF;
IN_NUMSEG]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`A-B=A-C<=> B=C`]
THEN EXPAND_TAC"l2"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`i<=k-p+2==> i=k-p+2 \/ i<k-p+2:num`)
THEN RESA_TAC;
MRESAL_TAC MOD_MULT[`k-p+2:num`;`1:num`][ARITH_RULE`p*1=p/\ SUC 0=1`];
MRESA_TAC
MOD_LT[`i:num`;`k-p+2:num`]
THEN SUBGOAL_THEN`
row i ((pmat2 (vecmats l)):real^3^N) =
row (p-2+i) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p ==> k - (k - p + 2) + i= p-2+i`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`
row (SUC i) ((pmat2 (vecmats l)):real^3^N) =
row (p-2+ SUC i) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p/\ i< k-p+2 ==> k - (k - p + 2) + SUC i= p-2+SUC i/\ 1<= SUC i /\ SUC i<= k-p+2`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
ASM_REWRITE_TAC[];
MRESA_TAC
SUM_EQ[` ((\x. cstab -
norm (
row (
FST x) (vecmats (l:real^(M,3)finite_product)) -
row (
SND x) (vecmats l))) o
(\(x,y). p - 2 + x,p - 2 + y))`;`(\x. cstab -
norm (
row (
FST x) (vecmats (l2:real^(N,3)finite_product)) -
row (
SND x) (vecmats l2)))`;`(
J1_SY (s3:stable_sy)
DELETE (k - p + 2,1))`]
THEN
MRESA_TAC
SUM_IMAGE[`(\(x,y). p - 2 + x,p - 2 + y)`;`(\x. cstab -
norm (
row (
FST x) (vecmats l) -
row (
SND x) (vecmats (l:real^(M,3)finite_product))))`;`
J1_SY (s3:stable_sy)
DELETE (k - p + 2,1)`]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM
th])
THEN MRESAL_TAC
SUM_DIFF[`(\x. cstab -
norm (
row (
FST x) (vecmats (l:real^(M,3)finite_product)) -
row (
SND x) (vecmats l)))`;`
J1_SY(s:stable_sy)`;`(
IMAGE (\(x,y). p - 2 + x,p - 2 + y) (
J1_SY (s3:stable_sy)
DELETE (k - p + 2,1)))`][
FINITE_J1_SY]
THEN MATCH_MP_TAC(REAL_ARITH`
d_sy s <=
d_sy s1+
d_sy s3
/\ &0<=
sum (
J1_SY s1
DELETE (p - 1,p))
(\x. cstab -
norm (
row (
FST x) (vecmats
l1) -
row (
SND x) (vecmats
l1)))
/\ &0<=
sum (
J1_SY s)
(\x. cstab -
norm (
row (
FST x) (vecmats l) -
row (
SND x) (vecmats l)))
-
sum (
IMAGE (\(x,y). p - 2 + x,p - 2 + y) (
J1_SY s3
DELETE (k - p + 2,1)))
(\x. cstab -
norm (
row (
FST x) (vecmats l) -
row (
SND x) (vecmats l)))
==>
d_sy s +
#0.1 *
-- &1 *
sum (
J1_SY (s:stable_sy))
(\x. cstab -
norm (
row (
FST x) (vecmats l) -
row (
SND x) (vecmats l))) <=
(
d_sy s1 +
#0.1 *
&1 *
(
sum (
J1_SY s1
DELETE (p - 1,p))
(\x. cstab -
norm (
row (
FST x) (vecmats (l1:real^(P,3)finite_product)) -
row (
SND x) (vecmats
l1))) +
cstab -
norm (
row (k - p + 2) (vecmats l2) -
row 1 (vecmats l2)))) +
d_sy s3 +
#0.1 *
-- &1 *
(
sum (
IMAGE (\(x,y). p - 2 + x,p - 2 + y) (
J1_SY s3
DELETE (k - p + 2,1)))
(\x. cstab -
norm (
row (
FST x) (vecmats l) -
row (
SND x) (vecmats (l:real^(M,3)finite_product)))) +
cstab -
norm (
row (k - p + 2) (vecmats (l2:real^(N,3)finite_product)) -
row 1 (vecmats l2)))`)
THEN RESA_TAC;
FIND_ASSUM MP_TAC `
COVER2_SY s s1 (s2:stable_sy)`
THEN REWRITE_TAC[
COVER2_SY]
THEN RESA_TAC;
STRIP_TAC;
MATCH_MP_TAC
SUM_POS_LE
THEN ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN DISJ_CASES_TAC(SET_RULE`x=p:num,1 \/ ~(x=p:num,1 )`);
ASM_REWRITE_TAC[]
THEN EXPAND_TAC"l1"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN SUBGOAL_THEN`1<= p/\ p<=
dimindex(:P)==>
row p ((pmat1 (vecmats l)):real^3^P) =
row k (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
ASSUME_TAC(ARITH_RULE`p<=p /\ ~(p<p:num) `)
THEN ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
POP_ASSUM MP_TAC
THEN ASSUME_TAC(ARITH_RULE`p<=p /\ ~(p<p:num) `)
THEN RESA_TAC
THEN SUBGOAL_THEN`
row 1 ((pmat1 (vecmats l)):real^3^P) =
row 1 (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`2<p==> 1<=1 /\ 1<p `)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
ASM_REWRITE_TAC[]
THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`p*1=p`]
THEN MRESAL_TAC (GEN_ALL
B_SY_LE_CSTAB)[`k:num`;`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`;][ARITH_RULE`SUC 0=1`]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
SUBGOAL_THEN`x
IN J1_SY (s1:stable_sy)
DELETE (p - 1,p)
DELETE (p,1)` ASSUME_TAC;
POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[
IN_ELIM_THM;
DELETE]
THEN SET_TAC[];
MP_TAC(SET_RULE`x
IN J1_SY s1
DELETE (p - 1,p)
DELETE (p,1)
/\
J1_SY s1
DELETE (p - 1,p)
DELETE (p,1)
SUBSET J1_SY s
==> x
IN J1_SY (s:stable_sy)`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"THY")
THEN DISCH_THEN(LABEL_TAC"THY1")
THEN REPEAT STRIP_TAC
THEN REMOVE_THEN"THY" MP_TAC
THEN REWRITE_TAC[
J1_SY;
DELETE;
IN_ELIM_THM;
IN_NUMSEG]
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REMOVE_THEN"THY1" MP_TAC
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`i<=p==> i=p \/ i<p:num`)
THEN RESA_TAC;
MRESAL_TAC MOD_MULT[`p:num`;`1:num`][ARITH_RULE`p*1=p/\ SUC 0=1`];
MP_TAC(ARITH_RULE`i< p /\ 2<p ==> i=p -1 \/ SUC i<p:num`)
THEN RESA_TAC;
MP_TAC(ARITH_RULE`2<p ==> p-1< p /\ SUC (p-1)=p`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`p-1:num`;`p:num`];
RESA_TAC
THEN RESA_TAC
THEN EXPAND_TAC"l1"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN MRESA_TAC
MOD_LT[`i:num`;`p:num`]
THEN SUBGOAL_THEN`
row i ((pmat1 (vecmats l)):real^3^P) =
row i (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`
row (SUC i) ((pmat1 (vecmats l)):real^3^P) =
row (SUC i) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`SUC i < p==> 1<= SUC i /\ SUC i <= p`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[
J1_SY;
IN_ELIM_THM;
IN_NUMSEG]
THEN STRIP_TAC
THEN MP_TAC(ARITH_RULE`SUC i < p /\ 1<=k-p ==> i <= k/\ i<k`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`i:num`;`k:num`]
THEN MRESA_TAC (GEN_ALL
B_SY_LE_CSTAB)[`i:num`;`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`;]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
POP_ASSUM(fun th-> REWRITE_TAC[SYM
th])
THEN MATCH_MP_TAC
SUM_POS_LE
THEN STRIP_TAC;
MATCH_MP_TAC
FINITE_DIFF
THEN REWRITE_TAC[
FINITE_J1_SY];
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[
J1_SY;
IN_ELIM_THM;
IN_NUMSEG;
DIFF]
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN MRESA_TAC (GEN_ALL
B_SY_LE_CSTAB)[`i:num`;`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`;]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
ASM_REWRITE_TAC[
d_fun]
THEN MRESA1_TAC
sigma_sy`s3:stable_sy`
THEN FIND_ASSUM MP_TAC`
SCHANGE (\x. if x=0 then 0 else (p-2+x) MOD k) s2 (s3:stable_sy)`
THEN REWRITE_TAC[
SCHANGE]
THEN RESA_TAC
THEN SUBGOAL_THEN`{0,1}
IN J_SY (s3:stable_sy)`ASSUME_TAC;
REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC
th[`0`;`1`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM
th;ARITH_RULE`A+0=A/\ ~(1=0)`])
THEN MP_TAC(ARITH_RULE`2<p ==> p-2+1 =p-1`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`p-1:num`;`k:num`];
MRESA_TAC (GEN_ALL
IN_J_IMP_IN_J1_SY)[`p:num`;`s1:stable_sy`]
THEN SUBGOAL_THEN`(k-p+2,1)
IN J1_SY (s3:stable_sy)`ASSUME_TAC;
REWRITE_TAC[
J1_SY;
IN_ELIM_THM]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN ASM_REWRITE_TAC[
IN_NUMSEG]
THEN STRIP_TAC
THEN STRIP_TAC
THEN EXISTS_TAC`k-p+2`
THEN ASM_REWRITE_TAC[]
THEN MRESAL_TAC MOD_MULT[`k-p+2:num`;`1:num`][ARITH_RULE`p*1=p/\1+0=1/\ SUC 0=1 /\ k - p + 2 <= k - p + 2`]
THEN MRESA_TAC
MOD_LT[`1:num`;`k-p+2:num`];
MRESAL_TAC
SUM_DELETE[`(\x. cstab -
norm (
row (
FST x) (vecmats
l1) -
row (
SND x) (vecmats (l1:real^(P,3)finite_product))))`;`
J1_SY (s1:stable_sy)`;`p-1,p`][
FINITE_J1_SY;REAL_ARITH`A=B-C<=> B=A+C`]
THEN MRESAL_TAC
SUM_DELETE[`(\x. cstab -
norm (
row (
FST x) (vecmats l2) -
row (
SND x) (vecmats (l2:real^(N,3)finite_product))))`;`
J1_SY (s3:stable_sy)`;`k-p+2,1`][
FINITE_J1_SY;REAL_ARITH`A=B-C<=> B=A+C`]
THEN SUBGOAL_THEN`
J1_SY s1
DELETE (p-1,p)
DELETE (p,1)
SUBSET J1_SY (s:stable_sy)` ASSUME_TAC;
ASM_REWRITE_TAC[
SUBSET;
J1_SY;
IN_ELIM_THM;
DELETE;
IN_NUMSEG]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[
PAIR_EQ;]
THEN MP_TAC(ARITH_RULE`i<=p ==> i=p \/ i< p:num`)
THEN RESA_TAC;
MRESAL_TAC MOD_MULT[`p:num`;`1:num`][ARITH_RULE`p*1=p /\ SUC 0=1`];
MP_TAC(ARITH_RULE`i<p /\ 2<p ==> i=p-1 \/ i< p-1:num`)
THEN RESA_TAC;
MP_TAC(ARITH_RULE`2<p ==> SUC(p-1)=p /\ p-1<p`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`p-1:num`;`p:num`];
STRIP_TAC
THEN STRIP_TAC
THEN EXISTS_TAC`i:num`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`i<p-1 /\ p < k /\ 2<p ==> i< k /\ i<=k:num /\ 1+i<k/\ 1+i< p/\ ~(i=1+i)/\ ~(i=p-1)/\ ~(p=2)`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`i:num`;`p:num`]
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[
th] THEN REPEAT STRIP_TAC)
THEN MRESA_TAC
MOD_LT[`i:num`;`k:num`]
THEN MRESA_TAC
MOD_LT[`1+i:num`;`k:num`]
THEN MRESA_TAC
MOD_LT[`1+i:num`;`p:num`]
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[SYM
th] )
THEN FIND_ASSUM MP_TAC`
J_SY s1
SUBSET J_SY (s:stable_sy)
UNION {{0, p - 1}}`
THEN REWRITE_TAC[
SUBSET;
UNION;
IN_ELIM_THM;
IN_SING]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC
th`{i,(1+i) MOD p}`)
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
MOD_LT[`1+i:num`;`p:num`]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`{i, 1 + i} = {0, p - 1} /\ ~(i=1+i) /\ ~(i=p-1) ==> i=0 /\ 1+i= p-1`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+0=p-1<=> p=2`];
SUBGOAL_THEN`
IMAGE (\(x,y). (p - 2 + x), (p - 2 + y)) (
J1_SY s3
DELETE (k-p+2,1))
SUBSET J1_SY (s:stable_sy)` ASSUME_TAC;
ASM_REWRITE_TAC[
J1_SY;
IMAGE;
DELETE;
SUBSET;
IN_ELIM_THM;
IN_NUMSEG]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[
PAIR_EQ;]
THEN MP_TAC(ARITH_RULE`i<=k-p+2 ==> i=k-p+2 \/ i< k-p+2:num`)
THEN RESA_TAC;
MRESAL_TAC MOD_MULT[`k-p+2:num`;`1:num`][ARITH_RULE`p*1=p /\ SUC 0=1`];
MP_TAC(ARITH_RULE`i<k-p+2 /\ 2<k-p+2 ==> i=k-p+1 \/ i< k-p+1:num`)
THEN RESA_TAC;
POP_ASSUM (fun th-> SUBST_ALL_TAC(
th))
THEN RESA_TAC
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`2<p /\ 2< k-p+2 /\ 2< k ==> p-2+k-p+1=k-1/\ SUC(k-p+1)=k-p+2 /\ k-p+1<k-p+2/\ p - 2 + k - p + 2=k/\ 1<=k-1 /\ k-1<=k/\ k-1<k/\ 1+k-1=k /\ SUC(k-1)=k/\ 1 + k - p + 1= k - p + 2 /\ ~(k-p+1=0)`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`k-p+1:num`;`k-p+2:num`]
THEN MRESA_TAC
MOD_LT[`k-1:num`;`k:num`]
THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`p*1=p /\ SUC 0=1`]
THEN EXISTS_TAC`k-1`
THEN ASM_REWRITE_TAC[]
THEN FIND_ASSUM MP_TAC`{(k - p + 1) MOD (k - p + 2), (
f_sy s2 o
(\x. if x = 0
then 0
else (p - 2 + x) MOD k))
((k - p + 1) MOD (k - p + 2))}
IN
J_SY (s3:stable_sy)`
THEN FIND_ASSUM(fun th-> REWRITE_TAC[SYM
th])`(\i. (1 + i) MOD (k - p + 2)) =
f_sy (s2:stable_sy) o (\x. if x = 0 then 0 else (p - 2 + x) MOD k)`
THEN ASM_REWRITE_TAC[]
THEN MRESAL_TAC MOD_MULT[`k-p+2:num`;`1:num`][ARITH_RULE`p*1=p /\ SUC 0=1`]
THEN STRIP_TAC
THEN FIND_ASSUM (fun th-> MP_TAC( ISPECL [`k-p+1`;`0`]
th))`!p' q.
{(if p' = 0 then 0 else (p - 2 + p') MOD k), (if q = 0
then 0
else (p - 2 + q) MOD
k)}
IN
J_SY s2 <=>
{p', q}
IN J_SY (s3:stable_sy)`
THEN POP_ASSUM (fun th-> REWRITE_TAC[
th;ARITH_RULE`0=0`])
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN FIND_ASSUM MP_TAC`
J_SY s2
SUBSET J_SY (s:stable_sy)
UNION {{0, p - 1}}`
THEN REWRITE_TAC[
SUBSET;
UNION;
IN_ELIM_THM;
IN_SING]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC
th`{k-1,0}`);
POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`1<=k-p /\2<p==> ~(k-1=p-1) /\ ~(0= p-1)`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`~(k-1=p-1) /\ ~(0= p-1)==> ~(p-1
IN {k-1,0})`)
THEN ASM_REWRITE_TAC[]
THEN SET_TAC[];
STRIP_TAC
THEN STRIP_TAC
THEN EXISTS_TAC`p-2+i:num`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`i<k - p + 1 /\ 2<p /\ 1<=i==> p-2+i< k/\ p-2+i<=k /\ 1<=p-2+i/\ 1+p-2+i<k /\ 1+i< k-p+2/\ p-2+1+i<k`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`p-2+1+i:num`;`k:num`]
THEN MRESA_TAC
MOD_LT[`p-2+i:num`;`k:num`]
THEN MP_TAC(ARITH_RULE`i<k - p + 1 /\ 2<p /\ 1<=i==> ~(i=0)/\ ~(1+i=0)`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`1+i:num`;`k-p+2:num`]
THEN MRESA_TAC
MOD_LT[`i:num`;`k-p+2:num`]
THEN REWRITE_TAC[ARITH_RULE`SUC (p - 2 + i)= p - 2 + SUC i`]
THEN MRESA_TAC
MOD_LT[`1+p-2+i:num`;`k:num`]
THEN FIND_ASSUM (fun th-> MP_TAC( ISPECL [`i MOD (k - p + 2)`;`(
f_sy (s2:stable_sy) o (\x. if x = 0 then 0 else (p - 2 + x) MOD k))
(i MOD (k - p + 2))`]
th))`!p' q.
{(if p' = 0 then 0 else (p - 2 + p') MOD k), (if q = 0
then 0
else (p - 2 + q) MOD
k)}
IN
J_SY s2 <=>
{p', q}
IN J_SY (s3:stable_sy)`
THEN FIND_ASSUM(fun th-> REWRITE_TAC[
th])`{i MOD (k - p + 2), (
f_sy s2 o (\x. if x = 0 then 0 else (p - 2 + x) MOD k))
(i MOD (k - p + 2))}
IN
J_SY (s3:stable_sy)`
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[
th])
THEN FIND_ASSUM(fun th-> REWRITE_TAC[SYM
th])`(\i. (1 + i) MOD (k - p + 2)) =
f_sy (s2:stable_sy) o (\x. if x = 0 then 0 else (p - 2 + x) MOD k)`
THEN POP_ASSUM(fun th-> REWRITE_TAC[
th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[
th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[
th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[
th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[
th])
THEN STRIP_TAC
THEN FIND_ASSUM MP_TAC`
J_SY s2
SUBSET J_SY (s:stable_sy)
UNION {{0, p - 1}}`
THEN REWRITE_TAC[
SUBSET;
UNION;
IN_ELIM_THM;
IN_SING]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC
th`{p-2+i,p-2+1+i}`);
ASM_REWRITE_TAC[ARITH_RULE`1+p-2+i= p-2+1+i`];
MP_TAC(SET_RULE`{p - 2 + i, p - 2 + 1 + i} = {0, p - 1} ==> (p-2+i=0) \/ (p-2+1+i=0)`)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`1<=i /\ 2< p==> ~(p-2+i=0) /\ ~(p-2+1+i=0)`)
THEN ASM_REWRITE_TAC[];
MRESAL_TAC
FINITE_DELETE_IMP[`
J1_SY (s1:stable_sy)`;`p-1,p`][
FINITE_J1_SY]
THEN MRESAL_TAC
FINITE_DELETE_IMP[`
J1_SY (s3:stable_sy)`;`k-p+2,1`][
FINITE_J1_SY]
THEN DISJ_CASES_TAC(SET_RULE`
ear_sy s1 \/ ~(
ear_sy (s1:stable_sy))`);
ASM_REWRITE_TAC[
sigma_sy]
THEN MATCH_MP_TAC(REAL_ARITH`
d_sy s <=
d_sy s1 +
d_sy s3
/\
&0<=
sum (
J1_SY s)
(\x. cstab -
norm (
row (
FST x) (vecmats l) -
row (
SND x) (vecmats l)))
/\
&0<=
sum (
J1_SY s1
DELETE (p - 1,p))
(\x. cstab -
norm (
row (
FST x) (vecmats
l1) -
row (
SND x) (vecmats
l1)))
/\ &0<= cstab -
norm (
row (p - 1) (vecmats
l1) -
row p (vecmats
l1))
/\
&0<=
sum (
J1_SY s3
DELETE (k - p + 2,1))
(\x. cstab -
norm (
row (
FST x) (vecmats l2) -
row (
SND x) (vecmats l2)))
/\ &0<= cstab -
norm (
row (k - p + 2) (vecmats l2) -
row 1 (vecmats l2))
==>
d_sy s +
#0.1 *
-- &1 *
sum (
J1_SY s)
(\x. cstab -
norm (
row (
FST x) (vecmats l) -
row (
SND x) (vecmats l))) <=
(
d_sy s1 +
#0.1 *
&1 *
(
sum (
J1_SY s1
DELETE (p - 1,p))
(\x. cstab -
norm (
row (
FST x) (vecmats
l1) -
row (
SND x) (vecmats
l1))) +
cstab -
norm (
row (p - 1) (vecmats
l1) -
row p (vecmats
l1)))) +
d_sy s3 +
#0.1 *
&1 *
(
sum (
J1_SY (s3:stable_sy)
DELETE (k - p + 2,1))
(\x. cstab -
norm (
row (
FST x) (vecmats l2) -
row (
SND x) (vecmats l2))) +
cstab -
norm (
row (k - p + 2) (vecmats l2) -
row 1 (vecmats l2)))`)
THEN RESA_TAC;
FIND_ASSUM MP_TAC `
COVER2_SY s s1 (s2:stable_sy)`
THEN REWRITE_TAC[
COVER2_SY]
THEN RESA_TAC;
STRIP_TAC;
MATCH_MP_TAC
SUM_POS_LE
THEN REWRITE_TAC[
FINITE_J1_SY]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[
J1_SY;
IN_ELIM_THM;
IN_NUMSEG]
THEN STRIP_TAC
THEN MRESA_TAC (GEN_ALL
B_SY_LE_CSTAB)[`i:num`;`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`;]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
STRIP_TAC;
MATCH_MP_TAC
SUM_POS_LE
THEN ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN DISJ_CASES_TAC(SET_RULE`x=p:num,1 \/ ~(x=p:num,1 )`);
ASM_REWRITE_TAC[]
THEN EXPAND_TAC"l1"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN SUBGOAL_THEN`1<= p/\ p<=
dimindex(:P)==>
row p ((pmat1 (vecmats l)):real^3^P) =
row k (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
ASSUME_TAC(ARITH_RULE`p<=p /\ ~(p<p:num) `)
THEN ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
POP_ASSUM MP_TAC
THEN ASSUME_TAC(ARITH_RULE`p<=p /\ ~(p<p:num) `)
THEN RESA_TAC
THEN SUBGOAL_THEN`
row 1 ((pmat1 (vecmats l)):real^3^P) =
row 1 (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`2<p==> 1<=1 /\ 1<p `)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
ASM_REWRITE_TAC[]
THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`p*1=p`]
THEN MRESAL_TAC (GEN_ALL
B_SY_LE_CSTAB)[`k:num`;`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`;][ARITH_RULE`SUC 0=1`]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
SUBGOAL_THEN`x
IN J1_SY (s1:stable_sy)
DELETE (p - 1,p)
DELETE (p,1)` ASSUME_TAC;
POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[
IN_ELIM_THM;
DELETE]
THEN SET_TAC[];
MP_TAC(SET_RULE`x
IN J1_SY s1
DELETE (p - 1,p)
DELETE (p,1)
/\
J1_SY s1
DELETE (p - 1,p)
DELETE (p,1)
SUBSET J1_SY s
==> x
IN J1_SY (s:stable_sy)`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"THY")
THEN DISCH_THEN(LABEL_TAC"THY1")
THEN REPEAT STRIP_TAC
THEN REMOVE_THEN"THY" MP_TAC
THEN REWRITE_TAC[
J1_SY;
DELETE;
IN_ELIM_THM;
IN_NUMSEG]
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REMOVE_THEN"THY1" MP_TAC
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`i<=p==> i=p \/ i<p:num`)
THEN RESA_TAC;
MRESAL_TAC MOD_MULT[`p:num`;`1:num`][ARITH_RULE`p*1=p/\ SUC 0=1`];
MP_TAC(ARITH_RULE`i< p /\ 2<p ==> i=p -1 \/ SUC i<p:num`)
THEN RESA_TAC;
MP_TAC(ARITH_RULE`2<p ==> p-1< p /\ SUC (p-1)=p`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`p-1:num`;`p:num`];
RESA_TAC
THEN RESA_TAC
THEN EXPAND_TAC"l1"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN MRESA_TAC
MOD_LT[`i:num`;`p:num`]
THEN SUBGOAL_THEN`
row i ((pmat1 (vecmats l)):real^3^P) =
row i (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`
row (SUC i) ((pmat1 (vecmats l)):real^3^P) =
row (SUC i) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`SUC i < p==> 1<= SUC i /\ SUC i <= p`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[
J1_SY;
IN_ELIM_THM;
IN_NUMSEG]
THEN STRIP_TAC
THEN MP_TAC(ARITH_RULE`SUC i < p /\ 1<=k-p ==> i <= k/\ i<k`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`i:num`;`k:num`]
THEN MRESA_TAC (GEN_ALL
B_SY_LE_CSTAB)[`i:num`;`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`;]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
STRIP_TAC;
SUBGOAL_THEN`1<= p/\ p<=
dimindex(:P)==>
row p ((pmat1 (vecmats l)):real^3^P) =
row k (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
ASSUME_TAC(ARITH_RULE`p<=p /\ ~(p<p:num) `)
THEN ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`p <= p`]
THEN EXPAND_TAC"l1"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN RESA_TAC
THEN SUBGOAL_THEN`
row (p-1) ((pmat1 (vecmats l)):real^3^P) =
row (p-1) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`2< p ==> p-1 <= p /\ 1<= p-1/\ p-1<p`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
ASM_REWRITE_TAC[]
THEN FIND_ASSUM (fun th-> MP_TAC(ISPECL [`p-1`;`k:num`]
th) )`!i j.
{i MOD k, j MOD k}
IN J_SY s
UNION {{0, p - 1}}
==>
norm (
row i (vecmats l) -
row j (vecmats (l:real^(M,3)finite_product))) <= cstab`
THEN REWRITE_TAC[
IN_ELIM_THM;
UNION;
IN_SING]
THEN MRESA_TAC
MOD_LT[`p-1:num`;`k:num`]
THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`p*1=p/\ SUC 0=1`;SET_RULE`{p-1,0}={0,p-1}`]
THEN REAL_ARITH_TAC;
STRIP_TAC;
MATCH_MP_TAC
SUM_POS_LE
THEN ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN DISJ_CASES_TAC(SET_RULE`x=k-p+1,k-p+2 \/ ~(x=k-p+1,k-p+2 )`);
ASM_REWRITE_TAC[]
THEN EXPAND_TAC"l2"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN SUBGOAL_THEN`
row (k-p+1) ((pmat2 (vecmats l)):real^3^N) =
row (k-1) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p ==> k-p+1<=k-p+2 /\ 1<= k-p+1 /\ k - (k - p + 2) + k - p + 1= k-1`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`
row (k-p+2) ((pmat2 (vecmats l)):real^3^N) =
row k (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p ==> k-p+2<=k-p+2 /\ 1<= k-p+2 /\ k - (k - p + 2) + k - p + 2= k`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE` 2<k ==> 1<=k-1 /\ k-1<= k /\ SUC (k - 1)= k /\ k-1<k`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`k-1:num`;`k:num`]
THEN MRESAL_TAC (GEN_ALL
B_SY_LE_CSTAB)[`k-1:num`;`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`;][ARITH_RULE`SUC 0=1`]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"THY")
THEN DISCH_THEN(LABEL_TAC"THY1")
THEN REMOVE_THEN"THY" MP_TAC
THEN REWRITE_TAC[
J1_SY;
DELETE;
IN_ELIM_THM;
IN_NUMSEG]
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REMOVE_THEN"THY1" MP_TAC
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`i<=k-p+2==> i=k-p+2 \/ i<k-p+2:num`)
THEN RESA_TAC;
MRESAL_TAC MOD_MULT[`k-p+2:num`;`1:num`][ARITH_RULE`p*1=p/\ SUC 0=1`];
MP_TAC(ARITH_RULE`i< k-p+2 /\ 2<p ==> i=k-p +1 \/ i< k-p+1:num`)
THEN RESA_TAC;
MP_TAC(ARITH_RULE`2<p /\ 1<= k-p ==> k-p+1< k-p+2 /\ SUC (k-p+1)=k-p+2`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`k-p+1:num`;`k-p+2:num`];
RESA_TAC
THEN RESA_TAC
THEN EXPAND_TAC"l2"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN MRESA_TAC
MOD_LT[`i:num`;`k-p+2:num`]
THEN SUBGOAL_THEN`
row i ((pmat2 (vecmats l)):real^3^N) =
row (p-2+i) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p ==> k - (k - p + 2) + i= p-2+i`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`
row (SUC i) ((pmat2 (vecmats l)):real^3^N) =
row (p-2+ SUC i) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p/\ i< k-p+1 ==> k - (k - p + 2) + SUC i= p-2+SUC i/\ 1<= SUC i /\ SUC i<= k-p+2`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE` i< k-p+1 /\ 2< p /\ 1<= k-p ==> 1<=p-2+i /\ p-2+i <= k /\ SUC (p-2+i)= p-2+ SUC i /\ p-2+i<k`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`p-2+i:num`;`k:num`]
THEN MRESAL_TAC (GEN_ALL
B_SY_LE_CSTAB)[`p-2+i:num`;`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`;][ARITH_RULE`SUC 0=1`]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
SUBGOAL_THEN`
row (k-p+2) ((pmat2 (vecmats l)):real^3^N) =
row k (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p ==> k-p+2<=k-p+2 /\ 1<= k-p+2 /\ k - (k - p + 2) + k - p + 2= k`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`
row 1 ((pmat2 (vecmats l)):real^3^N) =
row (p-1) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p ==> k - (k - p + 2) + 1= p-1/\ 1<=1 /\ 1<=k-p+2`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
EXPAND_TAC"l2"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN ASM_REWRITE_TAC[]
THEN FIND_ASSUM (fun th-> MP_TAC(ISPECL [`k:num`;`p-1:num`]
th) )`!i j.
{i MOD k, j MOD k}
IN J_SY s
UNION {{0, p - 1}}
==>
norm (
row i (vecmats l) -
row j (vecmats (l:real^(M,3)finite_product))) <= cstab`
THEN REWRITE_TAC[
IN_ELIM_THM;
UNION;
IN_SING]
THEN MRESA_TAC
MOD_LT[`p-1:num`;`k:num`]
THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`p*1=p/\ SUC 0=1`;SET_RULE`{p-1,0}={0,p-1}`]
THEN REAL_ARITH_TAC;
ASM_REWRITE_TAC[
sigma_sy]
THEN SUBGOAL_THEN `cstab -
norm (
row (p - 1) (vecmats (l1:real^(P,3)finite_product)) -
row p (vecmats
l1)) =cstab -
norm (
row (k-p + 2) (vecmats (l2:real^(N,3)finite_product)) -
row 1 (vecmats l2))` ASSUME_TAC;
REWRITE_TAC[REAL_ARITH`A-B=A-C<=> B=C`]
THEN EXPAND_TAC"l1"
THEN EXPAND_TAC"l2"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN SUBGOAL_THEN`
row 1 ((pmat2 (vecmats l)):real^3^N) =
row (p-1) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p ==> k - (k - p + 2) + 1= p-1/\ 1<=1 /\ 1<=k-p+2`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`
row (k-p+2) ((pmat2 (vecmats l)):real^3^N) =
row k (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p ==> k-p+2<=k-p+2 /\ 1<= k-p+2 /\ k - (k - p + 2) + k - p + 2= k`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`
row (p-1) ((pmat1 (vecmats l)):real^3^P) =
row (p-1) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`2< p ==> p-1 <= p /\ 1<= p-1/\ p-1<p`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`1<= p/\ p<=
dimindex(:P)==>
row p ((pmat1 (vecmats l)):real^3^P) =
row k (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
ASSUME_TAC(ARITH_RULE`p<=p /\ ~(p<p:num) `)
THEN ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`p <= p`]
THEN RESA_TAC
THEN SIMP_TAC[
NORM_SUB];
DISJ_CASES_TAC(SET_RULE`(p,1)
IN J1_SY s1
DELETE (p - 1,p) \/ ~((p,1)
IN J1_SY (s1:stable_sy)
DELETE (p - 1,p))`);
SUBGOAL_THEN`k,1
IN J1_SY (s:stable_sy)`ASSUME_TAC;
POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[
J1_SY;
IN_ELIM_THM;
DELETE;
PAIR_EQ;
IN_NUMSEG]
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM
th))
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC MOD_MULT[`p:num`;`1:num`][ARITH_RULE`p*1=p /\ 1+0=1`]
THEN MP_TAC(ARITH_RULE`2<p /\ 2< k==> 1<p /\ 1<k /\ k<=k`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`1:num`;`p:num`]
THEN STRIP_TAC
THEN EXISTS_TAC`k:num`
THEN ASM_REWRITE_TAC[]
THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`p*1=p /\ SUC 0=1/\ 1+0=1`]
THEN MRESA_TAC
MOD_LT[`1:num`;`k:num`]
THEN FIND_ASSUM MP_TAC`
J_SY s1
SUBSET J_SY (s:stable_sy)
UNION {{0, p - 1}}`
THEN REWRITE_TAC[
SUBSET;
UNION;
IN_ELIM_THM;
IN_SING]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC
th`{0,1}`);
MP_TAC(ARITH_RULE`2<p ==> ~(p-1=0) /\ ~(p-1=1)`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`~(p-1=0) /\ ~(p-1=1) ==> ~(p-1
IN {0,1})`)
THEN ASM_REWRITE_TAC[]
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN SET_TAC[];
MRESAL_TAC
SUM_DELETE[`(\x. cstab -
norm (
row (
FST x) (vecmats
l1) -
row (
SND x) (vecmats (l1:real^(P,3)finite_product))))`;`
J1_SY (s1:stable_sy)
DELETE (p-1,p)`;`p:num,1`][
FINITE_J1_SY;REAL_ARITH`A=B-C<=> B=A+C`]
THEN MRESAL_TAC
SUM_DELETE[`(\x. cstab -
norm (
row (
FST x) (vecmats l) -
row (
SND x) (vecmats (l:real^(M,3)finite_product))))`;`
J1_SY (s:stable_sy)`;`k:num,1`][
FINITE_J1_SY;REAL_ARITH`A=B-C<=> B=A+C`]
THEN EXPAND_TAC"l1"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN SUBGOAL_THEN`1<= p/\ p<=
dimindex(:P)==>
row p ((pmat1 (vecmats l)):real^3^P) =
row k (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
ASSUME_TAC(ARITH_RULE`p<=p /\ ~(p<p:num) `)
THEN ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
POP_ASSUM MP_TAC
THEN ASSUME_TAC(ARITH_RULE`p<=p /\ ~(p<p:num) `)
THEN RESA_TAC
THEN SUBGOAL_THEN`
row 1 ((pmat1 (vecmats l)):real^3^P) =
row 1 (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`2<p==> 1<=1 /\ 1<p `)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`
J1_SY s1
DELETE (p - 1,p)
DELETE (p,1)
SUBSET J1_SY (s:stable_sy)
DELETE (k,1)`ASSUME_TAC;
MATCH_MP_TAC(SET_RULE`~(x
IN A) /\ A
SUBSET B==> A
SUBSET B
DELETE x`)
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC(SET_RULE`~(x
IN A) ==> ~(x
IN A
DELETE y)`)
THEN MATCH_MP_TAC(SET_RULE`~(x
IN A) ==> ~(x
IN A
DELETE y)`)
THEN ASM_REWRITE_TAC[
J1_SY;
IN_ELIM_THM;
PAIR_EQ;
IN_NUMSEG]
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM
th))
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`1<= k-p ==> ~(k<=p)`)
THEN RESA_TAC;
ASM_REWRITE_TAC[REAL_ARITH`(A+ #0.1 * -- &1 *(C+B)) + D+ #0.1 * &1* (E+B)= (A+ #0.1 * -- &1 * C) + D+ #0.1 * &1 * E`]
THEN MRESAL_TAC
FINITE_DELETE_IMP[`
J1_SY (s:stable_sy)`;`k:num,1`][
FINITE_J1_SY]
THEN MRESAL_TAC
SUM_DIFF[`(\x. cstab -
norm (
row (
FST x) (vecmats (l:real^(M,3)finite_product)) -
row (
SND x) (vecmats l)))`;`
J1_SY(s:stable_sy)
DELETE (k,1)`;`
J1_SY (s1:stable_sy)
DELETE (p-1,p:num)
DELETE (p:num,1)`][
FINITE_J1_SY;]
THEN MATCH_MP_TAC(REAL_ARITH`
A1<= A+D /\ &0<= C1 -C /\ &0<= E
==> A1+ #0.1 * -- &1 * (C1+B) <=(A+ #0.1 * -- &1 *(C+B)) + D+ #0.1 * &1* E`)
THEN STRIP_TAC;
FIND_ASSUM MP_TAC `
COVER2_SY s s1 (s2:stable_sy)`
THEN REWRITE_TAC[
COVER2_SY]
THEN RESA_TAC;
STRIP_TAC;
SUBGOAL_THEN`!x. x
IN (
J1_SY (s1:stable_sy)
DELETE (p - 1,p)
DELETE (p,1))
==> (\x. cstab -
norm
(
row (
FST x) ((pmat1 (vecmats (l:real^(M,3)finite_product)):real^3^P)) -
row (
SND x) ((pmat1 (vecmats l)):real^3^P))) x
= (\x. cstab -
norm (
row (
FST x) (vecmats l) -
row (
SND x) (vecmats (l:real^(M,3)finite_product)))) x` ASSUME_TAC;
ASM_REWRITE_TAC[
J1_SY;
IN_ELIM_THM;
DELETE;
IN_NUMSEG]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`A-B=A-C<=> B=C`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`i<=p ==> i=p \/ i< p:num`)
THEN RESA_TAC;
MRESAL_TAC MOD_MULT[`p:num`;`1:num`][ARITH_RULE`p*1=p/\ SUC 0=1`];
MP_TAC(ARITH_RULE`i< p /\ 2<p ==> i=p -1 \/ SUC i<p:num`)
THEN RESA_TAC;
MP_TAC(ARITH_RULE`2<p ==> p-1< p /\ SUC (p-1)=p`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`p-1:num`;`p:num`];
RESA_TAC
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`i:num`;`p:num`]
THEN SUBGOAL_THEN`
row i ((pmat1 (vecmats l)):real^3^P) =
row i (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`
row (SUC i) ((pmat1 (vecmats l)):real^3^P) =
row (SUC i) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`SUC i < p==> 1<= SUC i /\ SUC i <= p`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
ASM_REWRITE_TAC[];
MRESA_TAC
SUM_EQ[`(\x. cstab -
norm
(
row (
FST x) ((pmat1 (vecmats (l:real^(M,3)finite_product)):real^3^P)) -
row (
SND x) ((pmat1 (vecmats l)):real^3^P)))`;`(\x. cstab -
norm (
row (
FST x) (vecmats l) -
row (
SND x) (vecmats (l:real^(M,3)finite_product))))`;`(
J1_SY (s1:stable_sy)
DELETE (p - 1,p)
DELETE (p,1))`]
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM
th])
THEN MATCH_MP_TAC
SUM_POS_LE
THEN STRIP_TAC;
MATCH_MP_TAC
FINITE_DIFF
THEN REWRITE_TAC[
FINITE_J1_SY;
FINITE_DELETE];
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[
J1_SY;
IN_ELIM_THM;
IN_NUMSEG;
DIFF;
DELETE]
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN MRESA_TAC (GEN_ALL
B_SY_LE_CSTAB)[`i:num`;`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`;]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
MATCH_MP_TAC
SUM_POS_LE
THEN ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN DISJ_CASES_TAC(SET_RULE`x=k-p+1,k-p+2 \/ ~(x=k-p+1,k-p+2 )`);
ASM_REWRITE_TAC[]
THEN EXPAND_TAC"l2"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN SUBGOAL_THEN`
row (k-p+1) ((pmat2 (vecmats l)):real^3^N) =
row (k-1) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p ==> k-p+1<=k-p+2 /\ 1<= k-p+1 /\ k - (k - p + 2) + k - p + 1= k-1`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`
row (k-p+2) ((pmat2 (vecmats l)):real^3^N) =
row k (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p ==> k-p+2<=k-p+2 /\ 1<= k-p+2 /\ k - (k - p + 2) + k - p + 2= k`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE` 2<k ==> 1<=k-1 /\ k-1<= k /\ SUC (k - 1)= k /\ k-1<k`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`k-1:num`;`k:num`]
THEN MRESAL_TAC (GEN_ALL
B_SY_LE_CSTAB)[`k-1:num`;`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`;][ARITH_RULE`SUC 0=1`]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"THY")
THEN DISCH_THEN(LABEL_TAC"THY1")
THEN REMOVE_THEN"THY" MP_TAC
THEN REWRITE_TAC[
J1_SY;
DELETE;
IN_ELIM_THM;
IN_NUMSEG]
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REMOVE_THEN"THY1" MP_TAC
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`i<=k-p+2==> i=k-p+2 \/ i<k-p+2:num`)
THEN RESA_TAC;
MRESAL_TAC MOD_MULT[`k-p+2:num`;`1:num`][ARITH_RULE`p*1=p/\ SUC 0=1`];
MP_TAC(ARITH_RULE`i< k-p+2 /\ 2<p ==> i=k-p +1 \/ i< k-p+1:num`)
THEN RESA_TAC;
MP_TAC(ARITH_RULE`2<p /\ 1<= k-p ==> k-p+1< k-p+2 /\ SUC (k-p+1)=k-p+2`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`k-p+1:num`;`k-p+2:num`];
RESA_TAC
THEN RESA_TAC
THEN EXPAND_TAC"l2"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN MRESA_TAC
MOD_LT[`i:num`;`k-p+2:num`]
THEN SUBGOAL_THEN`
row i ((pmat2 (vecmats l)):real^3^N) =
row (p-2+i) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p ==> k - (k - p + 2) + i= p-2+i`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`
row (SUC i) ((pmat2 (vecmats l)):real^3^N) =
row (p-2+ SUC i) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p/\ i< k-p+1 ==> k - (k - p + 2) + SUC i= p-2+SUC i/\ 1<= SUC i /\ SUC i<= k-p+2`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE` i< k-p+1 /\ 2< p /\ 1<= k-p ==> 1<=p-2+i /\ p-2+i <= k /\ SUC (p-2+i)= p-2+ SUC i /\ p-2+i<k`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`p-2+i:num`;`k:num`]
THEN MRESAL_TAC (GEN_ALL
B_SY_LE_CSTAB)[`p-2+i:num`;`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`;][ARITH_RULE`SUC 0=1`]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
MP_TAC(SET_RULE`~(p,1
IN J1_SY s1
DELETE (p - 1,p))
==>
J1_SY (s1:stable_sy)
DELETE (p - 1,p) =
J1_SY s1
DELETE (p - 1,p)
DELETE (p,1)`)
THEN RESA_TAC
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[
th])
THEN MATCH_MP_TAC(REAL_ARITH`
A1<= A+D /\ &0<= C1 -C /\ &0<= E
==> A1+ #0.1 * -- &1 * C1 <=(A+ #0.1 * -- &1 *(C+B)) + D+ #0.1 * &1* (E+B)`)
THEN STRIP_TAC;
FIND_ASSUM MP_TAC `
COVER2_SY s s1 (s2:stable_sy)`
THEN REWRITE_TAC[
COVER2_SY]
THEN RESA_TAC;
STRIP_TAC;
SUBGOAL_THEN`!x. x
IN (
J1_SY (s1:stable_sy)
DELETE (p - 1,p)
DELETE (p,1))
==> (\x. cstab -
norm
(
row (
FST x) ((pmat1 (vecmats (l:real^(M,3)finite_product)):real^3^P)) -
row (
SND x) ((pmat1 (vecmats l)):real^3^P))) x
= (\x. cstab -
norm (
row (
FST x) (vecmats l) -
row (
SND x) (vecmats (l:real^(M,3)finite_product)))) x` ASSUME_TAC;
ASM_REWRITE_TAC[
J1_SY;
IN_ELIM_THM;
DELETE;
IN_NUMSEG]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`A-B=A-C<=> B=C`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`i<=p ==> i=p \/ i< p:num`)
THEN RESA_TAC;
MRESAL_TAC MOD_MULT[`p:num`;`1:num`][ARITH_RULE`p*1=p/\ SUC 0=1`];
MP_TAC(ARITH_RULE`i< p /\ 2<p ==> i=p -1 \/ SUC i<p:num`)
THEN RESA_TAC;
MP_TAC(ARITH_RULE`2<p ==> p-1< p /\ SUC (p-1)=p`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`p-1:num`;`p:num`];
RESA_TAC
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`i:num`;`p:num`]
THEN SUBGOAL_THEN`
row i ((pmat1 (vecmats l)):real^3^P) =
row i (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`
row (SUC i) ((pmat1 (vecmats l)):real^3^P) =
row (SUC i) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`SUC i < p==> 1<= SUC i /\ SUC i <= p`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
ASM_REWRITE_TAC[];
MRESA_TAC
SUM_EQ[`(\x. cstab -
norm
(
row (
FST x) ((pmat1 (vecmats (l:real^(M,3)finite_product)):real^3^P)) -
row (
SND x) ((pmat1 (vecmats l)):real^3^P)))`;`(\x. cstab -
norm (
row (
FST x) (vecmats l) -
row (
SND x) (vecmats (l:real^(M,3)finite_product))))`;`(
J1_SY (s1:stable_sy)
DELETE (p - 1,p)
DELETE (p,1))`]
THEN EXPAND_TAC"l1"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN ASM_REWRITE_TAC[]
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN MRESAL_TAC
SUM_DIFF[`(\x. cstab -
norm (
row (
FST x) (vecmats (l:real^(M,3)finite_product)) -
row (
SND x) (vecmats l)))`;`
J1_SY(s:stable_sy) `;`
J1_SY (s1:stable_sy)
DELETE (p-1,p:num)
DELETE (p:num,1)`][
FINITE_J1_SY;]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM
th])
THEN MATCH_MP_TAC
SUM_POS_LE
THEN STRIP_TAC;
MATCH_MP_TAC
FINITE_DIFF
THEN REWRITE_TAC[
FINITE_J1_SY;
FINITE_DELETE];
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[
J1_SY;
IN_ELIM_THM;
IN_NUMSEG;
DIFF;
DELETE]
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN MRESA_TAC (GEN_ALL
B_SY_LE_CSTAB)[`i:num`;`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`;]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
MATCH_MP_TAC
SUM_POS_LE
THEN ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN DISJ_CASES_TAC(SET_RULE`x=k-p+1,k-p+2 \/ ~(x=k-p+1,k-p+2 )`);
ASM_REWRITE_TAC[]
THEN EXPAND_TAC"l2"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN SUBGOAL_THEN`
row (k-p+1) ((pmat2 (vecmats l)):real^3^N) =
row (k-1) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p ==> k-p+1<=k-p+2 /\ 1<= k-p+1 /\ k - (k - p + 2) + k - p + 1= k-1`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`
row (k-p+2) ((pmat2 (vecmats l)):real^3^N) =
row k (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p ==> k-p+2<=k-p+2 /\ 1<= k-p+2 /\ k - (k - p + 2) + k - p + 2= k`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE` 2<k ==> 1<=k-1 /\ k-1<= k /\ SUC (k - 1)= k /\ k-1<k`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`k-1:num`;`k:num`]
THEN MRESAL_TAC (GEN_ALL
B_SY_LE_CSTAB)[`k-1:num`;`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`;][ARITH_RULE`SUC 0=1`]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN DISCH_THEN(LABEL_TAC"THY")
THEN DISCH_THEN(LABEL_TAC"THY1")
THEN REMOVE_THEN"THY" MP_TAC
THEN REWRITE_TAC[
J1_SY;
DELETE;
IN_ELIM_THM;
IN_NUMSEG]
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REMOVE_THEN"THY1" MP_TAC
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`i<=k-p+2==> i=k-p+2 \/ i<k-p+2:num`)
THEN RESA_TAC;
MRESAL_TAC MOD_MULT[`k-p+2:num`;`1:num`][ARITH_RULE`p*1=p/\ SUC 0=1`];
MP_TAC(ARITH_RULE`i< k-p+2 /\ 2<p ==> i=k-p +1 \/ i< k-p+1:num`)
THEN RESA_TAC;
MP_TAC(ARITH_RULE`2<p /\ 1<= k-p ==> k-p+1< k-p+2 /\ SUC (k-p+1)=k-p+2`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`k-p+1:num`;`k-p+2:num`];
RESA_TAC
THEN RESA_TAC
THEN EXPAND_TAC"l2"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN MRESA_TAC
MOD_LT[`i:num`;`k-p+2:num`]
THEN SUBGOAL_THEN`
row i ((pmat2 (vecmats l)):real^3^N) =
row (p-2+i) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p ==> k - (k - p + 2) + i= p-2+i`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`
row (SUC i) ((pmat2 (vecmats l)):real^3^N) =
row (p-2+ SUC i) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p/\ i< k-p+1 ==> k - (k - p + 2) + SUC i= p-2+SUC i/\ 1<= SUC i /\ SUC i<= k-p+2`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE` i< k-p+1 /\ 2< p /\ 1<= k-p ==> 1<=p-2+i /\ p-2+i <= k /\ SUC (p-2+i)= p-2+ SUC i /\ p-2+i<k`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`p-2+i:num`;`k:num`]
THEN MRESAL_TAC (GEN_ALL
B_SY_LE_CSTAB)[`p-2+i:num`;`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`;][ARITH_RULE`SUC 0=1`]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
FIND_ASSUM MP_TAC `
COVER_SY 0 (p - 1) s s1 (s2:stable_sy)`
THEN REWRITE_TAC[
COVER_SY;
COVER3_SY;
COVER6_SY;]
THEN ASM_REWRITE_TAC[DE_MORGAN_THM]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[
d_fun]
THEN MRESA1_TAC
sigma_sy`s1:stable_sy`
THEN MRESA1_TAC
sigma_sy`s3:stable_sy`
THEN FIND_ASSUM MP_TAC`
SCHANGE (\x. if x=0 then 0 else (p-2+x) MOD k) s2 (s3:stable_sy)`
THEN REWRITE_TAC[
SCHANGE]
THEN RESA_TAC
THEN SUBGOAL_THEN`~({0,1}
IN J_SY (s3:stable_sy))`ASSUME_TAC;
FIND_ASSUM MP_TAC`~({0, p - 1}
IN J_SY (s2:stable_sy))`
THEN MATCH_MP_TAC MONO_NOT
THEN STRIP_TAC
THEN FIND_ASSUM (fun th-> MP_TAC(ISPECL [`0`;`1`]
th))`!p' q.
{(if p' = 0 then 0 else (p - 2 + p') MOD k), (if q = 0
then 0
else (p - 2 + q) MOD
k)}
IN
J_SY s2 <=>
{p', q}
IN J_SY (s3:stable_sy)`
THEN POP_ASSUM(fun th-> REWRITE_TAC[
th;ARITH_RULE`(0=0) /\ ~(1=0)`])
THEN MP_TAC(ARITH_RULE`2<p/\ 1<= k-p ==> p-2+1=p-1 /\ p-1<k`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`p-1:num`;`k:num`];
SUBGOAL_THEN`~(p - 1,p
IN J1_SY (s1:stable_sy))`ASSUME_TAC;
ASM_REWRITE_TAC[
J1_SY;
IN_ELIM_THM;
PAIR_EQ;
IN_NUMSEG]
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM
th))
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`2<p/\ 1<= k-p ==> p-2+1=p-1 /\ p-1<p/\ 1+p-1=p`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`p-1:num`;`p:num`]
THEN MRESAL_TAC MOD_MULT[`p:num`;`1:num`][ARITH_RULE`p*1=p/\ SUC 0=1`]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN RESA_TAC;
SUBGOAL_THEN`~((k-p+2,1)
IN J1_SY (s3:stable_sy))`ASSUME_TAC;
ASM_REWRITE_TAC[
J1_SY;
IN_ELIM_THM;
PAIR_EQ;
IN_NUMSEG]
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM
th))
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM
th))
THEN STRIP_TAC
THEN STRIP_TAC
THEN MRESAL_TAC MOD_MULT[`k-p+2:num`;`1:num`][ARITH_RULE`p*1=p/\ 1+0=1`]
THEN MRESA_TAC
MOD_LT[`1:num`;`k-p+2:num`];
SUBGOAL_THEN`
J1_SY s1
DELETE (p-1,p)
DELETE (p,1)
SUBSET J1_SY (s:stable_sy)` ASSUME_TAC;
ASM_REWRITE_TAC[
SUBSET;
J1_SY;
IN_ELIM_THM;
DELETE;
IN_NUMSEG]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[
PAIR_EQ;]
THEN MP_TAC(ARITH_RULE`i<=p ==> i=p \/ i< p:num`)
THEN RESA_TAC;
MRESAL_TAC MOD_MULT[`p:num`;`1:num`][ARITH_RULE`p*1=p /\ SUC 0=1`];
MP_TAC(ARITH_RULE`i<p /\ 2<p ==> i=p-1 \/ i< p-1:num`)
THEN RESA_TAC;
MP_TAC(ARITH_RULE`2<p ==> SUC(p-1)=p /\ p-1<p`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`p-1:num`;`p:num`];
STRIP_TAC
THEN STRIP_TAC
THEN EXISTS_TAC`i:num`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`i<p-1 /\ p < k /\ 2<p ==> i< k /\ i<=k:num /\ 1+i<k/\ 1+i< p/\ ~(i=1+i)/\ ~(i=p-1)/\ ~(p=2)`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`i:num`;`p:num`]
THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[
th] THEN REPEAT STRIP_TAC)
THEN MRESA_TAC
MOD_LT[`i:num`;`k:num`]
THEN MRESA_TAC
MOD_LT[`1+i:num`;`k:num`]
THEN MRESA_TAC
MOD_LT[`1+i:num`;`p:num`]
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[SYM
th] )
THEN FIND_ASSUM MP_TAC`
J_SY s1
SUBSET J_SY (s:stable_sy)
UNION {{0, p - 1}}`
THEN REWRITE_TAC[
SUBSET;
UNION;
IN_ELIM_THM;
IN_SING]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC
th`{i,(1+i) MOD p}`)
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC
MOD_LT[`1+i:num`;`p:num`]
THEN STRIP_TAC
THEN MP_TAC(SET_RULE`{i, 1 + i} = {0, p - 1} /\ ~(i=1+i) /\ ~(i=p-1) ==> i=0 /\ 1+i= p-1`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+0=p-1<=> p=2`];
SUBGOAL_THEN`
IMAGE (\(x,y). (p - 2 + x), (p - 2 + y)) (
J1_SY s3
DELETE (k-p+2,1))
SUBSET J1_SY (s:stable_sy)` ASSUME_TAC;
ASM_REWRITE_TAC[
J1_SY;
IMAGE;
DELETE;
SUBSET;
IN_ELIM_THM;
IN_NUMSEG]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[
PAIR_EQ;]
THEN MP_TAC(ARITH_RULE`i<=k-p+2 ==> i=k-p+2 \/ i< k-p+2:num`)
THEN RESA_TAC;
MRESAL_TAC MOD_MULT[`k-p+2:num`;`1:num`][ARITH_RULE`p*1=p /\ SUC 0=1`];
MP_TAC(ARITH_RULE`i<k-p+2 /\ 2<k-p+2 ==> i=k-p+1 \/ i< k-p+1:num`)
THEN RESA_TAC;
POP_ASSUM (fun th-> SUBST_ALL_TAC(
th))
THEN RESA_TAC
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`2<p /\ 2< k-p+2 /\ 2< k ==> p-2+k-p+1=k-1/\ SUC(k-p+1)=k-p+2 /\ k-p+1<k-p+2/\ p - 2 + k - p + 2=k/\ 1<=k-1 /\ k-1<=k/\ k-1<k/\ 1+k-1=k /\ SUC(k-1)=k/\ 1 + k - p + 1= k - p + 2 /\ ~(k-p+1=0)`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`k-p+1:num`;`k-p+2:num`]
THEN MRESA_TAC
MOD_LT[`k-1:num`;`k:num`]
THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`p*1=p /\ SUC 0=1`]
THEN EXISTS_TAC`k-1`
THEN ASM_REWRITE_TAC[]
THEN FIND_ASSUM MP_TAC`{(k - p + 1) MOD (k - p + 2), (
f_sy s2 o
(\x. if x = 0
then 0
else (p - 2 + x) MOD k))
((k - p + 1) MOD (k - p + 2))}
IN
J_SY (s3:stable_sy)`
THEN FIND_ASSUM(fun th-> REWRITE_TAC[SYM
th])`(\i. (1 + i) MOD (k - p + 2)) =
f_sy (s2:stable_sy) o (\x. if x = 0 then 0 else (p - 2 + x) MOD k)`
THEN ASM_REWRITE_TAC[]
THEN MRESAL_TAC MOD_MULT[`k-p+2:num`;`1:num`][ARITH_RULE`p*1=p /\ SUC 0=1`]
THEN STRIP_TAC
THEN FIND_ASSUM (fun th-> MP_TAC( ISPECL [`k-p+1`;`0`]
th))`!p' q.
{(if p' = 0 then 0 else (p - 2 + p') MOD k), (if q = 0
then 0
else (p - 2 + q) MOD
k)}
IN
J_SY s2 <=>
{p', q}
IN J_SY (s3:stable_sy)`
THEN POP_ASSUM (fun th-> REWRITE_TAC[
th;ARITH_RULE`0=0`])
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN FIND_ASSUM MP_TAC`
J_SY s2
SUBSET J_SY (s:stable_sy)
UNION {{0, p - 1}}`
THEN REWRITE_TAC[
SUBSET;
UNION;
IN_ELIM_THM;
IN_SING]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC
th`{k-1,0}`);
POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`1<=k-p /\2<p==> ~(k-1=p-1) /\ ~(0= p-1)`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`~(k-1=p-1) /\ ~(0= p-1)==> ~(p-1
IN {k-1,0})`)
THEN ASM_REWRITE_TAC[]
THEN SET_TAC[];
STRIP_TAC
THEN STRIP_TAC
THEN EXISTS_TAC`p-2+i:num`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`i<k - p + 1 /\ 2<p /\ 1<=i==> p-2+i< k/\ p-2+i<=k /\ 1<=p-2+i/\ 1+p-2+i<k /\ 1+i< k-p+2/\ p-2+1+i<k`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`p-2+1+i:num`;`k:num`]
THEN MRESA_TAC
MOD_LT[`p-2+i:num`;`k:num`]
THEN MP_TAC(ARITH_RULE`i<k - p + 1 /\ 2<p /\ 1<=i==> ~(i=0)/\ ~(1+i=0)`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`1+i:num`;`k-p+2:num`]
THEN MRESA_TAC
MOD_LT[`i:num`;`k-p+2:num`]
THEN REWRITE_TAC[ARITH_RULE`SUC (p - 2 + i)= p - 2 + SUC i`]
THEN MRESA_TAC
MOD_LT[`1+p-2+i:num`;`k:num`]
THEN FIND_ASSUM (fun th-> MP_TAC( ISPECL [`i MOD (k - p + 2)`;`(
f_sy (s2:stable_sy) o (\x. if x = 0 then 0 else (p - 2 + x) MOD k))
(i MOD (k - p + 2))`]
th))`!p' q.
{(if p' = 0 then 0 else (p - 2 + p') MOD k), (if q = 0
then 0
else (p - 2 + q) MOD
k)}
IN
J_SY s2 <=>
{p', q}
IN J_SY (s3:stable_sy)`
THEN FIND_ASSUM(fun th-> REWRITE_TAC[
th])`{i MOD (k - p + 2), (
f_sy s2 o (\x. if x = 0 then 0 else (p - 2 + x) MOD k))
(i MOD (k - p + 2))}
IN
J_SY (s3:stable_sy)`
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[
th])
THEN FIND_ASSUM(fun th-> REWRITE_TAC[SYM
th])`(\i. (1 + i) MOD (k - p + 2)) =
f_sy (s2:stable_sy) o (\x. if x = 0 then 0 else (p - 2 + x) MOD k)`
THEN POP_ASSUM(fun th-> REWRITE_TAC[
th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[
th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[
th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[
th])
THEN POP_ASSUM(fun th-> REWRITE_TAC[
th])
THEN STRIP_TAC
THEN FIND_ASSUM MP_TAC`
J_SY s2
SUBSET J_SY (s:stable_sy)
UNION {{0, p - 1}}`
THEN REWRITE_TAC[
SUBSET;
UNION;
IN_ELIM_THM;
IN_SING]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC
th`{p-2+i,p-2+1+i}`);
ASM_REWRITE_TAC[ARITH_RULE`1+p-2+i= p-2+1+i`];
MP_TAC(SET_RULE`{p - 2 + i, p - 2 + 1 + i} = {0, p - 1} ==> (p-2+i=0) \/ (p-2+1+i=0)`)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`1<=i /\ 2< p==> ~(p-2+i=0) /\ ~(p-2+1+i=0)`)
THEN ASM_REWRITE_TAC[];
MP_TAC(SET_RULE`~(k - p + 2,1
IN J1_SY s3) ==>
J1_SY (s3:stable_sy) =
J1_SY s3
DELETE (k - p + 2,1)`)
THEN RESA_TAC
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[
th])
THEN MP_TAC(SET_RULE`~(p -1,p
IN J1_SY s1) ==>
J1_SY (s1:stable_sy) =
J1_SY s1
DELETE (p -1,p)`)
THEN RESA_TAC
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[
th]);
DISJ_CASES_TAC(SET_RULE`(p,1)
IN J1_SY s1
DELETE (p - 1,p) \/ ~((p,1)
IN J1_SY (s1:stable_sy)
DELETE (p - 1,p))`);
SUBGOAL_THEN`k,1
IN J1_SY (s:stable_sy)`ASSUME_TAC;
POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[
J1_SY;
IN_ELIM_THM;
DELETE;
PAIR_EQ;
IN_NUMSEG]
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM
th))
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC MOD_MULT[`p:num`;`1:num`][ARITH_RULE`p*1=p /\ 1+0=1`]
THEN MP_TAC(ARITH_RULE`2<p /\ 2< k==> 1<p /\ 1<k /\ k<=k`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`1:num`;`p:num`]
THEN STRIP_TAC
THEN EXISTS_TAC`k:num`
THEN ASM_REWRITE_TAC[]
THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`p*1=p /\ SUC 0=1/\ 1+0=1`]
THEN MRESA_TAC
MOD_LT[`1:num`;`k:num`]
THEN FIND_ASSUM MP_TAC`
J_SY s1
SUBSET J_SY (s:stable_sy)
UNION {{0, p - 1}}`
THEN REWRITE_TAC[
SUBSET;
UNION;
IN_ELIM_THM;
IN_SING]
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC
th`{0,1}`);
MP_TAC(ARITH_RULE`2<p ==> ~(p-1=0) /\ ~(p-1=1)`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`~(p-1=0) /\ ~(p-1=1) ==> ~(p-1
IN {0,1})`)
THEN ASM_REWRITE_TAC[]
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN SET_TAC[];
MRESAL_TAC
FINITE_DELETE_IMP[`
J1_SY (s1:stable_sy)`;`p-1,p`][
FINITE_J1_SY]
THEN MRESAL_TAC
FINITE_DELETE_IMP[`
J1_SY (s3:stable_sy)`;`k-p+2,1`][
FINITE_J1_SY]
THEN MRESAL_TAC
SUM_DELETE[`(\x. cstab -
norm (
row (
FST x) (vecmats
l1) -
row (
SND x) (vecmats (l1:real^(P,3)finite_product))))`;`
J1_SY (s1:stable_sy)
DELETE (p-1,p)`;`p:num,1`][
FINITE_J1_SY;REAL_ARITH`A=B-C<=> B=A+C`]
THEN MRESAL_TAC
SUM_DELETE[`(\x. cstab -
norm (
row (
FST x) (vecmats l) -
row (
SND x) (vecmats (l:real^(M,3)finite_product))))`;`
J1_SY (s:stable_sy)`;`k:num,1`][
FINITE_J1_SY;REAL_ARITH`A=B-C<=> B=A+C`]
THEN EXPAND_TAC"l1"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN SUBGOAL_THEN`1<= p/\ p<=
dimindex(:P)==>
row p ((pmat1 (vecmats l)):real^3^P) =
row k (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
ASSUME_TAC(ARITH_RULE`p<=p /\ ~(p<p:num) `)
THEN ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
POP_ASSUM MP_TAC
THEN ASSUME_TAC(ARITH_RULE`p<=p /\ ~(p<p:num) `)
THEN RESA_TAC
THEN SUBGOAL_THEN`
row 1 ((pmat1 (vecmats l)):real^3^P) =
row 1 (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`2<p==> 1<=1 /\ 1<p `)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`
J1_SY s1
DELETE (p - 1,p)
DELETE (p,1)
SUBSET J1_SY (s:stable_sy)
DELETE (k,1)`ASSUME_TAC;
MATCH_MP_TAC(SET_RULE`~(x
IN A) /\ A
SUBSET B==> A
SUBSET B
DELETE x`)
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC(SET_RULE`~(x
IN A) ==> ~(x
IN A
DELETE y)`)
THEN MATCH_MP_TAC(SET_RULE`~(x
IN A) ==> ~(x
IN A
DELETE y)`)
THEN ASM_REWRITE_TAC[
J1_SY;
IN_ELIM_THM;
PAIR_EQ;
IN_NUMSEG]
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM
th))
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`1<= k-p ==> ~(k<=p)`)
THEN RESA_TAC;
ASM_REWRITE_TAC[REAL_ARITH`
A1+ #0.1 * -- &1 * (C1+B) <=(A+ #0.1 * -- &1 *(C+B)) + D+ #0.1 * -- &1* E
<=> A1+ #0.1 * -- &1 * (C1) <=(A+ #0.1 * -- &1 *(C)) + D+ #0.1 * -- &1* E
`]
THEN EXPAND_TAC"l1"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN MATCH_MP_TAC(REAL_ARITH`
A1<= A+D /\ &0<=C1-(C+E)
==>
A1+ #0.1 * -- &1 * (C1) <=(A+ #0.1 * -- &1 *(C)) + D+ #0.1 * -- &1* E`)
THEN STRIP_TAC;
FIND_ASSUM MP_TAC `
COVER2_SY s s1 (s2:stable_sy)`
THEN REWRITE_TAC[
COVER2_SY]
THEN RESA_TAC;
SUBGOAL_THEN`!x. x
IN (
J1_SY (s1:stable_sy)
DELETE (p - 1,p)
DELETE (p,1))
==> (\x. cstab -
norm
(
row (
FST x) ((pmat1 (vecmats (l:real^(M,3)finite_product)):real^3^P)) -
row (
SND x) ((pmat1 (vecmats l)):real^3^P))) x
= (\x. cstab -
norm (
row (
FST x) (vecmats l) -
row (
SND x) (vecmats (l:real^(M,3)finite_product)))) x` ASSUME_TAC;
ASM_REWRITE_TAC[
J1_SY;
IN_ELIM_THM;
DELETE;
IN_NUMSEG]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`A-B=A-C<=> B=C`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`i<=p ==> i=p \/ i< p:num`)
THEN RESA_TAC;
MRESAL_TAC MOD_MULT[`p:num`;`1:num`][ARITH_RULE`p*1=p/\ SUC 0=1`];
MP_TAC(ARITH_RULE`i< p /\ 2<p ==> i=p -1 \/ SUC i<p:num`)
THEN RESA_TAC;
MP_TAC(ARITH_RULE`2<p ==> p-1< p /\ SUC (p-1)=p`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`p-1:num`;`p:num`];
RESA_TAC
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`i:num`;`p:num`]
THEN SUBGOAL_THEN`
row i ((pmat1 (vecmats l)):real^3^P) =
row i (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`
row (SUC i) ((pmat1 (vecmats l)):real^3^P) =
row (SUC i) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`SUC i < p==> 1<= SUC i /\ SUC i <= p`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
ASM_REWRITE_TAC[];
MRESA_TAC
SUM_EQ[`(\x. cstab -
norm
(
row (
FST x) ((pmat1 (vecmats (l:real^(M,3)finite_product)):real^3^P)) -
row (
SND x) ((pmat1 (vecmats l)):real^3^P)))`;`(\x. cstab -
norm (
row (
FST x) (vecmats l) -
row (
SND x) (vecmats (l:real^(M,3)finite_product))))`;`(
J1_SY (s1:stable_sy)
DELETE (p - 1,p)
DELETE (p,1))`]
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN SUBGOAL_THEN`!x. x
IN (
J1_SY (s3:stable_sy)
DELETE (k - p + 2,1))
==>
((\x. cstab -
norm (
row (
FST x) (vecmats (l:real^(M,3)finite_product)) -
row (
SND x) (vecmats l))) o
(\(x,y). p - 2 + x,p - 2 + y)) x
= (\x. cstab -
norm (
row (
FST x) (vecmats (l2:real^(N,3)finite_product)) -
row (
SND x) (vecmats l2))) x`
ASSUME_TAC;
ASM_REWRITE_TAC[
J1_SY;
DELETE;
IN_ELIM_THM;
o_DEF;
IN_NUMSEG]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`A-B=A-C<=> B=C`]
THEN EXPAND_TAC"l2"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`i<=k-p+2==> i=k-p+2 \/ i<k-p+2:num`)
THEN RESA_TAC;
MRESAL_TAC MOD_MULT[`k-p+2:num`;`1:num`][ARITH_RULE`p*1=p/\ SUC 0=1`];
MRESA_TAC
MOD_LT[`i:num`;`k-p+2:num`]
THEN SUBGOAL_THEN`
row i ((pmat2 (vecmats l)):real^3^N) =
row (p-2+i) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p ==> k - (k - p + 2) + i= p-2+i`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`
row (SUC i) ((pmat2 (vecmats l)):real^3^N) =
row (p-2+ SUC i) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p/\ i< k-p+2 ==> k - (k - p + 2) + SUC i= p-2+SUC i/\ 1<= SUC i /\ SUC i<= k-p+2`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
ASM_REWRITE_TAC[];
MRESA_TAC
SUM_EQ[` ((\x. cstab -
norm (
row (
FST x) (vecmats (l:real^(M,3)finite_product)) -
row (
SND x) (vecmats l))) o
(\(x,y). p - 2 + x,p - 2 + y))`;`(\x. cstab -
norm (
row (
FST x) (vecmats (l2:real^(N,3)finite_product)) -
row (
SND x) (vecmats l2)))`;`(
J1_SY (s3:stable_sy)
DELETE (k - p + 2,1))`]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM
th])
THEN SUBGOAL_THEN`(!x y.
x
IN J1_SY s3
DELETE (k - p + 2,1) /\
y
IN J1_SY (s3:stable_sy)
DELETE (k - p + 2,1) /\
(\(x,y). p - 2 + x,p - 2 + y) x = (\(x,y). p - 2 + x,p - 2 + y) y
==> x = y)`ASSUME_TAC;
REWRITE_TAC[
J1_SY;
DELETE;
IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[
PAIR_EQ;ARITH_RULE`p-2+B=p-2+C<=> B=C`];
MRESA_TAC
SUM_IMAGE[`(\(x,y). p - 2 + x,p - 2 + y)`;`(\x. cstab -
norm (
row (
FST x) (vecmats l) -
row (
SND x) (vecmats (l:real^(M,3)finite_product))))`;`
J1_SY (s3:stable_sy)
DELETE (k - p + 2,1)`]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM
th])
THEN SUBGOAL_THEN`
J1_SY (s1:stable_sy)
DELETE (p - 1,p)
DELETE (p,1)
INTER (
IMAGE (\(x,y). p - 2 + x,p - 2 + y) (
J1_SY s3
DELETE (k - p + 2,1)))={}` ASSUME_TAC;
ASM_REWRITE_TAC[SET_RULE`A ={} <=> ~(?a. a
IN A)`;
INTER;
IN_ELIM_THM;
J1_SY;
DELETE;
IMAGE;
IN_NUMSEG]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[
PAIR_EQ]
THEN MP_TAC(ARITH_RULE`i<=p ==> i=p \/ i< p:num`)
THEN RESA_TAC;
POP_ASSUM (fun th-> SUBST_ALL_TAC(
th))
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[]
THEN MRESAL_TAC MOD_MULT[`p:num`;`1:num`][ARITH_RULE`p*1=p/\ SUC 0=1`];
MP_TAC(ARITH_RULE`i<p /\ 2< p ==> i=p-1 \/ i< p-1:num`)
THEN RESA_TAC;
POP_ASSUM (fun th-> SUBST_ALL_TAC(
th))
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE` 2< p ==> p-1< p:num/\ SUC (p-1)=p`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`p-1:num`;`p:num`];
MP_TAC(ARITH_RULE`1<= i /\ i< p-1 /\ 1<= i' ==> ~(i= p-2+i')`)
THEN RESA_TAC;
MRESA_TAC
FINITE_IMAGE[`(\(x,y). p - 2 + x,p - 2 + y)`;`(
J1_SY (s3:stable_sy)
DELETE (k - p + 2,1))`]
THEN MRESAL_TAC (GEN_ALL
SUM_UNION_EQ)[`(\x. cstab -
norm (
row (
FST x) (vecmats l) -
row (
SND x) (vecmats (l:real^(M,3)finite_product))))`;`
J1_SY (s1:stable_sy)
DELETE (p - 1,p)
DELETE (p,1)`;`(
IMAGE (\(x,y). p - 2 + x,p - 2 + y) (
J1_SY (s3:stable_sy)
DELETE (k - p + 2,1)))`;`
J1_SY (s1:stable_sy)
DELETE (p - 1,p)
DELETE (p,1)
UNION (
IMAGE (\(x,y). p - 2 + x,p - 2 + y) (
J1_SY (s3:stable_sy)
DELETE (k - p + 2,1)))`][
FINITE_UNION;
FINITE_DELETE]
THEN SUBGOAL_THEN`
IMAGE (\(x,y). p - 2 + x,p - 2 + y) (
J1_SY s3
DELETE (k - p + 2,1))
SUBSET
J1_SY s
DELETE (k,1)` ASSUME_TAC;
MATCH_MP_TAC(SET_RULE`~(x
IN A) /\ A
SUBSET B ==> A
SUBSET B
DELETE x`)
THEN ASM_REWRITE_TAC[]
THEN ASM_REWRITE_TAC[
IMAGE;
IN_ELIM_THM;
DELETE;
J1_SY;
IN_NUMSEG]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[
PAIR_EQ]
THEN MP_TAC(ARITH_RULE`i<= k-p+2 ==> i=k-p+2 \/ i< k-p+2`)
THEN RESA_TAC;
MRESAL_TAC MOD_MULT[`k-p+2:num`;`1:num`][ARITH_RULE`p*1=p/\ SUC 0=1`];
MP_TAC(ARITH_RULE`i< k-p+2 /\ 1<= k-p /\ 2< p ==> ~(k=p-2 +i)`)
THEN RESA_TAC;
MP_TAC(SET_RULE`
IMAGE (\(x,y). p - 2 + x,p - 2 + y) (
J1_SY s3
DELETE (k - p + 2,1))
SUBSET
J1_SY s
DELETE (k,1)
/\
J1_SY s1
DELETE (p - 1,p)
DELETE (p,1)
SUBSET J1_SY s
DELETE (k,1)
==>
J1_SY s1
DELETE (p - 1,p)
DELETE (p,1)
UNION (
IMAGE (\(x,y). p - 2 + x,p - 2 + y) (
J1_SY s3
DELETE (k - p + 2,1)))
SUBSET J1_SY (s:stable_sy)
DELETE (k,1)`)
THEN RESA_TAC
THEN MRESAL_TAC
SUM_DIFF[`(\x. cstab -
norm (
row (
FST x) (vecmats (l:real^(M,3)finite_product)) -
row (
SND x) (vecmats l)))`;`
J1_SY(s:stable_sy)
DELETE (k,1)`;`
J1_SY (s1:stable_sy)
DELETE (p-1,p:num)
DELETE (p:num,1)
UNION (
IMAGE (\(x,y). p - 2 + x,p - 2 + y) (
J1_SY s3
DELETE (k - p + 2,1)))`][
FINITE_J1_SY;
FINITE_DELETE]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM
th])
THEN MATCH_MP_TAC
SUM_POS_LE
THEN STRIP_TAC;
MATCH_MP_TAC
FINITE_DIFF
THEN REWRITE_TAC[
FINITE_J1_SY;
FINITE_DELETE];
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[
J1_SY;
IN_ELIM_THM;
IN_NUMSEG;
DIFF;
DELETE]
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN MRESA_TAC (GEN_ALL
B_SY_LE_CSTAB)[`i:num`;`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`;]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;
MP_TAC(SET_RULE`~(p,1
IN J1_SY s1
DELETE (p - 1,p))
==>
J1_SY (s1:stable_sy)
DELETE (p - 1,p) =
J1_SY s1
DELETE (p - 1,p)
DELETE (p,1)`)
THEN RESA_TAC
THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[
th])
THEN SUBGOAL_THEN`
J1_SY s1
DELETE (p - 1,p)
DELETE (p,1)
SUBSET J1_SY (s:stable_sy)
DELETE (k,1)`ASSUME_TAC;
MATCH_MP_TAC(SET_RULE`~(x
IN A) /\ A
SUBSET B==> A
SUBSET B
DELETE x`)
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC(SET_RULE`~(x
IN A) ==> ~(x
IN A
DELETE y)`)
THEN MATCH_MP_TAC(SET_RULE`~(x
IN A) ==> ~(x
IN A
DELETE y)`)
THEN ASM_REWRITE_TAC[
J1_SY;
IN_ELIM_THM;
PAIR_EQ;
IN_NUMSEG]
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM
th))
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`1<= k-p ==> ~(k<=p)`)
THEN RESA_TAC;
ASM_REWRITE_TAC[REAL_ARITH`
A1+ #0.1 * -- &1 * (C1+B) <=(A+ #0.1 * -- &1 *(C+B)) + D+ #0.1 * -- &1* E
<=> A1+ #0.1 * -- &1 * (C1) <=(A+ #0.1 * -- &1 *(C)) + D+ #0.1 * -- &1* E
`]
THEN MATCH_MP_TAC(REAL_ARITH`
A1<= A+D /\ &0<=C1-(C+E)
==>
A1+ #0.1 * -- &1 * (C1) <=(A+ #0.1 * -- &1 *(C)) + D+ #0.1 * -- &1* E`)
THEN STRIP_TAC;
FIND_ASSUM MP_TAC `
COVER2_SY s s1 (s2:stable_sy)`
THEN REWRITE_TAC[
COVER2_SY]
THEN RESA_TAC;
SUBGOAL_THEN`!x. x
IN (
J1_SY (s1:stable_sy)
DELETE (p - 1,p)
DELETE (p,1))
==> (\x. cstab -
norm
(
row (
FST x) ((pmat1 (vecmats (l:real^(M,3)finite_product)):real^3^P)) -
row (
SND x) ((pmat1 (vecmats l)):real^3^P))) x
= (\x. cstab -
norm (
row (
FST x) (vecmats l) -
row (
SND x) (vecmats (l:real^(M,3)finite_product)))) x` ASSUME_TAC;
ASM_REWRITE_TAC[
J1_SY;
IN_ELIM_THM;
DELETE;
IN_NUMSEG]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`A-B=A-C<=> B=C`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`i<=p ==> i=p \/ i< p:num`)
THEN RESA_TAC;
MRESAL_TAC MOD_MULT[`p:num`;`1:num`][ARITH_RULE`p*1=p/\ SUC 0=1`];
MP_TAC(ARITH_RULE`i< p /\ 2<p ==> i=p -1 \/ SUC i<p:num`)
THEN RESA_TAC;
MP_TAC(ARITH_RULE`2<p ==> p-1< p /\ SUC (p-1)=p`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`p-1:num`;`p:num`];
RESA_TAC
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`i:num`;`p:num`]
THEN SUBGOAL_THEN`
row i ((pmat1 (vecmats l)):real^3^P) =
row i (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`
row (SUC i) ((pmat1 (vecmats l)):real^3^P) =
row (SUC i) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`SUC i < p==> 1<= SUC i /\ SUC i <= p`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat1;
LAMBDA_BETA;
CART_EQ];
ASM_REWRITE_TAC[];
MRESA_TAC
SUM_EQ[`(\x. cstab -
norm
(
row (
FST x) ((pmat1 (vecmats (l:real^(M,3)finite_product)):real^3^P)) -
row (
SND x) ((pmat1 (vecmats l)):real^3^P)))`;`(\x. cstab -
norm (
row (
FST x) (vecmats l) -
row (
SND x) (vecmats (l:real^(M,3)finite_product))))`;`(
J1_SY (s1:stable_sy)
DELETE (p - 1,p)
DELETE (p,1))`]
THEN EXPAND_TAC"l1"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN ASM_REWRITE_TAC[]
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN SUBGOAL_THEN`!x. x
IN (
J1_SY (s3:stable_sy)
DELETE (k - p + 2,1))
==>
((\x. cstab -
norm (
row (
FST x) (vecmats (l:real^(M,3)finite_product)) -
row (
SND x) (vecmats l))) o
(\(x,y). p - 2 + x,p - 2 + y)) x
= (\x. cstab -
norm (
row (
FST x) (vecmats (l2:real^(N,3)finite_product)) -
row (
SND x) (vecmats l2))) x`
ASSUME_TAC;
ASM_REWRITE_TAC[
J1_SY;
DELETE;
IN_ELIM_THM;
o_DEF;
IN_NUMSEG]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`A-B=A-C<=> B=C`]
THEN EXPAND_TAC"l2"
THEN REWRITE_TAC[
VECMATS_MATVEC_ID;]
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`i<=k-p+2==> i=k-p+2 \/ i<k-p+2:num`)
THEN RESA_TAC;
MRESAL_TAC MOD_MULT[`k-p+2:num`;`1:num`][ARITH_RULE`p*1=p/\ SUC 0=1`];
MRESA_TAC
MOD_LT[`i:num`;`k-p+2:num`]
THEN SUBGOAL_THEN`
row i ((pmat2 (vecmats l)):real^3^N) =
row (p-2+i) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p ==> k - (k - p + 2) + i= p-2+i`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
SUBGOAL_THEN`
row (SUC i) ((pmat2 (vecmats l)):real^3^N) =
row (p-2+ SUC i) (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC;
MP_TAC(ARITH_RULE`1<=k-p/\ 2<p/\ i< k-p+2 ==> k - (k - p + 2) + SUC i= p-2+SUC i/\ 1<= SUC i /\ SUC i<= k-p+2`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[
row;pmat2;
LAMBDA_BETA;
CART_EQ];
ASM_REWRITE_TAC[];
MRESA_TAC
SUM_EQ[` ((\x. cstab -
norm (
row (
FST x) (vecmats (l:real^(M,3)finite_product)) -
row (
SND x) (vecmats l))) o
(\(x,y). p - 2 + x,p - 2 + y))`;`(\x. cstab -
norm (
row (
FST x) (vecmats (l2:real^(N,3)finite_product)) -
row (
SND x) (vecmats l2)))`;`(
J1_SY (s3:stable_sy)
DELETE (k - p + 2,1))`]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM
th])
THEN SUBGOAL_THEN`(!x y.
x
IN J1_SY s3
DELETE (k - p + 2,1) /\
y
IN J1_SY (s3:stable_sy)
DELETE (k - p + 2,1) /\
(\(x,y). p - 2 + x,p - 2 + y) x = (\(x,y). p - 2 + x,p - 2 + y) y
==> x = y)`ASSUME_TAC;
REWRITE_TAC[
J1_SY;
DELETE;
IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[
PAIR_EQ;ARITH_RULE`p-2+B=p-2+C<=> B=C`];
MRESA_TAC
SUM_IMAGE[`(\(x,y). p - 2 + x,p - 2 + y)`;`(\x. cstab -
norm (
row (
FST x) (vecmats l) -
row (
SND x) (vecmats (l:real^(M,3)finite_product))))`;`
J1_SY (s3:stable_sy)
DELETE (k - p + 2,1)`]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM
th])
THEN SUBGOAL_THEN`
J1_SY (s1:stable_sy)
DELETE (p - 1,p)
DELETE (p,1)
INTER (
IMAGE (\(x,y). p - 2 + x,p - 2 + y) (
J1_SY s3
DELETE (k - p + 2,1)))={}` ASSUME_TAC;
ASM_REWRITE_TAC[SET_RULE`A ={} <=> ~(?a. a
IN A)`;
INTER;
IN_ELIM_THM;
J1_SY;
DELETE;
IMAGE;
IN_NUMSEG]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[
PAIR_EQ]
THEN MP_TAC(ARITH_RULE`i<=p ==> i=p \/ i< p:num`)
THEN RESA_TAC;
POP_ASSUM (fun th-> SUBST_ALL_TAC(
th))
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[]
THEN MRESAL_TAC MOD_MULT[`p:num`;`1:num`][ARITH_RULE`p*1=p/\ SUC 0=1`];
MP_TAC(ARITH_RULE`i<p /\ 2< p ==> i=p-1 \/ i< p-1:num`)
THEN RESA_TAC;
POP_ASSUM (fun th-> SUBST_ALL_TAC(
th))
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE` 2< p ==> p-1< p:num/\ SUC (p-1)=p`)
THEN RESA_TAC
THEN MRESA_TAC
MOD_LT[`p-1:num`;`p:num`];
MP_TAC(ARITH_RULE`1<= i /\ i< p-1 /\ 1<= i' ==> ~(i= p-2+i')`)
THEN RESA_TAC;
MRESAL_TAC
FINITE_IMAGE[`(\(x,y). p - 2 + x,p - 2 + y)`;`(
J1_SY (s3:stable_sy)
DELETE (k - p + 2,1))`][
FINITE_J1_SY;
FINITE_DELETE]
THEN MRESAL_TAC (GEN_ALL
SUM_UNION_EQ)[`(\x. cstab -
norm (
row (
FST x) (vecmats l) -
row (
SND x) (vecmats (l:real^(M,3)finite_product))))`;`
J1_SY (s1:stable_sy)
DELETE (p - 1,p)
DELETE (p,1)`;`(
IMAGE (\(x,y). p - 2 + x,p - 2 + y) (
J1_SY (s3:stable_sy)
DELETE (k - p + 2,1)))`;`
J1_SY (s1:stable_sy)
DELETE (p - 1,p)
DELETE (p,1)
UNION (
IMAGE (\(x,y). p - 2 + x,p - 2 + y) (
J1_SY (s3:stable_sy)
DELETE (k - p + 2,1)))`][
FINITE_UNION;
FINITE_DELETE;
FINITE_J1_SY]
THEN MP_TAC(SET_RULE`
IMAGE (\(x,y). p - 2 + x,p - 2 + y) (
J1_SY s3
DELETE (k - p + 2,1))
SUBSET
J1_SY s
/\
J1_SY s1
DELETE (p - 1,p)
DELETE (p,1)
SUBSET J1_SY s
==>
J1_SY s1
DELETE (p - 1,p)
DELETE (p,1)
UNION (
IMAGE (\(x,y). p - 2 + x,p - 2 + y) (
J1_SY s3
DELETE (k - p + 2,1)))
SUBSET J1_SY (s:stable_sy) `)
THEN RESA_TAC
THEN MRESAL_TAC
SUM_DIFF[`(\x. cstab -
norm (
row (
FST x) (vecmats (l:real^(M,3)finite_product)) -
row (
SND x) (vecmats l)))`;`
J1_SY(s:stable_sy) `;`
J1_SY (s1:stable_sy)
DELETE (p-1,p:num)
DELETE (p:num,1)
UNION (
IMAGE (\(x,y). p - 2 + x,p - 2 + y) (
J1_SY s3
DELETE (k - p + 2,1)))`][
FINITE_J1_SY;
FINITE_DELETE]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM
th])
THEN MATCH_MP_TAC
SUM_POS_LE
THEN STRIP_TAC;
MATCH_MP_TAC
FINITE_DIFF
THEN REWRITE_TAC[
FINITE_J1_SY;
FINITE_DELETE];
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[
J1_SY;
IN_ELIM_THM;
IN_NUMSEG;
DIFF;
DELETE]
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN MRESA_TAC (GEN_ALL
B_SY_LE_CSTAB)[`i:num`;`k:num`;`s:stable_sy`;`l:real^(M,3)finite_product`;]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC]);;