Example (15)

昨日のsimplifyです．a+bの符号は:int上の処理に含めました．(* *)内はMESON任せの方法で時間が掛かります．

needs "Complex/make.ml";;

let lemma04 = prove
(`!a b:real. (?x. ~( x = Cx(&1) ) /\ x pow 3 = Cx(&1) /\ (Cx(a)*x+Cx(b))*(Cx(a)*x pow 2+Cx(b))*(Cx(a)*x pow 3+Cx(b)) = Cx(&1) ) <=> &0 <= a pow 2 -a*b+ b pow 2 /\ (a pow 2-a*b+b pow 2)*(a+b) = &1`,
let lemma01 = FULL_COMPLEX_QUELIM_CONV `?x. ~( x = Cx(&1) ) /\ x pow 3 = Cx(&1)` in
let lemma02 = COMPLEX_FIELD `~( x = Cx(&1) ) /\ x pow 3 = Cx(&1) ==> (a*x+b)*(a*x pow 2+b)*(a*x pow 3+b) = (a pow 2 -a*b + b pow 2)*(a+b)` in
let lemma03 = MESON[REAL_SOS `&0 <= a pow 2 -a*b+ b pow 2`;]`&0 <= a pow 2-a*b+b pow 2 /\ (a pow 2-a*b+b pow 2)*(a+b) = &1 <=> (a pow 2-a*b+b pow 2)*(a+b)= &1` in
REPEAT STRIP_TAC THEN
REWRITE_TAC [lemma03; GSYM CX_INJ; CX_POW; CX_MUL; CX_SUB; CX_ADD] THEN
MESON_TAC [lemma01; lemma02]);;
let lemma04_int = INT_OF_REAL_THM lemma04;;
(*
let lemma05 = MESON[
INT_ARITH`&0<= &1:int /\ &1* &1= &1:int`;
INT_ARITH`&0<=x:int ==> &0=x \/ &1=x \/ &2<=x`;
INT_RING`&0=x:int ==> ~(x*y= &1)`;
INT_ARITH`!y:int. y<= &0 \/ &1<=y`;
INT_OF_REAL_THM(REAL_SOS`y<= &0 \/ &1<=y ==> &2<=x ==> ~(x*y= &1)`);
INT_OF_REAL_THM(REAL_SOS`&1=x /\ x*y= &1 ==> &1=y`);
]`!x y:int. &0<=x /\ x*y= &1 <=> x= &1 /\ y= &1`;;
*)
let lemma05_01 = INT_OF_REAL_THM (REAL_SOS`&0<=x /\ x*y= &1 ==> &0<=y`);;
let lemma05_02 = prove
(`!x y:int. &0<=x /\ &0<=y /\ x*y= &1 <=> x= &1 /\ y= &1`,
(REPEAT GEN_TAC THEN EQ_TAC) THENL
[
(STRIP_TAC THEN FIRST_X_ASSUM MP_TAC) THEN
(SUBST1_TAC (UNDISCH(SPEC`x:int`(GSYM INT_OF_NUM_OF_INT)))) THEN
(SUBST1_TAC (UNDISCH(SPEC`y:int`(GSYM INT_OF_NUM_OF_INT)))) THEN
(REWRITE_TAC[INT_OF_NUM_MUL; INT_OF_NUM_EQ; MULT_EQ_1]) ;
(SIMP_TAC[INT_LE_01; INT_MUL_LID])]);;
let lemma05 = MESON[lemma05_01; lemma05_02]`!x y:int. &0<=x /\ x*y= &1 <=> x= &1 /\ y= &1`;;

let lemma06 = INT_RING`a pow 2 - a * b + b pow 2 = &1 /\ a + b = &1 <=> a= &0 /\ b= &1 \/ a= &1 /\ b= &0:int`;;
let thm00 = GEN_ALL( TRANS (SPEC_ALL lemma04_int) (TRANS (SPECL[`(a:int) pow 2 -a*b+ b pow 2`;`a+b:int`]lemma05) lemma06) );;
prioritize_num();;