BoolAlg (nholz)

BoolAlg Module

Namespace: HOL
Assembly: nholz.dll

This module proves various algebraic property theorems for the predicate logic operators.

Functions and values

Function or value	Description
`conj_absorb_disj_thm` Full Usage: `conj_absorb_disj_thm` Returns: `thm`	\|- !p q. p /\ (p \/ q) <=> p *) Returns: `thm`
`conj_assoc_thm` Full Usage: `conj_assoc_thm` Returns: `thm`	\|- !p q r. p /\ (q /\ r) <=> (p /\ q) /\ r *) Returns: `thm`
`conj_comm_thm` Full Usage: `conj_comm_thm` Returns: `thm`	\|- !p q. p /\ q <=> q /\ p Returns: `thm`
`conj_contr_thm` Full Usage: `conj_contr_thm` Returns: `thm`	\|- !p. p /\ ~ p <=> false Returns: `thm`
`conj_dist_left_disj_thm` Full Usage: `conj_dist_left_disj_thm` Returns: `thm`	\|- !p q r. (p \/ q) /\ r <=> (p /\ r) \/ (q /\ r) Returns: `thm`
`conj_dist_right_disj_thm` Full Usage: `conj_dist_right_disj_thm` Returns: `thm`	\|- !p q r. p /\ (q \/ r) <=> (p /\ q) \/ (p /\ r) Returns: `thm`
`conj_id_thm` Full Usage: `conj_id_thm` Returns: `thm`	\|- !p. p /\ true <=> p Returns: `thm`
`conj_idem_thm` Full Usage: `conj_idem_thm` Returns: `thm`	\|- !p. p /\ p <=> p Returns: `thm`
`conj_zero_thm` Full Usage: `conj_zero_thm` Returns: `thm`	\|- !p. p /\ false <=> false Returns: `thm`
`disj_absorb_conj_thm` Full Usage: `disj_absorb_conj_thm` Returns: `thm`	\|- !p q. p \/ (p /\ q) <=> p Returns: `thm`
`disj_assoc_thm` Full Usage: `disj_assoc_thm` Returns: `thm`	\|- !p q r. p \/ (q \/ r) <=> (p \/ q) \/ r Returns: `thm`
`disj_comm_thm` Full Usage: `disj_comm_thm` Returns: `thm`	\|- !p q. p \/ q <=> q \/ p Returns: `thm`
`disj_dist_left_conj_thm` Full Usage: `disj_dist_left_conj_thm` Returns: `thm`	\|- !p q r. (p /\ q) \/ r <=> (p \/ r) /\ (q \/ r) Returns: `thm`
`disj_dist_right_conj_thm` Full Usage: `disj_dist_right_conj_thm` Returns: `thm`	\|- !p q r. p \/ (q /\ r) <=> (p \/ q) /\ (p \/ r) Returns: `thm`
`disj_id_thm` Full Usage: `disj_id_thm` Returns: `thm`	\|- !p. p \/ false <=> p Returns: `thm`
`disj_idem_thm` Full Usage: `disj_idem_thm` Returns: `thm`	\|- !p. p \/ p <=> p Returns: `thm`
`disj_zero_thm` Full Usage: `disj_zero_thm` Returns: `thm`	\|- !p. p \/ true <=> true Returns: `thm`
`forall_dist_conj_thm` Full Usage: `forall_dist_conj_thm` Returns: `thm`	\|- !P Q. (!x. P x /\ Q x) <=> (!x. P x) /\ (!x. Q x) Returns: `thm`
`forall_null_thm` Full Usage: `forall_null_thm` Returns: `thm`	\|- !t. (!(x:'a). t) <=> t Returns: `thm`
`forall_one_point_thm` Full Usage: `forall_one_point_thm` Returns: `thm`	\|- !P a. (!x. x = a ==> P x) <=> P a Returns: `thm`
`imp_dist_left_disj_thm` Full Usage: `imp_dist_left_disj_thm` Returns: `thm`	\|- !p q r. (p \/ q ==> r) <=> (p ==> r) /\ (q ==> r) Returns: `thm`
`imp_dist_right_conj_thm` Full Usage: `imp_dist_right_conj_thm` Returns: `thm`	\|- !p q r. (p ==> q /\ r) <=> (p ==> q) /\ (p ==> r) Returns: `thm`
`imp_left_id_thm` Full Usage: `imp_left_id_thm` Returns: `thm`	\|- !p. (true ==> p) <=> p Returns: `thm`
`imp_left_zero_thm` Full Usage: `imp_left_zero_thm` Returns: `thm`	\|- !p. false ==> p Returns: `thm`
`imp_refl_thm` Full Usage: `imp_refl_thm` Returns: `thm`	\|- !p. p ==> p Returns: `thm`
`imp_right_zero_thm` Full Usage: `imp_right_zero_thm` Returns: `thm`	\|- !p. p ==> true Returns: `thm`
`load` Full Usage: `load` Returns: `(string * thm) list`	Force module evaluation Returns: `(string * thm) list`
`not_dist_disj_thm` Full Usage: `not_dist_disj_thm` Returns: `thm`	\|- !p q. ~ (p \/ q) <=> ~ p /\ ~ q Returns: `thm`
`not_false_thm` Full Usage: `not_false_thm` Returns: `thm`	\|- ~ false <=> true Returns: `thm`
`not_true_thm` Full Usage: `not_true_thm` Returns: `thm`	\|- ~ true <=> false Returns: `thm`
`p` Full Usage: `p` Returns: `term`	Returns: `term`
`q` Full Usage: `q` Returns: `term`	Returns: `term`
`r` Full Usage: `r` Returns: `term`	Returns: `term`
`true_not_eq_false_thm` Full Usage: `true_not_eq_false_thm` Returns: `thm`	\|- ~ (true <=> false) Returns: `thm`
`x` Full Usage: `x` Returns: `term`	Returns: `term`