acl2/ml/polytypicLib.sml

42 (* repeat               : ('a -> 'a) -> 'a -> 'a                             *)
119 fun repeat f x = repeat f (f x) handle e => if isFatal e then raise e else x;
453 fun UNDISCH_ALL_EQ thm = repeat UNDISCH_EQ thm
541                 ((repeat rator o lhs o concl) thm) (map #redex (fst match))
712         val constructors_axiom = map (repeat rator o rand o lhs o snd o strip_forall)
714         val constructors_term = map (repeat rator o rand o lhs o snd o strip_forall) (strip_conj term)
908                 null o set_diff (free_vars term) o map (repeat rator o lhs o snd o strip_forall) o strip_conj]
930 let     val cs = (map (repeat rator o rand o lhs o snd o strip_forall) o strip_conj) term
947 let     val all_fns = map (repeat rator o lhs o snd o strip_forall) (strip_conj term)
957         all (C mem all_fns o repeat rator) shortened
1109         (repeat rator new_term :: fvs,(GSYM rewrite,fst (dest_imp_only (concl func)))) handle e => wrapd e
1120         val funcs = with_exn (mk_set o map (repeat rator o lhs o snd o strip_forall)) clauses func_exn
1176                 ((with_exn (mk_set o map (repeat rator o lhs o snd o strip_forall) o strip_conj) term func_exn),
1254                 ((rev_assoc (repeat rator x) L) :: e_rev_assoc L xs) handle e => e_rev_assoc L xs
1355 let     val (outs,tm) = repeat (fn (l,x) =>
1458                          (not o free_in (rand func) o repeat rator o rhs o concl))] term_rec_thm
1508                                 (repeat rator func |-> list_mk_abs(tl args,(mk_abs(hd args,lhs (concl tc))))) end)
1519                         (zip    (map (repeat rator o fst) split_term)
1520                                 (map (repeat rator o lhs o snd o strip_forall) (strip_conj (concl thm1))))
1723         val zipped = with_exn (zip termsL o map ((repeat rator ## I) o dest_eq o snd o strip_forall)) clauses fun_exn
1766                 val vars = find_terms (C mem all_fns o repeat rator) body
1769                         first (curry op= (snd (fst (first (curry op= (repeat rator vf) o fst o snd) zipped)))
1822         val f_terms = with_exn (mk_set o map (repeat rator o lhs o snd o strip_forall)) clauses fun_exn
1841                                 (curry op= f_term o repeat rator o lhs o snd o strip_forall o concl)
1845         let     val poss = filter (curry op= ((repeat rator o lhs o snd o strip_forall) term) o
1846                                 repeat rator o lhs o rhs o concl) non_rec_terms'
1852         let     val poss = filter (curry op= ((repeat rator o lhs o snd o strip_forall) term) o
1853                                 repeat rator o lhs o rhs o concl) non_rec_terms'
1862         val lset = map (repeat rator o lhs o snd o strip_forall) o strip_conj;
2809 fun inst_pairs recfns vars main pair = repeat (C (single_inst recfns vars) pair) main
2831         val recfns = map (repeat rator o lhs o snd o strip_forall o hd o strip_conj o concl o fst) matched
2982                         (snd (repeat (add_defs_conv fvs functions) (funcs,REFL ante)))) THENC
3267 let     val total = (length o mk_set o map (repeat rator o lhs o snd o strip_forall) o strip_conj o concl) thm
3340                         (err1 mthm,fn t => set_eq       ((map (repeat rator o lhs o snd o strip_forall) o
3344                         (bucket_alist (map (fn x => ((repeat rator o lhs o snd o strip_forall o concl) x,x))
3360         val thm_vars = mk_set (map (repeat rator o lhs o snd o strip_forall) (strip_conj (concl thm'')))
3372         val func_names = map (fst o dest_var o repeat rator o get_func) all_types
3375                         (map (fn x => ((repeat rator o lhs o snd o strip_forall o concl) x,x)) (CONJUNCTS def)))
3376         val all_consts = map2 (curry mk_const) func_names (map (type_of o repeat rator o get_func) all_types)
3575                         (UNDISCH_ONLY (repeat (UNDISCH_ONLY o CONV_RULE