src/HOL/Tools/BNF/Tools/bnf_util.ML
changeset 55058 4e700eb471d4
parent 54921 862c36b6e57c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/BNF/Tools/bnf_util.ML	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -0,0 +1,583 @@
     1.4 +(*  Title:      HOL/BNF/Tools/bnf_util.ML
     1.5 +    Author:     Dmitriy Traytel, TU Muenchen
     1.6 +    Copyright   2012
     1.7 +
     1.8 +Library for bounded natural functors.
     1.9 +*)
    1.10 +
    1.11 +signature BNF_UTIL =
    1.12 +sig
    1.13 +  include CTR_SUGAR_UTIL
    1.14 +
    1.15 +  val map6: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g) ->
    1.16 +    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list
    1.17 +  val map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) ->
    1.18 +    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list
    1.19 +  val map8: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i) ->
    1.20 +    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> 'i list
    1.21 +  val map9: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j) ->
    1.22 +    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
    1.23 +    'i list -> 'j list
    1.24 +  val map10: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k) ->
    1.25 +    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
    1.26 +    'i list -> 'j list -> 'k list
    1.27 +  val map11: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l) ->
    1.28 +    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
    1.29 +    'i list -> 'j list -> 'k list -> 'l list
    1.30 +  val map12: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm) ->
    1.31 +    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
    1.32 +    'i list -> 'j list -> 'k list -> 'l list -> 'm list
    1.33 +  val map13: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n) ->
    1.34 +    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
    1.35 +    'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list
    1.36 +  val map14:
    1.37 +    ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n -> 'o) ->
    1.38 +    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
    1.39 +    'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list
    1.40 +  val fold_map4: ('a -> 'b -> 'c -> 'd -> 'e -> 'f * 'e) ->
    1.41 +    'a list -> 'b list -> 'c list -> 'd list -> 'e -> 'f list * 'e
    1.42 +  val fold_map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g * 'f) ->
    1.43 +    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f -> 'g list * 'f
    1.44 +  val fold_map6: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h * 'g) ->
    1.45 +    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g -> 'h list * 'g
    1.46 +  val fold_map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i * 'h) ->
    1.47 +    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h -> 'i list * 'h
    1.48 +  val fold_map8: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j * 'i) ->
    1.49 +    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> 'i ->
    1.50 +    'j list * 'i
    1.51 +  val fold_map9: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k * 'j) ->
    1.52 +    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
    1.53 +    'i list -> 'j -> 'k list * 'j
    1.54 +  val split_list4: ('a * 'b * 'c * 'd) list -> 'a list * 'b list * 'c list * 'd list
    1.55 +  val split_list5: ('a * 'b * 'c * 'd * 'e) list -> 'a list * 'b list * 'c list * 'd list * 'e list
    1.56 +  val find_indices: ('b * 'a -> bool) -> 'a list -> 'b list -> int list
    1.57 +
    1.58 +  val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context
    1.59 +  val mk_Freesss: string -> typ list list list -> Proof.context ->
    1.60 +    term list list list * Proof.context
    1.61 +  val mk_Freessss: string -> typ list list list list -> Proof.context ->
    1.62 +    term list list list list * Proof.context
    1.63 +  val nonzero_string_of_int: int -> string
    1.64 +  val retype_free: typ -> term -> term
    1.65 +
    1.66 +  val binder_fun_types: typ -> typ list
    1.67 +  val body_fun_type: typ -> typ
    1.68 +  val num_binder_types: typ -> int
    1.69 +  val strip_fun_type: typ -> typ list * typ
    1.70 +  val strip_typeN: int -> typ -> typ list * typ
    1.71 +
    1.72 +  val mk_pred2T: typ -> typ -> typ
    1.73 +  val mk_relT: typ * typ -> typ
    1.74 +  val dest_relT: typ -> typ * typ
    1.75 +  val dest_pred2T: typ -> typ * typ
    1.76 +  val mk_sumT: typ * typ -> typ
    1.77 +
    1.78 +  val ctwo: term
    1.79 +  val fst_const: typ -> term
    1.80 +  val snd_const: typ -> term
    1.81 +  val Id_const: typ -> term
    1.82 +
    1.83 +  val mk_Ball: term -> term -> term
    1.84 +  val mk_Bex: term -> term -> term
    1.85 +  val mk_Card_order: term -> term
    1.86 +  val mk_Field: term -> term
    1.87 +  val mk_Gr: term -> term -> term
    1.88 +  val mk_Grp: term -> term -> term
    1.89 +  val mk_UNION: term -> term -> term
    1.90 +  val mk_Union: typ -> term
    1.91 +  val mk_card_binop: string -> (typ * typ -> typ) -> term -> term -> term
    1.92 +  val mk_card_of: term -> term
    1.93 +  val mk_card_order: term -> term
    1.94 +  val mk_cexp: term -> term -> term
    1.95 +  val mk_cinfinite: term -> term
    1.96 +  val mk_collect: term list -> typ -> term
    1.97 +  val mk_converse: term -> term
    1.98 +  val mk_conversep: term -> term
    1.99 +  val mk_cprod: term -> term -> term
   1.100 +  val mk_csum: term -> term -> term
   1.101 +  val mk_dir_image: term -> term -> term
   1.102 +  val mk_fun_rel: term -> term -> term
   1.103 +  val mk_image: term -> term
   1.104 +  val mk_in: term list -> term list -> typ -> term
   1.105 +  val mk_leq: term -> term -> term
   1.106 +  val mk_ordLeq: term -> term -> term
   1.107 +  val mk_rel_comp: term * term -> term
   1.108 +  val mk_rel_compp: term * term -> term
   1.109 +
   1.110 +  (*parameterized terms*)
   1.111 +  val mk_nthN: int -> term -> int -> term
   1.112 +
   1.113 +  (*parameterized thms*)
   1.114 +  val mk_Un_upper: int -> int -> thm
   1.115 +  val mk_conjIN: int -> thm
   1.116 +  val mk_conjunctN: int -> int -> thm
   1.117 +  val conj_dests: int -> thm -> thm list
   1.118 +  val mk_nthI: int -> int -> thm
   1.119 +  val mk_nth_conv: int -> int -> thm
   1.120 +  val mk_ordLeq_csum: int -> int -> thm -> thm
   1.121 +  val mk_UnIN: int -> int -> thm
   1.122 +
   1.123 +  val Pair_eqD: thm
   1.124 +  val Pair_eqI: thm
   1.125 +  val ctrans: thm
   1.126 +  val id_apply: thm
   1.127 +  val meta_mp: thm
   1.128 +  val meta_spec: thm
   1.129 +  val o_apply: thm
   1.130 +  val set_mp: thm
   1.131 +  val set_rev_mp: thm
   1.132 +  val subset_UNIV: thm
   1.133 +  val mk_sym: thm -> thm
   1.134 +  val mk_trans: thm -> thm -> thm
   1.135 +
   1.136 +  val is_refl: thm -> bool
   1.137 +  val is_concl_refl: thm -> bool
   1.138 +  val no_refl: thm list -> thm list
   1.139 +  val no_reflexive: thm list -> thm list
   1.140 +
   1.141 +  val fold_thms: Proof.context -> thm list -> thm -> thm
   1.142 +
   1.143 +  val parse_binding_colon: binding parser
   1.144 +  val parse_opt_binding_colon: binding parser
   1.145 +  val parse_type_args_named_constrained: (binding option * (string * string option)) list parser
   1.146 +  val parse_map_rel_bindings: (binding * binding) parser
   1.147 +
   1.148 +  val typedef: binding * (string * sort) list * mixfix -> term ->
   1.149 +    (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory
   1.150 +end;
   1.151 +
   1.152 +structure BNF_Util : BNF_UTIL =
   1.153 +struct
   1.154 +
   1.155 +open Ctr_Sugar_Util
   1.156 +
   1.157 +(* Library proper *)
   1.158 +
   1.159 +fun map6 _ [] [] [] [] [] [] = []
   1.160 +  | map6 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) =
   1.161 +    f x1 x2 x3 x4 x5 x6 :: map6 f x1s x2s x3s x4s x5s x6s
   1.162 +  | map6 _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   1.163 +
   1.164 +fun map7 _ [] [] [] [] [] [] [] = []
   1.165 +  | map7 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) =
   1.166 +    f x1 x2 x3 x4 x5 x6 x7 :: map7 f x1s x2s x3s x4s x5s x6s x7s
   1.167 +  | map7 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   1.168 +
   1.169 +fun map8 _ [] [] [] [] [] [] [] [] = []
   1.170 +  | map8 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s) =
   1.171 +    f x1 x2 x3 x4 x5 x6 x7 x8 :: map8 f x1s x2s x3s x4s x5s x6s x7s x8s
   1.172 +  | map8 _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   1.173 +
   1.174 +fun map9 _ [] [] [] [] [] [] [] [] [] = []
   1.175 +  | map9 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
   1.176 +      (x9::x9s) =
   1.177 +    f x1 x2 x3 x4 x5 x6 x7 x8 x9 :: map9 f x1s x2s x3s x4s x5s x6s x7s x8s x9s
   1.178 +  | map9 _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   1.179 +
   1.180 +fun map10 _ [] [] [] [] [] [] [] [] [] [] = []
   1.181 +  | map10 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
   1.182 +      (x9::x9s) (x10::x10s) =
   1.183 +    f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 :: map10 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s
   1.184 +  | map10 _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   1.185 +
   1.186 +fun map11 _ [] [] [] [] [] [] [] [] [] [] [] = []
   1.187 +  | map11 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
   1.188 +      (x9::x9s) (x10::x10s) (x11::x11s) =
   1.189 +    f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 :: map11 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s
   1.190 +  | map11 _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   1.191 +
   1.192 +fun map12 _ [] [] [] [] [] [] [] [] [] [] [] [] = []
   1.193 +  | map12 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
   1.194 +      (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) =
   1.195 +    f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ::
   1.196 +      map12 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s
   1.197 +  | map12 _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   1.198 +
   1.199 +fun map13 _ [] [] [] [] [] [] [] [] [] [] [] [] [] = []
   1.200 +  | map13 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
   1.201 +      (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) =
   1.202 +    f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ::
   1.203 +      map13 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s
   1.204 +  | map13 _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   1.205 +
   1.206 +fun map14 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] = []
   1.207 +  | map14 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
   1.208 +      (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) =
   1.209 +    f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ::
   1.210 +      map14 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s
   1.211 +  | map14 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   1.212 +
   1.213 +fun fold_map4 _ [] [] [] [] acc = ([], acc)
   1.214 +  | fold_map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) acc =
   1.215 +    let
   1.216 +      val (x, acc') = f x1 x2 x3 x4 acc;
   1.217 +      val (xs, acc'') = fold_map4 f x1s x2s x3s x4s acc';
   1.218 +    in (x :: xs, acc'') end
   1.219 +  | fold_map4 _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   1.220 +
   1.221 +fun fold_map5 _ [] [] [] [] [] acc = ([], acc)
   1.222 +  | fold_map5 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) acc =
   1.223 +    let
   1.224 +      val (x, acc') = f x1 x2 x3 x4 x5 acc;
   1.225 +      val (xs, acc'') = fold_map5 f x1s x2s x3s x4s x5s acc';
   1.226 +    in (x :: xs, acc'') end
   1.227 +  | fold_map5 _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   1.228 +
   1.229 +fun fold_map6 _ [] [] [] [] [] [] acc = ([], acc)
   1.230 +  | fold_map6 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) acc =
   1.231 +    let
   1.232 +      val (x, acc') = f x1 x2 x3 x4 x5 x6 acc;
   1.233 +      val (xs, acc'') = fold_map6 f x1s x2s x3s x4s x5s x6s acc';
   1.234 +    in (x :: xs, acc'') end
   1.235 +  | fold_map6 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   1.236 +
   1.237 +fun fold_map7 _ [] [] [] [] [] [] [] acc = ([], acc)
   1.238 +  | fold_map7 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) acc =
   1.239 +    let
   1.240 +      val (x, acc') = f x1 x2 x3 x4 x5 x6 x7 acc;
   1.241 +      val (xs, acc'') = fold_map7 f x1s x2s x3s x4s x5s x6s x7s acc';
   1.242 +    in (x :: xs, acc'') end
   1.243 +  | fold_map7 _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   1.244 +
   1.245 +fun fold_map8 _ [] [] [] [] [] [] [] [] acc = ([], acc)
   1.246 +  | fold_map8 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
   1.247 +      acc =
   1.248 +    let
   1.249 +      val (x, acc') = f x1 x2 x3 x4 x5 x6 x7 x8 acc;
   1.250 +      val (xs, acc'') = fold_map8 f x1s x2s x3s x4s x5s x6s x7s x8s acc';
   1.251 +    in (x :: xs, acc'') end
   1.252 +  | fold_map8 _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   1.253 +
   1.254 +fun fold_map9 _ [] [] [] [] [] [] [] [] [] acc = ([], acc)
   1.255 +  | fold_map9 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
   1.256 +      (x9::x9s) acc =
   1.257 +    let
   1.258 +      val (x, acc') = f x1 x2 x3 x4 x5 x6 x7 x8 x9 acc;
   1.259 +      val (xs, acc'') = fold_map9 f x1s x2s x3s x4s x5s x6s x7s x8s x9s acc';
   1.260 +    in (x :: xs, acc'') end
   1.261 +  | fold_map9 _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   1.262 +
   1.263 +fun split_list4 [] = ([], [], [], [])
   1.264 +  | split_list4 ((x1, x2, x3, x4) :: xs) =
   1.265 +    let val (xs1, xs2, xs3, xs4) = split_list4 xs;
   1.266 +    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4) end;
   1.267 +
   1.268 +fun split_list5 [] = ([], [], [], [], [])
   1.269 +  | split_list5 ((x1, x2, x3, x4, x5) :: xs) =
   1.270 +    let val (xs1, xs2, xs3, xs4, xs5) = split_list5 xs;
   1.271 +    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5) end;
   1.272 +
   1.273 +val parse_binding_colon = parse_binding --| @{keyword ":"};
   1.274 +val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty;
   1.275 +
   1.276 +val parse_type_arg_constrained =
   1.277 +  Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort);
   1.278 +
   1.279 +val parse_type_arg_named_constrained =
   1.280 +   (Parse.minus --| @{keyword ":"} >> K NONE || parse_opt_binding_colon >> SOME) --
   1.281 +   parse_type_arg_constrained;
   1.282 +
   1.283 +val parse_type_args_named_constrained =
   1.284 +  parse_type_arg_constrained >> (single o pair (SOME Binding.empty)) ||
   1.285 +  @{keyword "("} |-- Parse.!!! (Parse.list1 parse_type_arg_named_constrained --| @{keyword ")"}) ||
   1.286 +  Scan.succeed [];
   1.287 +
   1.288 +val parse_map_rel_binding = Parse.short_ident --| @{keyword ":"} -- parse_binding;
   1.289 +
   1.290 +val no_map_rel = (Binding.empty, Binding.empty);
   1.291 +
   1.292 +fun extract_map_rel ("map", b) = apfst (K b)
   1.293 +  | extract_map_rel ("rel", b) = apsnd (K b)
   1.294 +  | extract_map_rel (s, _) = error ("Unknown label " ^ quote s ^ " (expected \"map\" or \"rel\")");
   1.295 +
   1.296 +val parse_map_rel_bindings =
   1.297 +  @{keyword "("} |-- Scan.repeat parse_map_rel_binding --| @{keyword ")"}
   1.298 +    >> (fn ps => fold extract_map_rel ps no_map_rel) ||
   1.299 +  Scan.succeed no_map_rel;
   1.300 +
   1.301 +
   1.302 +(*TODO: is this really different from Typedef.add_typedef_global?*)
   1.303 +fun typedef (b, Ts, mx) set opt_morphs tac lthy =
   1.304 +  let
   1.305 +    (*Work around loss of qualification in "typedef" axioms by replicating it in the name*)
   1.306 +    val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (#2 (Binding.dest b))) b;
   1.307 +    val ((name, info), (lthy, lthy_old)) =
   1.308 +      lthy
   1.309 +      |> Typedef.add_typedef (b', Ts, mx) set opt_morphs tac
   1.310 +      ||> `Local_Theory.restore;
   1.311 +    val phi = Proof_Context.export_morphism lthy_old lthy;
   1.312 +  in
   1.313 +    ((name, Typedef.transform_info phi info), lthy)
   1.314 +  end;
   1.315 +
   1.316 +
   1.317 +
   1.318 +(* Term construction *)
   1.319 +
   1.320 +(** Fresh variables **)
   1.321 +
   1.322 +fun nonzero_string_of_int 0 = ""
   1.323 +  | nonzero_string_of_int n = string_of_int n;
   1.324 +
   1.325 +val mk_TFreess = fold_map mk_TFrees;
   1.326 +
   1.327 +fun mk_Freesss x Tsss = fold_map2 mk_Freess (mk_names (length Tsss) x) Tsss;
   1.328 +fun mk_Freessss x Tssss = fold_map2 mk_Freesss (mk_names (length Tssss) x) Tssss;
   1.329 +
   1.330 +fun retype_free T (Free (s, _)) = Free (s, T)
   1.331 +  | retype_free _ t = raise TERM ("retype_free", [t]);
   1.332 +
   1.333 +
   1.334 +(** Types **)
   1.335 +
   1.336 +(*stolen from ~~/src/HOL/Tools/Nitpick/nitpick_hol.ML*)
   1.337 +fun num_binder_types (Type (@{type_name fun}, [_, T2])) =
   1.338 +    1 + num_binder_types T2
   1.339 +  | num_binder_types _ = 0
   1.340 +
   1.341 +(*maps [T1,...,Tn]--->T to ([T1,T2,...,Tn], T)*)
   1.342 +fun strip_typeN 0 T = ([], T)
   1.343 +  | strip_typeN n (Type (@{type_name fun}, [T, T'])) = strip_typeN (n - 1) T' |>> cons T
   1.344 +  | strip_typeN _ T = raise TYPE ("strip_typeN", [T], []);
   1.345 +
   1.346 +(*maps [T1,...,Tn]--->T-->U to ([T1,T2,...,Tn], T-->U), where U is not a function type*)
   1.347 +fun strip_fun_type T = strip_typeN (num_binder_types T - 1) T;
   1.348 +
   1.349 +val binder_fun_types = fst o strip_fun_type;
   1.350 +val body_fun_type = snd o strip_fun_type;
   1.351 +
   1.352 +fun mk_pred2T T U = mk_predT [T, U];
   1.353 +val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT;
   1.354 +val dest_relT = HOLogic.dest_prodT o HOLogic.dest_setT;
   1.355 +val dest_pred2T = apsnd Term.domain_type o Term.dest_funT;
   1.356 +fun mk_sumT (LT, RT) = Type (@{type_name Sum_Type.sum}, [LT, RT]);
   1.357 +
   1.358 +
   1.359 +(** Constants **)
   1.360 +
   1.361 +fun fst_const T = Const (@{const_name fst}, T --> fst (HOLogic.dest_prodT T));
   1.362 +fun snd_const T = Const (@{const_name snd}, T --> snd (HOLogic.dest_prodT T));
   1.363 +fun Id_const T = Const (@{const_name Id}, mk_relT (T, T));
   1.364 +
   1.365 +
   1.366 +(** Operators **)
   1.367 +
   1.368 +fun mk_converse R =
   1.369 +  let
   1.370 +    val RT = dest_relT (fastype_of R);
   1.371 +    val RST = mk_relT (snd RT, fst RT);
   1.372 +  in Const (@{const_name converse}, fastype_of R --> RST) $ R end;
   1.373 +
   1.374 +fun mk_rel_comp (R, S) =
   1.375 +  let
   1.376 +    val RT = fastype_of R;
   1.377 +    val ST = fastype_of S;
   1.378 +    val RST = mk_relT (fst (dest_relT RT), snd (dest_relT ST));
   1.379 +  in Const (@{const_name relcomp}, RT --> ST --> RST) $ R $ S end;
   1.380 +
   1.381 +fun mk_Gr A f =
   1.382 +  let val ((AT, BT), FT) = `dest_funT (fastype_of f);
   1.383 +  in Const (@{const_name Gr}, HOLogic.mk_setT AT --> FT --> mk_relT (AT, BT)) $ A $ f end;
   1.384 +
   1.385 +fun mk_conversep R =
   1.386 +  let
   1.387 +    val RT = dest_pred2T (fastype_of R);
   1.388 +    val RST = mk_pred2T (snd RT) (fst RT);
   1.389 +  in Const (@{const_name conversep}, fastype_of R --> RST) $ R end;
   1.390 +
   1.391 +fun mk_rel_compp (R, S) =
   1.392 +  let
   1.393 +    val RT = fastype_of R;
   1.394 +    val ST = fastype_of S;
   1.395 +    val RST = mk_pred2T (fst (dest_pred2T RT)) (snd (dest_pred2T ST));
   1.396 +  in Const (@{const_name relcompp}, RT --> ST --> RST) $ R $ S end;
   1.397 +
   1.398 +fun mk_Grp A f =
   1.399 +  let val ((AT, BT), FT) = `dest_funT (fastype_of f);
   1.400 +  in Const (@{const_name Grp}, HOLogic.mk_setT AT --> FT --> mk_pred2T AT BT) $ A $ f end;
   1.401 +
   1.402 +fun mk_image f =
   1.403 +  let val (T, U) = dest_funT (fastype_of f);
   1.404 +  in Const (@{const_name image},
   1.405 +    (T --> U) --> (HOLogic.mk_setT T) --> (HOLogic.mk_setT U)) $ f end;
   1.406 +
   1.407 +fun mk_Ball X f =
   1.408 +  Const (@{const_name Ball}, fastype_of X --> fastype_of f --> HOLogic.boolT) $ X $ f;
   1.409 +
   1.410 +fun mk_Bex X f =
   1.411 +  Const (@{const_name Bex}, fastype_of X --> fastype_of f --> HOLogic.boolT) $ X $ f;
   1.412 +
   1.413 +fun mk_UNION X f =
   1.414 +  let val (T, U) = dest_funT (fastype_of f);
   1.415 +  in Const (@{const_name SUPR}, fastype_of X --> (T --> U) --> U) $ X $ f end;
   1.416 +
   1.417 +fun mk_Union T =
   1.418 +  Const (@{const_name Sup}, HOLogic.mk_setT (HOLogic.mk_setT T) --> HOLogic.mk_setT T);
   1.419 +
   1.420 +fun mk_Field r =
   1.421 +  let val T = fst (dest_relT (fastype_of r));
   1.422 +  in Const (@{const_name Field}, mk_relT (T, T) --> HOLogic.mk_setT T) $ r end;
   1.423 +
   1.424 +fun mk_card_order bd =
   1.425 +  let
   1.426 +    val T = fastype_of bd;
   1.427 +    val AT = fst (dest_relT T);
   1.428 +  in
   1.429 +    Const (@{const_name card_order_on}, HOLogic.mk_setT AT --> T --> HOLogic.boolT) $
   1.430 +      (HOLogic.mk_UNIV AT) $ bd
   1.431 +  end;
   1.432 +
   1.433 +fun mk_Card_order bd =
   1.434 +  let
   1.435 +    val T = fastype_of bd;
   1.436 +    val AT = fst (dest_relT T);
   1.437 +  in
   1.438 +    Const (@{const_name card_order_on}, HOLogic.mk_setT AT --> T --> HOLogic.boolT) $
   1.439 +      mk_Field bd $ bd
   1.440 +  end;
   1.441 +
   1.442 +fun mk_cinfinite bd =
   1.443 +  Const (@{const_name cinfinite}, fastype_of bd --> HOLogic.boolT) $ bd;
   1.444 +
   1.445 +fun mk_ordLeq t1 t2 =
   1.446 +  HOLogic.mk_mem (HOLogic.mk_prod (t1, t2),
   1.447 +    Const (@{const_name ordLeq}, mk_relT (fastype_of t1, fastype_of t2)));
   1.448 +
   1.449 +fun mk_card_of A =
   1.450 +  let
   1.451 +    val AT = fastype_of A;
   1.452 +    val T = HOLogic.dest_setT AT;
   1.453 +  in
   1.454 +    Const (@{const_name card_of}, AT --> mk_relT (T, T)) $ A
   1.455 +  end;
   1.456 +
   1.457 +fun mk_dir_image r f =
   1.458 +  let val (T, U) = dest_funT (fastype_of f);
   1.459 +  in Const (@{const_name dir_image}, mk_relT (T, T) --> (T --> U) --> mk_relT (U, U)) $ r $ f end;
   1.460 +
   1.461 +fun mk_fun_rel R S =
   1.462 +  let
   1.463 +    val ((RA, RB), RT) = `dest_pred2T (fastype_of R);
   1.464 +    val ((SA, SB), ST) = `dest_pred2T (fastype_of S);
   1.465 +  in Const (@{const_name fun_rel}, RT --> ST --> mk_pred2T (RA --> SA) (RB --> SB)) $ R $ S end;
   1.466 +
   1.467 +(*FIXME: "x"?*)
   1.468 +(*(nth sets i) must be of type "T --> 'ai set"*)
   1.469 +fun mk_in As sets T =
   1.470 +  let
   1.471 +    fun in_single set A =
   1.472 +      let val AT = fastype_of A;
   1.473 +      in Const (@{const_name less_eq},
   1.474 +        AT --> AT --> HOLogic.boolT) $ (set $ Free ("x", T)) $ A end;
   1.475 +  in
   1.476 +    if length sets > 0
   1.477 +    then HOLogic.mk_Collect ("x", T, foldr1 (HOLogic.mk_conj) (map2 in_single sets As))
   1.478 +    else HOLogic.mk_UNIV T
   1.479 +  end;
   1.480 +
   1.481 +fun mk_leq t1 t2 =
   1.482 +  Const (@{const_name less_eq}, (fastype_of t1) --> (fastype_of t2) --> HOLogic.boolT) $ t1 $ t2;
   1.483 +
   1.484 +fun mk_card_binop binop typop t1 t2 =
   1.485 +  let
   1.486 +    val (T1, relT1) = `(fst o dest_relT) (fastype_of t1);
   1.487 +    val (T2, relT2) = `(fst o dest_relT) (fastype_of t2);
   1.488 +  in
   1.489 +    Const (binop, relT1 --> relT2 --> mk_relT (typop (T1, T2), typop (T1, T2))) $ t1 $ t2
   1.490 +  end;
   1.491 +
   1.492 +val mk_csum = mk_card_binop @{const_name csum} mk_sumT;
   1.493 +val mk_cprod = mk_card_binop @{const_name cprod} HOLogic.mk_prodT;
   1.494 +val mk_cexp = mk_card_binop @{const_name cexp} (op --> o swap);
   1.495 +val ctwo = @{term ctwo};
   1.496 +
   1.497 +fun mk_collect xs defT =
   1.498 +  let val T = (case xs of [] => defT | (x::_) => fastype_of x);
   1.499 +  in Const (@{const_name collect}, HOLogic.mk_setT T --> T) $ (HOLogic.mk_set T xs) end;
   1.500 +
   1.501 +fun find_indices eq xs ys = map_filter I
   1.502 +  (map_index (fn (i, y) => if member eq xs y then SOME i else NONE) ys);
   1.503 +
   1.504 +fun mk_trans thm1 thm2 = trans OF [thm1, thm2];
   1.505 +fun mk_sym thm = thm RS sym;
   1.506 +
   1.507 +(*TODO: antiquote heavily used theorems once*)
   1.508 +val Pair_eqD = @{thm iffD1[OF Pair_eq]};
   1.509 +val Pair_eqI = @{thm iffD2[OF Pair_eq]};
   1.510 +val ctrans = @{thm ordLeq_transitive};
   1.511 +val id_apply = @{thm id_apply};
   1.512 +val meta_mp = @{thm meta_mp};
   1.513 +val meta_spec = @{thm meta_spec};
   1.514 +val o_apply = @{thm o_apply};
   1.515 +val set_mp = @{thm set_mp};
   1.516 +val set_rev_mp = @{thm set_rev_mp};
   1.517 +val subset_UNIV = @{thm subset_UNIV};
   1.518 +
   1.519 +fun mk_nthN 1 t 1 = t
   1.520 +  | mk_nthN _ t 1 = HOLogic.mk_fst t
   1.521 +  | mk_nthN 2 t 2 = HOLogic.mk_snd t
   1.522 +  | mk_nthN n t m = mk_nthN (n - 1) (HOLogic.mk_snd t) (m - 1);
   1.523 +
   1.524 +fun mk_nth_conv n m =
   1.525 +  let
   1.526 +    fun thm b = if b then @{thm fstI} else @{thm sndI}
   1.527 +    fun mk_nth_conv _ 1 1 = refl
   1.528 +      | mk_nth_conv _ _ 1 = @{thm fst_conv}
   1.529 +      | mk_nth_conv _ 2 2 = @{thm snd_conv}
   1.530 +      | mk_nth_conv b _ 2 = @{thm snd_conv} RS thm b
   1.531 +      | mk_nth_conv b n m = mk_nth_conv false (n - 1) (m - 1) RS thm b;
   1.532 +  in mk_nth_conv (not (m = n)) n m end;
   1.533 +
   1.534 +fun mk_nthI 1 1 = @{thm TrueE[OF TrueI]}
   1.535 +  | mk_nthI n m = fold (curry op RS) (replicate (m - 1) @{thm sndI})
   1.536 +    (if m = n then @{thm TrueE[OF TrueI]} else @{thm fstI});
   1.537 +
   1.538 +fun mk_conjunctN 1 1 = @{thm TrueE[OF TrueI]}
   1.539 +  | mk_conjunctN _ 1 = conjunct1
   1.540 +  | mk_conjunctN 2 2 = conjunct2
   1.541 +  | mk_conjunctN n m = conjunct2 RS (mk_conjunctN (n - 1) (m - 1));
   1.542 +
   1.543 +fun conj_dests n thm = map (fn k => thm RS mk_conjunctN n k) (1 upto n);
   1.544 +
   1.545 +fun mk_conjIN 1 = @{thm TrueE[OF TrueI]}
   1.546 +  | mk_conjIN n = mk_conjIN (n - 1) RSN (2, conjI);
   1.547 +
   1.548 +fun mk_ordLeq_csum 1 1 thm = thm
   1.549 +  | mk_ordLeq_csum _ 1 thm = @{thm ordLeq_transitive} OF [thm, @{thm ordLeq_csum1}]
   1.550 +  | mk_ordLeq_csum 2 2 thm = @{thm ordLeq_transitive} OF [thm, @{thm ordLeq_csum2}]
   1.551 +  | mk_ordLeq_csum n m thm = @{thm ordLeq_transitive} OF
   1.552 +    [mk_ordLeq_csum (n - 1) (m - 1) thm, @{thm ordLeq_csum2[OF Card_order_csum]}];
   1.553 +
   1.554 +local
   1.555 +  fun mk_Un_upper' 0 = subset_refl
   1.556 +    | mk_Un_upper' 1 = @{thm Un_upper1}
   1.557 +    | mk_Un_upper' k = Library.foldr (op RS o swap)
   1.558 +      (replicate (k - 1) @{thm subset_trans[OF Un_upper1]}, @{thm Un_upper1});
   1.559 +in
   1.560 +  fun mk_Un_upper 1 1 = subset_refl
   1.561 +    | mk_Un_upper n 1 = mk_Un_upper' (n - 2) RS @{thm subset_trans[OF Un_upper1]}
   1.562 +    | mk_Un_upper n m = mk_Un_upper' (n - m) RS @{thm subset_trans[OF Un_upper2]};
   1.563 +end;
   1.564 +
   1.565 +local
   1.566 +  fun mk_UnIN' 0 = @{thm UnI2}
   1.567 +    | mk_UnIN' m = mk_UnIN' (m - 1) RS @{thm UnI1};
   1.568 +in
   1.569 +  fun mk_UnIN 1 1 = @{thm TrueE[OF TrueI]}
   1.570 +    | mk_UnIN n 1 = Library.foldr1 (op RS o swap) (replicate (n - 1) @{thm UnI1})
   1.571 +    | mk_UnIN n m = mk_UnIN' (n - m)
   1.572 +end;
   1.573 +
   1.574 +fun is_refl_prop t =
   1.575 +  op aconv (HOLogic.dest_eq (HOLogic.dest_Trueprop t))
   1.576 +  handle TERM _ => false;
   1.577 +
   1.578 +val is_refl = is_refl_prop o Thm.prop_of;
   1.579 +val is_concl_refl = is_refl_prop o Logic.strip_imp_concl o Thm.prop_of;
   1.580 +
   1.581 +val no_refl = filter_out is_refl;
   1.582 +val no_reflexive = filter_out Thm.is_reflexive;
   1.583 +
   1.584 +fun fold_thms ctxt thms = Local_Defs.fold ctxt (distinct Thm.eq_thm_prop thms);
   1.585 +
   1.586 +end;