bool_1 Theory

Theorems include standard logic ones, as well as `assert' theorems for converting between boolean and prop-valued predicates.

This implementation of bool differs from that in Nuprl V3. There, the booleans were defined as a subtype of the integers. Here, the use of the Unit + Unit type enables evaluation of boolean expressions, especially those involving ifthenelse, using Nuprl's direct computation rules. This is of great help when these expressions are used in definitions of recursive functions, whose proof of well-formedness relies heavily on direct-computation-style reasoning.

Summary of Definitions

Typed Definitions

bool *1

btrue *1

bfalse *2

ifthenelse *3

assert *1

b2i *1

bnot *1

band *1

bor *1

eq_bool *1

bxor *1

bimplies *1

rev_bimplies *1

eq_int *1

lt_int *1

eq_atom *1

le_int *1

Main Theorems

b2i_bounds *2

btrue_neq_bfalse *4

bool_cases *5

bool_ind *3

decidable__equal_bool *13

bnot_bnot_elim *4

bnot_thru_band *3

bnot_thru_bor *3

bnot_of_le_int *4

bnot_of_lt_int *1

bimplies_weakening *4

bimplies_transitivity *2

assert_functionality_wrt_bimplies *4

bor_ff_simp *1

bor_tt_simp *1

band_ff_simp *1

band_tt_simp *1

assert_of_tt *1

assert_of_ff *2

assert_elim *5

not_assert_elim *4

eqtt_to_assert *8

eqff_to_assert *10

decidable__assert *6

iff_imp_equal_bool *6

assert_of_eq_atom *8

assert_of_eq_int *10

neg_assert_of_eq_int *4

neg_assert_of_eq_atom *4

assert_of_lt_int *8

assert_of_eq_int_rw *1

assert_of_eq_bool *7

assert_of_bnot *12

assert_of_band *10

assert_of_bor *14

assert_of_bimplies *3

assert_of_le_int *4

ite_rw_test *2

ite_rw_false *2

ite_rw_true *2

fun_thru_ite *1

eq_int_eq_false *2

eq_int_eq_true *2

eq_int_eq_false_elim *7

eq_int_eq_true_elim *7

eq_int_cases_test *7