Structure fxpTheory
signature fxpTheory =
sig
type thm = Thm.thm
(* Definitions *)
val Attrib_def : thm
val BDIGFUN_def : thm
val BDIG_def : thm
val BWORD_def : thm
val Clip : thm
val Convergent : thm
val Exception_BIJ : thm
val Exception_TY_DEF : thm
val Exception_case : thm
val Exception_size_def : thm
val Fracbits_def : thm
val FxpAdd_def : thm
val FxpMul_def : thm
val FxpSub_def : thm
val Fxp_round_def : thm
val Fxperror_def : thm
val Intbits_def : thm
val Issigned_def : thm
val Isunsigned_def : thm
val Isvalid_def : thm
val MAX_def : thm
val MIN_def : thm
val Null_def : thm
val POSITIVE_def : thm
val Round : thm
val Signtype_def : thm
val Stream_def : thm
val Streamlength_def : thm
val TWOEXPONENT_def : thm
val To_plus_infinity : thm
val To_zero : thm
val Truncate : thm
val Wrap : thm
val Wrapp_def : thm
val attrib_def : thm
val bottomfxp_def : thm
val floor_def : thm
val fracbits_def : thm
val fraction_def : thm
val fxpAShift_def : thm
val fxpAbs_def : thm
val fxpAdd_def : thm
val fxpAnd_def : thm
val fxpDiv_def : thm
val fxpMul_def : thm
val fxpOr_def : thm
val fxpSub_def : thm
val fxp_TY_DEF : thm
val fxp_closest_def : thm
val fxp_round_def : thm
val fxp_roundmode_BIJ : thm
val fxp_roundmode_TY_DEF : thm
val fxp_roundmode_case : thm
val fxp_roundmode_size_def : thm
val fxp_tybij : thm
val fxperror_def : thm
val intbits_def : thm
val invalid : thm
val is_fxp_closest_def : thm
val is_signed_def : thm
val is_unsigned_def : thm
val is_valid_def : thm
val loss_sign : thm
val no_except : thm
val overflow : thm
val overflowmode_BIJ : thm
val overflowmode_TY_DEF : thm
val overflowmode_case : thm
val overflowmode_size_def : thm
val representable : thm
val signtype_def : thm
val stream_def : thm
val streamlength_def : thm
val topfxp_def : thm
val validAttr_def : thm
val value_def : thm
(* Theorems *)
val ADD_SUB2 : thm
val ATTRIB : thm
val B2 : thm
val B4 : thm
val BNVAL_WCAT2_SPLIT : thm
val BNVAL_WCATT_NBWORD : thm
val BNVAL_WCAT_NBWORD : thm
val COUNTINDUCT : thm
val DEFXP_FXP_NBWORD : thm
val DEFXP_FXP_REPLICATE : thm
val DEFXP_FXP_REPLICATEF : thm
val DEFXP_FXP_SPECIAL : thm
val DEFXP_FXP_WCAT : thm
val DEFXP_FXP_WCATT : thm
val DEFXP_FXP_WORDLEN : thm
val Exception2num_11 : thm
val Exception2num_ONTO : thm
val Exception2num_num2Exception : thm
val Exception2num_thm : thm
val Exception_Axiom : thm
val Exception_EQ_Exception : thm
val Exception_case_cong : thm
val Exception_case_def : thm
val Exception_distinct : thm
val Exception_induction : thm
val Exception_nchotomy : thm
val FINITECOUNT : thm
val FINITEFXPVALIDATTR : thm
val FINITEFXPVALIDATTRX : thm
val FINITEGENERAL : thm
val FINITELESSBASIS : thm
val FINITELESSINDUCT : thm
val FINITEPAIRLESS : thm
val FINITEVALID : thm
val FINITEVALIDATTR : thm
val FXP_ABSOLUTE_ERROR : thm
val FXP_ADD : thm
val FXP_ADD_ABSOLUTE_THM : thm
val FXP_ADD_ISVALID : thm
val FXP_ADD_THM : thm
val FXP_BOUND_AT_WORST_LEMMA : thm
val FXP_CLOSEST_IN_SET : thm
val FXP_CLOSEST_IS_EVERYTHING : thm
val FXP_CLOSEST_IS_FXP_CLOSEST : thm
val FXP_DIV_THM : thm
val FXP_ERROR_AT_WORST_LEMMA : thm
val FXP_ERROR_BOUND_LEMMA1_NEG_SIGNED : thm
val FXP_ERROR_BOUND_LEMMA1_POS_SIGNED : thm
val FXP_ERROR_BOUND_LEMMA1_UNSIGNED : thm
val FXP_ERROR_BOUND_LEMMA2_NEG_SIGNED : thm
val FXP_ERROR_BOUND_LEMMA2_POS_SIGNED : thm
val FXP_ERROR_BOUND_LEMMA2_UNSIGNED : thm
val FXP_ERROR_BOUND_LEMMA3_ABS_SIGNED : thm
val FXP_ERROR_BOUND_LEMMA3_NEG_SIGNED : thm
val FXP_ERROR_BOUND_LEMMA3_POS_SIGNED : thm
val FXP_ERROR_BOUND_LEMMA3_SIGNED : thm
val FXP_ERROR_BOUND_LEMMA3_UNSIGNED : thm
val FXP_FIRSTCROSS : thm
val FXP_FIRSTCROSS0 : thm
val FXP_FIRSTCROSS00 : thm
val FXP_FIRSTCROSS1 : thm
val FXP_FIRSTCROSS2 : thm
val FXP_FIRSTCROSS3 : thm
val FXP_MAIN_ERROR_BOUND_THEOREM : thm
val FXP_MAIN_ERROR_BOUND_THEOREM_SIGNED : thm
val FXP_MAIN_ERROR_BOUND_THEOREM_UNSIGNED : thm
val FXP_MUL : thm
val FXP_MUL_ABSOLUTE_THM : thm
val FXP_MUL_ISVALID : thm
val FXP_MUL_THM : thm
val FXP_SUB : thm
val FXP_SUB_ABSOLUTE_THM : thm
val FXP_SUB_ISVALID : thm
val FXP_SUB_THM : thm
val INSTANCE : thm
val INSTANCEFINITE : thm
val INTBITS : thm
val ISVALIDNBWORD : thm
val ISVALIDREPLICATE : thm
val ISVALIDREPLICATEF : thm
val ISVALIDWORDLEN : thm
val ISVALID_ATTR_IMAGE : thm
val ISVALID_ATTR_SUB : thm
val ISVALID_SUB : thm
val ISVALID_WCAT : thm
val ISVALID_WCATT : thm
val ISVALISPECIAL : thm
val IS_FXP_CLOSEST_EXISTS : thm
val IS_VALID_ATTRIB_NONEMPTY : thm
val IS_VALID_FXP_CLOSEST : thm
val IS_VALID_NONEMPTY : thm
val IS_VALID_ROUND_CONV_CLIP : thm
val LASTN1 : thm
val MAINFINITE : thm
val MATCHFINITE : thm
val MATCHFINITEVALID : thm
val MATCHFINITEVALIDATTR : thm
val NOTTiIsigned : thm
val NOTiIsigned : thm
val PWFLT_REAL : thm
val PWL1 : thm
val PWLGSNBW : thm
val REAL_BNVAL_NBWORD : thm
val REAL_OF_NUM_GT : thm
val REAL_OF_NUM_SUB : thm
val REPLICATELENGTH : thm
val REPLICATELENGTHF : thm
val SIGN : thm
val STREAM : thm
val STREAMLEN : thm
val TWOEXP : thm
val TWOEXPGE1 : thm
val WORDBASIS : thm
val WORDFINITE : thm
val WORDINDUCT : thm
val WORDPAIRIMAGE : thm
val datatype_Exception : thm
val datatype_fxp_roundmode : thm
val datatype_overflowmode : thm
val fxp_roundmode2num_11 : thm
val fxp_roundmode2num_ONTO : thm
val fxp_roundmode2num_num2fxp_roundmode : thm
val fxp_roundmode2num_thm : thm
val fxp_roundmode_Axiom : thm
val fxp_roundmode_EQ_fxp_roundmode : thm
val fxp_roundmode_case_cong : thm
val fxp_roundmode_case_def : thm
val fxp_roundmode_distinct : thm
val fxp_roundmode_induction : thm
val fxp_roundmode_nchotomy : thm
val iIsigned : thm
val invfracge0 : thm
val invfracgt0 : thm
val maxmin : thm
val num2Exception_11 : thm
val num2Exception_Exception2num : thm
val num2Exception_ONTO : thm
val num2Exception_thm : thm
val num2fxp_roundmode_11 : thm
val num2fxp_roundmode_ONTO : thm
val num2fxp_roundmode_fxp_roundmode2num : thm
val num2fxp_roundmode_thm : thm
val num2overflowmode_11 : thm
val num2overflowmode_ONTO : thm
val num2overflowmode_overflowmode2num : thm
val num2overflowmode_thm : thm
val opopow : thm
val opstream : thm
val opstream1 : thm
val otwoexpsl : thm
val otwoexpsl1 : thm
val otwoexpsl11 : thm
val overflowmode2num_11 : thm
val overflowmode2num_ONTO : thm
val overflowmode2num_num2overflowmode : thm
val overflowmode2num_thm : thm
val overflowmode_Axiom : thm
val overflowmode_EQ_overflowmode : thm
val overflowmode_case_cong : thm
val overflowmode_case_def : thm
val overflowmode_distinct : thm
val overflowmode_induction : thm
val overflowmode_nchotomy : thm
val pwv23le1 : thm
val pwv23le11 : thm
val pwv23lt : thm
val pwv23lt1 : thm
val pwv23lt11 : thm
val pwvexp126lt1 : thm
val pwvexp126lt11 : thm
val pwvexp23gt : thm
val pwvexp23lt : thm
val pwvexp23lt1 : thm
val pwvexp23lt11 : thm
val pwvexpfraclt : thm
val pwvexpfraclt1 : thm
val pwvfracle1 : thm
val pwvfracle11 : thm
val pwvfracle111 : thm
val pwvfracle2 : thm
val pwvfracle21 : thm
val pwvfraclereal : thm
val pwvfraclt : thm
val pwvfraclt1 : thm
val pwvfraclt11 : thm
val pwvfraclt111 : thm
val pwvfraclt2 : thm
val pwvfraclt21 : thm
val pwvfracltt1 : thm
val s3 : thm
val twoexpsl : thm
val twoone : thm
val fxp_grammars : type_grammar.grammar * term_grammar.grammar
(*
[integer] Parent theory of "fxp"
[real] Parent theory of "fxp"
[word] Parent theory of "fxp"
[Attrib_def] Definition
|- !a. Attrib a = attrib (defxp a)
[BDIGFUN_def] Definition
|- !a. BDIGFUN a = (\n. BDIG n a)
[BDIG_def] Definition
|- !n a. BDIG n a = VB ((a DIV 2 ** n) MOD 2)
[BWORD_def] Definition
|- !n m. BWORD n m = WORD (GENLIST (BDIGFUN n) m)
[Clip] Definition
|- Clip = num2overflowmode 1
[Convergent] Definition
|- Convergent = num2fxp_roundmode 4
[Exception_BIJ] Definition
|- (!a. num2Exception (Exception2num a) = a) /\
!r. (\n. n < 4) r = (Exception2num (num2Exception r) = r)
[Exception_TY_DEF] Definition
|- ?rep. TYPE_DEFINITION (\n. n < 4) rep
[Exception_case] Definition
|- !v0 v1 v2 v3 x.
(case x of
no_except -> v0
|| overflow -> v1
|| invalid -> v2
|| loss_sign -> v3) =
(\m.
(if m < 1 then
v0
else
(if m < 2 then v1 else (if m = 2 then v2 else v3))))
(Exception2num x)
[Exception_size_def] Definition
|- !x. Exception_size x = 0
[Fracbits_def] Definition
|- !a. Fracbits a = fracbits (Attrib a)
[FxpAdd_def] Definition
|- !X a b. FxpAdd X a b = FST (fxpAdd X Convergent Clip a b)
[FxpMul_def] Definition
|- !X a b. FxpMul X a b = FST (fxpMul X Convergent Clip a b)
[FxpSub_def] Definition
|- !X a b. FxpSub X a b = FST (fxpSub X Convergent Clip a b)
[Fxp_round_def] Definition
|- !X x. Fxp_round X x = FST (fxp_round X Convergent x Clip)
[Fxperror_def] Definition
|- !X x. Fxperror X x = fxperror X Convergent Clip x
[Intbits_def] Definition
|- !a. Intbits a = intbits (Attrib a)
[Issigned_def] Definition
|- !a. Issigned a = is_signed (Attrib a)
[Isunsigned_def] Definition
|- !a. Isunsigned a = is_unsigned (Attrib a)
[Isvalid_def] Definition
|- !a. Isvalid a = is_valid (defxp a)
[MAX_def] Definition
|- !X.
MAX X =
(if is_unsigned X then
(2 pow streamlength X - 1) / 2 pow fracbits X
else
(2 pow (streamlength X - 1) - 1) / 2 pow fracbits X)
[MIN_def] Definition
|- !X.
MIN X =
(if is_unsigned X then
0
else
~(2 pow (streamlength X - 1)) / 2 pow fracbits X)
[Null_def] Definition
|- Null = @a. ~Isvalid a
[POSITIVE_def] Definition
|- !x. POSITIVE x = 2 pow TWOEXPONENT x + x
[Round] Definition
|- Round = num2fxp_roundmode 0
[Signtype_def] Definition
|- !a. Signtype a = signtype (Attrib a)
[Stream_def] Definition
|- !a. Stream a = stream (defxp a)
[Streamlength_def] Definition
|- !a. Streamlength a = streamlength (Attrib a)
[TWOEXPONENT_def] Definition
|- !x. TWOEXPONENT x = @n. 2 pow n >= abs x /\ !m. 2 pow m >= abs x ==> n <= m
[To_plus_infinity] Definition
|- To_plus_infinity = num2fxp_roundmode 2
[To_zero] Definition
|- To_zero = num2fxp_roundmode 1
[Truncate] Definition
|- Truncate = num2fxp_roundmode 3
[Wrap] Definition
|- Wrap = num2overflowmode 0
[Wrapp_def] Definition
|- !X x.
Wrapp X x =
(if x >= 0 then
fxp
(WCAT
(BWORD (floor x) (intbits X),
BWORD (floor (2 pow fracbits X * fraction x)) (fracbits X)),X)
else
fxp
(WCAT
(BWORD (floor (POSITIVE x)) (intbits X) WOR
BWORD (2 ** TWOEXPONENT x) (intbits X),
BWORD (floor (2 pow fracbits X * fraction (POSITIVE x)))
(fracbits X)),X))
[attrib_def] Definition
|- !v a. attrib (v,a) = a
[bottomfxp_def] Definition
|- !X.
bottomfxp X =
(if is_unsigned X then
fxp (WORD (REPLICATE (streamlength X) F),X)
else
fxp (WCAT (WORD [T],WORD (REPLICATE (streamlength X - 1) F)),X))
[floor_def] Definition
|- !x. floor x = @n. & n <= abs x /\ !i. & i <= abs x ==> i <= n
[fracbits_def] Definition
|- !X.
fracbits X =
(if is_unsigned X then
streamlength X - intbits X
else
streamlength X - intbits X - 1)
[fraction_def] Definition
|- !x. fraction x = x - & (floor x)
[fxpAShift_def] Definition
|- !X rnd over a b.
fxpAShift X rnd over a b =
(if ~Isvalid a then
(Null,invalid)
else
(if b < 0 then
fxp_round X rnd
(value
(fxp
(WCAT
(WORD (REPLICATE (Num (ABS b)) (MSB (Stream a))),
WSEG (streamlength (Attrib a) - 1)
(streamlength (Attrib a) - Num (ABS b)) (Stream a)),
Attrib a))) over
else
fxp_round X rnd
(value
(fxp
(WCAT
(WORD (REPLICATE (Num (ABS b)) F),
WSEG (streamlength (Attrib a) - SUC (Num (ABS b))) 0
(Stream a)),Attrib a))) over))
[fxpAbs_def] Definition
|- !X rnd over a.
fxpAbs X rnd over a =
(if ~Isvalid a then
(Null,invalid)
else
fxp_round X rnd (abs (value a)) over)
[fxpAdd_def] Definition
|- !X rnd over a b.
fxpAdd X rnd over a b =
(if ~(Isvalid a /\ Isvalid b) then
(Null,invalid)
else
(if value a + value b < 0 /\ is_unsigned X then
(fxp (WORD (REPLICATE (streamlength X) F),X),loss_sign)
else
fxp_round X rnd (value a + value b) over))
[fxpAnd_def] Definition
|- !X a b.
fxpAnd X a b =
(if ~(Isvalid a /\ Isvalid b) \/ ~(Attrib a = X) \/ ~(Attrib b = X) then
(Null,invalid)
else
(fxp (Stream a WAND Stream b,X),no_except))
[fxpDiv_def] Definition
|- !X rnd over a b.
fxpDiv X rnd over a b =
(if ~(Isvalid a /\ Isvalid b) then
(Null,invalid)
else
(if value b = 0 then
(fxp (WORD (REPLICATE (streamlength X) F),X),invalid)
else
(if value a / value b < 0 /\ is_unsigned X then
(fxp (WORD (REPLICATE (streamlength X) F),X),loss_sign)
else
fxp_round X rnd (value a / value b) over)))
[fxpMul_def] Definition
|- !X rnd over a b.
fxpMul X rnd over a b =
(if ~(Isvalid a /\ Isvalid b) then
(Null,invalid)
else
(if value a * value b < 0 /\ is_unsigned X then
(fxp (WORD (REPLICATE (streamlength X) F),X),loss_sign)
else
fxp_round X rnd (value a * value b) over))
[fxpOr_def] Definition
|- !X a b.
fxpOr X a b =
(if ~(Isvalid a /\ Isvalid b) \/ ~(Attrib a = X) \/ ~(Attrib b = X) then
(Null,invalid)
else
(fxp (Stream a WOR Stream b,X),no_except))
[fxpSub_def] Definition
|- !X rnd over a b.
fxpSub X rnd over a b =
(if ~(Isvalid a /\ Isvalid b) then
(Null,invalid)
else
(if value a - value b < 0 /\ is_unsigned X then
(fxp (WORD (REPLICATE (streamlength X) F),X),loss_sign)
else
fxp_round X rnd (value a - value b) over))
[fxp_TY_DEF] Definition
|- ?rep. TYPE_DEFINITION is_valid rep
[fxp_closest_def] Definition
|- !v p s x.
fxp_closest v p s x =
@a.
is_fxp_closest v s x a /\ ((?b. is_fxp_closest v s x b /\ p b) ==> p a)
[fxp_round_def] Definition
|- (!X x mode.
fxp_round X Convergent x mode =
(if x > MAX X /\ (mode = Clip) then
(topfxp X,overflow)
else
(if x < MIN X /\ (mode = Clip) then
(bottomfxp X,overflow)
else
(if x > MAX X /\ (mode = Wrap) then
(Wrapp X x,overflow)
else
(if x < MIN X /\ (mode = Wrap) then
(Wrapp X x,overflow)
else
(fxp_closest value (\a. LSB (Stream a) = F)
{a | Isvalid a /\ (Attrib a = X)} x,no_except)))))) /\
(!X x mode.
fxp_round X To_zero x mode =
(if x > MAX X /\ (mode = Clip) then
(topfxp X,overflow)
else
(if x < MIN X /\ (mode = Clip) then
(bottomfxp X,overflow)
else
(if x >= MAX X /\ (mode = Wrap) then
(Wrapp X x,overflow)
else
(if x < MIN X /\ (mode = Wrap) then
(Wrapp X x,overflow)
else
(fxp_closest value (\a. T)
{a |
Isvalid a /\ (Attrib a = X) /\ abs (value a) <= abs x} x,
no_except)))))) /\
(!X x mode.
fxp_round X To_plus_infinity x mode =
(if x > MAX X /\ (mode = Clip) then
(topfxp X,overflow)
else
(if x < MIN X /\ (mode = Clip) then
(bottomfxp X,overflow)
else
(if x > MAX X /\ (mode = Wrap) then
(Wrapp X x,overflow)
else
(if x < MIN X /\ (mode = Wrap) then
(Wrapp X x,overflow)
else
(fxp_closest value (\a. T)
{a | Isvalid a /\ (Attrib a = X) /\ value a >= x} x,
no_except)))))) /\
(!X x mode.
fxp_round X Truncate x mode =
(if x > MAX X /\ (mode = Clip) then
(topfxp X,overflow)
else
(if x < MIN X /\ (mode = Clip) then
(bottomfxp X,overflow)
else
(if x > MAX X /\ (mode = Wrap) then
(Wrapp X x,overflow)
else
(if x < MIN X /\ (mode = Wrap) then
(Wrapp X x,overflow)
else
(fxp_closest value (\a. T)
{a | Isvalid a /\ (Attrib a = X) /\ value a <= x} x,
no_except)))))) /\
!X x mode.
fxp_round X Round x mode =
(if x > MAX X /\ (mode = Clip) then
(topfxp X,overflow)
else
(if x < MIN X /\ (mode = Clip) then
(bottomfxp X,overflow)
else
(if x > MAX X /\ (mode = Wrap) then
(Wrapp X x,overflow)
else
(if x < MIN X /\ (mode = Wrap) then
(Wrapp X x,overflow)
else
(fxp_closest value (\a. value (fxp (Stream a,X)) >= x)
{a | Isvalid a /\ (Attrib a = X)} x,no_except)))))
[fxp_roundmode_BIJ] Definition
|- (!a. num2fxp_roundmode (fxp_roundmode2num a) = a) /\
!r. (\n. n < 5) r = (fxp_roundmode2num (num2fxp_roundmode r) = r)
[fxp_roundmode_TY_DEF] Definition
|- ?rep. TYPE_DEFINITION (\n. n < 5) rep
[fxp_roundmode_case] Definition
|- !v0 v1 v2 v3 v4 x.
(case x of
Round -> v0
|| To_zero -> v1
|| To_plus_infinity -> v2
|| Truncate -> v3
|| Convergent -> v4) =
(\m.
(if m < 2 then
(if m = 0 then v0 else v1)
else
(if m < 3 then v2 else (if m = 3 then v3 else v4))))
(fxp_roundmode2num x)
[fxp_roundmode_size_def] Definition
|- !x. fxp_roundmode_size x = 0
[fxp_tybij] Definition
|- (!a. fxp (defxp a) = a) /\ !r. is_valid r = (defxp (fxp r) = r)
[fxperror_def] Definition
|- !X rnd over x.
fxperror X rnd over x = value (FST (fxp_round X rnd x over)) - x
[intbits_def] Definition
|- !b ib sf. intbits (b,ib,sf) = ib
[invalid] Definition
|- invalid = num2Exception 2
[is_fxp_closest_def] Definition
|- !v s x a.
is_fxp_closest v s x a =
a IN s /\ !b. b IN s ==> abs (v a - x) <= abs (v b - x)
[is_signed_def] Definition
|- !X. is_signed X = (signtype X = 1)
[is_unsigned_def] Definition
|- !X. is_unsigned X = (signtype X = 0)
[is_valid_def] Definition
|- !a.
is_valid a =
validAttr (attrib a) /\ (WORDLEN (stream a) = streamlength (attrib a))
[loss_sign] Definition
|- loss_sign = num2Exception 3
[no_except] Definition
|- no_except = num2Exception 0
[overflow] Definition
|- overflow = num2Exception 1
[overflowmode_BIJ] Definition
|- (!a. num2overflowmode (overflowmode2num a) = a) /\
!r. (\n. n < 2) r = (overflowmode2num (num2overflowmode r) = r)
[overflowmode_TY_DEF] Definition
|- ?rep. TYPE_DEFINITION (\n. n < 2) rep
[overflowmode_case] Definition
|- !v0 v1 x.
(case x of Wrap -> v0 || Clip -> v1) =
(\m. (if m = 0 then v0 else v1)) (overflowmode2num x)
[overflowmode_size_def] Definition
|- !x. overflowmode_size x = 0
[representable] Definition
|- !X x. representable X x = ~(x > MAX X) /\ ~(x < MIN X)
[signtype_def] Definition
|- !b ib st. signtype (b,ib,st) = st
[stream_def] Definition
|- !v a. stream (v,a) = v
[streamlength_def] Definition
|- !b ib sf. streamlength (b,ib,sf) = b
[topfxp_def] Definition
|- !X.
topfxp X =
(if is_unsigned X then
fxp (WORD (REPLICATE (streamlength X) T),X)
else
fxp (WCAT (WORD [F],WORD (REPLICATE (streamlength X - 1) T)),X))
[validAttr_def] Definition
|- !X.
validAttr X =
(streamlength X > 0 /\ streamlength X < 257) /\
intbits X < streamlength X + 1 /\ signtype X < 2
[value_def] Definition
|- !a.
value a =
(if Isunsigned a then
& (BNVAL (Stream a)) / 2 pow Fracbits a
else
(& (BNVAL (Stream a)) -
& (BV (MSB (Stream a)) * 2 ** Streamlength a)) / 2 pow Fracbits a)
[ADD_SUB2] Theorem
|- !m n. m + n - m = n
[ATTRIB] Theorem
|- !a. attrib a = SND a
[B2] Theorem
|- !n m s x.
x - 2 pow n * inv (2 pow fracbits (n,m,s)) <=
x -
(2 pow n * inv (2 pow fracbits (n,m,s)) - inv (2 pow fracbits (n,m,s)))
[B4] Theorem
|- !n m s.
(2 pow n - 1) / 2 pow fracbits (n,m,s) <=
2 pow n * inv (2 pow fracbits (n,m,s))
[BNVAL_WCAT2_SPLIT] Theorem
|- !n w x.
w IN PWORDLEN n ==> (BNVAL (WCAT (WORD [x],w)) = BV x * 2 ** n + BNVAL w)
[BNVAL_WCATT_NBWORD] Theorem
|- !n k.
BNVAL (WCAT (WORD [T],NBWORD (n - 1) k)) =
BV T * 2 ** (n - 1) + BNVAL (NBWORD (n - 1) k)
[BNVAL_WCAT_NBWORD] Theorem
|- !n k.
BNVAL (WCAT (WORD [F],NBWORD (n - 1) k)) =
BV F * 2 ** (n - 1) + BNVAL (NBWORD (n - 1) k)
[COUNTINDUCT] Theorem
|- !n. ({x | x < 0} = {}) /\ ({x | x < SUC n} = n INSERT {x | x < n})
[DEFXP_FXP_NBWORD] Theorem
|- !n m s k.
validAttr (n,m,s) ==>
(defxp (fxp (NBWORD n k,n,m,s)) = (NBWORD n k,n,m,s))
[DEFXP_FXP_REPLICATE] Theorem
|- !n m s.
validAttr (n,m,s) ==>
(defxp (fxp (WORD (REPLICATE n T),n,m,s)) = (WORD (REPLICATE n T),n,m,s))
[DEFXP_FXP_REPLICATEF] Theorem
|- !n m s.
validAttr (n,m,s) ==>
(defxp (fxp (WORD (REPLICATE n F),n,m,s)) = (WORD (REPLICATE n F),n,m,s))
[DEFXP_FXP_SPECIAL] Theorem
|- defxp (fxp (WORD (REPLICATE 2 T),2,1,1)) = (WORD (REPLICATE 2 T),2,1,1)
[DEFXP_FXP_WCAT] Theorem
|- !w n m s k.
validAttr (n,m,s) ==>
(defxp (fxp (WCAT (WORD [F],NBWORD (n - 1) k),n,m,s)) =
(WCAT (WORD [F],NBWORD (n - 1) k),n,m,s))
[DEFXP_FXP_WCATT] Theorem
|- !w n m s k.
validAttr (n,m,s) ==>
(defxp (fxp (WCAT (WORD [T],NBWORD (n - 1) k),n,m,s)) =
(WCAT (WORD [T],NBWORD (n - 1) k),n,m,s))
[DEFXP_FXP_WORDLEN] Theorem
|- !w m s.
validAttr (WORDLEN w,m,s) ==>
(defxp (fxp (w,WORDLEN w,m,s)) = (w,WORDLEN w,m,s))
[Exception2num_11] Theorem
|- !a a'. (Exception2num a = Exception2num a') = (a = a')
[Exception2num_ONTO] Theorem
|- !r. r < 4 = ?a. r = Exception2num a
[Exception2num_num2Exception] Theorem
|- !r. r < 4 = (Exception2num (num2Exception r) = r)
[Exception2num_thm] Theorem
|- (Exception2num no_except = 0) /\ (Exception2num overflow = 1) /\
(Exception2num invalid = 2) /\ (Exception2num loss_sign = 3)
[Exception_Axiom] Theorem
|- !x0 x1 x2 x3.
?f.
(f no_except = x0) /\ (f overflow = x1) /\ (f invalid = x2) /\
(f loss_sign = x3)
[Exception_EQ_Exception] Theorem
|- !a a'. (a = a') = (Exception2num a = Exception2num a')
[Exception_case_cong] Theorem
|- !M M' v0 v1 v2 v3.
(M = M') /\ ((M' = no_except) ==> (v0 = v0')) /\
((M' = overflow) ==> (v1 = v1')) /\ ((M' = invalid) ==> (v2 = v2')) /\
((M' = loss_sign) ==> (v3 = v3')) ==>
((case M of
no_except -> v0
|| overflow -> v1
|| invalid -> v2
|| loss_sign -> v3) =
case M' of
no_except -> v0'
|| overflow -> v1'
|| invalid -> v2'
|| loss_sign -> v3')
[Exception_case_def] Theorem
|- (!v0 v1 v2 v3.
(case no_except of
no_except -> v0
|| overflow -> v1
|| invalid -> v2
|| loss_sign -> v3) =
v0) /\
(!v0 v1 v2 v3.
(case overflow of
no_except -> v0
|| overflow -> v1
|| invalid -> v2
|| loss_sign -> v3) =
v1) /\
(!v0 v1 v2 v3.
(case invalid of
no_except -> v0
|| overflow -> v1
|| invalid -> v2
|| loss_sign -> v3) =
v2) /\
!v0 v1 v2 v3.
(case loss_sign of
no_except -> v0
|| overflow -> v1
|| invalid -> v2
|| loss_sign -> v3) =
v3
[Exception_distinct] Theorem
|- ~(no_except = overflow) /\ ~(no_except = invalid) /\
~(no_except = loss_sign) /\ ~(overflow = invalid) /\
~(overflow = loss_sign) /\ ~(invalid = loss_sign)
[Exception_induction] Theorem
|- !P. P invalid /\ P loss_sign /\ P no_except /\ P overflow ==> !a. P a
[Exception_nchotomy] Theorem
|- !a. (a = no_except) \/ (a = overflow) \/ (a = invalid) \/ (a = loss_sign)
[FINITECOUNT] Theorem
|- !n. FINITE {x | x < n}
[FINITEFXPVALIDATTR] Theorem
|- !n m s. FINITE {a | Isvalid a /\ (Attrib a = (n,m,s))}
[FINITEFXPVALIDATTRX] Theorem
|- !X. FINITE {a | Isvalid a /\ (Attrib a = X)}
[FINITEGENERAL] Theorem
|- !p q r.
FINITE
{a |
FST (SND a) < p /\ FST (SND (SND a)) < q /\ SND (SND (SND a)) < r /\
(WORDLEN (FST a) = FST (SND a))}
[FINITELESSBASIS] Theorem
|- {(w,x) | (WORDLEN w = x) /\ x < 0} = {}
[FINITELESSINDUCT] Theorem
|- !n.
FINITE {(w,x) | (WORDLEN w = x) /\ x < SUC n} =
FINITE
({(w,x) | (WORDLEN w = x) /\ (x = n)} UNION
{(w,x) | (WORDLEN w = x) /\ x < n})
[FINITEPAIRLESS] Theorem
|- !m. FINITE {(w,x) | (WORDLEN w = x) /\ x < m}
[FINITEVALID] Theorem
|- FINITE {a | is_valid a}
[FINITEVALIDATTR] Theorem
|- !n m s. FINITE {a | is_valid a /\ (attrib a = (n,m,s))}
[FXP_ABSOLUTE_ERROR] Theorem
|- !x X.
validAttr X /\ representable X x ==>
?e. abs e <= inv (2 pow fracbits X) /\ (value (Fxp_round X x) = x + e)
[FXP_ADD] Theorem
|- !a b X.
Isvalid a /\ Isvalid b /\ validAttr X /\
representable X (value a + value b) ==>
Isvalid (FxpAdd X a b) /\
(value (FxpAdd X a b) =
value a + value b + Fxperror X (value a + value b))
[FXP_ADD_ABSOLUTE_THM] Theorem
|- !a b X.
Isvalid a /\ Isvalid b /\ validAttr X /\
representable X (value a + value b) ==>
Isvalid (FxpAdd X a b) /\
?e.
abs e <= inv (2 pow fracbits X) /\
(value (FxpAdd X a b) = value a + value b + e)
[FXP_ADD_ISVALID] Theorem
|- !a b X.
Isvalid a /\ Isvalid b /\ validAttr X /\
representable X (value a + value b) ==>
Isvalid (FxpAdd X a b)
[FXP_ADD_THM] Theorem
|- !a b n m s.
Isvalid a /\ Isvalid b /\ validAttr (n,m,s) /\
~(value a + value b > MAX (n,m,s)) /\
~(value a + value b < MIN (n,m,s)) ==>
Isvalid (FST (fxpAdd (n,m,s) Convergent Clip a b)) /\
(value (FST (fxpAdd (n,m,s) Convergent Clip a b)) =
value a + value b + fxperror (n,m,s) Convergent Clip (value a + value b))
[FXP_BOUND_AT_WORST_LEMMA] Theorem
|- !a x n m s.
~(x > MAX (n,m,s)) /\ ~(x < MIN (n,m,s)) /\ validAttr (n,m,s) /\
Isvalid a /\ (Attrib a = (n,m,s)) ==>
abs (value (FST (fxp_round (n,m,s) Convergent x Clip)) - x) <=
abs (value a - x)
[FXP_CLOSEST_IN_SET] Theorem
|- !v p x s. FINITE s ==> ~(s = {}) ==> fxp_closest v p s x IN s
[FXP_CLOSEST_IS_EVERYTHING] Theorem
|- !v p x s.
FINITE s ==>
~(s = {}) ==>
is_fxp_closest v s x (fxp_closest v p s x) /\
((?b. is_fxp_closest v s x b /\ p b) ==> p (fxp_closest v p s x))
[FXP_CLOSEST_IS_FXP_CLOSEST] Theorem
|- !v p x s.
FINITE s ==> ~(s = {}) ==> is_fxp_closest v s x (fxp_closest v p s x)
[FXP_DIV_THM] Theorem
|- !a b n m s.
Isvalid a /\ Isvalid b /\ validAttr (n,m,s) /\
~(value a / value b > MAX (n,m,s)) /\
~(value a / value b < MIN (n,m,s)) /\ ~(value b = 0) ==>
Isvalid (FST (fxpDiv (n,m,s) Convergent Clip a b)) /\
(value (FST (fxpDiv (n,m,s) Convergent Clip a b)) =
value a / value b + fxperror (n,m,s) Convergent Clip (value a / value b))
[FXP_ERROR_AT_WORST_LEMMA] Theorem
|- !a x n m s.
~(x > MAX (n,m,s)) /\ ~(x < MIN (n,m,s)) /\ validAttr (n,m,s) /\
Isvalid a /\ (Attrib a = (n,m,s)) ==>
abs (fxperror (n,m,s) Convergent Clip x) <= abs (value a - x)
[FXP_ERROR_BOUND_LEMMA1_NEG_SIGNED] Theorem
|- !x n m s.
0 <= ~x /\
~x <= 2 pow (streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s) /\
validAttr (n,m,s) /\ ~is_unsigned (n,m,s) ==>
?k.
k < 2 ** (streamlength (n,m,s) - 1) /\
& k / 2 pow fracbits (n,m,s) <= ~x /\
~x <= & (SUC k) / 2 pow fracbits (n,m,s)
[FXP_ERROR_BOUND_LEMMA1_POS_SIGNED] Theorem
|- !x n m s.
0 <= x /\
x <= 2 pow (streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s) /\
validAttr (n,m,s) /\ ~is_unsigned (n,m,s) ==>
?k.
k < 2 ** (streamlength (n,m,s) - 1) /\
& k / 2 pow fracbits (n,m,s) <= x /\
x <= & (SUC k) / 2 pow fracbits (n,m,s)
[FXP_ERROR_BOUND_LEMMA1_UNSIGNED] Theorem
|- !x n m s.
~(x > MAX (n,m,s)) /\ ~(x < MIN (n,m,s)) /\ validAttr (n,m,s) /\
is_unsigned (n,m,s) ==>
?k.
k < 2 ** streamlength (n,m,s) /\ & k / 2 pow fracbits (n,m,s) <= x /\
x < & (SUC k) / 2 pow fracbits (n,m,s)
[FXP_ERROR_BOUND_LEMMA2_NEG_SIGNED] Theorem
|- !x n m s.
0 <= ~x /\
~x <= 2 pow (streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s) /\
validAttr (n,m,s) /\ ~is_unsigned (n,m,s) ==>
?k.
k < 2 ** (streamlength (n,m,s) - 1) /\
abs (~(& k / 2 pow fracbits (n,m,s)) - x) <=
inv (2 pow fracbits (n,m,s))
[FXP_ERROR_BOUND_LEMMA2_POS_SIGNED] Theorem
|- !x n m s.
0 <= x /\
x <= 2 pow (streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s) /\
validAttr (n,m,s) /\ ~is_unsigned (n,m,s) ==>
?k.
k < 2 ** (streamlength (n,m,s) - 1) /\
abs (x - & k / 2 pow fracbits (n,m,s)) <= inv (2 pow fracbits (n,m,s))
[FXP_ERROR_BOUND_LEMMA2_UNSIGNED] Theorem
|- !x n m s.
~(x > MAX (n,m,s)) /\ ~(x < MIN (n,m,s)) /\ validAttr (n,m,s) /\
is_unsigned (n,m,s) ==>
?k.
k <= 2 ** streamlength (n,m,s) /\
abs (x - & k / 2 pow fracbits (n,m,s)) <= inv (2 pow fracbits (n,m,s))
[FXP_ERROR_BOUND_LEMMA3_ABS_SIGNED] Theorem
|- !x n m s.
abs x <= 2 pow (streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s) /\
validAttr (n,m,s) /\ ~is_unsigned (n,m,s) ==>
?w.
abs (value (fxp (w,n,m,s)) - x) <= inv (2 pow fracbits (n,m,s)) /\
(WORDLEN w = n)
[FXP_ERROR_BOUND_LEMMA3_NEG_SIGNED] Theorem
|- !x n m s.
0 <= ~x /\
~x <= 2 pow (streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s) /\
validAttr (n,m,s) /\ ~is_unsigned (n,m,s) ==>
?w.
abs (value (fxp (w,n,m,s)) - x) <= inv (2 pow fracbits (n,m,s)) /\
(WORDLEN w = n)
[FXP_ERROR_BOUND_LEMMA3_POS_SIGNED] Theorem
|- !x n m s.
0 <= x /\
x <= 2 pow (streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s) /\
validAttr (n,m,s) /\ ~is_unsigned (n,m,s) ==>
?w.
abs (value (fxp (w,n,m,s)) - x) <= inv (2 pow fracbits (n,m,s)) /\
(WORDLEN w = n)
[FXP_ERROR_BOUND_LEMMA3_SIGNED] Theorem
|- !x n m s.
~(x > MAX (n,m,s)) /\ ~(x < MIN (n,m,s)) /\ validAttr (n,m,s) /\
~is_unsigned (n,m,s) ==>
?w.
abs (value (fxp (w,n,m,s)) - x) <= inv (2 pow fracbits (n,m,s)) /\
(WORDLEN w = n)
[FXP_ERROR_BOUND_LEMMA3_UNSIGNED] Theorem
|- !x n m s.
~(x > MAX (n,m,s)) /\ ~(x < MIN (n,m,s)) /\ validAttr (n,m,s) /\
is_unsigned (n,m,s) ==>
?w.
abs (value (fxp (w,n,m,s)) - x) <= inv (2 pow fracbits (n,m,s)) /\
(WORDLEN w = n)
[FXP_FIRSTCROSS] Theorem
|- !p q r.
{a |
FST (SND a) < p /\ FST (SND (SND a)) < q /\ SND (SND (SND a)) < r /\
(WORDLEN (FST a) = FST (SND a))} =
IMAGE (\((w,x),y,z). (w,x,y,z))
({(w,x) | (WORDLEN w = x) /\ x < p} CROSS
({y | y < q} CROSS {z | z < r}))
[FXP_FIRSTCROSS0] Theorem
|- !x p q r.
FST (SND x) < p /\ FST (SND (SND x)) < q /\ SND (SND (SND x)) < r /\
(WORDLEN (FST x) = FST (SND x)) ==>
(?x''.
(FST ((FST x,FST (SND x)),FST (SND (SND x)),SND (SND (SND x))),T) =
(\(w,x). ((w,x),(WORDLEN w = x) /\ x < p)) x'') /\
FST (SND ((FST x,FST (SND x)),FST (SND (SND x)),SND (SND (SND x)))) < q /\
SND (SND ((FST x,FST (SND x)),FST (SND (SND x)),SND (SND (SND x)))) < r
[FXP_FIRSTCROSS00] Theorem
|- !x p q r.
x =
(\((w,x),y,z). (w,x,y,z))
((FST x,FST (SND x)),FST (SND (SND x)),SND (SND (SND x)))
[FXP_FIRSTCROSS1] Theorem
|- !x p q r.
FST (SND x) < p /\ FST (SND (SND x)) < q /\ SND (SND (SND x)) < r /\
(WORDLEN (FST x) = FST (SND x)) ==>
?x'.
(x = (\((w,x),y,z). (w,x,y,z)) x') /\
(?x. (FST x',T) = (\(w,x). ((w,x),(WORDLEN w = x) /\ x < p)) x) /\
FST (SND x') < q /\ SND (SND x') < r
[FXP_FIRSTCROSS2] Theorem
|- !x p q r.
(?x'.
(x = (\((w,x),y,z). (w,x,y,z)) x') /\
(?x. (FST x',T) = (\(w,x). ((w,x),(WORDLEN w = x) /\ x < p)) x) /\
FST (SND x') < q /\ SND (SND x') < r) ==>
FST (SND x) < p /\ FST (SND (SND x)) < q /\ SND (SND (SND x)) < r /\
(WORDLEN (FST x) = FST (SND x))
[FXP_FIRSTCROSS3] Theorem
|- !x p q r.
FST (SND x) < p /\ FST (SND (SND x)) < q /\ SND (SND (SND x)) < r /\
(WORDLEN (FST x) = FST (SND x)) =
?x'.
(x = (\((w,x),y,z). (w,x,y,z)) x') /\
(?x. (FST x',T) = (\(w,x). ((w,x),(WORDLEN w = x) /\ x < p)) x) /\
FST (SND x') < q /\ SND (SND x') < r
[FXP_MAIN_ERROR_BOUND_THEOREM] Theorem
|- !x n m s.
~(x > MAX (n,m,s)) /\ ~(x < MIN (n,m,s)) /\ validAttr (n,m,s) ==>
abs (fxperror (n,m,s) Convergent Clip x) <= inv (2 pow fracbits (n,m,s))
[FXP_MAIN_ERROR_BOUND_THEOREM_SIGNED] Theorem
|- !x n m s.
~(x > MAX (n,m,s)) /\ ~(x < MIN (n,m,s)) /\ validAttr (n,m,s) /\
~is_unsigned (n,m,s) ==>
abs (fxperror (n,m,s) Convergent Clip x) <= inv (2 pow fracbits (n,m,s))
[FXP_MAIN_ERROR_BOUND_THEOREM_UNSIGNED] Theorem
|- !x n m s.
~(x > MAX (n,m,s)) /\ ~(x < MIN (n,m,s)) /\ validAttr (n,m,s) /\
is_unsigned (n,m,s) ==>
abs (fxperror (n,m,s) Convergent Clip x) <= inv (2 pow fracbits (n,m,s))
[FXP_MUL] Theorem
|- !a b X.
Isvalid a /\ Isvalid b /\ validAttr X /\
representable X (value a * value b) ==>
Isvalid (FxpMul X a b) /\
(value (FxpMul X a b) =
value a * value b + Fxperror X (value a * value b))
[FXP_MUL_ABSOLUTE_THM] Theorem
|- !a b X.
Isvalid a /\ Isvalid b /\ validAttr X /\
representable X (value a * value b) ==>
Isvalid (FxpMul X a b) /\
?e.
abs e <= inv (2 pow fracbits X) /\
(value (FxpMul X a b) = value a * value b + e)
[FXP_MUL_ISVALID] Theorem
|- !a b X.
Isvalid a /\ Isvalid b /\ validAttr X /\
representable X (value a * value b) ==>
Isvalid (FxpMul X a b)
[FXP_MUL_THM] Theorem
|- !a b n m s.
Isvalid a /\ Isvalid b /\ validAttr (n,m,s) /\
~(value a * value b > MAX (n,m,s)) /\
~(value a * value b < MIN (n,m,s)) ==>
Isvalid (FST (fxpMul (n,m,s) Convergent Clip a b)) /\
(value (FST (fxpMul (n,m,s) Convergent Clip a b)) =
value a * value b + fxperror (n,m,s) Convergent Clip (value a * value b))
[FXP_SUB] Theorem
|- !a b X.
Isvalid a /\ Isvalid b /\ validAttr X /\
representable X (value a - value b) ==>
Isvalid (FxpSub X a b) /\
(value (FxpSub X a b) =
value a - value b + Fxperror X (value a - value b))
[FXP_SUB_ABSOLUTE_THM] Theorem
|- !a b X.
Isvalid a /\ Isvalid b /\ validAttr X /\
representable X (value a - value b) ==>
Isvalid (FxpSub X a b) /\
?e.
abs e <= inv (2 pow fracbits X) /\
(value (FxpSub X a b) = value a - value b + e)
[FXP_SUB_ISVALID] Theorem
|- !a b X.
Isvalid a /\ Isvalid b /\ validAttr X /\
representable X (value a - value b) ==>
Isvalid (FxpSub X a b)
[FXP_SUB_THM] Theorem
|- !a b n m s.
Isvalid a /\ Isvalid b /\ validAttr (n,m,s) /\
~(value a - value b > MAX (n,m,s)) /\
~(value a - value b < MIN (n,m,s)) ==>
Isvalid (FST (fxpSub (n,m,s) Convergent Clip a b)) /\
(value (FST (fxpSub (n,m,s) Convergent Clip a b)) =
value a - value b + fxperror (n,m,s) Convergent Clip (value a - value b))
[INSTANCE] Theorem
|- {a |
FST (SND a) < 257 /\ FST (SND (SND a)) < FST (SND a) + 1 /\
SND (SND (SND a)) < 2 /\ (WORDLEN (FST a) = FST (SND a))} SUBSET
{a |
FST (SND a) < 257 /\ FST (SND (SND a)) < 257 /\ SND (SND (SND a)) < 2 /\
(WORDLEN (FST a) = FST (SND a))}
[INSTANCEFINITE] Theorem
|- FINITE
{a |
FST (SND a) < 257 /\ FST (SND (SND a)) < 257 /\ SND (SND (SND a)) < 2 /\
(WORDLEN (FST a) = FST (SND a))}
[INTBITS] Theorem
|- !X. intbits X = FST (SND X)
[ISVALIDNBWORD] Theorem
|- !n m s k. validAttr (n,m,s) ==> is_valid (NBWORD n k,n,m,s)
[ISVALIDREPLICATE] Theorem
|- !n m s. validAttr (n,m,s) ==> is_valid (WORD (REPLICATE n T),n,m,s)
[ISVALIDREPLICATEF] Theorem
|- !n m s. validAttr (n,m,s) ==> is_valid (WORD (REPLICATE n F),n,m,s)
[ISVALIDWORDLEN] Theorem
|- !w m s. validAttr (WORDLEN w,m,s) ==> is_valid (w,WORDLEN w,m,s)
[ISVALID_ATTR_IMAGE] Theorem
|- !n m s.
{a | Isvalid a /\ (Attrib a = (n,m,s))} =
IMAGE fxp {a | is_valid a /\ (attrib a = (n,m,s))}
[ISVALID_ATTR_SUB] Theorem
|- !n m s. {a | is_valid a /\ (attrib a = (n,m,s))} SUBSET {a | is_valid a}
[ISVALID_SUB] Theorem
|- {a | is_valid a} SUBSET
{a |
FST (SND a) < 257 /\ FST (SND (SND a)) < FST (SND a) + 1 /\
SND (SND (SND a)) < 2 /\ (WORDLEN (FST a) = FST (SND a))}
[ISVALID_WCAT] Theorem
|- !n m s k.
validAttr (n,m,s) ==> is_valid (WCAT (WORD [F],NBWORD (n - 1) k),n,m,s)
[ISVALID_WCATT] Theorem
|- !n m s k.
validAttr (n,m,s) ==> is_valid (WCAT (WORD [T],NBWORD (n - 1) k),n,m,s)
[ISVALISPECIAL] Theorem
|- is_valid (WORD (REPLICATE 2 T),2,1,1)
[IS_FXP_CLOSEST_EXISTS] Theorem
|- !v x s. FINITE s ==> ~(s = {}) ==> ?a. is_fxp_closest v s x a
[IS_VALID_ATTRIB_NONEMPTY] Theorem
|- !n m s.
validAttr (n,m,s) ==> ~({a | Isvalid a /\ (Attrib a = (n,m,s))} = {})
[IS_VALID_FXP_CLOSEST] Theorem
|- !v p x n m s.
validAttr (n,m,s) ==>
Isvalid (fxp_closest v p {a | Isvalid a /\ (Attrib a = (n,m,s))} x)
[IS_VALID_NONEMPTY] Theorem
|- ~({a | Isvalid a} = {})
[IS_VALID_ROUND_CONV_CLIP] Theorem
|- !n m s x.
validAttr (n,m,s) /\ ~(x > MAX (n,m,s)) /\ ~(x < MIN (n,m,s)) ==>
Isvalid (FST (fxp_round (n,m,s) Convergent x Clip))
[LASTN1] Theorem
|- !n k. LASTN n (F::NLIST n VB 2 k) = LASTN n (NLIST n VB 2 k)
[MAINFINITE] Theorem
|- FINITE
{a |
FST (SND a) < 257 /\ FST (SND (SND a)) < FST (SND a) + 1 /\
SND (SND (SND a)) < 2 /\ (WORDLEN (FST a) = FST (SND a))}
[MATCHFINITE] Theorem
|- {a |
FST (SND a) < 257 /\ FST (SND (SND a)) < FST (SND a) + 1 /\
SND (SND (SND a)) < 2 /\ (WORDLEN (FST a) = FST (SND a))} SUBSET
{a |
FST (SND a) < 257 /\ FST (SND (SND a)) < 257 /\ SND (SND (SND a)) < 2 /\
(WORDLEN (FST a) = FST (SND a))} ==>
FINITE
{a |
FST (SND a) < 257 /\ FST (SND (SND a)) < FST (SND a) + 1 /\
SND (SND (SND a)) < 2 /\ (WORDLEN (FST a) = FST (SND a))}
[MATCHFINITEVALID] Theorem
|- {a | is_valid a} SUBSET
{a |
FST (SND a) < 257 /\ FST (SND (SND a)) < FST (SND a) + 1 /\
SND (SND (SND a)) < 2 /\ (WORDLEN (FST a) = FST (SND a))} ==>
FINITE {a | is_valid a}
[MATCHFINITEVALIDATTR] Theorem
|- !n m s.
{a | is_valid a /\ (attrib a = (n,m,s))} SUBSET {a | is_valid a} ==>
FINITE {a | is_valid a /\ (attrib a = (n,m,s))}
[NOTTiIsigned] Theorem
|- !n m s k.
validAttr (n,m,s) /\ ~is_unsigned (n,m,s) ==>
~Isunsigned (fxp (WCAT (WORD [T],NBWORD (n - 1) k),n,m,s))
[NOTiIsigned] Theorem
|- !n m s k.
validAttr (n,m,s) /\ ~is_unsigned (n,m,s) ==>
~Isunsigned (fxp (WCAT (WORD [F],NBWORD (n - 1) k),n,m,s))
[PWFLT_REAL] Theorem
|- !n m s y.
x <= y / 2 pow fracbits (n,m,s) =
2 pow fracbits (n,m,s) * x <=
2 pow fracbits (n,m,s) * (y / 2 pow fracbits (n,m,s))
[PWL1] Theorem
|- WORD [F] IN PWORDLEN 1
[PWLGSNBW] Theorem
|- !n k. WORD (NLIST n VB 2 k) IN PWORDLEN n
[REAL_BNVAL_NBWORD] Theorem
|- !n k. k < 2 ** n ==> (& (BNVAL (NBWORD n k)) = & k)
[REAL_OF_NUM_GT] Theorem
|- !m n. & m > & n = m > n
[REAL_OF_NUM_SUB] Theorem
|- !m n. m <= n ==> (& n - & m = & (n - m))
[REPLICATELENGTH] Theorem
|- !n. LENGTH (REPLICATE n T) = n
[REPLICATELENGTHF] Theorem
|- !n. LENGTH (REPLICATE n F) = n
[SIGN] Theorem
|- !X. signtype X = SND (SND X)
[STREAM] Theorem
|- !a. stream a = FST a
[STREAMLEN] Theorem
|- !X. streamlength X = FST X
[TWOEXP] Theorem
|- !n. 2 ** n - 1 < 2 ** n
[TWOEXPGE1] Theorem
|- !n. 1 <= 2 ** n
[WORDBASIS] Theorem
|- FINITE {w | WORDLEN w = 0} = FINITE {WORD []}
[WORDFINITE] Theorem
|- !x. FINITE {w | WORDLEN w = x}
[WORDINDUCT] Theorem
|- !n.
{w | WORDLEN w = SUC n} =
IMAGE (\w. WCAT (WORD [T],w)) {w | WORDLEN w = n} UNION
IMAGE (\w. WCAT (WORD [F],w)) {w | WORDLEN w = n}
[WORDPAIRIMAGE] Theorem
|- !n.
{(w,x) | (WORDLEN w = x) /\ (x = n)} =
IMAGE (\w. (w,WORDLEN w)) {w | WORDLEN w = n}
[datatype_Exception] Theorem
|- DATATYPE (Exception no_except overflow invalid loss_sign)
[datatype_fxp_roundmode] Theorem
|- DATATYPE (fxp_roundmode Round To_zero To_plus_infinity Truncate Convergent)
[datatype_overflowmode] Theorem
|- DATATYPE (overflowmode Wrap Clip)
[fxp_roundmode2num_11] Theorem
|- !a a'. (fxp_roundmode2num a = fxp_roundmode2num a') = (a = a')
[fxp_roundmode2num_ONTO] Theorem
|- !r. r < 5 = ?a. r = fxp_roundmode2num a
[fxp_roundmode2num_num2fxp_roundmode] Theorem
|- !r. r < 5 = (fxp_roundmode2num (num2fxp_roundmode r) = r)
[fxp_roundmode2num_thm] Theorem
|- (fxp_roundmode2num Round = 0) /\ (fxp_roundmode2num To_zero = 1) /\
(fxp_roundmode2num To_plus_infinity = 2) /\
(fxp_roundmode2num Truncate = 3) /\ (fxp_roundmode2num Convergent = 4)
[fxp_roundmode_Axiom] Theorem
|- !x0 x1 x2 x3 x4.
?f.
(f Round = x0) /\ (f To_zero = x1) /\ (f To_plus_infinity = x2) /\
(f Truncate = x3) /\ (f Convergent = x4)
[fxp_roundmode_EQ_fxp_roundmode] Theorem
|- !a a'. (a = a') = (fxp_roundmode2num a = fxp_roundmode2num a')
[fxp_roundmode_case_cong] Theorem
|- !M M' v0 v1 v2 v3 v4.
(M = M') /\ ((M' = Round) ==> (v0 = v0')) /\
((M' = To_zero) ==> (v1 = v1')) /\
((M' = To_plus_infinity) ==> (v2 = v2')) /\
((M' = Truncate) ==> (v3 = v3')) /\ ((M' = Convergent) ==> (v4 = v4')) ==>
((case M of
Round -> v0
|| To_zero -> v1
|| To_plus_infinity -> v2
|| Truncate -> v3
|| Convergent -> v4) =
case M' of
Round -> v0'
|| To_zero -> v1'
|| To_plus_infinity -> v2'
|| Truncate -> v3'
|| Convergent -> v4')
[fxp_roundmode_case_def] Theorem
|- (!v0 v1 v2 v3 v4.
(case Round of
Round -> v0
|| To_zero -> v1
|| To_plus_infinity -> v2
|| Truncate -> v3
|| Convergent -> v4) =
v0) /\
(!v0 v1 v2 v3 v4.
(case To_zero of
Round -> v0
|| To_zero -> v1
|| To_plus_infinity -> v2
|| Truncate -> v3
|| Convergent -> v4) =
v1) /\
(!v0 v1 v2 v3 v4.
(case To_plus_infinity of
Round -> v0
|| To_zero -> v1
|| To_plus_infinity -> v2
|| Truncate -> v3
|| Convergent -> v4) =
v2) /\
(!v0 v1 v2 v3 v4.
(case Truncate of
Round -> v0
|| To_zero -> v1
|| To_plus_infinity -> v2
|| Truncate -> v3
|| Convergent -> v4) =
v3) /\
!v0 v1 v2 v3 v4.
(case Convergent of
Round -> v0
|| To_zero -> v1
|| To_plus_infinity -> v2
|| Truncate -> v3
|| Convergent -> v4) =
v4
[fxp_roundmode_distinct] Theorem
|- ~(Round = To_zero) /\ ~(Round = To_plus_infinity) /\ ~(Round = Truncate) /\
~(Round = Convergent) /\ ~(To_zero = To_plus_infinity) /\
~(To_zero = Truncate) /\ ~(To_zero = Convergent) /\
~(To_plus_infinity = Truncate) /\ ~(To_plus_infinity = Convergent) /\
~(Truncate = Convergent)
[fxp_roundmode_induction] Theorem
|- !P.
P Convergent /\ P Round /\ P To_plus_infinity /\ P To_zero /\
P Truncate ==>
!a. P a
[fxp_roundmode_nchotomy] Theorem
|- !a.
(a = Round) \/ (a = To_zero) \/ (a = To_plus_infinity) \/
(a = Truncate) \/ (a = Convergent)
[iIsigned] Theorem
|- !n m s k.
validAttr (n,m,s) /\ is_unsigned (n,m,s) ==>
Isunsigned (fxp (NBWORD n k,n,m,s))
[invfracge0] Theorem
|- !n m s. 0 <= inv (2 pow fracbits (n,m,s))
[invfracgt0] Theorem
|- !n m s. 0 < inv (2 pow fracbits (n,m,s))
[maxmin] Theorem
|- !x n m s.
~(x > MAX (n,m,s)) /\ ~(x < MIN (n,m,s)) /\ validAttr (n,m,s) /\
~is_unsigned (n,m,s) ==>
abs x <= 2 pow (streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s) /\
validAttr (n,m,s) /\ ~is_unsigned (n,m,s)
[num2Exception_11] Theorem
|- !r r'.
r < 4 ==> r' < 4 ==> ((num2Exception r = num2Exception r') = (r = r'))
[num2Exception_Exception2num] Theorem
|- !a. num2Exception (Exception2num a) = a
[num2Exception_ONTO] Theorem
|- !a. ?r. (a = num2Exception r) /\ r < 4
[num2Exception_thm] Theorem
|- (num2Exception 0 = no_except) /\ (num2Exception 1 = overflow) /\
(num2Exception 2 = invalid) /\ (num2Exception 3 = loss_sign)
[num2fxp_roundmode_11] Theorem
|- !r r'.
r < 5 ==>
r' < 5 ==>
((num2fxp_roundmode r = num2fxp_roundmode r') = (r = r'))
[num2fxp_roundmode_ONTO] Theorem
|- !a. ?r. (a = num2fxp_roundmode r) /\ r < 5
[num2fxp_roundmode_fxp_roundmode2num] Theorem
|- !a. num2fxp_roundmode (fxp_roundmode2num a) = a
[num2fxp_roundmode_thm] Theorem
|- (num2fxp_roundmode 0 = Round) /\ (num2fxp_roundmode 1 = To_zero) /\
(num2fxp_roundmode 2 = To_plus_infinity) /\
(num2fxp_roundmode 3 = Truncate) /\ (num2fxp_roundmode 4 = Convergent)
[num2overflowmode_11] Theorem
|- !r r'.
r < 2 ==>
r' < 2 ==>
((num2overflowmode r = num2overflowmode r') = (r = r'))
[num2overflowmode_ONTO] Theorem
|- !a. ?r. (a = num2overflowmode r) /\ r < 2
[num2overflowmode_overflowmode2num] Theorem
|- !a. num2overflowmode (overflowmode2num a) = a
[num2overflowmode_thm] Theorem
|- (num2overflowmode 0 = Wrap) /\ (num2overflowmode 1 = Clip)
[opopow] Theorem
|- !n m s.
0 < streamlength (n,m,s) ==>
1 + & (streamlength (n,m,s)) * 1 <= (1 + 1) pow streamlength (n,m,s)
[opstream] Theorem
|- !n m s.
0 < streamlength (n,m,s) ==> 1 + 0 < 1 + & (streamlength (n,m,s)) * 1
[opstream1] Theorem
|- !n m s.
0 < streamlength (n,m,s) ==> 1 + 0 < (1 + 1) pow streamlength (n,m,s)
[otwoexpsl] Theorem
|- !n m s.
validAttr (n,m,s) ==>
(1 + (2 ** streamlength (n,m,s) - 1) = 2 ** streamlength (n,m,s))
[otwoexpsl1] Theorem
|- !n m s.
validAttr (n,m,s) ==>
(2 ** streamlength (n,m,s) - 1 + 1 = 2 ** streamlength (n,m,s))
[otwoexpsl11] Theorem
|- !n m s.
validAttr (n,m,s) ==>
(2 pow streamlength (n,m,s) - 1 = & (2 ** streamlength (n,m,s) - 1))
[overflowmode2num_11] Theorem
|- !a a'. (overflowmode2num a = overflowmode2num a') = (a = a')
[overflowmode2num_ONTO] Theorem
|- !r. r < 2 = ?a. r = overflowmode2num a
[overflowmode2num_num2overflowmode] Theorem
|- !r. r < 2 = (overflowmode2num (num2overflowmode r) = r)
[overflowmode2num_thm] Theorem
|- (overflowmode2num Wrap = 0) /\ (overflowmode2num Clip = 1)
[overflowmode_Axiom] Theorem
|- !x0 x1. ?f. (f Wrap = x0) /\ (f Clip = x1)
[overflowmode_EQ_overflowmode] Theorem
|- !a a'. (a = a') = (overflowmode2num a = overflowmode2num a')
[overflowmode_case_cong] Theorem
|- !M M' v0 v1.
(M = M') /\ ((M' = Wrap) ==> (v0 = v0')) /\
((M' = Clip) ==> (v1 = v1')) ==>
((case M of Wrap -> v0 || Clip -> v1) =
case M' of Wrap -> v0' || Clip -> v1')
[overflowmode_case_def] Theorem
|- (!v0 v1. (case Wrap of Wrap -> v0 || Clip -> v1) = v0) /\
!v0 v1. (case Clip of Wrap -> v0 || Clip -> v1) = v1
[overflowmode_distinct] Theorem
|- ~(Wrap = Clip)
[overflowmode_induction] Theorem
|- !P. P Clip /\ P Wrap ==> !a. P a
[overflowmode_nchotomy] Theorem
|- !a. (a = Wrap) \/ (a = Clip)
[pwv23le1] Theorem
|- !x n. & n / 2 pow 23 <= x = 2 pow 23 * (& n / 2 pow 23) <= 2 pow 23 * x
[pwv23le11] Theorem
|- !x n. & n / 2 pow 23 <= x = & n <= 2 pow 23 * x
[pwv23lt] Theorem
|- !x. x < & n / 2 pow 23 = 2 pow 23 * x < 2 pow 23 * (& n / 2 pow 23)
[pwv23lt1] Theorem
|- !n. & n / 2 pow 23 < 1 = 2 pow 23 * (& n / 2 pow 23) < 2 pow 23 * 1
[pwv23lt11] Theorem
|- !x. & n / 2 pow 23 < 1 = & n < 2 pow 23
[pwvexp126lt1] Theorem
|- !x. x < inv (2 pow 126) = 2 pow 126 * x < 2 pow 126 * inv (2 pow 126)
[pwvexp126lt11] Theorem
|- !x. x < inv (2 pow 126) = 2 pow 126 * x < 1
[pwvexp23gt] Theorem
|- !n. n < 2 ** 23 = & n < 2 pow 23
[pwvexp23lt] Theorem
|- !n. n > 2 ** 23 = 2 pow 23 < & n
[pwvexp23lt1] Theorem
|- !x. x < 1 = 2 pow 23 * x < 2 pow 23 * 1
[pwvexp23lt11] Theorem
|- !x. x < 1 = 2 pow 23 * x < 2 pow 23
[pwvexpfraclt] Theorem
|- !n m s y. y > 2 ** fracbits (n,m,s) = 2 pow fracbits (n,m,s) < & y
[pwvexpfraclt1] Theorem
|- !n m s x. x < 1 = 2 pow fracbits (n,m,s) * x < 2 pow fracbits (n,m,s) * 1
[pwvfracle1] Theorem
|- !x n m s.
x <= (2 pow streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s) =
2 pow fracbits (n,m,s) * x <=
2 pow fracbits (n,m,s) *
((2 pow streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s))
[pwvfracle11] Theorem
|- !x n m s.
x <= (2 pow streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s) =
2 pow fracbits (n,m,s) * x <= 2 pow streamlength (n,m,s) - 1
[pwvfracle111] Theorem
|- !x n m s.
x <= 2 pow (streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s) =
2 pow fracbits (n,m,s) * x <= 2 pow (streamlength (n,m,s) - 1)
[pwvfracle2] Theorem
|- !x n m s.
& k / 2 pow fracbits (n,m,s) <= x =
2 pow fracbits (n,m,s) * (& k / 2 pow fracbits (n,m,s)) <=
2 pow fracbits (n,m,s) * x
[pwvfracle21] Theorem
|- !x n m s.
& k / 2 pow fracbits (n,m,s) <= x = & k <= 2 pow fracbits (n,m,s) * x
[pwvfraclereal] Theorem
|- !n m s y.
x < y / 2 pow fracbits (n,m,s) =
2 pow fracbits (n,m,s) * x <
2 pow fracbits (n,m,s) * (y / 2 pow fracbits (n,m,s))
[pwvfraclt] Theorem
|- !n m s y.
x < & y / 2 pow fracbits (n,m,s) =
2 pow fracbits (n,m,s) * x <
2 pow fracbits (n,m,s) * (& y / 2 pow fracbits (n,m,s))
[pwvfraclt1] Theorem
|- !n m s y.
& y / 2 pow fracbits (n,m,s) < 1 =
2 pow fracbits (n,m,s) * (& y / 2 pow fracbits (n,m,s)) <
2 pow fracbits (n,m,s) * 1
[pwvfraclt11] Theorem
|- !n m s y. & y / 2 pow fracbits (n,m,s) < 1 = & y < 2 pow fracbits (n,m,s)
[pwvfraclt111] Theorem
|- !x n m s.
x < 2 pow (streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s) =
2 pow fracbits (n,m,s) * x < 2 pow (streamlength (n,m,s) - 1)
[pwvfraclt2] Theorem
|- !x n m s.
& k / 2 pow fracbits (n,m,s) < x =
2 pow fracbits (n,m,s) * (& k / 2 pow fracbits (n,m,s)) <
2 pow fracbits (n,m,s) * x
[pwvfraclt21] Theorem
|- !x n m s.
& k / 2 pow fracbits (n,m,s) < x = & k < 2 pow fracbits (n,m,s) * x
[pwvfracltt1] Theorem
|- !x n m s.
x < 2 pow (streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s) =
2 pow fracbits (n,m,s) * x <
2 pow fracbits (n,m,s) *
(2 pow (streamlength (n,m,s) - 1) / 2 pow fracbits (n,m,s))
[s3] Theorem
|- !n m s.
(2 pow (streamlength (n,m,s) - 1) - 1) * inv (2 pow fracbits (n,m,s)) <=
2 pow (streamlength (n,m,s) - 1) * inv (2 pow fracbits (n,m,s))
[twoexpsl] Theorem
|- !n m s. validAttr (n,m,s) ==> 1 <= 2 ** streamlength (n,m,s)
[twoone] Theorem
|- 2 = 1 + 1
*)
end
HOL 4, Kananaskis-3