Lines Matching defs:target
60 fun target_bottom_value target bottom_target t =
64 val b2 = inst (map (fn t => t |-> target) types) b1
66 subst [mk_arb target |-> bottom_target] b2
148 (* Given the target type, each conv rewrites to convert a term given to *)
171 fun get_gen_type opr target t =
172 foldr (fn (x,t) => (opr (x,target)) --> t) (opr (t,target))
175 fun get_encode_type target t = get_gen_type op--> target t
177 fun get_decode_type target t = get_gen_type (uncurry (C (curry op-->))) target t
179 fun get_detect_type target t = get_gen_type (fn (_,a) => a --> bool) target t
191 fun get_fix_type target t = get_gen_type (fn (_,_) => target --> target) target t
204 fun mk_encode_var target t =
205 mk_var(mk_encode_string t,get_encode_type target t)
207 fun mk_decode_var target t =
208 mk_var(mk_decode_string t,get_decode_type target t)
210 fun mk_detect_var target t =
211 mk_var(mk_detect_string t,get_detect_type target t)
216 fun mk_fix_var target t =
217 mk_var(mk_fix_string t,get_fix_type target t)
222 fun mk_fix_var target t =
223 mk_var(mk_fix_string t,get_fix_type target t)
232 fun get_encode_const target t =
233 if t = target
234 then mk_const("I",t --> target)
236 (get_coding_function_const target t "encode") t
238 fun get_decode_const target t =
239 if t = target
240 then mk_const("I",target --> t)
242 (get_coding_function_const target t "decode") t
248 fun get_fix_const target t =
249 if t = target
250 then mk_const("I",target --> t)
252 (get_coding_function_const target t "fix") t
258 fun get_detect_const target t =
259 if t = target
260 then mk_comb(mk_const("K",bool --> target --> bool),T)
261 else new_const NONE (get_coding_function_const target t "detect") t
295 fun get_encode_function target t =
296 get_function (get_encode_const target)
297 (C (exists_coding_function_precise target) "encode")
298 (mk_encode_var target) t
300 fun get_decode_function target t =
301 get_function (get_decode_const target)
302 (C (exists_coding_function_precise target) "decode")
303 (mk_decode_var target) t
305 fun get_detect_function target t =
306 get_function (get_detect_const target)
307 (C (exists_coding_function_precise target) "detect")
308 (mk_detect_var target) t
315 fun get_fix_function target t =
316 get_function (get_fix_const target)
317 (C (exists_coding_function_precise target) "fix")
318 (mk_fix_var target) t
328 fun mk_detect_constructor_ns rest target C =
332 mk_comb(get_detect_function target (list_mk_prod list),rest)
334 fun mk_detect_constructor rest target C T =
335 if can dom_rng (type_of C) then mk_detect_constructor_ns rest target C else T
336 fun mk_detect_res_term label rest target t constructors T =
339 mk_detect_constructor rest target b T)) (enumerate 0 constructors))
341 fun mk_detect_term_label (p,x) target t constructors =
342 let val dnat = get_decode_function target num
343 val rnat = get_detect_function target num
345 mk_forall(x,mk_eq(mk_comb(get_detect_function target t,x),
347 mk_detect_res_term (mk_comb(dnat,x)) x target t constructors T,
350 fun mk_detect_term_all (p,x) target t constructors =
351 let val dnat = get_detect_function target num
353 val rest = mk_var("r",target)
354 val null = mk_comb(get_encode_function target bool,F)
356 list_mk_forall(snd (strip_comb (get_detect_function target t)),
357 mk_forall(x,mk_eq(mk_comb(get_detect_function target t,x),
359 [(mk_pair(label,rest),mk_comb(get_decode_function target (mk_prod(num,target)),x))],
360 mk_detect_res_term label rest target t constructors (mk_eq(rest,null))),
363 fun mk_detect_term_single (p,x) target t constructor =
364 let val t' = (mk_type o (I ## map (K target)) o dest_type) t
365 val p = get_detect_function target t'
367 list_mk_forall(snd (strip_comb (get_detect_function target t)),
368 mk_forall(x,mk_eq(mk_comb(get_detect_function target t,x),mk_detect_constructor x target constructor T)))
371 fun mk_detect_term target t =
374 val x = mk_var("x",target)
375 val p = mk_comb(get_detect_function target (mk_prod(num,target)),x)
378 then mk_detect_term_label (p,x) target t' constructors
381 then mk_detect_term_single (p,x) target t' (hd constructors)
383 else mk_detect_term_all (p,x) target t' constructors
389 fun full_bottom_value target bottom_target t =
390 let val bottom = target_bottom_value target bottom_target t
392 val decodef = get_decode_function target t
399 fun mk_decode_constructor_ns rest target C =
404 [(list_mk_pair vars,mk_comb(get_decode_function target (list_mk_prod list),rest))],
407 fun mk_decode_constructor rest target C =
408 if can dom_rng (type_of C) then mk_decode_constructor_ns rest target C else C
409 fun mk_decode_res_term label rest target t constructors bottom =
412 mk_decode_constructor rest target b)) (enumerate 0 constructors))
414 fun mk_decode_term_label (p,x) target t constructors =
415 let val dnat = get_decode_function target num
416 val rnat = get_detect_function target num
419 mk_forall(x,mk_eq(mk_comb(get_decode_function target t,x),
421 mk_decode_res_term (mk_comb(dnat,x)) x target t constructors bottom,
424 fun mk_decode_term_all (p,x) target t constructors =
425 let val dnat = get_decode_function target num
427 val rest = mk_var("r",target)
428 val bottom = full_bottom_value target (#bottom(get_translation_scheme target)) t
430 list_mk_forall(snd (strip_comb (get_decode_function target t)),
431 mk_forall(x,mk_eq(mk_comb(get_decode_function target t,x),
433 [(mk_pair(label,rest),mk_comb(get_decode_function target (mk_prod(num,target)),x))],
434 mk_decode_res_term label rest target t constructors bottom),
437 fun mk_decode_term_single (p,x) target t constructor =
438 let val t' = (mk_type o (I ## map (K target)) o dest_type) t
439 val p = get_detect_function target t'
441 list_mk_forall(snd (strip_comb (get_decode_function target t)),
442 mk_forall(x,mk_eq(mk_comb(get_decode_function target t,x),
444 mk_decode_constructor x target constructor,
445 full_bottom_value target (#bottom(get_translation_scheme target)) t))))
448 fun mk_decode_term target t =
451 val x = mk_var("x",target)
452 val p = mk_comb(get_detect_function target (mk_prod(num,target)),x)
455 then mk_decode_term_label (p,x) target t' constructors
458 then mk_decode_term_single (p,x) target t' (hd constructors)
460 else mk_decode_term_all (p,x) target t' constructors
466 fun mk_fix_constructor_ns all target C =
470 mk_comb(get_fix_function target (list_mk_prod (num::list)),all)
472 fun mk_fix_constructor all target dead n C =
474 then mk_fix_constructor_ns all target C
475 else mk_comb(get_encode_function target (mk_prod(num,bool)),
477 fun mk_fix_res_term label all target constructors dead bottom =
480 mk_fix_constructor all target dead a b)) (enumerate 0 constructors))
482 fun mk_fix_term_label x target t constructors =
483 let val dnat = get_decode_function target num
484 val rnat = get_detect_function target num
485 val enat = get_encode_function target num
487 mk_forall(x,mk_eq(mk_comb(get_fix_function target t,x),
491 mk_comb(get_encode_function target num,zero_tm))))
493 fun mk_fix_term_all (p,x) target t constructors dead =
494 let val dnat = get_fix_function target num
496 val rest = mk_var("r",target)
497 val t' = (mk_type o (I ## map (K target)) o dest_type) t
498 val instit = inst (map (fn v => v |-> target) (type_vars t))
499 val enc1 = instit (get_encode_function target t)
500 val enc2 = subst (map (fn v => instit (get_encode_function target v) |->
501 get_fix_function target v) (type_vars t)) enc1
502 val bottom = rimk_comb(enc2,target_bottom_value target dead t)
504 list_mk_forall(snd (strip_comb (get_fix_function target t)),
505 mk_forall(x,mk_eq(mk_comb(get_fix_function target t,x),
508 mk_comb(get_decode_function target (mk_prod(num,target)),x))],
509 mk_fix_res_term label x target constructors dead bottom),
512 fun mk_fix_term_single x target t constructor dead =
513 let val t' = (mk_type o (I ## map (K target)) o dest_type) t
514 val p = get_detect_function target t'
515 val instit = inst (map (fn v => v |-> target) (type_vars t))
516 val enc1 = instit (get_encode_function target t)
518 instit (get_encode_function target v) |->
519 get_fix_function target v) (type_vars t)) enc1
520 val bottom = rimk_comb(enc2,target_bottom_value target dead t)
523 list_mk_forall(snd (strip_comb (get_fix_function target t)),
524 mk_forall(x,mk_eq(mk_comb(get_fix_function target t,x),
526 mk_comb(get_fix_function target (list_mk_prod list),x),
530 fun mk_fix_term target t =
534 val x = mk_var("x",target)
535 val p = mk_comb(get_detect_function target (mk_prod(num,target)),x)
536 val dead = #bottom (get_translation_scheme target)
539 then mk_fix_term_label x target t' constructors
542 then mk_fix_term_single x target t' (hd constructors) dead
544 else mk_fix_term_all (p,x) target t' constructors dead
551 fun single_pair num target t cnst =
563 list_mk_forall(map (get_encode_function target) (snd (dest_type t)),
564 mk_eq(mk_comb(get_encode_function target t,
567 then mk_comb(get_encode_function target ``:num``,``0n``)
568 else (mk_comb(get_encode_function target
572 fun mk_encode_term_single target t cnst = single_pair NONE target t cnst
573 fun mk_encode_term_label target t cnsts =
574 let val num = get_encode_function target ``:num``
575 val func = get_encode_function target t
581 fun mk_encode_term_all target t cnsts =
582 list_mk_conj (map (fn (n,c) => single_pair (SOME n) target t c)
585 fun mk_encode_term target t =
591 then mk_encode_term_label target t' constructors
594 then mk_encode_term_single target t' (hd constructors)
596 else mk_encode_term_all target t' constructors
657 fun DC target term =
659 val pair_def = get_coding_function_def target (mk_prod(alpha,beta)) "detect"
672 fun SC target term =
674 val pair_def = get_coding_function_def target (mk_prod(alpha,beta)) "decode"
680 fun FIXC target term =
682 val pair_def = get_coding_function_def target (mk_prod(alpha,beta)) "fix"
684 (get_fix_function target (mk_prod(num,alpha))))
690 fun DETECT_CONV target term =
692 EVERY_CONJ_CONV (STRIP_QUANT_CONV (DC target THENC TRY_CONV (SC target))) term handle e => wrapException "DETECT_CONV" e)
693 fun DECODE_CONV target term =
695 EVERY_CONJ_CONV (STRIP_QUANT_CONV (DC target THENC TRY_CONV (SC target))) term handle e => wrapException "DECODE_CONV" e)
696 fun FIX_CONV target term =
698 EVERY_CONJ_CONV (STRIP_QUANT_CONV (DC target THENC TRY_CONV (SC target) THENC REWRITE_CONV [K_THM] THENC TRY_CONV (FIXC target))) term handle e => wrapException "FIX_CONV" e)
701 fun mk_encodes target t =
702 let val _ = if exists_coding_function target t "encode" then
704 ("Encoder function for translation: " ^ type_to_string t ^ " --> " ^ type_to_string target ^
707 ("Generating encoding function for: " ^ type_to_string t ^ " --> " ^ type_to_string target ^ "\n")
711 (mk_encode_term target)
712 (get_encode_function target)
713 (ENCODE_CONV (get_coding_function_def target (mk_prod(alpha,beta)) "encode"))
715 target
732 val target = (type_of o rand o lhs o snd o strip_forall o hd) clauses
733 val dead_thm = #bottom_thm (get_translation_scheme target)
734 val subs = (mk_type o (I ## map (fn a => if a = target then gen_tyvar() else a)) o dest_type)
735 val ts = (mk_prod(num,target))::mk_set (filter (not o is_vartype)
738 val encs = map (fn x => (generate_coding_function target "encode" (base_type x) ;
739 get_coding_function_def target x "encode")) ts
740 val decs = flatten (map CONJUNCTS (mapfilter (C (get_coding_function_def target) "decode") ts))
741 val fixs = map (REWRITE_RULE encs) (flatten (map CONJUNCTS (mapfilter (C (get_coding_function_def target) "fix") ts)))
742 val deads = dead_thm::mapfilter (generate_coding_theorem target "detect_dead" o base_type) ts;
761 fun mk_decodes target t =
762 let val _ = if exists_coding_function target t "decode" then
764 ("Decoder function for translation: " ^ type_to_string t ^ " --> " ^ type_to_string target ^
767 ("Generating decoding function for: " ^ type_to_string t ^ " --> " ^ type_to_string target ^ "\n")
771 (mk_decode_term target)
772 (get_decode_function target)
773 (DECODE_CONV target)
775 target
779 fun mk_detects target t =
780 let val _ = if exists_coding_function target t "detect" then
782 ("Detector function for translation: " ^ type_to_string t ^ " --> " ^ type_to_string target ^
785 ("Generating detecting function for: " ^ type_to_string t ^ " --> " ^ type_to_string target ^ "\n")
789 (mk_detect_term target)
790 (get_detect_function target)
791 (DETECT_CONV target)
793 target
831 fun mk_fixs target t =
832 let val _ = if exists_coding_function target t "fix" then
834 ("fix function for translation: " ^ type_to_string t ^ " --> " ^ type_to_string target ^
837 ("Generating fix function for: " ^ type_to_string t ^ " --> " ^ type_to_string target ^ "\n")
841 (mk_fix_term target)
842 (get_fix_function target)
843 (FIX_CONV target)
845 target
918 fun mk_encode_decode_map_conc target t =
919 let val enc = check_function (get_encode_function target) t handle e => wrap e
920 val dec = check_function (get_decode_function target) t handle e => wrap e
970 fun mk_encode_map_encode_conc target t =
971 let val encf = check_function (get_encode_function target) t handle e => w "mk_encode_map_encode_conc" e
989 fun mk_decode_encode_fix_conc target t =
990 let val enc = check_function (get_encode_function target) t
991 val dec = check_function (get_decode_function target) t
992 val fix = check_function (get_fix_function target) t
1003 fun mk_encode_detect_all_conc target t =
1004 let val enc = check_function (get_encode_function target) t
1005 val det = check_function (get_detect_function target) t
1007 val dbool = get_decode_function target bool
1037 fun mk_fix_id_conc target t =
1038 let val fix_term = check_function (get_fix_function target) t
1039 val det_term = check_function (get_detect_function target) t
1041 val hyps = map (mk_fix_id_conc target) (set_diff tvs [t])
1042 val x = mk_var("x",target)
1050 fun mk_general_detect_conc target t =
1051 let val p1 = check_function (get_detect_function target) t
1052 val t' = type_subst (map (fn v => v |-> target)
1054 val p2 = check_function (get_detect_function target) t'
1055 val xvar = mk_var("x",target)
1064 fun mk_encode_decode_conc target t =
1065 let val encode = check_function (get_encode_function target) t
1067 val decode = check_function (get_decode_function target) t
1074 mk_encode_decode_conc target) (set_diff tvs [t])
1076 list_mk_forall(map (get_encode_function target) tvs,
1077 list_mk_forall(map (get_decode_function target) tvs,
1087 fun mk_decode_encode_conc target t =
1088 let val encode = check_function (get_encode_function target) t
1090 val detect = check_function (get_detect_function target) t
1092 val decode = check_function (get_decode_function target) t
1094 val var = mk_var("x",target)
1100 mk_decode_encode_conc target) (set_diff tvs [t])
1102 list_mk_forall(map (get_encode_function target) tvs,
1103 list_mk_forall(map (get_decode_function target) tvs,
1104 list_mk_forall(map (get_detect_function target) tvs,
1114 fun mk_encode_detect_conc target t =
1115 let val encode = check_function (get_encode_function target) t
1117 val detect = check_function (get_detect_function target) t
1124 mk_encode_detect_conc target) (set_diff tvs [t])
1126 list_mk_forall(map (get_encode_function target) tvs,
1127 list_mk_forall(map (get_detect_function target) tvs,
1182 fun EMPTY_RING gconc name target t thms =
1183 let val conc = gconc target t
1187 fun RING_MATCH_THM gconc name target t =
1188 let val basetype = if t = target then t else
1190 (C (exists_coding_theorem_precise target) name) t
1192 val thm = SPEC_ALL (generate_coding_theorem target name basetype)
1193 val conc = gconc target t
1195 val sub_thms = map (RING_MATCH_THM gconc name target)
1200 fun CHECK_RING gconc name target t thms =
1202 then (EMPTY_RING gconc name target t thms handle _ =>
1203 RING_MATCH_THM gconc name target t)
1204 else RING_MATCH_THM gconc name target t
1206 fun FULL_ENCODE_DECODE_MAP_THM target t =
1207 if target = t
1208 then CONJUNCT1 (ISPEC (mk_const("I",target --> target)) I_o_ID)
1210 "encode_decode_map" target t
1212 fun FULL_ENCODE_DETECT_ALL_THM target t =
1213 if target = t
1215 (mk_comb(mk_const("K",bool --> target --> bool),T))
1218 "encode_detect_all" target t
1220 fun FULL_ENCODE_MAP_ENCODE_THM target t =
1221 if target = t
1222 then FULL_ENCODE_DECODE_MAP_THM target t
1224 CHECK_RING mk_encode_map_encode_conc "encode_map_encode" target t
1227 fun FULL_DECODE_ENCODE_FIX_THM target t =
1228 if target = t
1229 then FULL_ENCODE_DECODE_MAP_THM target t
1231 RING_MATCH_THM mk_decode_encode_fix_conc "decode_encode_fix" target t;
1287 fun FULL_FIX_ID_THM target t =
1289 val basetype = if target = t then t else
1291 (C (exists_coding_theorem_precise target) "fix_id") t
1293 val thm = generate_coding_theorem target "fix_id" basetype
1296 val conc = mk_fix_id_conc target t
1307 FULL_FIX_ID_THM target)
1313 val disch_set = map (mk_fix_id_conc target) tvs
1330 fun FEDT target t =
1333 val thm1 = generate_coding_theorem target "encode_decode_map" t
1339 val tvs = type_vars_avoiding_itself (get_encode_function target t) t
1341 snd o strip_forall o mk_encode_decode_conc target)
1357 val (vs,conc) = strip_forall (mk_encode_decode_conc target t)
1369 fun FULL_ENCODE_DECODE_THM target t =
1370 if target = t then
1372 (mk_encode_decode_conc target t))
1374 then DECIDE (mk_encode_decode_conc target t) else FEDT target t
1379 fun FDET target t =
1380 let val thm1 = generate_coding_theorem target "decode_encode_fix" t handle e => wrap e
1381 val thm2 = generate_coding_theorem target "fix_id" t handle e => wrap e
1397 val conc = mk_decode_encode_conc target t
1407 fun FULL_DECODE_ENCODE_THM target t =
1408 let val conc = (mk_decode_encode_conc target t)
1413 then DISCH_ALL (ASSUME (snd (dest_imp_only (snd (strip_forall (mk_decode_encode_conc target t))))))
1414 else FDET target t)
1422 fun FEDT target t =
1423 let val thm1 = FULL_ENCODE_DETECT_ALL_THM target t handle e => wrap e
1430 val conc = mk_encode_detect_conc target t handle e => wrap e
1432 snd o dest_imp_only o snd o strip_forall o mk_encode_detect_conc target) (type_vars t)
1449 fun FULL_ENCODE_DETECT_THM target t =
1450 if is_vartype t then DECIDE (mk_encode_detect_conc target t)
1451 else FEDT target t
1475 val target = type_of term
1476 val check = check_function (get_encode_function target) t
1477 val def = get_coding_function_def target t "encode"
1507 val target = type_of (rand term)
1508 val check = check_function (get_decode_function target) t
1509 val def = get_coding_function_def target t "decode"
1511 val pairp_pair = get_coding_theorem target (mk_prod(alpha,beta)) "encode_detect_all"
1512 val nump_num = get_coding_theorem target num "encode_detect_all"
1513 val labelled = mk_comb(get_detect_function target (mk_prod(num,target)),rand term)
1519 (SPEC_ALL (get_coding_theorem target (mk_prod(alpha,beta)) "encode_decode_map"))));
1520 val numd_num = get_coding_theorem target num "encode_decode_map";
1523 PURE_REWRITE_CONV [o_THM,PURE_REWRITE_RULE [FUN_EQ_THM,o_THM] nump_num,K_THM] (mk_comb(get_detect_function target num,rand term))
1525 PURE_REWRITE_RULE [get_coding_function_def target t "encode"]
1527 (PURE_REWRITE_RULE [FUN_EQ_THM,o_THM] (SPEC_ALL (generate_coding_theorem target "encode_detect_all" t))))
1531 PURE_REWRITE_CONV [o_THM,PURE_REWRITE_RULE [FUN_EQ_THM,o_THM] numd_num,I_THM] (mk_comb(get_decode_function target num,rand term))
1534 else PURE_REWRITE_CONV [paird_pair,numd_num,I_o_ID,I_THM] (mk_comb(get_decode_function target (mk_prod(num,target)),rand term))
1550 let val target = type_of (rand term)
1551 val check = check_function (get_detect_function target) t
1552 val def = get_coding_function_def target t "detect"
1554 val pairp_pair = generate_coding_theorem target "encode_detect_all" (mk_prod(alpha,beta))
1555 val nump_num = generate_coding_theorem target "encode_detect_all" num
1557 val labelled = mk_comb(get_detect_function target (mk_prod(num,target)),rand term)
1562 (PURE_REWRITE_RULE [FUN_EQ_THM,o_THM] (SPEC_ALL (get_coding_theorem target (mk_prod(alpha,beta)) "encode_decode_map"))));
1563 val numd_num = get_coding_theorem target num "encode_decode_map";
1566 PURE_REWRITE_CONV [o_THM,PURE_REWRITE_RULE [FUN_EQ_THM,o_THM] nump_num,K_THM] (mk_comb(get_detect_function target num,rand term))
1573 PURE_REWRITE_CONV [o_THM,PURE_REWRITE_RULE [FUN_EQ_THM,o_THM] numd_num,I_THM] (mk_comb(get_decode_function target num,rand term))
1576 else PURE_REWRITE_CONV [paird_pair,numd_num,I_o_ID,I_THM] (mk_comb(get_decode_function target (mk_prod(num,target)),rand term))
1606 fun encode_decode_map_tactic target (t:hol_type) (a,g) =
1609 val thms = map (generate_coding_theorem target "encode_decode_map") rts
1623 fun PTAC target rset t (a,g) =
1626 val thm1 = PURE_REWRITE_RULE [FUN_EQ_THM,o_THM] (SPEC_ALL (generate_coding_theorem target "encode_map_encode" t'));
1631 fun CTAC target rset t =
1634 else if length cs = 1 then ALL_TAC else PTAC target rset t
1637 fun encode_map_encode_tactic target (t:hol_type) (a,g) =
1641 val thms = map (generate_coding_theorem target "encode_map_encode") rts
1642 val enc_defs = map (C (get_coding_function_def target) "encode") (mk_prod(alpha,beta)::all_types t);
1649 PURE_REWRITE_TAC [I_THM,I_o_ID] THEN CTAC target rset t THEN ASM_REWRITE_TAC all_thms THEN
1670 fun encode_detect_all_tactic target (t:hol_type) (a,g) =
1672 val thms = map (generate_coding_theorem target "encode_detect_all") (relevant_types t)
1716 fun START_LABEL_TAC enc encoder target t =
1718 ONCE_REWRITE_TAC [get_coding_function_def target t "decode"] THEN
1719 ONCE_REWRITE_TAC [get_coding_function_def target t "fix"] THEN
1722 REWRITE_TAC [REWRITE_RULE [FUN_EQ_THM,o_THM] (generate_coding_theorem target "encode_map_encode" t)] THEN
1725 TRY (REWRITE_TAC [get_coding_function_def target (mk_prod(alpha,beta)) "encode",I_THM] THEN NO_TAC)
1726 fun LABEL_TAC thms enc encoder target t =
1727 START_LABEL_TAC enc encoder target t THEN
1730 MATCH_MP_TAC (get_coding_theorem target num "fix_id") THEN
1737 fun decode_encode_fix_tactic target _ (a,g) =
1741 val encoder = get_coding_function_def target t "encode";
1742 val mt = first (not o C (exists_coding_theorem target) "decode_encode_fix") (all_types t)
1744 val thms = map (generate_coding_theorem target "decode_encode_fix" o base_type) rts @
1745 mapfilter (generate_coding_theorem target "decode_encode_fix") rts
1746 val fix_defs = map (C (get_coding_function_def target) "fix") (mk_prod(alpha,beta)::num::all_types mt)
1747 val dead_thm = #bottom_thm (get_translation_scheme target)
1748 val all_defs = foldl (fn (a,b) => get_coding_function_def target a "encode"::get_source_function_def a "map"::
1749 get_coding_function_def target a "decode"::get_coding_function_def target a "fix"::
1750 get_coding_function_def target a "detect"::b) [o_THM,dead_thm] (all_types t)
1753 (SPEC_ALL (generate_coding_theorem target "encode_map_encode" (mk_prod(num,beta))))))
1758 LABEL_TAC thms enc encoder target t,
1759 START_LABEL_TAC enc encoder target t THEN
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
1775 fun MATCH_FIX_TAC target rset all_types (a,g) =
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;
1786 fun fix_id_tactic target t (a,g) =
1788 val mt = first (not o C (exists_coding_theorem target) "fix_id" o base_type) all_types
1789 val defs = map (C (get_coding_function_def target) "fix" o base_type) (mk_prod(alpha,beta)::num::all_types)
1790 val pdefs = flatten (mapfilter (CONJUNCTS o C (get_coding_function_def target) "detect" o base_type)
1792 val split_thm = generate_coding_theorem target "fix_id" (mk_prod(num,target))
1795 val def_thms = mapfilter (generate_coding_theorem target "decode_encode_fix" o base_type)
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"]
1799 (GSYM (generate_coding_theorem target "fix_id" (mk_prod(target,target))));
1802 generate_coding_theorem target "fix_id") (rev (mk_prod(alpha,beta)::num::rts))
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
1828 (FIRST_ASSUM ACCEPT_TAC ORELSE FIRST_ASSUM MATCH_MP_TAC ORELSE MATCH_FIX_TAC target rset all_types) 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
1833 TRY (FIRST_ASSUM MATCH_MP_TAC) THEN TRY (MATCH_FIX_TAC target rset all_types) THENL
1836 RES_TAC THEN IMP_RES_TAC (generate_coding_theorem target "general_detect" (base_type t)) THEN REPEAT CONJ_TAC 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
1839 MAP_EVERY (IMP_RES_TAC o generate_coding_theorem target "general_detect" o base_type) (filter (not o is_vartype) all_types))]) (a,g)
1857 fun general_detect_tactic target 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];
1864 in REPEAT GEN_TAC THEN REWRITE_TAC [get_coding_function_def target t "detect"] THEN
1871 COMPLETE thm split (mapfilter (generate_coding_theorem target "general_detect") all_types)
1876 fun DDR dead_value target t =
1877 let val def = get_coding_function_def target t "detect"
1878 val den = get_coding_theorem target num "detect_dead"
1880 val dead_thm = #bottom_thm (get_translation_scheme target)
1883 REWRITE_CONV (dead_thm::den::mapfilter (generate_coding_theorem target "detect_dead" o list_mk_prod) [t']))
1884 (mk_comb(check_function (get_detect_function target) t,dead_value))
1887 fun detect_dead_rule target t =
1888 let val dead_value = #bottom (get_translation_scheme target)
1890 if t = target then
1891 REWRITE_CONV [get_coding_theorem target bool "encode_decode",K_THM] (mk_comb(get_decode_function target bool,mk_comb(get_detect_function target t,dead_value)))
1892 else DDR dead_value target t
1947 fun mk_single_destructor target t c =
1952 val encoders = CONJUNCTS (get_coding_function_def target t "encode")
1954 val encoder = PART_MATCH (rator o lhs) e (get_encode_function target t)
1958 val applied = AP_TERM (get_decode_function target
1960 val decoder = SPEC_ALL (FULL_ENCODE_DECODE_THM target product)
1965 val product_encoder = get_encode_function target product;
1983 fun mk_destructors target t =
1985 unzip (mapf (mk_single_destructor target t) (constructors_of t))
2017 fun initialise_coding_function_generators target =
2020 (mk_encode_term target)
2021 (get_encode_function target)
2022 (ENCODE_CONV (get_coding_function_def target (mk_prod(alpha,beta)) "encode"))
2023 REFL target;
2026 (mk_detect_term target)
2027 (get_detect_function target)
2028 (DETECT_CONV target)
2029 REFL target;
2031 (detect_dead_rule target) target;
2035 generate_coding_function target "encode" (base_type t) ;
2036 mk_decode_term target t))
2037 (get_decode_function target)
2038 (DECODE_CONV target)
2040 target;
2043 (mk_fix_term target)
2044 (get_fix_function target)
2045 (FIX_CONV target)
2047 target;
2052 fun initialise_coding_theorem_generators target =
2054 target "encode_detect_all"
2055 (mk_encode_detect_all_conc target);
2063 target "encode_decode_map" (mk_encode_decode_map_conc target);
2065 target "encode_map_encode" (mk_encode_map_encode_conc target);
2067 target "general_detect" (mk_general_detect_conc target);
2069 target "decode_encode_fix" (mk_decode_encode_fix_conc target);
2071 target "fix_id" (mk_fix_id_conc target);
2075 target FUN_EQ_CONV
2076 (encode_detect_all_tactic target);
2088 target FUN_EQ_CONV
2089 (encode_decode_map_tactic target);
2092 target FUN_EQ_CONV
2093 (encode_map_encode_tactic target);
2096 target REFL
2097 (general_detect_tactic target);
2100 target FUN_EQ_CONV
2101 (decode_encode_fix_tactic target);
2104 target REFL
2105 (fix_id_tactic target);
2108 (exists_coding_theorem target t theorem_name) orelse
2109 not (can (C (get_coding_function_induction target) function_name) t)
2118 (FULL_ENCODE_DETECT_ALL_THM target)
2119 target;
2135 (FULL_ENCODE_DECODE_MAP_THM target)
2136 target;
2140 (FULL_ENCODE_MAP_ENCODE_THM target)
2141 target;
2144 (C (exists_coding_theorem target) "general_detect")
2145 (C (get_coding_theorem target) "general_detect")
2146 target;
2150 (FULL_DECODE_ENCODE_FIX_THM target)
2151 target;
2155 (FULL_FIX_ID_THM target)
2156 target;
2161 fun encode_type target t =
2165 val _ = if exists_translation target t
2167 else add_translation target t
2170 val _ = generate_coding_function target "encode" t
2171 val _ = generate_coding_function target "decode" t
2172 val _ = generate_coding_function target "detect" t
2173 val _ = generate_coding_function target "fix" t
2175 val _ = generate_coding_theorem target "encode_detect_all" t
2176 val _ = generate_coding_theorem target "encode_map_encode" t
2177 val _ = generate_coding_theorem target "encode_decode_map" t
2178 val _ = generate_coding_theorem target "decode_encode_fix" t
2180 val _ = generate_coding_theorem target "fix_id" t
2186 fun GENCF name f target t =
2187 if (target = t) then f target t
2189 (if exists_coding_function target t name
2190 then f target t
2191 else (encode_type target (base_type t) ; f target t))
2209 fun predicate_equivalence target t =
2212 val target_var = mk_var("x",target);
2213 val detect = mk_comb(get_detect_function target t,target_var)
2214 val decode = mk_comb(get_decode_function target t,target_var)
2215 val encode = mk_comb(get_encode_function target t,var)
2221 val encdet = UNDISCH_ALL (SPEC_ALL (FULL_ENCODE_DETECT_THM target t))
2222 val decenc = UNDISCH_ALL (SPEC_ALL (FULL_ENCODE_DECODE_THM target t))