author paulson Thu Oct 11 15:59:31 2007 +0200 (2007-10-11) changeset 24958 ff15f76741bd parent 24957 50959112a4e1 child 24959 119793c84647
rationalized redundant code
 src/HOL/Tools/cnf_funcs.ML file | annotate | diff | revisions src/HOL/Tools/metis_tools.ML file | annotate | diff | revisions src/HOL/Tools/res_atp.ML file | annotate | diff | revisions src/HOL/Tools/res_reconstruct.ML file | annotate | diff | revisions src/HOL/hologic.ML file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Tools/cnf_funcs.ML	Thu Oct 11 15:57:29 2007 +0200
1.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Thu Oct 11 15:59:31 2007 +0200
1.3 @@ -4,6 +4,8 @@
1.4      Author:     Tjark Weber
1.6
1.7 +  FIXME: major overlaps with the code in meson.ML
1.8 +
1.9    Description:
1.10    This file contains functions and tactics to transform a formula into
1.11    Conjunctive Normal Form (CNF).
1.12 @@ -122,9 +124,6 @@
1.13
1.14  fun clause_is_trivial c =
1.15  	let
1.16 -		(* Term.term -> Term.term list -> Term.term list *)
1.17 -		fun collect_literals (Const ("op |", _) \$ x \$ y) ls = collect_literals x (collect_literals y ls)
1.18 -		  | collect_literals x                           ls = x :: ls
1.19  		(* Term.term -> Term.term *)
1.20  		fun dual (Const ("Not", _) \$ x) = x
1.21  		  | dual x                      = HOLogic.Not \$ x
1.22 @@ -132,7 +131,7 @@
1.23  		fun has_duals []      = false
1.24  		  | has_duals (x::xs) = (dual x) mem xs orelse has_duals xs
1.25  	in
1.26 -		has_duals (collect_literals c [])
1.27 +		has_duals (HOLogic.disjuncts c)
1.28  	end;
1.29
1.30  (* ------------------------------------------------------------------------- *)
```
```     2.1 --- a/src/HOL/Tools/metis_tools.ML	Thu Oct 11 15:57:29 2007 +0200
2.2 +++ b/src/HOL/Tools/metis_tools.ML	Thu Oct 11 15:59:31 2007 +0200
2.3 @@ -529,9 +529,11 @@
2.4          tfrees = tfrees};
2.5
2.6    (* Function to generate metis clauses, including comb and type clauses *)
2.7 -  fun build_map mode thy ctxt cls ths =
2.8 -    let val isFO = (mode = ResAtp.Fol) orelse
2.9 -                    (mode <> ResAtp.Hol andalso ResAtp.is_fol_thms (cls @ ths))
2.10 +  fun build_map mode ctxt cls ths =
2.11 +    let val thy = ProofContext.theory_of ctxt
2.12 +        val all_thms_FO = forall (Meson.is_fol_term thy o prop_of)
2.13 +        val isFO = (mode = ResAtp.Fol) orelse
2.14 +                   (mode <> ResAtp.Hol andalso all_thms_FO (cls @ ths))
2.15          val lmap0 = foldl (add_thm true ctxt)
2.16                            {isFO = isFO, axioms = [], tfrees = init_tfrees ctxt} cls
2.18 @@ -559,8 +561,7 @@
2.19
2.20    (* Main function to start metis prove and reconstruction *)
2.21    fun FOL_SOLVE mode ctxt cls ths0 =
2.22 -    let val thy = ProofContext.theory_of ctxt
2.23 -        val th_cls_pairs = map (fn th => (PureThy.get_name_hint th, ResAxioms.cnf_axiom th)) ths0
2.24 +    let val th_cls_pairs = map (fn th => (PureThy.get_name_hint th, ResAxioms.cnf_axiom th)) ths0
2.25          val ths = List.concat (map #2 th_cls_pairs)
2.26          val _ = if exists(is_false o prop_of) cls then error "problem contains the empty clause"
2.27                  else ();
2.28 @@ -568,7 +569,7 @@
2.29          val _ = app (fn th => Output.debug (fn () => string_of_thm th)) cls
2.30          val _ = Output.debug (fn () => "THEOREM CLAUSES")
2.31          val _ = app (fn th => Output.debug (fn () => string_of_thm th)) ths
2.32 -        val {isFO,axioms,tfrees} = build_map mode thy ctxt cls ths
2.33 +        val {isFO,axioms,tfrees} = build_map mode ctxt cls ths
2.34          val _ = if null tfrees then ()
2.35                  else (Output.debug (fn () => "TFREE CLAUSES");
2.36                        app (fn tf => Output.debug (fn _ => ResClause.tptp_of_typeLit true tf)) tfrees)
```
```     3.1 --- a/src/HOL/Tools/res_atp.ML	Thu Oct 11 15:57:29 2007 +0200
3.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Oct 11 15:59:31 2007 +0200
3.3 @@ -36,7 +36,6 @@
3.4    val rm_simpset : unit -> unit
3.5    val rm_atpset : unit -> unit
3.6    val rm_clasimp : unit -> unit
3.7 -  val is_fol_thms : thm list -> bool
3.8    val tvar_classes_of_terms : term list -> string list
3.9    val tfree_classes_of_terms : term list -> string list
3.10    val type_consts_of_terms : theory -> term list -> string list
3.11 @@ -137,128 +136,9 @@
3.13  fun rm_atpset() = include_atpset:=false;
3.14
3.15 -
3.16 -(******************************************************************)
3.17 -(* detect whether a given problem (clauses) is FOL/HOL/HOLC/HOLCS *)
3.18 -(******************************************************************)
3.19 -
3.20 -datatype logic = FOL | HOL | HOLC | HOLCS;
3.21 -
3.22 -fun string_of_logic FOL = "FOL"
3.23 -  | string_of_logic HOL = "HOL"
3.24 -  | string_of_logic HOLC = "HOLC"
3.25 -  | string_of_logic HOLCS = "HOLCS";
3.26 -
3.27 -fun is_fol_logic FOL = true
3.28 -  | is_fol_logic  _ = false
3.29 -
3.30 -(*HOLCS will not occur here*)
3.31 -fun upgrade_lg HOLC _ = HOLC
3.32 -  | upgrade_lg HOL HOLC = HOLC
3.33 -  | upgrade_lg HOL _ = HOL
3.34 -  | upgrade_lg FOL lg = lg;
3.35 -
3.36 -(* check types *)
3.37 -fun has_bool_hfn (Type("bool",_)) = true
3.38 -  | has_bool_hfn (Type("fun",_)) = true
3.39 -  | has_bool_hfn (Type(_, Ts)) = exists has_bool_hfn Ts
3.40 -  | has_bool_hfn _ = false;
3.41 -
3.42 -fun is_hol_fn tp =
3.43 -    let val (targs,tr) = strip_type tp
3.44 -    in
3.45 -        exists (has_bool_hfn) (tr::targs)
3.46 -    end;
3.47 -
3.48 -fun is_hol_pred tp =
3.49 -    let val (targs,tr) = strip_type tp
3.50 -    in
3.51 -        exists (has_bool_hfn) targs
3.52 -    end;
3.53 -
3.54 -exception FN_LG of term;
3.55 -
3.56 -fun fn_lg (t as Const(f,tp)) (lg,seen) =
3.57 -    if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen)
3.58 -  | fn_lg (t as Free(f,tp)) (lg,seen) =
3.59 -    if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen)
3.60 -  | fn_lg (t as Var(f,tp)) (lg,seen) =
3.61 -    if is_hol_fn tp then (upgrade_lg HOL lg,insert (op =) t seen) else (lg,insert (op =) t seen)
3.62 -  | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,insert (op =) t seen)
3.63 -  | fn_lg f _ = raise FN_LG(f);
3.64 -
3.65 +fun strip_Trueprop (Const("Trueprop",_) \$ t) = t
3.66 +  | strip_Trueprop t = t;
3.67
3.68 -fun term_lg [] (lg,seen) = (lg,seen)
3.69 -  | term_lg (tm::tms) (FOL,seen) =
3.70 -      let val (f,args) = strip_comb tm
3.71 -          val (lg',seen') = if f mem seen then (FOL,seen)
3.72 -                            else fn_lg f (FOL,seen)
3.73 -      in
3.74 -        if is_fol_logic lg' then ()
3.75 -        else Output.debug (fn () => ("Found a HOL term: " ^ Display.raw_string_of_term f));
3.76 -        term_lg (args@tms) (lg',seen')
3.77 -      end
3.78 -  | term_lg _ (lg,seen) = (lg,seen)
3.79 -
3.80 -exception PRED_LG of term;
3.81 -
3.82 -fun pred_lg (t as Const(P,tp)) (lg,seen)=
3.83 -      if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen)
3.84 -      else (lg,insert (op =) t seen)
3.85 -  | pred_lg (t as Free(P,tp)) (lg,seen) =
3.86 -      if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen)
3.87 -      else (lg,insert (op =) t seen)
3.88 -  | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, insert (op =) t seen)
3.89 -  | pred_lg P _ = raise PRED_LG(P);
3.90 -
3.91 -
3.92 -fun lit_lg (Const("Not",_) \$ P) (lg,seen) = lit_lg P (lg,seen)
3.93 -  | lit_lg P (lg,seen) =
3.94 -      let val (pred,args) = strip_comb P
3.95 -          val (lg',seen') = if pred mem seen then (lg,seen)
3.96 -                            else pred_lg pred (lg,seen)
3.97 -      in
3.98 -        if is_fol_logic lg' then ()
3.99 -        else Output.debug (fn () => ("Found a HOL predicate: " ^ Display.raw_string_of_term pred));
3.100 -        term_lg args (lg',seen')
3.101 -      end;
3.102 -
3.103 -fun lits_lg [] (lg,seen) = (lg,seen)
3.104 -  | lits_lg (lit::lits) (FOL,seen) =
3.105 -      let val (lg,seen') = lit_lg lit (FOL,seen)
3.106 -      in
3.107 -        if is_fol_logic lg then ()
3.108 -        else Output.debug (fn () => ("Found a HOL literal: " ^ Display.raw_string_of_term lit));
3.109 -        lits_lg lits (lg,seen')
3.110 -      end
3.111 -  | lits_lg lits (lg,seen) = (lg,seen);
3.112 -
3.113 -fun dest_disj_aux (Const("Trueprop",_) \$ t) disjs = dest_disj_aux t disjs
3.114 -  | dest_disj_aux (Const ("op |", _) \$ t \$ t') disjs = dest_disj_aux t (dest_disj_aux t' disjs)
3.115 -  | dest_disj_aux t disjs = t::disjs;
3.116 -
3.117 -fun dest_disj t = dest_disj_aux t [];
3.118 -
3.119 -fun logic_of_clause tm = lits_lg (dest_disj tm);
3.120 -
3.121 -fun logic_of_clauses [] (lg,seen) = (lg,seen)
3.122 -  | logic_of_clauses (cls::clss) (FOL,seen) =
3.123 -    let val (lg,seen') = logic_of_clause cls (FOL,seen)
3.124 -        val _ =
3.125 -          if is_fol_logic lg then ()
3.126 -          else Output.debug (fn () => ("Found a HOL clause: " ^ Display.raw_string_of_term cls))
3.127 -    in
3.128 -        logic_of_clauses clss (lg,seen')
3.129 -    end
3.130 -  | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen);
3.131 -
3.132 -fun problem_logic_goals_aux [] (lg,seen) = lg
3.133 -  | problem_logic_goals_aux (subgoal::subgoals) (lg,seen) =
3.134 -    problem_logic_goals_aux subgoals (logic_of_clauses subgoal (lg,seen));
3.135 -
3.136 -fun problem_logic_goals subgoals = problem_logic_goals_aux subgoals (FOL,[]);
3.137 -
3.138 -fun is_fol_thms ths = ((fst(logic_of_clauses (map prop_of ths) (FOL,[]))) = FOL);
3.139
3.140  (***************************************************************)
3.141  (* Relevance Filtering                                         *)
3.142 @@ -544,7 +424,7 @@
3.143  fun hash_literal (Const("Not",_)\$P) = Word.notb(hashw_term(P,0w0))
3.144    | hash_literal P = hashw_term(P,0w0);
3.145
3.146 -fun hash_term t = Word.toIntX (xor_words (map hash_literal (dest_disj t)));
3.147 +fun hash_term t = Word.toIntX (xor_words (map hash_literal (HOLogic.disjuncts (strip_Trueprop t))));
3.148
3.149  fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);
3.150
3.151 @@ -705,9 +585,8 @@
3.152  val linkup_logic_mode = ref Auto;
3.153
3.154  (*Ensures that no higher-order theorems "leak out"*)
3.155 -fun restrict_to_logic thy logic cls =
3.156 -  if is_fol_logic logic then filter (Meson.is_fol_term thy o prop_of o fst) cls
3.157 -                        else cls;
3.158 +fun restrict_to_logic thy true cls = filter (Meson.is_fol_term thy o prop_of o fst) cls
3.159 +  | restrict_to_logic thy false cls = cls;
3.160
3.161  (**** Predicates to detect unwanted clauses (prolific or likely to cause unsoundness) ****)
3.162
3.163 @@ -752,17 +631,13 @@
3.164  val unwanted_types = ["Product_Type.unit","bool"];
3.165
3.166  fun unwanted t =
3.167 -    is_taut t orelse has_typed_var unwanted_types t orelse
3.168 -    forall too_general_equality (dest_disj t);
3.169 +  is_taut t orelse has_typed_var unwanted_types t orelse
3.170 +  forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t));
3.171
3.172  (*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and
3.173    likely to lead to unsound proofs.*)
3.174  fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
3.175
3.176 -fun tptp_writer thy logic = ResHolClause.tptp_write_file thy (logic=FOL);
3.177 -
3.178 -fun dfg_writer thy logic = ResHolClause.dfg_write_file thy (logic=FOL);
3.179 -
3.180  (*Called by the oracle-based methods declared in res_atp_methods.ML*)
3.181  fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
3.182      let val conj_cls = Meson.make_clauses conjectures
3.183 @@ -771,14 +646,14 @@
3.184          val goal_cls = conj_cls@hyp_cls
3.185          val goal_tms = map prop_of goal_cls
3.186          val thy = ProofContext.theory_of ctxt
3.187 -        val logic = case mode of
3.188 -                            Auto => problem_logic_goals [goal_tms]
3.189 -                          | Fol => FOL
3.190 -                          | Hol => HOL
3.191 +        val isFO = case mode of
3.192 +                            Auto => forall (Meson.is_fol_term thy) goal_tms
3.193 +                          | Fol => true
3.194 +                          | Hol => false
3.195          val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
3.196          val cla_simp_atp_clauses = included_thms
3.197                                       |> ResAxioms.cnf_rules_pairs |> make_unique
3.198 -                                     |> restrict_to_logic thy logic
3.199 +                                     |> restrict_to_logic thy isFO
3.200                                       |> remove_unwanted_clauses
3.201          val user_cls = ResAxioms.cnf_rules_pairs user_rules
3.202          val axclauses = make_unique (user_cls @ relevance_filter thy cla_simp_atp_clauses goal_tms)
3.203 @@ -789,11 +664,11 @@
3.204          (*TFrees in conjecture clauses; TVars in axiom clauses*)
3.205          val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers
3.206          val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
3.207 -        val writer = if dfg then dfg_writer else tptp_writer
3.208 +        val writer = if dfg then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file
3.209          and file = atp_input_file()
3.210          and user_lemmas_names = map #1 user_rules
3.211      in
3.212 -        writer thy logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
3.213 +        writer thy isFO goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
3.214          Output.debug (fn () => "Writing to " ^ file);
3.215          file
3.216      end;
3.217 @@ -866,13 +741,13 @@
3.218          | get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) ::
3.219                                           get_neg_subgoals gls (n+1)
3.220        val goal_cls = get_neg_subgoals goals 1
3.221 -      val logic = case !linkup_logic_mode of
3.222 -                Auto => problem_logic_goals (map (map prop_of) goal_cls)
3.223 -              | Fol => FOL
3.224 -              | Hol => HOL
3.225 +      val isFO = case !linkup_logic_mode of
3.226 +			  Auto => forall (Meson.is_fol_term thy) (map prop_of (List.concat goal_cls))
3.227 +			| Fol => true
3.228 +			| Hol => false
3.229        val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt chain_ths
3.230        val included_cls = included_thms |> ResAxioms.cnf_rules_pairs |> make_unique
3.231 -                                       |> restrict_to_logic thy logic
3.232 +                                       |> restrict_to_logic thy isFO
3.233                                         |> remove_unwanted_clauses
3.234        val _ = Output.debug (fn () => "included clauses = " ^ Int.toString(length included_cls))
3.235        val white_cls = ResAxioms.cnf_rules_pairs white_thms
3.236 @@ -880,7 +755,7 @@
3.237        val axcls_list = map (fn ngcls => white_cls @ relevance_filter thy included_cls (map prop_of ngcls)) goal_cls
3.238        val _ = app (fn axcls => Output.debug (fn () => "filtered clauses = " ^ Int.toString(length axcls)))
3.239                    axcls_list
3.240 -      val writer = if !prover = Recon.SPASS then dfg_writer else tptp_writer
3.241 +      val writer = if !prover = Recon.SPASS then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file
3.242        fun write_all [] [] _ = []
3.243          | write_all (ccls::ccls_list) (axcls::axcls_list) k =
3.244              let val fname = probfile k
3.245 @@ -901,7 +776,7 @@
3.246                  val _ = Output.debug (fn () => "arity clauses = " ^ Int.toString (length arity_clauses))
3.247                  val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
3.248                  val _ = Output.debug (fn () => "classrel clauses = " ^ Int.toString (length classrel_clauses))
3.249 -                val clnames = writer thy logic ccls fname (axcls,classrel_clauses,arity_clauses) []
3.250 +                val clnames = writer thy isFO ccls fname (axcls,classrel_clauses,arity_clauses) []
3.251                  val thm_names = Vector.fromList clnames
3.252                  val _ = if !Output.debugging then trace_vector fname thm_names else ()
3.253              in  (thm_names,fname) :: write_all ccls_list axcls_list (k+1)  end
```
```     4.1 --- a/src/HOL/Tools/res_reconstruct.ML	Thu Oct 11 15:57:29 2007 +0200
4.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Thu Oct 11 15:59:31 2007 +0200
4.3 @@ -282,12 +282,6 @@
4.4    let val vt0 = tfree_constraints_of_clauses Vartab.empty (map #3 tuples)
4.5    in  map (decode_tstp ctxt vt0) tuples  end;
4.6
4.7 -(*FIXME: simmilar function in res_atp. Move to HOLogic?*)
4.8 -fun dest_disj_aux (Const ("op |", _) \$ t \$ t') disjs = dest_disj_aux t (dest_disj_aux t' disjs)
4.9 -  | dest_disj_aux t disjs = t::disjs;
4.10 -
4.11 -fun dest_disj t = dest_disj_aux t [];
4.12 -
4.13  (** Finding a matching assumption. The literals may be permuted, and variable names
4.14      may disagree. We have to try all combinations of literals (quadratic!) and
4.15      match up the variable names consistently. **)
4.16 @@ -339,10 +333,10 @@
4.17    matches_aux [] (map Envir.eta_contract lits1) (map Envir.eta_contract lits2);
4.18
4.19  fun permuted_clause t =
4.20 -  let val lits = dest_disj t
4.21 +  let val lits = HOLogic.disjuncts t
4.22        fun perm [] = NONE
4.23          | perm (ctm::ctms) =
4.24 -            if matches (lits, dest_disj (HOLogic.dest_Trueprop (strip_alls ctm)))
4.25 +            if matches (lits, HOLogic.disjuncts (HOLogic.dest_Trueprop (strip_alls ctm)))
4.26              then SOME ctm else perm ctms
4.27    in perm end;
4.28
```
```     5.1 --- a/src/HOL/hologic.ML	Thu Oct 11 15:57:29 2007 +0200
5.2 +++ b/src/HOL/hologic.ML	Thu Oct 11 15:59:31 2007 +0200
5.3 @@ -31,6 +31,7 @@
5.4    val mk_not: term -> term
5.5    val dest_conj: term -> term list
5.6    val dest_disj: term -> term list
5.7 +  val disjuncts: term -> term list
5.8    val dest_imp: term -> term * term
5.9    val dest_not: term -> term
5.10    val dest_concls: term -> term list
5.11 @@ -184,6 +185,12 @@
5.12  fun dest_disj (Const ("op |", _) \$ t \$ t') = t :: dest_disj t'
5.13    | dest_disj t = [t];
5.14
5.15 +(*Like dest_disj, but flattens disjunctions however nested*)
5.16 +fun disjuncts_aux (Const ("op |", _) \$ t \$ t') disjs = disjuncts_aux t (disjuncts_aux t' disjs)
5.17 +  | disjuncts_aux t disjs = t::disjs;
5.18 +
5.19 +fun disjuncts t = disjuncts_aux t [];
5.20 +
5.21  fun dest_imp (Const("op -->",_) \$ A \$ B) = (A, B)
5.22    | dest_imp  t = raise TERM ("dest_imp", [t]);
5.23
```