g `!x. asn (sin x) = pi / &2 - abs (pi / &2 - (x - &2 * pi * floor ((x + pi / &2) / (&2 * pi))))` ;;
e( GEN_TAC );;
e( SUBGOAL_THEN `asn (sin x) = asn (sin (pi / &2 - abs (pi / &2 - (x - &2 * pi * floor ( (x + pi / &2) / (&2 * pi) ) ) )) ) /\ -- (pi / &2) <= pi / &2 - abs (pi / &2 - (x - &2 * pi * floor ( (x + pi / &2) / (&2 * pi) ) ) ) /\ pi / &2 - abs (pi / &2 - (x - &2 * pi * floor ( (x + pi / &2) / (&2 * pi) ) ) ) <= pi / &2` MP_TAC THEN STRIP_TAC );;
e( SIMP_TAC [GSYM COS_SIN;COS_ABS;GSYM SIN_COS;REAL_ARITH`x - &2 * pi * y = x + (&2 * pi) * (-- y)`;SIN_ADD;SIN_INTEGER_2PI;COS_INTEGER_2PI;FLOOR;INTEGER_NEG;REAL_MUL_RID;REAL_MUL_RZERO;REAL_ADD_RID] );;
e( STRIP_TAC );;
e( SIMP_TAC [REAL_ARITH`--(pi / &2) <= pi / &2 - abs (pi / &2 - (x - &2 * pi * f)) <=> pi * f <= x / &2 + pi / &4 /\ x / &2 + pi / &4 <= pi * (f + &1)`;SIMP_RULE [PI_POS] (REAL_FIELD`&0 < pi ==> x / &2 + pi / &4 = pi * (x / (&2 * pi) + &1 / &4)`);SIMP_RULE [PI_POS] (REAL_FIELD`&0 < pi ==> (x + pi / &2) / (&2 * pi) = x / (&2 * pi) + &1 / &4`);PI_POS;REAL_LE_LMUL_EQ]);;
e( SIMP_TAC [FLOOR;REAL_LT_IMP_LE] );;
e( REAL_ARITH_TAC );;
e( ASM_SIMP_TAC [ASN_SIN] );;
top_thm () ;;
# g `!x. asn (sin x) = pi / &2 - abs (pi / &2 - (x - &2 * pi * floor ( (x + pi / &2) / (&2 * pi) ) ) )` ;;
val it : goalstack = 1 subgoal (1 total)
`!x. asn (sin x) =
pi / &2 -
abs (pi / &2 - (x - &2 * pi * floor ((x + pi / &2) / (&2 * pi))))`
# e( GEN_TAC );;
val it : goalstack = 1 subgoal (1 total)
`asn (sin x) =
pi / &2 - abs (pi / &2 - (x - &2 * pi * floor ((x + pi / &2) / (&2 * pi))))`
# e( SUBGOAL_THEN `asn (sin x) = asn (sin (pi / &2 - abs (pi / &2 - (x - &2 * pi * floor ( (x + pi / &2) / (&2 * pi) ) ) )) ) /\ -- (pi / &2) <= pi / &2 - abs (pi / &2 - (x - &2 * pi * floor ( (x + pi / &2) / (&2 * pi) ) ) ) /\ pi / &2 - abs (pi / &2 - (x - &2 * pi * floor ( (x + pi / &2) / (&2 * pi) ) ) ) <= pi / &2` MP_TAC THEN STRIP_TAC );;
val it : goalstack = 3 subgoals (3 total)
0 [`asn (sin x) =
asn
(sin
(pi / &2 -
abs (pi / &2 - (x - &2 * pi * floor ((x + pi / &2) / (&2 * pi))))))`]
1 [`--(pi / &2) <=
pi / &2 -
abs (pi / &2 - (x - &2 * pi * floor ((x + pi / &2) / (&2 * pi))))`]
2 [`pi / &2 -
abs (pi / &2 - (x - &2 * pi * floor ((x + pi / &2) / (&2 * pi)))) <=
pi / &2`]
`asn (sin x) =
pi / &2 - abs (pi / &2 - (x - &2 * pi * floor ((x + pi / &2) / (&2 * pi))))`
`--(pi / &2) <=
pi / &2 - abs (pi / &2 - (x - &2 * pi * floor ((x + pi / &2) / (&2 * pi)))) /\
pi / &2 - abs (pi / &2 - (x - &2 * pi * floor ((x + pi / &2) / (&2 * pi)))) <=
pi / &2`
`asn (sin x) =
asn
(sin
(pi / &2 -
abs (pi / &2 - (x - &2 * pi * floor ((x + pi / &2) / (&2 * pi))))))`
# e( SIMP_TAC [GSYM COS_SIN;COS_ABS;GSYM SIN_COS;REAL_ARITH`x - &2 * pi * y = x + (&2 * pi) * (-- y)`;SIN_ADD;SIN_INTEGER_2PI;COS_INTEGER_2PI;FLOOR;INTEGER_NEG;REAL_MUL_RID;REAL_MUL_RZERO;REAL_ADD_RID] );;
val it : goalstack = 1 subgoal (2 total)
`--(pi / &2) <=
pi / &2 - abs (pi / &2 - (x - &2 * pi * floor ((x + pi / &2) / (&2 * pi)))) /\
pi / &2 - abs (pi / &2 - (x - &2 * pi * floor ((x + pi / &2) / (&2 * pi)))) <=
pi / &2`
# e( STRIP_TAC );;
val it : goalstack = 2 subgoals (3 total)
`pi / &2 - abs (pi / &2 - (x - &2 * pi * floor ((x + pi / &2) / (&2 * pi)))) <=
pi / &2`
`--(pi / &2) <=
pi / &2 - abs (pi / &2 - (x - &2 * pi * floor ((x + pi / &2) / (&2 * pi))))`
# e( SIMP_TAC [REAL_ARITH`--(pi / &2) <= pi / &2 - abs (pi / &2 - (x - &2 * pi * f)) <=> pi * f <= x / &2 + pi / &4 /\ x / &2 + pi / &4 <= pi * (f + &1)`;SIMP_RULE [PI_POS] (REAL_FIELD`&0 < pi ==> x / &2 + pi / &4 = pi * (x / (&2 * pi) + &1 / &4)`);SIMP_RULE [PI_POS] (REAL_FIELD`&0 < pi ==> (x + pi / &2) / (&2 * pi) = x / (&2 * pi) + &1 / &4`);PI_POS;REAL_LE_LMUL_EQ]);;
2 basis elements and 0 critical pairs
3 basis elements and 1 critical pairs
3 basis elements and 0 critical pairs
2 basis elements and 0 critical pairs
3 basis elements and 1 critical pairs
3 basis elements and 0 critical pairs
val it : goalstack = 1 subgoal (3 total)
`floor (x / (&2 * pi) + &1 / &4) <= x / (&2 * pi) + &1 / &4 /\
x / (&2 * pi) + &1 / &4 <= floor (x / (&2 * pi) + &1 / &4) + &1`
# e( SIMP_TAC [FLOOR;REAL_LT_IMP_LE] );;
val it : goalstack = 1 subgoal (2 total)
`pi / &2 - abs (pi / &2 - (x - &2 * pi * floor ((x + pi / &2) / (&2 * pi)))) <=
pi / &2`
# e( REAL_ARITH_TAC );;
val it : goalstack = 1 subgoal (1 total)
0 [`asn (sin x) =
asn
(sin
(pi / &2 -
abs (pi / &2 - (x - &2 * pi * floor ((x + pi / &2) / (&2 * pi))))))`]
1 [`--(pi / &2) <=
pi / &2 -
abs (pi / &2 - (x - &2 * pi * floor ((x + pi / &2) / (&2 * pi))))`]
2 [`pi / &2 -
abs (pi / &2 - (x - &2 * pi * floor ((x + pi / &2) / (&2 * pi)))) <=
pi / &2`]
`asn (sin x) =
pi / &2 - abs (pi / &2 - (x - &2 * pi * floor ((x + pi / &2) / (&2 * pi))))`
# e( ASM_SIMP_TAC [ASN_SIN] );;
val it : goalstack = No subgoals
# top_thm () ;;
val it : thm =
|- !x. asn (sin x) =
pi / &2 -
abs (pi / &2 - (x - &2 * pi * floor ((x + pi / &2) / (&2 * pi))))
