src/HOL/Tools/res_atp.ML
author paulson
Mon, 02 Oct 2006 17:30:56 +0200
changeset 20823 5480ec4b542d
parent 20781 e26fe5c63c2f
child 20854 f9cf9e62d11c
permissions -rw-r--r--
restored the "length of name > 2" check for package definitions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
     1
(*  Author: Jia Meng, Cambridge University Computer Laboratory, NICTA
15608
f161fa6f8fd5 bug fixes involving typechecking clauses
paulson
parents: 15603
diff changeset
     2
    ID: $Id$
f161fa6f8fd5 bug fixes involving typechecking clauses
paulson
parents: 15603
diff changeset
     3
    Copyright 2004 University of Cambridge
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
     4
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
     5
ATPs with TPTP format input.
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
     6
*)
15452
e2a721567f67 Jia Meng: delta simpsets and clasets
paulson
parents: 15347
diff changeset
     7
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
     8
(*FIXME: Do we need this signature?*)
16802
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
     9
signature RES_ATP =
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
    10
sig
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
    11
  val prover: string ref
16802
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
    12
  val custom_spass: string list ref
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
    13
  val destdir: string ref
17849
d7619ccf22e6 signature changes
paulson
parents: 17845
diff changeset
    14
  val helper_path: string -> string -> string
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
    15
  val problem_name: string ref
17690
8ba7c3cd24a8 time limit option; fixed bug concerning first line of ATP output
paulson
parents: 17525
diff changeset
    16
  val time_limit: int ref
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    17
   
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    18
  datatype mode = Auto | Fol | Hol
19450
651d949776f8 exported linkup_logic_mode and changed the default setting
paulson
parents: 19445
diff changeset
    19
  val linkup_logic_mode : mode ref
19722
e7a5b54248bc Added in settings used by "spass" method.
mengj
parents: 19718
diff changeset
    20
  val write_subgoal_file: bool -> mode -> Proof.context -> thm list -> thm list -> int -> string
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    21
  val vampire_time: int ref
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    22
  val eprover_time: int ref
19722
e7a5b54248bc Added in settings used by "spass" method.
mengj
parents: 19718
diff changeset
    23
  val spass_time: int ref
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    24
  val run_vampire: int -> unit
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    25
  val run_eprover: int -> unit
19722
e7a5b54248bc Added in settings used by "spass" method.
mengj
parents: 19718
diff changeset
    26
  val run_spass: int -> unit
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    27
  val vampireLimit: unit -> int
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    28
  val eproverLimit: unit -> int
19722
e7a5b54248bc Added in settings used by "spass" method.
mengj
parents: 19718
diff changeset
    29
  val spassLimit: unit -> int
20289
ba7a7c56bed5 normalized Proof.context/method type aliases;
wenzelm
parents: 20246
diff changeset
    30
  val atp_method: (Proof.context -> thm list -> int -> tactic) ->
ba7a7c56bed5 normalized Proof.context/method type aliases;
wenzelm
parents: 20246
diff changeset
    31
    Method.src -> Proof.context -> Proof.method
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    32
  val cond_rm_tmp: string -> unit
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    33
  val keep_atp_input: bool ref
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    34
  val fol_keep_types: bool ref
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    35
  val hol_full_types: unit -> unit
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    36
  val hol_partial_types: unit -> unit
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    37
  val hol_const_types_only: unit -> unit
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    38
  val hol_no_types: unit -> unit
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    39
  val hol_typ_level: unit -> ResHolClause.type_level
20246
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
    40
  val include_all: bool ref
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    41
  val run_relevance_filter: bool ref
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
    42
  val run_blacklist_filter: bool ref
20372
e42674e0486e blacklist augmented to block some "unit" theorems that cause unsound resolution proofs
paulson
parents: 20289
diff changeset
    43
  val blacklist: string list ref
19894
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
    44
  val add_all : unit -> unit
19227
d15f2baa7ecc Added more functions to the signature and tidied up some functions.
mengj
parents: 19205
diff changeset
    45
  val add_claset : unit -> unit
d15f2baa7ecc Added more functions to the signature and tidied up some functions.
mengj
parents: 19205
diff changeset
    46
  val add_simpset : unit -> unit
d15f2baa7ecc Added more functions to the signature and tidied up some functions.
mengj
parents: 19205
diff changeset
    47
  val add_clasimp : unit -> unit
d15f2baa7ecc Added more functions to the signature and tidied up some functions.
mengj
parents: 19205
diff changeset
    48
  val add_atpset : unit -> unit
19894
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
    49
  val rm_all : unit -> unit
19227
d15f2baa7ecc Added more functions to the signature and tidied up some functions.
mengj
parents: 19205
diff changeset
    50
  val rm_claset : unit -> unit
d15f2baa7ecc Added more functions to the signature and tidied up some functions.
mengj
parents: 19205
diff changeset
    51
  val rm_simpset : unit -> unit
d15f2baa7ecc Added more functions to the signature and tidied up some functions.
mengj
parents: 19205
diff changeset
    52
  val rm_atpset : unit -> unit
d15f2baa7ecc Added more functions to the signature and tidied up some functions.
mengj
parents: 19205
diff changeset
    53
  val rm_clasimp : unit -> unit
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    54
end;
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    55
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
    56
structure ResAtp =
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    57
struct
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
    58
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    59
(********************************************************************)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    60
(* some settings for both background automatic ATP calling procedure*)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    61
(* and also explicit ATP invocation methods                         *)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    62
(********************************************************************)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    63
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    64
(*** background linkup ***)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    65
val call_atp = ref false; 
17150
ce2a1aeb42aa DFG output now works for untyped rules (ML "ResClause.untyped();")
quigley
parents: 17091
diff changeset
    66
val hook_count = ref 0;
20419
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20372
diff changeset
    67
val time_limit = ref 80;
17404
d16c3a62c396 the experimental tagging system, and the usual tidying
paulson
parents: 17317
diff changeset
    68
val prover = ref "E";   (* use E as the default prover *)
17305
6cef3aedd661 axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents: 17235
diff changeset
    69
val custom_spass =   (*specialized options for SPASS*)
17690
8ba7c3cd24a8 time limit option; fixed bug concerning first line of ATP output
paulson
parents: 17525
diff changeset
    70
      ref ["-Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub"];
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
    71
val destdir = ref "";   (*Empty means write files to /tmp*)
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
    72
val problem_name = ref "prob";
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
    73
17819
1241e5d31d5b small tidy-up of utility functions
paulson
parents: 17775
diff changeset
    74
(*Return the path to a "helper" like SPASS or tptp2X, first checking that
1241e5d31d5b small tidy-up of utility functions
paulson
parents: 17775
diff changeset
    75
  it exists.  FIXME: modify to use Path primitives and move to some central place.*)  
1241e5d31d5b small tidy-up of utility functions
paulson
parents: 17775
diff changeset
    76
fun helper_path evar base =
1241e5d31d5b small tidy-up of utility functions
paulson
parents: 17775
diff changeset
    77
  case getenv evar of
1241e5d31d5b small tidy-up of utility functions
paulson
parents: 17775
diff changeset
    78
      "" => error  ("Isabelle environment variable " ^ evar ^ " not defined")
1241e5d31d5b small tidy-up of utility functions
paulson
parents: 17775
diff changeset
    79
    | home => 
1241e5d31d5b small tidy-up of utility functions
paulson
parents: 17775
diff changeset
    80
        let val path = home ^ "/" ^ base
1241e5d31d5b small tidy-up of utility functions
paulson
parents: 17775
diff changeset
    81
        in  if File.exists (File.unpack_platform_path path) then path 
1241e5d31d5b small tidy-up of utility functions
paulson
parents: 17775
diff changeset
    82
	    else error ("Could not find the file " ^ path)
1241e5d31d5b small tidy-up of utility functions
paulson
parents: 17775
diff changeset
    83
	end;  
1241e5d31d5b small tidy-up of utility functions
paulson
parents: 17775
diff changeset
    84
17717
7c6a96cbc966 improvements for problem generation
paulson
parents: 17690
diff changeset
    85
fun probfile_nosuffix _ = 
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
    86
  if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name)))
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
    87
  else if File.exists (File.unpack_platform_path (!destdir))
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
    88
  then !destdir ^ "/" ^ !problem_name
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
    89
  else error ("No such directory: " ^ !destdir);
15644
f2ef8c258fa4 *** empty log message ***
quigley
parents: 15608
diff changeset
    90
17717
7c6a96cbc966 improvements for problem generation
paulson
parents: 17690
diff changeset
    91
fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n;
7c6a96cbc966 improvements for problem generation
paulson
parents: 17690
diff changeset
    92
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    93
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    94
(*** ATP methods ***)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    95
val vampire_time = ref 60;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    96
val eprover_time = ref 60;
19722
e7a5b54248bc Added in settings used by "spass" method.
mengj
parents: 19718
diff changeset
    97
val spass_time = ref 60;
e7a5b54248bc Added in settings used by "spass" method.
mengj
parents: 19718
diff changeset
    98
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
    99
fun run_vampire time =  
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   100
    if (time >0) then vampire_time:= time
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   101
    else vampire_time:=60;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   102
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   103
fun run_eprover time = 
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   104
    if (time > 0) then eprover_time:= time
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   105
    else eprover_time:=60;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   106
19722
e7a5b54248bc Added in settings used by "spass" method.
mengj
parents: 19718
diff changeset
   107
fun run_spass time = 
e7a5b54248bc Added in settings used by "spass" method.
mengj
parents: 19718
diff changeset
   108
    if (time > 0) then spass_time:=time
e7a5b54248bc Added in settings used by "spass" method.
mengj
parents: 19718
diff changeset
   109
    else spass_time:=60;
e7a5b54248bc Added in settings used by "spass" method.
mengj
parents: 19718
diff changeset
   110
e7a5b54248bc Added in settings used by "spass" method.
mengj
parents: 19718
diff changeset
   111
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   112
fun vampireLimit () = !vampire_time;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   113
fun eproverLimit () = !eprover_time;
19722
e7a5b54248bc Added in settings used by "spass" method.
mengj
parents: 19718
diff changeset
   114
fun spassLimit () = !spass_time;
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   115
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   116
val keep_atp_input = ref false;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   117
val fol_keep_types = ResClause.keep_types;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   118
val hol_full_types = ResHolClause.full_types;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   119
val hol_partial_types = ResHolClause.partial_types;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   120
val hol_const_types_only = ResHolClause.const_types_only;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   121
val hol_no_types = ResHolClause.no_types;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   122
fun hol_typ_level () = ResHolClause.find_typ_level ();
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   123
fun is_typed_hol () = 
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   124
    let val tp_level = hol_typ_level()
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   125
    in
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   126
	not (tp_level = ResHolClause.T_NONE)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   127
    end;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   128
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   129
fun atp_input_file () =
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   130
    let val file = !problem_name 
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   131
    in
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   132
	if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file))
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   133
	else if File.exists (File.unpack_platform_path (!destdir))
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   134
	then !destdir ^ "/" ^ file
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   135
	else error ("No such directory: " ^ !destdir)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   136
    end;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   137
19894
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   138
val include_all = ref false;
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   139
val include_simpset = ref false;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   140
val include_claset = ref false; 
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   141
val include_atpset = ref true;
20246
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   142
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   143
(*Tests show that follow_defs gives VERY poor results with "include_all"*)
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   144
fun add_all() = (include_all:=true; ReduceAxiomsN.follow_defs := false);
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   145
fun rm_all() = include_all:=false;
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   146
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   147
fun add_simpset() = include_simpset:=true;
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   148
fun rm_simpset() = include_simpset:=false;
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   149
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   150
fun add_claset() = include_claset:=true;
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   151
fun rm_claset() = include_claset:=false;
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   152
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   153
fun add_clasimp() = (include_simpset:=true;include_claset:=true);
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   154
fun rm_clasimp() = (include_simpset:=false;include_claset:=false);
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   155
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   156
fun add_atpset() = include_atpset:=true;
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   157
fun rm_atpset() = include_atpset:=false;
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   158
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   159
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   160
(**** relevance filter ****)
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   161
val run_relevance_filter = ReduceAxiomsN.run_relevance_filter;
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   162
val run_blacklist_filter = ref true;
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   163
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   164
(******************************************************************)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   165
(* detect whether a given problem (clauses) is FOL/HOL/HOLC/HOLCS *)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   166
(******************************************************************)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   167
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   168
datatype logic = FOL | HOL | HOLC | HOLCS;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   169
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   170
fun string_of_logic FOL = "FOL"
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   171
  | string_of_logic HOL = "HOL"
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   172
  | string_of_logic HOLC = "HOLC"
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   173
  | string_of_logic HOLCS = "HOLCS";
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   174
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   175
fun is_fol_logic FOL = true
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   176
  | is_fol_logic  _ = false
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   177
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   178
(*HOLCS will not occur here*)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   179
fun upgrade_lg HOLC _ = HOLC
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   180
  | upgrade_lg HOL HOLC = HOLC
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   181
  | upgrade_lg HOL _ = HOL
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   182
  | upgrade_lg FOL lg = lg; 
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   183
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   184
(* check types *)
19451
c7a25c05986c Changed the logic detection method.
mengj
parents: 19450
diff changeset
   185
fun has_bool_hfn (Type("bool",_)) = true
c7a25c05986c Changed the logic detection method.
mengj
parents: 19450
diff changeset
   186
  | has_bool_hfn (Type("fun",_)) = true
c7a25c05986c Changed the logic detection method.
mengj
parents: 19450
diff changeset
   187
  | has_bool_hfn (Type(_, Ts)) = exists has_bool_hfn Ts
c7a25c05986c Changed the logic detection method.
mengj
parents: 19450
diff changeset
   188
  | has_bool_hfn _ = false;
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   189
19451
c7a25c05986c Changed the logic detection method.
mengj
parents: 19450
diff changeset
   190
fun is_hol_fn tp =
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   191
    let val (targs,tr) = strip_type tp
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   192
    in
19451
c7a25c05986c Changed the logic detection method.
mengj
parents: 19450
diff changeset
   193
	exists (has_bool_hfn) (tr::targs)
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   194
    end;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   195
19451
c7a25c05986c Changed the logic detection method.
mengj
parents: 19450
diff changeset
   196
fun is_hol_pred tp =
c7a25c05986c Changed the logic detection method.
mengj
parents: 19450
diff changeset
   197
    let val (targs,tr) = strip_type tp
c7a25c05986c Changed the logic detection method.
mengj
parents: 19450
diff changeset
   198
    in
c7a25c05986c Changed the logic detection method.
mengj
parents: 19450
diff changeset
   199
	exists (has_bool_hfn) targs
c7a25c05986c Changed the logic detection method.
mengj
parents: 19450
diff changeset
   200
    end;
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   201
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   202
exception FN_LG of term;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   203
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   204
fun fn_lg (t as Const(f,tp)) (lg,seen) = 
19451
c7a25c05986c Changed the logic detection method.
mengj
parents: 19450
diff changeset
   205
    if is_hol_fn tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   206
  | fn_lg (t as Free(f,tp)) (lg,seen) = 
19451
c7a25c05986c Changed the logic detection method.
mengj
parents: 19450
diff changeset
   207
    if is_hol_fn tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   208
  | fn_lg (t as Var(f,tp)) (lg,seen) =
19451
c7a25c05986c Changed the logic detection method.
mengj
parents: 19450
diff changeset
   209
    if is_hol_fn tp then (upgrade_lg HOL lg,t ins seen) else (lg,t ins seen)
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   210
  | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,t ins seen)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   211
  | fn_lg f _ = raise FN_LG(f); 
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   212
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   213
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   214
fun term_lg [] (lg,seen) = (lg,seen)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   215
  | term_lg (tm::tms) (FOL,seen) =
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   216
      let val (f,args) = strip_comb tm
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   217
	  val (lg',seen') = if f mem seen then (FOL,seen) 
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   218
			    else fn_lg f (FOL,seen)
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   219
      in
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   220
	if is_fol_logic lg' then ()
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   221
        else Output.debug ("Found a HOL term: " ^ Display.raw_string_of_term f);
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   222
        term_lg (args@tms) (lg',seen')
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   223
      end
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   224
  | term_lg _ (lg,seen) = (lg,seen)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   225
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   226
exception PRED_LG of term;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   227
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   228
fun pred_lg (t as Const(P,tp)) (lg,seen)= 
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   229
      if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) 
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   230
  | pred_lg (t as Free(P,tp)) (lg,seen) =
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   231
      if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen)
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   232
  | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, t ins seen)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   233
  | pred_lg P _ = raise PRED_LG(P);
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   234
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   235
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   236
fun lit_lg (Const("Not",_) $ P) (lg,seen) = lit_lg P (lg,seen)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   237
  | lit_lg P (lg,seen) =
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   238
      let val (pred,args) = strip_comb P
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   239
	  val (lg',seen') = if pred mem seen then (lg,seen) 
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   240
			    else pred_lg pred (lg,seen)
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   241
      in
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   242
	if is_fol_logic lg' then ()
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   243
	else Output.debug ("Found a HOL predicate: " ^ Display.raw_string_of_term pred);
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   244
	term_lg args (lg',seen')
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   245
      end;
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   246
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   247
fun lits_lg [] (lg,seen) = (lg,seen)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   248
  | lits_lg (lit::lits) (FOL,seen) =
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   249
      let val (lg,seen') = lit_lg lit (FOL,seen)
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   250
      in
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   251
	if is_fol_logic lg then ()
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   252
	else Output.debug ("Found a HOL literal: " ^ Display.raw_string_of_term lit);
19227
d15f2baa7ecc Added more functions to the signature and tidied up some functions.
mengj
parents: 19205
diff changeset
   253
	lits_lg lits (lg,seen')
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   254
      end
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   255
  | lits_lg lits (lg,seen) = (lg,seen);
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   256
19227
d15f2baa7ecc Added more functions to the signature and tidied up some functions.
mengj
parents: 19205
diff changeset
   257
fun dest_disj_aux (Const ("op |", _) $ t $ t') disjs = 
d15f2baa7ecc Added more functions to the signature and tidied up some functions.
mengj
parents: 19205
diff changeset
   258
    dest_disj_aux t (dest_disj_aux t' disjs)
d15f2baa7ecc Added more functions to the signature and tidied up some functions.
mengj
parents: 19205
diff changeset
   259
  | dest_disj_aux t disjs = t::disjs;
d15f2baa7ecc Added more functions to the signature and tidied up some functions.
mengj
parents: 19205
diff changeset
   260
d15f2baa7ecc Added more functions to the signature and tidied up some functions.
mengj
parents: 19205
diff changeset
   261
fun dest_disj t = dest_disj_aux t [];
d15f2baa7ecc Added more functions to the signature and tidied up some functions.
mengj
parents: 19205
diff changeset
   262
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   263
fun logic_of_clause tm (lg,seen) =
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   264
    let val tm' = HOLogic.dest_Trueprop tm
19227
d15f2baa7ecc Added more functions to the signature and tidied up some functions.
mengj
parents: 19205
diff changeset
   265
	val disjs = dest_disj tm'
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   266
    in
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   267
	lits_lg disjs (lg,seen)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   268
    end;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   269
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   270
fun logic_of_clauses [] (lg,seen) = (lg,seen)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   271
  | logic_of_clauses (cls::clss) (FOL,seen) =
19227
d15f2baa7ecc Added more functions to the signature and tidied up some functions.
mengj
parents: 19205
diff changeset
   272
    let val (lg,seen') = logic_of_clause cls (FOL,seen)
19641
f1de44e61ec1 replaced low-level Term.str_of by Display.raw_string_of_term (should actually use Display.string_of_term);
wenzelm
parents: 19617
diff changeset
   273
	val _ =
f1de44e61ec1 replaced low-level Term.str_of by Display.raw_string_of_term (should actually use Display.string_of_term);
wenzelm
parents: 19617
diff changeset
   274
          if is_fol_logic lg then ()
19746
9ac97dc14214 warnings to debug outputs
paulson
parents: 19744
diff changeset
   275
          else Output.debug ("Found a HOL clause: " ^ Display.raw_string_of_term cls)
19227
d15f2baa7ecc Added more functions to the signature and tidied up some functions.
mengj
parents: 19205
diff changeset
   276
    in
d15f2baa7ecc Added more functions to the signature and tidied up some functions.
mengj
parents: 19205
diff changeset
   277
	logic_of_clauses clss (lg,seen')
d15f2baa7ecc Added more functions to the signature and tidied up some functions.
mengj
parents: 19205
diff changeset
   278
    end
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   279
  | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen);
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   280
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   281
fun problem_logic_goals_aux [] (lg,seen) = lg
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   282
  | problem_logic_goals_aux (subgoal::subgoals) (lg,seen) = 
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   283
    problem_logic_goals_aux subgoals (logic_of_clauses subgoal (lg,seen));
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   284
    
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   285
fun problem_logic_goals subgoals = problem_logic_goals_aux subgoals (FOL,[]);
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   286
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   287
(***************************************************************)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   288
(* Retrieving and filtering lemmas                             *)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   289
(***************************************************************)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   290
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   291
(*** white list and black list of lemmas ***)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   292
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   293
(*The rule subsetI is frequently omitted by the relevance filter.*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   294
val whitelist = ref [subsetI]; 
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   295
20444
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   296
(*Names of theorems and theorem lists to be banned. The final numeric suffix of
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   297
  theorem lists is first removed.
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   298
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   299
  These theorems typically produce clauses that are prolific (match too many equality or
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   300
  membership literals) and relate to seldom-used facts. Some duplicate other rules.
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   301
  FIXME: this blacklist needs to be maintained using theory data and added to using
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   302
  an attribute.*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   303
val blacklist = ref
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   304
  ["Datatype.prod.size",
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   305
   "Datatype.unit.induct", (*"unit" thms cause unsound proofs; unit.nchotomy is caught automatically*)
20372
e42674e0486e blacklist augmented to block some "unit" theorems that cause unsound resolution proofs
paulson
parents: 20289
diff changeset
   306
   "Datatype.unit.inducts",
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   307
   "Datatype.unit.split_asm", 
20372
e42674e0486e blacklist augmented to block some "unit" theorems that cause unsound resolution proofs
paulson
parents: 20289
diff changeset
   308
   "Datatype.unit.split",
20444
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   309
   "Datatype.unit.splits",
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   310
   "Divides.dvd_0_left_iff",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   311
   "Finite_Set.card_0_eq",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   312
   "Finite_Set.card_infinite",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   313
   "Finite_Set.Max_ge",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   314
   "Finite_Set.Max_in",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   315
   "Finite_Set.Max_le_iff",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   316
   "Finite_Set.Max_less_iff",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   317
   "Finite_Set.max.f_below_strict_below.below_f_conv", (*duplicates in Orderings.*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   318
   "Finite_Set.max.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   319
   "Finite_Set.Min_ge_iff",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   320
   "Finite_Set.Min_gr_iff",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   321
   "Finite_Set.Min_in",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   322
   "Finite_Set.Min_le",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   323
   "Finite_Set.min_max.below_inf_sup_Inf_Sup.inf_Sup_absorb", 
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   324
   "Finite_Set.min_max.below_inf_sup_Inf_Sup.sup_Inf_absorb", 
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   325
   "Finite_Set.min.f_below_strict_below.below_f_conv",        (*duplicates in Orderings.*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   326
   "Finite_Set.min.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   327
   "Fun.vimage_image_eq",   (*involves an existential quantifier*)
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   328
   "HOL.split_if_asm",     (*splitting theorem*)
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   329
   "HOL.split_if",         (*splitting theorem*)
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   330
   "IntDef.abs_split",
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   331
   "IntDef.Integ.Abs_Integ_inject",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   332
   "IntDef.Integ.Abs_Integ_inverse",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   333
   "IntDiv.zdvd_0_left",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   334
   "List.append_eq_append_conv",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   335
   "List.hd_Cons_tl",   (*Says everything is [] or Cons. Probably prolific.*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   336
   "List.in_listsD",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   337
   "List.in_listsI",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   338
   "List.lists.Cons",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   339
   "List.listsE",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   340
   "Nat.less_one", (*not directional? obscure*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   341
   "Nat.not_gr0",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   342
   "Nat.one_eq_mult_iff", (*duplicate by symmetry*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   343
   "NatArith.of_nat_0_eq_iff",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   344
   "NatArith.of_nat_eq_0_iff",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   345
   "NatArith.of_nat_le_0_iff",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   346
   "NatSimprocs.divide_le_0_iff_number_of",  (*too many clauses*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   347
   "NatSimprocs.divide_less_0_iff_number_of",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   348
   "NatSimprocs.equation_minus_iff_1",  (*not directional*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   349
   "NatSimprocs.equation_minus_iff_number_of", (*not directional*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   350
   "NatSimprocs.le_minus_iff_1", (*not directional*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   351
   "NatSimprocs.le_minus_iff_number_of",  (*not directional*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   352
   "NatSimprocs.less_minus_iff_1", (*not directional*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   353
   "NatSimprocs.less_minus_iff_number_of", (*not directional*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   354
   "NatSimprocs.minus_equation_iff_number_of", (*not directional*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   355
   "NatSimprocs.minus_le_iff_1", (*not directional*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   356
   "NatSimprocs.minus_le_iff_number_of", (*not directional*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   357
   "NatSimprocs.minus_less_iff_1", (*not directional*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   358
   "NatSimprocs.mult_le_cancel_left_number_of", (*excessive case analysis*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   359
   "NatSimprocs.mult_le_cancel_right_number_of", (*excessive case analysis*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   360
   "NatSimprocs.mult_less_cancel_left_number_of", (*excessive case analysis*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   361
   "NatSimprocs.mult_less_cancel_right_number_of", (*excessive case analysis*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   362
   "NatSimprocs.zero_le_divide_iff_number_of", (*excessive case analysis*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   363
   "NatSimprocs.zero_less_divide_iff_number_of",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   364
   "OrderedGroup.abs_0_eq", (*duplicate by symmetry*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   365
   "OrderedGroup.diff_eq_0_iff_eq", (*prolific?*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   366
   "OrderedGroup.join_0_eq_0",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   367
   "OrderedGroup.meet_0_eq_0",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   368
   "OrderedGroup.pprt_eq_0",   (*obscure*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   369
   "OrderedGroup.pprt_eq_id",   (*obscure*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   370
   "OrderedGroup.pprt_mono",   (*obscure*)
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   371
   "Orderings.split_max",      (*splitting theorem*)
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   372
   "Orderings.split_min",      (*splitting theorem*)
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   373
   "Parity.even_nat_power",   (*obscure, somewhat prolilfic*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   374
   "Parity.power_eq_0_iff_number_of",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   375
   "Parity.power_le_zero_eq_number_of",   (*obscure and prolific*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   376
   "Parity.power_less_zero_eq_number_of",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   377
   "Parity.zero_le_power_eq_number_of",   (*obscure and prolific*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   378
   "Parity.zero_less_power_eq_number_of",   (*obscure and prolific*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   379
   "Power.zero_less_power_abs_iff",
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   380
   "Product_Type.split_eta_SetCompr",   (*involves an existential quantifier*)
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   381
   "Product_Type.split_paired_Ball_Sigma",     (*splitting theorem*)
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   382
   "Product_Type.split_paired_Bex_Sigma",      (*splitting theorem*)
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   383
   "Product_Type.split_split_asm",             (*splitting theorem*)
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   384
   "Product_Type.split_split",                 (*splitting theorem*)
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   385
   "Product_Type.unit_abs_eta_conv",
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   386
   "Product_Type.unit_induct",
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   387
   "Relation.diagI",
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   388
   "Relation.Domain_def",   (*involves an existential quantifier*)
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   389
   "Relation.Image_def",   (*involves an existential quantifier*)
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   390
   "Relation.ImageI",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   391
   "Ring_and_Field.divide_cancel_left", (*fields are seldom used & often prolific*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   392
   "Ring_and_Field.divide_cancel_right",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   393
   "Ring_and_Field.divide_divide_eq_left",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   394
   "Ring_and_Field.divide_divide_eq_right",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   395
   "Ring_and_Field.divide_eq_0_iff",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   396
   "Ring_and_Field.divide_eq_1_iff",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   397
   "Ring_and_Field.divide_eq_eq_1",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   398
   "Ring_and_Field.divide_le_0_1_iff",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   399
   "Ring_and_Field.divide_le_eq_1_neg",  (*obscure and prolific*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   400
   "Ring_and_Field.divide_le_eq_1_pos",  (*obscure and prolific*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   401
   "Ring_and_Field.divide_less_0_1_iff",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   402
   "Ring_and_Field.divide_less_eq_1_neg",  (*obscure and prolific*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   403
   "Ring_and_Field.divide_less_eq_1_pos",  (*obscure and prolific*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   404
   "Ring_and_Field.eq_divide_eq_1", (*duplicate by symmetry*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   405
   "Ring_and_Field.field_mult_cancel_left",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   406
   "Ring_and_Field.field_mult_cancel_right",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   407
   "Ring_and_Field.inverse_le_iff_le_neg",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   408
   "Ring_and_Field.inverse_le_iff_le",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   409
   "Ring_and_Field.inverse_less_iff_less_neg",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   410
   "Ring_and_Field.inverse_less_iff_less",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   411
   "Ring_and_Field.le_divide_eq_1_neg", (*obscure and prolific*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   412
   "Ring_and_Field.le_divide_eq_1_pos", (*obscure and prolific*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   413
   "Ring_and_Field.less_divide_eq_1_neg", (*obscure and prolific*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   414
   "Ring_and_Field.less_divide_eq_1_pos", (*obscure and prolific*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   415
   "Ring_and_Field.one_eq_divide_iff",  (*duplicate by symmetry*)
20444
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   416
   "Set.ball_simps", "Set.bex_simps",   (*quantifier rewriting: useless*)
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   417
   "Set.Collect_bex_eq",   (*involves an existential quantifier*)
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   418
   "Set.Collect_ex_eq",   (*involves an existential quantifier*)
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   419
   "Set.Diff_eq_empty_iff", (*redundant with paramodulation*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   420
   "Set.Diff_insert0",
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   421
   "Set.disjoint_insert",
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   422
   "Set.empty_Union_conv",   (*redundant with paramodulation*)
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   423
   "Set.full_SetCompr_eq",   (*involves an existential quantifier*)
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   424
   "Set.image_Collect",      (*involves an existential quantifier*)
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   425
   "Set.image_def",          (*involves an existential quantifier*)
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   426
   "Set.insert_disjoint",
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   427
   "Set.Int_UNIV",  (*redundant with paramodulation*)
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   428
   "Set.Inter_iff", (*We already have InterI, InterE*)
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   429
   "Set.Inter_UNIV_conv",
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   430
   "Set.psubsetE",    (*too prolific and obscure*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   431
   "Set.psubsetI",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   432
   "Set.singleton_insert_inj_eq'",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   433
   "Set.singleton_insert_inj_eq",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   434
   "Set.singletonD",  (*these two duplicate some "insert" lemmas*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   435
   "Set.singletonI",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   436
   "Set.Un_empty", (*redundant with paramodulation*)
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   437
   "Set.UNION_def",   (*involves an existential quantifier*)
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   438
   "Set.Union_empty_conv", (*redundant with paramodulation*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   439
   "Set.Union_iff",              (*We already have UnionI, UnionE*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   440
   "SetInterval.atLeastAtMost_iff", (*obscure and prolific*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   441
   "SetInterval.atLeastLessThan_iff", (*obscure and prolific*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   442
   "SetInterval.greaterThanAtMost_iff", (*obscure and prolific*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   443
   "SetInterval.greaterThanLessThan_iff", (*obscure and prolific*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   444
   "SetInterval.ivl_subset"];  (*excessive case analysis*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   445
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   446
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   447
(*These might be prolific but are probably OK, and min and max are basic.
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   448
   "Orderings.max_less_iff_conj", 
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   449
   "Orderings.min_less_iff_conj",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   450
   "Orderings.min_max.below_inf.below_inf_conv",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   451
   "Orderings.min_max.below_sup.above_sup_conv",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   452
Very prolific and somewhat obscure:
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   453
   "Set.InterD",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   454
   "Set.UnionI",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   455
*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   456
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   457
(*** retrieve lemmas from clasimpset and atpset, may filter them ***)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   458
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   459
(*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   460
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   461
exception HASH_CLAUSE and HASH_STRING;
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   462
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   463
(*Catches (for deletion) theorems automatically generated from other theorems*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   464
fun insert_suffixed_names ht x = 
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   465
     (Polyhash.insert ht (x^"_iff1", ()); 
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   466
      Polyhash.insert ht (x^"_iff2", ()); 
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   467
      Polyhash.insert ht (x^"_dest", ())); 
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   468
20444
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   469
(*Are all characters in this string digits?*)
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   470
fun all_numeric s = null (String.tokens Char.isDigit s);
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   471
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   472
(*Delete a suffix of the form _\d+*)
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   473
fun delete_numeric_suffix s =
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   474
  case rev (String.fields (fn c => c = #"_") s) of
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   475
      last::rest => 
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   476
          if all_numeric last 
20446
7e616709bca2 String.concatWith (not available in PolyML) replaced by space_implode
webertj
parents: 20444
diff changeset
   477
          then [s, space_implode "_" (rev rest)]
20444
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   478
          else [s]
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   479
    | [] => [s];
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   480
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   481
fun banned_thmlist s =
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   482
  (Sign.base_name s) mem_string ["induct","inducts","split","splits","split_asm"];
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   483
20757
fe84fe0dfd30 Definitions produced by packages are now blacklisted.
paulson
parents: 20661
diff changeset
   484
(*Reject theorems with names like "List.filter.filter_list_def" or
20823
5480ec4b542d restored the "length of name > 2" check for package definitions
paulson
parents: 20781
diff changeset
   485
  "Accessible_Part.acc.defs", as these are definitions arising from packages.
5480ec4b542d restored the "length of name > 2" check for package definitions
paulson
parents: 20781
diff changeset
   486
  FIXME: this will also block definitions within locales*)
20757
fe84fe0dfd30 Definitions produced by packages are now blacklisted.
paulson
parents: 20661
diff changeset
   487
fun is_package_def a =
20823
5480ec4b542d restored the "length of name > 2" check for package definitions
paulson
parents: 20781
diff changeset
   488
   length (NameSpace.unpack a) > 2 andalso 
5480ec4b542d restored the "length of name > 2" check for package definitions
paulson
parents: 20781
diff changeset
   489
   String.isSuffix "_def" a  orelse  String.isSuffix "_defs" a;
20757
fe84fe0dfd30 Definitions produced by packages are now blacklisted.
paulson
parents: 20661
diff changeset
   490
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   491
fun make_banned_test xs = 
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   492
  let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   493
                                (6000, HASH_STRING)
20757
fe84fe0dfd30 Definitions produced by packages are now blacklisted.
paulson
parents: 20661
diff changeset
   494
      fun banned_aux s = 
fe84fe0dfd30 Definitions produced by packages are now blacklisted.
paulson
parents: 20661
diff changeset
   495
            isSome (Polyhash.peek ht s) orelse banned_thmlist s orelse is_package_def s
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   496
      fun banned s = exists banned_aux (delete_numeric_suffix s)
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   497
  in  app (fn x => Polyhash.insert ht (x,())) (!blacklist);
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   498
      app (insert_suffixed_names ht) (!blacklist @ xs); 
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   499
      banned
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   500
  end;
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   501
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   502
(** a hash function from Term.term to int, and also a hash table **)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   503
val xor_words = List.foldl Word.xorb 0w0;
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   504
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   505
fun hashw_term ((Const(c,_)), w) = Polyhash.hashw_string (c,w)
20661
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   506
  | hashw_term ((Free(a,_)), w) = Polyhash.hashw_string (a,w)
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   507
  | hashw_term ((Var(_,_)), w) = w
20661
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   508
  | hashw_term ((Bound i), w) = Polyhash.hashw_int(i,w)
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   509
  | hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   510
  | hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w)));
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   511
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   512
fun hashw_pred (P,w) = 
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   513
    let val (p,args) = strip_comb P
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   514
    in
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   515
	List.foldl hashw_term w (p::args)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   516
    end;
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   517
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   518
fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_pred(P,0w0))
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   519
  | hash_literal P = hashw_pred(P,0w0);
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   520
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   521
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   522
fun get_literals (Const("Trueprop",_)$P) lits = get_literals P lits
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   523
  | get_literals (Const("op |",_)$P$Q) lits = get_literals Q (get_literals P lits)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   524
  | get_literals lit lits = (lit::lits);
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   525
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   526
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   527
fun hash_term t = Word.toIntX (xor_words (map hash_literal (get_literals t [])));
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   528
20661
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   529
(*Versions ONLY for "faking" a theorem name. Here we take variable names into account
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   530
  so that similar theorems don't collide.  FIXME: this entire business of "faking" 
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   531
  theorem names must end!*)
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   532
fun hashw_typ (TVar ((a,i), _), w) = Polyhash.hashw_string (a, Polyhash.hashw_int(i,w))
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   533
  | hashw_typ (TFree (a,_), w) = Polyhash.hashw_string (a,w)
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   534
  | hashw_typ (Type (a, Ts), w) = Polyhash.hashw_string (a, List.foldl hashw_typ w Ts);
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   535
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   536
fun full_hashw_term ((Const(c,T)), w) = Polyhash.hashw_string (c, hashw_typ(T,w))
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   537
  | full_hashw_term ((Free(a,_)), w) = Polyhash.hashw_string (a,w)
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   538
  | full_hashw_term ((Var((a,i),_)), w) = Polyhash.hashw_string (a, Polyhash.hashw_int(i,w))
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   539
  | full_hashw_term ((Bound i), w) = Polyhash.hashw_int(i,w)
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   540
  | full_hashw_term ((Abs(_,T,t)), w) = full_hashw_term (t, hashw_typ(T,w))
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   541
  | full_hashw_term ((P$Q), w) = full_hashw_term (Q, (full_hashw_term (P, w)));
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   542
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   543
fun full_hashw_thm (th,w) = 
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   544
  let val {prop,hyps,...} = rep_thm th
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   545
  in List.foldl full_hashw_term w (prop::hyps) end
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   546
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   547
fun full_hash_thm th = full_hashw_thm (th,0w0);
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   548
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   549
fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   550
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   551
(*Create a hash table for clauses, of the given size*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   552
fun mk_clause_table n =
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   553
      Polyhash.mkTable (hash_term o prop_of, equal_thm)
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   554
                       (n, HASH_CLAUSE);
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   555
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   556
(*Use a hash table to eliminate duplicates from xs. Argument is a list of
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   557
  (name, theorem) pairs, but the theorems are hashed into the table. *)
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   558
fun make_unique xs = 
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   559
  let val ht = mk_clause_table 2200
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   560
  in
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   561
      (app (ignore o Polyhash.peekInsert ht) (map swap xs);  
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   562
       map swap (Polyhash.listItems ht))
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   563
  end;
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   564
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   565
(*FIXME: SLOW!!!*)
20022
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   566
fun mem_thm th [] = false
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   567
  | mem_thm th ((th',_)::thms_names) = equal_thm (th,th') orelse mem_thm th thms_names;
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   568
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   569
(*FIXME: SLOW!!! These two functions are called only by get_relevant_clauses.
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   570
  It would be faster to compare names, rather than theorems, and to use
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   571
  a symbol table or hash table.*)
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   572
fun insert_thms [] thms_names = thms_names
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   573
  | insert_thms ((thm,name)::thms_names) thms_names' =
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   574
      if mem_thm thm thms_names' then insert_thms thms_names thms_names' 
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   575
      else insert_thms thms_names ((thm,name)::thms_names');
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   576
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   577
(* filter axiom clauses, but keep supplied clauses and clauses in whitelist *)
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   578
fun get_relevant_clauses thy cls_thms white_cls goals =
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   579
  insert_thms white_cls (ReduceAxiomsN.relevance_filter thy cls_thms goals);
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   580
20661
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   581
(*This name is cryptic but short. Unlike gensym, we get the same name each time.*)
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   582
fun fake_thm_name th = 
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   583
    Context.theory_name (theory_of_thm th) ^ "." ^ Word.toString (full_hash_thm th);
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   584
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   585
fun put_name_pair ("",th) = (fake_thm_name th, th)
46832fee1215 Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions
paulson
parents: 20643
diff changeset
   586
  | put_name_pair (a,th)  = (a,th);
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   587
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   588
fun display_thms [] = ()
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   589
  | display_thms ((name,thm)::nthms) = 
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   590
      let val nthm = name ^ ": " ^ (string_of_thm thm)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   591
      in Output.debug nthm; display_thms nthms  end;
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   592
 
19894
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   593
fun all_facts_of ctxt =
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   594
  FactIndex.find (ProofContext.fact_index_of ctxt) ([], [])
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   595
  |> maps #2 |> map (`Thm.name_of_thm);
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   596
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   597
(* get lemmas from claset, simpset, atpset and extra supplied rules *)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   598
fun get_clasimp_atp_lemmas ctxt user_thms = 
19894
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   599
  let val included_thms =
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   600
	if !include_all 
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   601
	then (tap (fn ths => Output.debug
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   602
	             ("Including all " ^ Int.toString (length ths) ^ " theorems")) 
19894
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   603
	          (all_facts_of ctxt @ PureThy.all_thms_of (ProofContext.theory_of ctxt)))
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   604
	else 
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   605
	let val claset_thms =
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   606
		if !include_claset then ResAxioms.claset_rules_of_ctxt ctxt
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   607
		else []
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   608
	    val simpset_thms = 
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   609
		if !include_simpset then ResAxioms.simpset_rules_of_ctxt ctxt
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   610
		else []
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   611
	    val atpset_thms =
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   612
		if !include_atpset then ResAxioms.atpset_rules_of_ctxt ctxt
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   613
		else []
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   614
	    val _ = if !Output.show_debug_msgs 
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   615
		    then (Output.debug "ATP theorems: "; display_thms atpset_thms) 
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   616
		    else ()		 
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   617
	in  claset_thms @ simpset_thms @ atpset_thms  end
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   618
      val user_rules = map (put_name_pair o ResAxioms.pairname)
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   619
			   (if null user_thms then !whitelist else user_thms)
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   620
  in
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   621
      (map put_name_pair included_thms, user_rules)
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   622
  end;
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   623
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   624
(*Remove lemmas that are banned from the backlist. Also remove duplicates. *)
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   625
fun blacklist_filter thms = 
19894
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   626
  if !run_blacklist_filter then 
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   627
      let val banned = make_banned_test (map #1 thms)
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   628
	  fun ok (a,_) = not (banned a)
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   629
      in  filter ok thms  end
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   630
  else thms;
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   631
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   632
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   633
(***************************************************************)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   634
(* ATP invocation methods setup                                *)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   635
(***************************************************************)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   636
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   637
fun cnf_hyps_thms ctxt = 
20224
9c40a144ee0e moved basic assumption operations from structure ProofContext to Assumption;
wenzelm
parents: 20131
diff changeset
   638
    let val ths = Assumption.prems_of ctxt
19617
7cb4b67d4b97 avoid raw equality on type thm;
wenzelm
parents: 19490
diff changeset
   639
    in fold (fold (insert Thm.eq_thm) o ResAxioms.skolem_thm) ths [] end;
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   640
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   641
(*Translation mode can be auto-detected, or forced to be first-order or higher-order*)
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   642
datatype mode = Auto | Fol | Hol;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   643
19450
651d949776f8 exported linkup_logic_mode and changed the default setting
paulson
parents: 19445
diff changeset
   644
val linkup_logic_mode = ref Auto;
19205
4ec788c69f82 Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
paulson
parents: 19194
diff changeset
   645
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   646
(*Ensures that no higher-order theorems "leak out"*)
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   647
fun restrict_to_logic logic cls =
20532
64181717e37c made SML/NJ happy;
wenzelm
parents: 20526
diff changeset
   648
  if is_fol_logic logic then filter (Meson.is_fol_term o prop_of o fst) cls 
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   649
	                else cls;
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   650
20131
c89ee2f4efd5 Pass user lemmas' names to ResHolClause.tptp_write_file and dfg_write_file.
mengj
parents: 20022
diff changeset
   651
fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas =
19445
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   652
    if is_fol_logic logic 
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   653
    then ResClause.tptp_write_file goals filename (axioms, classrels, arities)
20131
c89ee2f4efd5 Pass user lemmas' names to ResHolClause.tptp_write_file and dfg_write_file.
mengj
parents: 20022
diff changeset
   654
    else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities) user_lemmas;
19445
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   655
20131
c89ee2f4efd5 Pass user lemmas' names to ResHolClause.tptp_write_file and dfg_write_file.
mengj
parents: 20022
diff changeset
   656
fun dfg_writer logic goals filename (axioms,classrels,arities) user_lemmas =
19445
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   657
    if is_fol_logic logic 
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   658
    then ResClause.dfg_write_file goals filename (axioms, classrels, arities)
20131
c89ee2f4efd5 Pass user lemmas' names to ResHolClause.tptp_write_file and dfg_write_file.
mengj
parents: 20022
diff changeset
   659
    else ResHolClause.dfg_write_file goals filename (axioms, classrels, arities) user_lemmas;
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   660
20022
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   661
(*Called by the oracle-based methods declared in res_atp_methods.ML*)
19722
e7a5b54248bc Added in settings used by "spass" method.
mengj
parents: 19718
diff changeset
   662
fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
19442
ad8bb8346e51 Tidied up some programs.
mengj
parents: 19352
diff changeset
   663
    let val conj_cls = make_clauses conjectures 
20444
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   664
                         |> ResAxioms.assume_abstract_list |> Meson.finish_cnf
19442
ad8bb8346e51 Tidied up some programs.
mengj
parents: 19352
diff changeset
   665
	val hyp_cls = cnf_hyps_thms ctxt
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   666
	val goal_cls = conj_cls@hyp_cls
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   667
	val logic = case mode of 
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   668
                            Auto => problem_logic_goals [map prop_of goal_cls]
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   669
			  | Fol => FOL
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   670
			  | Hol => HOL
19894
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   671
	val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   672
	val cla_simp_atp_clauses = included_thms |> blacklist_filter
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   673
	                             |> make_unique |> ResAxioms.cnf_rules_pairs
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   674
                                     |> restrict_to_logic logic 
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   675
	val user_cls = ResAxioms.cnf_rules_pairs user_rules
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   676
	val thy = ProofContext.theory_of ctxt
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   677
	val axclauses = get_relevant_clauses thy cla_simp_atp_clauses
20022
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   678
	                            user_cls (map prop_of goal_cls)
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   679
	val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol ()
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   680
	val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   681
	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
19722
e7a5b54248bc Added in settings used by "spass" method.
mengj
parents: 19718
diff changeset
   682
        val writer = if dfg then dfg_writer else tptp_writer 
20757
fe84fe0dfd30 Definitions produced by packages are now blacklisted.
paulson
parents: 20661
diff changeset
   683
	and file = atp_input_file()
fe84fe0dfd30 Definitions produced by packages are now blacklisted.
paulson
parents: 20661
diff changeset
   684
	and user_lemmas_names = map #1 user_rules
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   685
    in
20757
fe84fe0dfd30 Definitions produced by packages are now blacklisted.
paulson
parents: 20661
diff changeset
   686
	writer logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
fe84fe0dfd30 Definitions produced by packages are now blacklisted.
paulson
parents: 20661
diff changeset
   687
	Output.debug ("Writing to " ^ file);
fe84fe0dfd30 Definitions produced by packages are now blacklisted.
paulson
parents: 20661
diff changeset
   688
	file
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   689
    end;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   690
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   691
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   692
(**** remove tmp files ****)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   693
fun cond_rm_tmp file = 
19746
9ac97dc14214 warnings to debug outputs
paulson
parents: 19744
diff changeset
   694
    if !keep_atp_input then Output.debug "ATP input kept..." 
9ac97dc14214 warnings to debug outputs
paulson
parents: 19744
diff changeset
   695
    else if !destdir <> "" then Output.debug ("ATP input kept in directory " ^ (!destdir))
9ac97dc14214 warnings to debug outputs
paulson
parents: 19744
diff changeset
   696
    else (Output.debug "deleting ATP inputs..."; OS.FileSys.remove file);
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   697
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   698
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   699
(****** setup ATPs as Isabelle methods ******)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   700
fun atp_meth' tac ths ctxt = 
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   701
    Method.SIMPLE_METHOD' HEADGOAL
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   702
    (tac ctxt ths);
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   703
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   704
fun atp_meth tac ths ctxt = 
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   705
    let val thy = ProofContext.theory_of ctxt
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   706
	val _ = ResClause.init thy
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   707
	val _ = ResHolClause.init thy
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   708
    in
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   709
	atp_meth' tac ths ctxt
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   710
    end;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   711
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   712
fun atp_method tac = Method.thms_ctxt_args (atp_meth tac);
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   713
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   714
(***************************************************************)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   715
(* automatic ATP invocation                                    *)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   716
(***************************************************************)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   717
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   718
(* call prover with settings and problem file for the current subgoal *)
17764
fde495b9e24b improved process handling. tidied
paulson
parents: 17746
diff changeset
   719
fun watcher_call_provers sign sg_terms (childin, childout, pid) =
16802
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
   720
  let
17422
3b237822985d massive tidy-up and simplification
paulson
parents: 17404
diff changeset
   721
    fun make_atp_list [] n = []
17717
7c6a96cbc966 improvements for problem generation
paulson
parents: 17690
diff changeset
   722
      | make_atp_list (sg_term::xs) n =
16802
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
   723
          let
17717
7c6a96cbc966 improvements for problem generation
paulson
parents: 17690
diff changeset
   724
            val probfile = prob_pathname n
17690
8ba7c3cd24a8 time limit option; fixed bug concerning first line of ATP output
paulson
parents: 17525
diff changeset
   725
            val time = Int.toString (!time_limit)
16802
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
   726
          in
18680
677e2bdd75f0 Output.debug;
wenzelm
parents: 18675
diff changeset
   727
            Output.debug ("problem file in watcher_call_provers is " ^ probfile);
17764
fde495b9e24b improved process handling. tidied
paulson
parents: 17746
diff changeset
   728
            (*options are separated by Watcher.setting_sep, currently #"%"*)
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   729
            if !prover = "spass"
16802
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
   730
            then
19445
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   731
              let val spass = helper_path "SPASS_HOME" "SPASS"
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   732
                  val sopts =
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   733
   "-Auto%-SOS=1%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   734
              in 
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   735
                  ("spass", spass, sopts, probfile) :: make_atp_list xs (n+1)
16802
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
   736
              end
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   737
            else if !prover = "vampire"
17235
8e55ad29b690 Added ECommunication.ML and modified res_atp.ML, Reconstruction.thy, and
quigley
parents: 17234
diff changeset
   738
	    then 
17819
1241e5d31d5b small tidy-up of utility functions
paulson
parents: 17775
diff changeset
   739
              let val vampire = helper_path "VAMPIRE_HOME" "vampire"
19445
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   740
                  val casc = if !time_limit > 70 then "--mode casc%" else ""
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   741
                  val vopts = casc ^ "-m 100000%-t " ^ time
16802
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
   742
              in
19445
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   743
                  ("vampire", vampire, vopts, probfile) :: make_atp_list xs (n+1)
16802
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
   744
              end
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   745
      	     else if !prover = "E"
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   746
      	     then
17819
1241e5d31d5b small tidy-up of utility functions
paulson
parents: 17775
diff changeset
   747
	       let val Eprover = helper_path "E_HOME" "eproof"
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   748
	       in
19445
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   749
		  ("E", Eprover, 
19744
73aab222fecb Giving the "--silent" switch to E, to produce less output
paulson
parents: 19722
diff changeset
   750
		     "--tptp-in%-l5%-xAuto%-tAuto%--silent%--cpu-limit=" ^ time, probfile) ::
19445
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   751
		   make_atp_list xs (n+1)
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   752
	       end
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   753
	     else error ("Invalid prover name: " ^ !prover)
16802
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
   754
          end
15452
e2a721567f67 Jia Meng: delta simpsets and clasets
paulson
parents: 15347
diff changeset
   755
17422
3b237822985d massive tidy-up and simplification
paulson
parents: 17404
diff changeset
   756
    val atp_list = make_atp_list sg_terms 1
16802
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
   757
  in
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
   758
    Watcher.callResProvers(childout,atp_list);
18680
677e2bdd75f0 Output.debug;
wenzelm
parents: 18675
diff changeset
   759
    Output.debug "Sent commands to watcher!"
16802
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
   760
  end
20022
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   761
  
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   762
fun trace_array fname =
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   763
  let val path = File.tmp_path (Path.basic fname)
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   764
  in  Array.app (File.append path o (fn s => s ^ "\n"))  end;
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16259
diff changeset
   765
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   766
(*Converting a subgoal into negated conjecture clauses*)
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   767
fun neg_clauses th n =
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   768
  let val tacs = [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac]
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   769
      val st = Seq.hd (EVERY' tacs n th)
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   770
      val negs = Option.valOf (metahyps_thms n st)
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   771
  in make_clauses negs |> ResAxioms.assume_abstract_list |> Meson.finish_cnf end;
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   772
		                       
20022
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   773
(*We write out problem files for each subgoal. Argument probfile generates filenames,
18986
5060ca625e02 tidying
paulson
parents: 18863
diff changeset
   774
  and allows the suppression of the suffix "_1" in problem-generation mode.
5060ca625e02 tidying
paulson
parents: 18863
diff changeset
   775
  FIXME: does not cope with &&, and it isn't easy because one could have multiple
5060ca625e02 tidying
paulson
parents: 18863
diff changeset
   776
  subgoals, each involving &&.*)
20022
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   777
fun write_problem_files probfile (ctxt,th)  =
18753
aa82bd41555d ResClasimp.get_clasimp_lemmas now takes all subgoals rather than only the first
paulson
parents: 18700
diff changeset
   778
  let val goals = Thm.prems_of th
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   779
      val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
17717
7c6a96cbc966 improvements for problem generation
paulson
parents: 17690
diff changeset
   780
      val thy = ProofContext.theory_of ctxt
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   781
      fun get_neg_subgoals [] _ = []
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   782
        | get_neg_subgoals (gl::gls) n = neg_clauses th n :: get_neg_subgoals gls (n+1)
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   783
      val goal_cls = get_neg_subgoals goals 1
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   784
      val logic = case !linkup_logic_mode of
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   785
		Auto => problem_logic_goals (map ((map prop_of)) goal_cls)
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   786
	      | Fol => FOL
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   787
	      | Hol => HOL
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   788
      val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   789
      val included_cls = included_thms |> blacklist_filter
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   790
                                       |> make_unique |> ResAxioms.cnf_rules_pairs 
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   791
                                       |> restrict_to_logic logic 
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   792
      val white_cls = ResAxioms.cnf_rules_pairs white_thms
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   793
      (*clauses relevant to goal gl*)
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   794
      val axcls_list = map (fn gl => get_relevant_clauses thy included_cls white_cls [gl])
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   795
                           goals
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   796
      val _ = Output.debug ("clauses = " ^ Int.toString(length included_cls))
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   797
      val keep_types = if is_fol_logic logic then !ResClause.keep_types 
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   798
                       else is_typed_hol ()
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   799
      val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   800
                             else []
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   801
      val _ = Output.debug ("classrel clauses = " ^ 
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   802
                            Int.toString (length classrel_clauses))
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   803
      val arity_clauses = if keep_types then ResClause.arity_clause_thy thy 
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   804
                          else []
18680
677e2bdd75f0 Output.debug;
wenzelm
parents: 18675
diff changeset
   805
      val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
19718
e709f643c578 Added support for DFG format, used by SPASS.
mengj
parents: 19675
diff changeset
   806
      val writer = if !prover = "spass" then dfg_writer else tptp_writer 
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   807
      fun write_all [] [] _ = []
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   808
	| write_all (ccls::ccls_list) (axcls::axcls_list) k =
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   809
	   (writer logic ccls (probfile k) (axcls,classrel_clauses,arity_clauses) [],
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   810
	    probfile k) 
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   811
	   :: write_all ccls_list axcls_list (k+1)
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   812
      val (clnames::_, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
20022
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   813
      val thm_names = Array.fromList clnames
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   814
      val _ = if !Output.show_debug_msgs 
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   815
              then trace_array "thm_names" thm_names else ()
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   816
  in
20022
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   817
      (filenames, thm_names)
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   818
  end;
15644
f2ef8c258fa4 *** empty log message ***
quigley
parents: 15608
diff changeset
   819
17775
2679ba74411f minor code tidyig
paulson
parents: 17773
diff changeset
   820
val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
2679ba74411f minor code tidyig
paulson
parents: 17773
diff changeset
   821
                                    Posix.Process.pid * string list) option);
2679ba74411f minor code tidyig
paulson
parents: 17773
diff changeset
   822
2679ba74411f minor code tidyig
paulson
parents: 17773
diff changeset
   823
fun kill_last_watcher () =
2679ba74411f minor code tidyig
paulson
parents: 17773
diff changeset
   824
    (case !last_watcher_pid of 
2679ba74411f minor code tidyig
paulson
parents: 17773
diff changeset
   825
         NONE => ()
19445
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   826
       | SOME (_, _, pid, files) => 
18680
677e2bdd75f0 Output.debug;
wenzelm
parents: 18675
diff changeset
   827
	  (Output.debug ("Killing old watcher, pid = " ^ string_of_pid pid);
17775
2679ba74411f minor code tidyig
paulson
parents: 17773
diff changeset
   828
	   Watcher.killWatcher pid;  
2679ba74411f minor code tidyig
paulson
parents: 17773
diff changeset
   829
	   ignore (map (try OS.FileSys.remove) files)))
18680
677e2bdd75f0 Output.debug;
wenzelm
parents: 18675
diff changeset
   830
     handle OS.SysErr _ => Output.debug "Attempt to kill watcher failed";
17525
ae5bb6001afb tidying, and support for axclass/classrel clauses
paulson
parents: 17502
diff changeset
   831
ae5bb6001afb tidying, and support for axclass/classrel clauses
paulson
parents: 17502
diff changeset
   832
(*writes out the current clasimpset to a tptp file;
ae5bb6001afb tidying, and support for axclass/classrel clauses
paulson
parents: 17502
diff changeset
   833
  turns off xsymbol at start of function, restoring it at end    *)
17484
f6a225f97f0a simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents: 17435
diff changeset
   834
val isar_atp = setmp print_mode [] 
17717
7c6a96cbc966 improvements for problem generation
paulson
parents: 17690
diff changeset
   835
 (fn (ctxt, th) =>
7c6a96cbc966 improvements for problem generation
paulson
parents: 17690
diff changeset
   836
  if Thm.no_prems th then ()
16802
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
   837
  else
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
   838
    let
17775
2679ba74411f minor code tidyig
paulson
parents: 17773
diff changeset
   839
      val _ = kill_last_watcher()
19675
a4894fb2a5f2 removing the string array from the result of get_clasimp_atp_lemmas
paulson
parents: 19641
diff changeset
   840
      val (files,thm_names) = write_problem_files prob_pathname (ctxt,th)
a4894fb2a5f2 removing the string array from the result of get_clasimp_atp_lemmas
paulson
parents: 19641
diff changeset
   841
      val (childin, childout, pid) = Watcher.createWatcher (th, thm_names)
15608
f161fa6f8fd5 bug fixes involving typechecking clauses
paulson
parents: 15603
diff changeset
   842
    in
17772
818cec5f82a4 major simplification: removal of the goalstring argument
paulson
parents: 17764
diff changeset
   843
      last_watcher_pid := SOME (childin, childout, pid, files);
18680
677e2bdd75f0 Output.debug;
wenzelm
parents: 18675
diff changeset
   844
      Output.debug ("problem files: " ^ space_implode ", " files); 
677e2bdd75f0 Output.debug;
wenzelm
parents: 18675
diff changeset
   845
      Output.debug ("pid: " ^ string_of_pid pid);
17717
7c6a96cbc966 improvements for problem generation
paulson
parents: 17690
diff changeset
   846
      watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
16802
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
   847
    end);
15608
f161fa6f8fd5 bug fixes involving typechecking clauses
paulson
parents: 15603
diff changeset
   848
17422
3b237822985d massive tidy-up and simplification
paulson
parents: 17404
diff changeset
   849
val isar_atp_writeonly = setmp print_mode [] 
17717
7c6a96cbc966 improvements for problem generation
paulson
parents: 17690
diff changeset
   850
      (fn (ctxt,th) =>
7c6a96cbc966 improvements for problem generation
paulson
parents: 17690
diff changeset
   851
       if Thm.no_prems th then ()
7c6a96cbc966 improvements for problem generation
paulson
parents: 17690
diff changeset
   852
       else 
20022
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   853
         let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix 
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   854
          	            else prob_pathname
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   855
         in ignore (write_problem_files probfile (ctxt,th)) end);
15452
e2a721567f67 Jia Meng: delta simpsets and clasets
paulson
parents: 15347
diff changeset
   856
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16259
diff changeset
   857
16802
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
   858
(** the Isar toplevel hook **)
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
   859
19205
4ec788c69f82 Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
paulson
parents: 19194
diff changeset
   860
fun invoke_atp_ml (ctxt, goal) =
4ec788c69f82 Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
paulson
parents: 19194
diff changeset
   861
  let val thy = ProofContext.theory_of ctxt;
16802
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
   862
  in
18680
677e2bdd75f0 Output.debug;
wenzelm
parents: 18675
diff changeset
   863
    Output.debug ("subgoals in isar_atp:\n" ^ 
19205
4ec788c69f82 Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
paulson
parents: 19194
diff changeset
   864
		  Pretty.string_of (ProofContext.pretty_term ctxt
4ec788c69f82 Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
paulson
parents: 19194
diff changeset
   865
		    (Logic.mk_conjunction_list (Thm.prems_of goal))));
18680
677e2bdd75f0 Output.debug;
wenzelm
parents: 18675
diff changeset
   866
    Output.debug ("current theory: " ^ Context.theory_name thy);
20419
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20372
diff changeset
   867
    inc hook_count;
18680
677e2bdd75f0 Output.debug;
wenzelm
parents: 18675
diff changeset
   868
    Output.debug ("in hook for time: " ^ Int.toString (!hook_count));
16925
0fd7b1438d28 simpler variable names, and no types for monomorphic constants
paulson
parents: 16904
diff changeset
   869
    ResClause.init thy;
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   870
    ResHolClause.init thy;
17690
8ba7c3cd24a8 time limit option; fixed bug concerning first line of ATP output
paulson
parents: 17525
diff changeset
   871
    if !destdir = "" andalso !time_limit > 0 then isar_atp (ctxt, goal)
17502
8836793df947 further tidying; killing of old Watcher loops
paulson
parents: 17488
diff changeset
   872
    else isar_atp_writeonly (ctxt, goal)
19205
4ec788c69f82 Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
paulson
parents: 19194
diff changeset
   873
  end;
4ec788c69f82 Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
paulson
parents: 19194
diff changeset
   874
4ec788c69f82 Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
paulson
parents: 19194
diff changeset
   875
val invoke_atp = Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep
4ec788c69f82 Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
paulson
parents: 19194
diff changeset
   876
 (fn state =>
4ec788c69f82 Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
paulson
parents: 19194
diff changeset
   877
  let val (ctxt, (_, goal)) = Proof.get_goal (Toplevel.proof_of state)
4ec788c69f82 Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
paulson
parents: 19194
diff changeset
   878
  in  invoke_atp_ml (ctxt, goal)  end);
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16259
diff changeset
   879
17091
13593aa6a546 new command to invoke ATPs
paulson
parents: 16955
diff changeset
   880
val call_atpP =
17746
af59c748371d fixed the ascii-armouring of goalstring
paulson
parents: 17717
diff changeset
   881
  OuterSyntax.command 
17091
13593aa6a546 new command to invoke ATPs
paulson
parents: 16955
diff changeset
   882
    "ProofGeneral.call_atp" 
13593aa6a546 new command to invoke ATPs
paulson
parents: 16955
diff changeset
   883
    "call automatic theorem provers" 
13593aa6a546 new command to invoke ATPs
paulson
parents: 16955
diff changeset
   884
    OuterKeyword.diag
19205
4ec788c69f82 Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
paulson
parents: 19194
diff changeset
   885
    (Scan.succeed invoke_atp);
17091
13593aa6a546 new command to invoke ATPs
paulson
parents: 16955
diff changeset
   886
13593aa6a546 new command to invoke ATPs
paulson
parents: 16955
diff changeset
   887
val _ = OuterSyntax.add_parsers [call_atpP];
13593aa6a546 new command to invoke ATPs
paulson
parents: 16955
diff changeset
   888
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
   889
end;