src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
author blanchet
Fri Feb 14 15:03:24 2014 +0100 (2014-02-14)
changeset 55480 59cc4a8bc28a
parent 55471 198498f861ee
child 55535 10194808430d
permissions -rw-r--r--
allow different functions to recurse on the same type, like in the old package
blanchet@54701
     1
(*  Title:      HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
blanchet@54397
     2
    Author:     Dmitriy Traytel, TU Muenchen
blanchet@54008
     3
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@54397
     4
    Copyright   2012, 2013
blanchet@54008
     5
blanchet@54008
     6
Library for wrapping existing freely generated type's constructors.
blanchet@54008
     7
*)
blanchet@54008
     8
blanchet@54008
     9
signature CTR_SUGAR_UTIL =
blanchet@54008
    10
sig
blanchet@54008
    11
  val map3: ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
blanchet@54008
    12
  val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
blanchet@54008
    13
  val map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f) ->
blanchet@54008
    14
    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list
blanchet@54008
    15
  val fold_map2: ('a -> 'b -> 'c -> 'd * 'c) -> 'a list -> 'b list -> 'c -> 'd list * 'c
blanchet@54008
    16
  val fold_map3: ('a -> 'b -> 'c -> 'd -> 'e * 'd) ->
blanchet@54008
    17
    'a list -> 'b list -> 'c list -> 'd -> 'e list * 'd
blanchet@54008
    18
  val seq_conds: (bool -> 'a -> 'b) -> int -> int -> 'a list -> 'b list
blanchet@54008
    19
  val transpose: 'a list list -> 'a list list
blanchet@54008
    20
  val pad_list: 'a -> int -> 'a list -> 'a list
blanchet@54008
    21
  val splice: 'a list -> 'a list -> 'a list
blanchet@55480
    22
  val permute_like_unique: ('a * 'b -> bool) -> 'a list -> 'b list -> 'c list -> 'c list
blanchet@55480
    23
  val permute_like: ('a * 'a -> bool) -> 'a list -> 'a list -> 'b list -> 'b list
blanchet@54008
    24
blanchet@54008
    25
  val mk_names: int -> string -> string list
blanchet@54008
    26
  val mk_fresh_names: Proof.context -> int -> string -> string list * Proof.context
blanchet@54008
    27
  val mk_TFrees': sort list -> Proof.context -> typ list * Proof.context
blanchet@54008
    28
  val mk_TFrees: int -> Proof.context -> typ list * Proof.context
blanchet@54008
    29
  val mk_Frees': string -> typ list -> Proof.context ->
blanchet@54008
    30
    (term list * (string * typ) list) * Proof.context
blanchet@54008
    31
  val mk_Freess': string -> typ list list -> Proof.context ->
blanchet@54008
    32
    (term list list * (string * typ) list list) * Proof.context
blanchet@54008
    33
  val mk_Frees: string -> typ list -> Proof.context -> term list * Proof.context
blanchet@54008
    34
  val mk_Freess: string -> typ list list -> Proof.context -> term list list * Proof.context
blanchet@54008
    35
  val resort_tfree: sort -> typ -> typ
blanchet@54008
    36
  val variant_types: string list -> sort list -> Proof.context ->
blanchet@54008
    37
    (string * sort) list * Proof.context
blanchet@54008
    38
  val variant_tfrees: string list -> Proof.context -> typ list * Proof.context
blanchet@54008
    39
blanchet@54435
    40
  val typ_subst_nonatomic: (typ * typ) list -> typ -> typ
blanchet@54435
    41
  val subst_nonatomic_types: (typ * typ) list -> term -> term
blanchet@54435
    42
blanchet@55471
    43
  val lhs_heads_of : thm -> term list
blanchet@55471
    44
blanchet@54008
    45
  val mk_predT: typ list -> typ
blanchet@54008
    46
  val mk_pred1T: typ -> typ
blanchet@54008
    47
blanchet@54008
    48
  val mk_disjIN: int -> int -> thm
blanchet@54008
    49
blanchet@54008
    50
  val mk_unabs_def: int -> thm -> thm
blanchet@54008
    51
blanchet@54008
    52
  val mk_IfN: typ -> term list -> term list -> term
blanchet@54008
    53
  val mk_Trueprop_eq: term * term -> term
blanchet@54008
    54
blanchet@54008
    55
  val rapp: term -> term -> term
blanchet@54008
    56
blanchet@54008
    57
  val list_all_free: term list -> term -> term
blanchet@54008
    58
  val list_exists_free: term list -> term -> term
blanchet@54008
    59
blanchet@54008
    60
  val fo_match: Proof.context -> term -> term -> Type.tyenv * Envir.tenv
blanchet@54008
    61
blanchet@54540
    62
  val cterm_instantiate_pos: cterm option list -> thm -> thm
blanchet@54008
    63
  val unfold_thms: Proof.context -> thm list -> thm -> thm
blanchet@54008
    64
blanchet@54008
    65
  val certifyT: Proof.context -> typ -> ctyp
blanchet@54008
    66
  val certify: Proof.context -> term -> cterm
blanchet@54008
    67
blanchet@54008
    68
  val standard_binding: binding
blanchet@54008
    69
  val equal_binding: binding
blanchet@54008
    70
  val parse_binding: binding parser
blanchet@55469
    71
  val parse_binding_colon: binding parser
blanchet@55469
    72
  val parse_opt_binding_colon: binding parser
blanchet@54008
    73
blanchet@54008
    74
  val ss_only: thm list -> Proof.context -> Proof.context
blanchet@54540
    75
blanchet@54540
    76
  val WRAP: ('a -> tactic) -> ('a -> tactic) -> 'a list -> tactic -> tactic
blanchet@54540
    77
  val WRAP': ('a -> int -> tactic) -> ('a -> int -> tactic) -> 'a list -> (int -> tactic) -> int ->
blanchet@54540
    78
    tactic
blanchet@54540
    79
  val CONJ_WRAP_GEN: tactic -> ('a -> tactic) -> 'a list -> tactic
blanchet@54540
    80
  val CONJ_WRAP_GEN': (int -> tactic) -> ('a -> int -> tactic) -> 'a list -> int -> tactic
blanchet@54540
    81
  val CONJ_WRAP: ('a -> tactic) -> 'a list -> tactic
blanchet@54540
    82
  val CONJ_WRAP': ('a -> int -> tactic) -> 'a list -> int -> tactic
blanchet@54008
    83
end;
blanchet@54008
    84
blanchet@54008
    85
structure Ctr_Sugar_Util : CTR_SUGAR_UTIL =
blanchet@54008
    86
struct
blanchet@54008
    87
blanchet@54008
    88
fun map3 _ [] [] [] = []
blanchet@54008
    89
  | map3 f (x1::x1s) (x2::x2s) (x3::x3s) = f x1 x2 x3 :: map3 f x1s x2s x3s
blanchet@54008
    90
  | map3 _ _ _ _ = raise ListPair.UnequalLengths;
blanchet@54008
    91
blanchet@54008
    92
fun map4 _ [] [] [] [] = []
blanchet@54008
    93
  | map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) = f x1 x2 x3 x4 :: map4 f x1s x2s x3s x4s
blanchet@54008
    94
  | map4 _ _ _ _ _ = raise ListPair.UnequalLengths;
blanchet@54008
    95
blanchet@54008
    96
fun map5 _ [] [] [] [] [] = []
blanchet@54008
    97
  | map5 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) =
blanchet@54008
    98
    f x1 x2 x3 x4 x5 :: map5 f x1s x2s x3s x4s x5s
blanchet@54008
    99
  | map5 _ _ _ _ _ _ = raise ListPair.UnequalLengths;
blanchet@54008
   100
blanchet@54008
   101
fun fold_map2 _ [] [] acc = ([], acc)
blanchet@54008
   102
  | fold_map2 f (x1::x1s) (x2::x2s) acc =
blanchet@54008
   103
    let
blanchet@54008
   104
      val (x, acc') = f x1 x2 acc;
blanchet@54008
   105
      val (xs, acc'') = fold_map2 f x1s x2s acc';
blanchet@54008
   106
    in (x :: xs, acc'') end
blanchet@54008
   107
  | fold_map2 _ _ _ _ = raise ListPair.UnequalLengths;
blanchet@54008
   108
blanchet@54008
   109
fun fold_map3 _ [] [] [] acc = ([], acc)
blanchet@54008
   110
  | fold_map3 f (x1::x1s) (x2::x2s) (x3::x3s) acc =
blanchet@54008
   111
    let
blanchet@54008
   112
      val (x, acc') = f x1 x2 x3 acc;
blanchet@54008
   113
      val (xs, acc'') = fold_map3 f x1s x2s x3s acc';
blanchet@54008
   114
    in (x :: xs, acc'') end
blanchet@54008
   115
  | fold_map3 _ _ _ _ _ = raise ListPair.UnequalLengths;
blanchet@54008
   116
blanchet@54008
   117
fun seq_conds f n k xs =
blanchet@54008
   118
  if k = n then
blanchet@54008
   119
    map (f false) (take (k - 1) xs)
blanchet@54008
   120
  else
blanchet@54008
   121
    let val (negs, pos) = split_last (take k xs) in
blanchet@54008
   122
      map (f false) negs @ [f true pos]
blanchet@54008
   123
    end;
blanchet@54008
   124
blanchet@54008
   125
fun transpose [] = []
blanchet@54008
   126
  | transpose ([] :: xss) = transpose xss
blanchet@54008
   127
  | transpose xss = map hd xss :: transpose (map tl xss);
blanchet@54008
   128
blanchet@54008
   129
fun pad_list x n xs = xs @ replicate (n - length xs) x;
blanchet@54008
   130
blanchet@54008
   131
fun splice xs ys = flat (map2 (fn x => fn y => [x, y]) xs ys);
blanchet@54008
   132
blanchet@55480
   133
fun permute_like_unique eq xs xs' ys =
blanchet@55480
   134
  map (nth ys o (fn y => find_index (fn x => eq (x, y)) xs)) xs';
blanchet@55480
   135
blanchet@55480
   136
fun fresh eq x names =
blanchet@55480
   137
  (case AList.lookup eq names x of
blanchet@55480
   138
    NONE => ((x, 0), (x, 0) :: names)
blanchet@55480
   139
  | SOME n => ((x, n + 1), AList.update eq (x, n + 1) names));
blanchet@55480
   140
blanchet@55480
   141
fun deambiguate eq xs = fst (fold_map (fresh eq) xs []);
blanchet@55480
   142
blanchet@55480
   143
fun permute_like eq xs xs' =
blanchet@55480
   144
  permute_like_unique (eq_pair eq (op =)) (deambiguate eq xs) (deambiguate eq xs');
blanchet@54008
   145
blanchet@54008
   146
fun mk_names n x = if n = 1 then [x] else map (fn i => x ^ string_of_int i) (1 upto n);
blanchet@54008
   147
fun mk_fresh_names ctxt = (fn xs => Variable.variant_fixes xs ctxt) oo mk_names;
blanchet@54008
   148
blanchet@54008
   149
val mk_TFrees' = apfst (map TFree) oo Variable.invent_types;
blanchet@54008
   150
blanchet@54008
   151
fun mk_TFrees n = mk_TFrees' (replicate n HOLogic.typeS);
blanchet@54008
   152
blanchet@54008
   153
fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => `(map Free) (xs ~~ Ts));
blanchet@54008
   154
fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list;
blanchet@54008
   155
blanchet@54008
   156
fun mk_Frees x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => map2 (curry Free) xs Ts);
blanchet@54008
   157
fun mk_Freess x Tss = fold_map2 mk_Frees (mk_names (length Tss) x) Tss;
blanchet@54008
   158
blanchet@54008
   159
fun resort_tfree S (TFree (s, _)) = TFree (s, S);
blanchet@54008
   160
blanchet@54008
   161
fun ensure_prefix pre s = s |> not (String.isPrefix pre s) ? prefix pre;
blanchet@54008
   162
blanchet@54008
   163
fun variant_types ss Ss ctxt =
blanchet@54008
   164
  let
blanchet@54008
   165
    val (tfrees, _) =
blanchet@54008
   166
      fold_map2 (fn s => fn S => Name.variant s #> apfst (rpair S)) ss Ss (Variable.names_of ctxt);
blanchet@54008
   167
    val ctxt' = fold (Variable.declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
blanchet@54008
   168
  in (tfrees, ctxt') end;
blanchet@54008
   169
blanchet@54008
   170
fun variant_tfrees ss =
blanchet@54008
   171
  apfst (map TFree) o
blanchet@54008
   172
    variant_types (map (ensure_prefix "'") ss) (replicate (length ss) HOLogic.typeS);
blanchet@54008
   173
blanchet@54435
   174
(*Replace each Ti by Ui (starting from the leaves); inst = [(T1, U1), ..., (Tn, Un)].*)
blanchet@54435
   175
fun typ_subst_nonatomic [] = I
blanchet@54435
   176
  | typ_subst_nonatomic inst =
blanchet@54435
   177
    let
blanchet@54435
   178
      fun subst (Type (s, Ts)) = perhaps (AList.lookup (op =) inst) (Type (s, map subst Ts))
blanchet@54435
   179
        | subst T = perhaps (AList.lookup (op =) inst) T;
blanchet@54435
   180
    in subst end;
blanchet@54435
   181
blanchet@54435
   182
fun subst_nonatomic_types [] = I
blanchet@54435
   183
  | subst_nonatomic_types inst = map_types (typ_subst_nonatomic inst);
blanchet@54435
   184
blanchet@55471
   185
fun lhs_heads_of thm =
blanchet@55471
   186
  [Term.head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))))];
blanchet@55471
   187
blanchet@54008
   188
fun mk_predT Ts = Ts ---> HOLogic.boolT;
blanchet@54008
   189
fun mk_pred1T T = mk_predT [T];
blanchet@54008
   190
blanchet@54008
   191
fun mk_disjIN 1 1 = @{thm TrueE[OF TrueI]}
blanchet@54008
   192
  | mk_disjIN _ 1 = disjI1
blanchet@54008
   193
  | mk_disjIN 2 2 = disjI2
blanchet@54008
   194
  | mk_disjIN n m = (mk_disjIN (n - 1) (m - 1)) RS disjI2;
blanchet@54008
   195
blanchet@54008
   196
fun mk_unabs_def n = funpow n (fn thm => thm RS fun_cong);
blanchet@54008
   197
blanchet@54008
   198
fun mk_IfN _ _ [t] = t
blanchet@54008
   199
  | mk_IfN T (c :: cs) (t :: ts) =
blanchet@54008
   200
    Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ c $ t $ mk_IfN T cs ts;
blanchet@54008
   201
blanchet@54008
   202
val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
blanchet@54008
   203
blanchet@54008
   204
fun rapp u t = betapply (t, u);
blanchet@54008
   205
blanchet@54008
   206
fun list_quant_free quant_const =
blanchet@54491
   207
  fold_rev (fn Free (xT as (_, T)) => fn P => quant_const T $ Term.absfree xT P);
blanchet@54008
   208
blanchet@54008
   209
val list_all_free = list_quant_free HOLogic.all_const;
blanchet@54008
   210
val list_exists_free = list_quant_free HOLogic.exists_const;
blanchet@54008
   211
blanchet@54008
   212
fun fo_match ctxt t pat =
blanchet@54008
   213
  let val thy = Proof_Context.theory_of ctxt in
blanchet@54008
   214
    Pattern.first_order_match thy (pat, t) (Vartab.empty, Vartab.empty)
blanchet@54008
   215
  end;
blanchet@54008
   216
blanchet@54540
   217
fun cterm_instantiate_pos cts thm =
blanchet@54540
   218
  let
blanchet@54540
   219
    val cert = Thm.cterm_of (Thm.theory_of_thm thm);
blanchet@54540
   220
    val vars = Term.add_vars (prop_of thm) [];
blanchet@54540
   221
    val vars' = rev (drop (length vars - length cts) vars);
blanchet@54540
   222
    val ps = map_filter (fn (_, NONE) => NONE
blanchet@54540
   223
      | (var, SOME ct) => SOME (cert (Var var), ct)) (vars' ~~ cts);
blanchet@54540
   224
  in
blanchet@54540
   225
    Drule.cterm_instantiate ps thm
blanchet@54540
   226
  end;
blanchet@54540
   227
blanchet@54008
   228
fun unfold_thms ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms);
blanchet@54008
   229
blanchet@54008
   230
(*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*)
blanchet@54008
   231
fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);
blanchet@54008
   232
fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
blanchet@54008
   233
blanchet@54008
   234
(* The standard binding stands for a name generated following the canonical convention (e.g.,
blanchet@54008
   235
   "is_Nil" from "Nil"). In contrast, the empty binding is either the standard binding or no
blanchet@54008
   236
   binding at all, depending on the context. *)
blanchet@54008
   237
val standard_binding = @{binding _};
blanchet@54008
   238
val equal_binding = @{binding "="};
blanchet@54008
   239
blanchet@54008
   240
val parse_binding = Parse.binding || @{keyword "="} >> K equal_binding;
blanchet@55469
   241
val parse_binding_colon = parse_binding --| @{keyword ":"};
blanchet@55469
   242
val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty;
blanchet@54008
   243
blanchet@54008
   244
fun ss_only thms ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps thms;
blanchet@54008
   245
blanchet@54540
   246
(*Tactical WRAP surrounds a static given tactic (core) with two deterministic chains of tactics*)
blanchet@54540
   247
fun WRAP gen_before gen_after xs core_tac =
blanchet@54540
   248
  fold_rev (fn x => fn tac => gen_before x THEN tac THEN gen_after x) xs core_tac;
blanchet@54540
   249
blanchet@54540
   250
fun WRAP' gen_before gen_after xs core_tac =
blanchet@54540
   251
  fold_rev (fn x => fn tac => gen_before x THEN' tac THEN' gen_after x) xs core_tac;
blanchet@54540
   252
blanchet@54540
   253
fun CONJ_WRAP_GEN conj_tac gen_tac xs =
blanchet@54540
   254
  let val (butlast, last) = split_last xs;
blanchet@54540
   255
  in WRAP (fn thm => conj_tac THEN gen_tac thm) (K all_tac) butlast (gen_tac last) end;
blanchet@54540
   256
blanchet@54540
   257
fun CONJ_WRAP_GEN' conj_tac gen_tac xs =
blanchet@54540
   258
  let val (butlast, last) = split_last xs;
blanchet@54540
   259
  in WRAP' (fn thm => conj_tac THEN' gen_tac thm) (K (K all_tac)) butlast (gen_tac last) end;
blanchet@54540
   260
blanchet@54540
   261
(*not eta-converted because of monotype restriction*)
blanchet@54540
   262
fun CONJ_WRAP gen_tac = CONJ_WRAP_GEN (rtac conjI 1) gen_tac;
blanchet@54540
   263
fun CONJ_WRAP' gen_tac = CONJ_WRAP_GEN' (rtac conjI) gen_tac;
blanchet@54540
   264
blanchet@54008
   265
end;