src/HOL/Tools/res_axioms.ML
author haftmann
Wed Jan 31 16:05:10 2007 +0100 (2007-01-31)
changeset 22218 30a8890d2967
parent 22130 0906fd95e0b5
child 22345 85f76b341893
permissions -rw-r--r--
dropped lemma duplicates in HOL.thy
     1 (*  Author: Jia Meng, Cambridge University Computer Laboratory
     2     ID: $Id$
     3     Copyright 2004 University of Cambridge
     4 
     5 Transformation of axiom rules (elim/intro/etc) into CNF forms.
     6 *)
     7 
     8 signature RES_AXIOMS =
     9 sig
    10   val trace_abs: bool ref
    11   val cnf_axiom : string * thm -> thm list
    12   val cnf_name : string -> thm list
    13   val meta_cnf_axiom : thm -> thm list
    14   val pairname : thm -> string * thm
    15   val skolem_thm : thm -> thm list
    16   val to_nnf : thm -> thm
    17   val cnf_rules_pairs : (string * thm) list -> (thm * (string * int)) list
    18   val meson_method_setup : theory -> theory
    19   val setup : theory -> theory
    20   val assume_abstract_list: thm list -> thm list
    21   val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list
    22   val claset_rules_of: Proof.context -> (string * thm) list   (*FIXME DELETE*)
    23   val simpset_rules_of: Proof.context -> (string * thm) list  (*FIXME DELETE*)
    24   val atpset_rules_of: Proof.context -> (string * thm) list
    25 end;
    26 
    27 structure ResAxioms =
    28 struct
    29 
    30 (*For running the comparison between combinators and abstractions.
    31   CANNOT be a ref, as the setting is used while Isabelle is built.
    32   Currently FALSE, i.e. all the "abstraction" code below is unused, but so far
    33   it seems to be inferior to combinators...*)
    34 val abstract_lambdas = true;
    35 
    36 val trace_abs = ref false;
    37 
    38 (* FIXME legacy *)
    39 fun freeze_thm th = #1 (Drule.freeze_thaw th);
    40 
    41 val lhs_of = #1 o Logic.dest_equals o Thm.prop_of;
    42 val rhs_of = #2 o Logic.dest_equals o Thm.prop_of;
    43 
    44 
    45 (*Store definitions of abstraction functions, ensuring that identical right-hand
    46   sides are denoted by the same functions and thereby reducing the need for
    47   extensionality in proofs.
    48   FIXME!  Store in theory data!!*)
    49 
    50 (*Populate the abstraction cache with common combinators.*)
    51 fun seed th net =
    52   let val (_,ct) = Thm.dest_abs NONE (Drule.rhs_of th)
    53       val t = Logic.legacy_varify (term_of ct)
    54   in  Net.insert_term eq_thm (t, th) net end;
    55   
    56 val abstraction_cache = ref 
    57       (seed (thm"ATP_Linkup.I_simp") 
    58        (seed (thm"ATP_Linkup.B_simp") 
    59 	(seed (thm"ATP_Linkup.K_simp") Net.empty)));
    60 
    61 
    62 (**** Transformation of Elimination Rules into First-Order Formulas****)
    63 
    64 val cfalse = cterm_of HOL.thy HOLogic.false_const;
    65 val ctp_false = cterm_of HOL.thy (HOLogic.mk_Trueprop HOLogic.false_const);
    66 
    67 (*Converts an elim-rule into an equivalent theorem that does not have the
    68   predicate variable.  Leaves other theorems unchanged.  We simply instantiate the
    69   conclusion variable to False.*)
    70 fun transform_elim th =
    71   case concl_of th of    (*conclusion variable*)
    72        Const("Trueprop",_) $ (v as Var(_,Type("bool",[]))) => 
    73            Thm.instantiate ([], [(cterm_of HOL.thy v, cfalse)]) th
    74     | v as Var(_, Type("prop",[])) => 
    75            Thm.instantiate ([], [(cterm_of HOL.thy v, ctp_false)]) th
    76     | _ => th;
    77 
    78 (**** Transformation of Clasets and Simpsets into First-Order Axioms ****)
    79 
    80 (*Transfer a theorem into theory ATP_Linkup.thy if it is not already
    81   inside that theory -- because it's needed for Skolemization *)
    82 
    83 (*This will refer to the final version of theory ATP_Linkup.*)
    84 val recon_thy_ref = Theory.self_ref (the_context ());
    85 
    86 (*If called while ATP_Linkup is being created, it will transfer to the
    87   current version. If called afterward, it will transfer to the final version.*)
    88 fun transfer_to_ATP_Linkup th =
    89     transfer (Theory.deref recon_thy_ref) th handle THM _ => th;
    90 
    91 
    92 (**** SKOLEMIZATION BY INFERENCE (lcp) ****)
    93 
    94 (*Traverse a theorem, declaring Skolem function definitions. String s is the suggested
    95   prefix for the Skolem constant. Result is a new theory*)
    96 fun declare_skofuns s th thy =
    97   let val nref = ref 0
    98       fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (thy, axs) =
    99             (*Existential: declare a Skolem function, then insert into body and continue*)
   100             let val cname = Name.internal (s ^ "_sko" ^ Int.toString (inc nref))
   101                 val args = term_frees xtp  (*get the formal parameter list*)
   102                 val Ts = map type_of args
   103                 val cT = Ts ---> T
   104                 val c = Const (Sign.full_name thy cname, cT)
   105                 val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
   106                         (*Forms a lambda-abstraction over the formal parameters*)
   107                 val thy' = Sign.add_consts_authentic [(cname, cT, NoSyn)] thy
   108                            (*Theory is augmented with the constant, then its def*)
   109                 val cdef = cname ^ "_def"
   110                 val thy'' = Theory.add_defs_i false false [(cdef, equals cT $ c $ rhs)] thy'
   111             in dec_sko (subst_bound (list_comb(c,args), p))
   112                        (thy'', get_axiom thy'' cdef :: axs)
   113             end
   114         | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) thx =
   115             (*Universal quant: insert a free variable into body and continue*)
   116             let val fname = Name.variant (add_term_names (p,[])) a
   117             in dec_sko (subst_bound (Free(fname,T), p)) thx end
   118         | dec_sko (Const ("op &", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
   119         | dec_sko (Const ("op |", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
   120         | dec_sko (Const ("Trueprop", _) $ p) thx = dec_sko p thx
   121         | dec_sko t thx = thx (*Do nothing otherwise*)
   122   in  dec_sko (prop_of th) (thy,[])  end;
   123 
   124 (*Traverse a theorem, accumulating Skolem function definitions.*)
   125 fun assume_skofuns th =
   126   let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
   127             (*Existential: declare a Skolem function, then insert into body and continue*)
   128             let val skos = map (#1 o Logic.dest_equals) defs  (*existing sko fns*)
   129                 val args = term_frees xtp \\ skos  (*the formal parameters*)
   130                 val Ts = map type_of args
   131                 val cT = Ts ---> T
   132                 val c = Free (gensym "sko_", cT)
   133                 val rhs = list_abs_free (map dest_Free args,
   134                                          HOLogic.choice_const T $ xtp)
   135                       (*Forms a lambda-abstraction over the formal parameters*)
   136                 val def = equals cT $ c $ rhs
   137             in dec_sko (subst_bound (list_comb(c,args), p))
   138                        (def :: defs)
   139             end
   140         | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) defs =
   141             (*Universal quant: insert a free variable into body and continue*)
   142             let val fname = Name.variant (add_term_names (p,[])) a
   143             in dec_sko (subst_bound (Free(fname,T), p)) defs end
   144         | dec_sko (Const ("op &", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
   145         | dec_sko (Const ("op |", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
   146         | dec_sko (Const ("Trueprop", _) $ p) defs = dec_sko p defs
   147         | dec_sko t defs = defs (*Do nothing otherwise*)
   148   in  dec_sko (prop_of th) []  end;
   149 
   150 
   151 (**** REPLACING ABSTRACTIONS BY FUNCTION DEFINITIONS ****)
   152 
   153 (*Returns the vars of a theorem*)
   154 fun vars_of_thm th =
   155   map (Thm.cterm_of (theory_of_thm th) o Var) (Drule.fold_terms Term.add_vars th []);
   156 
   157 (*Make a version of fun_cong with a given variable name*)
   158 local
   159     val fun_cong' = fun_cong RS asm_rl; (*renumber f, g to prevent clashes with (a,0)*)
   160     val cx = hd (vars_of_thm fun_cong');
   161     val ty = typ_of (ctyp_of_term cx);
   162     val thy = theory_of_thm fun_cong;
   163     fun mkvar a = cterm_of thy (Var((a,0),ty));
   164 in
   165 fun xfun_cong x = Thm.instantiate ([], [(cx, mkvar x)]) fun_cong'
   166 end;
   167 
   168 (*Removes the lambdas from an equation of the form t = (%x. u).  A non-negative n,
   169   serves as an upper bound on how many to remove.*)
   170 fun strip_lambdas 0 th = th
   171   | strip_lambdas n th = 
   172       case prop_of th of
   173 	  _ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) =>
   174 	      strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x))
   175 	| _ => th;
   176 
   177 (*Convert meta- to object-equality. Fails for theorems like split_comp_eq,
   178   where some types have the empty sort.*)
   179 val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq";
   180 fun mk_object_eq th = th RS meta_eq_to_obj_eq
   181     handle THM _ => error ("Theorem contains empty sort: " ^ string_of_thm th);
   182 
   183 (*Apply a function definition to an argument, beta-reducing the result.*)
   184 fun beta_comb cf x =
   185   let val th1 = combination cf (reflexive x)
   186       val th2 = beta_conversion false (Drule.rhs_of th1)
   187   in  transitive th1 th2  end;
   188 
   189 (*Apply a function definition to arguments, beta-reducing along the way.*)
   190 fun list_combination cf [] = cf
   191   | list_combination cf (x::xs) = list_combination (beta_comb cf x) xs;
   192 
   193 fun list_cabs ([] ,     t) = t
   194   | list_cabs (v::vars, t) = Thm.cabs v (list_cabs(vars,t));
   195 
   196 fun assert_eta_free ct =
   197   let val t = term_of ct
   198   in if (t aconv Envir.eta_contract t) then ()
   199      else error ("Eta redex in term: " ^ string_of_cterm ct)
   200   end;
   201 
   202 fun eq_absdef (th1, th2) =
   203     Context.joinable (theory_of_thm th1, theory_of_thm th2)  andalso
   204     rhs_of th1 aconv rhs_of th2;
   205 
   206 fun lambda_free (Abs _) = false
   207   | lambda_free (t $ u) = lambda_free t andalso lambda_free u
   208   | lambda_free _ = true;
   209 
   210 fun monomorphic t =
   211   Term.fold_types (Term.fold_atyps (fn TVar _ => K false | _ => I)) t true;
   212 
   213 fun dest_abs_list ct =
   214   let val (cv,ct') = Thm.dest_abs NONE ct
   215       val (cvs,cu) = dest_abs_list ct'
   216   in (cv::cvs, cu) end
   217   handle CTERM _ => ([],ct);
   218 
   219 fun lambda_list [] u = u
   220   | lambda_list (v::vs) u = lambda v (lambda_list vs u);
   221 
   222 fun abstract_rule_list [] [] th = th
   223   | abstract_rule_list (v::vs) (ct::cts) th = abstract_rule v ct (abstract_rule_list vs cts th)
   224   | abstract_rule_list _ _ th = raise THM ("abstract_rule_list", 0, [th]);
   225 
   226 
   227 val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0
   228 
   229 (*Does an existing abstraction definition have an RHS that matches the one we need now?
   230   thy is the current theory, which must extend that of theorem th.*)
   231 fun match_rhs thy t th =
   232   let val _ = if !trace_abs then warning ("match_rhs: " ^ string_of_cterm (cterm_of thy t) ^ 
   233                                           " against\n" ^ string_of_thm th) else ();
   234       val (tyenv,tenv) = Pattern.first_order_match thy (rhs_of th, t) (tyenv0,tenv0)
   235       val term_insts = map Meson.term_pair_of (Vartab.dest tenv)
   236       val ct_pairs = if subthy (theory_of_thm th, thy) andalso 
   237                         forall lambda_free (map #2 term_insts) 
   238                      then map (pairself (cterm_of thy)) term_insts
   239                      else raise Pattern.MATCH (*Cannot allow lambdas in the instantiation*)
   240       fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T)
   241       val th' = cterm_instantiate ct_pairs th
   242   in  SOME (th, instantiate (map ctyp2 (Vartab.dest tyenv), []) th')  end
   243   handle _ => NONE;
   244 
   245 (*Traverse a theorem, declaring abstraction function definitions. String s is the suggested
   246   prefix for the constants. Resulting theory is returned in the first theorem. *)
   247 fun declare_absfuns th =
   248   let fun abstract thy ct =
   249         if lambda_free (term_of ct) then (transfer thy (reflexive ct), [])
   250         else
   251         case term_of ct of
   252           Abs _ =>
   253             let val cname = Name.internal (gensym "abs_");
   254                 val _ = assert_eta_free ct;
   255                 val (cvs,cta) = dest_abs_list ct
   256                 val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs)
   257                 val _ = if !trace_abs then warning ("Nested lambda: " ^ string_of_cterm cta) else ();
   258                 val (u'_th,defs) = abstract thy cta
   259                 val _ = if !trace_abs then warning ("Returned " ^ string_of_thm u'_th) else ();
   260                 val cu' = Drule.rhs_of u'_th
   261                 val u' = term_of cu'
   262                 val abs_v_u = lambda_list (map term_of cvs) u'
   263                 (*get the formal parameters: ALL variables free in the term*)
   264                 val args = term_frees abs_v_u
   265                 val _ = if !trace_abs then warning (Int.toString (length args) ^ " arguments") else ();
   266                 val rhs = list_abs_free (map dest_Free args, abs_v_u)
   267                       (*Forms a lambda-abstraction over the formal parameters*)
   268                 val _ = if !trace_abs then warning ("Looking up " ^ string_of_cterm cu') else ();
   269                 val thy = theory_of_thm u'_th
   270                 val (ax,ax',thy) =
   271                  case List.mapPartial (match_rhs thy abs_v_u) 
   272                          (Net.match_term (!abstraction_cache) u') of
   273                      (ax,ax')::_ => 
   274                        (if !trace_abs then warning ("Re-using axiom " ^ string_of_thm ax) else ();
   275                         (ax,ax',thy))
   276                    | [] =>
   277                       let val _ = if !trace_abs then warning "Lookup was empty" else ();
   278                           val Ts = map type_of args
   279                           val cT = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu'))
   280                           val c = Const (Sign.full_name thy cname, cT)
   281                           val thy = Sign.add_consts_authentic [(cname, cT, NoSyn)] thy
   282                                      (*Theory is augmented with the constant,
   283                                        then its definition*)
   284                           val cdef = cname ^ "_def"
   285                           val thy = Theory.add_defs_i false false
   286                                        [(cdef, equals cT $ c $ rhs)] thy
   287                           val _ = if !trace_abs then (warning ("Definition is " ^ 
   288                                                       string_of_thm (get_axiom thy cdef))) 
   289                                   else ();
   290                           val ax = get_axiom thy cdef |> freeze_thm
   291                                      |> mk_object_eq |> strip_lambdas (length args)
   292                                      |> mk_meta_eq |> Meson.generalize
   293                           val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax)
   294                           val _ = if !trace_abs then 
   295                                     (warning ("Declaring: " ^ string_of_thm ax);
   296                                      warning ("Instance: " ^ string_of_thm ax')) 
   297                                   else ();
   298                           val _ = abstraction_cache := Net.insert_term eq_absdef 
   299                                             ((Logic.varify u'), ax) (!abstraction_cache)
   300                             handle Net.INSERT =>
   301                               raise THM ("declare_absfuns: INSERT", 0, [th,u'_th,ax])
   302                        in  (ax,ax',thy)  end
   303             in if !trace_abs then warning ("Lookup result: " ^ string_of_thm ax') else ();
   304                (transitive (abstract_rule_list vs cvs u'_th) (symmetric ax'), ax::defs) end
   305         | (t1$t2) =>
   306             let val (ct1,ct2) = Thm.dest_comb ct
   307                 val (th1,defs1) = abstract thy ct1
   308                 val (th2,defs2) = abstract (theory_of_thm th1) ct2
   309             in  (combination th1 th2, defs1@defs2)  end
   310       val _ = if !trace_abs then warning ("declare_absfuns, Abstracting: " ^ string_of_thm th) else ();
   311       val (eqth,defs) = abstract (theory_of_thm th) (cprop_of th)
   312       val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs
   313       val _ = if !trace_abs then warning ("declare_absfuns, Result: " ^ string_of_thm (hd ths)) else ();
   314   in  (theory_of_thm eqth, map Drule.eta_contraction_rule ths)  end;
   315 
   316 fun name_of def = try (#1 o dest_Free o lhs_of) def;
   317 
   318 (*A name is valid provided it isn't the name of a defined abstraction.*)
   319 fun valid_name defs (Free(x,T)) = not (x mem_string (List.mapPartial name_of defs))
   320   | valid_name defs _ = false;
   321 
   322 fun assume_absfuns th =
   323   let val thy = theory_of_thm th
   324       val cterm = cterm_of thy
   325       fun abstract ct =
   326         if lambda_free (term_of ct) then (reflexive ct, [])
   327         else
   328         case term_of ct of
   329           Abs (_,T,u) =>
   330             let val _ = assert_eta_free ct;
   331                 val (cvs,cta) = dest_abs_list ct
   332                 val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs)
   333                 val (u'_th,defs) = abstract cta
   334                 val cu' = Drule.rhs_of u'_th
   335                 val u' = term_of cu'
   336                 (*Could use Thm.cabs instead of lambda to work at level of cterms*)
   337                 val abs_v_u = lambda_list (map term_of cvs) (term_of cu')
   338                 (*get the formal parameters: free variables not present in the defs
   339                   (to avoid taking abstraction function names as parameters) *)
   340                 val args = filter (valid_name defs) (term_frees abs_v_u)
   341                 val crhs = list_cabs (map cterm args, cterm abs_v_u)
   342                       (*Forms a lambda-abstraction over the formal parameters*)
   343                 val rhs = term_of crhs
   344                 val (ax,ax') =
   345                  case List.mapPartial (match_rhs thy abs_v_u) 
   346                         (Net.match_term (!abstraction_cache) u') of
   347                      (ax,ax')::_ => 
   348                        (if !trace_abs then warning ("Re-using axiom " ^ string_of_thm ax) else ();
   349                         (ax,ax'))
   350                    | [] =>
   351                       let val Ts = map type_of args
   352                           val const_ty = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu'))
   353                           val c = Free (gensym "abs_", const_ty)
   354                           val ax = assume (Thm.capply (cterm (equals const_ty $ c)) crhs)
   355                                      |> mk_object_eq |> strip_lambdas (length args)
   356                                      |> mk_meta_eq |> Meson.generalize
   357                           val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax)
   358                           val _ = abstraction_cache := Net.insert_term eq_absdef (rhs,ax)
   359                                     (!abstraction_cache)
   360                             handle Net.INSERT =>
   361                               raise THM ("assume_absfuns: INSERT", 0, [th,u'_th,ax])
   362                       in (ax,ax') end
   363             in if !trace_abs then warning ("Lookup result: " ^ string_of_thm ax') else ();
   364                (transitive (abstract_rule_list vs cvs u'_th) (symmetric ax'), ax::defs) end
   365         | (t1$t2) =>
   366             let val (ct1,ct2) = Thm.dest_comb ct
   367                 val (t1',defs1) = abstract ct1
   368                 val (t2',defs2) = abstract ct2
   369             in  (combination t1' t2', defs1@defs2)  end
   370       val _ = if !trace_abs then warning ("assume_absfuns, Abstracting: " ^ string_of_thm th) else ();
   371       val (eqth,defs) = abstract (cprop_of th)
   372       val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs
   373       val _ = if !trace_abs then warning ("assume_absfuns, Result: " ^ string_of_thm (hd ths)) else ();
   374   in  map Drule.eta_contraction_rule ths  end;
   375 
   376 
   377 (*cterms are used throughout for efficiency*)
   378 val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop;
   379 
   380 (*cterm version of mk_cTrueprop*)
   381 fun c_mkTrueprop A = Thm.capply cTrueprop A;
   382 
   383 (*Given an abstraction over n variables, replace the bound variables by free
   384   ones. Return the body, along with the list of free variables.*)
   385 fun c_variant_abs_multi (ct0, vars) =
   386       let val (cv,ct) = Thm.dest_abs NONE ct0
   387       in  c_variant_abs_multi (ct, cv::vars)  end
   388       handle CTERM _ => (ct0, rev vars);
   389 
   390 (*Given the definition of a Skolem function, return a theorem to replace
   391   an existential formula by a use of that function.
   392    Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
   393 fun skolem_of_def def =
   394   let val (c,rhs) = Drule.dest_equals (cprop_of (freeze_thm def))
   395       val (ch, frees) = c_variant_abs_multi (rhs, [])
   396       val (chilbert,cabs) = Thm.dest_comb ch
   397       val {sign,t, ...} = rep_cterm chilbert
   398       val T = case t of Const ("Hilbert_Choice.Eps", Type("fun",[_,T])) => T
   399                       | _ => raise THM ("skolem_of_def: expected Eps", 0, [def])
   400       val cex = Thm.cterm_of sign (HOLogic.exists_const T)
   401       val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
   402       and conc =  c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees)));
   403       fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS someI_ex) 1
   404   in  Goal.prove_raw [ex_tm] conc tacf
   405        |> forall_intr_list frees
   406        |> forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)
   407        |> Thm.varifyT
   408   end;
   409 
   410 (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
   411 fun to_nnf th =
   412     th |> transfer_to_ATP_Linkup
   413        |> transform_elim |> zero_var_indexes |> freeze_thm
   414        |> ObjectLogic.atomize_thm |> make_nnf |> strip_lambdas ~1;
   415 
   416 (*The cache prevents repeated clausification of a theorem,
   417   and also repeated declaration of Skolem functions*)
   418   (* FIXME better use Termtab!? No, we MUST use theory data!!*)
   419 val clause_cache = ref (Symtab.empty : (thm * thm list) Symtab.table)
   420 
   421 
   422 (*Generate Skolem functions for a theorem supplied in nnf*)
   423 fun skolem_of_nnf th =
   424   map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns th);
   425 
   426 fun assert_lambda_free ths msg = 
   427   case filter (not o lambda_free o prop_of) ths of
   428       [] => ()
   429      | ths' => error (msg ^ "\n" ^ space_implode "\n" (map string_of_thm ths'));
   430 
   431 fun assume_abstract th =
   432   if lambda_free (prop_of th) then [th]
   433   else th |> Drule.eta_contraction_rule |> assume_absfuns
   434           |> tap (fn ths => assert_lambda_free ths "assume_abstract: lambdas")
   435 
   436 (*Replace lambdas by assumed function definitions in the theorems*)
   437 fun assume_abstract_list ths =
   438   if abstract_lambdas then List.concat (map assume_abstract ths)
   439   else map Drule.eta_contraction_rule ths;
   440 
   441 (*Replace lambdas by declared function definitions in the theorems*)
   442 fun declare_abstract' (thy, []) = (thy, [])
   443   | declare_abstract' (thy, th::ths) =
   444       let val (thy', th_defs) =
   445             if lambda_free (prop_of th) then (thy, [th])
   446             else
   447                 th |> zero_var_indexes |> freeze_thm
   448                    |> Drule.eta_contraction_rule |> transfer thy |> declare_absfuns
   449           val _ = assert_lambda_free th_defs "declare_abstract: lambdas"
   450           val (thy'', ths') = declare_abstract' (thy', ths)
   451       in  (thy'', th_defs @ ths')  end;
   452 
   453 fun declare_abstract (thy, ths) =
   454   if abstract_lambdas then declare_abstract' (thy, ths)
   455   else (thy, map Drule.eta_contraction_rule ths);
   456 
   457 (*Skolemize a named theorem, with Skolem functions as additional premises.*)
   458 fun skolem_thm th =
   459   let val nnfth = to_nnf th
   460   in  Meson.make_cnf (skolem_of_nnf nnfth) nnfth |> assume_abstract_list |> Meson.finish_cnf
   461   end
   462   handle THM _ => [];
   463 
   464 (*Keep the full complexity of the original name*)
   465 fun flatten_name s = space_implode "_X" (NameSpace.explode s);
   466 
   467 (*Declare Skolem functions for a theorem, supplied in nnf and with its name.
   468   It returns a modified theory, unless skolemization fails.*)
   469 fun skolem thy (name,th) =
   470   let val cname = (case name of "" => gensym "" | s => flatten_name s)
   471       val _ = Output.debug (fn () => "skolemizing " ^ name ^ ": ")
   472   in Option.map
   473         (fn nnfth =>
   474           let val (thy',defs) = declare_skofuns cname nnfth thy
   475               val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth
   476               val (thy'',cnfs') = declare_abstract (thy',cnfs)
   477           in (thy'', Meson.finish_cnf cnfs')
   478           end)
   479       (SOME (to_nnf th)  handle THM _ => NONE)
   480   end;
   481 
   482 (*Populate the clause cache using the supplied theorem. Return the clausal form
   483   and modified theory.*)
   484 fun skolem_cache_thm (name,th) thy =
   485   case Symtab.lookup (!clause_cache) name of
   486       NONE =>
   487         (case skolem thy (name, Thm.transfer thy th) of
   488              NONE => ([th],thy)
   489            | SOME (thy',cls) => 
   490                let val cls = map Goal.close_result cls
   491                in
   492                   if null cls then warning ("skolem_cache: empty clause set for " ^ name)
   493                   else ();
   494                   change clause_cache (Symtab.update (name, (th, cls))); 
   495                   (cls,thy')
   496                end)
   497     | SOME (th',cls) =>
   498         if eq_thm(th,th') then (cls,thy)
   499         else (Output.debug (fn () => "skolem_cache: Ignoring variant of theorem " ^ name);
   500               Output.debug (fn () => string_of_thm th);
   501               Output.debug (fn () => string_of_thm th');
   502               ([th],thy));
   503 
   504 (*Exported function to convert Isabelle theorems into axiom clauses*)
   505 fun cnf_axiom (name,th) =
   506  (Output.debug (fn () => "cnf_axiom called, theorem name = " ^ name);
   507   case name of
   508         "" => skolem_thm th (*no name, so can't cache*)
   509       | s  => case Symtab.lookup (!clause_cache) s of
   510                 NONE => 
   511                   let val cls = map Goal.close_result (skolem_thm th)
   512                   in Output.debug (fn () => "inserted into cache");
   513                      change clause_cache (Symtab.update (s, (th, cls))); cls 
   514                   end
   515               | SOME(th',cls) =>
   516                   if eq_thm(th,th') then cls
   517                   else
   518                     (Output.debug (fn () => "cnf_axiom: duplicate or variant of theorem " ^ name);
   519                      Output.debug (fn () => string_of_thm th);
   520                      Output.debug (fn () => string_of_thm th');
   521                      cls)
   522  );
   523 
   524 fun pairname th = (PureThy.get_name_hint th, th);
   525 
   526 (*Principally for debugging*)
   527 fun cnf_name s = 
   528   let val th = thm s
   529   in cnf_axiom (PureThy.get_name_hint th, th) end;
   530 
   531 (**** Extract and Clausify theorems from a theory's claset and simpset ****)
   532 
   533 fun rules_of_claset cs =
   534   let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs
   535       val intros = safeIs @ hazIs
   536       val elims  = map Classical.classical_rule (safeEs @ hazEs)
   537   in
   538      Output.debug (fn () => "rules_of_claset intros: " ^ Int.toString(length intros) ^
   539             " elims: " ^ Int.toString(length elims));
   540      map pairname (intros @ elims)
   541   end;
   542 
   543 fun rules_of_simpset ss =
   544   let val ({rules,...}, _) = rep_ss ss
   545       val simps = Net.entries rules
   546   in
   547     Output.debug (fn () => "rules_of_simpset: " ^ Int.toString(length simps));
   548     map (fn r => (#name r, #thm r)) simps
   549   end;
   550 
   551 fun claset_rules_of ctxt = rules_of_claset (local_claset_of ctxt);
   552 fun simpset_rules_of ctxt = rules_of_simpset (local_simpset_of ctxt);
   553 
   554 fun atpset_rules_of ctxt = map pairname (ResAtpset.get_atpset ctxt);
   555 
   556 
   557 (**** Translate a set of classical/simplifier rules into CNF (still as type "thm")  ****)
   558 
   559 (* classical rules: works for both FOL and HOL *)
   560 fun cnf_rules [] err_list = ([],err_list)
   561   | cnf_rules ((name,th) :: ths) err_list =
   562       let val (ts,es) = cnf_rules ths err_list
   563       in  (cnf_axiom (name,th) :: ts,es) handle  _ => (ts, (th::es))  end;
   564 
   565 fun pair_name_cls k (n, []) = []
   566   | pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss)
   567 
   568 fun cnf_rules_pairs_aux pairs [] = pairs
   569   | cnf_rules_pairs_aux pairs ((name,th)::ths) =
   570       let val pairs' = (pair_name_cls 0 (name, cnf_axiom(name,th))) @ pairs
   571                        handle THM _ => pairs | ResClause.CLAUSE _ => pairs
   572       in  cnf_rules_pairs_aux pairs' ths  end;
   573 
   574 (*The combination of rev and tail recursion preserves the original order*)
   575 fun cnf_rules_pairs l = cnf_rules_pairs_aux [] (rev l);
   576 
   577 
   578 (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)
   579 
   580 (*Setup function: takes a theory and installs ALL known theorems into the clause cache*)
   581 
   582 fun skolem_cache (name,th) thy =
   583   let val prop = Thm.prop_of th
   584   in
   585       if lambda_free prop 
   586          (*Monomorphic theorems can be Skolemized on demand,
   587            but there are problems with re-use of abstraction functions if we don't
   588            do them now, even for monomorphic theorems.*)
   589       then thy  
   590       else #2 (skolem_cache_thm (name,th) thy)
   591   end;
   592 
   593 (*The cache can be kept smaller by augmenting the condition above with 
   594     orelse (not abstract_lambdas andalso monomorphic prop).
   595   However, while this step does not reduce the time needed to build HOL, 
   596   it doubles the time taken by the first call to the ATP link-up.*)
   597 
   598 fun clause_cache_setup thy = fold skolem_cache (PureThy.all_thms_of thy) thy;
   599 
   600 
   601 (*** meson proof methods ***)
   602 
   603 fun skolem_use_cache_thm th =
   604   case Symtab.lookup (!clause_cache) (PureThy.get_name_hint th) of
   605       NONE => skolem_thm th
   606     | SOME (th',cls) =>
   607         if eq_thm(th,th') then cls else skolem_thm th;
   608 
   609 fun cnf_rules_of_ths ths = List.concat (map skolem_use_cache_thm ths);
   610 
   611 val meson_method_setup = Method.add_methods
   612   [("meson", Method.thms_args (fn ths =>
   613       Method.SIMPLE_METHOD' (CHANGED_PROP o Meson.meson_claset_tac (cnf_rules_of_ths ths) HOL_cs)),
   614     "MESON resolution proof procedure")];
   615 
   616 (** Attribute for converting a theorem into clauses **)
   617 
   618 fun meta_cnf_axiom th = map Meson.make_meta_clause (cnf_axiom (pairname th));
   619 
   620 fun clausify_rule (th,i) = List.nth (meta_cnf_axiom th, i)
   621 
   622 val clausify = Attrib.syntax (Scan.lift Args.nat
   623   >> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i))));
   624 
   625 
   626 (*** Converting a subgoal into negated conjecture clauses. ***)
   627 
   628 val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac];
   629 val neg_clausify = Meson.finish_cnf o assume_abstract_list o make_clauses;
   630 
   631 fun neg_conjecture_clauses st0 n =
   632   let val st = Seq.hd (neg_skolemize_tac n st0)
   633       val (params,_,_) = strip_context (Logic.nth_prem (n, Thm.prop_of st))
   634   in (neg_clausify (Option.valOf (metahyps_thms n st)), params) end;
   635 
   636 (*Conversion of a subgoal to conjecture clauses. Each clause has  
   637   leading !!-bound universal variables, to express generality. *)
   638 val neg_clausify_tac = 
   639   neg_skolemize_tac THEN' 
   640   SUBGOAL
   641     (fn (prop,_) =>
   642      let val ts = Logic.strip_assums_hyp prop
   643      in EVERY1 
   644 	 [METAHYPS
   645 	    (fn hyps => 
   646               (Method.insert_tac
   647                 (map forall_intr_vars (neg_clausify hyps)) 1)),
   648 	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
   649      end);
   650 
   651 (** The Skolemization attribute **)
   652 
   653 fun conj2_rule (th1,th2) = conjI OF [th1,th2];
   654 
   655 (*Conjoin a list of theorems to form a single theorem*)
   656 fun conj_rule []  = TrueI
   657   | conj_rule ths = foldr1 conj2_rule ths;
   658 
   659 fun skolem_attr (Context.Theory thy, th) =
   660       let val name = PureThy.get_name_hint th
   661           val (cls, thy') = skolem_cache_thm (name, th) thy
   662       in (Context.Theory thy', conj_rule cls) end
   663   | skolem_attr (context, th) = (context, conj_rule (skolem_use_cache_thm th));
   664 
   665 val setup_attrs = Attrib.add_attributes
   666   [("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem"),
   667    ("clausify", clausify, "conversion of theorem to clauses")];
   668 
   669 val setup_methods = Method.add_methods
   670   [("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac), 
   671     "conversion of goal to conjecture clauses")];
   672      
   673 val setup = clause_cache_setup #> setup_attrs #> setup_methods;
   674 
   675 end;