src/HOL/Tools/res_atp.ML
changeset 24958 ff15f76741bd
parent 24920 2a45e400fdad
child 25006 fcf5a999d1c3
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Oct 11 15:57:29 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Oct 11 15:59:31 2007 +0200
     1.3 @@ -36,7 +36,6 @@
     1.4    val rm_simpset : unit -> unit
     1.5    val rm_atpset : unit -> unit
     1.6    val rm_clasimp : unit -> unit
     1.7 -  val is_fol_thms : thm list -> bool
     1.8    val tvar_classes_of_terms : term list -> string list
     1.9    val tfree_classes_of_terms : term list -> string list
    1.10    val type_consts_of_terms : theory -> term list -> string list
    1.11 @@ -137,128 +136,9 @@
    1.12  fun add_atpset() = include_atpset:=true;
    1.13  fun rm_atpset() = include_atpset:=false;
    1.14  
    1.15 -
    1.16 -(******************************************************************)
    1.17 -(* detect whether a given problem (clauses) is FOL/HOL/HOLC/HOLCS *)
    1.18 -(******************************************************************)
    1.19 -
    1.20 -datatype logic = FOL | HOL | HOLC | HOLCS;
    1.21 -
    1.22 -fun string_of_logic FOL = "FOL"
    1.23 -  | string_of_logic HOL = "HOL"
    1.24 -  | string_of_logic HOLC = "HOLC"
    1.25 -  | string_of_logic HOLCS = "HOLCS";
    1.26 -
    1.27 -fun is_fol_logic FOL = true
    1.28 -  | is_fol_logic  _ = false
    1.29 -
    1.30 -(*HOLCS will not occur here*)
    1.31 -fun upgrade_lg HOLC _ = HOLC
    1.32 -  | upgrade_lg HOL HOLC = HOLC
    1.33 -  | upgrade_lg HOL _ = HOL
    1.34 -  | upgrade_lg FOL lg = lg;
    1.35 -
    1.36 -(* check types *)
    1.37 -fun has_bool_hfn (Type("bool",_)) = true
    1.38 -  | has_bool_hfn (Type("fun",_)) = true
    1.39 -  | has_bool_hfn (Type(_, Ts)) = exists has_bool_hfn Ts
    1.40 -  | has_bool_hfn _ = false;
    1.41 -
    1.42 -fun is_hol_fn tp =
    1.43 -    let val (targs,tr) = strip_type tp
    1.44 -    in
    1.45 -        exists (has_bool_hfn) (tr::targs)
    1.46 -    end;
    1.47 -
    1.48 -fun is_hol_pred tp =
    1.49 -    let val (targs,tr) = strip_type tp
    1.50 -    in
    1.51 -        exists (has_bool_hfn) targs
    1.52 -    end;
    1.53 -
    1.54 -exception FN_LG of term;
    1.55 -
    1.56 -fun fn_lg (t as Const(f,tp)) (lg,seen) =
    1.57 -    if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen)
    1.58 -  | fn_lg (t as Free(f,tp)) (lg,seen) =
    1.59 -    if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen)
    1.60 -  | fn_lg (t as Var(f,tp)) (lg,seen) =
    1.61 -    if is_hol_fn tp then (upgrade_lg HOL lg,insert (op =) t seen) else (lg,insert (op =) t seen)
    1.62 -  | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,insert (op =) t seen)
    1.63 -  | fn_lg f _ = raise FN_LG(f);
    1.64 -
    1.65 +fun strip_Trueprop (Const("Trueprop",_) $ t) = t
    1.66 +  | strip_Trueprop t = t;
    1.67  
    1.68 -fun term_lg [] (lg,seen) = (lg,seen)
    1.69 -  | term_lg (tm::tms) (FOL,seen) =
    1.70 -      let val (f,args) = strip_comb tm
    1.71 -          val (lg',seen') = if f mem seen then (FOL,seen)
    1.72 -                            else fn_lg f (FOL,seen)
    1.73 -      in
    1.74 -        if is_fol_logic lg' then ()
    1.75 -        else Output.debug (fn () => ("Found a HOL term: " ^ Display.raw_string_of_term f));
    1.76 -        term_lg (args@tms) (lg',seen')
    1.77 -      end
    1.78 -  | term_lg _ (lg,seen) = (lg,seen)
    1.79 -
    1.80 -exception PRED_LG of term;
    1.81 -
    1.82 -fun pred_lg (t as Const(P,tp)) (lg,seen)=
    1.83 -      if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen)
    1.84 -      else (lg,insert (op =) t seen)
    1.85 -  | pred_lg (t as Free(P,tp)) (lg,seen) =
    1.86 -      if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen)
    1.87 -      else (lg,insert (op =) t seen)
    1.88 -  | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, insert (op =) t seen)
    1.89 -  | pred_lg P _ = raise PRED_LG(P);
    1.90 -
    1.91 -
    1.92 -fun lit_lg (Const("Not",_) $ P) (lg,seen) = lit_lg P (lg,seen)
    1.93 -  | lit_lg P (lg,seen) =
    1.94 -      let val (pred,args) = strip_comb P
    1.95 -          val (lg',seen') = if pred mem seen then (lg,seen)
    1.96 -                            else pred_lg pred (lg,seen)
    1.97 -      in
    1.98 -        if is_fol_logic lg' then ()
    1.99 -        else Output.debug (fn () => ("Found a HOL predicate: " ^ Display.raw_string_of_term pred));
   1.100 -        term_lg args (lg',seen')
   1.101 -      end;
   1.102 -
   1.103 -fun lits_lg [] (lg,seen) = (lg,seen)
   1.104 -  | lits_lg (lit::lits) (FOL,seen) =
   1.105 -      let val (lg,seen') = lit_lg lit (FOL,seen)
   1.106 -      in
   1.107 -        if is_fol_logic lg then ()
   1.108 -        else Output.debug (fn () => ("Found a HOL literal: " ^ Display.raw_string_of_term lit));
   1.109 -        lits_lg lits (lg,seen')
   1.110 -      end
   1.111 -  | lits_lg lits (lg,seen) = (lg,seen);
   1.112 -
   1.113 -fun dest_disj_aux (Const("Trueprop",_) $ t) disjs = dest_disj_aux t disjs
   1.114 -  | dest_disj_aux (Const ("op |", _) $ t $ t') disjs = dest_disj_aux t (dest_disj_aux t' disjs)
   1.115 -  | dest_disj_aux t disjs = t::disjs;
   1.116 -
   1.117 -fun dest_disj t = dest_disj_aux t [];
   1.118 -
   1.119 -fun logic_of_clause tm = lits_lg (dest_disj tm);
   1.120 -
   1.121 -fun logic_of_clauses [] (lg,seen) = (lg,seen)
   1.122 -  | logic_of_clauses (cls::clss) (FOL,seen) =
   1.123 -    let val (lg,seen') = logic_of_clause cls (FOL,seen)
   1.124 -        val _ =
   1.125 -          if is_fol_logic lg then ()
   1.126 -          else Output.debug (fn () => ("Found a HOL clause: " ^ Display.raw_string_of_term cls))
   1.127 -    in
   1.128 -        logic_of_clauses clss (lg,seen')
   1.129 -    end
   1.130 -  | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen);
   1.131 -
   1.132 -fun problem_logic_goals_aux [] (lg,seen) = lg
   1.133 -  | problem_logic_goals_aux (subgoal::subgoals) (lg,seen) =
   1.134 -    problem_logic_goals_aux subgoals (logic_of_clauses subgoal (lg,seen));
   1.135 -
   1.136 -fun problem_logic_goals subgoals = problem_logic_goals_aux subgoals (FOL,[]);
   1.137 -
   1.138 -fun is_fol_thms ths = ((fst(logic_of_clauses (map prop_of ths) (FOL,[]))) = FOL);
   1.139  
   1.140  (***************************************************************)
   1.141  (* Relevance Filtering                                         *)
   1.142 @@ -544,7 +424,7 @@
   1.143  fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_term(P,0w0))
   1.144    | hash_literal P = hashw_term(P,0w0);
   1.145  
   1.146 -fun hash_term t = Word.toIntX (xor_words (map hash_literal (dest_disj t)));
   1.147 +fun hash_term t = Word.toIntX (xor_words (map hash_literal (HOLogic.disjuncts (strip_Trueprop t))));
   1.148  
   1.149  fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);
   1.150  
   1.151 @@ -705,9 +585,8 @@
   1.152  val linkup_logic_mode = ref Auto;
   1.153  
   1.154  (*Ensures that no higher-order theorems "leak out"*)
   1.155 -fun restrict_to_logic thy logic cls =
   1.156 -  if is_fol_logic logic then filter (Meson.is_fol_term thy o prop_of o fst) cls
   1.157 -                        else cls;
   1.158 +fun restrict_to_logic thy true cls = filter (Meson.is_fol_term thy o prop_of o fst) cls
   1.159 +  | restrict_to_logic thy false cls = cls;
   1.160  
   1.161  (**** Predicates to detect unwanted clauses (prolific or likely to cause unsoundness) ****)
   1.162  
   1.163 @@ -752,17 +631,13 @@
   1.164  val unwanted_types = ["Product_Type.unit","bool"];
   1.165  
   1.166  fun unwanted t =
   1.167 -    is_taut t orelse has_typed_var unwanted_types t orelse
   1.168 -    forall too_general_equality (dest_disj t);
   1.169 +  is_taut t orelse has_typed_var unwanted_types t orelse
   1.170 +  forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t));
   1.171  
   1.172  (*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and
   1.173    likely to lead to unsound proofs.*)
   1.174  fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
   1.175  
   1.176 -fun tptp_writer thy logic = ResHolClause.tptp_write_file thy (logic=FOL);
   1.177 -
   1.178 -fun dfg_writer thy logic = ResHolClause.dfg_write_file thy (logic=FOL);
   1.179 -
   1.180  (*Called by the oracle-based methods declared in res_atp_methods.ML*)
   1.181  fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
   1.182      let val conj_cls = Meson.make_clauses conjectures
   1.183 @@ -771,14 +646,14 @@
   1.184          val goal_cls = conj_cls@hyp_cls
   1.185          val goal_tms = map prop_of goal_cls
   1.186          val thy = ProofContext.theory_of ctxt
   1.187 -        val logic = case mode of
   1.188 -                            Auto => problem_logic_goals [goal_tms]
   1.189 -                          | Fol => FOL
   1.190 -                          | Hol => HOL
   1.191 +        val isFO = case mode of
   1.192 +                            Auto => forall (Meson.is_fol_term thy) goal_tms
   1.193 +                          | Fol => true
   1.194 +                          | Hol => false
   1.195          val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
   1.196          val cla_simp_atp_clauses = included_thms
   1.197                                       |> ResAxioms.cnf_rules_pairs |> make_unique
   1.198 -                                     |> restrict_to_logic thy logic
   1.199 +                                     |> restrict_to_logic thy isFO
   1.200                                       |> remove_unwanted_clauses
   1.201          val user_cls = ResAxioms.cnf_rules_pairs user_rules
   1.202          val axclauses = make_unique (user_cls @ relevance_filter thy cla_simp_atp_clauses goal_tms)
   1.203 @@ -789,11 +664,11 @@
   1.204          (*TFrees in conjecture clauses; TVars in axiom clauses*)
   1.205          val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers
   1.206          val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
   1.207 -        val writer = if dfg then dfg_writer else tptp_writer
   1.208 +        val writer = if dfg then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file
   1.209          and file = atp_input_file()
   1.210          and user_lemmas_names = map #1 user_rules
   1.211      in
   1.212 -        writer thy logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
   1.213 +        writer thy isFO goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
   1.214          Output.debug (fn () => "Writing to " ^ file);
   1.215          file
   1.216      end;
   1.217 @@ -866,13 +741,13 @@
   1.218          | get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) ::
   1.219                                           get_neg_subgoals gls (n+1)
   1.220        val goal_cls = get_neg_subgoals goals 1
   1.221 -      val logic = case !linkup_logic_mode of
   1.222 -                Auto => problem_logic_goals (map (map prop_of) goal_cls)
   1.223 -              | Fol => FOL
   1.224 -              | Hol => HOL
   1.225 +      val isFO = case !linkup_logic_mode of
   1.226 +			  Auto => forall (Meson.is_fol_term thy) (map prop_of (List.concat goal_cls))
   1.227 +			| Fol => true
   1.228 +			| Hol => false
   1.229        val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt chain_ths
   1.230        val included_cls = included_thms |> ResAxioms.cnf_rules_pairs |> make_unique
   1.231 -                                       |> restrict_to_logic thy logic
   1.232 +                                       |> restrict_to_logic thy isFO
   1.233                                         |> remove_unwanted_clauses
   1.234        val _ = Output.debug (fn () => "included clauses = " ^ Int.toString(length included_cls))
   1.235        val white_cls = ResAxioms.cnf_rules_pairs white_thms
   1.236 @@ -880,7 +755,7 @@
   1.237        val axcls_list = map (fn ngcls => white_cls @ relevance_filter thy included_cls (map prop_of ngcls)) goal_cls
   1.238        val _ = app (fn axcls => Output.debug (fn () => "filtered clauses = " ^ Int.toString(length axcls)))
   1.239                    axcls_list
   1.240 -      val writer = if !prover = Recon.SPASS then dfg_writer else tptp_writer
   1.241 +      val writer = if !prover = Recon.SPASS then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file
   1.242        fun write_all [] [] _ = []
   1.243          | write_all (ccls::ccls_list) (axcls::axcls_list) k =
   1.244              let val fname = probfile k
   1.245 @@ -901,7 +776,7 @@
   1.246                  val _ = Output.debug (fn () => "arity clauses = " ^ Int.toString (length arity_clauses))
   1.247                  val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
   1.248                  val _ = Output.debug (fn () => "classrel clauses = " ^ Int.toString (length classrel_clauses))
   1.249 -                val clnames = writer thy logic ccls fname (axcls,classrel_clauses,arity_clauses) []
   1.250 +                val clnames = writer thy isFO ccls fname (axcls,classrel_clauses,arity_clauses) []
   1.251                  val thm_names = Vector.fromList clnames
   1.252                  val _ = if !Output.debugging then trace_vector fname thm_names else ()
   1.253              in  (thm_names,fname) :: write_all ccls_list axcls_list (k+1)  end