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