(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION *)
(* *)
(* Chapter: Local Fan *)
(* Author: Hoang Le Truong *)
(* Date: 2012-04-01 *)
(* ========================================================================= *)
(*
remaining conclusions from appendix to Local Fan chapter
*)
module Cnicgsf = struct
open Polyhedron;;
open Sphere;;
open Topology;;
open Fan_misc;;
open Planarity;;
open Conforming;;
open Hypermap;;
open Fan;;
open Topology;;
open Wrgcvdr_cizmrrh;;
open Local_lemmas;;
open Collect_geom;;
open Dih2k_hypermap;;
open Wjscpro;;
open Tecoxbm;;
open Hdplygy;;
open Nkezbfc_local;;
open Flyspeck_constants;;
open Gbycpxs;;
open Pcrttid;;
open Local_lemmas1;;
open Pack_defs;;
open Hales_tactic;;
open Appendix;;
open Hypermap;;
open Fan;;
open Wrgcvdr_cizmrrh;;
open Local_lemmas;;
open Flyspeck_constants;;
open Pack_defs;;
open Hales_tactic;;
open Appendix;;
open Zithlqn;;
open Xwitccn;;
open Ayqjtmd;;
open Jkqewgv;;
open Mtuwlun;;
open Uxckfpe;;
open Sgtrnaf;;
open Yxionxl;;
open Qknvmlb;;
open Odxlstcv2;;
open Yxionxl2;;
open Eyypqdw;;
open Ocbicby;;
open Imjxphr;;
open Nuxcoea;;
open Aursipd;;
open Cuxvzoz;;
open Rrcwnsj;;
open Tfitskc;;
open Hexagons;;
open Otmtotj;;
open Hijqaha;;
(*******************)
let SCS_5I1_SLICE_02=prove_by_refinement(
`
scs_arrow_v39
{
scs_stab_diag_v39 scs_5I1 0 2}
{
scs_prop_equ_v39 scs_3M1 1,
scs_prop_equ_v39 scs_4M2 1}`,
[MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
THEN ASM_SIMP_TAC[
SCS_DIAG_SCS_5I1_02;
STAB_5I1_SCS;
SCS_K_D_A_STAB_EQ;]
THEN EXISTS_TAC`0`
THEN EXISTS_TAC`2`
THEN ASM_SIMP_TAC[
SCS_DIAG_SCS_5I1_02]
THEN REWRITE_TAC[
is_scs_slice_v39;
LET_DEF;
LET_END_DEF;
PAIR_EQ]
THEN REPEAT RESA_TAC;
REWRITE_TAC[
is_scs_slice_v39;
LET_DEF;
LET_END_DEF;
PAIR_EQ;
scs_slice_v39;]
THEN STRIP_TAC
THEN MATCH_MP_TAC
scs_inj
THEN ASM_SIMP_TAC[
SCS_5I1_BASIC;
SCS_3M1_BASIC;
J_SCS_4M2;
BASIC_HALF_SLICE_STAB;
J_SCS_3M1;
D_HALF_SLICE;
BAISC_PROP_EQU;
K_SCS_PROP_EUQ;
SCS_4M2_BASIC]
THEN STRIP_TAC;
ASM_SIMP_TAC[
scs_half_slice_v39;
mk_unadorned_v39;scs_v39_explicit;
LET_DEF;
LET_END_DEF;
SCS_K_D_A_STAB_EQ;
K_SCS_3M1;
scs_basic;
unadorned_v39;
scs_stab_diag_v39;
scs_stab_diag_v39;
K_SCS_5I1]
THEN ARITH_TAC;
STRIP_TAC
THEN ASM_REWRITE_TAC[
scs_half_slice_v39;
mk_unadorned_v39;scs_v39_explicit;
LET_DEF;
LET_END_DEF;
SCS_K_D_A_STAB_EQ;
K_SCS_5I1;
scs_basic;
unadorned_v39;
scs_stab_diag_v39;
scs_stab_diag_v39;
K_SCS_3M1;
scs_3M1;
scs_5M3;
ARITH_RULE`(2 + 1 + 5 - 0) MOD 5= 3/\ 0 MOD 5=0/\ a+0=a`;
scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[
FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[
FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;
DIVISION]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;
DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;
ASSOCD_v39;
MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;
PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;
PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;
PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;
ASSOCD_v39;
MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;
PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;
PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;
ASM_SIMP_TAC[
scs_half_slice_v39;
mk_unadorned_v39;scs_v39_explicit;
LET_DEF;
LET_END_DEF;
SCS_K_D_A_STAB_EQ;
K_SCS_4M2;
scs_basic;
unadorned_v39;
scs_stab_diag_v39;
scs_stab_diag_v39;
K_SCS_5I1]
THEN ARITH_TAC;
STRIP_TAC
THEN
ASM_REWRITE_TAC[
scs_half_slice_v39;
mk_unadorned_v39;scs_v39_explicit;
LET_DEF;
LET_END_DEF;
SCS_K_D_A_STAB_EQ;
K_SCS_5I1;
scs_basic;
unadorned_v39;
scs_stab_diag_v39;
scs_stab_diag_v39;
K_SCS_4M2;scs_3T4_prime;
scs_5M3;
ARITH_RULE`(0+1 + 5 - 2) MOD 5= 4/\ 2 MOD 5=2/\ a+0=a`;
scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[
FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[
FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 4<4==> x MOD 4=0\/ x MOD 4=1\/ x MOD 4=2\/ x MOD 4=3`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;
DIVISION]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 4<4==> x' MOD 4=0\/ x' MOD 4=1\/ x' MOD 4=2\/x' MOD 4=3`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;
DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;
ASSOCD_v39;
MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;
PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;
PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`0`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`1`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`2`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`3`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`0`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`1`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`2`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`3`;`1`][ARITH_RULE`~(4=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;
PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;
ASSOCD_v39;
MAP;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC;
PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;
PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`1+x:num`;`1+x':num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;
SCS_TAC
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC
THEN REWRITE_TAC[
J_SCS_3M1]]);;
let SCS_5I2_SLICE_02=prove_by_refinement(`
scs_arrow_v39
{
scs_stab_diag_v39 scs_5I2 0 2}
{
scs_prop_equ_v39 scs_3T1 1,
scs_prop_equ_v39 scs_4M3' 1}`,
[
MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
THEN ASM_SIMP_TAC[
SCS_DIAG_SCS_5I2_02;
STAB_5I2_SCS;
SCS_K_D_A_STAB_EQ;]
THEN EXISTS_TAC`0`
THEN EXISTS_TAC`2`
THEN ASM_SIMP_TAC[
SCS_DIAG_SCS_5I2_02]
THEN REWRITE_TAC[
is_scs_slice_v39;
LET_DEF;
LET_END_DEF;
PAIR_EQ]
THEN REPEAT RESA_TAC;
REWRITE_TAC[
is_scs_slice_v39;
LET_DEF;
LET_END_DEF;
PAIR_EQ;
scs_slice_v39;]
THEN STRIP_TAC
THEN MATCH_MP_TAC
scs_inj
THEN ASM_SIMP_TAC[
SCS_5I2_BASIC;
SCS_3T1_BASIC;
J_SCS_4M3;
BASIC_HALF_SLICE_STAB;
J_SCS_3T1;
D_HALF_SLICE;
BAISC_PROP_EQU;
K_SCS_PROP_EUQ;
SCS_4M3_BASIC]
THEN STRIP_TAC;
ASM_SIMP_TAC[
scs_half_slice_v39;
mk_unadorned_v39;scs_v39_explicit;
LET_DEF;
LET_END_DEF;
SCS_K_D_A_STAB_EQ;
K_SCS_3T1;
scs_basic;
unadorned_v39;
scs_stab_diag_v39;
scs_stab_diag_v39;
K_SCS_5I2]
THEN ARITH_TAC;
STRIP_TAC
THEN ASM_REWRITE_TAC[
scs_half_slice_v39;
mk_unadorned_v39;scs_v39_explicit;
LET_DEF;
LET_END_DEF;
SCS_K_D_A_STAB_EQ;
K_SCS_5I2;
scs_basic;
unadorned_v39;
scs_stab_diag_v39;
scs_stab_diag_v39;
K_SCS_3M1;
scs_3M1;
scs_5M3;
ARITH_RULE`(2 + 1 + 5 - 0) MOD 5= 3/\ 0 MOD 5=0/\ a+0=a`;
scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[
FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[
FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;
DIVISION]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;
DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;
ASSOCD_v39;
MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;
PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;
PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;
PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;
ASSOCD_v39;
MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;
PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;
PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;
ASM_SIMP_TAC[
scs_half_slice_v39;
mk_unadorned_v39;scs_v39_explicit;
LET_DEF;
LET_END_DEF;
SCS_K_D_A_STAB_EQ;
K_SCS_4M3;
scs_basic;
unadorned_v39;
scs_stab_diag_v39;
scs_stab_diag_v39;
K_SCS_5I2]
THEN ARITH_TAC;
STRIP_TAC
THEN
ASM_REWRITE_TAC[
scs_half_slice_v39;
mk_unadorned_v39;scs_v39_explicit;
LET_DEF;
LET_END_DEF;
SCS_K_D_A_STAB_EQ;
K_SCS_5I2;
scs_basic;
unadorned_v39;
scs_stab_diag_v39;
scs_stab_diag_v39;
K_SCS_4M3;
ARITH_RULE`(0+1 + 5 - 2) MOD 5= 4/\ 2 MOD 5=2/\ a+0=a`;
scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[
FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[
FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 4<4==> x MOD 4=0\/ x MOD 4=1\/ x MOD 4=2\/ x MOD 4=3`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;
DIVISION]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 4<4==> x' MOD 4=0\/ x' MOD 4=1\/ x' MOD 4=2\/x' MOD 4=3`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;
DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;
ASSOCD_v39;
MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;
PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;
PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`0`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`1`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`2`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`3`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`0`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`1`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`2`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`3`;`1`][ARITH_RULE`~(4=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;
PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;
ASSOCD_v39;
MAP;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC;
PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;
PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`1+x:num`;`1+x':num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;
SCS_TAC
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC
THEN REWRITE_TAC[
J_SCS_3T1];
]);;
let SCS_5M1_SLICE_02=prove_by_refinement(
`
scs_arrow_v39
{
scs_stab_diag_v39 scs_5M1 0 2}
{
scs_prop_equ_v39 scs_3T4 2,
scs_prop_equ_v39 scs_4M2 1}`,
[
MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
THEN ASM_SIMP_TAC[
SCS_DIAG_SCS_5M1_02;
STAB_5M1_SCS;
SCS_K_D_A_STAB_EQ;]
THEN EXISTS_TAC`0`
THEN EXISTS_TAC`2`
THEN ASM_SIMP_TAC[
SCS_DIAG_SCS_5M1_02]
THEN REWRITE_TAC[
is_scs_slice_v39;
LET_DEF;
LET_END_DEF;
PAIR_EQ]
THEN REPEAT RESA_TAC;
REWRITE_TAC[
is_scs_slice_v39;
LET_DEF;
LET_END_DEF;
PAIR_EQ;
scs_slice_v39;]
THEN STRIP_TAC
THEN MATCH_MP_TAC
scs_inj
THEN ASM_SIMP_TAC[
SCS_5M1_BASIC;
SCS_3T4_BASIC;
J_SCS_4M2;
BASIC_HALF_SLICE_STAB;
J_SCS_3T4;
D_HALF_SLICE;
BAISC_PROP_EQU;
K_SCS_PROP_EUQ;
SCS_4M2_BASIC]
THEN STRIP_TAC;
ASM_SIMP_TAC[
scs_half_slice_v39;
mk_unadorned_v39;scs_v39_explicit;
LET_DEF;
LET_END_DEF;
SCS_K_D_A_STAB_EQ;
K_SCS_3T4;
scs_basic;
unadorned_v39;
scs_stab_diag_v39;
scs_stab_diag_v39;
K_SCS_5M1]
THEN ARITH_TAC;
STRIP_TAC
THEN ASM_REWRITE_TAC[
scs_half_slice_v39;
mk_unadorned_v39;scs_v39_explicit;
LET_DEF;
LET_END_DEF;
SCS_K_D_A_STAB_EQ;
K_SCS_5M1;
scs_basic;
unadorned_v39;
scs_stab_diag_v39;
scs_stab_diag_v39;
K_SCS_3T4;
scs_3M1;
scs_5M3;
ARITH_RULE`(2 + 1 + 5 - 0) MOD 5= 3/\ 0 MOD 5=0/\ a+0=a`;
scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[
FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[
FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;
DIVISION]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;
DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;
ASSOCD_v39;
MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;
PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;
PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`2`][ARITH_RULE`~(3=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;
PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;
ASSOCD_v39;
MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;
PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;
PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`2+x:num`;`2+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;
ASM_SIMP_TAC[
scs_half_slice_v39;
mk_unadorned_v39;scs_v39_explicit;
LET_DEF;
LET_END_DEF;
SCS_K_D_A_STAB_EQ;
K_SCS_4M2;
scs_basic;
unadorned_v39;
scs_stab_diag_v39;
scs_stab_diag_v39;
K_SCS_5M1]
THEN ARITH_TAC;
STRIP_TAC
THEN
ASM_REWRITE_TAC[
scs_half_slice_v39;
mk_unadorned_v39;scs_v39_explicit;
LET_DEF;
LET_END_DEF;
SCS_K_D_A_STAB_EQ;
K_SCS_5M1;
scs_basic;
unadorned_v39;
scs_stab_diag_v39;
scs_stab_diag_v39;
K_SCS_4M2;
ARITH_RULE`(0+1 + 5 - 2) MOD 5= 4/\ 2 MOD 5=2/\ a+0=a`;
scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[
FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[
FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 4<4==> x MOD 4=0\/ x MOD 4=1\/ x MOD 4=2\/ x MOD 4=3`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;
DIVISION]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 4<4==> x' MOD 4=0\/ x' MOD 4=1\/ x' MOD 4=2\/x' MOD 4=3`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;
DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;
ASSOCD_v39;
MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;
PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;
PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`0`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`1`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`2`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`3`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`0`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`1`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`2`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`3`;`1`][ARITH_RULE`~(4=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;
PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;
ASSOCD_v39;
MAP;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC;
PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;
PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`1+x:num`;`1+x':num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;
SCS_TAC
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC
THEN REWRITE_TAC[
J_SCS_3T4];
]);;
let SCS_5M1_SLICE_03=prove_by_refinement(`
scs_arrow_v39
{
scs_stab_diag_v39 scs_5M1 0 3}
{
scs_prop_equ_v39 scs_4M4' 1,
scs_prop_equ_v39 scs_3M1 1}`,
[
MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
THEN ASM_SIMP_TAC[
SCS_DIAG_SCS_5M1_03;
STAB_5M1_SCS;
SCS_K_D_A_STAB_EQ;]
THEN EXISTS_TAC`0`
THEN EXISTS_TAC`3`
THEN ASM_SIMP_TAC[
SCS_DIAG_SCS_5M1_03]
THEN REWRITE_TAC[
is_scs_slice_v39;
LET_DEF;
LET_END_DEF;
PAIR_EQ]
THEN REPEAT RESA_TAC;
REWRITE_TAC[
is_scs_slice_v39;
LET_DEF;
LET_END_DEF;
PAIR_EQ;
scs_slice_v39;]
THEN STRIP_TAC
THEN MATCH_MP_TAC
scs_inj
THEN ASM_SIMP_TAC[
SCS_5M1_BASIC;
SCS_3M1_BASIC;
J_SCS_4M4;
BASIC_HALF_SLICE_STAB;
J_SCS_3M1;
D_HALF_SLICE;
BAISC_PROP_EQU;
K_SCS_PROP_EUQ;
SCS_4M4_BASIC]
THEN STRIP_TAC;
ASM_SIMP_TAC[
scs_half_slice_v39;
mk_unadorned_v39;scs_v39_explicit;
LET_DEF;
LET_END_DEF;
SCS_K_D_A_STAB_EQ;
K_SCS_4M4;
scs_basic;
unadorned_v39;
scs_stab_diag_v39;
scs_stab_diag_v39;
K_SCS_5M1]
THEN ARITH_TAC;
STRIP_TAC
THEN
ASM_REWRITE_TAC[
scs_half_slice_v39;
mk_unadorned_v39;scs_v39_explicit;
LET_DEF;
LET_END_DEF;
SCS_K_D_A_STAB_EQ;
K_SCS_5M1;
scs_basic;
unadorned_v39;
scs_stab_diag_v39;
scs_stab_diag_v39;
K_SCS_4M4;
ARITH_RULE`(3+1 + 5 - 0) MOD 5= 4/\ 0 MOD 5=0/\ a+0=a`;
scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[
FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[
FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 4<4==> x MOD 4=0\/ x MOD 4=1\/ x MOD 4=2\/ x MOD 4=3`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;
DIVISION]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 4<4==> x' MOD 4=0\/ x' MOD 4=1\/ x' MOD 4=2\/x' MOD 4=3`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;
DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;
ASSOCD_v39;
MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;
PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;
PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`0`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`1`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`2`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`3`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`0`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`1`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`2`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`3`;`1`][ARITH_RULE`~(4=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;
PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;
ASSOCD_v39;
MAP;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC;
PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;
PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`1+x:num`;`1+x':num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1/\ 3+1=4`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;
ASM_SIMP_TAC[
scs_half_slice_v39;
mk_unadorned_v39;scs_v39_explicit;
LET_DEF;
LET_END_DEF;
SCS_K_D_A_STAB_EQ;
K_SCS_3M1;
scs_basic;
unadorned_v39;
scs_stab_diag_v39;
scs_stab_diag_v39;
K_SCS_5M1]
THEN ARITH_TAC;
STRIP_TAC
THEN ASM_REWRITE_TAC[
scs_half_slice_v39;
mk_unadorned_v39;scs_v39_explicit;
LET_DEF;
LET_END_DEF;
SCS_K_D_A_STAB_EQ;
K_SCS_5M1;
scs_basic;
unadorned_v39;
scs_stab_diag_v39;
scs_stab_diag_v39;
K_SCS_3M1;
scs_3M1;
scs_5M3;
ARITH_RULE`(0 + 1 + 5 - 3) MOD 5= 3/\ 3 MOD 5=3/\ a+0=a`;
scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[
FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[
FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;
DIVISION]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;
DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;
ASSOCD_v39;
MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;
PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;
PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;
PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;
ASSOCD_v39;
MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;
PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;
PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;
SCS_TAC
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC
THEN REWRITE_TAC[
J_SCS_4M4];
]);;
let SCS_5M1_SLICE_24=prove_by_refinement(`
scs_arrow_v39
{
scs_stab_diag_v39 scs_5M1 2 4}
{
scs_prop_equ_v39 scs_3M1 1,
scs_prop_equ_v39 scs_4M5' 1}`,
[
MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
THEN ASM_SIMP_TAC[
SCS_DIAG_SCS_5M1_24;
STAB_5M1_SCS;
SCS_K_D_A_STAB_EQ;]
THEN EXISTS_TAC`2`
THEN EXISTS_TAC`4`
THEN ASM_SIMP_TAC[
SCS_DIAG_SCS_5M1_24]
THEN REWRITE_TAC[
is_scs_slice_v39;
LET_DEF;
LET_END_DEF;
PAIR_EQ]
THEN REPEAT RESA_TAC;
REWRITE_TAC[
is_scs_slice_v39;
LET_DEF;
LET_END_DEF;
PAIR_EQ;
scs_slice_v39;]
THEN STRIP_TAC
THEN MATCH_MP_TAC
scs_inj
THEN ASM_SIMP_TAC[
SCS_5M1_BASIC;
SCS_3M1_BASIC;
J_SCS_4M5;
BASIC_HALF_SLICE_STAB;
J_SCS_3M1;
D_HALF_SLICE;
BAISC_PROP_EQU;
K_SCS_PROP_EUQ;
SCS_4M5_BASIC]
THEN STRIP_TAC;
ASM_SIMP_TAC[
scs_half_slice_v39;
mk_unadorned_v39;scs_v39_explicit;
LET_DEF;
LET_END_DEF;
SCS_K_D_A_STAB_EQ;
K_SCS_3M1;
scs_basic;
unadorned_v39;
scs_stab_diag_v39;
scs_stab_diag_v39;
K_SCS_5M1]
THEN ARITH_TAC;
STRIP_TAC
THEN
ASM_REWRITE_TAC[
scs_half_slice_v39;
mk_unadorned_v39;scs_v39_explicit;
LET_DEF;
LET_END_DEF;
SCS_K_D_A_STAB_EQ;
K_SCS_5M1;
scs_basic;
unadorned_v39;
scs_stab_diag_v39;
scs_stab_diag_v39;
K_SCS_3M1;
scs_3M1;
scs_5M3;
ARITH_RULE`(4 + 1 + 5 - 2) MOD 5= 3/\ 2 MOD 5=2/\ a+0=a`;
scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[
FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[
FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;
DIVISION]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;
DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;
ASSOCD_v39;
MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;
PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;
PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;
PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;
ASSOCD_v39;
MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;
PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;
PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;
ASM_SIMP_TAC[
scs_half_slice_v39;
mk_unadorned_v39;scs_v39_explicit;
LET_DEF;
LET_END_DEF;
SCS_K_D_A_STAB_EQ;
K_SCS_4M5;
scs_basic;
unadorned_v39;
scs_stab_diag_v39;
scs_stab_diag_v39;
K_SCS_5M1]
THEN ARITH_TAC;
STRIP_TAC
THEN
ASM_REWRITE_TAC[
scs_half_slice_v39;
mk_unadorned_v39;scs_v39_explicit;
LET_DEF;
LET_END_DEF;
SCS_K_D_A_STAB_EQ;
K_SCS_5M1;
scs_basic;
unadorned_v39;
scs_stab_diag_v39;
scs_stab_diag_v39;
K_SCS_4M4;
ARITH_RULE`(2+1 + 5 - 4) MOD 5= 4/\ 4 MOD 5=4/\ a+0=a`;
scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[
FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[
FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 4<4==> x MOD 4=0\/ x MOD 4=1\/ x MOD 4=2\/ x MOD 4=3`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;
DIVISION]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 4<4==> x' MOD 4=0\/ x' MOD 4=1\/ x' MOD 4=2\/x' MOD 4=3`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;
DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;
ASSOCD_v39;
MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;
PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;
PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`0`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`1`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`2`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`3`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`0`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`1`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`2`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`3`;`1`][ARITH_RULE`~(4=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;
PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;
ASSOCD_v39;
MAP;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC;
PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;
PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`1+x:num`;`1+x':num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1/\ 2+4=6/\ 3+4=7/\ 7 MOD 5=2`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;
SCS_TAC
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC
THEN REWRITE_TAC[
J_SCS_3M1];
]);;