author paulson Fri Nov 10 20:58:48 2006 +0100 (2006-11-10) changeset 21290 33b6bb5d6ab8 parent 21289 920b7b893d9c child 21291 d59cbb8ce002
Improvement to classrel clauses: now outputs the minimum needed.
Theorem names: trying to minimize the number of multiple theorem names presented
 src/HOL/Tools/res_atp.ML file | annotate | diff | revisions src/HOL/Tools/res_axioms.ML file | annotate | diff | revisions src/HOL/Tools/res_clause.ML file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Nov 10 19:04:18 2006 +0100
1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Nov 10 20:58:48 2006 +0100
1.3 @@ -72,7 +72,7 @@
1.4  fun set_prover atp =
1.5    case String.map Char.toLower atp of
1.6        "e" =>
1.7 -          (ReduceAxiomsN.max_new := 80;
1.8 +          (ReduceAxiomsN.max_new := 100;
1.9             ReduceAxiomsN.theory_const := false;
1.10             prover := "E")
1.11      | "spass" =>
1.12 @@ -585,11 +585,16 @@
1.13  fun multi_name a (th, (n,pairs)) =
1.14    (n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs)
1.15
1.16 -fun multi_names ((a, []), pairs) = pairs
1.17 -  | multi_names ((a, [th]), pairs) = (a,th)::pairs
1.18 -  | multi_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths);
1.19 +fun add_multi_names ((a, []), pairs) = pairs
1.20 +  | add_multi_names ((a, [th]), pairs) = (a,th)::pairs
1.21 +  | add_multi_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths);
1.22
1.23 -fun name_thm_pairs ctxt = foldl multi_names [] (all_valid_thms ctxt);
1.24 +fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
1.25 +
1.26 +(*The single theorems go BEFORE the multiple ones*)
1.27 +fun name_thm_pairs ctxt =
1.28 +  let val (mults,singles) = List.partition is_multi (all_valid_thms ctxt)
1.30
1.31  fun check_named ("",th) = (warning ("No name for theorem " ^ string_of_thm th); false)
1.32    | check_named (_,th) = true;
1.33 @@ -633,6 +638,24 @@
1.34        in  okthms end
1.35    else thms;
1.36
1.37 +(***************************************************************)
1.38 +(* Type Classes Present in the Axiom or Conjecture Clauses     *)
1.39 +(***************************************************************)
1.40 +
1.41 +fun setinsert (x,s) = Symtab.update (x,()) s;
1.42 +
1.43 +fun add_classes (sorts, cset) = foldl setinsert cset (List.concat sorts);
1.44 +
1.45 +(*Remove this trivial type class*)
1.46 +fun delete_type cset = Symtab.delete_safe "HOL.type" cset;
1.47 +
1.48 +fun tvar_classes_of_terms ts =
1.49 +  let val sorts_list = map (map #2 o term_tvars) ts
1.50 +  in  Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list))  end;
1.51 +
1.52 +fun tfree_classes_of_terms ts =
1.53 +  let val sorts_list = map (map #2 o term_tfrees) ts
1.54 +  in  Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list))  end;
1.55
1.56  (***************************************************************)
1.57  (* ATP invocation methods setup                                *)
1.58 @@ -681,7 +704,12 @@
1.59  	val axclauses = get_relevant_clauses thy cla_simp_atp_clauses
1.60  	                            user_cls (map prop_of goal_cls) |> make_unique
1.61  	val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol ()
1.62 -	val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
1.63 +        val subs = tfree_classes_of_terms (map prop_of goal_cls)
1.64 +        and supers = tvar_classes_of_terms (map (prop_of o #1) axclauses)
1.65 +        (*TFrees in conjecture clauses; TVars in axiom clauses*)
1.66 +        val classrel_clauses =
1.67 +              if keep_types then ResClause.make_classrel_clauses thy subs supers
1.68 +              else []
1.69  	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
1.70          val writer = if dfg then dfg_writer else tptp_writer
1.71  	and file = atp_input_file()
1.72 @@ -800,10 +828,6 @@
1.73                    axcls_list
1.74        val keep_types = if is_fol_logic logic then !ResClause.keep_types
1.75                         else is_typed_hol ()
1.76 -      val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy
1.77 -                             else []
1.78 -      val _ = Output.debug ("classrel clauses = " ^
1.79 -                            Int.toString (length classrel_clauses))
1.80        val arity_clauses = if keep_types then ResClause.arity_clause_thy thy
1.81                            else []
1.82        val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
1.83 @@ -813,6 +837,13 @@
1.84              let val fname = probfile k
1.85                  val axcls = make_unique axcls
1.86                  val ccls = subtract_cls ccls axcls
1.87 +                val subs = tfree_classes_of_terms (map prop_of ccls)
1.88 +                and supers = tvar_classes_of_terms (map (prop_of o #1) axcls)
1.89 +                (*TFrees in conjecture clauses; TVars in axiom clauses*)
1.90 +                val classrel_clauses =
1.91 +                      if keep_types then ResClause.make_classrel_clauses thy subs supers
1.92 +                      else []
1.93 +                val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
1.94                  val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) []
1.95                  val thm_names = Array.fromList clnames
1.96                  val _ = if !Output.show_debug_msgs
```
```     2.1 --- a/src/HOL/Tools/res_axioms.ML	Fri Nov 10 19:04:18 2006 +0100
2.2 +++ b/src/HOL/Tools/res_axioms.ML	Fri Nov 10 20:58:48 2006 +0100
2.3 @@ -647,7 +647,8 @@
2.4                         handle THM _ => pairs | ResClause.CLAUSE _ => pairs
2.5        in  cnf_rules_pairs_aux pairs' ths  end;
2.6
2.7 -val cnf_rules_pairs = cnf_rules_pairs_aux [];
2.8 +(*The combination of rev and tail recursion preserves the original order*)
2.9 +fun cnf_rules_pairs l = cnf_rules_pairs_aux [] (rev l);
2.10
2.11
2.12  (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)
```
```     3.1 --- a/src/HOL/Tools/res_clause.ML	Fri Nov 10 19:04:18 2006 +0100
3.2 +++ b/src/HOL/Tools/res_clause.ML	Fri Nov 10 20:58:48 2006 +0100
3.3 @@ -23,7 +23,7 @@
3.4    val arity_clause_thy: theory -> arityClause list
3.5    val ascii_of : string -> string
3.6    val bracket_pack : string list -> string
3.7 -  val classrel_clauses_thy: theory -> classrelClause list
3.8 +  val make_classrel_clauses: theory -> class list -> class list -> classrelClause list
3.9    val clause_prefix : string
3.10    val clause2tptp : clause -> string * string list
3.11    val const_prefix : string
3.12 @@ -529,23 +529,22 @@
3.13  	 ClassrelClause of {axiom_name: axiom_name,
3.14  			    subclass: class,
3.15  			    superclass: class};
3.16 -
3.17 -fun make_axiom_classrelClause n subclass superclass =
3.18 -  ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of subclass ^
3.19 -                                "_" ^ Int.toString n,
3.20 -                  subclass = make_type_class subclass,
3.21 -                  superclass = make_type_class superclass};
3.22 +
3.23 +(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
3.24 +fun class_pairs thy subs supers =
3.25 +  let val class_less = Sorts.class_less(Sign.classes_of thy)
3.26 +      fun add_super sub (super,pairs) =
3.27 +            if class_less (sub,super) then (sub,super)::pairs else pairs
3.29 +  in  foldl add_supers [] subs  end;
3.30
3.31 -fun classrelClauses_of_aux n sub [] = []
3.32 -  | classrelClauses_of_aux n sub ("HOL.type"::sups) = (*Should be ignored*)
3.33 -      classrelClauses_of_aux n sub sups
3.34 -  | classrelClauses_of_aux n sub (sup::sups) =
3.35 -      make_axiom_classrelClause n sub sup :: classrelClauses_of_aux (n+1) sub sups;
3.36 +fun make_classrelClause (sub,super) =
3.37 +  ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of sub ^ "_" ^ ascii_of super,
3.38 +                  subclass = make_type_class sub,
3.39 +                  superclass = make_type_class super};
3.40
3.41 -fun classrelClauses_of (sub,sups) = classrelClauses_of_aux 0 sub sups;
3.42 -
3.43 -val classrel_clauses_thy =
3.44 -  maps classrelClauses_of o Graph.dest o #classes o Sorts.rep_algebra o Sign.classes_of;
3.45 +fun make_classrel_clauses thy subs supers =
3.46 +  map make_classrelClause (class_pairs thy subs supers);
3.47
3.48
3.49  (** Isabelle arities **)
```