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