src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML
author wenzelm
Fri Mar 06 15:58:56 2015 +0100 (2015-03-06)
changeset 59621 291934bac95e
parent 59586 ddf6deaadfe8
child 59639 f596ed647018
permissions -rw-r--r--
Thm.cterm_of and Thm.ctyp_of operate on local context;
sultana@55596
     1
(*  Title:      HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML
sultana@55596
     2
    Author:     Nik Sultana, Cambridge University Computer Laboratory
sultana@55596
     3
Collection of general functions used in the reconstruction module.
sultana@55596
     4
*)
sultana@55596
     5
sultana@55596
     6
signature TPTP_RECONSTRUCT_LIBRARY =
sultana@55596
     7
sig
sultana@55596
     8
  exception BREAK_LIST
sultana@55596
     9
  val break_list : 'a list -> 'a * 'a list
sultana@55596
    10
  val break_seq : 'a Seq.seq -> 'a * 'a Seq.seq
sultana@55596
    11
  exception MULTI_ELEMENT_LIST
sultana@55596
    12
  val cascaded_filter_single : bool -> ('a list -> 'a list) list -> 'a list -> 'a option
sultana@55596
    13
  val concat_between : 'a list list -> ('a option * 'a option) -> 'a list
sultana@55596
    14
  exception DIFF_TYPE of typ * typ
sultana@55596
    15
  exception DIFF of term * term
sultana@55596
    16
  val diff :
sultana@55596
    17
     theory ->
sultana@55596
    18
     term * term -> (term * term) list * (typ * typ) list
sultana@55596
    19
  exception DISPLACE_KV
sultana@55596
    20
  val displace_kv : ''a -> (''a * 'b) list -> (''a * 'b) list
sultana@55596
    21
  val enumerate : int -> 'a list -> (int * 'a) list
sultana@55596
    22
  val fold_options : 'a option list -> 'a list
sultana@55596
    23
  val find_and_remove : ('a -> bool) -> 'a list -> 'a * 'a list
sultana@55596
    24
  val lift_option : ('a -> 'b) -> 'a option -> 'b option
sultana@55596
    25
  val list_diff : ''a list -> ''a list -> ''a list
sultana@55596
    26
  val list_prod : 'a list list -> 'a list -> 'a list -> 'a list list
sultana@55596
    27
  val permute : ''a list -> ''a list list
sultana@55596
    28
  val prefix_intersection_list :
sultana@55596
    29
     ''a list -> ''a list -> ''a list
sultana@55596
    30
  val repeat_until_fixpoint : (''a -> ''a) -> ''a -> ''a
sultana@55596
    31
  val switch : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
sultana@55596
    32
  val zip_amap :
sultana@55596
    33
       'a list ->
sultana@55596
    34
       'b list ->
sultana@55596
    35
       ('a * 'b) list -> ('a * 'b) list * ('a list * 'b list)
sultana@55596
    36
sultana@55596
    37
  val consts_in : term -> term list
wenzelm@59533
    38
  val head_quantified_variable : Proof.context -> int -> thm -> (string * typ) option
sultana@55596
    39
  val push_allvar_in : string -> term -> term
sultana@55596
    40
  val strip_top_All_var : term -> (string * typ) * term
sultana@55596
    41
  val strip_top_All_vars : term -> (string * typ) list * term
sultana@55596
    42
  val strip_top_all_vars :
sultana@55596
    43
     (string * typ) list -> term -> (string * typ) list * term
wenzelm@59533
    44
  val trace_tac' : Proof.context -> string ->
sultana@55596
    45
     ('a -> thm -> 'b Seq.seq) -> 'a -> thm -> 'b Seq.seq
sultana@55596
    46
  val try_dest_Trueprop : term -> term
sultana@55596
    47
sultana@55596
    48
  val type_devar : ((indexname * sort) * typ) list -> term -> term
sultana@55596
    49
  val diff_and_instantiate : Proof.context -> thm -> term -> term -> thm
sultana@55596
    50
wenzelm@59533
    51
  val batter_tac : Proof.context -> int -> tactic
wenzelm@59533
    52
  val break_hypotheses_tac : Proof.context -> int -> tactic
wenzelm@59533
    53
  val clause_breaker_tac : Proof.context -> int -> tactic
sultana@55596
    54
  (* val dist_all_and_tac : Proof.context -> int -> tactic *)(*FIXME unused*)
sultana@55596
    55
  val reassociate_conjs_tac : Proof.context -> int -> tactic
sultana@55596
    56
sultana@55596
    57
  val ASAP : (int -> tactic) -> (int -> tactic) -> int -> tactic
sultana@55596
    58
  val COND' :
sultana@55596
    59
     ('a -> thm -> bool) ->
sultana@55596
    60
     ('a -> tactic) -> ('a -> tactic) -> 'a -> tactic
sultana@55596
    61
sultana@55596
    62
  val TERMFUN :
sultana@55596
    63
     (term list * term -> 'a) -> int option -> thm -> 'a list
sultana@55596
    64
  val TERMPRED :
sultana@55596
    65
     (term -> bool) ->
sultana@55596
    66
     (term -> bool) -> int option -> thm -> bool
sultana@55596
    67
sultana@55596
    68
  val guided_abstract :
sultana@55596
    69
     bool -> term -> term -> ((string * typ) * term) * term list
sultana@55596
    70
  val abstract :
sultana@55596
    71
     term list -> term -> ((string * typ) * term) list * term
sultana@55596
    72
end
sultana@55596
    73
sultana@55596
    74
structure TPTP_Reconstruct_Library : TPTP_RECONSTRUCT_LIBRARY =
sultana@55596
    75
struct
sultana@55596
    76
sultana@55596
    77
(*zip as much as possible*)
sultana@55596
    78
fun zip_amap [] ys acc = (acc, ([], ys))
sultana@55596
    79
  | zip_amap xs [] acc = (acc, (xs, []))
sultana@55596
    80
  | zip_amap (x :: xs) (y :: ys) acc =
sultana@55596
    81
      zip_amap xs ys ((x, y) :: acc);
sultana@55596
    82
sultana@55596
    83
(*Pair a list up with the position number of each element,
sultana@55596
    84
  starting from n*)
sultana@55596
    85
fun enumerate n ls =
sultana@55596
    86
  let
sultana@55596
    87
    fun enumerate' [] _ acc = acc
sultana@55596
    88
      | enumerate' (x :: xs) n acc = enumerate' xs (n + 1) ((n, x) :: acc)
sultana@55596
    89
  in
sultana@55596
    90
    enumerate' ls n []
sultana@55596
    91
    |> rev
sultana@55596
    92
  end
sultana@55596
    93
sultana@55596
    94
(*
sultana@55596
    95
enumerate 0 [];
sultana@55596
    96
enumerate 0 ["a", "b", "c"];
sultana@55596
    97
*)
sultana@55596
    98
sultana@55596
    99
(*List subtraction*)
sultana@55596
   100
fun list_diff l1 l2 =
wenzelm@58412
   101
  filter (fn x => forall (fn y => x <> y) l2) l1
sultana@55596
   102
sultana@55596
   103
val _ = @{assert}
sultana@55596
   104
  (list_diff [1,2,3] [2,4] = [1, 3])
sultana@55596
   105
sultana@55596
   106
(* [a,b] times_list [c,d] gives [[a,c,d], [b,c,d]] *)
sultana@55596
   107
fun list_prod acc [] _ = rev acc
sultana@55596
   108
  | list_prod acc (x :: xs) ys = list_prod ((x :: ys) :: acc) xs ys
sultana@55596
   109
sultana@55596
   110
fun repeat_until_fixpoint f x =
sultana@55596
   111
  let
sultana@55596
   112
    val x' = f x
sultana@55596
   113
  in
sultana@55596
   114
    if x = x' then x else repeat_until_fixpoint f x'
sultana@55596
   115
  end
sultana@55596
   116
sultana@55596
   117
(*compute all permutations of a list*)
sultana@55596
   118
fun permute l =
sultana@55596
   119
  let
sultana@55596
   120
    fun permute' (l, []) = [(l, [])]
sultana@55596
   121
      | permute' (l, xs) =
sultana@55596
   122
          map (fn x => (x :: l, filter (fn y => y <> x) xs)) xs
wenzelm@58411
   123
          |> maps permute'
sultana@55596
   124
  in
sultana@55596
   125
    permute' ([], l)
sultana@55596
   126
    |> map fst
sultana@55596
   127
  end
sultana@55596
   128
(*
sultana@55596
   129
permute [1,2,3];
sultana@55596
   130
permute ["A", "B"]
sultana@55596
   131
*)
sultana@55596
   132
sultana@55596
   133
(*this exception is raised when the pair we wish to displace
sultana@55596
   134
  isn't found in the association list*)
sultana@55596
   135
exception DISPLACE_KV;
sultana@55596
   136
(*move a key-value pair, determined by the k, to the beginning of
sultana@55596
   137
  an association list. it moves the first occurrence of a pair
sultana@55596
   138
  keyed by "k"*)
sultana@55596
   139
local
sultana@55596
   140
  fun fold_fun k (kv as (k', v)) (l, buff) =
sultana@55596
   141
    if is_some buff then (kv :: l, buff)
sultana@55596
   142
    else
sultana@55596
   143
      if k = k' then
sultana@55596
   144
        (l, SOME kv)
sultana@55596
   145
      else
sultana@55596
   146
        (kv :: l, buff)
sultana@55596
   147
in
sultana@55596
   148
  (*"k" is the key value of the pair we wish to displace*)
sultana@55596
   149
  fun displace_kv k alist =
sultana@55596
   150
    let
sultana@55596
   151
      val (pre_alist, kv) = fold (fold_fun k) alist ([], NONE)
sultana@55596
   152
    in
sultana@55596
   153
      if is_some kv then
sultana@55596
   154
        the kv :: rev pre_alist
sultana@55596
   155
      else raise DISPLACE_KV
sultana@55596
   156
    end
sultana@55596
   157
end
sultana@55596
   158
sultana@55596
   159
(*Given two lists, it generates a new list where
sultana@55596
   160
  the intersection of the lists forms the prefix
sultana@55596
   161
  of the new list.*)
sultana@55596
   162
local
sultana@55596
   163
  fun prefix_intersection_list' (acc_pre, acc_pro) l1 l2 =
sultana@55596
   164
    if null l1 then
sultana@55596
   165
      List.rev acc_pre @ List.rev acc_pro
sultana@55596
   166
    else if null l2 then
sultana@55596
   167
      List.rev acc_pre @ l1 @ List.rev acc_pro
sultana@55596
   168
    else
sultana@55596
   169
      let val l1_hd = hd l1
sultana@55596
   170
      in
sultana@55596
   171
        prefix_intersection_list'
sultana@55596
   172
         (if member (op =) l2 l1_hd then
sultana@55596
   173
            (l1_hd :: acc_pre, acc_pro)
sultana@55596
   174
          else
sultana@55596
   175
           (acc_pre, l1_hd :: acc_pro))
sultana@55596
   176
         (tl l1) l2
sultana@55596
   177
      end
sultana@55596
   178
in
sultana@55596
   179
  fun prefix_intersection_list l1 l2 = prefix_intersection_list' ([], []) l1 l2
sultana@55596
   180
end;
sultana@55596
   181
sultana@55596
   182
val _ = @{assert}
sultana@55596
   183
  (prefix_intersection_list [1,2,3,4,5] [1,3,5] = [1, 3, 5, 2, 4]);
sultana@55596
   184
sultana@55596
   185
val _ = @{assert}
sultana@55596
   186
  (prefix_intersection_list [1,2,3,4,5] [] = [1,2,3,4,5]);
sultana@55596
   187
sultana@55596
   188
val _ = @{assert}
sultana@55596
   189
  (prefix_intersection_list [] [1,3,5] = [])
sultana@55596
   190
sultana@55596
   191
fun switch f y x = f x y
sultana@55596
   192
sultana@55596
   193
(*Given a value of type "'a option list", produce
sultana@55596
   194
  a value of type "'a list" by dropping the NONE elements
sultana@55596
   195
  and projecting the SOME elements.*)
sultana@55596
   196
fun fold_options opt_list =
sultana@55596
   197
  fold
sultana@55596
   198
   (fn x => fn l => if is_some x then the x :: l else l)
sultana@55596
   199
   opt_list
sultana@55596
   200
   [];
sultana@55596
   201
sultana@55596
   202
val _ = @{assert}
sultana@55596
   203
  ([2,0,1] =
sultana@55596
   204
   fold_options [NONE, SOME 1, NONE, SOME 0, NONE, NONE, SOME 2]);
sultana@55596
   205
sultana@55596
   206
fun lift_option (f : 'a -> 'b) (x_opt : 'a option) : 'b option =
sultana@55596
   207
  case x_opt of
sultana@55596
   208
      NONE => NONE
sultana@55596
   209
    | SOME x => SOME (f x)
sultana@55596
   210
sultana@55596
   211
fun break_seq x = (Seq.hd x, Seq.tl x)
sultana@55596
   212
sultana@55596
   213
exception BREAK_LIST
sultana@55596
   214
fun break_list (x :: xs) = (x, xs)
sultana@55596
   215
  | break_list _ = raise BREAK_LIST
sultana@55596
   216
sultana@55596
   217
exception MULTI_ELEMENT_LIST
sultana@55596
   218
(*Try a number of predicates, in order, to find a single element.
sultana@55596
   219
  Predicates are expected to either return an empty list or a
sultana@55596
   220
  singleton list. If strict=true and list has more than one element,
sultana@55596
   221
  then raise an exception. Otherwise try a new predicate.*)
sultana@55596
   222
fun cascaded_filter_single strict preds l =
sultana@55596
   223
  case preds of
sultana@55596
   224
      [] => NONE
sultana@55596
   225
    | (p :: ps) =>
sultana@55596
   226
      case p l of
sultana@55596
   227
          [] => cascaded_filter_single strict ps l
sultana@55596
   228
        | [x] => SOME x
sultana@55596
   229
        | l =>
sultana@55596
   230
            if strict then raise MULTI_ELEMENT_LIST
sultana@55596
   231
            else cascaded_filter_single strict ps l
sultana@55596
   232
sultana@55596
   233
(*concat but with optional before-and-after delimiters*)
sultana@55596
   234
fun concat_between [] _ = []
sultana@55596
   235
  | concat_between [l] _ = l
sultana@55596
   236
  | concat_between (l :: ls) (seps as (bef, aft)) =
sultana@55596
   237
    let
sultana@55596
   238
      val pre = if is_some bef then the bef :: l else l
sultana@55596
   239
      val mid = if is_some aft then [the aft] else []
sultana@55596
   240
      val post = concat_between ls seps
sultana@55596
   241
    in
sultana@55596
   242
      pre @ mid @ post
sultana@55596
   243
    end
sultana@55596
   244
sultana@55596
   245
(*Given a list, find an element satisfying pred, and return
sultana@55596
   246
  a pair consisting of that element and the list minus the element.*)
sultana@55596
   247
fun find_and_remove pred l =
sultana@55596
   248
  find_index pred l
sultana@55596
   249
  |> switch chop l
sultana@55596
   250
  |> apsnd break_list
sultana@55596
   251
  |> (fn (xs, (y, ys)) => (y, xs @ ys))
sultana@55596
   252
sultana@55596
   253
val _ = @{assert} (find_and_remove (curry (op =) 3) [0,1,2,3,4,5] = (3, [0,1,2,4,5]))
sultana@55596
   254
sultana@55596
   255
sultana@55596
   256
(** Functions on terms **)
sultana@55596
   257
sultana@55596
   258
(*Extract the forall-prefix of a term, and return a pair consisting of the prefix
sultana@55596
   259
  and the body*)
sultana@55596
   260
local
sultana@55596
   261
  (*Strip off HOL's All combinator if it's at the toplevel*)
sultana@55596
   262
  fun try_dest_All (Const (@{const_name HOL.All}, _) $ t) = t
sultana@55596
   263
    | try_dest_All (Const (@{const_name HOL.Trueprop}, _) $ t) = try_dest_All t
sultana@55596
   264
    | try_dest_All t = t
sultana@55596
   265
sultana@55596
   266
  val _ = @{assert}
sultana@55596
   267
    ((@{term "! x. (! y. P) = True"}
sultana@55596
   268
      |> try_dest_All
sultana@55596
   269
      |> Term.strip_abs_vars)
sultana@55596
   270
     = [("x", @{typ "'a"})])
sultana@55596
   271
sultana@55596
   272
  val _ = @{assert}
sultana@55596
   273
    ((@{prop "! x. (! y. P) = True"}
sultana@55596
   274
      |> try_dest_All
sultana@55596
   275
      |> Term.strip_abs_vars)
sultana@55596
   276
     = [("x", @{typ "'a"})])
sultana@55596
   277
sultana@55596
   278
  fun strip_top_All_vars' once acc t =
sultana@55596
   279
    let
sultana@55596
   280
      val t' = try_dest_All t
sultana@55596
   281
      val var =
sultana@55596
   282
        try (Term.strip_abs_vars #> hd) t'
sultana@55596
   283
sultana@55596
   284
      fun strip v t =
sultana@55596
   285
        (v, subst_bounds ([Free v], Term.strip_abs_body t))
sultana@55596
   286
    in
sultana@55596
   287
      if t' = t orelse is_none var then (acc, t)
sultana@55596
   288
      else
sultana@55596
   289
        let
sultana@55596
   290
          val (v, t) = strip (the var) t'
sultana@55596
   291
          val acc' = v :: acc
sultana@55596
   292
        in
sultana@55596
   293
          if once then (acc', t)
sultana@55596
   294
          else strip_top_All_vars' once acc' t
sultana@55596
   295
        end
sultana@55596
   296
    end
sultana@55596
   297
in
sultana@55596
   298
  fun strip_top_All_vars t = strip_top_All_vars' false [] t
sultana@55596
   299
sultana@55596
   300
val _ =
sultana@55596
   301
  let
sultana@55596
   302
    val answer =
sultana@55596
   303
      ([("x", @{typ "'a"})],
sultana@55596
   304
       HOLogic.all_const @{typ "'a"} $
sultana@55596
   305
        (HOLogic.eq_const @{typ "'a"} $
sultana@55596
   306
         Free ("x", @{typ "'a"})))
sultana@55596
   307
  in
sultana@55596
   308
    @{assert}
sultana@55596
   309
      ((@{term "! x. All (op = x)"}
sultana@55596
   310
        |> strip_top_All_vars)
sultana@55596
   311
       = answer)
sultana@55596
   312
  end
sultana@55596
   313
sultana@55596
   314
  (*like strip_top_All_vars, but peels a single variable off, instead of all of them*)
sultana@55596
   315
  fun strip_top_All_var t =
sultana@55596
   316
    strip_top_All_vars' true [] t
sultana@55596
   317
    |> apfst the_single
sultana@55596
   318
end
sultana@55596
   319
wenzelm@56245
   320
(*like strip_top_All_vars but for "Pure.all" instead of "HOL.All"*)
sultana@55596
   321
fun strip_top_all_vars acc t =
sultana@55596
   322
  if Logic.is_all t then
sultana@55596
   323
    let
sultana@55596
   324
      val (v, t') = Logic.dest_all t
sultana@55596
   325
      (*bound instances in t' are replaced with free vars*)
sultana@55596
   326
    in
sultana@55596
   327
      strip_top_all_vars (v :: acc) t'
sultana@55596
   328
    end
sultana@55596
   329
  else (acc, (*variables are returned in FILO order*)
sultana@55596
   330
        t)
sultana@55596
   331
sultana@55596
   332
(*given a term "t"
sultana@55596
   333
    ! X Y Z. t'
sultana@55596
   334
  then then "push_allvar_in "X" t" will give
sultana@55596
   335
    ! Y Z X. t'
sultana@55596
   336
*)
sultana@55596
   337
fun push_allvar_in v t =
sultana@55596
   338
  let
sultana@55596
   339
    val (vs, t') = strip_top_All_vars t
sultana@55596
   340
    val vs' = displace_kv v vs
sultana@55596
   341
  in
sultana@55596
   342
    fold (fn (v, ty) => fn t =>
sultana@55596
   343
      HOLogic.mk_all (v, ty, t)) vs' t'
sultana@55596
   344
  end
sultana@55596
   345
sultana@55596
   346
(*Lists all consts in a term, uniquely*)
sultana@55596
   347
fun consts_in (Const c) = [Const c]
sultana@55596
   348
  | consts_in (Free _) = []
sultana@55596
   349
  | consts_in (Var _) = []
sultana@55596
   350
  | consts_in (Bound _) = []
sultana@55596
   351
  | consts_in (Abs (_, _, t)) = consts_in t
sultana@55596
   352
  | consts_in (t1 $ t2) = union (op =) (consts_in t1) (consts_in t2);
sultana@55596
   353
sultana@55596
   354
exception DIFF of term * term
sultana@55596
   355
exception DIFF_TYPE of typ * typ
sultana@55596
   356
(*This carries out naive form of matching.  It "diffs" two formulas,
sultana@55596
   357
  to create a function which maps (schematic or non-schematic)
sultana@55596
   358
  variables to terms.  The first argument is the more "general" term.
sultana@55596
   359
  The second argument is used to find the "image" for the variables in
sultana@55596
   360
  the first argument which don't appear in the second argument.
sultana@55596
   361
sultana@55596
   362
  Note that the list that is returned might have duplicate entries.
sultana@55596
   363
  It's not checked to see if the same variable maps to different
sultana@55596
   364
  values -- that should be regarded as an error.*)
sultana@55596
   365
fun diff thy (initial as (t_gen, t)) =
sultana@55596
   366
  let
sultana@55596
   367
    fun diff_ty acc [] = acc
sultana@55596
   368
      | diff_ty acc ((pair as (ty_gen, ty)) :: ts) =
sultana@55596
   369
          case pair of
sultana@55596
   370
              (Type (s1, ty_gens1), Type (s2, ty_gens2)) =>
sultana@55596
   371
                if s1 <> s2 orelse
sultana@55596
   372
                 length ty_gens1 <> length ty_gens2 then
sultana@55596
   373
                  raise (DIFF (t_gen, t))
sultana@55596
   374
                else
sultana@55596
   375
                  diff_ty acc
sultana@55596
   376
                   (ts @ ListPair.zip (ty_gens1, ty_gens2))
sultana@55596
   377
            | (TFree (s1, so1), TFree (s2, so2)) =>
sultana@55596
   378
                if s1 <> s2 orelse
sultana@55596
   379
                 not (Sign.subsort thy (so2, so1)) then
sultana@55596
   380
                  raise (DIFF (t_gen, t))
sultana@55596
   381
                else
sultana@55596
   382
                  diff_ty acc ts
sultana@55596
   383
            | (TVar (idx1, so1), TVar (idx2, so2)) =>
sultana@55596
   384
                if idx1 <> idx2 orelse
sultana@55596
   385
                 not (Sign.subsort thy (so2, so1)) then
sultana@55596
   386
                  raise (DIFF (t_gen, t))
sultana@55596
   387
                else
sultana@55596
   388
                  diff_ty acc ts
sultana@55596
   389
            | (TFree _, _) => diff_ty (pair :: acc) ts
sultana@55596
   390
            | (TVar _, _) => diff_ty (pair :: acc) ts
sultana@55596
   391
            | _ => raise (DIFF_TYPE pair)
sultana@55596
   392
sultana@55596
   393
    fun diff' (acc as (acc_t, acc_ty)) (pair as (t_gen, t)) ts =
sultana@55596
   394
      case pair of
sultana@55596
   395
          (Const (s1, ty1), Const (s2, ty2)) =>
sultana@55596
   396
            if s1 <> s2 orelse
sultana@55596
   397
             not (Sign.typ_instance thy (ty2, ty1)) then
sultana@55596
   398
              raise (DIFF (t_gen, t))
sultana@55596
   399
            else
sultana@55596
   400
              diff_probs acc ts
sultana@55596
   401
        | (Free (s1, ty1), Free (s2, ty2)) =>
sultana@55596
   402
            if s1 <> s2 orelse
sultana@55596
   403
             not (Sign.typ_instance thy (ty2, ty1)) then
sultana@55596
   404
              raise (DIFF (t_gen, t))
sultana@55596
   405
            else
sultana@55596
   406
              diff_probs acc ts
sultana@55596
   407
        | (Var (idx1, ty1), Var (idx2, ty2)) =>
sultana@55596
   408
            if idx1 <> idx2 orelse
sultana@55596
   409
             not (Sign.typ_instance thy (ty2, ty1)) then
sultana@55596
   410
              raise (DIFF (t_gen, t))
sultana@55596
   411
            else
sultana@55596
   412
              diff_probs acc ts
sultana@55596
   413
        | (Bound i1, Bound i2) =>
sultana@55596
   414
            if i1 <> i2 then
sultana@55596
   415
              raise (DIFF (t_gen, t))
sultana@55596
   416
            else
sultana@55596
   417
              diff_probs acc ts
sultana@55596
   418
        | (Abs (s1, ty1, t1), Abs (s2, ty2, t2)) =>
sultana@55596
   419
            if s1 <> s2 orelse
sultana@55596
   420
             not (Sign.typ_instance thy (ty2, ty1)) then
sultana@55596
   421
              raise (DIFF (t_gen, t))
sultana@55596
   422
            else
sultana@55596
   423
              diff' acc (t1, t2) ts
sultana@55596
   424
        | (ta1 $ ta2, tb1 $ tb2) =>
sultana@55596
   425
            diff_probs acc ((ta1, tb1) :: (ta2, tb2) :: ts)
sultana@55596
   426
sultana@55596
   427
        (*the particularly important bit*)
sultana@55596
   428
        | (Free (_, ty), _) =>
sultana@55596
   429
            diff_probs
sultana@55596
   430
             (pair :: acc_t,
sultana@55596
   431
              diff_ty acc_ty [(ty, Term.fastype_of t)])
sultana@55596
   432
             ts
sultana@55596
   433
        | (Var (_, ty), _) =>
sultana@55596
   434
            diff_probs
sultana@55596
   435
             (pair :: acc_t,
sultana@55596
   436
              diff_ty acc_ty [(ty, Term.fastype_of t)])
sultana@55596
   437
             ts
sultana@55596
   438
sultana@55596
   439
        (*everything else is problematic*)
sultana@55596
   440
        | _ => raise (DIFF (t_gen, t))
sultana@55596
   441
sultana@55596
   442
    and diff_probs acc ts =
sultana@55596
   443
      case ts of
sultana@55596
   444
          [] => acc
sultana@55596
   445
        | (pair :: ts') => diff' acc pair ts'
sultana@55596
   446
  in
sultana@55596
   447
    diff_probs ([], []) [initial]
sultana@55596
   448
  end
sultana@55596
   449
sultana@55596
   450
(*Abstracts occurrences of "t_sub" in "t", returning a list of
sultana@55596
   451
  abstractions of "t" with a Var at each occurrence of "t_sub".
sultana@55596
   452
  If "strong=true" then it uses strong abstraction (i.e., replaces
sultana@55596
   453
   all occurrnces of "t_sub"), otherwise it uses weak abstraction
sultana@55596
   454
   (i.e., replaces the occurrences one at a time).
sultana@55596
   455
  NOTE there are many more possibilities between strong and week.
sultana@55596
   456
    These can be enumerated by abstracting based on the powerset
sultana@55596
   457
    of occurrences (minus the null element, which would correspond
sultana@55596
   458
    to "t").
sultana@55596
   459
*)
sultana@55596
   460
fun guided_abstract strong t_sub t =
sultana@55596
   461
  let
sultana@55596
   462
    val varnames = Term.add_frees t [] |> map #1
sultana@55596
   463
    val prefixK = "v"
sultana@55596
   464
    val freshvar =
sultana@55596
   465
      let
sultana@55596
   466
        fun find_fresh i =
sultana@55596
   467
          let
sultana@55596
   468
            val varname = prefixK ^ Int.toString i
sultana@55596
   469
          in
sultana@55596
   470
            if member (op =) varnames varname then
sultana@55596
   471
              find_fresh (i + 1)
sultana@55596
   472
            else
sultana@55596
   473
              (varname, fastype_of t_sub)
sultana@55596
   474
          end
sultana@55596
   475
      in
sultana@55596
   476
        find_fresh 0
sultana@55596
   477
      end
sultana@55596
   478
sultana@55596
   479
    fun guided_abstract' t =
sultana@55596
   480
      case t of
sultana@55596
   481
          Abs (s, ty, t') =>
sultana@55596
   482
            if t = t_sub then [Free freshvar]
sultana@55596
   483
            else
sultana@55596
   484
              (map (fn t' => Abs (s, ty, t'))
sultana@55596
   485
               (guided_abstract' t'))
sultana@55596
   486
        | t1 $ t2 =>
sultana@55596
   487
            if t = t_sub then [Free freshvar]
sultana@55596
   488
            else
sultana@55596
   489
                (map (fn t' => t' $ t2)
sultana@55596
   490
                  (guided_abstract' t1)) @
sultana@55596
   491
                (map (fn t' => t1 $ t')
sultana@55596
   492
                  (guided_abstract' t2))
sultana@55596
   493
        | _ =>
sultana@55596
   494
            if t = t_sub then [Free freshvar]
sultana@55596
   495
            else [t]
sultana@55596
   496
sultana@55596
   497
    fun guided_abstract_strong' t =
sultana@55596
   498
      let
sultana@55596
   499
        fun continue t = guided_abstract_strong' t
sultana@55596
   500
          |> (fn x => if null x then t
sultana@55596
   501
                else the_single x)
sultana@55596
   502
      in
sultana@55596
   503
        case t of
sultana@55596
   504
            Abs (s, ty, t') =>
sultana@55596
   505
              if t = t_sub then [Free freshvar]
sultana@55596
   506
              else
sultana@55596
   507
                [Abs (s, ty, continue t')]
sultana@55596
   508
          | t1 $ t2 =>
sultana@55596
   509
              if t = t_sub then [Free freshvar]
sultana@55596
   510
              else
sultana@55596
   511
                [continue t1 $ continue t2]
sultana@55596
   512
          | _ =>
sultana@55596
   513
              if t = t_sub then [Free freshvar]
sultana@55596
   514
              else [t]
sultana@55596
   515
      end
sultana@55596
   516
sultana@55596
   517
  in
sultana@55596
   518
    ((freshvar, t_sub),
sultana@55596
   519
     if strong then guided_abstract_strong' t
sultana@55596
   520
     else guided_abstract' t)
sultana@55596
   521
  end
sultana@55596
   522
sultana@55596
   523
(*Carries out strong abstraction of a term guided by a list of
sultana@55596
   524
  other terms.
sultana@55596
   525
  In case some of the latter terms happen to be the same, it
sultana@55596
   526
  only abstracts them once.
sultana@55596
   527
  It returns the abstracted term, together with a map from
sultana@55596
   528
   the fresh names to the terms.*)
sultana@55596
   529
fun abstract ts t =
sultana@55596
   530
  fold_map (apsnd the_single oo (guided_abstract true)) ts t
sultana@55596
   531
  |> (fn (v_and_ts, t') =>
sultana@55596
   532
       let
sultana@55596
   533
         val (vs, ts) = ListPair.unzip v_and_ts
sultana@55596
   534
         val vs' =
sultana@55596
   535
           (* list_diff vs (list_diff (Term.add_frees t' []) vs) *)
sultana@55596
   536
           Term.add_frees t' []
sultana@55596
   537
           |> list_diff vs
sultana@55596
   538
           |> list_diff vs
sultana@55596
   539
         val v'_and_ts =
sultana@55596
   540
           map (fn v =>
sultana@55596
   541
             (v, AList.lookup (op =) v_and_ts v |> the))
sultana@55596
   542
            vs'
sultana@55596
   543
       in
sultana@55596
   544
         (v'_and_ts, t')
sultana@55596
   545
       end)
sultana@55596
   546
sultana@55596
   547
(*Instantiate type variables in a term, based on a type environment*)
sultana@55596
   548
fun type_devar (tyenv : ((indexname * sort) * typ) list) (t : term) : term =
sultana@55596
   549
  case t of
sultana@55596
   550
      Const (s, ty) => Const (s, Term_Subst.instantiateT tyenv ty)
sultana@55596
   551
    | Free (s, ty) => Free (s, Term_Subst.instantiateT tyenv ty)
sultana@55596
   552
    | Var (idx, ty) => Var (idx, Term_Subst.instantiateT tyenv ty)
sultana@55596
   553
    | Bound _ => t
sultana@55596
   554
    | Abs (s, ty, t') =>
sultana@55596
   555
        Abs (s, Term_Subst.instantiateT tyenv ty, type_devar tyenv t')
sultana@55596
   556
    | t1 $ t2 => type_devar tyenv t1 $ type_devar tyenv t2
sultana@55596
   557
sultana@55596
   558
(*Take a "diff" between an (abstract) thm's term, and another term
sultana@55596
   559
  (the latter is an instance of the form), then instantiate the
sultana@55596
   560
  abstract theorem. This is a way of turning the latter term into
sultana@55596
   561
  a theorem, but without exposing the proof-search functions to
sultana@55596
   562
  complex terms.
sultana@55596
   563
  In addition to the abstract thm ("scheme_thm"), this function is
sultana@55596
   564
  also supplied with the (sub)term of the abstract thm ("scheme_t")
sultana@55596
   565
  we want to use in the diff, in case only part of "scheme_t"
wenzelm@59582
   566
  might be needed (not the whole "Thm.prop_of scheme_thm")*)
sultana@55596
   567
fun diff_and_instantiate ctxt scheme_thm scheme_t instance_t =
sultana@55596
   568
  let
sultana@55596
   569
    val thy = Proof_Context.theory_of ctxt
sultana@55596
   570
sultana@55596
   571
    val (term_pairing, type_pairing) =
sultana@55596
   572
      diff thy (scheme_t, instance_t)
sultana@55596
   573
sultana@55596
   574
    (*valuation of type variables*)
wenzelm@59621
   575
    val typeval = map (apply2 (Thm.global_ctyp_of thy)) type_pairing
sultana@55596
   576
sultana@55596
   577
    val typeval_env =
sultana@55596
   578
      map (apfst dest_TVar) type_pairing
sultana@55596
   579
    (*valuation of term variables*)
sultana@55596
   580
    val termval =
sultana@55596
   581
      map (apfst (type_devar typeval_env)) term_pairing
wenzelm@59621
   582
      |> map (apply2 (Thm.global_cterm_of thy))
sultana@55596
   583
  in
sultana@55596
   584
    Thm.instantiate (typeval, termval) scheme_thm
sultana@55596
   585
  end
sultana@55596
   586
sultana@55596
   587
(*FIXME this is bad form?*)
sultana@55596
   588
val try_dest_Trueprop = perhaps (try HOLogic.dest_Trueprop)
sultana@55596
   589
sultana@55596
   590
sultana@55596
   591
(** Some tacticals **)
sultana@55596
   592
sultana@55596
   593
(*Lift COND to be parametrised by subgoal number*)
sultana@55596
   594
fun COND' sat' tac'1 tac'2 i =
sultana@55596
   595
  COND (sat' i) (tac'1 i) (tac'2 i)
sultana@55596
   596
sultana@55596
   597
(*Apply simplification ("wittler") as few times as possible
sultana@55596
   598
  before being able to apply a tactic ("tac").
sultana@55596
   599
  This is like a lazy version of REPEAT, since it attempts
sultana@55596
   600
  to REPEAT a tactic the smallest number times as possible,
sultana@55596
   601
  to make some other tactic succeed subsequently.*)
sultana@55596
   602
fun ASAP wittler (tac : int -> tactic) (i : int) = fn st =>
sultana@55596
   603
  let
sultana@55596
   604
    val tac_result = tac i st
sultana@55596
   605
    val pulled_tac_result = Seq.pull tac_result
sultana@55596
   606
    val tac_failed =
sultana@55596
   607
      is_none pulled_tac_result orelse
sultana@55596
   608
       not (has_fewer_prems 1 (fst (the pulled_tac_result)))
sultana@55596
   609
  in
sultana@55596
   610
    if tac_failed then (wittler THEN' ASAP wittler tac) i st
sultana@55596
   611
    else tac_result
sultana@55596
   612
  end
sultana@55596
   613
sultana@55596
   614
sultana@55596
   615
(** Some tactics **)
sultana@55596
   616
wenzelm@59533
   617
fun break_hypotheses_tac ctxt =
wenzelm@59533
   618
  CHANGED o
wenzelm@59533
   619
   ((REPEAT_DETERM o eresolve_tac ctxt @{thms conjE}) THEN'
wenzelm@59533
   620
    (REPEAT_DETERM o eresolve_tac ctxt @{thms disjE}))
sultana@55596
   621
sultana@55596
   622
(*Prove subgoals of form A ==> B1 | ... | A | ... | Bn*)
wenzelm@59533
   623
fun clause_breaker_tac ctxt =
wenzelm@59533
   624
  (REPEAT o resolve_tac ctxt @{thms disjI1 disjI2 conjI}) THEN'
wenzelm@59533
   625
  assume_tac ctxt
sultana@55596
   626
sultana@55596
   627
(*
sultana@55596
   628
  Refines a subgoal have the form:
sultana@55596
   629
    A1 ... An ==> B1 | ... | Aj | ... | Bi | ... | Ak | ...
sultana@55596
   630
  into multiple subgoals of the form:
sultana@55596
   631
    A'1 ==> B1 | ... | Aj | ... | Bi | ... | Ak | ...
sultana@55596
   632
     :
sultana@55596
   633
    A'm ==> B1 | ... | Aj | ... | Bi | ... | Ak | ...
sultana@55596
   634
  where {A'1 .. A'm} is disjoint from {B1, ..., Aj, ..., Bi, ..., Ak, ...}
sultana@55596
   635
  (and solves the subgoal completely if the first set is empty)
sultana@55596
   636
*)
wenzelm@59533
   637
fun batter_tac ctxt i =
wenzelm@59533
   638
  break_hypotheses_tac ctxt i THEN
wenzelm@59533
   639
  ALLGOALS (TRY o clause_breaker_tac ctxt)
sultana@55596
   640
sultana@55596
   641
(*Same idiom as ex_expander_tac*)
sultana@55596
   642
fun dist_all_and_tac ctxt i =
sultana@55596
   643
   let
sultana@55596
   644
     val simpset =
sultana@55596
   645
       empty_simpset ctxt
sultana@55596
   646
       |> Simplifier.add_simp
sultana@55596
   647
           @{lemma "! x. P x & Q x \<equiv> (! x. P x) & (! x. Q x)"
sultana@55596
   648
              by (rule eq_reflection, auto)}
sultana@55596
   649
   in
sultana@55596
   650
     CHANGED (asm_full_simp_tac simpset i)
sultana@55596
   651
   end
sultana@55596
   652
sultana@55596
   653
fun reassociate_conjs_tac ctxt =
sultana@55596
   654
  asm_full_simp_tac
sultana@55596
   655
   (Simplifier.add_simp
sultana@55596
   656
    @{lemma "(A & B) & C == A & B & C" by auto} (*FIXME duplicates @{thm simp_meta(3)}*)
sultana@55596
   657
    (Raw_Simplifier.empty_simpset ctxt))
sultana@55596
   658
  #> CHANGED
sultana@55596
   659
  #> REPEAT_DETERM
sultana@55596
   660
sultana@55596
   661
sultana@55596
   662
(** Subgoal analysis **)
sultana@55596
   663
sultana@55596
   664
(*Given an inference
sultana@55596
   665
        C
sultana@55596
   666
      -----
sultana@55596
   667
        D
sultana@55596
   668
  This function returns "SOME X" if C = "! X. C'".
sultana@55596
   669
  If C has no quantification prefix, then returns NONE.*)
wenzelm@59533
   670
fun head_quantified_variable ctxt i = fn st =>
sultana@55596
   671
  let
sultana@55596
   672
    val gls =
wenzelm@59582
   673
      Thm.prop_of st
sultana@55596
   674
      |> Logic.strip_horn
sultana@55596
   675
      |> fst
sultana@55596
   676
sultana@55596
   677
    val hypos =
sultana@55596
   678
      if null gls then []
sultana@55596
   679
      else
sultana@55596
   680
        rpair (i - 1) gls
sultana@55596
   681
        |> uncurry nth
sultana@55596
   682
        |> strip_top_all_vars []
sultana@55596
   683
        |> snd
sultana@55596
   684
        |> Logic.strip_horn
sultana@55596
   685
        |> fst
sultana@55596
   686
sultana@55596
   687
    fun foralls_of_hd_hypos () =
sultana@55596
   688
      hd hypos
sultana@55596
   689
      |> try_dest_Trueprop
sultana@55596
   690
      |> strip_top_All_vars
sultana@55596
   691
      |> #1
sultana@55596
   692
      |> rev
sultana@55596
   693
sultana@55596
   694
    val quantified_variables = foralls_of_hd_hypos ()
sultana@55596
   695
  in
sultana@55596
   696
    if null hypos orelse null quantified_variables then NONE
sultana@55596
   697
    else SOME (hd quantified_variables)
sultana@55596
   698
  end
sultana@55596
   699
sultana@55596
   700
sultana@55596
   701
(** Builders for goal analysers or transformers **)
sultana@55596
   702
sultana@55596
   703
(*Lifts function over terms to apply it to subgoals.
sultana@55596
   704
  "fun_over_terms" has type (term list * term -> 'a), where
sultana@55596
   705
  (term list * term) will be the term representations of the
sultana@55596
   706
  hypotheses and conclusion.
sultana@55596
   707
  if i_opt=SOME i then applies fun_over_terms to that
sultana@55596
   708
   subgoal and returns singleton result.
sultana@55596
   709
  otherwise applies fun_over_terms to all subgoals and return
sultana@55596
   710
   list of results.*)
sultana@55596
   711
fun TERMFUN
sultana@55596
   712
 (fun_over_terms : term list * term -> 'a)
sultana@55596
   713
 (i_opt : int option) : thm -> 'a list = fn st =>
sultana@55596
   714
  let
sultana@55596
   715
    val t_raws =
wenzelm@59586
   716
        Thm.prop_of st
sultana@55596
   717
        |> strip_top_all_vars []
sultana@55596
   718
        |> snd
sultana@55596
   719
        |> Logic.strip_horn
sultana@55596
   720
        |> fst
sultana@55596
   721
  in
sultana@55596
   722
    if null t_raws then []
sultana@55596
   723
    else
sultana@55596
   724
      let
sultana@55596
   725
        val ts =
sultana@55596
   726
          let
sultana@55596
   727
            val stripper =
sultana@55596
   728
              strip_top_all_vars []
sultana@55596
   729
              #> snd
sultana@55596
   730
              #> Logic.strip_horn
sultana@55596
   731
              #> apsnd try_dest_Trueprop
sultana@55596
   732
              #> apfst (map try_dest_Trueprop)
sultana@55596
   733
          in
sultana@55596
   734
            map stripper t_raws
sultana@55596
   735
          end
sultana@55596
   736
      in
sultana@55596
   737
        case i_opt of
sultana@55596
   738
            NONE =>
sultana@55596
   739
              map fun_over_terms ts
sultana@55596
   740
          | SOME i =>
sultana@55596
   741
              nth ts (i - 1)
sultana@55596
   742
              |> fun_over_terms
sultana@55596
   743
              |> single
sultana@55596
   744
      end
sultana@55596
   745
  end
sultana@55596
   746
sultana@55596
   747
(*Applies a predicate to subgoal(s) conclusion(s)*)
sultana@55596
   748
fun TERMPRED
sultana@55596
   749
 (hyp_pred_over_terms : term -> bool)
sultana@55596
   750
 (conc_pred_over_terms : term -> bool)
sultana@55596
   751
 (i_opt : int option) : thm -> bool = fn st =>
sultana@55596
   752
    let
sultana@55596
   753
      val hyp_results =
sultana@55596
   754
        TERMFUN (fst (*discard hypotheses*)
sultana@55596
   755
                 #> map hyp_pred_over_terms) i_opt st
sultana@55596
   756
      val conc_results =
sultana@55596
   757
        TERMFUN (snd (*discard hypotheses*)
sultana@55596
   758
                 #> conc_pred_over_terms) i_opt st
sultana@55596
   759
      val _ = @{assert} (length hyp_results = length conc_results)
sultana@55596
   760
    in
sultana@55596
   761
      if null hyp_results then true
sultana@55596
   762
      else
sultana@55596
   763
        let
sultana@55596
   764
          val hyps_conjoined =
sultana@55596
   765
            fold (fn a => fn b =>
wenzelm@58412
   766
              b andalso (forall (fn x => x) a)) hyp_results true
sultana@55596
   767
          val concs_conjoined =
sultana@55596
   768
            fold (fn a => fn b =>
sultana@55596
   769
              b andalso a) conc_results true
sultana@55596
   770
        in hyps_conjoined andalso concs_conjoined end
sultana@55596
   771
    end
sultana@55596
   772
sultana@55596
   773
sultana@55596
   774
(** Tracing **)
sultana@55596
   775
(*If "tac i st" succeeds then msg is printed to "trace" channel*)
wenzelm@59533
   776
fun trace_tac' ctxt msg tac i st =
sultana@55596
   777
  let
sultana@55596
   778
    val result = tac i st
sultana@55596
   779
  in
sultana@55596
   780
    if Config.get ctxt tptp_trace_reconstruction andalso
sultana@55596
   781
     not (is_none (Seq.pull result)) then
sultana@55596
   782
      (tracing msg; result)
sultana@55596
   783
    else result
sultana@55596
   784
  end
sultana@55596
   785
sultana@55596
   786
end