John R Harrison writes:
> p permutes s <=> (!x. ~(x IN s) ==> p(x) = x) /\ (!y. ?!x. p x = y)
> For example, you could say in your setting
> p permutes {i:num | i < n}
Thanks for the suggestion. I'm currently thinking that my readers will
be comfortable identifying permutations of S with S-complement-fixing
permutations of the type---the same way that readers are comfortable
identifying natural numbers with nonnegative integers. :-)
The theory of S-complement-fixing permutations of type A should
decompose nicely into
* a theory of permutations of A (group structure, cycles, etc.)---
this is a simplification since it doesn't have to talk about the
subset S---and
* a theory of "p fixes T" (e.g., as a subgroup).
I've verified some theorems for permutations of A (see, e.g.,
pow_int_plus and cycle_shift below), and I guess the Right Thing would
have been to go via Library/grouptheory.ml for the definition of perm^i
or at least for proving perm^(i+j) = perm^i perm^j. Obviously I'm still
learning what's available for proof construction, and I wouldn't be
surprised if my 1000 lines to get to XbackXforth_cyclemin_xor1 below can
be massively compressed, but even as a newbie I'm finding the whole
proof process fast enough. The only frustrations were some time lost at
the beginning from the Debian Bullseye ocaml incompatibility, plus maybe
an hour working around SPEC failures before learning about ISPEC.
---Dan
(* ----- Definitions *)
let xor1 = new_definition
`xor1 (n:num) = if EVEN n then n+1 else n-1`;;
(* "num" in HOL Light is the type {0,1,2,...}.
Can just say "xor1 n"; type-checker will figure it out. *)
(* Warning: If n:num is 0 then n-1 is 0 in HOL Light.
This definition uses n-1 only for positive n. *)
let involution = new_definition
`involution (f:A->A) <=> !x. f(f x) = x`;;
(* "!x" in HOL Light is "for all x of this type".
Type-checker automatically chooses type of x here
as A since x is an f input (and an f output). *)
(* Simpler special case of built-in SURJ. *)
let surjection = new_definition
`surjection (f:A->B) <=> !y. ?x. f x = y`;;
(* "?x" in HOL Light is "there exists x of this type". *)
(* Simpler special case of built-in INJ. *)
let injection = new_definition
`injection (f:A->B) <=> !x y. f x = f y ==> x = y`;;
(* Simpler special case of built-in BIJ. *)
let bijection = new_definition
`bijection (f:A->B) <=> surjection f /\ injection f`;;
(* /\ in HOL Light is "and". *)
(* Same as "inverse" in permutations.ml. *)
let inverse = new_definition
`inverse (f:A->B) = \y. @x. f x = y`;;
(* \y.f(y) in HOL Light is lambda notation
for the function y|->f(y). *)
(* @x.P(x) in HOL Light is some x such that P(x).
Warning: returns an arbitrary element if P(x) is never true. *)
parse_as_infix("pow_num",(24,"left"));;
let pow_num = define
`((p:A->A) pow_num n) = if n = 0 then (I:A->A) else (p o (p pow_num(n-1)))`;;
(* "I" in HOL Light is the identity map. *)
(* "define" is like "new_definition" but allows recursion. *)
parse_as_infix("pow_int",(24,"left"));;
let pow_int = define
`(p:A->A) pow_int (k:int)
= if (&0 <= k) then (p pow_num(num_of_int k))
else (inverse p pow_num(num_of_int(--k)))`;;
(* "&" in HOL Light maps naturals to integers.
Or to real numbers! Important to declare k as an int. *)
(* "--k" in HOL Light is the negative of k. *)
(* "num_of_int k" is @n. &n = k.
Warning: returns an arbitrary natural if k is negative. *)
let cycle = new_definition
`cycle (p:A->A) x = { y | ?k:int. y = (p pow_int k)(x) }`;;
let cyclemin = new_definition
`cyclemin p x = (minimal) (cycle p x)`;;
(* HOL Light defines minimal only for sets of naturals,
so this definition forces p:num->num. *)
parse_as_infix("vanishesifonbothsidesof",(12,"right"));;
let vanishesifonbothsidesof = new_definition
`(p:A->A) vanishesifonbothsidesof (q:A->A) <=> p o q o p = q`;;
parse_as_infix("fixesge",(12,"right"));;
let fixesge = new_definition
`(p:num->num) fixesge n <=> !x. x >= n ==> p(x) = x`;;
(* Special case of "permutes" from permutations.ml.
There isn't a type {0,1,...,n-1} in HOL Light;
easiest way to describe a permutation of {0,1,...,n-1}
is as a permutation of the integers that fixes {n,n+1,...}. *)
parse_as_infix("permutesrange",(12,"right"));;
let permutesrange = new_definition
`(p:num->num) permutesrange n <=> bijection p /\ p fixesge n`;;
let XbackXforth = new_definition
`XbackXforth pi = pi o xor1 o inverse pi o xor1`;;
(* ----- injection basics *)
let involution_I = prove(
`involution (I:A->A)`,
MESON_TAC[I_DEF;involution]);;
let injection_ifinvolution = prove(
`!(p:A->A). involution p ==> injection p`,
REWRITE_TAC[involution;injection]
THEN MESON_TAC[]);;
let injection_I = prove(
`injection (I:A->A)`,
MESON_TAC[involution_I;injection_ifinvolution]);;
let injection_composes = prove(
`!p:A->B q:B->C. injection p /\ injection q ==> injection(q o p)`,
REWRITE_TAC[injection]
THEN REWRITE_TAC[o_THM] THEN MESON_TAC[]);;
(* ----- surjection basics *)
let surjection_ifinvolution = prove(
`!p:A->A. involution p ==> surjection p`,
REWRITE_TAC[involution;surjection]
THEN GEN_TAC THEN DISCH_TAC THEN GEN_TAC
THEN EXISTS_TAC `(p:A->A)(y)`
THEN ASM_MESON_TAC[]);;
let surjection_I = prove(
`surjection (I:A->A)`,
MESON_TAC[involution_I;surjection_ifinvolution]);;
let surjection_composes = prove(
`!p:A->B q:B->C. surjection p /\ surjection q ==> surjection(q o p)`,
REWRITE_TAC[surjection;o_THM]
THEN MESON_TAC[]);;
(* ----- bijection basics *)
let bijection_ifinvolution = prove(
`!p:A->A. involution p ==> bijection p`,
MESON_TAC[surjection_ifinvolution;injection_ifinvolution;bijection]);;
let bijection_I = prove(
`bijection (I:A->A)`,
MESON_TAC[involution_I;bijection_ifinvolution]);;
let bijection_composes = prove(
`!p:A->B q:B->C. bijection p /\ bijection q ==> bijection(q o p)`,
REWRITE_TAC[bijection]
THEN MESON_TAC[surjection_composes;injection_composes]);;
let bijection_inverseisinjection = prove(
`bijection (p:A->B) ==> injection(inverse p)`,
REWRITE_TAC[bijection;surjection;injection;inverse]
THEN MESON_TAC[]);;
let bijection_inverseissurjection = prove(
`bijection (p:A->B) ==> surjection(inverse p)`,
REWRITE_TAC[bijection;surjection;injection;inverse]
THEN MESON_TAC[]);;
let bijection_inverseisbijection = prove(
`bijection (p:A->B) ==> bijection(inverse p)`,
MESON_TAC[bijection_inverseisinjection;
bijection_inverseissurjection;bijection]);;
let bijection_inverse_composition1 = prove(
`!p:A->B x. bijection p ==> p((inverse p)x) = x`,
REWRITE_TAC[bijection;surjection;injection;inverse]
THEN MESON_TAC[]);;
let bijection_inverse_composition2 = prove(
`!p:A->B. bijection p ==> !x. (inverse p)(p x) = x`,
REWRITE_TAC[bijection;surjection;injection;inverse]
THEN MESON_TAC[]);;
let bijection_inverse_composition3 = prove(
`!p:A->B. bijection p ==> !x. (p o inverse p)x = x`,
MESON_TAC[bijection_inverse_composition1;o_THM]);;
let bijection_inverse_composition4 = prove(
`!p:A->B. bijection p ==> !x. (inverse p o p)x = x`,
MESON_TAC[bijection_inverse_composition2;o_THM]);;
let bijection_inverse_composition5 = prove(
`!p:A->B. bijection p ==> p o inverse p = I`,
MESON_TAC[bijection_inverse_composition3;I_THM;EQ_EXT]);;
let bijection_inverse_composition6 = prove(
`!p:A->B. bijection p ==> inverse p o p = I`,
MESON_TAC[bijection_inverse_composition4;I_THM;EQ_EXT]);;
let bijection_frominverse = prove(
`!p:A->B q:B->A. q o p = I /\ p o q = I ==> bijection p /\ q = inverse p`,
REWRITE_TAC[bijection;surjection;injection;inverse]
THEN MESON_TAC[I_THM;o_THM;EQ_EXT]);;
let bijection_matchinverse = prove(
`!p:A->B. bijection p ==> !q:B->A. p o q = I ==> q = inverse p`,
REWRITE_TAC[bijection;surjection;injection;inverse] THEN
MESON_TAC[I_THM;o_THM;EQ_EXT]);;
let bijection_matchinverse2 = prove(
`!p:A->B. bijection p ==> !q:B->A. q o p = I ==> q = inverse p`,
REWRITE_TAC[bijection;surjection;injection;inverse] THEN
MESON_TAC[I_THM;o_THM;EQ_EXT]);;
let bijection_inverse_inverse = prove(
`!p:A->B. bijection p ==> inverse(inverse p) = p`,
MESON_TAC[bijection_inverse_composition5;
bijection_inverse_composition6;bijection_frominverse]);;
(* ----- EVEN, ODD basics *)
let suc_isadd1 = prove(
`!n. SUC n = n+1`,
MESON_TAC[ONE;ADD_SUC;ADD_0]);;
let nonzero_sub1add1 = prove(
`!n. ~(n = 0) ==> (n-1)+1 = n`,
MESON_TAC[LTE_CASES;LE_1;SUB_ADD]);;
let nonzero_subsuc = prove(
`!n. ~(n = 0) ==> SUC(n-1) = n`,
MESON_TAC[nonzero_sub1add1;suc_isadd1]);;
let nonzero_pre_le_suc = prove(
`!n. ~(n = 0) ==> n-1 <= SUC(n-1)`,
MESON_TAC[LE_REFL;LE]);;
let pre_le_ifnonzero = prove(
`!n. ~(n = 0) ==> n-1 <= n`,
MESON_TAC[nonzero_pre_le_suc;nonzero_subsuc]);;
let pre_le_ifzero = prove(
`!n. n = 0 ==> n-1 <= n`,
CONV_TAC ARITH_RULE);;
let pre_le = prove(
`!n. n-1 <= n`,
MESON_TAC[pre_le_ifzero;pre_le_ifnonzero]);;
let even_odd_add1 = prove(
`!n. EVEN n ==> ODD(n+1)`,
REWRITE_TAC[ODD_ADD;ODD;EVEN;ONE;NOT_ODD]);;
let even_add1_odd = prove(
`!n. EVEN(n+1) ==> ODD n`,
MESON_TAC[ONE;NOT_EVEN;EVEN_ADD;EVEN;ODD]);;
let odd_even_sub1 = prove(
`!n. ODD n ==> EVEN(n-1)`,
MESON_TAC[EVEN_SUB;ODD;EVEN;NOT_EVEN;ONE;LTE_CASES]);;
let odd_sub1add1 = prove(
`!n. ODD n ==> (n-1)+1 = n`,
MESON_TAC[nonzero_sub1add1;ODD]);;
let odd_sub1distinct = prove(
`!n. ODD n ==> ~(n-1 = n)`,
GEN_TAC THEN
ASSUME_TAC(ARITH_RULE `~(n-1 = (n-1)+1)`) THEN
ASM_MESON_TAC[odd_sub1add1]);;
let sandwich_suc = prove(
`!m n. m < n /\ n <= SUC m ==> SUC m = n`,
MESON_TAC[LE_ANTISYM;LE_SUC_LT]);;
let sandwich_add1 = prove(
`!m n. m < n /\ n <= m+1 ==> m+1 = n`,
MESON_TAC[sandwich_suc;suc_isadd1]);;
let sandwich_even_add1_odd = prove(
`n < 2*b /\ 2*b <= n+1 ==> ODD n`,
MESON_TAC[EVEN_DOUBLE;sandwich_add1;even_add1_odd;NOT_EVEN]);;
(* ----- xor1 basics *)
let xor1_distinct = prove(
`!n. ~(xor1 n = n)`,
REWRITE_TAC[xor1] THEN GEN_TAC THEN
ASSUME_TAC(ARITH_RULE `~(n+1 = n)`) THEN
ASSUME_TAC(SPEC `n:num` odd_sub1distinct) THEN
DISJ_CASES_TAC (SPEC `n:num` EVEN_OR_ODD) THEN
ASM_SIMP_TAC[] THEN
ASM_MESON_TAC[NOT_ODD]);;
let xor1_oneven_isadd1 = prove(
`!n. EVEN n ==> xor1 n = n+1`,
MESON_TAC[xor1]);;
let xor1_oneven_isodd = prove(
`!n. EVEN n ==> ODD(xor1 n)`,
MESON_TAC[even_odd_add1;xor1]);;
let xor1_onodd_issub1 = prove(
`!n. ODD n ==> xor1 n = n-1`,
MESON_TAC[NOT_EVEN;xor1]);;
let xor1_onodd_iseven = prove(
`!n. ODD n ==> EVEN(xor1 n)`,
MESON_TAC[xor1_onodd_issub1;odd_even_sub1]);;
let xor1xor1_ifeven = prove(
`!n. EVEN n ==> xor1(xor1 n) = n`,
MESON_TAC[xor1_oneven_isodd;xor1_onodd_issub1;
xor1_oneven_isadd1;ARITH_RULE `(n+1)-1 = n`]);;
let xor1xor1_ifodd = prove(
`!n. ODD n ==> xor1(xor1 n) = n`,
MESON_TAC[xor1_onodd_iseven;xor1_onodd_issub1;
xor1_oneven_isadd1;odd_sub1add1]);;
let xor1xor1 = prove(
`!n. xor1(xor1 n) = n`,
MESON_TAC[xor1xor1_ifodd;xor1xor1_ifeven;EVEN_OR_ODD]);;
let xor1_involution = prove(
`xor1 o xor1 = I`,
REWRITE_TAC[I_DEF;o_DEF;xor1xor1]);;
let xor1_involution2 = prove(
`involution xor1`,
MESON_TAC[xor1xor1;involution]);;
let xor1_lteven = prove(
`!n b. n < 2*b ==> xor1 n < 2*b`,
REWRITE_TAC[xor1]
THEN DISJ_CASES_TAC(SPEC `n:num` EVEN_OR_ODD)
THEN MESON_TAC[LTE_CASES;sandwich_even_add1_odd;
NOT_EVEN;pre_le;NOT_EVEN;LET_TRANS]);;
let xor1_geeven = prove(
`!n b. n >= 2*b ==> xor1 n >= 2*b`,
MESON_TAC[xor1xor1;xor1_lteven;NOT_LT;GE]);;
let xor1_lemma101 = prove(
`!m n. EVEN m ==> EVEN n ==> ~(n = m + 1)`,
MESON_TAC[even_odd_add1;NOT_ODD]);;
let xor1_lemma102 = prove(
`!m n. EVEN m ==> EVEN n ==> n <= m + 1 ==> n <= m`,
REPEAT STRIP_TAC THEN
ASSUME_TAC(SPEC `m:num` suc_isadd1) THEN
ASM_MESON_TAC[xor1_lemma101;LE_LT;LT_SUC_LE]);;
let xor1_lemma103 = prove(
`!m n. EVEN m ==> EVEN n ==> m < xor1 n /\ n <= xor1 m ==> m = n`,
REPEAT GEN_TAC THEN DISCH_TAC THEN DISCH_TAC THEN
REWRITE_TAC[xor1] THEN
ASM_SIMP_TAC[] THEN
ASSUME_TAC(ARITH_RULE `n <= m /\ m < n + 1 ==> m = n`) THEN
ASM_MESON_TAC[xor1_lemma102]);;
let xor1_lemma104 = prove(
`!m n. ~EVEN m ==> ~EVEN n ==> m < xor1 n ==> xor1 m < n`,
REPEAT GEN_TAC THEN DISCH_TAC THEN DISCH_TAC THEN
REWRITE_TAC[xor1] THEN
ASM_SIMP_TAC[] THEN
ARITH_TAC);;
let xor1_lemma105 = prove(
`!m n. ~EVEN m ==> EVEN n ==> m < xor1 n /\ n <= xor1 m ==> m = n`,
REPEAT GEN_TAC THEN DISCH_TAC THEN DISCH_TAC THEN
REWRITE_TAC[xor1] THEN
ASM_SIMP_TAC[] THEN
ARITH_TAC);;
let xor1_lemma106 = prove(
`!m n. EVEN m ==> ~EVEN n ==> m < xor1 n ==> xor1 m < n`,
REPEAT GEN_TAC THEN DISCH_TAC THEN DISCH_TAC THEN
REWRITE_TAC[xor1] THEN
ASM_SIMP_TAC[] THEN
ARITH_TAC);;
let xor1_lemma107 = prove(
`!m n. m < xor1 n /\ n <= xor1 m ==> m = n`,
REPEAT GEN_TAC THEN
DISJ_CASES_TAC (TAUT `EVEN m \/ ~EVEN m`) THEN
DISJ_CASES_TAC (TAUT `EVEN n \/ ~EVEN n`) THEN
ASM_MESON_TAC[NOT_LT;xor1_lemma103;xor1_lemma104;xor1_lemma105;xor1_lemma106]);;
let xor1_lemma108 = prove(
`!m n. m <= xor1 n /\ n <= xor1 m /\ ~(m = n) ==> m = xor1 n`,
MESON_TAC[xor1_lemma107;LE_LT]);;
(* ----- natural powers of a function from A to A *)
let pow_num_eval = prove(
`!p:A->A. !n. ~(n = 0) ==> !x. (p pow_num n)x = p((p pow_num(n-1))x)`,
ASM_MESON_TAC[pow_num;o_DEF]);;
let pow_num_0 = prove(
`!p:A->A. p pow_num 0 = I`,
REWRITE_TAC[pow_num]);;
let pow_num_0_eval = prove(
`!p:A->A. !x. (p pow_num 0)x = x`,
REWRITE_TAC[pow_num_0;I_DEF]);;
let pow_num_11 = prove(
`!p:A->A. p pow_num (1-1) = I`,
REWRITE_TAC[ARITH_RULE `1-1=0`;pow_num_0]);;
let pow_num_111 = prove(
`!p:A->A. p o (p pow_num (1-1)) = p`,
REWRITE_TAC[pow_num_11;I_O_ID]);;
let pow_num_1 = prove(
`!p:A->A. p pow_num 1 = p`,
ASM_MESON_TAC[pow_num;pow_num_111;ARITH_RULE `~(1 = 0)`]);;
let pow_num_1_eval = prove(
`!p:A->A. !x. (p pow_num 1) x = p x`,
REWRITE_TAC[pow_num_1]);;
let pow_num_n11 = prove(
`!n p:A->A. p pow_num(n+1) = p o (p pow_num((n+1)-1))`,
ASM_MESON_TAC[pow_num;ARITH_RULE `~(n+1 = 0)`]);;
let pow_num_plus1 = prove(
`!n p:A->A. p pow_num(n+1) = p o (p pow_num n)`,
ASM_MESON_TAC[pow_num_n11;ARITH_RULE `(n+1)-1 = n`]);;
let pow_num_plus1_eval = prove(
`!n p:A->A. !x. (p pow_num(n+1)) x = p((p pow_num n) x)`,
ASM_MESON_TAC[pow_num_plus1;o_DEF]);;
let pow_num_plus_flip = prove(
`!m n p:A->A. p pow_num(n+m) = (p pow_num m) o (p pow_num n)`,
INDUCT_TAC THENL [
REWRITE_TAC[pow_num_0;I_O_ID;ARITH_RULE `n+0 = n`]
;
REWRITE_TAC[suc_isadd1;ARITH_RULE `n+m+1 = (n+m)+1`;pow_num_plus1]
THEN ASM_MESON_TAC[o_ASSOC]
]);;
let pow_num_plus_flip_eval = prove(
`!m n p:A->A. !x. (p pow_num(n+m))x = (p pow_num m)((p pow_num n) x)`,
ASM_MESON_TAC[pow_num_plus_flip;o_DEF]);;
let pow_num_plus = prove(
`!m n p:A->A. p pow_num(m+n) = (p pow_num m) o (p pow_num n)`,
MESON_TAC[pow_num_plus_flip;ARITH_RULE `n+m = m+n`]);;
let pow_num_plus_eval = prove(
`!m n p:A->A. !x. (p pow_num(m+n))x = (p pow_num m)((p pow_num n) x)`,
MESON_TAC[pow_num_plus_flip_eval;ARITH_RULE `n+m = m+n`]);;
let pow_num_plus1_right = prove(
`!n p:A->A. p pow_num(n+1) = (p pow_num n) o p`,
MESON_TAC[pow_num_plus;pow_num_1]);;
let pow_num_plus1_right_eval = prove(
`!n p:A->A. !x. (p pow_num(n+1))x = (p pow_num n)(p x)`,
MESON_TAC[pow_num_plus1_right;o_DEF]);;
let pow_num_bijection = prove(
`!p:A->A. bijection p ==> !n. bijection (p pow_num n)`,
GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THENL
[ REWRITE_TAC[pow_num_0;bijection_I]
; REWRITE_TAC[suc_isadd1] THEN
ASM_MESON_TAC[pow_num_plus1;bijection_composes]
]);;
let pow_num_plus1_bijection = prove(
`!n p:A->A. bijection p ==> inverse p o (p pow_num(n+1)) = p pow_num n`,
REWRITE_TAC[pow_num_plus1] THEN
MESON_TAC[bijection_inverse_composition6;o_ASSOC;I_O_ID]);;
let pow_num_plus1_inverse = prove(
`!n p:A->A. bijection p ==> p o ((inverse p) pow_num(n+1)) = (inverse p)
pow_num n`,
MESON_TAC[pow_num_plus1_bijection;
bijection_inverseisbijection;bijection_inverse_inverse]);;
(* ----- integer powers of a permutation of A *)
let pow_int_0 = prove(
`!p:A->A. p pow_int &0 = I`,
REWRITE_TAC[pow_int;NUM_OF_INT_OF_NUM;pow_num_0] THEN
SIMP_TAC[INT_ARITH `&0:int <= &0`]);;
let pow_int_1 = prove(
`!p:A->A. p pow_int &1 = p`,
REWRITE_TAC[pow_int;NUM_OF_INT_OF_NUM;pow_num_1] THEN
SIMP_TAC[INT_ARITH `&0:int <= &1`]);;
let pow_int_bijection_nonnegative = prove(
`!p:A->A. bijection p ==> !k:int. &0 <= k ==> bijection (p pow_int k)`,
GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
REWRITE_TAC[pow_int] THEN
ASM_SIMP_TAC[] THEN
ASM_MESON_TAC[pow_num_bijection]);;
let pow_int_bijection_negative = prove(
`!p:A->A. !k:int. bijection p /\ k < &0 ==> bijection (p pow_int k)`,
GEN_TAC THEN GEN_TAC THEN DISCH_TAC THEN
REWRITE_TAC[pow_int] THEN
ASM_MESON_TAC[pow_num_bijection;bijection_inverseisbijection]);;
let pow_int_bijection = prove(
`!p:A->A. !k:int. bijection p ==> bijection (p pow_int k)`,
REPEAT GEN_TAC THEN DISCH_TAC THEN
DISJ_CASES_TAC(INT_ARITH `k:int < &0 \/ &0 <= k`) THENL
[ ASM_MESON_TAC[pow_int_bijection_negative]
; ASM_MESON_TAC[pow_int_bijection_nonnegative]
]);;
let pow_int_cancel = prove(
`!p:A->A k x y. bijection p /\ (p pow_int k) x = (p pow_int k) y ==> x = y`,
REPEAT GEN_TAC THEN
ASSUME_TAC(SPEC `p:A->A` pow_int_bijection) THEN
ASM_MESON_TAC[bijection;injection]);;
let pow_int_plus1_nonnegative = prove(
`!p:A->A. !k:int. &0 <= k ==> p pow_int(k + &1) = p o (p pow_int k)`,
REWRITE_TAC[pow_int] THEN
GEN_TAC THEN GEN_TAC THEN DISCH_TAC THEN
ASSUME_TAC(INT_ARITH `&0 <= k:int ==> &0 <= k + &1`) THEN
ASSUME_TAC(SPEC `p:A->A`(SPEC `num_of_int(k:int)` pow_num_plus1)) THEN
ASSUME_TAC(INT_ARITH `(&0:int) <= &1`) THEN
ASSUME_TAC(SPEC `1` NUM_OF_INT_OF_NUM) THEN
ASSUME_TAC(SPECL[`k:int`;`&1:int`]NUM_OF_INT_ADD) THEN
SUBGOAL_THEN `&0 <= (k:int) + &1` ASSUME_TAC THEN
ASM_SIMP_TAC[] THEN
ASM_MESON_TAC[]);;
let int_negative_num_towards0 = prove(
`!k:int. k < &0 ==> num_of_int(--(k + &1)) + 1 = num_of_int(--k)`,
GEN_TAC THEN DISCH_TAC THEN
ASSUME_TAC(SPECL[`--((k:int) + &1)`;`&1:int`]NUM_OF_INT_ADD) THEN
ASSUME_TAC(INT_ARITH `k:int < &0 ==> &0 <= --(k + &1)`) THEN
ASSUME_TAC(INT_ARITH `--((k:int) + &1) + &1 = --k`) THEN
ASSUME_TAC(INT_ARITH `(&0:int) <= &1`) THEN
ASSUME_TAC(SPEC `1` NUM_OF_INT_OF_NUM) THEN
ASM_MESON_TAC[]);;
let pow_int_plus1_negative = prove(
`!p:A->A. bijection p ==> !k:int. k < &0 ==> p pow_int(k + &1) = p o (p
pow_int k)`,
REWRITE_TAC[pow_int] THEN
GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
DISJ_CASES_TAC(INT_ARITH `-- &1 <= k:int \/ k < -- &1`) THENL
[
ASSUME_TAC(INT_ARITH `-- &1 <= (k:int) /\ k < &0 ==> k = -- &1`) THEN
ASSUME_TAC(INT_ARITH `k:int = -- &1 ==> ~(&0 <= k)`) THEN
ASSUME_TAC(INT_ARITH `k:int = -- &1 ==> &0 <= k + &1`) THEN
ASSUME_TAC(INT_ARITH `-- -- &1:int = &1`) THEN
ASSUME_TAC(INT_ARITH `-- (&1:int) + &1 = &0`) THEN
ASSUME_TAC(SPEC `1` NUM_OF_INT_OF_NUM) THEN
ASSUME_TAC(SPEC `0` NUM_OF_INT_OF_NUM) THEN
ASSUME_TAC(SPEC `p:A->A` pow_num_0) THEN
ASSUME_TAC(SPEC `inverse(p:A->A)` pow_num_1) THEN
ASM_SIMP_TAC[] THEN
ASM_MESON_TAC[bijection_inverse_composition5]
;
ASSUME_TAC(INT_ARITH `k:int < -- &1 ==> ~(&0 <= k)`) THEN
ASSUME_TAC(INT_ARITH `k:int < -- &1 ==> ~(&0 <= k + &1)`) THEN
ASSUME_TAC(SPEC `k:int` int_negative_num_towards0) THEN
ASSUME_TAC(SPECL[`num_of_int(--((k:int) +
&1))`;`p:A->A`]pow_num_plus1_inverse) THEN
ASM_MESON_TAC[]
]);;
let pow_int_plus1 = prove(
`!p:A->A. bijection p ==> !k:int. p pow_int(k + &1) = p o (p pow_int k)`,
GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN
DISJ_CASES_TAC(INT_ARITH `k:int < &0 \/ &0 <= k`)
THENL[ASM_MESON_TAC[pow_int_plus1_negative];
ASM_MESON_TAC[pow_int_plus1_nonnegative]]);;
let pow_int_plusnum = prove(
`!p:A->A. bijection p ==> !m. !k:int. p pow_int(k + &m) = (p pow_num m) o (p
pow_int k)`,
GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THENL
[
ASSUME_TAC(INT_ARITH `(k:int) + &0 = k`) THEN
ASM_SIMP_TAC[] THEN
REWRITE_TAC[pow_num_0;I_O_ID]
;
GEN_TAC THEN
REWRITE_TAC[suc_isadd1] THEN
REWRITE_TAC[pow_num_plus1] THEN
ASSUME_TAC(INT_ARITH `(k:int) + (&m + &1) = (k + &m) + &1`) THEN
ASSUME_TAC(SPECL[`m:num`;`1:num`]INT_OF_NUM_ADD) THEN
ASM_MESON_TAC[o_ASSOC;pow_int_plus1]
]);;
let pow_int_plus_nonnegative = prove(
`!p:A->A. bijection p ==> !j:int. &0 <= j ==>
!k:int. p pow_int(k + j) = (p pow_int j) o (p pow_int k)`,
GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
ASSUME_TAC(SPEC `j:int` NUM_OF_INT) THEN
ASM_MESON_TAC[pow_int_plusnum;pow_int]);;
let pow_int_inverse_lemma1 = prove(
`!p:A->A. bijection p ==> !j:int. &0 <= j ==>
p pow_int(--j + j) = (p pow_int j) o (p pow_int --j)`,
MESON_TAC[pow_int_plus_nonnegative]);;
let pow_int_inverse_lemma2 = prove(
`!p:A->A. bijection p ==> !j:int. &0 <= j ==>
p pow_int &0 = (p pow_int j) o (p pow_int --j)`,
GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
ASSUME_TAC(INT_ARITH `--j + (j:int) = &0`) THEN
ASM_MESON_TAC[pow_int_inverse_lemma1]);;
let pow_int_inverse_lemma3 = prove(
`!p:A->A. bijection p ==> !j:int. &0 <= j ==>
(p pow_int j) o (p pow_int --j) = I`,
MESON_TAC[pow_int_inverse_lemma2;pow_int_0]);;
let pow_int_inverse_nonnegative = prove(
`!p:A->A. bijection p ==> !j:int. &0 <= j ==>
p pow_int --j = inverse(p pow_int j)`,
GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
ASM_MESON_TAC[pow_int_bijection;bijection_matchinverse;pow_int_inverse_lemma3]);;
let pow_int_inverse_negative = prove(
`!p:A->A. bijection p ==> !j:int. j < &0 ==>
p pow_int --j = inverse(p pow_int j)`,
GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
ASSUME_TAC(ARITH_RULE `(j:int) < &0 ==> &0 <= --j`) THEN
ASSUME_TAC(ARITH_RULE `(j:int) = -- --j`) THEN
ASM_MESON_TAC[pow_int_bijection;
bijection_inverse_inverse;pow_int_inverse_nonnegative]);;
let pow_int_inverse = prove(
`!p:A->A. !j:int. bijection p ==>
p pow_int --j = inverse(p pow_int j)`,
REPEAT GEN_TAC THEN DISCH_TAC THEN
DISJ_CASES_TAC(INT_ARITH `j:int < &0 \/ &0 <= j`) THENL
[ ASM_MESON_TAC[pow_int_inverse_negative]
; ASM_MESON_TAC[pow_int_inverse_nonnegative]
]);;
let pow_int_plus_lemma1 = prove(
`!p:A->A. bijection p ==> !j:int. j < &0 ==>
!k:int. p pow_int(k + --j) = (p pow_int --j) o (p pow_int k)`,
GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
ASSUME_TAC(ARITH_RULE `(j:int) < &0 ==> &0 <= --j`) THEN
ASM_MESON_TAC[pow_int_plus_nonnegative]);;
let pow_int_plus_lemma2 = prove(
`!p:A->A. !j:int. !k:int. bijection p /\ j < &0 ==>
p pow_int(k - j) = (p pow_int --j) o (p pow_int k)`,
REPEAT STRIP_TAC THEN
REWRITE_TAC[ARITH_RULE `(k:int)-(j:int) = k + --j`] THEN
ASM_MESON_TAC[pow_int_plus_lemma1]);;
let pow_int_plus_lemma3 = prove(
`!p:A->A. !j:int. !k:int. bijection p /\ j < &0 ==>
p pow_int(k-j) = inverse(p pow_int j) o (p pow_int k)`,
MESON_TAC[pow_int_plus_lemma2;pow_int_inverse;pow_int_bijection]);;
let pow_int_plus_lemma4 = prove(
`!p:A->A j:int k:int. bijection p /\ j < &0 ==>
(p pow_int j) o (p pow_int(k-j)) = p pow_int k`,
REPEAT STRIP_TAC THEN
ASSUME_TAC(SPECL[`p:A->A`;`j:int`;`k:int`]pow_int_plus_lemma3) THEN
ASSUME_TAC(SPECL[`p:A->A`;`j:int`]pow_int_bijection) THEN
ASSUME_TAC(ISPEC `(p:A->A) pow_int (j:int)` bijection_inverse_composition5)
THEN
ASM_MESON_TAC[o_ASSOC;I_O_ID]);;
let pow_int_plus_negative = prove(
`!p:A->A. bijection p ==> !j:int. j < &0 ==>
!k:int. (p pow_int j) o (p pow_int k) = p pow_int (k+j)`,
REPEAT STRIP_TAC THEN
ASSUME_TAC(SPECL[`p:A->A`;`j:int`;`(k:int)+j`]pow_int_plus_lemma4) THEN
ASSUME_TAC(ARITH_RULE `((k:int)+(j:int))-j=k`) THEN
ASM_MESON_TAC[]);;
let pow_int_plus_swap = prove(
`!p:A->A j:int k:int. bijection p ==>
p pow_int(k+j) = (p pow_int j) o (p pow_int k)`,
REPEAT STRIP_TAC THEN
DISJ_CASES_TAC(INT_ARITH `j:int < &0 \/ &0 <= j`) THENL
[ ASM_MESON_TAC[pow_int_plus_negative]
; ASM_MESON_TAC[pow_int_plus_nonnegative]
]);;
let pow_int_plus = prove(
`!p:A->A j:int k:int. bijection p ==>
p pow_int(j+k) = (p pow_int j) o (p pow_int k)`,
REPEAT STRIP_TAC THEN
ASSUME_TAC(ARITH_RULE `(k:int)+(j:int)=j+k`) THEN
ASM_MESON_TAC[pow_int_plus_swap]);;
let pow_int_plus_eval = prove(
`!p:A->A j:int k:int x. bijection p ==>
(p pow_int(j+k))x = (p pow_int j)((p pow_int k)x)`,
MESON_TAC[pow_int_plus;o_THM]);;
(* ----- cycle basics *)
let cycle_contains_start = prove(
`!p:A->A x. x IN cycle p x`,
REPEAT GEN_TAC THEN
REWRITE_TAC[cycle;IN_ELIM_THM] THEN
EXISTS_TAC `&0:int` THEN
REWRITE_TAC[pow_int_0;I_THM]);;
let cycle_lemma1 = prove(
`!p:A->A x y k. bijection p /\ y = (p pow_int k) (p x) ==>
y = (p pow_int (k + &1)) x`,
REPEAT STRIP_TAC THEN
ASM_SIMP_TAC[pow_int_plus_eval;pow_int_1]);;
let cycle_lemma2 = prove(
`!p:A->A x y k. bijection p /\ y = (p pow_int k) (p x) ==>
y IN cycle p x`,
REPEAT STRIP_TAC THEN
REWRITE_TAC[cycle;IN_ELIM_THM] THEN
EXISTS_TAC `(k:int) + &1` THEN
ASM_MESON_TAC[cycle_lemma1]);;
let cycle_lemma3 = prove(
`!p:A->A x y. y IN cycle p x ==> ?k:int. y = (p pow_int k)(x)`,
REWRITE_TAC[cycle;IN_ELIM_THM]);;
let cycle_lemma4 = prove(
`!p:A->A x y k. bijection p /\ y = (p pow_int k) x ==>
y = (p pow_int (k - &1)) (p x)`,
REPEAT STRIP_TAC THEN
ASSUME_TAC(INT_ARITH `(k:int) = (k - &1) + &1`) THEN
ASM_MESON_TAC[pow_int_plus_eval;pow_int_1]);;
let cycle_lemma5 = prove(
`!p:A->A x y k. bijection p /\ y = (p pow_int k) x ==>
y IN cycle p (p x)`,
REPEAT STRIP_TAC THEN
REWRITE_TAC[cycle;IN_ELIM_THM] THEN
EXISTS_TAC `(k:int) - &1` THEN
ASM_MESON_TAC[cycle_lemma4]);;
let cycle_shift_forward = prove(
`!p:A->A x y. bijection p ==> y IN cycle p (p x) ==> y IN cycle p x`,
REPEAT STRIP_TAC THEN
MATCH_MP_TAC cycle_lemma2 THEN
ASM_MESON_TAC[cycle_lemma3]);;
let cycle_shift_backward = prove(
`!p:A->A x y. bijection p ==> y IN cycle p x ==> y IN cycle p (p x)`,
REPEAT STRIP_TAC THEN
MATCH_MP_TAC cycle_lemma5 THEN
ASM_MESON_TAC[cycle_lemma3]);;
let cycle_shift = prove(
`!p:A->A x. bijection p ==> cycle p (p x) = cycle p x`,
MESON_TAC[cycle_shift_backward;cycle_shift_forward;EXTENSION]);;
let cycle_ifpow = prove(
`!p:A->A x y k. y = (p pow_int k) x ==> y IN cycle p x`,
REWRITE_TAC[cycle;IN_ELIM_THM] THEN
MESON_TAC[]);;
let cycle_aspow = prove(
`!p:A->A x y. y IN cycle p x ==> ?k. y = (p pow_int k) x`,
REWRITE_TAC[cycle;IN_ELIM_THM]);;
let cyclemin_in_cycle = prove(
`!p x. cyclemin p x IN cycle p x`,
REPEAT GEN_TAC THEN
REWRITE_TAC[IN] THEN
REWRITE_TAC[cyclemin] THEN
MATCH_MP_TAC(prove(`!P. (?n. P n) ==> P((minimal) P)`,MESON_TAC[MINIMAL]))
THEN
ASSUME_TAC(ISPECL[`p:num->num`;`x:num`]cycle_contains_start) THEN
ASM_MESON_TAC[IN]);;
let cyclemin_le = prove(
`!p x. cyclemin p x <= x`,
REPEAT GEN_TAC THEN
REWRITE_TAC[cyclemin] THEN
MATCH_MP_TAC MINIMAL_UBOUND THEN
MESON_TAC[cycle_contains_start;IN]);;
let cyclemin_aspow = prove(
`!p x. ?k. cyclemin p x = (p pow_int k) x`,
REPEAT STRIP_TAC THEN
MATCH_MP_TAC cycle_aspow THEN
ASM_MESON_TAC[cyclemin_in_cycle]);;
(* ----- vanishesifonbothsidesof basics *)
let vanishesifonbothsidesof_eval = prove(
`!p:A->A q:A->A. p vanishesifonbothsidesof q <=> !x. p(q(p x)) = q x`,
REWRITE_TAC[vanishesifonbothsidesof] THEN
MESON_TAC[o_DEF;EQ_EXT]);;
let vanishesifonbothsidesof_pow_num_eval = prove(
`!p:A->A q:A->A. p vanishesifonbothsidesof q ==>
!n. !x. (p pow_num n)(q((p pow_num n)x)) = q x`,
REWRITE_TAC[vanishesifonbothsidesof_eval] THEN
REPEAT GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THENL
[
REWRITE_TAC[pow_num_0;I_DEF]
;
REWRITE_TAC[suc_isadd1] THEN
ASSUME_TAC(SPECL[`n:num`;`p:A->A`]pow_num_plus1_eval) THEN
ASSUME_TAC(SPECL[`n:num`;`p:A->A`]pow_num_plus1_right_eval) THEN
ASM_MESON_TAC[]
]);;
let vanishesifonbothsidesof_pow_num_lemma = prove(
`!p:A->A q:A->A. p vanishesifonbothsidesof q ==>
!n. (p pow_num n) o q o (p pow_num n) = q`,
REPEAT GEN_TAC THEN DISCH_TAC THEN
ASM_MESON_TAC[vanishesifonbothsidesof_pow_num_eval;o_DEF;EQ_EXT]);;
let vanishesifonbothsidesof_pow_num = prove(
`!p:A->A q:A->A. p vanishesifonbothsidesof q ==>
!n. (p pow_num n) vanishesifonbothsidesof q`,
MESON_TAC[vanishesifonbothsidesof_pow_num_lemma;vanishesifonbothsidesof]);;
let vanishesifonbothsidesof_inverse = prove(
`!p:A->A. bijection p ==> !q:A->A. p vanishesifonbothsidesof q ==>
inverse p vanishesifonbothsidesof q`,
REWRITE_TAC[vanishesifonbothsidesof_eval] THEN
GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
ASSUME_TAC(ISPEC `p:A->A` bijection_inverse_composition1) THEN
ASSUME_TAC(ISPEC `p:A->A` bijection_inverse_composition2) THEN
ASM_MESON_TAC[]);;
let vanishesifonbothsidesof_pow_int = prove(
`!p:A->A. bijection p ==> !q:A->A. p vanishesifonbothsidesof q
==> !k:int. p pow_int k vanishesifonbothsidesof q`,
REWRITE_TAC[pow_int] THEN GEN_TAC THEN
DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN
ASSUME_TAC(INT_ARITH `k < &0 ==> ~(&0 <= k)`) THEN
ASM_MESON_TAC[vanishesifonbothsidesof_pow_num;vanishesifonbothsidesof_inverse]);;
(* ----- XbackXforth basics *)
let permutesrange_inverts_1 = prove(
`!p n. p permutesrange n ==> inverse p fixesge n`,
REWRITE_TAC[permutesrange;bijection;surjection;injection;
inverse;fixesge] THEN MESON_TAC[]);;
let permutesrange_inverts_2 = prove(
`!p n. bijection p /\ (!x. x >= n ==> p x = x) ==> !x. x >= n ==> inverse p x
= x`,
MESON_TAC[permutesrange;permutesrange_inverts_1;fixesge]);;
let XbackXforth_fixesge = prove(
`!p b. p permutesrange(2*b) ==> XbackXforth p fixesge(2*b)`,
REWRITE_TAC[XbackXforth;permutesrange;fixesge;o_THM]
THEN REPEAT GEN_TAC THEN DISCH_TAC THEN
SUBGOAL_THEN `!x. x >= 2*b ==> xor1 x >= 2*b` ASSUME_TAC
THENL [MESON_TAC[xor1_geeven];ALL_TAC] THEN
SUBGOAL_THEN `!x. x >= 2*b ==> p(xor1 x) = xor1 x` ASSUME_TAC
THENL [ASM_MESON_TAC[];ALL_TAC] THEN
SUBGOAL_THEN `!x. x >= 2*b ==> xor1(p(xor1 x)) = x` ASSUME_TAC
THENL [ASM_MESON_TAC[xor1xor1];ALL_TAC] THEN
SUBGOAL_THEN `!x. x >= 2*b ==> inverse p(xor1(p(xor1 x))) = x` ASSUME_TAC
THENL [ASM_MESON_TAC[permutesrange_inverts_2];ALL_TAC]
THEN ASM_MESON_TAC[]);;
let XbackXforth_bijection = prove(
`!p. bijection p ==> bijection(XbackXforth p)`,
REWRITE_TAC[XbackXforth] THEN
MESON_TAC[xor1_involution2;bijection_ifinvolution;
bijection_inverseisbijection;bijection_composes]);;
let XbackXforth_permutesrange = prove(
`!p b. p permutesrange(2*b) ==> XbackXforth p permutesrange(2*b)`,
MESON_TAC[XbackXforth_bijection;XbackXforth_fixesge;permutesrange]);;
let XbackXforth_lemmapiqi1 = prove(
`!i:A->A p:A->A q:A->A.
(!x. (i o i)x = x) /\ (!x. (q o p)x = x) /\ (!x. (p o q)x = x) ==>
!x. ((p o i o q o i) o i o (p o i o q o i))x = i x`,
REWRITE_TAC[o_DEF] THEN MESON_TAC[]);;
let XbackXforth_lemmapiqi2 = prove(
`!i:A->A p:A->A q:A->A. i o i = I /\ q o p = I /\ p o q = I ==>
(!x. (i o i)x = x) /\ (!x. (q o p)x = x) /\ (!x. (p o q)x = x)`,
REWRITE_TAC[I_DEF;o_DEF] THEN MESON_TAC[]);;
let XbackXforth_lemmapiqi3 = prove(
`!i:A->A p:A->A q:A->A. i o i = I /\ q o p = I /\ p o q = I ==>
!x. ((p o i o q o i) o i o (p o i o q o i))x = i x`,
REPEAT GEN_TAC THEN DISCH_TAC THEN
ASSUME_TAC(SPECL[`i:A->A`;`p:A->A`;`q:A->A`]XbackXforth_lemmapiqi1) THEN
ASSUME_TAC(SPECL[`i:A->A`;`p:A->A`;`q:A->A`]XbackXforth_lemmapiqi2) THEN
ASM_MESON_TAC[]);;
let XbackXforth_lemmapiqi4 = prove(
`!i:A->A p:A->A q:A->A. i o i = I /\ q o p = I /\ p o q = I ==>
(p o i o q o i) o i o (p o i o q o i) = i`,
ASM_MESON_TAC[XbackXforth_lemmapiqi3;EQ_EXT]);;
let XbackXforth_lemmapiqi5 = prove(
`!i:A->A p:A->A q:A->A. i o i = I /\ q o p = I /\ p o q = I ==>
p o i o q o i vanishesifonbothsidesof i`,
ASM_MESON_TAC[XbackXforth_lemmapiqi4;vanishesifonbothsidesof]);;
let XbackXforth_lemmapiqi6 = prove(
`!i:A->A. i o i = I ==> !p:A->A. bijection p ==>
p o i o inverse p o i vanishesifonbothsidesof i`,
ASM_MESON_TAC[XbackXforth_lemmapiqi5;
bijection_inverse_composition5;
bijection_inverse_composition6]);;
let XbackXforth_vanishesifonbothsidesof_xor1 = prove(
`!p. bijection p ==> XbackXforth p vanishesifonbothsidesof xor1`,
REWRITE_TAC[XbackXforth] THEN
MESON_TAC[xor1_involution;XbackXforth_lemmapiqi6]);;
let XbackXforth_power_vanishesifonbothsidesof_xor1 = prove(
`!p k:int. bijection p ==> (XbackXforth p pow_int k) vanishesifonbothsidesof
xor1`,
MESON_TAC[XbackXforth_bijection;
XbackXforth_vanishesifonbothsidesof_xor1;
vanishesifonbothsidesof_pow_int]);;
let XbackXforth_power_vanishesifonbothsidesof_xor1_eval = prove(
`!p k:int x. bijection p ==> (XbackXforth p pow_int k) (xor1((XbackXforth p
pow_int k) x)) = xor1 x`,
REPEAT GEN_TAC THEN DISCH_TAC THEN
ASSUME_TAC(SPECL[`p:num->num`;`k:int`]XbackXforth_power_vanishesifonbothsidesof_xor1)
THEN
ASM_MESON_TAC[vanishesifonbothsidesof;o_THM]);;
let XbackXforth_even_avoids_xor1 = prove(
`!p k:int x. bijection p ==>
~((XbackXforth p pow_int (k+k)) x = xor1 x)`,
REPEAT GEN_TAC THEN DISCH_TAC THEN
ASSUME_TAC(SPECL[`p:num->num`;`k:int`;`x:num`]XbackXforth_power_vanishesifonbothsidesof_xor1_eval)
THEN
ASSUME_TAC(SPEC `p:num->num` XbackXforth_bijection) THEN
ASSUME_TAC(ISPECL[`XbackXforth p:num->num`;`k:int`;`k:int`]pow_int_plus) THEN
ASSUME_TAC(ISPECL[
`XbackXforth p:num->num`;
`k:int`;
`(XbackXforth (p:num->num) pow_int (k:int))(x:num)`;
`xor1((XbackXforth (p:num->num) pow_int (k:int))(x:num))`
]pow_int_cancel) THEN
ASSUME_TAC(SPEC
`(XbackXforth (p:num->num) pow_int (k:int)) (x:num)`
xor1_distinct) THEN
ASM_MESON_TAC[o_THM]);;
let XbackXforth_1_avoids_xor1 = prove(
`!p x. bijection p ==> ~(XbackXforth p x = xor1 x)`,
REWRITE_TAC[XbackXforth;o_DEF] THEN
MESON_TAC[xor1_distinct;bijection_inverse_composition2]);;
let XbackXforth_odd_avoids_xor1 = prove(
`!p k:int x. bijection p ==>
~((XbackXforth p pow_int ((k + &1) + k)) x = xor1 x)`,
REPEAT GEN_TAC THEN DISCH_TAC THEN
ASSUME_TAC(SPEC `p:num->num` XbackXforth_bijection) THEN
ASM_SIMP_TAC[ISPECL[`XbackXforth p:num->num`;`(k:int)+
&1`;`k:int`]pow_int_plus] THEN
ASM_SIMP_TAC[o_THM] THEN
ASM_SIMP_TAC[ISPECL[`XbackXforth p:num->num`;`k:int`;`&1:int`]pow_int_plus]
THEN
ASM_SIMP_TAC[o_THM] THEN
ASM_SIMP_TAC[ISPECL[`XbackXforth p:num->num`]pow_int_1] THEN
ASSUME_TAC(SPECL[`p:num->num`;`k:int`;`x:num`]XbackXforth_power_vanishesifonbothsidesof_xor1_eval)
THEN
ASSUME_TAC(ISPECL[`XbackXforth p:num->num`;`k:int`]pow_int_bijection) THEN
ASSUME_TAC(ISPECL[
`XbackXforth p:num->num`;
`k:int`;
`(XbackXforth (p:num->num))((XbackXforth p pow_int (k:int))(x:num))`;
`xor1((XbackXforth (p:num->num) pow_int (k:int))(x:num))`
]pow_int_cancel) THEN
ASSUME_TAC(SPECL
[`p:num->num`;`(XbackXforth (p:num->num) pow_int (k:int)) (x:num)`]
XbackXforth_1_avoids_xor1) THEN
ASM_MESON_TAC[o_THM]);;
let XbackXforth_pow_avoids_xor1 = prove(
`!p n:int x. bijection p ==>
~((XbackXforth p pow_int n) x = xor1 x)`,
REPEAT GEN_TAC THEN DISCH_TAC THEN
ASSUME_TAC(SPECL[`n:int`;`&2:int`]INT_DIVISION_SIMP) THEN
DISJ_CASES_TAC(SPEC `n:int` INT_REM_2_CASES) THENL
[
ASSUME_TAC(INT_ARITH `(n:int) div &2 * &2 + &0 = n div &2 + n div &2`) THEN
ASM_MESON_TAC[XbackXforth_even_avoids_xor1]
;
ASSUME_TAC(INT_ARITH `(n:int) div &2 * &2 + &1 = (n div &2 + &1) + n div
&2`) THEN
ASM_MESON_TAC[XbackXforth_odd_avoids_xor1]
]);;
let XbackXforth_powpow_avoids_xor1 = prove(
`!p n:int m:int x. bijection p ==>
~((XbackXforth p pow_int n) x =
xor1 ((XbackXforth p pow_int m) x))`,
REPEAT GEN_TAC THEN DISCH_TAC THEN
ASSUME_TAC(SPEC `p:num->num` XbackXforth_bijection) THEN
ASSUME_TAC(ISPECL[`XbackXforth p:num->num`;`m:int`]pow_int_bijection) THEN
ASSUME_TAC(ISPECL[`XbackXforth
p:num->num`;`(n:int)-(m:int)`;`m:int`]pow_int_plus) THEN
ASSUME_TAC(INT_ARITH `((n:int)-(m:int))+m = n`) THEN
ASSUME_TAC(SPECL[`p:num->num`;
`(n:int)-(m:int)`;
`((XbackXforth (p:num->num) pow_int (m:int)) x)`
]XbackXforth_pow_avoids_xor1) THEN
ASM_MESON_TAC[o_THM]);;
let XbackXforth_powpow2_avoids_xor1 = prove(
`!p n:int m:int x. bijection p ==>
~((XbackXforth p pow_int n) x =
(XbackXforth p pow_int m) (xor1 x))`,
REPEAT GEN_TAC THEN DISCH_TAC THEN
ASSUME_TAC(SPEC `p:num->num` XbackXforth_bijection) THEN
ASSUME_TAC(ISPECL[`XbackXforth p:num->num`;`m:int`]pow_int_bijection) THEN
ASSUME_TAC(ISPECL[`XbackXforth
p:num->num`;`m:int`;`(n:int)-(m:int)`]pow_int_plus) THEN
ASSUME_TAC(INT_ARITH `m+((n:int)-(m:int)) = n`) THEN
ASSUME_TAC(ISPECL[
`XbackXforth p:num->num`;
`m:int`;
`(XbackXforth (p:num->num) pow_int ((n:int)-(m:int)))x`;
`xor1 x:num`
]pow_int_cancel) THEN
ASSUME_TAC(SPECL[`p:num->num`;
`(n:int)-(m:int)`;
`x:num`
]XbackXforth_pow_avoids_xor1) THEN
ASM_MESON_TAC[o_THM]);;
let XbackXforth_pow_xor1 = prove(
`!p k:int x. bijection p ==>
xor1((XbackXforth p pow_int k) x) =
(XbackXforth p pow_int --k)(xor1 x)`,
REPEAT STRIP_TAC THEN
ASSUME_TAC(ISPECL[`p:num->num`]XbackXforth_bijection) THEN
ASM_SIMP_TAC[ISPECL[`XbackXforth p:num->num`;`k:int`]pow_int_inverse] THEN
ASSUME_TAC(ISPECL[`XbackXforth p:num->num`;`k:int`]pow_int_bijection) THEN
ASSUME_TAC(SPECL[`p:num->num`;`k:int`;`x:num`]
XbackXforth_power_vanishesifonbothsidesof_xor1_eval) THEN
ASSUME_TAC(ISPECL[`XbackXforth (p:num->num) pow_int (k:int)`;
`xor1 x:num`]bijection_inverse_composition1)
THEN
ASSUME_TAC(ISPECL[
`XbackXforth p:num->num`;
`k:int`;
`inverse(XbackXforth (p:num->num) pow_int (k:int))(xor1(x:num))`;
`xor1((XbackXforth (p:num->num) pow_int (k:int))(x:num))`
]pow_int_cancel) THEN
ASM_MESON_TAC[]);;
let XbackXforth_pow_xor1_incycle = prove(
`!p k:int x. bijection p ==>
xor1((XbackXforth p pow_int k) x) IN
cycle (XbackXforth p) (xor1 x)`,
REPEAT STRIP_TAC THEN
MATCH_MP_TAC(ISPECL[`XbackXforth p`;
`xor1 x`;
`xor1((XbackXforth p pow_int k) x)`;
`--k:int`
]cycle_ifpow) THEN
ASM_MESON_TAC[XbackXforth_pow_xor1]);;
let XbackXforth_pow_xor1_gecyclemin = prove(
`!p x k:int. bijection p ==>
cyclemin (XbackXforth p) (xor1 x) <=
xor1((XbackXforth p pow_int k) x)`,
REPEAT STRIP_TAC THEN
REWRITE_TAC[cyclemin] THEN
MATCH_MP_TAC MINIMAL_UBOUND THEN
ASM_MESON_TAC[XbackXforth_pow_xor1_incycle;IN]);;
let XbackXforth_cyclemin_xor1_gecyclemin = prove(
`!p x. bijection p ==>
cyclemin (XbackXforth p) (xor1 x) <=
xor1(cyclemin (XbackXforth p) x)`,
REPEAT STRIP_TAC THEN
ASSUME_TAC(SPECL[`XbackXforth p:num->num`;`x:num`]cyclemin_aspow) THEN
ASSUME_TAC(SPECL[`p:num->num`;`x:num`]XbackXforth_pow_xor1_gecyclemin)
THEN
ASM_MESON_TAC[]);;
let XbackXforth_cyclemin_xor1_gecyclemin_reverse = prove(
`!p x. bijection p ==>
cyclemin (XbackXforth p) x <=
xor1(cyclemin (XbackXforth p) (xor1 x))`,
MESON_TAC[xor1xor1;XbackXforth_cyclemin_xor1_gecyclemin]);;
let XbackXforth_cyclemin_xor1_ne = prove(
`!p x k:int. bijection p ==>
~(cyclemin(XbackXforth p) (xor1 x) = cyclemin(XbackXforth p) x)`,
REPEAT GEN_TAC THEN DISCH_TAC THEN
ASM_MESON_TAC[XbackXforth_powpow2_avoids_xor1;cyclemin_aspow]);;
let XbackXforth_cyclemin_xor1 = prove(
`!p x. bijection p ==>
cyclemin (XbackXforth p) (xor1 x) =
xor1(cyclemin (XbackXforth p) x)`,
MESON_TAC[xor1_lemma108;
XbackXforth_cyclemin_xor1_ne;
XbackXforth_cyclemin_xor1_gecyclemin_reverse;
XbackXforth_cyclemin_xor1_gecyclemin]);;
signature.asc
Description: PGP signature
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
