Example (14)

　今回は，虚数と整数とが混在する証明です．変数はintとし，&，real_of_int，num_of_intを介して各ドメインの性質を適用します．なお，SOS系の利用はできるだけ控えました．

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 /\ &0 <= a+b /\ (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<=x /\ x*y= &1 ==> &0<=y)`;]`&0 <= a pow 2-a*b+b pow 2 /\ &0 <= a+b /\ (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 = 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
MP_TAC (SPEC`x:int`(GSYM INT_OF_NUM_OF_INT)) THEN ASM_SIMP_TAC THEN STRIP_TAC THEN FIRST_X_ASSUM SUBST1_TAC THEN
MP_TAC (SPEC`y:int`(GSYM INT_OF_NUM_OF_INT)) THEN ASM_SIMP_TAC THEN STRIP_TAC THEN FIRST_X_ASSUM SUBST1_TAC THEN
REWRITE_TAC [INT_OF_NUM_MUL; INT_OF_NUM_EQ; MULT_EQ_1];
SIMP_TAC [INT_LE_01; INT_MUL_LID] ]);;
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) );;