src/HOL/Tools/res_axioms.ML
author paulson
Thu Sep 27 17:55:28 2007 +0200 (2007-09-27)
changeset 24742 73b8b42a36b6
parent 24669 4579eac2c997
child 24771 6c7e94742afa
permissions -rw-r--r--
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
theorems of Nat.thy are hidden by the Ordering.thy versions
     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 cnf_axiom: thm -> thm list
    11   val meta_cnf_axiom: thm -> thm list
    12   val pairname: thm -> string * thm
    13   val skolem_thm: thm -> thm list
    14   val cnf_rules_pairs: (string * thm) list -> (thm * (string * int)) list
    15   val cnf_rules_of_ths: thm list -> thm list
    16   val neg_clausify: thm list -> thm list
    17   val expand_defs_tac: thm -> tactic
    18   val assume_abstract_list: string -> thm list -> thm list
    19   val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list
    20   val claset_rules_of: Proof.context -> (string * thm) list   (*FIXME DELETE*)
    21   val simpset_rules_of: Proof.context -> (string * thm) list  (*FIXME DELETE*)
    22   val atpset_rules_of: Proof.context -> (string * thm) list
    23   val meson_method_setup: theory -> theory
    24   val clause_cache_endtheory: theory -> theory option
    25   val setup: theory -> theory
    26 end;
    27 
    28 structure ResAxioms: RES_AXIOMS =
    29 struct
    30 
    31 (* FIXME legacy *)
    32 fun freeze_thm th = #1 (Drule.freeze_thaw th);
    33 
    34 val lhs_of = #1 o Logic.dest_equals o Thm.prop_of;
    35 val rhs_of = #2 o Logic.dest_equals o Thm.prop_of;
    36 
    37 
    38 (*Store definitions of abstraction functions, ensuring that identical right-hand
    39   sides are denoted by the same functions and thereby reducing the need for
    40   extensionality in proofs.
    41   FIXME!  Store in theory data!!*)
    42 
    43 (*Populate the abstraction cache with common combinators.*)
    44 fun seed th net =
    45   let val (_,ct) = Thm.dest_abs NONE (Thm.rhs_of th)
    46       val t = Logic.legacy_varify (term_of ct)
    47   in  Net.insert_term Thm.eq_thm (t, th) net end;
    48 
    49 val abstraction_cache = ref
    50       (seed (thm"ATP_Linkup.I_simp")
    51        (seed (thm"ATP_Linkup.B_simp")
    52         (seed (thm"ATP_Linkup.K_simp") Net.empty)));
    53 
    54 
    55 (**** Transformation of Elimination Rules into First-Order Formulas****)
    56 
    57 val cfalse = cterm_of HOL.thy HOLogic.false_const;
    58 val ctp_false = cterm_of HOL.thy (HOLogic.mk_Trueprop HOLogic.false_const);
    59 
    60 (*Converts an elim-rule into an equivalent theorem that does not have the
    61   predicate variable.  Leaves other theorems unchanged.  We simply instantiate the
    62   conclusion variable to False.*)
    63 fun transform_elim th =
    64   case concl_of th of    (*conclusion variable*)
    65        Const("Trueprop",_) $ (v as Var(_,Type("bool",[]))) =>
    66            Thm.instantiate ([], [(cterm_of HOL.thy v, cfalse)]) th
    67     | v as Var(_, Type("prop",[])) =>
    68            Thm.instantiate ([], [(cterm_of HOL.thy v, ctp_false)]) th
    69     | _ => th;
    70 
    71 (*To enforce single-threading*)
    72 exception Clausify_failure of theory;
    73 
    74 (**** SKOLEMIZATION BY INFERENCE (lcp) ****)
    75 
    76 fun rhs_extra_types lhsT rhs =
    77   let val lhs_vars = Term.add_tfreesT lhsT []
    78       fun add_new_TFrees (TFree v) =
    79 	    if member (op =) lhs_vars v then I else insert (op =) (TFree v)
    80 	| add_new_TFrees _ = I
    81       val rhs_consts = fold_aterms (fn Const c => insert (op =) c | _ => I) rhs []
    82   in fold (#2 #> Term.fold_atyps add_new_TFrees) rhs_consts [] end;
    83 
    84 (*Traverse a theorem, declaring Skolem function definitions. String s is the suggested
    85   prefix for the Skolem constant. Result is a new theory*)
    86 fun declare_skofuns s th thy =
    87   let val nref = ref 0
    88       fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (thy, axs) =
    89             (*Existential: declare a Skolem function, then insert into body and continue*)
    90             let val cname = Name.internal ("sko_" ^ s ^ "_" ^ Int.toString (inc nref))
    91                 val args0 = term_frees xtp  (*get the formal parameter list*)
    92                 val Ts = map type_of args0
    93                 val extraTs = rhs_extra_types (Ts ---> T) xtp
    94                 val _ = if null extraTs then () else
    95                    warning ("Skolemization: extra type vars: " ^ 
    96                             commas_quote (map (Sign.string_of_typ thy) extraTs)); 
    97                 val argsx = map (fn T => Free(gensym"vsk", T)) extraTs
    98                 val args = argsx @ args0
    99                 val cT = extraTs ---> Ts ---> T
   100                 val c = Const (Sign.full_name thy cname, cT)
   101                 val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
   102                         (*Forms a lambda-abstraction over the formal parameters*)
   103                 val _ = Output.debug (fn () => "declaring the constant " ^ cname)
   104                 val thy' = Sign.add_consts_authentic [(cname, cT, NoSyn)] thy
   105                            (*Theory is augmented with the constant, then its def*)
   106                 val cdef = cname ^ "_def"
   107                 val thy'' = Theory.add_defs_i false false [(cdef, equals cT $ c $ rhs)] thy'
   108                             handle ERROR _ => raise Clausify_failure thy'
   109             in dec_sko (subst_bound (list_comb(c,args), p))
   110 			       (thy'', get_axiom thy'' cdef :: axs)
   111             end
   112         | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) thx =
   113             (*Universal quant: insert a free variable into body and continue*)
   114             let val fname = Name.variant (add_term_names (p,[])) a
   115             in dec_sko (subst_bound (Free(fname,T), p)) thx end
   116         | dec_sko (Const ("op &", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
   117         | dec_sko (Const ("op |", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
   118         | dec_sko (Const ("Trueprop", _) $ p) thx = dec_sko p thx
   119         | dec_sko t thx = thx (*Do nothing otherwise*)
   120   in  dec_sko (prop_of th) (thy,[])  end;
   121 
   122 (*Traverse a theorem, accumulating Skolem function definitions.*)
   123 fun assume_skofuns s th =
   124   let val sko_count = ref 0
   125       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 id = "sko_" ^ s ^ "_" ^ Int.toString (inc sko_count)
   132                 val c = Free (id, 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) (Thm.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 (Thm.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 val lambda_free = not o Term.has_abs;
   207 
   208 val monomorphic = not o Term.exists_type (Term.exists_subtype Term.is_TVar);
   209 
   210 fun dest_abs_list ct =
   211   let val (cv,ct') = Thm.dest_abs NONE ct
   212       val (cvs,cu) = dest_abs_list ct'
   213   in (cv::cvs, cu) end
   214   handle CTERM _ => ([],ct);
   215 
   216 fun abstract_rule_list [] [] th = th
   217   | abstract_rule_list (v::vs) (ct::cts) th = abstract_rule v ct (abstract_rule_list vs cts th)
   218   | abstract_rule_list _ _ th = raise THM ("abstract_rule_list", 0, [th]);
   219 
   220 
   221 val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0
   222 
   223 (*Does an existing abstraction definition have an RHS that matches the one we need now?
   224   thy is the current theory, which must extend that of theorem th.*)
   225 fun match_rhs thy t th =
   226   let val _ = Output.debug (fn()=> "match_rhs: " ^ string_of_cterm (cterm_of thy t) ^
   227                                    " against\n" ^ string_of_thm th);
   228       val (tyenv,tenv) = Pattern.first_order_match thy (rhs_of th, t) (tyenv0,tenv0)
   229       val term_insts = map Meson.term_pair_of (Vartab.dest tenv)
   230       val ct_pairs = if subthy (theory_of_thm th, thy) andalso
   231                         forall lambda_free (map #2 term_insts)
   232                      then map (pairself (cterm_of thy)) term_insts
   233                      else raise Pattern.MATCH (*Cannot allow lambdas in the instantiation*)
   234       fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T)
   235       val th' = cterm_instantiate ct_pairs th
   236   in  SOME (th, instantiate (map ctyp2 (Vartab.dest tyenv), []) th')  end
   237   handle _ => NONE;
   238 
   239 (*Traverse a theorem, declaring abstraction function definitions. String s is the suggested
   240   prefix for the constants. Resulting theory is returned in the first theorem. *)
   241 fun declare_absfuns s th =
   242   let val nref = ref 0
   243       fun abstract thy ct =
   244         if lambda_free (term_of ct) then (transfer thy (reflexive ct), [])
   245         else
   246         case term_of ct of
   247           Abs _ =>
   248             let val cname = Name.internal ("llabs_" ^ s ^ "_" ^ Int.toString (inc nref))
   249                 val _ = assert_eta_free ct;
   250                 val (cvs,cta) = dest_abs_list ct
   251                 val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs)
   252                 val _ = Output.debug (fn()=>"Nested lambda: " ^ string_of_cterm cta);
   253                 val (u'_th,defs) = abstract thy cta
   254                 val _ = Output.debug (fn()=>"Returned " ^ string_of_thm u'_th);
   255                 val cu' = Thm.rhs_of u'_th
   256                 val u' = term_of cu'
   257                 val abs_v_u = fold_rev (lambda o term_of) cvs u'
   258                 (*get the formal parameters: ALL variables free in the term*)
   259                 val args = term_frees abs_v_u
   260                 val _ = Output.debug (fn()=>Int.toString (length args) ^ " arguments");
   261                 val rhs = list_abs_free (map dest_Free args, abs_v_u)
   262                       (*Forms a lambda-abstraction over the formal parameters*)
   263                 val _ = Output.debug (fn()=>"Looking up " ^ string_of_cterm cu');
   264                 val thy = theory_of_thm u'_th
   265                 val (ax,ax',thy) =
   266                  case List.mapPartial (match_rhs thy abs_v_u)
   267                          (Net.match_term (!abstraction_cache) u') of
   268                      (ax,ax')::_ =>
   269                        (Output.debug (fn()=>"Re-using axiom " ^ string_of_thm ax);
   270                         (ax,ax',thy))
   271                    | [] =>
   272                       let val _ = Output.debug (fn()=>"Lookup was empty");
   273                           val Ts = map type_of args
   274                           val cT = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu'))
   275                           val c = Const (Sign.full_name thy cname, cT)
   276                           val thy = Sign.add_consts_authentic [(cname, cT, NoSyn)] thy
   277                                      (*Theory is augmented with the constant,
   278                                        then its definition*)
   279                           val cdef = cname ^ "_def"
   280                           val thy = Theory.add_defs_i false false
   281                                        [(cdef, equals cT $ c $ rhs)] thy
   282                                     handle ERROR _ => raise Clausify_failure thy
   283                           val _ = Output.debug (fn()=> "Definition is " ^ string_of_thm (get_axiom thy cdef));
   284                           val ax = get_axiom thy cdef |> freeze_thm
   285                                      |> mk_object_eq |> strip_lambdas (length args)
   286                                      |> mk_meta_eq |> Meson.generalize
   287                           val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax)
   288                           val _ = Output.debug (fn()=> "Declaring: " ^ string_of_thm ax ^ "\n" ^
   289                                                        "Instance: " ^ string_of_thm ax');
   290                           val _ = abstraction_cache := Net.insert_term eq_absdef
   291                                             ((Logic.varify u'), ax) (!abstraction_cache)
   292                             handle Net.INSERT =>
   293                               raise THM ("declare_absfuns: INSERT", 0, [th,u'_th,ax])
   294                        in  (ax,ax',thy)  end
   295             in Output.debug (fn()=>"Lookup result: " ^ string_of_thm ax');
   296                (transitive (abstract_rule_list vs cvs u'_th) (symmetric ax'), ax::defs) end
   297         | (t1$t2) =>
   298             let val (ct1,ct2) = Thm.dest_comb ct
   299                 val (th1,defs1) = abstract thy ct1
   300                 val (th2,defs2) = abstract (theory_of_thm th1) ct2
   301             in  (combination th1 th2, defs1@defs2)  end
   302       val _ = Output.debug (fn()=>"declare_absfuns, Abstracting: " ^ string_of_thm th);
   303       val (eqth,defs) = abstract (theory_of_thm th) (cprop_of th)
   304       val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs
   305       val _ = Output.debug (fn()=>"declare_absfuns, Result: " ^ string_of_thm (hd ths));
   306   in  (theory_of_thm eqth, map Drule.eta_contraction_rule ths)  end;
   307 
   308 fun name_of def = try (#1 o dest_Free o lhs_of) def;
   309 
   310 (*A name is valid provided it isn't the name of a defined abstraction.*)
   311 fun valid_name defs (Free(x,T)) = not (x mem_string (List.mapPartial name_of defs))
   312   | valid_name defs _ = false;
   313 
   314 (*s is the theorem name (hint) or the word "subgoal"*)
   315 fun assume_absfuns s th =
   316   let val thy = theory_of_thm th
   317       val cterm = cterm_of thy
   318       val abs_count = ref 0
   319       fun abstract ct =
   320         if lambda_free (term_of ct) then (reflexive ct, [])
   321         else
   322         case term_of ct of
   323           Abs (_,T,u) =>
   324             let val _ = assert_eta_free ct;
   325                 val (cvs,cta) = dest_abs_list ct
   326                 val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs)
   327                 val (u'_th,defs) = abstract cta
   328                 val cu' = Thm.rhs_of u'_th
   329                 val u' = term_of cu'
   330                 (*Could use Thm.cabs instead of lambda to work at level of cterms*)
   331                 val abs_v_u = fold_rev (lambda o term_of) cvs (term_of cu')
   332                 (*get the formal parameters: free variables not present in the defs
   333                   (to avoid taking abstraction function names as parameters) *)
   334                 val args = filter (valid_name defs) (term_frees abs_v_u)
   335                 val crhs = list_cabs (map cterm args, cterm abs_v_u)
   336                       (*Forms a lambda-abstraction over the formal parameters*)
   337                 val rhs = term_of crhs
   338                 val (ax,ax') =
   339                  case List.mapPartial (match_rhs thy abs_v_u)
   340                         (Net.match_term (!abstraction_cache) u') of
   341                      (ax,ax')::_ =>
   342                        (Output.debug (fn()=>"Re-using axiom " ^ string_of_thm ax);
   343                         (ax,ax'))
   344                    | [] =>
   345                       let val Ts = map type_of args
   346                           val const_ty = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu'))
   347                           val id = "llabs_" ^ s ^ "_" ^ Int.toString (inc abs_count)
   348                           val c = Free (id, const_ty)
   349                           val ax = assume (Thm.capply (cterm (equals const_ty $ c)) crhs)
   350                                      |> mk_object_eq |> strip_lambdas (length args)
   351                                      |> mk_meta_eq |> Meson.generalize
   352                           val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax)
   353                           val _ = abstraction_cache := Net.insert_term eq_absdef (rhs,ax)
   354                                     (!abstraction_cache)
   355                             handle Net.INSERT =>
   356                               raise THM ("assume_absfuns: INSERT", 0, [th,u'_th,ax])
   357                       in (ax,ax') end
   358             in Output.debug (fn()=>"Lookup result: " ^ string_of_thm ax');
   359                (transitive (abstract_rule_list vs cvs u'_th) (symmetric ax'), ax::defs) end
   360         | (t1$t2) =>
   361             let val (ct1,ct2) = Thm.dest_comb ct
   362                 val (t1',defs1) = abstract ct1
   363                 val (t2',defs2) = abstract ct2
   364             in  (combination t1' t2', defs1@defs2)  end
   365       val _ = Output.debug (fn()=>"assume_absfuns, Abstracting: " ^ string_of_thm th);
   366       val (eqth,defs) = abstract (cprop_of th)
   367       val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs
   368       val _ = Output.debug (fn()=>"assume_absfuns, Result: " ^ string_of_thm (hd ths));
   369   in  map Drule.eta_contraction_rule ths  end;
   370 
   371 
   372 (*cterms are used throughout for efficiency*)
   373 val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop;
   374 
   375 (*cterm version of mk_cTrueprop*)
   376 fun c_mkTrueprop A = Thm.capply cTrueprop A;
   377 
   378 (*Given an abstraction over n variables, replace the bound variables by free
   379   ones. Return the body, along with the list of free variables.*)
   380 fun c_variant_abs_multi (ct0, vars) =
   381       let val (cv,ct) = Thm.dest_abs NONE ct0
   382       in  c_variant_abs_multi (ct, cv::vars)  end
   383       handle CTERM _ => (ct0, rev vars);
   384 
   385 (*Given the definition of a Skolem function, return a theorem to replace
   386   an existential formula by a use of that function.
   387    Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
   388 fun skolem_of_def def =
   389   let val (c,rhs) = Thm.dest_equals (cprop_of (freeze_thm def))
   390       val (ch, frees) = c_variant_abs_multi (rhs, [])
   391       val (chilbert,cabs) = Thm.dest_comb ch
   392       val {thy,t, ...} = rep_cterm chilbert
   393       val T = case t of Const ("Hilbert_Choice.Eps", Type("fun",[_,T])) => T
   394                       | _ => raise THM ("skolem_of_def: expected Eps", 0, [def])
   395       val cex = Thm.cterm_of thy (HOLogic.exists_const T)
   396       val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
   397       and conc =  c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees)));
   398       fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS someI_ex) 1
   399   in  Goal.prove_internal [ex_tm] conc tacf
   400        |> forall_intr_list frees
   401        |> forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)
   402        |> Thm.varifyT
   403   end;
   404 
   405 
   406 (*This will refer to the final version of theory ATP_Linkup.*)
   407 val atp_linkup_thy_ref = Theory.check_thy @{theory}
   408 
   409 (*Transfer a theorem into theory ATP_Linkup.thy if it is not already
   410   inside that theory -- because it's needed for Skolemization.
   411   If called while ATP_Linkup is being created, it will transfer to the
   412   current version. If called afterward, it will transfer to the final version.*)
   413 fun transfer_to_ATP_Linkup th =
   414     transfer (Theory.deref atp_linkup_thy_ref) th handle THM _ => th;
   415 
   416 (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
   417 fun to_nnf th =
   418     th |> transfer_to_ATP_Linkup
   419        |> transform_elim |> zero_var_indexes |> freeze_thm
   420        |> Conv.fconv_rule ObjectLogic.atomize |> Meson.make_nnf |> strip_lambdas ~1;
   421 
   422 (*Generate Skolem functions for a theorem supplied in nnf*)
   423 fun skolem_of_nnf s th =
   424   map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s 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" ^ cat_lines (map string_of_thm ths'));
   430 
   431 fun assume_abstract s th =
   432   if lambda_free (prop_of th) then [th]
   433   else th |> Drule.eta_contraction_rule |> assume_absfuns s
   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 s ths = List.concat (map (assume_abstract s) ths);
   438 
   439 (*Replace lambdas by declared function definitions in the theorems*)
   440 fun declare_abstract s (thy, []) = (thy, [])
   441   | declare_abstract s (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 s
   447                 handle Clausify_failure thy_e => (thy_e,[])
   448           val _ = assert_lambda_free th_defs "declare_abstract: lambdas"
   449           val (thy'', ths') = declare_abstract (s^"'") (thy', ths)
   450       in  (thy'', th_defs @ ths')  end;
   451 
   452 (*Keep the full complexity of the original name*)
   453 fun flatten_name s = space_implode "_X" (NameSpace.explode s);
   454 
   455 fun fake_name th =
   456   if PureThy.has_name_hint th then flatten_name (PureThy.get_name_hint th)
   457   else gensym "unknown_thm_";
   458 
   459 fun name_or_string th =
   460   if PureThy.has_name_hint th then PureThy.get_name_hint th
   461   else string_of_thm th;
   462 
   463 (*Skolemize a named theorem, with Skolem functions as additional premises.*)
   464 fun skolem_thm th =
   465   let val nnfth = to_nnf th and s = fake_name th
   466   in  Meson.make_cnf (skolem_of_nnf s nnfth) nnfth |> assume_abstract_list s |> Meson.finish_cnf
   467   end
   468   handle THM _ => [];
   469 
   470 (*Declare Skolem functions for a theorem, supplied in nnf and with its name.
   471   It returns a modified theory, unless skolemization fails.*)
   472 fun skolem thy th =
   473      Option.map
   474         (fn nnfth =>
   475           let val _ = Output.debug (fn () => "skolemizing " ^ name_or_string th ^ ": ")
   476               val _ = Output.debug (fn () => string_of_thm nnfth)
   477               val s = fake_name th
   478               val (thy',defs) = declare_skofuns s nnfth thy
   479               val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth
   480               val _ = Output.debug (fn () => Int.toString (length cnfs) ^ " clauses yielded")
   481               val (thy'',cnfs') = declare_abstract s (thy',cnfs)
   482           in (map Goal.close_result (Meson.finish_cnf cnfs'), thy'') end
   483           handle Clausify_failure thy_e => ([],thy_e)
   484         )
   485       (try to_nnf th);
   486 
   487 (*The cache prevents repeated clausification of a theorem, and also repeated declaration of
   488   Skolem functions.*)
   489 structure ThmCache = TheoryDataFun
   490 (
   491   type T = (thm list) Thmtab.table;
   492   val empty = Thmtab.empty;
   493   fun copy tab : T = tab;
   494   val extend = copy;
   495   fun merge _ (tab1, tab2) : T = Thmtab.merge (K true) (tab1, tab2);
   496 );
   497 
   498 (*Populate the clause cache using the supplied theorem. Return the clausal form
   499   and modified theory.*)
   500 fun skolem_cache_thm th thy =
   501   case Thmtab.lookup (ThmCache.get thy) th of
   502       NONE =>
   503         (case skolem thy (Thm.transfer thy th) of
   504              NONE => ([th],thy)
   505            | SOME (cls,thy') =>
   506                  (Output.debug (fn () => "skolem_cache_thm: " ^ Int.toString (length cls) ^ 
   507                                          " clauses inserted into cache: " ^ name_or_string th);
   508                   (cls, ThmCache.put (Thmtab.update (th,cls) (ThmCache.get thy')) thy')))
   509     | SOME cls => (cls,thy);
   510 
   511 (*Exported function to convert Isabelle theorems into axiom clauses*)
   512 fun cnf_axiom th =
   513   let val thy = Theory.merge (Theory.deref atp_linkup_thy_ref, Thm.theory_of_thm th)
   514   in
   515       case Thmtab.lookup (ThmCache.get thy) th of
   516 	  NONE => (Output.debug (fn () => "cnf_axiom: " ^ name_or_string th);
   517 		   map Goal.close_result (skolem_thm th))
   518 	| SOME cls => cls
   519   end;
   520 
   521 fun pairname th = (PureThy.get_name_hint th, th);
   522 
   523 (**** Extract and Clausify theorems from a theory's claset and simpset ****)
   524 
   525 fun rules_of_claset cs =
   526   let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs
   527       val intros = safeIs @ hazIs
   528       val elims  = map Classical.classical_rule (safeEs @ hazEs)
   529   in
   530      Output.debug (fn () => "rules_of_claset intros: " ^ Int.toString(length intros) ^
   531             " elims: " ^ Int.toString(length elims));
   532      map pairname (intros @ elims)
   533   end;
   534 
   535 fun rules_of_simpset ss =
   536   let val ({rules,...}, _) = rep_ss ss
   537       val simps = Net.entries rules
   538   in
   539     Output.debug (fn () => "rules_of_simpset: " ^ Int.toString(length simps));
   540     map (fn r => (#name r, #thm r)) simps
   541   end;
   542 
   543 fun claset_rules_of ctxt = rules_of_claset (local_claset_of ctxt);
   544 fun simpset_rules_of ctxt = rules_of_simpset (local_simpset_of ctxt);
   545 
   546 fun atpset_rules_of ctxt = map pairname (ResAtpset.get ctxt);
   547 
   548 
   549 (**** Translate a set of theorems into CNF ****)
   550 
   551 (* classical rules: works for both FOL and HOL *)
   552 fun cnf_rules [] err_list = ([],err_list)
   553   | cnf_rules ((name,th) :: ths) err_list =
   554       let val (ts,es) = cnf_rules ths err_list
   555       in  (cnf_axiom th :: ts,es) handle  _ => (ts, (th::es))  end;
   556 
   557 fun pair_name_cls k (n, []) = []
   558   | pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss)
   559 
   560 fun cnf_rules_pairs_aux pairs [] = pairs
   561   | cnf_rules_pairs_aux pairs ((name,th)::ths) =
   562       let val pairs' = (pair_name_cls 0 (name, cnf_axiom th)) @ pairs
   563                        handle THM _ => pairs | ResClause.CLAUSE _ => pairs
   564       in  cnf_rules_pairs_aux pairs' ths  end;
   565 
   566 (*The combination of rev and tail recursion preserves the original order*)
   567 fun cnf_rules_pairs l = cnf_rules_pairs_aux [] (rev l);
   568 
   569 
   570 (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)
   571 
   572 (*Setup function: takes a theory and installs ALL known theorems into the clause cache*)
   573 
   574 val mark_skolemized = Sign.add_consts_i [("ResAxioms_endtheory", HOLogic.boolT, NoSyn)];
   575 
   576 fun skolem_cache th thy = #2 (skolem_cache_thm th thy);
   577 
   578 fun skolem_cache_all thy = fold skolem_cache (map #2 (PureThy.all_thms_of thy)) thy;
   579 
   580 fun skolem_cache_new thy = fold skolem_cache (map #2 (PureThy.thms_of thy)) thy;
   581 
   582 (*The cache can be kept smaller by inspecting the prop of each thm. Can ignore all that are
   583   lambda_free, but then the individual theory caches become much bigger.*)
   584 
   585 (*The new constant is a hack to prevent multiple execution*)
   586 fun clause_cache_endtheory thy =
   587   let val _ = Output.debug (fn () => "RexAxioms end theory action: " ^ Context.str_of_thy thy)
   588   in
   589     Option.map skolem_cache_new (try mark_skolemized thy)
   590   end;
   591 
   592 (*** meson proof methods ***)
   593 
   594 fun cnf_rules_of_ths ths = List.concat (map cnf_axiom ths);
   595 
   596 (*Expand all new*definitions of abstraction or Skolem functions in a proof state.*)
   597 fun is_absko (Const ("==", _) $ Free (a,_) $ u) = String.isPrefix "llabs_" a orelse String.isPrefix "sko_" a
   598   | is_absko _ = false;
   599 
   600 fun is_okdef xs (Const ("==", _) $ t $ u) =   (*Definition of Free, not in certain terms*)
   601       is_Free t andalso not (member (op aconv) xs t)
   602   | is_okdef _ _ = false
   603 
   604 (*This function tries to cope with open locales, which introduce hypotheses of the form
   605   Free == t, conjecture clauses, which introduce various hypotheses, and also definitions
   606   of llabs_ and sko_ functions. *)
   607 fun expand_defs_tac st0 st =
   608   let val hyps0 = #hyps (rep_thm st0)
   609       val hyps = #hyps (crep_thm st)
   610       val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps
   611       val defs = filter (is_absko o Thm.term_of) newhyps
   612       val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
   613                                       (map Thm.term_of hyps)
   614       val fixed = term_frees (concl_of st) @
   615                   foldl (gen_union (op aconv)) [] (map term_frees remaining_hyps)
   616   in  Output.debug (fn _ => "expand_defs_tac: " ^ string_of_thm st);
   617       Output.debug (fn _ => "  st0: " ^ string_of_thm st0);
   618       Output.debug (fn _ => "  defs: " ^ commas (map string_of_cterm defs));
   619       Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st]
   620   end;
   621 
   622 
   623 fun meson_general_tac ths i st0 =
   624  let val _ = Output.debug (fn () => "Meson called: " ^ cat_lines (map string_of_thm ths))
   625  in  (Meson.meson_claset_tac (cnf_rules_of_ths ths) HOL_cs i THEN expand_defs_tac st0) st0 end;
   626 
   627 val meson_method_setup = Method.add_methods
   628   [("meson", Method.thms_args (fn ths =>
   629       Method.SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths)),
   630     "MESON resolution proof procedure")];
   631 
   632 (** Attribute for converting a theorem into clauses **)
   633 
   634 fun meta_cnf_axiom th = map Meson.make_meta_clause (cnf_axiom th);
   635 
   636 fun clausify_rule (th,i) = List.nth (meta_cnf_axiom th, i)
   637 
   638 val clausify = Attrib.syntax (Scan.lift Args.nat
   639   >> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i))));
   640 
   641 
   642 (*** Converting a subgoal into negated conjecture clauses. ***)
   643 
   644 val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac];
   645 
   646 (*finish_cnf removes tautologies and functional reflexivity axioms, but by calling Thm.varifyT
   647   it can introduce TVars, which are useless in conjecture clauses.*)
   648 val no_tvars = null o term_tvars o prop_of;
   649 
   650 val neg_clausify =
   651   filter no_tvars o Meson.finish_cnf o assume_abstract_list "subgoal" o Meson.make_clauses;
   652 
   653 fun neg_conjecture_clauses st0 n =
   654   let val st = Seq.hd (neg_skolemize_tac n st0)
   655       val (params,_,_) = strip_context (Logic.nth_prem (n, Thm.prop_of st))
   656   in (neg_clausify (Option.valOf (metahyps_thms n st)), params) end
   657   handle Option => raise ERROR "unable to Skolemize subgoal";
   658 
   659 (*Conversion of a subgoal to conjecture clauses. Each clause has
   660   leading !!-bound universal variables, to express generality. *)
   661 val neg_clausify_tac =
   662   neg_skolemize_tac THEN'
   663   SUBGOAL
   664     (fn (prop,_) =>
   665      let val ts = Logic.strip_assums_hyp prop
   666      in EVERY1
   667          [METAHYPS
   668             (fn hyps =>
   669               (Method.insert_tac
   670                 (map forall_intr_vars (neg_clausify hyps)) 1)),
   671           REPEAT_DETERM_N (length ts) o (etac thin_rl)]
   672      end);
   673 
   674 (** The Skolemization attribute **)
   675 
   676 fun conj2_rule (th1,th2) = conjI OF [th1,th2];
   677 
   678 (*Conjoin a list of theorems to form a single theorem*)
   679 fun conj_rule []  = TrueI
   680   | conj_rule ths = foldr1 conj2_rule ths;
   681 
   682 fun skolem_attr (Context.Theory thy, th) =
   683       let val (cls, thy') = skolem_cache_thm th thy
   684       in (Context.Theory thy', conj_rule cls) end
   685   | skolem_attr (context, th) = (context, th)
   686 
   687 val setup_attrs = Attrib.add_attributes
   688   [("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem"),
   689    ("clausify", clausify, "conversion of theorem to clauses")];
   690 
   691 val setup_methods = Method.add_methods
   692   [("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac),
   693     "conversion of goal to conjecture clauses")];
   694 
   695 val setup = mark_skolemized #> skolem_cache_all #> ThmCache.init #> setup_attrs #> setup_methods;
   696 
   697 end;