Selected Objects

Introduction		Introductory Remarks
def	bool	== Unit+Unit
def	btrue	true == inl()
def	bfalse	false == inr()
def	ifthenelse	if b t else f fi == InjCase(b ; t; f)
def	assert	b == if b True else False fi
def	b2i	b2i(b) == if b 1 else 0 fi
THM	b2i_bounds	b:. 0b2i(b) & b2i(b)1
def	bnot	b == if b false else true fi
def	band	pq == if p q else false fi
def	bor	p  q == if p true else q fi
def	eq_bool	p=q == (pq)  (pq)
def	bxor	pq == (pq)  (pq)
def	bimplies	pq == p  q
def	rev_bimplies	pq == qp
def	eq_int	i=j == if i=j true ; false fi
def	lt_int	i<j == if i<j true ; false fi
def	eq_atom	x=yAtom == if x=yAtomtrue; false fi
def	le_int	ij == j<i
COM	bool_thms	================GENERAL THEOREMS================
THM	btrue_neq_bfalse	true = false
THM	bool_cases	b:. b = true  b = false
THM	bool_ind	P:(Prop). P(false)  P(true)  (b:. P(b))
THM	decidable__equal_bool	a,b:. Dec(a = b)
THM	bnot_bnot_elim	p:. p = p
THM	bnot_thru_band	p,q:. (pq) = (p  q)
THM	bnot_thru_bor	p,q:. (p  q) = (pq)
THM	bnot_of_le_int	i,j:. ij = (j<i)
THM	bimplies_weakening	u,v:. u = v  uv
THM	bimplies_transitivity	u,v,w:. uv  vw  uw
THM	assert_functionality_wrt_bimplies	u,v:. uv  u  v
COM	bool_simp_1	CONSTANT SIMPLIFICATION ...
THM	bor_ff_simp	u:. (u  false) = u
THM	bor_tt_simp	u:. (u  true) = true
THM	band_ff_simp	u:. (ufalse) = false
THM	band_tt_simp	u:. (utrue) = u
COM	assert_com	`ASSERT'-RELATED THEOREMS
THM	assert_of_tt	true
THM	assert_of_ff	false
THM	assert_elim	b:. b  b = true
THM	not_assert_elim	b:. b  b = false
THM	eqtt_to_assert	b:. b = true  b
THM	eqff_to_assert	b:. b = false  b
THM	decidable__assert	b:. Dec(b)
THM	iff_imp_equal_bool	a,b:. (a  b)  a = b
THM	assert_of_eq_atom	x,y:Atom. x=yAtom  x = y
THM	assert_of_eq_int	x,y:. x=y  x = y
THM	neg_assert_of_eq_int	x,y:. x=y  x  y
THM	neg_assert_of_eq_atom	x,y:Atom. x=yAtom  x  y
THM	assert_of_lt_int	x,y:. x<y  x<y
THM	assert_of_eq_int_rw	x,y:. x=y  x = y
THM	assert_of_eq_bool	p,q:. p=q  p = q
THM	assert_of_bnot	p:. p  p
THM	assert_of_band	p,q:. (pq)  p & q
THM	assert_of_bor	p,q:. (p  q)  p  q
THM	assert_of_bimplies	p,q:. pq  (p  q)
THM	assert_of_le_int	x,y:. xy  xy
THM	ite_rw_test	n:, i:{1..n}. 0 = 0 & n = 0  False
THM	ite_rw_false	b:, x,y:T. b  if b x else y fi = y
THM	ite_rw_true	b:, x,y:T. b  if b x else y fi = x
THM	fun_thru_ite	f:(ST), b:, p,q:S. f(if b p else q fi) = if b f(p) else f(q) fi
COM	old_bool_1_stuff	OLD STUFF ...
THM	eq_int_eq_false	i,j:. i  j  (i=j) = false
THM	eq_int_eq_true	i,j:. i = j  (i=j) = true
THM	eq_int_eq_false_elim	i,j:. (i=j) = false  i  j
THM	eq_int_eq_true_elim	i,j:. (i=j) = true  i = j
THM	eq_int_cases_test	x,y:A, P:(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