Origin Definitions Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
bool_1
Nuprl Section: bool_1

Selected Objects
IntroductionIntroductory Remarks
defbool  == Unit+Unit
defbtrue true == inl()
defbfalse false == inr()
defifthenelse if b t else f fi == InjCase(b ; tf)
defassert b == if b True else False fi
defb2i b2i(b) == if b 1 else 0 fi
THMb2i_bounds b:. 0b2i(b) & b2i(b)1
defbnot b == if b false else true fi
defband pq == if p q else false fi
defbor p  q == if p true else q fi
defeq_bool p=q == (pq (pq)
defbxor pq == (pq (pq)
defbimplies pq == p  q
defrev_bimplies pq == qp
defeq_int i=j == if i=j true ; false fi
deflt_int i<j == if i<j true ; false fi
defeq_atom x=yAtom == if x=yAtomtrue; false fi
defle_int ij == j<i
COMbool_thms ================GENERAL THEOREMS================
THMbtrue_neq_bfalse true = false
THMbool_cases b:b = true  b = false
THMbool_ind P:(Prop). P(false P(true (b:P(b))
THMdecidable__equal_bool a,b:. Dec(a = b)
THMbnot_bnot_elim p:p = p
THMbnot_thru_band p,q:(pq) = (p  q)
THMbnot_thru_bor p,q:(p  q) = (pq)
THMbnot_of_le_int i,j:ij = (j<i)
THMbimplies_weakening u,v:u = v  uv
THMbimplies_transitivity u,v,w:uv  vw  uw
THMassert_functionality_wrt_bimplies u,v:uv  u  v
COMbool_simp_1 CONSTANT SIMPLIFICATION ...
THMbor_ff_simp u:. (u  false) = u
THMbor_tt_simp u:. (u  true) = true
THMband_ff_simp u:. (ufalse) = false
THMband_tt_simp u:. (utrue) = u
COMassert_com `ASSERT'-RELATED THEOREMS
THMassert_of_tt true
THMassert_of_ff false
THMassert_elim b:b  b = true
THMnot_assert_elim b:b  b = false
THMeqtt_to_assert b:b = true  b
THMeqff_to_assert b:b = false  b
THMdecidable__assert b:. Dec(b)
THMiff_imp_equal_bool a,b:. (a  b a = b
THMassert_of_eq_atom x,y:Atom. x=yAtom  x = y
THMassert_of_eq_int x,y:x=y  x = y
THMneg_assert_of_eq_int x,y:x=y  x  y
THMneg_assert_of_eq_atom x,y:Atom. x=yAtom  x  y
THMassert_of_lt_int x,y:x<y  x<y
THMassert_of_eq_int_rw x,y:x=y  x = y
THMassert_of_eq_bool p,q:p=q  p = q
THMassert_of_bnot p:p  p
THMassert_of_band p,q:. (pq p & q
THMassert_of_bor p,q:. (p  q p  q
THMassert_of_bimplies p,q:pq  (p  q)
THMassert_of_le_int x,y:xy  xy
THMite_rw_test n:i:{1..n}. 0 = 0 & n = 0  False
THMite_rw_false b:x,y:Tb  if b x else y fi = y
THMite_rw_true b:x,y:Tb  if b x else y fi = x
THMfun_thru_ite f:(ST), b:p,q:Sf(if b p else q fi) = if b f(p) else f(q) fi
COMold_bool_1_stuff OLD STUFF ...
THMeq_int_eq_false i,j:i  j  (i=j) = false
THMeq_int_eq_true i,j:i = j  (i=j) = true
THMeq_int_eq_false_elim i,j:. (i=j) = false  i  j
THMeq_int_eq_true_elim i,j:. (i=j) = true  i = j
THMeq_int_cases_test x,y:AP:(AProp), i,j:P(if i=j x else y fi)  P(if i=j x else y fi)
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Origin Definitions Sections StandardLIB Doc