Lines Matching defs:wrap
1032 fun wrap e = wrapException "SPLIT_HFUN_CONV" e
1055 end) (fvs,[]) function_terms handle e => wrap e
1058 handle e => wrap e;
1064 handle e => wrap e
1067 handle e => wrap e
1071 (RFUN_CONV rewrites term)) handle e => wrap e))
1079 fun wrap UNCHANGED = raise UNCHANGED | wrap e = wrapException "SPLIT_PAIR_CONV" e
1124 val double_terms = mk_set (map snd (filter (uncurry (is_double_term funcs)) split_terms)) handle e => wrap e
1131 handle e => wrap e
1137 handle e => wrap e)
1145 fun wrap e = wrapException "SPLIT_FUNCTION_CONV" e
1167 | e => wrap e
1290 fun wrap "" e = wrapException "create_mutual_theorem" e
1291 | wrap s e = wrapException ("create_mutual_theorem (" ^ s ^ ")") e
1298 fun make_outp a b c = make_out a b c handle e => wrap "make_out" e;
1306 fun make_inp a b c = make_in a b c handle e => wrap "make_in" e;
1318 fun make_out_thmp a b c = make_out_thm a b c handle e => wrap "make_out_thm" e;
1320 fun make_rec_term func_types rt n = make_outp func_types n (mk_comb(rt,term_of_int n) handle e => wrap "make_rec_term" e);
1328 handle e => wrap "make_single_term" e);
1336 mk_cond(mk_eq(var,term_of_int n),r,f) handle e => wrap "make_f_term" e
1352 handle e => wrap "make_c_term" e)
1362 handle UNCHANGED => raise UNCHANGED | e => wrap "FTERM_CONV" e
1393 in list_mk_abs([x_var',rlt',rrt',v],ft) handle e => wrap "" e end
1397 (butlast call_graph))) handle e => wrap "" e;
1400 handle e => wrap "" e
1401 val thm2 = BETA_RULE (INST [f0 |-> f0term, c0 |-> c0term] thm1) handle e => wrap "" e
1407 handle e => wrap "" e
1410 handle e => wrap "" e;
1419 end) thm4 call_graph handle e => wrap "" e
1422 (INST_TYPE [res_t |-> ``:num`` --> sum_t] thm)) thm5 handle e => wrap "" e
1433 fun wrap "" e = wrapException "instantiate_mutual_theorem" e
1434 | wrap s e = wrapException ("instantiate_mutual_theorem (" ^ s ^ ")") e
1462 handle e => wrap "instantiate_clause" e
1470 insttt mthm) handle e => wrap "instantiate_clause" e
1502 args thm_clauses handle e => wrap "" e;
1509 thm_clauses' split_term handle e => wrap "" e;
1521 handle e => wrap "" e
1524 CHOOSE_L (fst (strip_exists (concl mthm')),mthm') thm2 handle e => wrap "" e
1530 fun wrap e = wrapException "create_ind_theorem" e
1550 call_graph handle e => wrap e
1552 map (fn (n,_) => mk_forall(x,mk_imp(mk_neg(isPcomb),mkP_var n))) call_graph handle e => wrap e
1555 handle e => wrap e
1561 ind_terms_pre)) handle e => wrap e
1563 dest_imp_only o concl o SPEC_ALL) full_ind_thm handle e => wrap e
1568 handle e => wrap e
1574 handle e => wrap e
1673 fun wrap e = wrapException "prove_induction_recursion_thms" e;
1823 val (non_rec_terms,rec_terms) = partition (is_single_constructor scheme) clauses handle e => wrap e
1825 val non_rec_terms' = map fix_nr_term non_rec_terms handle e => wrap e
1834 handle e => wrap e
1835 val (induction,mapping) = add_redundant_ind clauses scheme induction1 handle e => wrap e
1860 val thm2 = foldr (fn (v,thm) => SIMPLE_EXISTS v thm) thm1 f_terms handle e => wrap e
1881 handle e => wrap e
2778 fun wrap "" e = wrapException ("expanded_function_def") e
2779 | wrap s e = wrapException ("expanded_function_def (" ^ s ^ ")") e;
2787 LIST_CONJ (map (gen1 vars o SPEC_ALL) (CONJUNCTS thm)) handle e => wrap "GEN_RAND" e
2790 GEN_RAND vars (LIST_CONJ (map (C (PART_MATCH (rator o lhs)) term) (CONJUNCTS thm)) handle e => wrap "inst_it" e)
2797 (concl main) handle e => wrap "single_inst" e)
2822 val base_types = split_nested_recursive_set (base_type t) handle e => wrap "" e
2823 val functions = map (get_def ## map get_def o fst) base_types handle e => wrap "" e
2856 let fun wrap e = wrapException ("mk_split_" ^ func ^ "_function (mk_eq_thm)") e
2859 val terms = map (mk_term o fst) recursive_types handle e => wrap e
2860 val pair = CONV_RULE conv (get_def tm) handle e => wrap e
2863 val term = list_mk_conj (flatten (map strip_conj terms)) handle e => wrap e
2867 SPLIT_FUNCTION_CONV (is_double_term_source,pair) hfuns) term handle e => wrap e
2931 fun wrap "" e = wrapException "strengthenProof" e
2932 | wrap s e = wrapException ("strengthenProof (" ^ s ^ ")") e
2941 handle e => wrap "undef_hofs" e;
2946 handle e => wrap "gen_const" e;
2951 handle e => wrap "match_term" e;
2966 end handle e => wrap "add_defs_conv" e;
2977 val (ante,conc) = guarenteed dest_imp_only term handle e => wrap "" e;
2978 val clauses = strip_conj ante handle e => wrap "" e;
2979 val funcs = map (rator o lhs o snd o strip_forall) clauses handle e => wrap "" e;
2984 handle e => wrap "" e
2985 val new_term = guarenteed (fst o dest_imp_only o concl) thm1 handle e => wrap "" e
2992 handle e => wrap "" e
2993 val subs = subst (map (op|-> o dest_eq o snd o strip_forall) (strip_conj conc)) handle e => wrap "" e
2996 handle e => wrap "" e
2997 val final_term = mk_imp(fst (dest_imp_only new_term),list_mk_conj conc') handle e => wrap "" e
3001 (strip_conj conc))))) handle e => wrap "" e
3008 fun wrap e = wrapException "prove_split_term" e
3016 val equivs = (map ((I ## dest_eq) o strip_forall) o strip_conj o snd o dest_imp_only) term handle e => wrap e
3018 val tt = mk_forall(mk_var("t",alpha),mk_comb(mk_var("P",alpha --> bool),mk_var("t",alpha))) handle e => wrap e
3024 induction handle e => wrap e
3027 (strip_conj (fst (dest_imp_only term)))) handle e => wrap e;
3045 (list_mk_forall(a,mk_eq b))) match))) handle e => wrap e
3056 val assums = map (SPEC_ALL o ASSUME) ((strip_conj o fst o dest_imp_only) term) handle e => wrap e
3085 val terms = (strip_conj o fst o dest_imp_only o concl) inst handle e => wrap e
3118 (mk_eq((snd o dest_imp_only o concl) inst,(snd o dest_imp_only) term)))))) inst handle e => wrap e
3133 fun wrap "" e = wrapException "prove_all_split_terms" e
3134 | wrap s e = wrapException ("prove_all_split_terms (" ^ s ^ ")") e
3148 handle e => wrap "full_prove_split_term" e
3149 val (induction,mapping) = get_ind t handle e => wrap "full_prove_split_term" e
3204 handle e => wrap "" e
3209 fun wrap "" e = wrapException "remove_hyp_terms" e
3210 | wrap s e = wrapException ("remove_hyp_terms (" ^ s ^ ")") e
3224 end handle e => wrap "fix_pair1" e
3230 end handle e => wrap "fix_pair2" e
3241 end handle Empty => raise Empty | e => wrap "PROVE_HYP_CONJ" e
3304 fun wrap e = wrapException "unsplit_function" e
3345 (CONJUNCTS (ASSUME mterm)))) handle e => wrap e
3349 val prod = pairLib.mk_prod(alpha,beta) handle e => wrap e
3352 val pair_thm = get_def prod handle e => wrap e
3353 val matches = zip (map get_func htypes) htypes handle e => wrap e
3354 val (proofs,thm') = prove_all_split_terms (get_ind,get_def,conv,create_conv,dead_thm,dead_value) matches thm handle e => wrap e
3355 val thm'' = remove_hyp_terms pair_thm proofs (mthms,thm') handle e => wrap e
3359 val hyp_vars = fst (strip_exists (concl mthm)) handle e => wrap e
3361 handle e => wrap e
3364 handle e => wrap e
3411 fun wrap e = wrapException "mk_source_functions" e
3413 val (mthm,ethm) = mk_split_source_function mk_term get_def get_func conv create_conv t handle e => wrap e
3416 get_def get_func conv create_conv (TRUTH,mk_arb alpha) t (mthm,ethm) handle e => wrap e
3424 fun wrap e = wrapException "mk_coding_functions" e
3426 val (mthm,ethm) = mk_split_source_function mk_term get_def get_func conv create_conv t handle e => wrap e
3431 get_def get_func conv create_conv (dead_thm,dead_value) t (mthm,ethm) handle e => wrap e
3441 fun wrap e = wrapException "mk_target_functions" e
3446 (get_translation_scheme target) t handle e => wrap e
3448 val result = complete_function name mk_term get_ind get_def get_func conv create_conv (dead_thm,dead_value) t (mthm,ethm) handle e => wrap e