src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
changeset 55058 4e700eb471d4
parent 55057 6b0fcbeebaba
child 55059 ef2e0fb783c6
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Mon Jan 20 18:24:55 2014 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,67 +0,0 @@
     1.4 -(*  Title:      HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
     1.5 -    Author:     Lorenz Panny, TU Muenchen
     1.6 -    Author:     Jasmin Blanchette, TU Muenchen
     1.7 -    Copyright   2013
     1.8 -
     1.9 -Library for recursor and corecursor sugar.
    1.10 -*)
    1.11 -
    1.12 -signature BNF_FP_REC_SUGAR_UTIL =
    1.13 -sig
    1.14 -  val indexed: 'a list -> int -> int list * int
    1.15 -  val indexedd: 'a list list -> int -> int list list * int
    1.16 -  val indexeddd: 'a list list list -> int -> int list list list * int
    1.17 -  val indexedddd: 'a list list list list -> int -> int list list list list * int
    1.18 -  val find_index_eq: ''a list -> ''a -> int
    1.19 -  val finds: ('a * 'b -> bool) -> 'a list -> 'b list -> ('a * 'b list) list * 'b list
    1.20 -
    1.21 -  val drop_all: term -> term
    1.22 -
    1.23 -  val mk_partial_compN: int -> typ -> term -> term
    1.24 -  val mk_partial_comp: typ -> typ -> term -> term
    1.25 -  val mk_compN: int -> typ list -> term * term -> term
    1.26 -  val mk_comp: typ list -> term * term -> term
    1.27 -
    1.28 -  val get_indices: ((binding * typ) * 'a) list -> term -> int list
    1.29 -end;
    1.30 -
    1.31 -structure BNF_FP_Rec_Sugar_Util : BNF_FP_REC_SUGAR_UTIL =
    1.32 -struct
    1.33 -
    1.34 -fun indexe _ h = (h, h + 1);
    1.35 -fun indexed xs = fold_map indexe xs;
    1.36 -fun indexedd xss = fold_map indexed xss;
    1.37 -fun indexeddd xsss = fold_map indexedd xsss;
    1.38 -fun indexedddd xssss = fold_map indexeddd xssss;
    1.39 -
    1.40 -fun find_index_eq hs h = find_index (curry (op =) h) hs;
    1.41 -
    1.42 -fun finds eq = fold_map (fn x => List.partition (curry eq x) #>> pair x);
    1.43 -
    1.44 -fun drop_all t =
    1.45 -  subst_bounds (strip_qnt_vars @{const_name all} t |> map Free |> rev,
    1.46 -    strip_qnt_body @{const_name all} t);
    1.47 -
    1.48 -fun mk_partial_comp gT fT g =
    1.49 -  let val T = domain_type fT --> range_type gT in
    1.50 -    Const (@{const_name Fun.comp}, gT --> fT --> T) $ g
    1.51 -  end;
    1.52 -
    1.53 -fun mk_partial_compN 0 _ g = g
    1.54 -  | mk_partial_compN n fT g =
    1.55 -    let val g' = mk_partial_compN (n - 1) (range_type fT) g in
    1.56 -      mk_partial_comp (fastype_of g') fT g'
    1.57 -    end;
    1.58 -
    1.59 -fun mk_compN n bound_Ts (g, f) =
    1.60 -  let val typof = curry fastype_of1 bound_Ts in
    1.61 -    mk_partial_compN n (typof f) g $ f
    1.62 -  end;
    1.63 -
    1.64 -val mk_comp = mk_compN 1;
    1.65 -
    1.66 -fun get_indices fixes t = map (fst #>> Binding.name_of #> Free) fixes
    1.67 -  |> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE)
    1.68 -  |> map_filter I;
    1.69 -
    1.70 -end;