THM	decidable_iff_exists_bool_function	T:. P:T . (x:T. Dec(P[x])) (f_p:T . x:T. P[x] (f_p x))
THM	decidable_iff_exists_bool_function_2	T,Z:. P:T Z . (x:T. y:Z. Dec(P[x;y])) (f_p:T Z . x:T. y:Z. P[x;y] (f_p x y))
ML	decidable_to_bool_constructor	% caldwell - 27 March 1994 % % This file contains the ideas for ML code to construct a boolean equality for a type <T> by using the extract of a theorem "decidable__T". Extraction was not working in Nuprl 4.0 and the file has not been brought up to date with release 4.1 % % let mk_bool_from_decidable_prop (t :tok) = let name = (tok_to_string t) in let concat = concatenate_strings in let type = (mk_term (t,[]) []) in let f_name = (t ^ `_2`) in let f_name_str = (tok_to_string f_name) in let bool = (mk_term (`bool`, []) []) in create_object (f_name ^ `_df`) "disp" (concat ["after decidable__" name]); string_to_object_body (concat [name; ":{<i:level>}(<x:T>) ==" f_name_str; "{<i>:l}(< x>);;" name; "(<x:T>) ==" f_name_str; "{\\\\v:l}(<x>);;"]) (f_name ^ `_df`); create_abs_obj (string_to_term (concat [f_name_str; "{\\\\v:l}"])) (let pi1 = (string_to_term "lambda(x.spread(x;z,w.z))") in (fst (ReduceC null_env (mk_apply_term pi1 (mk_apply_term (beta_reduce_term (mk_apply_term (extract_of_thm_object `decidable_iff_exists_bool_function_2`) type)) (extract_of_thm_object (`decidable__` ^ t))))))) f_name (concat ["after " f_name_str; "_df"]); create_thm_obj (mk_member_term (mk_function_term null_var type (mk_function_term null_var type bool)) (string_to_term (concat [f_name_str; "{\\\\v:l}"]))) (concat [ "Try (Unfolds ``" f_name_str; " " name; "`` 0"]) (f_name ^ `_wf`) (concat ["after " f_name_str]) ;; %
THM	sq_stable_functionality_wrt_or	P,Q:. SqStable(P) SqStable(Q) {SqStable(P Q) SqStable(P) SqStable(Q)}
THM	sq_stable__or	P,Q:. Dec(P) Dec(Q) SqStable(P Q)
THM	decidable_functionality_wrt_iff	P,Q:. {P Q} {Dec(P) Dec(Q)}
THM	decidable__true	Dec(True)
THM	decidable__equal_nil	T:. Dec([] = [])
THM	demorgan	P,Q:. Dec(P) Dec(Q) {(P Q) P Q}
THM	demorgan1	P,Q:. Dec(P) Dec(Q) {(P Q) P Q}
THM	demorgan2	P,Q:. Dec(P) Dec(Q) {(P Q) P Q}
THM	contrapositive	P,Q:. Dec(P) Dec(Q) {(P Q) (Q P)}
THM	pair_functionality_wrt_equal	T,U:. t1,t2:T. u1,u2:U. {t1 = t2} {u1 = u2} {<t1, u1> = <t2, u2>}
DISP	equivalence_df	{<T:type:L>}== {<T>}
ABS	equivalence	{T} == {f:T T | (x:T. (f x x)) (x,y:T. (f x y) (f y x)) (x,y,z:T. (f x y) (f y z) (f x z))}
THM	equivalence_wf	T:. {T} '
THM	equivalence_inc	T:. {T} T T
THM	discrete_equality_inc_equivalence	T:. {T=} {T}
THM	equivalence_type	T:. eq:{T}. eq T T
THM	equivalence_properties	T:. f:{T}. (x,y,z:T. (f x y) (f y z) (f x z)) (x,y:T. (f x y) (f y x)) (x:T. (f x x)) f T T
THM	equivalence_symmetric	T:. eq:{T}. x,y:T. (eq x y) (eq y x)
ML	equiv_tac	let is_equivalence_term t = (opid_of_term t) = `equivalence` ;; let Equivalence i p = (let T = type_of_hyp i p in let i = get_pos_hyp_num i p in if is_equivalence_term T then let name = mk_var_term (var_of_hyp i p) in let type = hd (subterms_of_term T) in InstLemma `equivalence_properties` [type;name] THENA Auto THEN RepeatFor 3 (D (-1) THEN CopyToHyp (i + 1) (-2) THEN Thin (-2)) THEN CopyToHyp (i + 1) (-1) THEN Thin (-1) else failwith `Equivalence: hyp is not an equivalence term.` )p ;; let EquivT i p = (let T = type_of_hyp i p in let i = get_pos_hyp_num i p in if is_equivalence_term T then let name = mk_var_term (var_of_hyp i p) in let type = hd (subterms_of_term T) in InstLemma `equivalence_type` [type;name] THENA Auto THEN CopyToHyp (i + 1) (-1) THEN Thin (-1) else failwith `EquivT: hyp is not an equivalence term.` )p ;;
THM	equivalence_bool_function	T:. eq:{T}. eq T T
THM	equivalence_reflexive	T:. eq:{T}. u:T. (eq u u)
THM	discrete_equality_is_equivalence	T:. EQ:{T=}. EQ {T}
THM	equivalence_weakening_lemma	T:. eq:{T=}. f:{T}. x,y:T. (eq x y) (f x y)
THM	not_equivalence_implies_not_discrete_eq	T:. eq:{T}. f:{T=}. x,y:T. (eq x y) (f x y)
THM	decidable__spread	T,U:. P:T U . (x:T. y:U. Dec(P[x;y])) (p:T U. Dec(let <l,r> = p in P[l;r]))
THM	not_not_rw	T:. P:T . (x:T. Dec(P[x])) (x:T. P[x] P[x])

the other theories