Introduction

Selected Objects

DEF	bool	== Unit+Unit
DEF	btrue	true ==
DEF	bfalse	false ==
DEF	ifthenelse	if b t else f fi == dec(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=jtrue; false fi
DEF	lt_int	i < z j == if i < j true ; false fi
DEF	eq_atom	x=yAtom == if x=yAtomtrue; false fi
DEF	le_int	i z j == j < z 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:. i z j = j < z 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 xy
THM	neg_assert_of_eq_atom	x,y:Atom. x=yAtom xy
THM	assert_of_lt_int	x,y:. x < z 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:. x z y 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:. ij (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 ij
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)