acl2/ml/acl2encodeLib.sml

24 val bool = ``:bool``;
169     val _ = add_translation sexp bool
170     val _ = add_coding_function sexp bool "encode"
171         {const = ``bool``,definition = translateTheory.bool_def,
173     val _ = add_coding_function sexp bool "decode"
176     val _ = add_coding_function sexp bool "detect"
181     val _ = add_source_function bool "map"
183     val _ = add_source_function bool "all"
185     val _ = add_coding_function sexp bool "fix"
189     val _ = add_coding_theorem sexp bool "encode_decode_map"
191     val _ = add_coding_theorem sexp bool "encode_detect_all"
193     val _ = add_coding_theorem sexp bool "decode_encode_fix"
195     val _ = add_coding_theorem sexp bool "encode_map_encode"
196             (simple_encode_map_encode ``bool``)
197     val _ = add_coding_theorem sexp bool "fix_id"
199     val _ = add_source_theorem bool "map_compose" (simple_map_compose bool);
201     val _ = add_coding_theorem sexp bool "detect_dead"
203     val _ = add_coding_theorem sexp bool "general_detect"
418     (list_ind,[(``P0:sexp -> bool``,(``sexp_to_list f``,list)),
419                (``P1:sexp -> bool``,(``sexp_to_pair f (sexp_to_list f)``,
422     (list_ind,[(``P0:sexp -> bool``,(``listp f``,list)),
423                (``P1:sexp -> bool``,(``pairp f (listp f)``,
426     (list_ind,[(``P0:sexp -> bool``,(``fix_list f``,list)),
427                (``P1:sexp -> bool``,(``fix_pair f (fix_list f)``,
432     [(``P:'a list -> bool``,(``list f``,list))]);
435     [(``P:'a list -> bool``,(``MAP f``,list))]);
438     [(``P:'a list -> bool``,(``EVERY f``,list))]);
511         {const = ``fcp_detect : (sexp -> bool) -> 'b itself -> sexp -> bool``,
519         {const = ``FCP_EVERY : ('a -> bool) -> 'a ** 'b -> bool``,
631             {const = ``(K T):sexp -> bool``,
793             (at --> at --> bool) --> (bt --> at) --> bt --> bt --> bool);
844             (prove(``bool (0 = a) = zp (nat a)``,
897     val _ = add_standard_rewrite 0 "bool ~" translateTheory.BOOL_NOT;
1150 in  mk_comb(mk_const("ONE_ONE", (t1 --> t2) --> bool), term)
1344 val _ = add_translations add_bool_translations bool;
1361 val _ = add_rewrites add_bool_rewrites bool;