acl2/ml/encodeLib.sml

61 let val b1 = construct_bottom_value is_vartype (mk_arb alpha) t
642         val t = mk_prod(numLib.num,alpha)
659         val pair_def = get_coding_function_def target (mk_prod(alpha,beta)) "detect"
674         val pair_def = get_coding_function_def target (mk_prod(alpha,beta)) "decode"
682         val pair_def = get_coding_function_def target (mk_prod(alpha,beta)) "fix"
684                                 (get_fix_function target (mk_prod(num,alpha))))
713                         (ENCODE_CONV (get_coding_function_def target (mk_prod(alpha,beta)) "encode"))
825                                 (PURE_REWRITE_CONV [get_source_function_def (mk_prod(alpha,beta)) "all"])))) x
1274     if can (match_term (mk_const(alpha --> alpha))) (getf t)
1421                 (ASSUME (mk_eq(mk_var("A",alpha --> bool),mk_comb(mk_const("K",bool --> alpha --> bool),T)))))
1511         val pairp_pair = get_coding_theorem target (mk_prod(alpha,beta)) "encode_detect_all"
1514         val pairp_id = get_source_theorem (mk_prod(alpha,beta)) "all_id"
1515         val pair_map = get_source_function_def (mk_prod(alpha,beta)) "map"
1519                                 (SPEC_ALL (get_coding_theorem target (mk_prod(alpha,beta)) "encode_decode_map"))));
1554         val pairp_pair = generate_coding_theorem target "encode_detect_all" (mk_prod(alpha,beta))
1556         val pairp_id = generate_source_theorem "all_id" (mk_prod(alpha,beta))
1558         val pair_all = get_source_function_def (mk_prod(alpha,beta)) "all"
1559         val pair_map = get_source_function_def (mk_prod(alpha,beta)) "map"
1562                                         (PURE_REWRITE_RULE [FUN_EQ_THM,o_THM] (SPEC_ALL (get_coding_theorem target (mk_prod(alpha,beta)) "encode_decode_map"))));
1616                 ASM_REWRITE_TAC (get_source_function_def (mk_prod(alpha,beta)) "map"::thms) THEN
1642         val enc_defs = map (C (get_coding_function_def target) "encode") (mk_prod(alpha,beta)::all_types t);
1658         val map_defs = map (C get_source_function_def "map") (mk_prod(alpha,beta)::all_types t);
1679                 ASM_REWRITE_TAC (get_source_function_def (mk_prod(alpha,beta)) "all"::thms) THEN
1689         val alpha = gen_tyvar()
1691         val goutput = list_mk_comb(mk_var("M",list_mk_fun(flatten (map (map type_of o strip_pair o fst) ginput),alpha)),
1693         val gterml = mk_comb(mk_var("f",alpha --> beta),pairSyntax.mk_anylet (ginput,goutput));
1694         val gtermr = pairSyntax.mk_anylet(ginput,mk_comb(mk_var("f",alpha --> beta),goutput));
1725         TRY (REWRITE_TAC [get_coding_function_def target (mk_prod(alpha,beta)) "encode",I_THM] THEN NO_TAC)
1743         val rts = mk_prod(alpha,beta)::num::relevant_types mt
1746         val fix_defs = map (C (get_coding_function_def target) "fix") (mk_prod(alpha,beta)::num::all_types mt)
1751         val thm = REWRITE_RULE [I_THM,get_source_function_def (mk_prod(alpha,beta)) "map"]
1760                 TRY (FULL_SIMP_TAC std_ss [get_coding_function_def target (mk_prod(alpha,beta)) "detect"] THEN NO_TAC) THEN
1766                 ASM_REWRITE_TAC (last (CONJUNCTS sexpTheory.sexp_11)::get_coding_function_def target (mk_prod(alpha,beta)) "encode"::thms) THEN
1789         val defs = map (C (get_coding_function_def target) "fix" o base_type) (mk_prod(alpha,beta)::num::all_types)
1791                                 (mk_prod(alpha,beta)::num::all_types))
1796                                 (mk_prod(alpha,beta)::num::rts)
1797         val tsplit_thm = SIMP_RULE std_ss [get_coding_function_def target (mk_prod(alpha,beta)) "detect",
1798                                 get_coding_function_def target (mk_prod(alpha,beta)) "fix"]
1802                         generate_coding_theorem target "fix_id") (rev (mk_prod(alpha,beta)::num::rts))
1803         val cond_tm = mk_cond(mk_var("p",bool),mk_var("a",alpha),(mk_var("b",alpha)));
1810                 RULE_ASSUM_TAC (ONCE_REWRITE_RULE [get_coding_function_def target (mk_prod(alpha,beta)) "detect"]) THEN
1820                         PAT_ASSUM cond_tm MP_TAC THEN ASM_REWRITE_TAC [get_coding_function_def target (mk_prod(alpha,beta)) "encode"] THEN TRY STRIP_TAC THEN
1826                         REWRITE_TAC [get_coding_function_def target (mk_prod(alpha,beta)) "decode"] 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
1858 let     val all_types = map base_type ((mk_prod(alpha,beta))::(filter (not o is_vartype) (flatten (map (op@ o snd) (split_nested_recursive_set t)))));
1859         val pair_def = get_coding_function_def target (mk_prod(alpha,beta)) "detect"
1860         val thms = [K_THM,get_coding_function_def target (mk_prod(alpha,beta)) "decode",I_THM];
1900         val pair_def = get_source_function_def (mk_prod(alpha,beta)) "all"
1909         val pair_def = get_source_function_def (mk_prod(alpha,beta)) "map"
2010                         (PURE_REWRITE_CONV [get_source_function_def (mk_prod(alpha,beta)) "all"])))) x
2022                 (ENCODE_CONV (get_coding_function_def target (mk_prod(alpha,beta)) "encode"))