acl2/ml/encodeLib.sml

198 fun mk_detect_string t = "detect" ^ (get_type_string t)
261        else new_const NONE (get_coding_function_const target t "detect") t
307                  (C (exists_coding_function_precise target) "detect")
659         val pair_def = get_coding_function_def target (mk_prod(alpha,beta)) "detect"
780 let     val _ = if exists_coding_function target t "detect" then
788                         "detect"
870 (*     ?- (detect f o encode g) = all (f o g)                                *)
879 (*     ?- !x. detect f g x ==> detect (K T) (K T) x                          *)
883 (*                    !x. detect p x ==> encode g (decode f x) = x           *)
884 (*     ?- (!x. p (g x)) ==> !x. detect p (encode g x)                        *)
1090     val detect = check_function (get_detect_function target) t
1095     val conc = mk_forall(var,mk_imp(mk_comb(detect,var),
1117     val detect = check_function (get_detect_function target) t
1120     val conc = mk_forall(var,mk_comb(detect,mk_comb(encode,var)))
1166 (*            |- !x. detect detect x ==> encode encode (decode decode x) = x)*)
1170 (*            |- !x. detect detect (encode encode x)                         *)
1468 (*        DETECT_PAIR_CONV : |- (detect (encode_pair f g a)) =               *)
1469 (*                              (detect (f (FST (SND a)))) /\ ...            *)
1552         val def = get_coding_function_def target t "detect"
1601 (*    Generates a single application of detect to 'nil'. Used in             *)
1750                                 get_coding_function_def target a "detect"::b) [o_THM,dead_thm] (all_types t)
1760                 TRY (FULL_SIMP_TAC std_ss [get_coding_function_def target (mk_prod(alpha,beta)) "detect"] THEN NO_TAC) THEN
1790         val pdefs = flatten (mapfilter (CONJUNCTS o C (get_coding_function_def target) "detect" o base_type)
1797         val tsplit_thm = SIMP_RULE std_ss [get_coding_function_def target (mk_prod(alpha,beta)) "detect",
1810                 RULE_ASSUM_TAC (ONCE_REWRITE_RULE [get_coding_function_def target (mk_prod(alpha,beta)) "detect"]) THEN
1829                 FULL_SIMP_TAC std_ss [get_coding_function_def target (mk_prod(alpha,beta)) "detect",get_coding_function_def target (mk_prod(alpha,beta)) "decode"] THEN
1838                         ONCE_REWRITE_TAC [get_coding_function_def target t "detect"] THEN REPEAT (IF_CASES_TAC THEN ASM_REWRITE_TAC []) THEN REPEAT STRIP_TAC THEN
1859         val pair_def = get_coding_function_def target (mk_prod(alpha,beta)) "detect"
1864 in      REPEAT GEN_TAC THEN REWRITE_TAC [get_coding_function_def target t "detect"] THEN
1877 let     val def = get_coding_function_def target t "detect"
2025                 "detect"
2095                 "detect" "general_detect"
2172         val _ = generate_coding_function target "detect" t
2196 val gen_detect_function = GENCF "detect" get_detect_function
2202 (*         |- (!x. P x) = (!x. detect x ==> P (decode x))                    *)
2213     val detect = mk_comb(get_detect_function target t,target_var)
2219     val thm1 = GEN target_var (DISCH detect (SPEC decode (ASSUME full_pred)))