方程式の解き方

前回の lem03 にあるように，REAL/COMPLEX_FIELD が知っているのは有理式までなので，それ以外のものを扱うには，必要な性質を前件として与えて証明させた後，SIMP,REWRITEなどにより前件を消去します．

SIMP_RULE[COMPLEX_POW_II_2;
          GSYM CX_POW; SQRT_POW_2; ARITH_RULE `&0 <= &3`;
          GSYM CX_DIV; GSYM CX_MUL; GSYM REAL_NEG_MINUS1; GSYM COMPLEX_TRAD;]
 (COMPLEX_FIELD `Cx(sqrt(&3)) pow 2 = Cx(&3) /\ ii pow 2 = --Cx(&1) ==>
                 (c pow 2 - c + Cx(&1) = Cx(&0)
                 <=> c = Cx(&1/ &2) + ii * Cx(sqrt (&3))/ Cx(&2)
                  \/ c = Cx(&1/ &2) + ii * Cx(-- &1) * Cx(sqrt (&3))/ Cx(&2))`) ;;

対話的に書くと．．．

g `c pow 2 - c + Cx (&1) = Cx (&0) <=>
c = complex (&1 / &2,sqrt (&3) / &2) \/
c = complex (&1 / &2,--(sqrt (&3) / &2))` ;;
e( ONCE_REWRITE_TAC [REAL_NEG_MINUS1] );;
e( REWRITE_TAC [COMPLEX_TRAD; CX_MUL; CX_DIV] );;
e( MP_TAC COMPLEX_POW_II_2 );;
e( MP_TAC (SIMP_RULE[SQRT_POW_2; ARITH_RULE `&0 <= &3`] (SPECL[`sqrt (&3)`; `2`]CX_POW)) );;
e( CONV_TAC COMPLEX_FIELD );;

g `c pow 2 - c + Cx (&1) = Cx (&0) <=>
c = complex (&1 / &2,sqrt (&3) / &2) \/
c = complex (&1 / &2,--(sqrt (&3) / &2))` ;;
e( ONCE_REWRITE_TAC [REAL_NEG_MINUS1] );;
e( REWRITE_TAC [COMPLEX_TRAD; CX_MUL; CX_DIV] );;
e( MP_TAC COMPLEX_POW_II_2 );;
e( SUBGOAL_THEN `Cx(sqrt(&3)) pow 2 = Cx(&3)` MP_TAC );;
e( SIMP_TAC[SQRT_POW_2; ARITH_RULE `&0 <= &3`; GSYM CX_POW] );;
e( CONV_TAC COMPLEX_FIELD );;

のようにやや譲歩せねばなりません．