rationalized redundant code
authorpaulson
Thu Oct 11 15:59:31 2007 +0200 (2007-10-11)
changeset 24958ff15f76741bd
parent 24957 50959112a4e1
child 24959 119793c84647
rationalized redundant code
src/HOL/Tools/cnf_funcs.ML
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_reconstruct.ML
src/HOL/hologic.ML
     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.5      Copyright   2005-2006
     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.17          val lmap = foldl (add_thm false ctxt) (add_tfrees lmap0) ths
    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.12  fun add_atpset() = include_atpset:=true;
    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