src/HOL/Tools/res_atp.ML
author paulson
Wed, 13 Sep 2006 12:20:21 +0200
changeset 20526 756c4f1fd04c
parent 20457 85414caac94a
child 20532 64181717e37c
permissions -rw-r--r--
Extended the blacklist with higher-order theorems. Restructured. Added checks to ensure that no higher-order clauses are output in first-order mode.
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
val include_combS = ResHolClause.include_combS;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   129
val include_min_comb = ResHolClause.include_min_comb;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   130
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   131
fun atp_input_file () =
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   132
    let val file = !problem_name 
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   133
    in
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   134
	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
   135
	else if File.exists (File.unpack_platform_path (!destdir))
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   136
	then !destdir ^ "/" ^ file
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   137
	else error ("No such directory: " ^ !destdir)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   138
    end;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   139
19894
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   140
val include_all = ref false;
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   141
val include_simpset = ref false;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   142
val include_claset = ref false; 
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   143
val include_atpset = ref true;
20246
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   144
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   145
(*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
   146
fun add_all() = (include_all:=true; ReduceAxiomsN.follow_defs := false);
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   147
fun rm_all() = include_all:=false;
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   148
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   149
fun add_simpset() = include_simpset:=true;
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   150
fun rm_simpset() = include_simpset:=false;
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   151
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   152
fun add_claset() = include_claset:=true;
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   153
fun rm_claset() = include_claset:=false;
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   154
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   155
fun add_clasimp() = (include_simpset:=true;include_claset:=true);
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   156
fun rm_clasimp() = (include_simpset:=false;include_claset:=false);
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   157
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   158
fun add_atpset() = include_atpset:=true;
fdfe7399e057 "all theorems" mode forces definition-expansion off.
paulson
parents: 20224
diff changeset
   159
fun rm_atpset() = include_atpset:=false;
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   160
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   161
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   162
(**** relevance filter ****)
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   163
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
   164
val run_blacklist_filter = ref true;
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   165
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
(* 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
   168
(******************************************************************)
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
datatype logic = FOL | HOL | HOLC | HOLCS;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   171
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   172
fun string_of_logic FOL = "FOL"
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   173
  | string_of_logic HOL = "HOL"
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   174
  | string_of_logic HOLC = "HOLC"
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   175
  | string_of_logic HOLCS = "HOLCS";
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   176
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   177
fun is_fol_logic FOL = true
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   178
  | is_fol_logic  _ = false
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   179
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   180
(*HOLCS will not occur here*)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   181
fun upgrade_lg HOLC _ = HOLC
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   182
  | upgrade_lg HOL HOLC = HOLC
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   183
  | upgrade_lg HOL _ = HOL
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   184
  | upgrade_lg FOL lg = lg; 
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   185
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   186
(* check types *)
19451
c7a25c05986c Changed the logic detection method.
mengj
parents: 19450
diff changeset
   187
fun has_bool_hfn (Type("bool",_)) = true
c7a25c05986c Changed the logic detection method.
mengj
parents: 19450
diff changeset
   188
  | has_bool_hfn (Type("fun",_)) = true
c7a25c05986c Changed the logic detection method.
mengj
parents: 19450
diff changeset
   189
  | has_bool_hfn (Type(_, Ts)) = exists has_bool_hfn Ts
c7a25c05986c Changed the logic detection method.
mengj
parents: 19450
diff changeset
   190
  | has_bool_hfn _ = false;
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   191
19451
c7a25c05986c Changed the logic detection method.
mengj
parents: 19450
diff changeset
   192
fun is_hol_fn tp =
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   193
    let val (targs,tr) = strip_type tp
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   194
    in
19451
c7a25c05986c Changed the logic detection method.
mengj
parents: 19450
diff changeset
   195
	exists (has_bool_hfn) (tr::targs)
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   196
    end;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   197
19451
c7a25c05986c Changed the logic detection method.
mengj
parents: 19450
diff changeset
   198
fun is_hol_pred tp =
c7a25c05986c Changed the logic detection method.
mengj
parents: 19450
diff changeset
   199
    let val (targs,tr) = strip_type tp
c7a25c05986c Changed the logic detection method.
mengj
parents: 19450
diff changeset
   200
    in
c7a25c05986c Changed the logic detection method.
mengj
parents: 19450
diff changeset
   201
	exists (has_bool_hfn) targs
c7a25c05986c Changed the logic detection method.
mengj
parents: 19450
diff changeset
   202
    end;
19194
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
exception FN_LG of term;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   205
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   206
fun fn_lg (t as Const(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 Free(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 Var(f,tp)) (lg,seen) =
19451
c7a25c05986c Changed the logic detection method.
mengj
parents: 19450
diff changeset
   211
    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
   212
  | 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
   213
  | fn_lg f _ = raise FN_LG(f); 
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   214
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   215
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   216
fun term_lg [] (lg,seen) = (lg,seen)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   217
  | term_lg (tm::tms) (FOL,seen) =
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   218
      let val (f,args) = strip_comb tm
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   219
	  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
   220
			    else fn_lg f (FOL,seen)
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   221
      in
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   222
	if is_fol_logic lg' then ()
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   223
        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
   224
        term_lg (args@tms) (lg',seen')
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   225
      end
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   226
  | term_lg _ (lg,seen) = (lg,seen)
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
exception PRED_LG of term;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   229
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   230
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
   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 Free(P,tp)) (lg,seen) =
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   233
      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
   234
  | 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
   235
  | pred_lg P _ = raise PRED_LG(P);
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   236
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   237
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   238
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
   239
  | lit_lg P (lg,seen) =
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   240
      let val (pred,args) = strip_comb P
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   241
	  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
   242
			    else pred_lg pred (lg,seen)
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   243
      in
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   244
	if is_fol_logic lg' then ()
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   245
	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
   246
	term_lg args (lg',seen')
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   247
      end;
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   248
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   249
fun lits_lg [] (lg,seen) = (lg,seen)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   250
  | lits_lg (lit::lits) (FOL,seen) =
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   251
      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
   252
      in
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   253
	if is_fol_logic lg then ()
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   254
	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
   255
	lits_lg lits (lg,seen')
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   256
      end
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   257
  | lits_lg lits (lg,seen) = (lg,seen);
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   258
19227
d15f2baa7ecc Added more functions to the signature and tidied up some functions.
mengj
parents: 19205
diff changeset
   259
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
   260
    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
   261
  | dest_disj_aux t disjs = t::disjs;
d15f2baa7ecc Added more functions to the signature and tidied up some functions.
mengj
parents: 19205
diff changeset
   262
d15f2baa7ecc Added more functions to the signature and tidied up some functions.
mengj
parents: 19205
diff changeset
   263
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
   264
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   265
fun logic_of_clause tm (lg,seen) =
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   266
    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
   267
	val disjs = dest_disj tm'
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   268
    in
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   269
	lits_lg disjs (lg,seen)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   270
    end;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   271
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   272
fun logic_of_clauses [] (lg,seen) = (lg,seen)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   273
  | 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
   274
    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
   275
	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
   276
          if is_fol_logic lg then ()
19746
9ac97dc14214 warnings to debug outputs
paulson
parents: 19744
diff changeset
   277
          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
   278
    in
d15f2baa7ecc Added more functions to the signature and tidied up some functions.
mengj
parents: 19205
diff changeset
   279
	logic_of_clauses clss (lg,seen')
d15f2baa7ecc Added more functions to the signature and tidied up some functions.
mengj
parents: 19205
diff changeset
   280
    end
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   281
  | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen);
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   282
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   283
fun problem_logic_goals_aux [] (lg,seen) = lg
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   284
  | problem_logic_goals_aux (subgoal::subgoals) (lg,seen) = 
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   285
    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
   286
    
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   287
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
   288
19768
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
(* Retrieving and filtering lemmas                             *)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   291
(***************************************************************)
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
(*** white list and black list of lemmas ***)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   294
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   295
(*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
   296
val whitelist = ref [subsetI]; 
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   297
20444
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   298
(*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
   299
  theorem lists is first removed.
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   300
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   301
  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
   302
  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
   303
  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
   304
  an attribute.*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   305
val blacklist = ref
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   306
  ["Datatype.prod.size",
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   307
   "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
   308
   "Datatype.unit.inducts",
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   309
   "Datatype.unit.split_asm", 
20372
e42674e0486e blacklist augmented to block some "unit" theorems that cause unsound resolution proofs
paulson
parents: 20289
diff changeset
   310
   "Datatype.unit.split",
20444
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   311
   "Datatype.unit.splits",
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   312
   "Divides.dvd_0_left_iff",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   313
   "Finite_Set.card_0_eq",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   314
   "Finite_Set.card_infinite",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   315
   "Finite_Set.Max_ge",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   316
   "Finite_Set.Max_in",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   317
   "Finite_Set.Max_le_iff",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   318
   "Finite_Set.Max_less_iff",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   319
   "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
   320
   "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
   321
   "Finite_Set.Min_ge_iff",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   322
   "Finite_Set.Min_gr_iff",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   323
   "Finite_Set.Min_in",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   324
   "Finite_Set.Min_le",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   325
   "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
   326
   "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
   327
   "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
   328
   "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
   329
   "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
   330
   "HOL.split_if_asm",     (*splitting theorem*)
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   331
   "HOL.split_if",         (*splitting theorem*)
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   332
   "IntDef.abs_split",
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   333
   "IntDef.Integ.Abs_Integ_inject",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   334
   "IntDef.Integ.Abs_Integ_inverse",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   335
   "IntDiv.zdvd_0_left",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   336
   "List.append_eq_append_conv",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   337
   "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
   338
   "List.in_listsD",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   339
   "List.in_listsI",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   340
   "List.lists.Cons",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   341
   "List.listsE",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   342
   "Nat.less_one", (*not directional? obscure*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   343
   "Nat.not_gr0",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   344
   "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
   345
   "NatArith.of_nat_0_eq_iff",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   346
   "NatArith.of_nat_eq_0_iff",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   347
   "NatArith.of_nat_le_0_iff",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   348
   "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
   349
   "NatSimprocs.divide_less_0_iff_number_of",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   350
   "NatSimprocs.equation_minus_iff_1",  (*not directional*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   351
   "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
   352
   "NatSimprocs.le_minus_iff_1", (*not directional*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   353
   "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
   354
   "NatSimprocs.less_minus_iff_1", (*not directional*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   355
   "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
   356
   "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
   357
   "NatSimprocs.minus_le_iff_1", (*not directional*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   358
   "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
   359
   "NatSimprocs.minus_less_iff_1", (*not directional*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   360
   "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
   361
   "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
   362
   "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
   363
   "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
   364
   "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
   365
   "NatSimprocs.zero_less_divide_iff_number_of",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   366
   "OrderedGroup.abs_0_eq", (*duplicate by symmetry*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   367
   "OrderedGroup.diff_eq_0_iff_eq", (*prolific?*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   368
   "OrderedGroup.join_0_eq_0",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   369
   "OrderedGroup.meet_0_eq_0",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   370
   "OrderedGroup.pprt_eq_0",   (*obscure*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   371
   "OrderedGroup.pprt_eq_id",   (*obscure*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   372
   "OrderedGroup.pprt_mono",   (*obscure*)
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   373
   "Orderings.split_max",      (*splitting theorem*)
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   374
   "Orderings.split_min",      (*splitting theorem*)
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   375
   "Parity.even_nat_power",   (*obscure, somewhat prolilfic*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   376
   "Parity.power_eq_0_iff_number_of",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   377
   "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
   378
   "Parity.power_less_zero_eq_number_of",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   379
   "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
   380
   "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
   381
   "Power.zero_less_power_abs_iff",
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   382
   "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
   383
   "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
   384
   "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
   385
   "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
   386
   "Product_Type.split_split",                 (*splitting theorem*)
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   387
   "Product_Type.unit_abs_eta_conv",
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   388
   "Product_Type.unit_induct",
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   389
   "Relation.diagI",
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   390
   "Relation.Domain_def",   (*involves an existential quantifier*)
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   391
   "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
   392
   "Relation.ImageI",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   393
   "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
   394
   "Ring_and_Field.divide_cancel_right",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   395
   "Ring_and_Field.divide_divide_eq_left",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   396
   "Ring_and_Field.divide_divide_eq_right",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   397
   "Ring_and_Field.divide_eq_0_iff",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   398
   "Ring_and_Field.divide_eq_1_iff",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   399
   "Ring_and_Field.divide_eq_eq_1",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   400
   "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
   401
   "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
   402
   "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
   403
   "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
   404
   "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
   405
   "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
   406
   "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
   407
   "Ring_and_Field.field_mult_cancel_left",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   408
   "Ring_and_Field.field_mult_cancel_right",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   409
   "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
   410
   "Ring_and_Field.inverse_le_iff_le",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   411
   "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
   412
   "Ring_and_Field.inverse_less_iff_less",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   413
   "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
   414
   "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
   415
   "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
   416
   "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
   417
   "Ring_and_Field.one_eq_divide_iff",  (*duplicate by symmetry*)
20444
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   418
   "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
   419
   "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
   420
   "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
   421
   "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
   422
   "Set.Diff_insert0",
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   423
   "Set.disjoint_insert",
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   424
   "Set.empty_Union_conv",   (*redundant with paramodulation*)
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   425
   "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
   426
   "Set.image_Collect",      (*involves an existential quantifier*)
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   427
   "Set.image_def",          (*involves an existential quantifier*)
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   428
   "Set.insert_disjoint",
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   429
   "Set.Int_UNIV",  (*redundant with paramodulation*)
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   430
   "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
   431
   "Set.Inter_UNIV_conv",
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   432
   "Set.psubsetE",    (*too prolific and obscure*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   433
   "Set.psubsetI",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   434
   "Set.singleton_insert_inj_eq'",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   435
   "Set.singleton_insert_inj_eq",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   436
   "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
   437
   "Set.singletonI",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   438
   "Set.Un_empty", (*redundant with paramodulation*)
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   439
   "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
   440
   "Set.Union_empty_conv", (*redundant with paramodulation*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   441
   "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
   442
   "SetInterval.atLeastAtMost_iff", (*obscure and prolific*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   443
   "SetInterval.atLeastLessThan_iff", (*obscure and prolific*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   444
   "SetInterval.greaterThanAtMost_iff", (*obscure and prolific*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   445
   "SetInterval.greaterThanLessThan_iff", (*obscure and prolific*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   446
   "SetInterval.ivl_subset"];  (*excessive case analysis*)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   447
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   448
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   449
(*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
   450
   "Orderings.max_less_iff_conj", 
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   451
   "Orderings.min_less_iff_conj",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   452
   "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
   453
   "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
   454
Very prolific and somewhat obscure:
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   455
   "Set.InterD",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   456
   "Set.UnionI",
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   457
*)
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
(*** 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
   460
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   461
fun fake_thm_name th = 
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   462
    Context.theory_name (theory_of_thm th) ^ "." ^ gensym"";
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   463
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   464
fun put_name_pair ("",th) = (fake_thm_name th, th)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   465
  | put_name_pair (a,th)  = (a,th);
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   466
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   467
(*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
   468
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   469
exception HASH_CLAUSE and HASH_STRING;
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   470
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   471
(*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
   472
fun insert_suffixed_names ht x = 
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   473
     (Polyhash.insert ht (x^"_iff1", ()); 
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   474
      Polyhash.insert ht (x^"_iff2", ()); 
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   475
      Polyhash.insert ht (x^"_dest", ())); 
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   476
20444
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   477
(*Are all characters in this string digits?*)
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   478
fun all_numeric s = null (String.tokens Char.isDigit s);
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   479
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   480
(*Delete a suffix of the form _\d+*)
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   481
fun delete_numeric_suffix s =
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   482
  case rev (String.fields (fn c => c = #"_") s) of
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   483
      last::rest => 
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   484
          if all_numeric last 
20446
7e616709bca2 String.concatWith (not available in PolyML) replaced by space_implode
webertj
parents: 20444
diff changeset
   485
          then [s, space_implode "_" (rev rest)]
20444
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   486
          else [s]
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   487
    | [] => [s];
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   488
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   489
fun banned_thmlist s =
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   490
  (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
   491
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   492
fun make_banned_test xs = 
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   493
  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
   494
                                (6000, HASH_STRING)
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   495
      fun banned_aux s = isSome (Polyhash.peek ht s) orelse banned_thmlist s
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)
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   506
  | hashw_term ((Free(_,_)), w) = w
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   507
  | hashw_term ((Var(_,_)), w) = w
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   508
  | hashw_term ((Bound _), w) = w
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
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   529
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
   530
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   531
(*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
   532
fun mk_clause_table n =
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   533
      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
   534
                       (n, HASH_CLAUSE);
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   535
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   536
(*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
   537
  (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
   538
fun make_unique xs = 
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   539
  let val ht = mk_clause_table 2200
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   540
  in
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   541
      (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
   542
       map swap (Polyhash.listItems ht))
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   543
  end;
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   544
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   545
(*FIXME: SLOW!!!*)
20022
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   546
fun mem_thm th [] = false
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   547
  | 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
   548
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   549
(*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
   550
  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
   551
  a symbol table or hash table.*)
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   552
fun insert_thms [] thms_names = thms_names
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   553
  | 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
   554
      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
   555
      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
   556
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   557
(* 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
   558
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
   559
  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
   560
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   561
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   562
fun display_thms [] = ()
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   563
  | display_thms ((name,thm)::nthms) = 
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   564
      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
   565
      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
   566
 
19894
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   567
fun all_facts_of ctxt =
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   568
  FactIndex.find (ProofContext.fact_index_of ctxt) ([], [])
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   569
  |> maps #2 |> map (`Thm.name_of_thm);
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   570
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   571
(* 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
   572
fun get_clasimp_atp_lemmas ctxt user_thms = 
19894
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   573
  let val included_thms =
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   574
	if !include_all 
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   575
	then (tap (fn ths => Output.debug
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   576
	             ("Including all " ^ Int.toString (length ths) ^ " theorems")) 
19894
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   577
	          (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
   578
	else 
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   579
	let val claset_thms =
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   580
		if !include_claset then ResAxioms.claset_rules_of_ctxt ctxt
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   581
		else []
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   582
	    val simpset_thms = 
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   583
		if !include_simpset then ResAxioms.simpset_rules_of_ctxt ctxt
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   584
		else []
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   585
	    val atpset_thms =
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   586
		if !include_atpset then ResAxioms.atpset_rules_of_ctxt ctxt
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   587
		else []
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   588
	    val _ = if !Output.show_debug_msgs 
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   589
		    then (Output.debug "ATP theorems: "; display_thms atpset_thms) 
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   590
		    else ()		 
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   591
	in  claset_thms @ simpset_thms @ atpset_thms  end
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   592
      val user_rules = map (put_name_pair o ResAxioms.pairname)
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   593
			   (if null user_thms then !whitelist else user_thms)
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   594
  in
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   595
      (map put_name_pair included_thms, user_rules)
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   596
  end;
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   597
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   598
(*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
   599
fun blacklist_filter thms = 
19894
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   600
  if !run_blacklist_filter then 
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   601
      let val banned = make_banned_test (map #1 thms)
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   602
	  fun ok (a,_) = not (banned a)
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   603
      in  filter ok thms  end
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   604
  else thms;
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   605
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   606
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   607
(***************************************************************)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   608
(* ATP invocation methods setup                                *)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   609
(***************************************************************)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   610
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   611
fun cnf_hyps_thms ctxt = 
20224
9c40a144ee0e moved basic assumption operations from structure ProofContext to Assumption;
wenzelm
parents: 20131
diff changeset
   612
    let val ths = Assumption.prems_of ctxt
19617
7cb4b67d4b97 avoid raw equality on type thm;
wenzelm
parents: 19490
diff changeset
   613
    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
   614
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   615
(*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
   616
datatype mode = Auto | Fol | Hol;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   617
19450
651d949776f8 exported linkup_logic_mode and changed the default setting
paulson
parents: 19445
diff changeset
   618
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
   619
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   620
(*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
   621
fun restrict_to_logic logic cls =
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   622
  if is_fol_logic logic then filter (Meson.is_fol_term o prop_of o #1) cls 
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   623
	                else cls;
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   624
20131
c89ee2f4efd5 Pass user lemmas' names to ResHolClause.tptp_write_file and dfg_write_file.
mengj
parents: 20022
diff changeset
   625
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
   626
    if is_fol_logic logic 
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   627
    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
   628
    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
   629
20131
c89ee2f4efd5 Pass user lemmas' names to ResHolClause.tptp_write_file and dfg_write_file.
mengj
parents: 20022
diff changeset
   630
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
   631
    if is_fol_logic logic 
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   632
    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
   633
    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
   634
20022
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   635
(*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
   636
fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
19442
ad8bb8346e51 Tidied up some programs.
mengj
parents: 19352
diff changeset
   637
    let val conj_cls = make_clauses conjectures 
20444
6c5e38a73db0 blacklist now handles thm lists
paulson
parents: 20423
diff changeset
   638
                         |> ResAxioms.assume_abstract_list |> Meson.finish_cnf
19442
ad8bb8346e51 Tidied up some programs.
mengj
parents: 19352
diff changeset
   639
	val hyp_cls = cnf_hyps_thms ctxt
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   640
	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
   641
	val logic = case mode of 
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   642
                            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
   643
			  | Fol => FOL
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   644
			  | Hol => HOL
19894
7c7e15b27145 the "all_theorems" option and some fixes
paulson
parents: 19768
diff changeset
   645
	val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
20131
c89ee2f4efd5 Pass user lemmas' names to ResHolClause.tptp_write_file and dfg_write_file.
mengj
parents: 20022
diff changeset
   646
	val user_lemmas_names = map #1 user_rules
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   647
	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
   648
	                             |> make_unique |> ResAxioms.cnf_rules_pairs
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   649
                                     |> restrict_to_logic logic 
19768
9afd9b9c47d0 ATP/res_clasimpset.ML has been merged into res_atp.ML.
mengj
parents: 19746
diff changeset
   650
	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
   651
	val thy = ProofContext.theory_of ctxt
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   652
	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
   653
	                            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
   654
	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
   655
	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
   656
	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
   657
        val writer = if dfg then dfg_writer else tptp_writer 
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   658
	val file = atp_input_file()
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   659
    in
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   660
	(writer logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
19746
9ac97dc14214 warnings to debug outputs
paulson
parents: 19744
diff changeset
   661
	 Output.debug ("Writing to " ^ file);
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   662
	 file)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   663
    end;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   664
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   665
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   666
(**** remove tmp files ****)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   667
fun cond_rm_tmp file = 
19746
9ac97dc14214 warnings to debug outputs
paulson
parents: 19744
diff changeset
   668
    if !keep_atp_input then Output.debug "ATP input kept..." 
9ac97dc14214 warnings to debug outputs
paulson
parents: 19744
diff changeset
   669
    else if !destdir <> "" then Output.debug ("ATP input kept in directory " ^ (!destdir))
9ac97dc14214 warnings to debug outputs
paulson
parents: 19744
diff changeset
   670
    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
   671
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   672
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   673
(****** setup ATPs as Isabelle methods ******)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   674
fun atp_meth' tac ths ctxt = 
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   675
    Method.SIMPLE_METHOD' HEADGOAL
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   676
    (tac ctxt ths);
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   677
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   678
fun atp_meth tac ths ctxt = 
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   679
    let val thy = ProofContext.theory_of ctxt
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   680
	val _ = ResClause.init thy
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   681
	val _ = ResHolClause.init thy
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   682
    in
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   683
	atp_meth' tac ths ctxt
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   684
    end;
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   685
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   686
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
   687
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   688
(***************************************************************)
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   689
(* automatic ATP invocation                                    *)
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
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   692
(* call prover with settings and problem file for the current subgoal *)
17764
fde495b9e24b improved process handling. tidied
paulson
parents: 17746
diff changeset
   693
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
   694
  let
17422
3b237822985d massive tidy-up and simplification
paulson
parents: 17404
diff changeset
   695
    fun make_atp_list [] n = []
17717
7c6a96cbc966 improvements for problem generation
paulson
parents: 17690
diff changeset
   696
      | 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
   697
          let
17717
7c6a96cbc966 improvements for problem generation
paulson
parents: 17690
diff changeset
   698
            val probfile = prob_pathname n
17690
8ba7c3cd24a8 time limit option; fixed bug concerning first line of ATP output
paulson
parents: 17525
diff changeset
   699
            val time = Int.toString (!time_limit)
16802
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
   700
          in
18680
677e2bdd75f0 Output.debug;
wenzelm
parents: 18675
diff changeset
   701
            Output.debug ("problem file in watcher_call_provers is " ^ probfile);
17764
fde495b9e24b improved process handling. tidied
paulson
parents: 17746
diff changeset
   702
            (*options are separated by Watcher.setting_sep, currently #"%"*)
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   703
            if !prover = "spass"
16802
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
   704
            then
19445
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   705
              let val spass = helper_path "SPASS_HOME" "SPASS"
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   706
                  val sopts =
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   707
   "-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
   708
              in 
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   709
                  ("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
   710
              end
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   711
            else if !prover = "vampire"
17235
8e55ad29b690 Added ECommunication.ML and modified res_atp.ML, Reconstruction.thy, and
quigley
parents: 17234
diff changeset
   712
	    then 
17819
1241e5d31d5b small tidy-up of utility functions
paulson
parents: 17775
diff changeset
   713
              let val vampire = helper_path "VAMPIRE_HOME" "vampire"
19445
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   714
                  val casc = if !time_limit > 70 then "--mode casc%" else ""
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   715
                  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
   716
              in
19445
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   717
                  ("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
   718
              end
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   719
      	     else if !prover = "E"
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   720
      	     then
17819
1241e5d31d5b small tidy-up of utility functions
paulson
parents: 17775
diff changeset
   721
	       let val Eprover = helper_path "E_HOME" "eproof"
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   722
	       in
19445
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   723
		  ("E", Eprover, 
19744
73aab222fecb Giving the "--silent" switch to E, to produce less output
paulson
parents: 19722
diff changeset
   724
		     "--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
   725
		   make_atp_list xs (n+1)
17306
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   726
	       end
5cde710a8a23 Progress on eprover linkup, also massive tidying
paulson
parents: 17305
diff changeset
   727
	     else error ("Invalid prover name: " ^ !prover)
16802
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
   728
          end
15452
e2a721567f67 Jia Meng: delta simpsets and clasets
paulson
parents: 15347
diff changeset
   729
17422
3b237822985d massive tidy-up and simplification
paulson
parents: 17404
diff changeset
   730
    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
   731
  in
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
   732
    Watcher.callResProvers(childout,atp_list);
18680
677e2bdd75f0 Output.debug;
wenzelm
parents: 18675
diff changeset
   733
    Output.debug "Sent commands to watcher!"
16802
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
   734
  end
20022
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   735
  
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   736
fun trace_array fname =
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   737
  let val path = File.tmp_path (Path.basic fname)
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   738
  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
   739
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   740
(*Converting a subgoal into negated conjecture clauses*)
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   741
fun neg_clauses th n =
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   742
  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
   743
      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
   744
      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
   745
  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
   746
		                       
20022
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   747
(*We write out problem files for each subgoal. Argument probfile generates filenames,
18986
5060ca625e02 tidying
paulson
parents: 18863
diff changeset
   748
  and allows the suppression of the suffix "_1" in problem-generation mode.
5060ca625e02 tidying
paulson
parents: 18863
diff changeset
   749
  FIXME: does not cope with &&, and it isn't easy because one could have multiple
5060ca625e02 tidying
paulson
parents: 18863
diff changeset
   750
  subgoals, each involving &&.*)
20022
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   751
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
   752
  let val goals = Thm.prems_of th
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   753
      val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
17717
7c6a96cbc966 improvements for problem generation
paulson
parents: 17690
diff changeset
   754
      val thy = ProofContext.theory_of ctxt
20457
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   755
      fun get_neg_subgoals [] _ = []
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   756
        | 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
   757
      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
   758
      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
   759
		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
   760
	      | Fol => FOL
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   761
	      | Hol => HOL
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   762
      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
   763
      val included_cls = included_thms |> blacklist_filter
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   764
                                       |> make_unique |> ResAxioms.cnf_rules_pairs 
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   765
                                       |> restrict_to_logic logic 
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   766
      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
   767
      (*clauses relevant to goal gl*)
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   768
      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
   769
                           goals
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   770
      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
   771
      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
   772
                       else is_typed_hol ()
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   773
      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
   774
                             else []
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   775
      val _ = Output.debug ("classrel clauses = " ^ 
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   776
                            Int.toString (length classrel_clauses))
85414caac94a refinements to conversion into clause form, esp for the HO case
paulson
parents: 20446
diff changeset
   777
      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
   778
                          else []
18680
677e2bdd75f0 Output.debug;
wenzelm
parents: 18675
diff changeset
   779
      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
   780
      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
   781
      fun write_all [] [] _ = []
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   782
	| 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
   783
	   (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
   784
	    probfile k) 
20526
756c4f1fd04c Extended the blacklist with higher-order theorems. Restructured. Added checks to
paulson
parents: 20457
diff changeset
   785
	   :: 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
   786
      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
   787
      val thm_names = Array.fromList clnames
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   788
      val _ = if !Output.show_debug_msgs 
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   789
              then trace_array "thm_names" thm_names else ()
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   790
  in
20022
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   791
      (filenames, thm_names)
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   792
  end;
15644
f2ef8c258fa4 *** empty log message ***
quigley
parents: 15608
diff changeset
   793
17775
2679ba74411f minor code tidyig
paulson
parents: 17773
diff changeset
   794
val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
2679ba74411f minor code tidyig
paulson
parents: 17773
diff changeset
   795
                                    Posix.Process.pid * string list) option);
2679ba74411f minor code tidyig
paulson
parents: 17773
diff changeset
   796
2679ba74411f minor code tidyig
paulson
parents: 17773
diff changeset
   797
fun kill_last_watcher () =
2679ba74411f minor code tidyig
paulson
parents: 17773
diff changeset
   798
    (case !last_watcher_pid of 
2679ba74411f minor code tidyig
paulson
parents: 17773
diff changeset
   799
         NONE => ()
19445
da75577642a9 tidying; ATP options including CASC mode for Vampire
paulson
parents: 19442
diff changeset
   800
       | SOME (_, _, pid, files) => 
18680
677e2bdd75f0 Output.debug;
wenzelm
parents: 18675
diff changeset
   801
	  (Output.debug ("Killing old watcher, pid = " ^ string_of_pid pid);
17775
2679ba74411f minor code tidyig
paulson
parents: 17773
diff changeset
   802
	   Watcher.killWatcher pid;  
2679ba74411f minor code tidyig
paulson
parents: 17773
diff changeset
   803
	   ignore (map (try OS.FileSys.remove) files)))
18680
677e2bdd75f0 Output.debug;
wenzelm
parents: 18675
diff changeset
   804
     handle OS.SysErr _ => Output.debug "Attempt to kill watcher failed";
17525
ae5bb6001afb tidying, and support for axclass/classrel clauses
paulson
parents: 17502
diff changeset
   805
ae5bb6001afb tidying, and support for axclass/classrel clauses
paulson
parents: 17502
diff changeset
   806
(*writes out the current clasimpset to a tptp file;
ae5bb6001afb tidying, and support for axclass/classrel clauses
paulson
parents: 17502
diff changeset
   807
  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
   808
val isar_atp = setmp print_mode [] 
17717
7c6a96cbc966 improvements for problem generation
paulson
parents: 17690
diff changeset
   809
 (fn (ctxt, th) =>
7c6a96cbc966 improvements for problem generation
paulson
parents: 17690
diff changeset
   810
  if Thm.no_prems th then ()
16802
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
   811
  else
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
   812
    let
17775
2679ba74411f minor code tidyig
paulson
parents: 17773
diff changeset
   813
      val _ = kill_last_watcher()
19675
a4894fb2a5f2 removing the string array from the result of get_clasimp_atp_lemmas
paulson
parents: 19641
diff changeset
   814
      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
   815
      val (childin, childout, pid) = Watcher.createWatcher (th, thm_names)
15608
f161fa6f8fd5 bug fixes involving typechecking clauses
paulson
parents: 15603
diff changeset
   816
    in
17772
818cec5f82a4 major simplification: removal of the goalstring argument
paulson
parents: 17764
diff changeset
   817
      last_watcher_pid := SOME (childin, childout, pid, files);
18680
677e2bdd75f0 Output.debug;
wenzelm
parents: 18675
diff changeset
   818
      Output.debug ("problem files: " ^ space_implode ", " files); 
677e2bdd75f0 Output.debug;
wenzelm
parents: 18675
diff changeset
   819
      Output.debug ("pid: " ^ string_of_pid pid);
17717
7c6a96cbc966 improvements for problem generation
paulson
parents: 17690
diff changeset
   820
      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
   821
    end);
15608
f161fa6f8fd5 bug fixes involving typechecking clauses
paulson
parents: 15603
diff changeset
   822
17422
3b237822985d massive tidy-up and simplification
paulson
parents: 17404
diff changeset
   823
val isar_atp_writeonly = setmp print_mode [] 
17717
7c6a96cbc966 improvements for problem generation
paulson
parents: 17690
diff changeset
   824
      (fn (ctxt,th) =>
7c6a96cbc966 improvements for problem generation
paulson
parents: 17690
diff changeset
   825
       if Thm.no_prems th then ()
7c6a96cbc966 improvements for problem generation
paulson
parents: 17690
diff changeset
   826
       else 
20022
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   827
         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
   828
          	            else prob_pathname
b07a138b4e7d some tidying; fixed the output of theorem names
paulson
parents: 19894
diff changeset
   829
         in ignore (write_problem_files probfile (ctxt,th)) end);
15452
e2a721567f67 Jia Meng: delta simpsets and clasets
paulson
parents: 15347
diff changeset
   830
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16259
diff changeset
   831
16802
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
   832
(** the Isar toplevel hook **)
6eeee59dac4c use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
wenzelm
parents: 16767
diff changeset
   833
19205
4ec788c69f82 Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
paulson
parents: 19194
diff changeset
   834
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
   835
  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
   836
  in
18680
677e2bdd75f0 Output.debug;
wenzelm
parents: 18675
diff changeset
   837
    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
   838
		  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
   839
		    (Logic.mk_conjunction_list (Thm.prems_of goal))));
18680
677e2bdd75f0 Output.debug;
wenzelm
parents: 18675
diff changeset
   840
    Output.debug ("current theory: " ^ Context.theory_name thy);
20419
df257a9cf0e9 abstraction of lambda-expressions
paulson
parents: 20372
diff changeset
   841
    inc hook_count;
18680
677e2bdd75f0 Output.debug;
wenzelm
parents: 18675
diff changeset
   842
    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
   843
    ResClause.init thy;
19194
7681c04d8bff Merged res_atp_setup.ML into res_atp.ML.
mengj
parents: 18986
diff changeset
   844
    ResHolClause.init thy;
17690
8ba7c3cd24a8 time limit option; fixed bug concerning first line of ATP output
paulson
parents: 17525
diff changeset
   845
    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
   846
    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
   847
  end;
4ec788c69f82 Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
paulson
parents: 19194
diff changeset
   848
4ec788c69f82 Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
paulson
parents: 19194
diff changeset
   849
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
   850
 (fn state =>
4ec788c69f82 Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
paulson
parents: 19194
diff changeset
   851
  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
   852
  in  invoke_atp_ml (ctxt, goal)  end);
16357
f1275d2a1dee All subgoals sent to the watcher at once now.
quigley
parents: 16259
diff changeset
   853
17091
13593aa6a546 new command to invoke ATPs
paulson
parents: 16955
diff changeset
   854
val call_atpP =
17746
af59c748371d fixed the ascii-armouring of goalstring
paulson
parents: 17717
diff changeset
   855
  OuterSyntax.command 
17091
13593aa6a546 new command to invoke ATPs
paulson
parents: 16955
diff changeset
   856
    "ProofGeneral.call_atp" 
13593aa6a546 new command to invoke ATPs
paulson
parents: 16955
diff changeset
   857
    "call automatic theorem provers" 
13593aa6a546 new command to invoke ATPs
paulson
parents: 16955
diff changeset
   858
    OuterKeyword.diag
19205
4ec788c69f82 Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
paulson
parents: 19194
diff changeset
   859
    (Scan.succeed invoke_atp);
17091
13593aa6a546 new command to invoke ATPs
paulson
parents: 16955
diff changeset
   860
13593aa6a546 new command to invoke ATPs
paulson
parents: 16955
diff changeset
   861
val _ = OuterSyntax.add_parsers [call_atpP];
13593aa6a546 new command to invoke ATPs
paulson
parents: 16955
diff changeset
   862
15347
14585bc8fa09 resolution package tools by Jia Meng
paulson
parents:
diff changeset
   863
end;