src/HOL/BNF/Tools/bnf_util.ML
author blanchet
Mon May 06 21:20:54 2013 +0200 (2013-05-06)
changeset 51884 2928fda12661
parent 51861 0a04c2a89ea9
child 51893 596baae88a88
permissions -rw-r--r--
factor out construction of iterator
     1 (*  Title:      HOL/BNF/Tools/bnf_util.ML
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Copyright   2012
     4 
     5 Library for bounded natural functors.
     6 *)
     7 
     8 signature BNF_UTIL =
     9 sig
    10   val map3: ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
    11   val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
    12   val map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f) ->
    13     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list
    14   val map6: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g) ->
    15     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list
    16   val map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) ->
    17     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list
    18   val map8: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i) ->
    19     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> 'i list
    20   val map9: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j) ->
    21     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
    22     'i list -> 'j list
    23   val map10: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k) ->
    24     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
    25     'i list -> 'j list -> 'k list
    26   val map11: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l) ->
    27     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
    28     'i list -> 'j list -> 'k list -> 'l list
    29   val map12: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm) ->
    30     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
    31     'i list -> 'j list -> 'k list -> 'l list -> 'm list
    32   val fold_map2: ('a -> 'b -> 'c -> 'd * 'c) -> 'a list -> 'b list -> 'c -> 'd list * 'c
    33   val fold_map3: ('a -> 'b -> 'c -> 'd -> 'e * 'd) ->
    34     'a list -> 'b list -> 'c list -> 'd -> 'e list * 'd
    35   val fold_map4: ('a -> 'b -> 'c -> 'd -> 'e -> 'f * 'e) ->
    36     'a list -> 'b list -> 'c list -> 'd list -> 'e -> 'f list * 'e
    37   val fold_map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g * 'f) ->
    38     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f -> 'g list * 'f
    39   val fold_map6: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h * 'g) ->
    40     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g -> 'h list * 'g
    41   val fold_map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i * 'h) ->
    42     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h -> 'i list * 'h
    43   val fold_map8: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j * 'i) ->
    44     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> 'i ->
    45     'j list * 'i
    46   val fold_map9: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k * 'j) ->
    47     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
    48     'i list -> 'j -> 'k list * 'j
    49   val splice: 'a list -> 'a list -> 'a list
    50   val transpose: 'a list list -> 'a list list
    51   val unsort: ('a * 'b -> bool) -> 'b list -> 'c list -> 'a list -> 'c list
    52   val seq_conds: (bool -> 'a -> 'b) -> int -> int -> 'a list -> 'b list
    53   val pad_list: 'a -> int -> 'a list -> 'a list
    54 
    55   val mk_fresh_names: Proof.context -> int -> string -> string list * Proof.context
    56   val mk_TFrees: int -> Proof.context -> typ list * Proof.context
    57   val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context
    58   val mk_TFrees': sort list -> Proof.context -> typ list * Proof.context
    59   val mk_Frees: string -> typ list -> Proof.context -> term list * Proof.context
    60   val mk_Freess: string -> typ list list -> Proof.context -> term list list * Proof.context
    61   val mk_Freesss: string -> typ list list list -> Proof.context ->
    62     term list list list * Proof.context
    63   val mk_Freessss: string -> typ list list list list -> Proof.context ->
    64     term list list list list * Proof.context
    65   val mk_Frees': string -> typ list -> Proof.context ->
    66     (term list * (string * typ) list) * Proof.context
    67   val mk_Freess': string -> typ list list -> Proof.context ->
    68     (term list list * (string * typ) list list) * Proof.context
    69   val retype_free: typ -> term -> term
    70   val nonzero_string_of_int: int -> string
    71 
    72   val strip_typeN: int -> typ -> typ list * typ
    73 
    74   val mk_predT: typ list -> typ
    75   val mk_pred1T: typ -> typ
    76   val mk_pred2T: typ -> typ -> typ
    77   val mk_optionT: typ -> typ
    78   val mk_relT: typ * typ -> typ
    79   val dest_relT: typ -> typ * typ
    80   val mk_sumT: typ * typ -> typ
    81 
    82   val ctwo: term
    83   val fst_const: typ -> term
    84   val snd_const: typ -> term
    85   val Id_const: typ -> term
    86 
    87   val mk_Ball: term -> term -> term
    88   val mk_Bex: term -> term -> term
    89   val mk_Card_order: term -> term
    90   val mk_Field: term -> term
    91   val mk_Gr: term -> term -> term
    92   val mk_IfN: typ -> term list -> term list -> term
    93   val mk_Trueprop_eq: term * term -> term
    94   val mk_UNION: term -> term -> term
    95   val mk_Union: typ -> term
    96   val mk_card_binop: string -> (typ * typ -> typ) -> term -> term -> term
    97   val mk_card_of: term -> term
    98   val mk_card_order: term -> term
    99   val mk_ccexp: term -> term -> term
   100   val mk_cexp: term -> term -> term
   101   val mk_cinfinite: term -> term
   102   val mk_collect: term list -> typ -> term
   103   val mk_converse: term -> term
   104   val mk_cprod: term -> term -> term
   105   val mk_csum: term -> term -> term
   106   val mk_dir_image: term -> term -> term
   107   val mk_image: term -> term
   108   val mk_in: term list -> term list -> typ -> term
   109   val mk_ordLeq: term -> term -> term
   110   val mk_rel_comp: term * term -> term
   111   val mk_subset: term -> term -> term
   112   val mk_wpull: term -> term -> term -> term -> term -> (term * term) option -> term -> term -> term
   113 
   114   val rapp: term -> term -> term
   115 
   116   val list_all_free: term list -> term -> term
   117   val list_exists_free: term list -> term -> term
   118 
   119   (*parameterized terms*)
   120   val mk_nthN: int -> term -> int -> term
   121 
   122   (*parameterized thms*)
   123   val mk_Un_upper: int -> int -> thm
   124   val mk_conjIN: int -> thm
   125   val mk_conjunctN: int -> int -> thm
   126   val conj_dests: int -> thm -> thm list
   127   val mk_disjIN: int -> int -> thm
   128   val mk_nthI: int -> int -> thm
   129   val mk_nth_conv: int -> int -> thm
   130   val mk_ordLeq_csum: int -> int -> thm -> thm
   131   val mk_UnIN: int -> int -> thm
   132 
   133   val Pair_eqD: thm
   134   val Pair_eqI: thm
   135   val ctrans: thm
   136   val id_apply: thm
   137   val meta_mp: thm
   138   val meta_spec: thm
   139   val o_apply: thm
   140   val set_mp: thm
   141   val set_rev_mp: thm
   142   val subset_UNIV: thm
   143   val mk_sym: thm -> thm
   144   val mk_trans: thm -> thm -> thm
   145   val mk_unabs_def: int -> thm -> thm
   146 
   147   val is_triv_implies: thm -> bool
   148   val is_refl: thm -> bool
   149   val is_concl_refl: thm -> bool
   150   val no_refl: thm list -> thm list
   151   val no_reflexive: thm list -> thm list
   152 
   153   val cterm_instantiate_pos: cterm option list -> thm -> thm
   154   val fold_thms: Proof.context -> thm list -> thm -> thm
   155   val unfold_thms: Proof.context -> thm list -> thm -> thm
   156 
   157   val mk_permute: ''a list -> ''a list -> 'b list -> 'b list
   158   val find_indices: ''a list -> ''a list -> int list
   159 
   160   val certifyT: Proof.context -> typ -> ctyp
   161   val certify: Proof.context -> term -> cterm
   162 
   163   val standard_binding: binding
   164   val equal_binding: binding
   165   val parse_binding: Token.T list -> binding * Token.T list
   166   val parse_binding_colon: Token.T list -> binding * Token.T list
   167   val parse_opt_binding_colon: Token.T list -> binding * Token.T list
   168 
   169   val typedef: binding * (string * sort) list * mixfix -> term ->
   170     (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory
   171 
   172   val WRAP: ('a -> tactic) -> ('a -> tactic) -> 'a list -> tactic -> tactic
   173   val WRAP': ('a -> int -> tactic) -> ('a -> int -> tactic) -> 'a list -> (int -> tactic) -> int ->
   174     tactic
   175   val CONJ_WRAP_GEN: tactic -> ('a -> tactic) -> 'a list -> tactic
   176   val CONJ_WRAP_GEN': (int -> tactic) -> ('a -> int -> tactic) -> 'a list -> int -> tactic
   177   val CONJ_WRAP: ('a -> tactic) -> 'a list -> tactic
   178   val CONJ_WRAP': ('a -> int -> tactic) -> 'a list -> int -> tactic
   179 end;
   180 
   181 structure BNF_Util : BNF_UTIL =
   182 struct
   183 
   184 (* Library proper *)
   185 
   186 fun map3 _ [] [] [] = []
   187   | map3 f (x1::x1s) (x2::x2s) (x3::x3s) = f x1 x2 x3 :: map3 f x1s x2s x3s
   188   | map3 _ _ _ _ = raise ListPair.UnequalLengths;
   189 
   190 fun map4 _ [] [] [] [] = []
   191   | map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) = f x1 x2 x3 x4 :: map4 f x1s x2s x3s x4s
   192   | map4 _ _ _ _ _ = raise ListPair.UnequalLengths;
   193 
   194 fun map5 _ [] [] [] [] [] = []
   195   | map5 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) =
   196     f x1 x2 x3 x4 x5 :: map5 f x1s x2s x3s x4s x5s
   197   | map5 _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   198 
   199 fun map6 _ [] [] [] [] [] [] = []
   200   | map6 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) =
   201     f x1 x2 x3 x4 x5 x6 :: map6 f x1s x2s x3s x4s x5s x6s
   202   | map6 _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   203 
   204 fun map7 _ [] [] [] [] [] [] [] = []
   205   | map7 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) =
   206     f x1 x2 x3 x4 x5 x6 x7 :: map7 f x1s x2s x3s x4s x5s x6s x7s
   207   | map7 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   208 
   209 fun map8 _ [] [] [] [] [] [] [] [] = []
   210   | map8 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s) =
   211     f x1 x2 x3 x4 x5 x6 x7 x8 :: map8 f x1s x2s x3s x4s x5s x6s x7s x8s
   212   | map8 _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   213 
   214 fun map9 _ [] [] [] [] [] [] [] [] [] = []
   215   | map9 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s)
   216       (x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) =
   217     f x1 x2 x3 x4 x5 x6 x7 x8 x9 :: map9 f x1s x2s x3s x4s x5s x6s x7s x8s x9s
   218   | map9 _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   219 
   220 fun map10 _ [] [] [] [] [] [] [] [] [] [] = []
   221   | map10 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s)
   222       (x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) (x10::x10s) =
   223     f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 :: map10 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s
   224   | map10 _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   225 
   226 fun map11 _ [] [] [] [] [] [] [] [] [] [] [] = []
   227   | map11 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s)
   228       (x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) (x10::x10s) (x11::x11s) =
   229     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
   230   | map11 _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   231 
   232 fun map12 _ [] [] [] [] [] [] [] [] [] [] [] [] = []
   233   | map12 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s)
   234       (x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) =
   235     f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ::
   236       map12 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s
   237   | map12 _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   238 
   239 fun fold_map2 _ [] [] acc = ([], acc)
   240   | fold_map2 f (x1::x1s) (x2::x2s) acc =
   241     let
   242       val (x, acc') = f x1 x2 acc;
   243       val (xs, acc'') = fold_map2 f x1s x2s acc';
   244     in (x :: xs, acc'') end
   245   | fold_map2 _ _ _ _ = raise ListPair.UnequalLengths;
   246 
   247 fun fold_map3 _ [] [] [] acc = ([], acc)
   248   | fold_map3 f (x1::x1s) (x2::x2s) (x3::x3s) acc =
   249     let
   250       val (x, acc') = f x1 x2 x3 acc;
   251       val (xs, acc'') = fold_map3 f x1s x2s x3s acc';
   252     in (x :: xs, acc'') end
   253   | fold_map3 _ _ _ _ _ = raise ListPair.UnequalLengths;
   254 
   255 fun fold_map4 _ [] [] [] [] acc = ([], acc)
   256   | fold_map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) acc =
   257     let
   258       val (x, acc') = f x1 x2 x3 x4 acc;
   259       val (xs, acc'') = fold_map4 f x1s x2s x3s x4s acc';
   260     in (x :: xs, acc'') end
   261   | fold_map4 _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   262 
   263 fun fold_map5 _ [] [] [] [] [] acc = ([], acc)
   264   | fold_map5 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) acc =
   265     let
   266       val (x, acc') = f x1 x2 x3 x4 x5 acc;
   267       val (xs, acc'') = fold_map5 f x1s x2s x3s x4s x5s acc';
   268     in (x :: xs, acc'') end
   269   | fold_map5 _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   270 
   271 fun fold_map6 _ [] [] [] [] [] [] acc = ([], acc)
   272   | fold_map6 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) acc =
   273     let
   274       val (x, acc') = f x1 x2 x3 x4 x5 x6 acc;
   275       val (xs, acc'') = fold_map6 f x1s x2s x3s x4s x5s x6s acc';
   276     in (x :: xs, acc'') end
   277   | fold_map6 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   278 
   279 fun fold_map7 _ [] [] [] [] [] [] [] acc = ([], acc)
   280   | fold_map7 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) acc =
   281     let
   282       val (x, acc') = f x1 x2 x3 x4 x5 x6 x7 acc;
   283       val (xs, acc'') = fold_map7 f x1s x2s x3s x4s x5s x6s x7s acc';
   284     in (x :: xs, acc'') end
   285   | fold_map7 _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   286 
   287 fun fold_map8 _ [] [] [] [] [] [] [] [] acc = ([], acc)
   288   | fold_map8 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
   289       acc =
   290     let
   291       val (x, acc') = f x1 x2 x3 x4 x5 x6 x7 x8 acc;
   292       val (xs, acc'') = fold_map8 f x1s x2s x3s x4s x5s x6s x7s x8s acc';
   293     in (x :: xs, acc'') end
   294   | fold_map8 _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   295 
   296 fun fold_map9 _ [] [] [] [] [] [] [] [] [] acc = ([], acc)
   297   | fold_map9 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
   298       (x9::x9s) acc =
   299     let
   300       val (x, acc') = f x1 x2 x3 x4 x5 x6 x7 x8 x9 acc;
   301       val (xs, acc'') = fold_map9 f x1s x2s x3s x4s x5s x6s x7s x8s x9s acc';
   302     in (x :: xs, acc'') end
   303   | fold_map9 _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   304 
   305 (*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*)
   306 fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
   307 fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);
   308 
   309 (* The standard binding stands for a name generated following the canonical convention (e.g.
   310    "is_Nil" from "Nil"). The smart binding is either the standard binding or no binding at all,
   311    depending on the context. *)
   312 val standard_binding = @{binding _};
   313 val equal_binding = @{binding "="};
   314 
   315 val parse_binding = Parse.binding || @{keyword "="} >> K equal_binding;
   316 val parse_binding_colon = parse_binding --| @{keyword ":"};
   317 val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty;
   318 
   319 (*TODO: is this really different from Typedef.add_typedef_global?*)
   320 fun typedef typ set opt_morphs tac lthy =
   321   let
   322     val ((name, info), (lthy, lthy_old)) =
   323       lthy
   324       |> Typedef.add_typedef typ set opt_morphs tac
   325       ||> `Local_Theory.restore;
   326     val phi = Proof_Context.export_morphism lthy_old lthy;
   327   in
   328     ((name, Typedef.transform_info phi info), lthy)
   329   end;
   330 
   331 (*Tactical WRAP surrounds a static given tactic (core) with two deterministic chains of tactics*)
   332 fun WRAP gen_before gen_after xs core_tac =
   333   fold_rev (fn x => fn tac => gen_before x THEN tac THEN gen_after x) xs core_tac;
   334 
   335 fun WRAP' gen_before gen_after xs core_tac =
   336   fold_rev (fn x => fn tac => gen_before x THEN' tac THEN' gen_after x) xs core_tac;
   337 
   338 fun CONJ_WRAP_GEN conj_tac gen_tac xs =
   339   let val (butlast, last) = split_last xs;
   340   in WRAP (fn thm => conj_tac THEN gen_tac thm) (K all_tac) butlast (gen_tac last) end;
   341 
   342 fun CONJ_WRAP_GEN' conj_tac gen_tac xs =
   343   let val (butlast, last) = split_last xs;
   344   in WRAP' (fn thm => conj_tac THEN' gen_tac thm) (K (K all_tac)) butlast (gen_tac last) end;
   345 
   346 (*not eta-converted because of monotype restriction*)
   347 fun CONJ_WRAP gen_tac = CONJ_WRAP_GEN (rtac conjI 1) gen_tac;
   348 fun CONJ_WRAP' gen_tac = CONJ_WRAP_GEN' (rtac conjI) gen_tac;
   349 
   350 
   351 
   352 (* Term construction *)
   353 
   354 (** Fresh variables **)
   355 
   356 fun nonzero_string_of_int 0 = ""
   357   | nonzero_string_of_int n = string_of_int n;
   358 
   359 val mk_TFrees' = apfst (map TFree) oo Variable.invent_types;
   360 
   361 fun mk_TFrees n = mk_TFrees' (replicate n HOLogic.typeS);
   362 val mk_TFreess = fold_map mk_TFrees;
   363 
   364 fun mk_names n x = if n = 1 then [x] else map (fn i => x ^ string_of_int i) (1 upto n);
   365 
   366 fun mk_fresh_names ctxt = (fn xs => Variable.variant_fixes xs ctxt) oo mk_names;
   367 fun mk_Frees x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => map2 (curry Free) xs Ts);
   368 fun mk_Freess x Tss = fold_map2 mk_Frees (mk_names (length Tss) x) Tss;
   369 fun mk_Freesss x Tsss = fold_map2 mk_Freess (mk_names (length Tsss) x) Tsss;
   370 fun mk_Freessss x Tssss = fold_map2 mk_Freesss (mk_names (length Tssss) x) Tssss;
   371 fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => `(map Free) (xs ~~ Ts));
   372 fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list;
   373 
   374 fun retype_free T (Free (s, _)) = Free (s, T);
   375 
   376 
   377 (** Types **)
   378 
   379 fun strip_typeN 0 T = ([], T)
   380   | strip_typeN n (Type (@{type_name fun}, [T, T'])) = strip_typeN (n - 1) T' |>> cons T
   381   | strip_typeN _ T = raise TYPE ("strip_typeN", [T], []);
   382 
   383 fun mk_predT Ts = Ts ---> HOLogic.boolT;
   384 fun mk_pred1T T = mk_predT [T];
   385 fun mk_pred2T T U = mk_predT [T, U];
   386 fun mk_optionT T = Type (@{type_name option}, [T]);
   387 val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT;
   388 val dest_relT = HOLogic.dest_prodT o HOLogic.dest_setT;
   389 fun mk_sumT (LT, RT) = Type (@{type_name Sum_Type.sum}, [LT, RT]);
   390 fun mk_partial_funT (ranT, domT) = domT --> mk_optionT ranT;
   391 
   392 
   393 (** Constants **)
   394 
   395 fun fst_const T = Const (@{const_name fst}, T --> fst (HOLogic.dest_prodT T));
   396 fun snd_const T = Const (@{const_name snd}, T --> snd (HOLogic.dest_prodT T));
   397 fun Id_const T = Const (@{const_name Id}, mk_relT (T, T));
   398 
   399 
   400 (** Operators **)
   401 
   402 val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
   403 
   404 fun mk_IfN _ _ [t] = t
   405   | mk_IfN T (c :: cs) (t :: ts) =
   406     Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ c $ t $ mk_IfN T cs ts;
   407 
   408 fun mk_converse R =
   409   let
   410     val RT = dest_relT (fastype_of R);
   411     val RST = mk_relT (snd RT, fst RT);
   412   in Const (@{const_name converse}, fastype_of R --> RST) $ R end;
   413 
   414 fun mk_rel_comp (R, S) =
   415   let
   416     val RT = fastype_of R;
   417     val ST = fastype_of S;
   418     val RST = mk_relT (fst (dest_relT RT), snd (dest_relT ST));
   419   in Const (@{const_name relcomp}, RT --> ST --> RST) $ R $ S end;
   420 
   421 fun mk_Gr A f =
   422   let val ((AT, BT), FT) = `dest_funT (fastype_of f);
   423   in Const (@{const_name Gr}, HOLogic.mk_setT AT --> FT --> mk_relT (AT, BT)) $ A $ f end;
   424 
   425 fun mk_image f =
   426   let val (T, U) = dest_funT (fastype_of f);
   427   in Const (@{const_name image},
   428     (T --> U) --> (HOLogic.mk_setT T) --> (HOLogic.mk_setT U)) $ f end;
   429 
   430 fun mk_Ball X f =
   431   Const (@{const_name Ball}, fastype_of X --> fastype_of f --> HOLogic.boolT) $ X $ f;
   432 
   433 fun mk_Bex X f =
   434   Const (@{const_name Bex}, fastype_of X --> fastype_of f --> HOLogic.boolT) $ X $ f;
   435 
   436 fun mk_UNION X f =
   437   let val (T, U) = dest_funT (fastype_of f);
   438   in Const (@{const_name SUPR}, fastype_of X --> (T --> U) --> U) $ X $ f end;
   439 
   440 fun mk_Union T =
   441   Const (@{const_name Sup}, HOLogic.mk_setT (HOLogic.mk_setT T) --> HOLogic.mk_setT T);
   442 
   443 fun mk_Field r =
   444   let val T = fst (dest_relT (fastype_of r));
   445   in Const (@{const_name Field}, mk_relT (T, T) --> HOLogic.mk_setT T) $ r end;
   446 
   447 fun mk_card_order bd =
   448   let
   449     val T = fastype_of bd;
   450     val AT = fst (dest_relT T);
   451   in
   452     Const (@{const_name card_order_on}, HOLogic.mk_setT AT --> T --> HOLogic.boolT) $
   453       (HOLogic.mk_UNIV AT) $ bd
   454   end;
   455 
   456 fun mk_Card_order bd =
   457   let
   458     val T = fastype_of bd;
   459     val AT = fst (dest_relT T);
   460   in
   461     Const (@{const_name card_order_on}, HOLogic.mk_setT AT --> T --> HOLogic.boolT) $
   462       mk_Field bd $ bd
   463   end;
   464 
   465 fun mk_cinfinite bd =
   466   Const (@{const_name cinfinite}, fastype_of bd --> HOLogic.boolT) $ bd;
   467 
   468 fun mk_ordLeq t1 t2 =
   469   HOLogic.mk_mem (HOLogic.mk_prod (t1, t2),
   470     Const (@{const_name ordLeq}, mk_relT (fastype_of t1, fastype_of t2)));
   471 
   472 fun mk_card_of A =
   473   let
   474     val AT = fastype_of A;
   475     val T = HOLogic.dest_setT AT;
   476   in
   477     Const (@{const_name card_of}, AT --> mk_relT (T, T)) $ A
   478   end;
   479 
   480 fun mk_dir_image r f =
   481   let val (T, U) = dest_funT (fastype_of f);
   482   in Const (@{const_name dir_image}, mk_relT (T, T) --> (T --> U) --> mk_relT (U, U)) $ r $ f end;
   483 
   484 (*FIXME: "x"?*)
   485 (*(nth sets i) must be of type "T --> 'ai set"*)
   486 fun mk_in As sets T =
   487   let
   488     fun in_single set A =
   489       let val AT = fastype_of A;
   490       in Const (@{const_name less_eq},
   491         AT --> AT --> HOLogic.boolT) $ (set $ Free ("x", T)) $ A end;
   492   in
   493     if length sets > 0
   494     then HOLogic.mk_Collect ("x", T, foldr1 (HOLogic.mk_conj) (map2 in_single sets As))
   495     else HOLogic.mk_UNIV T
   496   end;
   497 
   498 fun mk_wpull A B1 B2 f1 f2 pseudo p1 p2 =
   499   let
   500     val AT = fastype_of A;
   501     val BT1 = fastype_of B1;
   502     val BT2 = fastype_of B2;
   503     val FT1 = fastype_of f1;
   504     val FT2 = fastype_of f2;
   505     val PT1 = fastype_of p1;
   506     val PT2 = fastype_of p2;
   507     val T1 = HOLogic.dest_setT BT1;
   508     val T2 = HOLogic.dest_setT BT2;
   509     val domP = domain_type PT1;
   510     val ranF = range_type FT1;
   511     val _ = if is_some pseudo orelse
   512                (HOLogic.dest_setT AT = domP andalso
   513                domain_type FT1 = T1 andalso
   514                domain_type FT2 = T2 andalso
   515                domain_type PT2 = domP andalso
   516                range_type PT1 = T1 andalso
   517                range_type PT2 = T2 andalso
   518                range_type FT2 = ranF)
   519       then () else raise TYPE ("mk_wpull", [BT1, BT2, FT1, FT2, PT1, PT2], []);
   520   in
   521     (case pseudo of
   522       NONE => Const (@{const_name wpull},
   523         AT --> BT1 --> BT2 --> FT1 --> FT2 --> PT1 --> PT2 --> HOLogic.boolT) $
   524         A $ B1 $ B2 $ f1 $ f2 $ p1 $ p2
   525     | SOME (e1, e2) => Const (@{const_name wppull},
   526         AT --> BT1 --> BT2 --> FT1 --> FT2 --> fastype_of e1 --> fastype_of e2 -->
   527           PT1 --> PT2 --> HOLogic.boolT) $
   528         A $ B1 $ B2 $ f1 $ f2 $ e1 $ e2 $ p1 $ p2)
   529   end;
   530 
   531 fun mk_subset t1 t2 =
   532   Const (@{const_name less_eq}, (fastype_of t1) --> (fastype_of t2) --> HOLogic.boolT) $ t1 $ t2;
   533 
   534 fun mk_card_binop binop typop t1 t2 =
   535   let
   536     val (T1, relT1) = `(fst o dest_relT) (fastype_of t1);
   537     val (T2, relT2) = `(fst o dest_relT) (fastype_of t2);
   538   in
   539     Const (binop, relT1 --> relT2 --> mk_relT (typop (T1, T2), typop (T1, T2))) $ t1 $ t2
   540   end;
   541 
   542 val mk_csum = mk_card_binop @{const_name csum} mk_sumT;
   543 val mk_cprod = mk_card_binop @{const_name cprod} HOLogic.mk_prodT;
   544 val mk_cexp = mk_card_binop @{const_name cexp} mk_partial_funT;
   545 val mk_ccexp = mk_card_binop @{const_name ccexp} mk_partial_funT;
   546 val ctwo = @{term ctwo};
   547 
   548 fun mk_collect xs defT =
   549   let val T = (case xs of [] => defT | (x::_) => fastype_of x);
   550   in Const (@{const_name collect}, HOLogic.mk_setT T --> T) $ (HOLogic.mk_set T xs) end;
   551 
   552 fun mk_permute src dest xs = map (nth xs o (fn x => find_index ((curry op =) x) src)) dest;
   553 
   554 fun rapp u t = betapply (t, u);
   555 
   556 val list_all_free =
   557   fold_rev (fn free => fn P =>
   558     let val (x, T) = Term.dest_Free free;
   559     in HOLogic.all_const T $ Term.absfree (x, T) P end);
   560 
   561 val list_exists_free =
   562   fold_rev (fn free => fn P =>
   563     let val (x, T) = Term.dest_Free free;
   564     in HOLogic.exists_const T $ Term.absfree (x, T) P end);
   565 
   566 fun find_indices xs ys = map_filter I
   567   (map_index (fn (i, y) => if member (op =) xs y then SOME i else NONE) ys);
   568 
   569 fun mk_trans thm1 thm2 = trans OF [thm1, thm2];
   570 fun mk_sym thm = sym OF [thm];
   571 
   572 (*TODO: antiquote heavily used theorems once*)
   573 val Pair_eqD = @{thm iffD1[OF Pair_eq]};
   574 val Pair_eqI = @{thm iffD2[OF Pair_eq]};
   575 val ctrans = @{thm ordLeq_transitive};
   576 val id_apply = @{thm id_apply};
   577 val meta_mp = @{thm meta_mp};
   578 val meta_spec = @{thm meta_spec};
   579 val o_apply = @{thm o_apply};
   580 val set_mp = @{thm set_mp};
   581 val set_rev_mp = @{thm set_rev_mp};
   582 val subset_UNIV = @{thm subset_UNIV};
   583 
   584 fun mk_nthN 1 t 1 = t
   585   | mk_nthN _ t 1 = HOLogic.mk_fst t
   586   | mk_nthN 2 t 2 = HOLogic.mk_snd t
   587   | mk_nthN n t m = mk_nthN (n - 1) (HOLogic.mk_snd t) (m - 1);
   588 
   589 fun mk_nth_conv n m =
   590   let
   591     fun thm b = if b then @{thm fst_snd} else @{thm snd_snd}
   592     fun mk_nth_conv _ 1 1 = refl
   593       | mk_nth_conv _ _ 1 = @{thm fst_conv}
   594       | mk_nth_conv _ 2 2 = @{thm snd_conv}
   595       | mk_nth_conv b _ 2 = @{thm snd_conv} RS thm b
   596       | mk_nth_conv b n m = mk_nth_conv false (n - 1) (m - 1) RS thm b;
   597   in mk_nth_conv (not (m = n)) n m end;
   598 
   599 fun mk_nthI 1 1 = @{thm TrueE[OF TrueI]}
   600   | mk_nthI n m = fold (curry op RS) (replicate (m - 1) @{thm sndI})
   601     (if m = n then @{thm TrueE[OF TrueI]} else @{thm fstI});
   602 
   603 fun mk_conjunctN 1 1 = @{thm TrueE[OF TrueI]}
   604   | mk_conjunctN _ 1 = conjunct1
   605   | mk_conjunctN 2 2 = conjunct2
   606   | mk_conjunctN n m = conjunct2 RS (mk_conjunctN (n - 1) (m - 1));
   607 
   608 fun conj_dests n thm = map (fn k => thm RS mk_conjunctN n k) (1 upto n);
   609 
   610 fun mk_conjIN 1 = @{thm TrueE[OF TrueI]}
   611   | mk_conjIN n = mk_conjIN (n - 1) RSN (2, conjI);
   612 
   613 fun mk_disjIN 1 1 = @{thm TrueE[OF TrueI]}
   614   | mk_disjIN _ 1 = disjI1
   615   | mk_disjIN 2 2 = disjI2
   616   | mk_disjIN n m = (mk_disjIN (n - 1) (m - 1)) RS disjI2;
   617 
   618 fun mk_ordLeq_csum 1 1 thm = thm
   619   | mk_ordLeq_csum _ 1 thm = @{thm ordLeq_transitive} OF [thm, @{thm ordLeq_csum1}]
   620   | mk_ordLeq_csum 2 2 thm = @{thm ordLeq_transitive} OF [thm, @{thm ordLeq_csum2}]
   621   | mk_ordLeq_csum n m thm = @{thm ordLeq_transitive} OF
   622     [mk_ordLeq_csum (n - 1) (m - 1) thm, @{thm ordLeq_csum2[OF Card_order_csum]}];
   623 
   624 local
   625   fun mk_Un_upper' 0 = subset_refl
   626     | mk_Un_upper' 1 = @{thm Un_upper1}
   627     | mk_Un_upper' k = Library.foldr (op RS o swap)
   628       (replicate (k - 1) @{thm subset_trans[OF Un_upper1]}, @{thm Un_upper1});
   629 in
   630   fun mk_Un_upper 1 1 = subset_refl
   631     | mk_Un_upper n 1 = mk_Un_upper' (n - 2) RS @{thm subset_trans[OF Un_upper1]}
   632     | mk_Un_upper n m = mk_Un_upper' (n - m) RS @{thm subset_trans[OF Un_upper2]};
   633 end;
   634 
   635 local
   636   fun mk_UnIN' 0 = @{thm UnI2}
   637     | mk_UnIN' m = mk_UnIN' (m - 1) RS @{thm UnI1};
   638 in
   639   fun mk_UnIN 1 1 = @{thm TrueE[OF TrueI]}
   640     | mk_UnIN n 1 = Library.foldr1 (op RS o swap) (replicate (n - 1) @{thm UnI1})
   641     | mk_UnIN n m = mk_UnIN' (n - m)
   642 end;
   643 
   644 fun splice xs ys = flat (map2 (fn x => fn y => [x, y]) xs ys);
   645 
   646 fun transpose [] = []
   647   | transpose ([] :: xss) = transpose xss
   648   | transpose xss = map hd xss :: transpose (map tl xss);
   649 
   650 fun unsort eq ys zs = map (fn x => nth zs (find_index (curry eq x) ys));
   651 
   652 fun seq_conds f n k xs =
   653   if k = n then
   654     map (f false) (take (k - 1) xs)
   655   else
   656     let val (negs, pos) = split_last (take k xs) in
   657       map (f false) negs @ [f true pos]
   658     end;
   659 
   660 fun pad_list x n xs = xs @ replicate (n - length xs) x;
   661 
   662 fun mk_unabs_def n = funpow n (fn thm => thm RS fun_cong);
   663 
   664 fun is_triv_implies thm =
   665   op aconv (Logic.dest_implies (Thm.prop_of thm))
   666   handle TERM _ => false;
   667 
   668 fun is_refl_prop t =
   669   op aconv (HOLogic.dest_eq (HOLogic.dest_Trueprop t))
   670   handle TERM _ => false;
   671 
   672 val is_refl = is_refl_prop o Thm.prop_of;
   673 val is_concl_refl = is_refl_prop o Logic.strip_imp_concl o Thm.prop_of;
   674 
   675 val no_refl = filter_out is_refl;
   676 val no_reflexive = filter_out Thm.is_reflexive;
   677 
   678 fun cterm_instantiate_pos cts thm =
   679   let
   680     val cert = Thm.cterm_of (Thm.theory_of_thm thm);
   681     val vars = Term.add_vars (prop_of thm) [];
   682     val vars' = rev (drop (length vars - length cts) vars);
   683     val ps = map_filter (fn (_, NONE) => NONE
   684       | (var, SOME ct) => SOME (cert (Var var), ct)) (vars' ~~ cts);
   685   in
   686     Drule.cterm_instantiate ps thm
   687   end;
   688 
   689 fun fold_thms ctxt thms = Local_Defs.fold ctxt (distinct Thm.eq_thm_prop thms);
   690 fun unfold_thms ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms);
   691 
   692 end;