src/HOL/Tools/res_atp.ML
changeset 20457 85414caac94a
parent 20446 7e616709bca2
child 20526 756c4f1fd04c
     1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Sep 01 08:36:55 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Sep 01 08:51:53 2006 +0200
     1.3 @@ -5,6 +5,7 @@
     1.4  ATPs with TPTP format input.
     1.5  *)
     1.6  
     1.7 +(*FIXME: Do we need this signature?*)
     1.8  signature RES_ATP =
     1.9  sig
    1.10    val prover: string ref
    1.11 @@ -52,7 +53,7 @@
    1.12    val rm_clasimp : unit -> unit
    1.13  end;
    1.14  
    1.15 -structure ResAtp : RES_ATP =
    1.16 +structure ResAtp =
    1.17  struct
    1.18  
    1.19  (********************************************************************)
    1.20 @@ -159,7 +160,7 @@
    1.21  
    1.22  
    1.23  (**** relevance filter ****)
    1.24 -val run_relevance_filter = ref true;
    1.25 +val run_relevance_filter = ReduceAxiomsN.run_relevance_filter;
    1.26  val run_blacklist_filter = ref true;
    1.27  
    1.28  (******************************************************************)
    1.29 @@ -173,11 +174,9 @@
    1.30    | string_of_logic HOLC = "HOLC"
    1.31    | string_of_logic HOLCS = "HOLCS";
    1.32  
    1.33 -
    1.34  fun is_fol_logic FOL = true
    1.35    | is_fol_logic  _ = false
    1.36  
    1.37 -
    1.38  (*HOLCS will not occur here*)
    1.39  fun upgrade_lg HOLC _ = HOLC
    1.40    | upgrade_lg HOL HOLC = HOLC
    1.41 @@ -216,51 +215,47 @@
    1.42  
    1.43  fun term_lg [] (lg,seen) = (lg,seen)
    1.44    | term_lg (tm::tms) (FOL,seen) =
    1.45 -    let val (f,args) = strip_comb tm
    1.46 -	val (lg',seen') = if f mem seen then (FOL,seen) 
    1.47 -			  else fn_lg f (FOL,seen)
    1.48 -	val _ =
    1.49 -          if is_fol_logic lg' then ()
    1.50 -          else Output.debug ("Found a HOL term: " ^ Display.raw_string_of_term f)
    1.51 -	 in
    1.52 -	     term_lg (args@tms) (lg',seen')
    1.53 -    end
    1.54 +      let val (f,args) = strip_comb tm
    1.55 +	  val (lg',seen') = if f mem seen then (FOL,seen) 
    1.56 +			    else fn_lg f (FOL,seen)
    1.57 +      in
    1.58 +	if is_fol_logic lg' then ()
    1.59 +        else Output.debug ("Found a HOL term: " ^ Display.raw_string_of_term f);
    1.60 +        term_lg (args@tms) (lg',seen')
    1.61 +      end
    1.62    | term_lg _ (lg,seen) = (lg,seen)
    1.63  
    1.64  exception PRED_LG of term;
    1.65  
    1.66  fun pred_lg (t as Const(P,tp)) (lg,seen)= 
    1.67 -    if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) 
    1.68 +      if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) 
    1.69    | pred_lg (t as Free(P,tp)) (lg,seen) =
    1.70 -    if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen)
    1.71 +      if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen)
    1.72    | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, t ins seen)
    1.73    | pred_lg P _ = raise PRED_LG(P);
    1.74  
    1.75  
    1.76  fun lit_lg (Const("Not",_) $ P) (lg,seen) = lit_lg P (lg,seen)
    1.77    | lit_lg P (lg,seen) =
    1.78 -    let val (pred,args) = strip_comb P
    1.79 -	val (lg',seen') = if pred mem seen then (lg,seen) 
    1.80 -			  else pred_lg pred (lg,seen)
    1.81 -	val _ =
    1.82 -          if is_fol_logic lg' then ()
    1.83 -          else Output.debug ("Found a HOL predicate: " ^ Display.raw_string_of_term pred)
    1.84 -    in
    1.85 +      let val (pred,args) = strip_comb P
    1.86 +	  val (lg',seen') = if pred mem seen then (lg,seen) 
    1.87 +			    else pred_lg pred (lg,seen)
    1.88 +      in
    1.89 +	if is_fol_logic lg' then ()
    1.90 +	else Output.debug ("Found a HOL predicate: " ^ Display.raw_string_of_term pred);
    1.91  	term_lg args (lg',seen')
    1.92 -    end;
    1.93 +      end;
    1.94  
    1.95  fun lits_lg [] (lg,seen) = (lg,seen)
    1.96    | lits_lg (lit::lits) (FOL,seen) =
    1.97 -    let val (lg,seen') = lit_lg lit (FOL,seen)
    1.98 -	val _ =
    1.99 -          if is_fol_logic lg then ()
   1.100 -          else Output.debug ("Found a HOL literal: " ^ Display.raw_string_of_term lit)
   1.101 -    in
   1.102 +      let val (lg,seen') = lit_lg lit (FOL,seen)
   1.103 +      in
   1.104 +	if is_fol_logic lg then ()
   1.105 +	else Output.debug ("Found a HOL literal: " ^ Display.raw_string_of_term lit);
   1.106  	lits_lg lits (lg,seen')
   1.107 -    end
   1.108 +      end
   1.109    | lits_lg lits (lg,seen) = (lg,seen);
   1.110  
   1.111 -
   1.112  fun dest_disj_aux (Const ("op |", _) $ t $ t') disjs = 
   1.113      dest_disj_aux t (dest_disj_aux t' disjs)
   1.114    | dest_disj_aux t disjs = t::disjs;
   1.115 @@ -314,11 +309,10 @@
   1.116     "Datatype.unit.inducts",
   1.117     "Datatype.unit.split",
   1.118     "Datatype.unit.splits",
   1.119 -   "Product_Type.unit_abs_eta_conv",
   1.120 -   "Product_Type.unit_induct",
   1.121 +   "Datatype.prod.size",
   1.122  
   1.123 -   "Datatype.prod.size",
   1.124     "Divides.dvd_0_left_iff",
   1.125 +
   1.126     "Finite_Set.card_0_eq",
   1.127     "Finite_Set.card_infinite",
   1.128     "Finite_Set.Max_ge",
   1.129 @@ -335,15 +329,22 @@
   1.130     "Finite_Set.min_max.below_inf_sup_Inf_Sup.sup_Inf_absorb", 
   1.131     "Finite_Set.min.f_below_strict_below.below_f_conv",        (*duplicates in Orderings.*)
   1.132     "Finite_Set.min.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
   1.133 +   
   1.134 +   "HOL.split_if",         (*splitting theorem*)
   1.135 +   "HOL.split_if_asm",     (*splitting theorem*)
   1.136 +
   1.137     "IntDef.Integ.Abs_Integ_inject",
   1.138     "IntDef.Integ.Abs_Integ_inverse",
   1.139 +   "IntDef.abs_split",
   1.140     "IntDiv.zdvd_0_left",
   1.141 +   
   1.142     "List.append_eq_append_conv",
   1.143     "List.hd_Cons_tl",   (*Says everything is [] or Cons. Probably prolific.*)
   1.144     "List.in_listsD",
   1.145     "List.in_listsI",
   1.146     "List.lists.Cons",
   1.147     "List.listsE",
   1.148 +
   1.149     "Nat.less_one", (*not directional? obscure*)
   1.150     "Nat.not_gr0",
   1.151     "Nat.one_eq_mult_iff", (*duplicate by symmetry*)
   1.152 @@ -368,6 +369,7 @@
   1.153     "NatSimprocs.mult_less_cancel_right_number_of", (*excessive case analysis*)
   1.154     "NatSimprocs.zero_le_divide_iff_number_of", (*excessive case analysis*)
   1.155     "NatSimprocs.zero_less_divide_iff_number_of",
   1.156 +
   1.157     "OrderedGroup.abs_0_eq", (*duplicate by symmetry*)
   1.158     "OrderedGroup.diff_eq_0_iff_eq", (*prolific?*)
   1.159     "OrderedGroup.join_0_eq_0",
   1.160 @@ -375,6 +377,9 @@
   1.161     "OrderedGroup.pprt_eq_0",   (*obscure*)
   1.162     "OrderedGroup.pprt_eq_id",   (*obscure*)
   1.163     "OrderedGroup.pprt_mono",   (*obscure*)
   1.164 +   "Orderings.split_min",      (*splitting theorem*)
   1.165 +   "Orderings.split_max",      (*splitting theorem*)
   1.166 +
   1.167     "Parity.even_nat_power",   (*obscure, somewhat prolilfic*)
   1.168     "Parity.power_eq_0_iff_number_of",
   1.169     "Parity.power_le_zero_eq_number_of",   (*obscure and prolific*)
   1.170 @@ -382,6 +387,14 @@
   1.171     "Parity.zero_le_power_eq_number_of",   (*obscure and prolific*)
   1.172     "Parity.zero_less_power_eq_number_of",   (*obscure and prolific*)
   1.173     "Power.zero_less_power_abs_iff",
   1.174 +   "Product_Type.unit_abs_eta_conv",
   1.175 +   "Product_Type.unit_induct",
   1.176 +
   1.177 +   "Product_Type.split_paired_Ball_Sigma",     (*splitting theorem*)
   1.178 +   "Product_Type.split_paired_Bex_Sigma",      (*splitting theorem*)
   1.179 +   "Product_Type.split_split",                 (*splitting theorem*)
   1.180 +   "Product_Type.split_split_asm",             (*splitting theorem*)
   1.181 +
   1.182     "Relation.diagI",
   1.183     "Relation.ImageI",
   1.184     "Ring_and_Field.divide_cancel_left", (*fields are seldom used & often prolific*)
   1.185 @@ -446,18 +459,8 @@
   1.186  
   1.187  (*** retrieve lemmas from clasimpset and atpset, may filter them ***)
   1.188  
   1.189 -(*The "name" of a theorem is its statement, if nothing else is available.*)
   1.190 -val plain_string_of_thm =
   1.191 -    setmp show_question_marks false 
   1.192 -      (setmp print_mode [] 
   1.193 -	(Pretty.setmp_margin 999 string_of_thm));
   1.194 -	
   1.195 -(*Returns the first substring enclosed in quotation marks, typically omitting 
   1.196 -  the [.] of meta-level assumptions.*)
   1.197 -val firstquoted = hd o (String.tokens (fn c => c = #"\""))
   1.198 -	
   1.199  fun fake_thm_name th = 
   1.200 -    Context.theory_name (theory_of_thm th) ^ "." ^ firstquoted (plain_string_of_thm th);
   1.201 +    Context.theory_name (theory_of_thm th) ^ "." ^ gensym"";
   1.202  
   1.203  fun put_name_pair ("",th) = (fake_thm_name th, th)
   1.204    | put_name_pair (a,th)  = (a,th);
   1.205 @@ -484,11 +487,14 @@
   1.206            else [s]
   1.207      | [] => [s];
   1.208  
   1.209 +fun banned_thmlist s =
   1.210 +  (Sign.base_name s) mem_string ["induct","inducts","split","splits","split_asm"];
   1.211 +
   1.212  fun make_banned_test xs = 
   1.213    let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)
   1.214                                  (6000, HASH_STRING)
   1.215 -      fun banned s = exists (fn s' => isSome (Polyhash.peek ht s')) 
   1.216 -                            (delete_numeric_suffix s)
   1.217 +      fun banned_aux s = isSome (Polyhash.peek ht s) orelse banned_thmlist s
   1.218 +      fun banned s = exists banned_aux (delete_numeric_suffix s)
   1.219    in  app (fn x => Polyhash.insert ht (x,())) (!blacklist);
   1.220        app (insert_suffixed_names ht) (!blacklist @ xs); 
   1.221        banned
   1.222 @@ -519,28 +525,41 @@
   1.223    | get_literals lit lits = (lit::lits);
   1.224  
   1.225  
   1.226 -fun hash_term term = Word.toIntX (xor_words (map hash_literal (get_literals term [])));
   1.227 -
   1.228 -fun hash_thm  thm = hash_term (prop_of thm);
   1.229 +fun hash_term t = Word.toIntX (xor_words (map hash_literal (get_literals t [])));
   1.230  
   1.231  fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);
   1.232 +
   1.233  (*Create a hash table for clauses, of the given size*)
   1.234  fun mk_clause_table n =
   1.235 -      Polyhash.mkTable (hash_thm, equal_thm)
   1.236 +      Polyhash.mkTable (hash_term o prop_of, equal_thm)
   1.237                         (n, HASH_CLAUSE);
   1.238  
   1.239 -(*Use a hash table to eliminate duplicates from xs*)
   1.240 -fun make_unique ht xs = 
   1.241 -      (app (ignore o Polyhash.peekInsert ht) xs;  Polyhash.listItems ht);
   1.242 +(*Use a hash table to eliminate duplicates from xs. Argument is a list of
   1.243 +  (name, theorem) pairs, but the theorems are hashed into the table. *)
   1.244 +fun make_unique xs = 
   1.245 +  let val ht = mk_clause_table 2200
   1.246 +  in
   1.247 +      (app (ignore o Polyhash.peekInsert ht) (map swap xs);  
   1.248 +       map swap (Polyhash.listItems ht))
   1.249 +  end;
   1.250  
   1.251 +(*FIXME: SLOW!!!*)
   1.252  fun mem_thm th [] = false
   1.253    | mem_thm th ((th',_)::thms_names) = equal_thm (th,th') orelse mem_thm th thms_names;
   1.254  
   1.255 +(*FIXME: SLOW!!! These two functions are called only by get_relevant_clauses.
   1.256 +  It would be faster to compare names, rather than theorems, and to use
   1.257 +  a symbol table or hash table.*)
   1.258  fun insert_thms [] thms_names = thms_names
   1.259    | insert_thms ((thm,name)::thms_names) thms_names' =
   1.260        if mem_thm thm thms_names' then insert_thms thms_names thms_names' 
   1.261        else insert_thms thms_names ((thm,name)::thms_names');
   1.262  
   1.263 +(* filter axiom clauses, but keep supplied clauses and clauses in whitelist *)
   1.264 +fun get_relevant_clauses thy cls_thms white_cls goals =
   1.265 +  insert_thms white_cls (ReduceAxiomsN.relevance_filter thy cls_thms goals);
   1.266 +
   1.267 +
   1.268  fun display_thms [] = ()
   1.269    | display_thms ((name,thm)::nthms) = 
   1.270        let val nthm = name ^ ": " ^ (string_of_thm thm)
   1.271 @@ -555,8 +574,8 @@
   1.272  fun get_clasimp_atp_lemmas ctxt user_thms = 
   1.273    let val included_thms =
   1.274  	if !include_all 
   1.275 -	then (tap (fn ths => Output.debug ("Including all " ^ Int.toString (length ths) ^
   1.276 -	                                   " theorems")) 
   1.277 +	then (tap (fn ths => Output.debug
   1.278 +	             ("Including all " ^ Int.toString (length ths) ^ " theorems")) 
   1.279  	          (all_facts_of ctxt @ PureThy.all_thms_of (ProofContext.theory_of ctxt)))
   1.280  	else 
   1.281  	let val claset_thms =
   1.282 @@ -578,7 +597,7 @@
   1.283        (map put_name_pair included_thms, user_rules)
   1.284    end;
   1.285  
   1.286 -(* remove lemmas that are banned from the backlist *)
   1.287 +(*Remove lemmas that are banned from the backlist. Also remove duplicates. *)
   1.288  fun blacklist_filter thms = 
   1.289    if !run_blacklist_filter then 
   1.290        let val banned = make_banned_test (map #1 thms)
   1.291 @@ -586,22 +605,10 @@
   1.292        in  filter ok thms  end
   1.293    else thms;
   1.294  
   1.295 -(* filter axiom clauses, but keep supplied clauses and clauses in whitelist *)
   1.296 -fun get_relevant_clauses ctxt cls_thms white_cls goals =
   1.297 - let val cls_thms_list = make_unique (mk_clause_table 2200) (List.concat (white_cls@cls_thms))
   1.298 -     val relevant_cls_thms_list = 
   1.299 -	 if !run_relevance_filter 
   1.300 -	 then ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_thms_list goals 
   1.301 -	 else cls_thms_list
   1.302 - in
   1.303 -     insert_thms (List.concat white_cls) relevant_cls_thms_list 
   1.304 - end;
   1.305 -
   1.306  (***************************************************************)
   1.307  (* ATP invocation methods setup                                *)
   1.308  (***************************************************************)
   1.309  
   1.310 -
   1.311  (**** prover-specific format: TPTP ****)
   1.312  
   1.313  
   1.314 @@ -634,12 +641,12 @@
   1.315  	val goal_cls = conj_cls@hyp_cls
   1.316  	val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
   1.317  	val user_lemmas_names = map #1 user_rules
   1.318 -	val rm_black_cls = blacklist_filter included_thms 
   1.319 -	val cla_simp_atp_clauses = ResAxioms.cnf_rules_pairs rm_black_cls
   1.320 +	val cla_simp_atp_clauses = included_thms |> blacklist_filter
   1.321 +	                             |> make_unique |> ResAxioms.cnf_rules_pairs
   1.322  	val user_cls = ResAxioms.cnf_rules_pairs user_rules
   1.323 -	val axclauses = get_relevant_clauses ctxt cla_simp_atp_clauses
   1.324 +	val thy = ProofContext.theory_of ctxt
   1.325 +	val axclauses = get_relevant_clauses thy cla_simp_atp_clauses
   1.326  	                            user_cls (map prop_of goal_cls)
   1.327 -	val thy = ProofContext.theory_of ctxt
   1.328  	val prob_logic = case mode of 
   1.329                              Auto => problem_logic_goals [map prop_of goal_cls]
   1.330  			  | Fol => FOL
   1.331 @@ -730,6 +737,13 @@
   1.332    let val path = File.tmp_path (Path.basic fname)
   1.333    in  Array.app (File.append path o (fn s => s ^ "\n"))  end;
   1.334  
   1.335 +(*Converting a subgoal into negated conjecture clauses*)
   1.336 +fun neg_clauses th n =
   1.337 +  let val tacs = [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac]
   1.338 +      val st = Seq.hd (EVERY' tacs n th)
   1.339 +      val negs = Option.valOf (metahyps_thms n st)
   1.340 +  in make_clauses negs |> ResAxioms.assume_abstract_list |> Meson.finish_cnf end;
   1.341 +		                       
   1.342  (*We write out problem files for each subgoal. Argument probfile generates filenames,
   1.343    and allows the suppression of the suffix "_1" in problem-generation mode.
   1.344    FIXME: does not cope with &&, and it isn't easy because one could have multiple
   1.345 @@ -738,38 +752,39 @@
   1.346    let val goals = Thm.prems_of th
   1.347        val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
   1.348        val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
   1.349 -      val rm_blacklist_cls = blacklist_filter included_thms
   1.350 -      val cla_simp_atp_clauses = ResAxioms.cnf_rules_pairs rm_blacklist_cls
   1.351 -      val axclauses = get_relevant_clauses ctxt cla_simp_atp_clauses (ResAxioms.cnf_rules_pairs white_thms) goals 
   1.352 -      val _ = Output.debug ("total clauses from thms = " ^ Int.toString (length axclauses))
   1.353 +      val cla_simp_atp_clauses = included_thms |> blacklist_filter
   1.354 +                                   |> make_unique |> ResAxioms.cnf_rules_pairs 
   1.355 +      val white_cls = ResAxioms.cnf_rules_pairs white_thms
   1.356 +      val _ = Output.debug ("clauses = " ^ Int.toString(length cla_simp_atp_clauses))
   1.357        val thy = ProofContext.theory_of ctxt
   1.358 -      fun get_neg_subgoals n =
   1.359 -	  if n=0 then []
   1.360 -	  else
   1.361 -	      let val st = Seq.hd (EVERY' [rtac ccontr, ObjectLogic.atomize_tac, 
   1.362 -	                                   skolemize_tac] n th)
   1.363 -		  val negs = Option.valOf (metahyps_thms n st)
   1.364 -		  val negs_clauses = make_clauses negs |> ResAxioms.assume_abstract_list
   1.365 -		                       |> Meson.finish_cnf
   1.366 +      fun get_neg_subgoals [] _ = []
   1.367 +        | get_neg_subgoals (gl::gls) n =
   1.368 +	      let val axclauses = get_relevant_clauses thy cla_simp_atp_clauses
   1.369 +	                            white_cls [gl]  (*relevant to goal*)
   1.370  	      in
   1.371 -		  negs_clauses :: get_neg_subgoals (n-1)
   1.372 +		  (neg_clauses th n, axclauses) :: get_neg_subgoals gls (n+1)
   1.373  	      end
   1.374 -      val neg_subgoals = get_neg_subgoals (length goals) 
   1.375 -      val goals_logic = case !linkup_logic_mode of
   1.376 -                            Auto => problem_logic_goals (map (map prop_of) neg_subgoals)
   1.377 -			  | Fol => FOL
   1.378 -			  | Hol => HOL
   1.379 -      val keep_types = if is_fol_logic goals_logic then !ResClause.keep_types else is_typed_hol ()
   1.380 -      val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
   1.381 -      val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
   1.382 -      val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
   1.383 +      val goal_pairs = get_neg_subgoals goals 1
   1.384 +      val logic = case !linkup_logic_mode of
   1.385 +		Auto => problem_logic_goals (map ((map prop_of) o #1) goal_pairs)
   1.386 +	      | Fol => FOL
   1.387 +	      | Hol => HOL
   1.388 +      val keep_types = if is_fol_logic logic then !ResClause.keep_types 
   1.389 +                       else is_typed_hol ()
   1.390 +      val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy
   1.391 +                             else []
   1.392 +      val _ = Output.debug ("classrel clauses = " ^ 
   1.393 +                            Int.toString (length classrel_clauses))
   1.394 +      val arity_clauses = if keep_types then ResClause.arity_clause_thy thy 
   1.395 +                          else []
   1.396        val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
   1.397        val writer = if !prover = "spass" then dfg_writer else tptp_writer 
   1.398        fun write_all [] _ = []
   1.399 -	| write_all (sub::subgoals) k =
   1.400 -	   (writer goals_logic sub (probfile k) (axclauses,classrel_clauses,arity_clauses) [],
   1.401 -	    probfile k) :: write_all subgoals (k-1)
   1.402 -      val (clnames::_, filenames) = ListPair.unzip (write_all neg_subgoals (length goals))
   1.403 +	| write_all ((ccls,axcls)::subgoals) k =
   1.404 +	   (writer logic ccls (probfile k) (axcls,classrel_clauses,arity_clauses) [],
   1.405 +	    probfile k) 
   1.406 +	   :: write_all subgoals (k+1)
   1.407 +      val (clnames::_, filenames) = ListPair.unzip (write_all goal_pairs 1)
   1.408        val thm_names = Array.fromList clnames
   1.409        val _ = if !Output.show_debug_msgs 
   1.410                then trace_array "thm_names" thm_names else ()