Tidied up some programs.
authormengj
Tue Apr 18 05:36:38 2006 +0200 (2006-04-18 ago)
changeset 19442ad8bb8346e51
parent 19441 a479b800cc8c
child 19443 e32a4703d834
Tidied up some programs.
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Sun Apr 16 08:22:29 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Apr 18 05:36:38 2006 +0200
     1.3 @@ -313,18 +313,6 @@
     1.4      end
     1.5    | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen);
     1.6  
     1.7 -fun logic_of_nclauses [] (lg,seen) = (lg,seen)
     1.8 -  | logic_of_nclauses (cls::clss) (FOL,seen) =
     1.9 -    logic_of_nclauses clss (logic_of_clauses (snd cls) (FOL,seen))
    1.10 -  | logic_of_nclauses clss (lg,seen) = (lg,seen);
    1.11 -
    1.12 -fun problem_logic (goal_cls,rules_cls) =
    1.13 -    let val (lg1,seen1) = logic_of_clauses goal_cls (FOL,[])
    1.14 -	val (lg2,seen2) = logic_of_nclauses rules_cls (lg1,seen1)
    1.15 -    in
    1.16 -	lg2
    1.17 -    end;
    1.18 -
    1.19  fun problem_logic_goals_aux [] (lg,seen) = lg
    1.20    | problem_logic_goals_aux (subgoal::subgoals) (lg,seen) = 
    1.21      problem_logic_goals_aux subgoals (logic_of_clauses subgoal (lg,seen));
    1.22 @@ -360,13 +348,13 @@
    1.23  
    1.24  
    1.25  fun write_subgoal_file mode ctxt conjectures user_thms n =
    1.26 -    let val conj_cls = map prop_of (make_clauses conjectures) 
    1.27 -	val hyp_cls = map prop_of (cnf_hyps_thms ctxt)
    1.28 +    let val conj_cls = make_clauses conjectures 
    1.29 +	val hyp_cls = cnf_hyps_thms ctxt
    1.30  	val goal_cls = conj_cls@hyp_cls
    1.31  	val user_rules = map ResAxioms.pairname user_thms
    1.32 -	val (names_arr,axclauses_as_thms) = ResClasimp.get_clasimp_atp_lemmas ctxt (goal_cls) user_rules (!include_claset,!include_simpset,!include_atpset) (!run_relevance_filter)  
    1.33 +	val (names_arr,axclauses_as_thms) = ResClasimp.get_clasimp_atp_lemmas ctxt (map prop_of goal_cls) user_rules (!include_claset,!include_simpset,!include_atpset) (!run_relevance_filter)  
    1.34  	val thy = ProofContext.theory_of ctxt
    1.35 -	val prob_logic = case mode of Auto => problem_logic_goals [goal_cls]
    1.36 +	val prob_logic = case mode of Auto => problem_logic_goals [map prop_of goal_cls]
    1.37  				    | Fol => FOL
    1.38  				    | Hol => HOL
    1.39  	val keep_types = if is_fol_logic prob_logic then !fol_keep_types else is_typed_hol ()
    1.40 @@ -465,7 +453,7 @@
    1.41  fun write_problem_files pf (ctxt,th)  =
    1.42    let val goals = Thm.prems_of th
    1.43        val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
    1.44 -      val (names_arr, axclauses_as_terms) = ResClasimp.get_clasimp_atp_lemmas ctxt goals [] (true,true,true) (!run_relevance_filter) (* no user supplied rules here, because no user invocation *)
    1.45 +      val (names_arr, axclauses) = ResClasimp.get_clasimp_atp_lemmas ctxt goals [] (true,true,true) (!run_relevance_filter) (* no user supplied rules here, because no user invocation *)
    1.46        val _ = Output.debug ("claset, simprules and atprules total clauses = " ^ 
    1.47                       Int.toString (Array.length names_arr))
    1.48        val thy = ProofContext.theory_of ctxt
    1.49 @@ -475,12 +463,12 @@
    1.50  	      let val st = Seq.hd (EVERY'
    1.51  				       [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac] n th)
    1.52  		  val negs = Option.valOf (metahyps_thms n st)
    1.53 -		  val negs_clauses = map prop_of (make_clauses negs)
    1.54 +		  val negs_clauses = make_clauses negs
    1.55  	      in
    1.56  		  negs_clauses::(get_neg_subgoals (n - 1))
    1.57  	      end
    1.58        val neg_subgoals = get_neg_subgoals (length goals) 
    1.59 -      val goals_logic = case !linkup_logic_mode of Auto => problem_logic_goals neg_subgoals
    1.60 +      val goals_logic = case !linkup_logic_mode of Auto => problem_logic_goals (map (map prop_of) neg_subgoals)
    1.61  						 | Fol => FOL
    1.62  						 | Hol => HOL
    1.63        val keep_types = if is_fol_logic goals_logic then !ResClause.keep_types else is_typed_hol ()
    1.64 @@ -491,7 +479,7 @@
    1.65        val writer = (*if !prover ~= "spass" then *)tptp_writer 
    1.66        fun write_all [] _ = []
    1.67  	| write_all (subgoal::subgoals) k =
    1.68 -	  (writer goals_logic subgoal (pf k) (axclauses_as_terms,classrel_clauses,arity_clauses); pf k):: (write_all subgoals (k - 1))
    1.69 +	  (writer goals_logic subgoal (pf k) (axclauses,classrel_clauses,arity_clauses); pf k):: (write_all subgoals (k - 1))
    1.70    in
    1.71        (write_all neg_subgoals (length goals), names_arr)
    1.72    end;
     2.1 --- a/src/HOL/Tools/res_axioms.ML	Sun Apr 16 08:22:29 2006 +0200
     2.2 +++ b/src/HOL/Tools/res_axioms.ML	Tue Apr 18 05:36:38 2006 +0200
     2.3 @@ -12,22 +12,15 @@
     2.4    val elimRule_tac : thm -> Tactical.tactic
     2.5    val elimR2Fol : thm -> term
     2.6    val transform_elim : thm -> thm
     2.7 -  val clausify_axiom_pairs : (string*thm) -> (ResClause.clause*thm) list
     2.8 -  val clausify_axiom_pairsH : (string*thm) -> (ResHolClause.clause*thm) list
     2.9    val cnf_axiom : (string * thm) -> thm list
    2.10    val meta_cnf_axiom : thm -> thm list
    2.11    val claset_rules_of_thy : theory -> (string * thm) list
    2.12    val simpset_rules_of_thy : theory -> (string * thm) list
    2.13    val claset_rules_of_ctxt: Proof.context -> (string * thm) list
    2.14    val simpset_rules_of_ctxt : Proof.context -> (string * thm) list
    2.15 -  val clausify_rules_pairs : (string*thm) list -> (ResClause.clause*thm) list list
    2.16 -  val clausify_rules_pairsH : (string*thm) list -> (ResHolClause.clause*thm) list list
    2.17    val pairname : thm -> (string * thm)
    2.18    val skolem_thm : thm -> thm list
    2.19 -  val cnf_rules1 : (string * thm) list -> string list -> (string * thm list) list * string list
    2.20 -  val cnf_rules2 : (string * thm) list -> string list -> (string * term list) list * string list
    2.21    val cnf_rules_pairs : (string * Thm.thm) list -> (Thm.thm * (string * int)) list list;
    2.22 -  val clausify_rules_pairs_abs : (string * thm) list -> (Term.term * (string * int)) list list
    2.23    val meson_method_setup : theory -> theory
    2.24    val setup : theory -> theory
    2.25  
    2.26 @@ -391,19 +384,6 @@
    2.27  (*works for both FOL and HOL*)
    2.28  val cnf_rules = cnf_rules_g cnf_axiom;
    2.29  
    2.30 -fun cnf_rules1 [] err_list = ([],err_list)
    2.31 -  | cnf_rules1 ((name,th) :: ths) err_list =
    2.32 -      let val (ts,es) = cnf_rules1 ths err_list
    2.33 -      in ((name,cnf_axiom (name,th)) :: ts,es) handle _ => (ts,(name::es)) end;
    2.34 -
    2.35 -fun cnf_rules2 [] err_list = ([],err_list)
    2.36 -  | cnf_rules2 ((name,th) :: ths) err_list =
    2.37 -      let val (ts,es) = cnf_rules2 ths err_list
    2.38 -      in
    2.39 -	((name,map prop_of (cnf_axiom (name,th))) :: ts,es) handle _ => (ts,(name::es)) 
    2.40 -      end;
    2.41 -
    2.42 -
    2.43  fun cnf_rules_pairs_aux [] = []
    2.44    | cnf_rules_pairs_aux ((name,th)::ths) =
    2.45      let val ts = cnf_rules_pairs_aux ths
    2.46 @@ -418,70 +398,9 @@
    2.47  
    2.48  fun cnf_rules_pairs thms = rev (cnf_rules_pairs_aux thms);
    2.49  
    2.50 -fun clausify_rules_pairs_abs_aux [] = []
    2.51 -  | clausify_rules_pairs_abs_aux ((name,th)::ths) =
    2.52 -      let val ts = clausify_rules_pairs_abs_aux ths
    2.53 -	  fun pair_name_cls k (n, []) = []
    2.54 -	    | pair_name_cls k (n, cls::clss) =
    2.55 -		(prop_of cls, (n,k)) :: (pair_name_cls (k+1) (n, clss))
    2.56 -      in
    2.57 -	  pair_name_cls 0 (name, (cnf_axiom(name,th))) :: ts
    2.58 -	  handle THM _ => ts | ResClause.CLAUSE _ => ts | ResHolClause.LAM2COMB _ => ts
    2.59 -      end;
    2.60 -
    2.61 -fun clausify_rules_pairs_abs thms = rev (clausify_rules_pairs_abs_aux thms);
    2.62 -
    2.63  
    2.64  (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)
    2.65  
    2.66 -fun make_axiom_clauses _ _ [] = []
    2.67 -  | make_axiom_clauses name i (th::ths) =
    2.68 -      case ResClause.make_axiom_clause (prop_of th) (name,i) of 
    2.69 -          SOME cls => (cls, th) :: make_axiom_clauses name (i+1) ths
    2.70 -        | NONE => make_axiom_clauses name i ths;
    2.71 -
    2.72 -(* outputs a list of (clause,theorem) pairs *)
    2.73 -fun clausify_axiom_pairs (name,th) = 
    2.74 -    filter (fn (c,th) => not (ResClause.isTaut c))
    2.75 -           (make_axiom_clauses name 0 (cnf_axiom (name,th)));
    2.76 -
    2.77 -fun make_axiom_clausesH _ _ [] = []
    2.78 -  | make_axiom_clausesH name i (th::ths) =
    2.79 -      (ResHolClause.make_axiom_clause (prop_of th) (name,i), th) ::
    2.80 -      (make_axiom_clausesH name (i+1) ths)
    2.81 -
    2.82 -fun clausify_axiom_pairsH (name,th) = 
    2.83 -    filter (fn (c,th) => not (ResHolClause.isTaut c))
    2.84 -           (make_axiom_clausesH name 0 (cnf_axiom (name,th)));
    2.85 -
    2.86 -
    2.87 -fun clausify_rules_pairs_aux result [] = result
    2.88 -  | clausify_rules_pairs_aux result ((name,th)::ths) =
    2.89 -      clausify_rules_pairs_aux (clausify_axiom_pairs (name,th) :: result) ths
    2.90 -      handle THM (msg,_,_) =>  
    2.91 -	      (Output.debug ("Cannot clausify " ^ name ^ ": " ^ msg); 
    2.92 -	       clausify_rules_pairs_aux result ths)
    2.93 -	 |  ResClause.CLAUSE (msg,t) => 
    2.94 -	      (Output.debug ("Cannot clausify " ^ name ^ ": " ^ msg ^
    2.95 -		      ": " ^ TermLib.string_of_term t); 
    2.96 -	       clausify_rules_pairs_aux result ths)
    2.97 -
    2.98 -
    2.99 -fun clausify_rules_pairs_auxH result [] = result
   2.100 -  | clausify_rules_pairs_auxH result ((name,th)::ths) =
   2.101 -      clausify_rules_pairs_auxH (clausify_axiom_pairsH (name,th) :: result) ths
   2.102 -      handle THM (msg,_,_) =>  
   2.103 -	      (Output.debug ("Cannot clausify " ^ name ^ ": " ^ msg); 
   2.104 -	       clausify_rules_pairs_auxH result ths)
   2.105 -	 |  ResHolClause.LAM2COMB (t) => 
   2.106 -	      (Output.debug ("Cannot clausify "  ^ TermLib.string_of_term t); 
   2.107 -	       clausify_rules_pairs_auxH result ths)
   2.108 -
   2.109 -
   2.110 -
   2.111 -val clausify_rules_pairs = clausify_rules_pairs_aux [];
   2.112 -
   2.113 -val clausify_rules_pairsH = clausify_rules_pairs_auxH [];
   2.114  
   2.115  (*These should include any plausibly-useful theorems, especially if they need
   2.116    Skolem functions. FIXME: this list is VERY INCOMPLETE*)