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