src/HOL/Tools/res_axioms.ML
author wenzelm
Tue Sep 19 23:15:32 2006 +0200 (2006-09-19)
changeset 20624 ba081ac0ed7e
parent 20567 93ae490fe02c
child 20710 384bfce59254
permissions -rw-r--r--
sko/abs: Name.internal prevents choking of print_theory;
     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 (*FIXME: does this signature serve any purpose?*)
     9 signature RES_AXIOMS =
    10   sig
    11   val elimRule_tac : thm -> Tactical.tactic
    12   val elimR2Fol : thm -> term
    13   val transform_elim : thm -> thm
    14   val cnf_axiom : (string * thm) -> thm list
    15   val meta_cnf_axiom : thm -> thm list
    16   val claset_rules_of_thy : theory -> (string * thm) list
    17   val simpset_rules_of_thy : theory -> (string * thm) list
    18   val claset_rules_of_ctxt: Proof.context -> (string * thm) list
    19   val simpset_rules_of_ctxt : Proof.context -> (string * thm) list
    20   val pairname : thm -> (string * thm)
    21   val skolem_thm : thm -> thm list
    22   val to_nnf : thm -> thm
    23   val cnf_rules_pairs : (string * Thm.thm) list -> (Thm.thm * (string * int)) list list;
    24   val meson_method_setup : theory -> theory
    25   val setup : theory -> theory
    26 
    27   val atpset_rules_of_thy : theory -> (string * thm) list
    28   val atpset_rules_of_ctxt : Proof.context -> (string * thm) list
    29   end;
    30 
    31 structure ResAxioms =
    32 
    33 struct
    34 
    35 (*FIXME DELETE: For running the comparison between combinators and abstractions.
    36   CANNOT be a ref, as the setting is used while Isabelle is built.*)
    37 val abstract_lambdas = true;
    38 
    39 val trace_abs = ref false;
    40 
    41 (*Store definitions of abstraction functions, ensuring that identical right-hand
    42   sides are denoted by the same functions and thereby reducing the need for
    43   extensionality in proofs.
    44   FIXME!  Store in theory data!!*)
    45 val abstraction_cache = ref Net.empty : thm Net.net ref;
    46 
    47 (**** Transformation of Elimination Rules into First-Order Formulas****)
    48 
    49 (* a tactic used to prove an elim-rule. *)
    50 fun elimRule_tac th =
    51     (resolve_tac [impI,notI] 1) THEN (etac th 1) THEN REPEAT(fast_tac HOL_cs 1);
    52 
    53 fun add_EX tm [] = tm
    54   | add_EX tm ((x,xtp)::xs) = add_EX (HOLogic.exists_const xtp $ Abs(x,xtp,tm)) xs;
    55 
    56 (*Checks for the premise ~P when the conclusion is P.*)
    57 fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_)))
    58            (Const("Trueprop",_) $ Free(q,_)) = (p = q)
    59   | is_neg _ _ = false;
    60 
    61 exception ELIMR2FOL;
    62 
    63 (*Handles the case where the dummy "conclusion" variable appears negated in the
    64   premises, so the final consequent must be kept.*)
    65 fun strip_concl' prems bvs (Const ("==>",_) $ P $ Q) =
    66       strip_concl' (HOLogic.dest_Trueprop P :: prems) bvs  Q
    67   | strip_concl' prems bvs P =
    68       let val P' = HOLogic.Not $ (HOLogic.dest_Trueprop P)
    69       in add_EX (foldr1 HOLogic.mk_conj (P'::prems)) bvs end;
    70 
    71 (*Recurrsion over the minor premise of an elimination rule. Final consequent
    72   is ignored, as it is the dummy "conclusion" variable.*)
    73 fun strip_concl prems bvs concl (Const ("all", _) $ Abs (x,xtp,body)) =
    74       strip_concl prems ((x,xtp)::bvs) concl body
    75   | strip_concl prems bvs concl (Const ("==>",_) $ P $ Q) =
    76       if (is_neg P concl) then (strip_concl' prems bvs Q)
    77       else strip_concl (HOLogic.dest_Trueprop P::prems) bvs  concl Q
    78   | strip_concl prems bvs concl Q =
    79       if concl aconv Q then add_EX (foldr1 HOLogic.mk_conj prems) bvs
    80       else raise ELIMR2FOL (*expected conclusion not found!*)
    81 
    82 fun trans_elim (major,[],_) = HOLogic.Not $ major
    83   | trans_elim (major,minors,concl) =
    84       let val disjs = foldr1 HOLogic.mk_disj (map (strip_concl [] [] concl) minors)
    85       in  HOLogic.mk_imp (major, disjs)  end;
    86 
    87 (* convert an elim rule into an equivalent formula, of type term. *)
    88 fun elimR2Fol elimR =
    89   let val elimR' = #1 (Drule.freeze_thaw elimR)
    90       val (prems,concl) = (prems_of elimR', concl_of elimR')
    91       val cv = case concl of    (*conclusion variable*)
    92                   Const("Trueprop",_) $ (v as Free(_,Type("bool",[]))) => v
    93                 | v as Free(_, Type("prop",[])) => v
    94                 | _ => raise ELIMR2FOL
    95   in case prems of
    96       [] => raise ELIMR2FOL
    97     | (Const("Trueprop",_) $ major) :: minors =>
    98         if member (op aconv) (term_frees major) cv then raise ELIMR2FOL
    99         else (trans_elim (major, minors, concl) handle TERM _ => raise ELIMR2FOL)
   100     | _ => raise ELIMR2FOL
   101   end;
   102 
   103 (* convert an elim-rule into an equivalent theorem that does not have the
   104    predicate variable.  Leave other theorems unchanged.*)
   105 fun transform_elim th =
   106     let val ctm = cterm_of (sign_of_thm th) (HOLogic.mk_Trueprop (elimR2Fol th))
   107     in Goal.prove_raw [] ctm (fn _ => elimRule_tac th) end
   108     handle ELIMR2FOL => th (*not an elimination rule*)
   109          | exn => (warning ("transform_elim failed: " ^ Toplevel.exn_message exn ^
   110                             " for theorem " ^ string_of_thm th); th)
   111 
   112 
   113 (**** Transformation of Clasets and Simpsets into First-Order Axioms ****)
   114 
   115 (*Transfer a theorem into theory Reconstruction.thy if it is not already
   116   inside that theory -- because it's needed for Skolemization *)
   117 
   118 (*This will refer to the final version of theory Reconstruction.*)
   119 val recon_thy_ref = Theory.self_ref (the_context ());
   120 
   121 (*If called while Reconstruction is being created, it will transfer to the
   122   current version. If called afterward, it will transfer to the final version.*)
   123 fun transfer_to_Reconstruction th =
   124     transfer (Theory.deref recon_thy_ref) th handle THM _ => th;
   125 
   126 fun is_taut th =
   127       case (prop_of th) of
   128            (Const ("Trueprop", _) $ Const ("True", _)) => true
   129          | _ => false;
   130 
   131 (* remove tautologous clauses *)
   132 val rm_redundant_cls = List.filter (not o is_taut);
   133 
   134 
   135 (**** SKOLEMIZATION BY INFERENCE (lcp) ****)
   136 
   137 (*Traverse a theorem, declaring Skolem function definitions. String s is the suggested
   138   prefix for the Skolem constant. Result is a new theory*)
   139 fun declare_skofuns s th thy =
   140   let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (thy, axs) =
   141             (*Existential: declare a Skolem function, then insert into body and continue*)
   142             let val cname = Name.internal (gensym ("sko_" ^ s ^ "_"))
   143                 val args = term_frees xtp  (*get the formal parameter list*)
   144                 val Ts = map type_of args
   145                 val cT = Ts ---> T
   146                 val c = Const (Sign.full_name thy cname, cT)
   147                 val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
   148                         (*Forms a lambda-abstraction over the formal parameters*)
   149                 val thy' = Theory.add_consts_i [(cname, cT, NoSyn)] thy
   150                            (*Theory is augmented with the constant, then its def*)
   151                 val cdef = cname ^ "_def"
   152                 val thy'' = Theory.add_defs_i false false [(cdef, equals cT $ c $ rhs)] thy'
   153             in dec_sko (subst_bound (list_comb(c,args), p))
   154                        (thy'', get_axiom thy'' cdef :: axs)
   155             end
   156         | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) thx =
   157             (*Universal quant: insert a free variable into body and continue*)
   158             let val fname = Name.variant (add_term_names (p,[])) a
   159             in dec_sko (subst_bound (Free(fname,T), p)) thx end
   160         | dec_sko (Const ("op &", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
   161         | dec_sko (Const ("op |", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
   162         | dec_sko (Const ("Trueprop", _) $ p) thx = dec_sko p thx
   163         | dec_sko t thx = thx (*Do nothing otherwise*)
   164   in  dec_sko (prop_of th) (thy,[])  end;
   165 
   166 (*Traverse a theorem, accumulating Skolem function definitions.*)
   167 fun assume_skofuns th =
   168   let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
   169             (*Existential: declare a Skolem function, then insert into body and continue*)
   170             let val skos = map (#1 o Logic.dest_equals) defs  (*existing sko fns*)
   171                 val args = term_frees xtp \\ skos  (*the formal parameters*)
   172                 val Ts = map type_of args
   173                 val cT = Ts ---> T
   174                 val c = Free (gensym "sko_", cT)
   175                 val rhs = list_abs_free (map dest_Free args,
   176                                          HOLogic.choice_const T $ xtp)
   177                       (*Forms a lambda-abstraction over the formal parameters*)
   178                 val def = equals cT $ c $ rhs
   179             in dec_sko (subst_bound (list_comb(c,args), p))
   180                        (def :: defs)
   181             end
   182         | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) defs =
   183             (*Universal quant: insert a free variable into body and continue*)
   184             let val fname = Name.variant (add_term_names (p,[])) a
   185             in dec_sko (subst_bound (Free(fname,T), p)) defs end
   186         | dec_sko (Const ("op &", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
   187         | dec_sko (Const ("op |", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
   188         | dec_sko (Const ("Trueprop", _) $ p) defs = dec_sko p defs
   189         | dec_sko t defs = defs (*Do nothing otherwise*)
   190   in  dec_sko (prop_of th) []  end;
   191 
   192 
   193 (**** REPLACING ABSTRACTIONS BY FUNCTION DEFINITIONS ****)
   194 
   195 (*Returns the vars of a theorem*)
   196 fun vars_of_thm th =
   197   map (Thm.cterm_of (theory_of_thm th) o Var) (Drule.fold_terms Term.add_vars th []);
   198 
   199 (*Make a version of fun_cong with a given variable name*)
   200 local
   201     val fun_cong' = fun_cong RS asm_rl; (*renumber f, g to prevent clashes with (a,0)*)
   202     val cx = hd (vars_of_thm fun_cong');
   203     val ty = typ_of (ctyp_of_term cx);
   204     val thy = theory_of_thm fun_cong;
   205     fun mkvar a = cterm_of thy (Var((a,0),ty));
   206 in
   207 fun xfun_cong x = Thm.instantiate ([], [(cx, mkvar x)]) fun_cong'
   208 end;
   209 
   210 (*Removes the lambdas from an equation of the form t = (%x. u)*)
   211 fun strip_lambdas th =
   212   case prop_of th of
   213       _ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) =>
   214           strip_lambdas (#1 (Drule.freeze_thaw (th RS xfun_cong x)))
   215     | _ => th;
   216 
   217 (*Convert meta- to object-equality. Fails for theorems like split_comp_eq,
   218   where some types have the empty sort.*)
   219 fun object_eq th = th RS def_imp_eq
   220     handle THM _ => error ("Theorem contains empty sort: " ^ string_of_thm th);
   221 
   222 (*Contract all eta-redexes in the theorem, lest they give rise to needless abstractions*)
   223 fun eta_conversion_rule th =
   224   equal_elim (eta_conversion (cprop_of th)) th;
   225 
   226 fun crhs_of th =
   227   case Drule.strip_comb (cprop_of th) of
   228       (f, [_, rhs]) =>
   229           (case term_of f of Const ("==", _) => rhs
   230              | _ => raise THM ("crhs_of", 0, [th]))
   231     | _ => raise THM ("crhs_of", 1, [th]);
   232 
   233 fun lhs_of th =
   234   case prop_of th of (Const("==",_) $ lhs $ _) => lhs
   235     | _ => raise THM ("lhs_of", 1, [th]);
   236 
   237 fun rhs_of th =
   238   case prop_of th of (Const("==",_) $ _ $ rhs) => rhs
   239     | _ => raise THM ("rhs_of", 1, [th]);
   240 
   241 (*Apply a function definition to an argument, beta-reducing the result.*)
   242 fun beta_comb cf x =
   243   let val th1 = combination cf (reflexive x)
   244       val th2 = beta_conversion false (crhs_of th1)
   245   in  transitive th1 th2  end;
   246 
   247 (*Apply a function definition to arguments, beta-reducing along the way.*)
   248 fun list_combination cf [] = cf
   249   | list_combination cf (x::xs) = list_combination (beta_comb cf x) xs;
   250 
   251 fun list_cabs ([] ,     t) = t
   252   | list_cabs (v::vars, t) = Thm.cabs v (list_cabs(vars,t));
   253 
   254 fun assert_eta_free ct =
   255   let val t = term_of ct
   256   in if (t aconv Envir.eta_contract t) then ()
   257      else error ("Eta redex in term: " ^ string_of_cterm ct)
   258   end;
   259 
   260 fun eq_absdef (th1, th2) =
   261     Context.joinable (theory_of_thm th1, theory_of_thm th2)  andalso
   262     rhs_of th1 aconv rhs_of th2;
   263 
   264 fun lambda_free (Abs _) = false
   265   | lambda_free (t $ u) = lambda_free t andalso lambda_free u
   266   | lambda_free _ = true;
   267 
   268 fun monomorphic t =
   269   Term.fold_types (Term.fold_atyps (fn TVar _ => K false | _ => I)) t true;
   270 
   271 (*Traverse a theorem, declaring abstraction function definitions. String s is the suggested
   272   prefix for the constants. Resulting theory is returned in the first theorem. *)
   273 fun declare_absfuns th =
   274   let fun abstract thy ct =
   275         if lambda_free (term_of ct) then (transfer thy (reflexive ct), [])
   276         else
   277         case term_of ct of
   278           Abs (_,T,u) =>
   279             let val cname = Name.internal (gensym "abs_");
   280                 val _ = assert_eta_free ct;
   281                 val (cv,cta) = Thm.dest_abs NONE ct
   282                 val v = (#1 o dest_Free o term_of) cv
   283                 val (u'_th,defs) = abstract thy cta
   284                 val cu' = crhs_of u'_th
   285                 val abs_v_u = lambda (term_of cv) (term_of cu')
   286                 (*get the formal parameters: ALL variables free in the term*)
   287                 val args = term_frees abs_v_u
   288                 val rhs = list_abs_free (map dest_Free args, abs_v_u)
   289                       (*Forms a lambda-abstraction over the formal parameters*)
   290                 val v_rhs = Logic.varify rhs
   291                 val (ax,thy) =
   292                  case List.find (fn ax => v_rhs aconv rhs_of ax)
   293                         (Net.match_term (!abstraction_cache) v_rhs) of
   294                      SOME ax => (ax,thy)   (*cached axiom, current theory*)
   295                    | NONE =>
   296                       let val Ts = map type_of args
   297                           val cT = Ts ---> (T --> typ_of (ctyp_of_term cu'))
   298                           val thy = theory_of_thm u'_th
   299                           val c = Const (Sign.full_name thy cname, cT)
   300                           val thy = Theory.add_consts_i [(cname, cT, NoSyn)] thy
   301                                      (*Theory is augmented with the constant,
   302                                        then its definition*)
   303                           val cdef = cname ^ "_def"
   304                           val thy = Theory.add_defs_i false false
   305                                        [(cdef, equals cT $ c $ rhs)] thy
   306                           val ax = get_axiom thy cdef
   307                           val _ = abstraction_cache := Net.insert_term eq_absdef (v_rhs,ax)
   308                                     (!abstraction_cache)
   309                             handle Net.INSERT =>
   310                               raise THM ("declare_absfuns: INSERT", 0, [th,u'_th,ax])
   311                        in  (ax,thy)  end
   312                 val _ = assert (v_rhs aconv rhs_of ax) "declare_absfuns: rhs mismatch"
   313                 val def = #1 (Drule.freeze_thaw ax)
   314                 val def_args = list_combination def (map (cterm_of thy) args)
   315             in (transitive (abstract_rule v cv u'_th) (symmetric def_args),
   316                 def :: defs) end
   317         | (t1$t2) =>
   318             let val (ct1,ct2) = Thm.dest_comb ct
   319                 val (th1,defs1) = abstract thy ct1
   320                 val (th2,defs2) = abstract (theory_of_thm th1) ct2
   321             in  (combination th1 th2, defs1@defs2)  end
   322       val _ = if !trace_abs then warning (string_of_thm th) else ();
   323       val (eqth,defs) = abstract (theory_of_thm th) (cprop_of th)
   324       val ths = equal_elim eqth th ::
   325                 map (forall_intr_vars o strip_lambdas o object_eq) defs
   326   in  (theory_of_thm eqth, ths)  end;
   327 
   328 fun name_of def = SOME (#1 (dest_Free (lhs_of def))) handle _ => NONE;
   329 
   330 (*A name is valid provided it isn't the name of a defined abstraction.*)
   331 fun valid_name defs (Free(x,T)) = not (x mem_string (List.mapPartial name_of defs))
   332   | valid_name defs _ = false;
   333 
   334 fun assume_absfuns th =
   335   let val thy = theory_of_thm th
   336       val cterm = cterm_of thy
   337       fun abstract ct =
   338         if lambda_free (term_of ct) then (reflexive ct, [])
   339         else
   340         case term_of ct of
   341           Abs (_,T,u) =>
   342             let val (cv,cta) = Thm.dest_abs NONE ct
   343                 val _ = assert_eta_free ct;
   344                 val v = (#1 o dest_Free o term_of) cv
   345                 val (u'_th,defs) = abstract cta
   346                 val cu' = crhs_of u'_th
   347                 val abs_v_u = Thm.cabs cv cu'
   348                 (*get the formal parameters: free variables not present in the defs
   349                   (to avoid taking abstraction function names as parameters) *)
   350                 val args = filter (valid_name defs) (term_frees (term_of abs_v_u))
   351                 val crhs = list_cabs (map cterm args, abs_v_u)
   352                       (*Forms a lambda-abstraction over the formal parameters*)
   353                 val rhs = term_of crhs
   354                 val def =  (*FIXME: can we also reuse the const-abstractions?*)
   355                  case List.find (fn ax => rhs aconv rhs_of ax andalso
   356                                           Context.joinable (thy, theory_of_thm ax))
   357                         (Net.match_term (!abstraction_cache) rhs) of
   358                      SOME ax => ax
   359                    | NONE =>
   360                       let val Ts = map type_of args
   361                           val const_ty = Ts ---> (T --> typ_of (ctyp_of_term cu'))
   362                           val c = Free (gensym "abs_", const_ty)
   363                           val ax = assume (Thm.capply (cterm (equals const_ty $ c)) crhs)
   364                           val _ = abstraction_cache := Net.insert_term eq_absdef (rhs,ax)
   365                                     (!abstraction_cache)
   366                             handle Net.INSERT =>
   367                               raise THM ("assume_absfuns: INSERT", 0, [th,u'_th,ax])
   368                       in ax end
   369                 val _ = assert (rhs aconv rhs_of def) "assume_absfuns: rhs mismatch"
   370                 val def_args = list_combination def (map cterm args)
   371             in (transitive (abstract_rule v cv u'_th) (symmetric def_args),
   372                 def :: defs) end
   373         | (t1$t2) =>
   374             let val (ct1,ct2) = Thm.dest_comb ct
   375                 val (t1',defs1) = abstract ct1
   376                 val (t2',defs2) = abstract ct2
   377             in  (combination t1' t2', defs1@defs2)  end
   378       val (eqth,defs) = abstract (cprop_of th)
   379   in  equal_elim eqth th ::
   380       map (forall_intr_vars o strip_lambdas o object_eq) defs
   381   end;
   382 
   383 
   384 (*cterms are used throughout for efficiency*)
   385 val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop;
   386 
   387 (*cterm version of mk_cTrueprop*)
   388 fun c_mkTrueprop A = Thm.capply cTrueprop A;
   389 
   390 (*Given an abstraction over n variables, replace the bound variables by free
   391   ones. Return the body, along with the list of free variables.*)
   392 fun c_variant_abs_multi (ct0, vars) =
   393       let val (cv,ct) = Thm.dest_abs NONE ct0
   394       in  c_variant_abs_multi (ct, cv::vars)  end
   395       handle CTERM _ => (ct0, rev vars);
   396 
   397 (*Given the definition of a Skolem function, return a theorem to replace
   398   an existential formula by a use of that function.
   399    Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
   400 fun skolem_of_def def =
   401   let val (c,rhs) = Drule.dest_equals (cprop_of (#1 (Drule.freeze_thaw def)))
   402       val (ch, frees) = c_variant_abs_multi (rhs, [])
   403       val (chilbert,cabs) = Thm.dest_comb ch
   404       val {sign,t, ...} = rep_cterm chilbert
   405       val T = case t of Const ("Hilbert_Choice.Eps", Type("fun",[_,T])) => T
   406                       | _ => raise THM ("skolem_of_def: expected Eps", 0, [def])
   407       val cex = Thm.cterm_of sign (HOLogic.exists_const T)
   408       val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
   409       and conc =  c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees)));
   410       fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS someI_ex) 1
   411   in  Goal.prove_raw [ex_tm] conc tacf
   412        |> forall_intr_list frees
   413        |> forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)
   414        |> Thm.varifyT
   415   end;
   416 
   417 (*Converts an Isabelle theorem (intro, elim or simp format) into nnf.*)
   418 (*It now works for HOL too. *)
   419 fun to_nnf th =
   420     th |> transfer_to_Reconstruction
   421        |> transform_elim |> zero_var_indexes |> Drule.freeze_thaw |> #1
   422        |> ObjectLogic.atomize_thm |> make_nnf;
   423 
   424 (*The cache prevents repeated clausification of a theorem,
   425   and also repeated declaration of Skolem functions*)
   426   (* FIXME better use Termtab!? No, we MUST use theory data!!*)
   427 val clause_cache = ref (Symtab.empty : (thm * thm list) Symtab.table)
   428 
   429 
   430 (*Generate Skolem functions for a theorem supplied in nnf*)
   431 fun skolem_of_nnf th =
   432   map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns th);
   433 
   434 fun assert_lambda_free ths = assert (forall (lambda_free o prop_of) ths);
   435 
   436 fun assume_abstract th =
   437   if lambda_free (prop_of th) then [th]
   438   else th |> eta_conversion_rule |> assume_absfuns
   439           |> tap (fn ths => assert_lambda_free ths "assume_abstract: lambdas")
   440 
   441 (*Replace lambdas by assumed function definitions in the theorems*)
   442 fun assume_abstract_list ths =
   443   if abstract_lambdas then List.concat (map assume_abstract ths)
   444   else map eta_conversion_rule ths;
   445 
   446 (*Replace lambdas by declared function definitions in the theorems*)
   447 fun declare_abstract' (thy, []) = (thy, [])
   448   | declare_abstract' (thy, th::ths) =
   449       let val (thy', th_defs) =
   450             if lambda_free (prop_of th) then (thy, [th])
   451             else
   452                 th |> zero_var_indexes |> Drule.freeze_thaw |> #1
   453                    |> eta_conversion_rule |> transfer thy |> declare_absfuns
   454           val _ = assert_lambda_free th_defs "declare_abstract: lambdas"
   455           val (thy'', ths') = declare_abstract' (thy', ths)
   456       in  (thy'', th_defs @ ths')  end;
   457 
   458 (*FIXME DELETE if we decide to switch to abstractions*)
   459 fun declare_abstract (thy, ths) =
   460   if abstract_lambdas then declare_abstract' (thy, ths)
   461   else (thy, map eta_conversion_rule ths);
   462 
   463 (*Skolemize a named theorem, with Skolem functions as additional premises.*)
   464 (*also works for HOL*)
   465 fun skolem_thm th =
   466   let val nnfth = to_nnf th
   467   in  Meson.make_cnf (skolem_of_nnf nnfth) nnfth
   468       |> assume_abstract_list |> Meson.finish_cnf |> rm_redundant_cls
   469   end
   470   handle THM _ => [];
   471 
   472 (*Declare Skolem functions for a theorem, supplied in nnf and with its name.
   473   It returns a modified theory, unless skolemization fails.*)
   474 fun skolem thy (name,th) =
   475   let val cname = (case name of "" => gensym "" | s => Sign.base_name s)
   476       val _ = Output.debug ("skolemizing " ^ name ^ ": ")
   477   in Option.map
   478         (fn nnfth =>
   479           let val (thy',defs) = declare_skofuns cname nnfth thy
   480               val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth
   481               val (thy'',cnfs') = declare_abstract (thy',cnfs)
   482           in (thy'', rm_redundant_cls (Meson.finish_cnf cnfs'))
   483           end)
   484       (SOME (to_nnf th)  handle THM _ => NONE)
   485   end;
   486 
   487 (*Populate the clause cache using the supplied theorem. Return the clausal form
   488   and modified theory.*)
   489 fun skolem_cache_thm (name,th) thy =
   490   case Symtab.lookup (!clause_cache) name of
   491       NONE =>
   492         (case skolem thy (name, Thm.transfer thy th) of
   493              NONE => ([th],thy)
   494            | SOME (thy',cls) => 
   495                let val cls = map Drule.local_standard cls
   496                in
   497                   if null cls then warning ("skolem_cache: empty clause set for " ^ name)
   498                   else ();
   499                   change clause_cache (Symtab.update (name, (th, cls))); 
   500                   (cls,thy')
   501                end)
   502     | SOME (th',cls) =>
   503         if eq_thm(th,th') then (cls,thy)
   504         else (Output.debug ("skolem_cache: Ignoring variant of theorem " ^ name);
   505               Output.debug (string_of_thm th);
   506               Output.debug (string_of_thm th');
   507               ([th],thy));
   508 
   509 (*Exported function to convert Isabelle theorems into axiom clauses*)
   510 fun cnf_axiom (name,th) =
   511   case name of
   512         "" => skolem_thm th (*no name, so can't cache*)
   513       | s  => case Symtab.lookup (!clause_cache) s of
   514                 NONE => 
   515                   let val cls = map Drule.local_standard (skolem_thm th)
   516                   in change clause_cache (Symtab.update (s, (th, cls))); cls end
   517               | SOME(th',cls) =>
   518                   if eq_thm(th,th') then cls
   519                   else (Output.debug ("cnf_axiom: duplicate or variant of theorem " ^ name);
   520                         Output.debug (string_of_thm th);
   521                         Output.debug (string_of_thm th');
   522                         cls);
   523 
   524 fun pairname th = (Thm.name_of_thm th, th);
   525 
   526 fun meta_cnf_axiom th =
   527     map Meson.make_meta_clause (cnf_axiom (pairname th));
   528 
   529 
   530 (**** Extract and Clausify theorems from a theory's claset and simpset ****)
   531 
   532 (*Preserve the name of "th" after the transformation "f"*)
   533 fun preserve_name f th = Thm.name_thm (Thm.name_of_thm th, f th);
   534 
   535 fun rules_of_claset cs =
   536   let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs
   537       val intros = safeIs @ hazIs
   538       val elims  = map Classical.classical_rule (safeEs @ hazEs)
   539   in
   540      Output.debug ("rules_of_claset intros: " ^ Int.toString(length intros) ^
   541             " elims: " ^ Int.toString(length elims));
   542      map pairname (intros @ elims)
   543   end;
   544 
   545 fun rules_of_simpset ss =
   546   let val ({rules,...}, _) = rep_ss ss
   547       val simps = Net.entries rules
   548   in
   549       Output.debug ("rules_of_simpset: " ^ Int.toString(length simps));
   550       map (fn r => (#name r, #thm r)) simps
   551   end;
   552 
   553 fun claset_rules_of_thy thy = rules_of_claset (claset_of thy);
   554 fun simpset_rules_of_thy thy = rules_of_simpset (simpset_of thy);
   555 
   556 fun atpset_rules_of_thy thy = map pairname (ResAtpSet.atp_rules_of_thy thy);
   557 
   558 
   559 fun claset_rules_of_ctxt ctxt = rules_of_claset (local_claset_of ctxt);
   560 fun simpset_rules_of_ctxt ctxt = rules_of_simpset (local_simpset_of ctxt);
   561 
   562 fun atpset_rules_of_ctxt ctxt = map pairname (ResAtpSet.atp_rules_of_ctxt ctxt);
   563 
   564 (**** Translate a set of classical/simplifier rules into CNF (still as type "thm")  ****)
   565 
   566 (* classical rules: works for both FOL and HOL *)
   567 fun cnf_rules [] err_list = ([],err_list)
   568   | cnf_rules ((name,th) :: ths) err_list =
   569       let val (ts,es) = cnf_rules ths err_list
   570       in  (cnf_axiom (name,th) :: ts,es) handle  _ => (ts, (th::es))  end;
   571 
   572 fun pair_name_cls k (n, []) = []
   573   | pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss)
   574 
   575 fun cnf_rules_pairs_aux pairs [] = pairs
   576   | cnf_rules_pairs_aux pairs ((name,th)::ths) =
   577       let val pairs' = (pair_name_cls 0 (name, cnf_axiom(name,th))) @ pairs
   578                        handle THM _ => pairs | ResClause.CLAUSE _ => pairs
   579                             | ResHolClause.LAM2COMB _ => pairs
   580       in  cnf_rules_pairs_aux pairs' ths  end;
   581 
   582 val cnf_rules_pairs = cnf_rules_pairs_aux [];
   583 
   584 
   585 (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)
   586 
   587 (*Setup function: takes a theory and installs ALL known theorems into the clause cache*)
   588 
   589 fun skolem_cache (name,th) thy =
   590   let val prop = Thm.prop_of th
   591   in
   592       if lambda_free prop orelse monomorphic prop
   593       then thy    (*monomorphic theorems can be Skolemized on demand*)
   594       else #2 (skolem_cache_thm (name,th) thy)
   595   end;
   596 
   597 fun clause_cache_setup thy = fold skolem_cache (PureThy.all_thms_of thy) thy;
   598 
   599 
   600 (*** meson proof methods ***)
   601 
   602 fun cnf_rules_of_ths ths = List.concat (#1 (cnf_rules (map pairname ths) []));
   603 
   604 fun meson_meth ths ctxt =
   605   Method.SIMPLE_METHOD' HEADGOAL
   606     (CHANGED_PROP o Meson.meson_claset_tac (cnf_rules_of_ths ths) (local_claset_of ctxt));
   607 
   608 val meson_method_setup =
   609   Method.add_methods
   610     [("meson", Method.thms_ctxt_args meson_meth,
   611       "MESON resolution proof procedure")];
   612 
   613 
   614 
   615 (*** The Skolemization attribute ***)
   616 
   617 fun conj2_rule (th1,th2) = conjI OF [th1,th2];
   618 
   619 (*Conjoin a list of theorems to form a single theorem*)
   620 fun conj_rule []  = TrueI
   621   | conj_rule ths = foldr1 conj2_rule ths;
   622 
   623 fun skolem_attr (Context.Theory thy, th) =
   624       let val name = Thm.name_of_thm th
   625           val (cls, thy') = skolem_cache_thm (name, th) thy
   626       in (Context.Theory thy', conj_rule cls) end
   627   | skolem_attr (context, th) = (context, conj_rule (skolem_thm th));
   628 
   629 val setup_attrs = Attrib.add_attributes
   630   [("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem")];
   631 
   632 val setup = clause_cache_setup #> setup_attrs;
   633 
   634 end;