acl2/ml/encodeLib.sml

1182 fun EMPTY_RING gconc name target t thms =
1185     EQT_ELIM (REWRITE_CONV thms conc)
1200 fun CHECK_RING gconc name target t thms =
1202        then (EMPTY_RING gconc name target t thms handle _ =>
1609         val thms = map (generate_coding_theorem target "encode_decode_map") rts
1613         FIRST [ CONV_TAC (LAND_CONV (RATOR_CONV (FIRST_CONV (map REWR_CONV thms)))) THEN
1614                 RULE_ASSUM_TAC GSYM THEN ASM_REWRITE_TAC (map_defs @ thms),
1616                 ASM_REWRITE_TAC (get_source_function_def (mk_prod(alpha,beta)) "map"::thms) THEN
1617                 RULE_ASSUM_TAC GSYM THEN ASM_REWRITE_TAC (map_defs @ thms)]) (a,g)
1641         val thms = map (generate_coding_theorem target "encode_map_encode") rts
1643         val all_thms = map (PURE_REWRITE_RULE [o_THM,FUN_EQ_THM]) thms @ thms @ enc_defs
1646         FIRST [ CONV_TAC (LAND_CONV (RATOR_CONV (FIRST_CONV (map REWR_CONV thms)))) THEN
1657         val thms = map (generate_source_theorem "map_compose") rts
1659         val all_thms = map (PURE_REWRITE_RULE [o_THM,FUN_EQ_THM]) thms @ thms @ map_defs
1662          FIRST [CONV_TAC (LAND_CONV (RATOR_CONV (FIRST_CONV (map REWR_CONV thms)))) THEN
1672         val thms = map (generate_coding_theorem target "encode_detect_all") (relevant_types t)
1676         FIRST [ CONV_TAC (LAND_CONV (RATOR_CONV (FIRST_CONV (map REWR_CONV thms)))) THEN
1677                 RULE_ASSUM_TAC GSYM THEN ASM_REWRITE_TAC (all_defs @ thms),
1679                 ASM_REWRITE_TAC (get_source_function_def (mk_prod(alpha,beta)) "all"::thms) THEN
1680                 RULE_ASSUM_TAC GSYM THEN ASM_REWRITE_TAC (all_defs @ thms)]) (a,g)
1726 fun LABEL_TAC thms enc encoder target t =
1729         REWRITE_TAC (map (REWRITE_RULE [FUN_EQ_THM,o_THM]) thms) THEN
1744         val thms = map (generate_coding_theorem target "decode_encode_fix" o base_type) rts @
1757                 CONV_TAC (LAND_CONV (RATOR_CONV (FIRST_CONV (mapfilter REWR_CONV thms)))),
1758                 LABEL_TAC thms enc encoder target t,
1763                 CONV_TAC (LAND_CONV (FIRST_CONV (mapfilter (REWR_CONV o PURE_REWRITE_RULE [FUN_EQ_THM,o_THM]) thms))) THEN
1766                 ASM_REWRITE_TAC (last (CONJUNCTS sexpTheory.sexp_11)::get_coding_function_def target (mk_prod(alpha,beta)) "encode"::thms) THEN
1767                 RULE_ASSUM_TAC GSYM THEN ASM_REWRITE_TAC (map GSYM thms)) THEN
1779         val thms = map (fn a => (C (PART_MATCH I) (snd (strip_forall (mk_fix_id_conc target a))) o FULL_FIX_ID_THM target) a) ftypes;
1780         val thms' = map (CONV_RULE (DEPTH_CONV RIGHT_IMP_FORALL_CONV THENC REWRITE_CONV [AND_IMP_INTRO])) thms
1783                         snd o strip_forall o snd o strip_imp o snd o strip_forall o concl) thms')) (a,g)
1800         val thms = mapfilter (GEN_ALL o (CONV_RULE (DEPTH_CONV RIGHT_IMP_FORALL_CONV THENC
1850 fun COMPLETE thm split thms (a,g) =
1853                 MAP_FIRST (MATCH_MP_TAC o GEN_ALL) thms THEN FIRST_ASSUM FULL_MATCH_TAC,
1854                 CONV_TAC (UNDISCH o PART_MATCH (lhs o snd o dest_imp_only) thm) THEN REPEAT CONJ_TAC THEN COMPLETE thm split thms,
1855                 IMP_RES_TAC thm THEN RES_TAC THEN COMPLETE thm split thms]) (a,g)
1860         val thms = [K_THM,get_coding_function_def target (mk_prod(alpha,beta)) "decode",I_THM];
1866         REWRITE_TAC [LET_DEF] THEN GEN_BETA_TAC THEN ASM_REWRITE_TAC thms THEN