Consolidation of code to "blacklist" unhelpful theorems, including record
authorpaulson
Wed Nov 22 20:08:07 2006 +0100 (2006-11-22)
changeset 214707c1b59ddcd56
parent 21469 1e45e9ef327e
child 21471 03a5ef1936c5
Consolidation of code to "blacklist" unhelpful theorems, including record
surjectivity properties
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/res_clause.ML
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Nov 22 19:55:22 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Nov 22 20:08:07 2006 +0100
     1.3 @@ -247,9 +247,11 @@
     1.4  exception PRED_LG of term;
     1.5  
     1.6  fun pred_lg (t as Const(P,tp)) (lg,seen)= 
     1.7 -      if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg,insert (op =) t seen) 
     1.8 +      if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) 
     1.9 +      else (lg,insert (op =) t seen) 
    1.10    | pred_lg (t as Free(P,tp)) (lg,seen) =
    1.11 -      if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg,insert (op =) t seen)
    1.12 +      if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) 
    1.13 +      else (lg,insert (op =) t seen)
    1.14    | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, insert (op =) t seen)
    1.15    | pred_lg P _ = raise PRED_LG(P);
    1.16  
    1.17 @@ -275,18 +277,13 @@
    1.18        end
    1.19    | lits_lg lits (lg,seen) = (lg,seen);
    1.20  
    1.21 -fun dest_disj_aux (Const ("op |", _) $ t $ t') disjs = 
    1.22 -    dest_disj_aux t (dest_disj_aux t' disjs)
    1.23 +fun dest_disj_aux (Const("Trueprop",_) $ t) disjs = dest_disj_aux t disjs
    1.24 +  | dest_disj_aux (Const ("op |", _) $ t $ t') disjs = dest_disj_aux t (dest_disj_aux t' disjs)
    1.25    | dest_disj_aux t disjs = t::disjs;
    1.26  
    1.27  fun dest_disj t = dest_disj_aux t [];
    1.28  
    1.29 -fun logic_of_clause tm (lg,seen) =
    1.30 -    let val tm' = HOLogic.dest_Trueprop tm
    1.31 -	val disjs = dest_disj tm'
    1.32 -    in
    1.33 -	lits_lg disjs (lg,seen)
    1.34 -    end;
    1.35 +fun logic_of_clause tm = lits_lg (dest_disj tm);
    1.36  
    1.37  fun logic_of_clauses [] (lg,seen) = (lg,seen)
    1.38    | logic_of_clauses (cls::clss) (FOL,seen) =
    1.39 @@ -316,7 +313,7 @@
    1.40  (*The rule subsetI is frequently omitted by the relevance filter.*)
    1.41  val whitelist = ref [subsetI]; 
    1.42    
    1.43 -(*Names of theorems (not theorem lists! See multi_blacklist above) to be banned. 
    1.44 +(*Names of theorems (not theorem lists! See multi_blacklist below) to be banned. 
    1.45  
    1.46    These theorems typically produce clauses that are prolific (match too many equality or
    1.47    membership literals) and relate to seldom-used facts. Some duplicate other rules.
    1.48 @@ -471,10 +468,6 @@
    1.49        Polyhash.insert ht (x^"_iff2", ()); 
    1.50        Polyhash.insert ht (x^"_dest", ())); 
    1.51  
    1.52 -(*FIXME: probably redundant now that ALL boolean-valued variables are banned*)
    1.53 -fun banned_thmlist s =
    1.54 -  (Sign.base_name s) mem_string ["induct","inducts","split","splits","split_asm"];
    1.55 -
    1.56  (*Reject theorems with names like "List.filter.filter_list_def" or
    1.57    "Accessible_Part.acc.defs", as these are definitions arising from packages.
    1.58    FIXME: this will also block definitions within locales*)
    1.59 @@ -486,7 +479,7 @@
    1.60    let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)
    1.61                                  (6000, HASH_STRING)
    1.62        fun banned s = 
    1.63 -            isSome (Polyhash.peek ht s) orelse banned_thmlist s orelse is_package_def s
    1.64 +            isSome (Polyhash.peek ht s) orelse is_package_def s
    1.65    in  app (fn x => Polyhash.insert ht (x,())) (!blacklist);
    1.66        app (insert_suffixed_names ht) (!blacklist @ xs); 
    1.67        banned
    1.68 @@ -505,12 +498,7 @@
    1.69  fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_term(P,0w0))
    1.70    | hash_literal P = hashw_term(P,0w0);
    1.71  
    1.72 -
    1.73 -fun get_literals (Const("Trueprop",_)$P) lits = get_literals P lits
    1.74 -  | get_literals (Const("op |",_)$P$Q) lits = get_literals Q (get_literals P lits)
    1.75 -  | get_literals lit lits = (lit::lits);
    1.76 -
    1.77 -fun hash_term t = Word.toIntX (xor_words (map hash_literal (get_literals t [])));
    1.78 +fun hash_term t = Word.toIntX (xor_words (map hash_literal (dest_disj t)));
    1.79  
    1.80  fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);
    1.81  
    1.82 @@ -565,9 +553,13 @@
    1.83    ["Set.ball_simps", "Set.bex_simps",  (*quantifier rewriting: useless*)
    1.84     "Set.disjoint_insert", "Set.insert_disjoint", "Set.Inter_UNIV_conv"];
    1.85  
    1.86 +val multi_base_blacklist =
    1.87 +  ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm"];
    1.88 +
    1.89  (*Ignore blacklisted theorem lists*)
    1.90  fun add_multi_names ((a, ths), pairs) = 
    1.91 -  if a mem_string multi_blacklist then pairs
    1.92 +  if a mem_string multi_blacklist orelse (Sign.base_name a) mem_string multi_base_blacklist
    1.93 +  then pairs
    1.94    else add_multi_names_aux ((a, ths), pairs);
    1.95  
    1.96  fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
    1.97 @@ -675,16 +667,50 @@
    1.98    if is_fol_logic logic then filter (Meson.is_fol_term o prop_of o fst) cls 
    1.99  	                else cls;
   1.100  
   1.101 +(**** Predicates to detect unwanted clauses (prolific or likely to cause unsoundness) ****)
   1.102 +
   1.103 +(** Too general means, positive equality literal with a variable X as one operand,
   1.104 +  when X does not occur properly in the other operand. This rules out clearly
   1.105 +  inconsistent clauses such as V=a|V=b, though it by no means guarantees soundness. **)
   1.106 + 
   1.107 +fun occurs ix =
   1.108 +    let fun occ(Var (jx,_)) = (ix=jx)
   1.109 +          | occ(t1$t2)      = occ t1 orelse occ t2
   1.110 +          | occ(Abs(_,_,t)) = occ t
   1.111 +          | occ _           = false
   1.112 +    in occ end;
   1.113 +
   1.114 +fun is_recordtype T = not (null (RecordPackage.dest_recTs T));
   1.115 +
   1.116 +(*Unwanted equalities include
   1.117 +  (1) those between a variable that does not properly occur in the second operand,
   1.118 +  (2) those between a variable and a record, since these seem to be prolific "cases" thms
   1.119 +*)  
   1.120 +fun too_general_eqterms (Var (ix,T), t) = not (occurs ix t) orelse is_recordtype T
   1.121 +  | too_general_eqterms _ = false;
   1.122 +
   1.123 +fun too_general_equality (Const ("op =", _) $ x $ y) =
   1.124 +      too_general_eqterms (x,y) orelse too_general_eqterms(y,x)
   1.125 +  | too_general_equality _ = false;
   1.126 +
   1.127 +(* tautologous? *)
   1.128 +fun is_taut (Const ("Trueprop", _) $ Const ("True", _)) = true
   1.129 +  | is_taut _ = false;
   1.130 +
   1.131  (*True if the term contains a variable whose (atomic) type is in the given list.*)
   1.132  fun has_typed_var tycons = 
   1.133    let fun var_tycon (Var (_, Type(a,_))) = a mem_string tycons
   1.134          | var_tycon _ = false
   1.135    in  exists var_tycon o term_vars  end;
   1.136  
   1.137 +fun unwanted t =
   1.138 +    is_taut t orelse has_typed_var ["Product_Type.unit","bool"] t orelse
   1.139 +    forall too_general_equality (dest_disj t);
   1.140 +
   1.141  (*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and
   1.142    likely to lead to unsound proofs.*)
   1.143 -fun remove_finite_types cls =
   1.144 -  filter (not o has_typed_var ["Product_Type.unit","bool"] o prop_of o fst) cls;
   1.145 +fun remove_unwanted_clauses cls =
   1.146 +  filter (not o unwanted o prop_of o fst) cls;
   1.147  
   1.148  fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas =
   1.149      if is_fol_logic logic 
   1.150 @@ -711,7 +737,7 @@
   1.151  	val cla_simp_atp_clauses = included_thms |> blacklist_filter
   1.152  	                             |> ResAxioms.cnf_rules_pairs |> make_unique 
   1.153                                       |> restrict_to_logic logic 
   1.154 -                                     |> remove_finite_types
   1.155 +                                     |> remove_unwanted_clauses
   1.156  	val user_cls = ResAxioms.cnf_rules_pairs user_rules
   1.157  	val thy = ProofContext.theory_of ctxt
   1.158  	val axclauses = make_unique (get_relevant_clauses thy cla_simp_atp_clauses user_cls goal_tms)
   1.159 @@ -833,7 +859,7 @@
   1.160        val included_cls = included_thms |> blacklist_filter
   1.161                                         |> ResAxioms.cnf_rules_pairs |> make_unique 
   1.162                                         |> restrict_to_logic logic
   1.163 -                                       |> remove_finite_types
   1.164 +                                       |> remove_unwanted_clauses
   1.165        val _ = Output.debug ("clauses = " ^ Int.toString(length included_cls))
   1.166        val white_cls = ResAxioms.cnf_rules_pairs white_thms
   1.167        (*clauses relevant to goal gl*)
     2.1 --- a/src/HOL/Tools/res_axioms.ML	Wed Nov 22 19:55:22 2006 +0100
     2.2 +++ b/src/HOL/Tools/res_axioms.ML	Wed Nov 22 20:08:07 2006 +0100
     2.3 @@ -91,14 +91,6 @@
     2.4  fun transfer_to_ATP_Linkup th =
     2.5      transfer (Theory.deref recon_thy_ref) th handle THM _ => th;
     2.6  
     2.7 -fun is_taut th =
     2.8 -      case (prop_of th) of
     2.9 -           (Const ("Trueprop", _) $ Const ("True", _)) => true
    2.10 -         | _ => false;
    2.11 -
    2.12 -(* remove tautologous clauses *)
    2.13 -val rm_redundant_cls = List.filter (not o is_taut);
    2.14 -
    2.15  
    2.16  (**** SKOLEMIZATION BY INFERENCE (lcp) ****)
    2.17  
    2.18 @@ -467,8 +459,7 @@
    2.19  (*Skolemize a named theorem, with Skolem functions as additional premises.*)
    2.20  fun skolem_thm th =
    2.21    let val nnfth = to_nnf th
    2.22 -  in  Meson.make_cnf (skolem_of_nnf nnfth) nnfth
    2.23 -      |> assume_abstract_list |> Meson.finish_cnf |> rm_redundant_cls
    2.24 +  in  Meson.make_cnf (skolem_of_nnf nnfth) nnfth |> assume_abstract_list |> Meson.finish_cnf
    2.25    end
    2.26    handle THM _ => [];
    2.27  
    2.28 @@ -485,7 +476,7 @@
    2.29            let val (thy',defs) = declare_skofuns cname nnfth thy
    2.30                val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth
    2.31                val (thy'',cnfs') = declare_abstract (thy',cnfs)
    2.32 -          in (thy'', rm_redundant_cls (Meson.finish_cnf cnfs'))
    2.33 +          in (thy'', Meson.finish_cnf cnfs')
    2.34            end)
    2.35        (SOME (to_nnf th)  handle THM _ => NONE)
    2.36    end;
     3.1 --- a/src/HOL/Tools/res_clause.ML	Wed Nov 22 19:55:22 2006 +0100
     3.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Nov 22 20:08:07 2006 +0100
     3.3 @@ -417,35 +417,14 @@
     3.4  	  (vss, fs union fss)
     3.5        end;
     3.6  
     3.7 -(** Too general means, positive equality literal with a variable X as one operand,
     3.8 -  when X does not occur properly in the other operand. This rules out clearly
     3.9 -  inconsistent clauses such as V=a|V=b, though it by no means guarantees soundness. **)
    3.10 -
    3.11 -fun occurs a (UVar(b,_)) = a=b
    3.12 -  | occurs a (Fun (_,_,ts)) = exists (occurs a) ts
    3.13 -
    3.14 -(*Is the first operand a variable that does not properly occur in the second operand?*)
    3.15 -fun too_general_terms (UVar _, UVar _) = false
    3.16 -  | too_general_terms (Fun _, _) = false
    3.17 -  | too_general_terms (UVar (a,_), t) = not (occurs a t);
    3.18 -
    3.19 -fun too_general_lit (Literal (true, Predicate("equal",_,[x,y]))) =
    3.20 -      too_general_terms (x,y) orelse too_general_terms(y,x)
    3.21 -  | too_general_lit _ = false;
    3.22 -
    3.23 -
    3.24  
    3.25  (** make axiom and conjecture clauses. **)
    3.26  
    3.27  exception MAKE_CLAUSE;
    3.28  fun make_clause (clause_id, axiom_name, th, kind) =
    3.29 -  let val term = prop_of th
    3.30 -      val (lits,types_sorts) = literals_of_term term
    3.31 +  let val (lits,types_sorts) = literals_of_term (prop_of th)
    3.32    in if forall isFalse lits 
    3.33       then error "Problem too trivial for resolution (empty clause)"
    3.34 -     else if kind=Axiom andalso forall too_general_lit lits 
    3.35 -     then (Output.debug ("Omitting " ^ axiom_name ^ ": equalities are too general"); 
    3.36 -           raise MAKE_CLAUSE)
    3.37       else Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, 
    3.38                    kind = kind, literals = lits, types_sorts = types_sorts}
    3.39    end;		     
     4.1 --- a/src/HOL/Tools/res_hol_clause.ML	Wed Nov 22 19:55:22 2006 +0100
     4.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Wed Nov 22 20:08:07 2006 +0100
     4.3 @@ -418,21 +418,6 @@
     4.4  
     4.5  fun literals_of_term P = literals_of_term1 ([],[]) P;
     4.6  
     4.7 -fun occurs a (CombVar(b,_)) = a = b
     4.8 -  | occurs a (CombApp(t1,t2,_)) = (occurs a t1) orelse (occurs a t2)
     4.9 -  | occurs _ _ = false
    4.10 -
    4.11 -fun too_general_terms (CombVar(v,_), t) = not (occurs v t)
    4.12 -  | too_general_terms _ = false;
    4.13 -
    4.14 -fun too_general_equality (Literal(true,(Bool(CombApp(CombApp(CombConst("equal",tp,tps),t1,tp1),t2,tp2))))) =
    4.15 -      too_general_terms (t1,t2) orelse too_general_terms (t2,t1)
    4.16 -  | too_general_equality _ = false;
    4.17 -
    4.18 -(* forbid the literal hBOOL(V) *)
    4.19 -fun too_general_bool (Literal(_,Bool(CombVar _))) = true
    4.20 -  | too_general_bool _ = false;
    4.21 -
    4.22  (* making axiom and conjecture clauses *)
    4.23  exception MAKE_CLAUSE
    4.24  fun make_clause(clause_id,axiom_name,kind,thm,is_user) =
    4.25 @@ -443,10 +428,6 @@
    4.26      in
    4.27  	if forall isFalse lits
    4.28  	then error "Problem too trivial for resolution (empty clause)"
    4.29 -	else if (!typ_level <> T_FULL) andalso kind=Axiom andalso 
    4.30 -	        (forall too_general_equality lits orelse exists too_general_bool lits)
    4.31 -	    then (Output.debug ("Omitting " ^ axiom_name ^ ": clause is too prolific"); 
    4.32 -	          raise MAKE_CLAUSE) 
    4.33  	else
    4.34  	    Clause {clause_id = clause_id, axiom_name = axiom_name, th = thm, kind = kind,
    4.35  		    literals = lits, ctypes_sorts = ctypes_sorts, 
    4.36 @@ -718,16 +699,6 @@
    4.37  
    4.38  val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname)
    4.39  
    4.40 -(*Simulate the result of conversion to CNF*)
    4.41 -fun pretend_cnf s = (thm s, (s,0));
    4.42 -
    4.43 -(*These theorems allow the proof of P=Q from P-->Q and Q-->P, so they are necessary for
    4.44 -  completeness. Unfortunately, they are very prolific, causing greatly increased runtimes.
    4.45 -  They also lead to many unsound proofs. Thus it is well that the "exists too_general_bool"
    4.46 -  test deletes them except with the full-typed translation.*)
    4.47 -val iff_thms = [pretend_cnf "ATP_Linkup.iff_positive", 
    4.48 -                pretend_cnf "ATP_Linkup.iff_negative"];
    4.49 -
    4.50  fun get_helper_clauses () =
    4.51      let val IK = if !combI_count > 0 orelse !combK_count > 0 
    4.52                   then (Output.debug "Include combinator I K"; cnf_helper_thms [comb_I,comb_K]) 
    4.53 @@ -746,7 +717,7 @@
    4.54  	         else []
    4.55  	val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal]
    4.56      in
    4.57 -	make_axiom_clauses (iff_thms @ other @ IK @ BC @ S @ B'C' @ S') []
    4.58 +	make_axiom_clauses (other @ IK @ BC @ S @ B'C' @ S') []
    4.59      end
    4.60  
    4.61