src/HOL/Tools/Sledgehammer/clausifier.ML
author blanchet
Tue Jun 29 10:25:53 2010 +0200 (2010-06-29)
changeset 37626 1146291fe718
parent 37620 537beae999d7
child 37628 78334f400ae6
permissions -rw-r--r--
move blacklisting completely out of the clausifier;
the only reason it was in the clausifier as well was the Skolem cache
     1 (*  Title:      HOL/Tools/Sledgehammer/clausifier.ML
     2     Author:     Jia Meng, Cambridge University Computer Laboratory
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 
     5 Transformation of axiom rules (elim/intro/etc) into CNF forms.
     6 *)
     7 
     8 signature CLAUSIFIER =
     9 sig
    10   val cnf_axiom: theory -> thm -> thm list
    11   val cnf_rules_pairs :
    12     theory -> (string * thm) list -> ((string * int) * thm) list
    13   val neg_clausify: thm -> thm list
    14   val neg_conjecture_clauses:
    15     Proof.context -> thm -> int -> thm list list * (string * typ) list
    16 end;
    17 
    18 structure Clausifier : CLAUSIFIER =
    19 struct
    20 
    21 (**** Transformation of Elimination Rules into First-Order Formulas****)
    22 
    23 val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
    24 val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);
    25 
    26 (*Converts an elim-rule into an equivalent theorem that does not have the
    27   predicate variable.  Leaves other theorems unchanged.  We simply instantiate the
    28   conclusion variable to False.*)
    29 fun transform_elim th =
    30   case concl_of th of    (*conclusion variable*)
    31        @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
    32            Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
    33     | v as Var(_, @{typ prop}) =>
    34            Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
    35     | _ => th;
    36 
    37 (*To enforce single-threading*)
    38 exception Clausify_failure of theory;
    39 
    40 
    41 (**** SKOLEMIZATION BY INFERENCE (lcp) ****)
    42 
    43 fun mk_skolem_id t =
    44   let val T = fastype_of t in
    45     Const (@{const_name skolem_id}, T --> T) $ t
    46   end
    47 
    48 fun beta_eta_under_lambdas (Abs (s, T, t')) =
    49     Abs (s, T, beta_eta_under_lambdas t')
    50   | beta_eta_under_lambdas t = Envir.beta_eta_contract t
    51 
    52 (*Traverse a theorem, accumulating Skolem function definitions.*)
    53 fun assume_skolem_funs th =
    54   let
    55     fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) rhss =
    56         (*Existential: declare a Skolem function, then insert into body and continue*)
    57         let
    58           val args = OldTerm.term_frees body
    59           val Ts = map type_of args
    60           val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *)
    61           (* Forms a lambda-abstraction over the formal parameters *)
    62           val rhs =
    63             list_abs_free (map dest_Free args,
    64                            HOLogic.choice_const T $ beta_eta_under_lambdas body)
    65             |> mk_skolem_id
    66           val comb = list_comb (rhs, args)
    67         in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
    68       | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
    69         (*Universal quant: insert a free variable into body and continue*)
    70         let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
    71         in dec_sko (subst_bound (Free(fname,T), p)) rhss end
    72       | dec_sko (@{const "op &"} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
    73       | dec_sko (@{const "op |"} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
    74       | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss
    75       | dec_sko _ rhss = rhss
    76   in  dec_sko (prop_of th) []  end;
    77 
    78 
    79 (**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
    80 
    81 (*Returns the vars of a theorem*)
    82 fun vars_of_thm th =
    83   map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
    84 
    85 val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
    86 
    87 (* Removes the lambdas from an equation of the form t = (%x. u). *)
    88 fun extensionalize th =
    89   case prop_of th of
    90     _ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _]))
    91          $ _ $ Abs (s, _, _)) => extensionalize (th RS fun_cong_all)
    92   | _ => th
    93 
    94 fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true
    95   | is_quasi_lambda_free (t1 $ t2) =
    96     is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2
    97   | is_quasi_lambda_free (Abs _) = false
    98   | is_quasi_lambda_free _ = true
    99 
   100 val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B}));
   101 val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C}));
   102 val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S}));
   103 
   104 (*FIXME: requires more use of cterm constructors*)
   105 fun abstract ct =
   106   let
   107       val thy = theory_of_cterm ct
   108       val Abs(x,_,body) = term_of ct
   109       val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct)
   110       val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT
   111       fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K}
   112   in
   113       case body of
   114           Const _ => makeK()
   115         | Free _ => makeK()
   116         | Var _ => makeK()  (*though Var isn't expected*)
   117         | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
   118         | rator$rand =>
   119             if loose_bvar1 (rator,0) then (*C or S*)
   120                if loose_bvar1 (rand,0) then (*S*)
   121                  let val crator = cterm_of thy (Abs(x,xT,rator))
   122                      val crand = cterm_of thy (Abs(x,xT,rand))
   123                      val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S}
   124                      val (_,rhs) = Thm.dest_equals (cprop_of abs_S')
   125                  in
   126                    Thm.transitive abs_S' (Conv.binop_conv abstract rhs)
   127                  end
   128                else (*C*)
   129                  let val crator = cterm_of thy (Abs(x,xT,rator))
   130                      val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C}
   131                      val (_,rhs) = Thm.dest_equals (cprop_of abs_C')
   132                  in
   133                    Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
   134                  end
   135             else if loose_bvar1 (rand,0) then (*B or eta*)
   136                if rand = Bound 0 then Thm.eta_conversion ct
   137                else (*B*)
   138                  let val crand = cterm_of thy (Abs(x,xT,rand))
   139                      val crator = cterm_of thy rator
   140                      val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B}
   141                      val (_,rhs) = Thm.dest_equals (cprop_of abs_B')
   142                  in Thm.transitive abs_B' (Conv.arg_conv abstract rhs) end
   143             else makeK()
   144         | _ => raise Fail "abstract: Bad term"
   145   end;
   146 
   147 (* Traverse a theorem, remplacing lambda-abstractions with combinators. *)
   148 fun do_introduce_combinators ct =
   149   if is_quasi_lambda_free (term_of ct) then
   150     Thm.reflexive ct
   151   else case term_of ct of
   152     Abs _ =>
   153     let
   154       val (cv, cta) = Thm.dest_abs NONE ct
   155       val (v, _) = dest_Free (term_of cv)
   156       val u_th = do_introduce_combinators cta
   157       val cu = Thm.rhs_of u_th
   158       val comb_eq = abstract (Thm.cabs cv cu)
   159     in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
   160   | _ $ _ =>
   161     let val (ct1, ct2) = Thm.dest_comb ct in
   162         Thm.combination (do_introduce_combinators ct1)
   163                         (do_introduce_combinators ct2)
   164     end
   165 
   166 fun introduce_combinators th =
   167   if is_quasi_lambda_free (prop_of th) then
   168     th
   169   else
   170     let
   171       val th = Drule.eta_contraction_rule th
   172       val eqth = do_introduce_combinators (cprop_of th)
   173     in Thm.equal_elim eqth th end
   174     handle THM (msg, _, _) =>
   175            (warning ("Error in the combinator translation of " ^
   176                      Display.string_of_thm_without_context th ^
   177                      "\nException message: " ^ msg ^ ".");
   178             (* A type variable of sort "{}" will make abstraction fail. *)
   179             TrueI)
   180 
   181 (*cterms are used throughout for efficiency*)
   182 val cTrueprop = Thm.cterm_of @{theory HOL} HOLogic.Trueprop;
   183 
   184 (*Given an abstraction over n variables, replace the bound variables by free
   185   ones. Return the body, along with the list of free variables.*)
   186 fun c_variant_abs_multi (ct0, vars) =
   187       let val (cv,ct) = Thm.dest_abs NONE ct0
   188       in  c_variant_abs_multi (ct, cv::vars)  end
   189       handle CTERM _ => (ct0, rev vars);
   190 
   191 val skolem_id_def_raw = @{thms skolem_id_def_raw}
   192 
   193 (* Given the definition of a Skolem function, return a theorem to replace
   194    an existential formula by a use of that function.
   195    Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
   196 fun skolem_theorem_of_def thy rhs0 =
   197   let
   198     val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> Thm.cterm_of thy
   199     val rhs' = rhs |> Thm.dest_comb |> snd
   200     val (ch, frees) = c_variant_abs_multi (rhs', [])
   201     val (hilbert, cabs) = ch |> Thm.dest_comb |>> term_of
   202     val T =
   203       case hilbert of
   204         Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T
   205       | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [hilbert])
   206     val cex = Thm.cterm_of thy (HOLogic.exists_const T)
   207     val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs)
   208     and conc =
   209       Drule.list_comb (rhs, frees)
   210       |> Drule.beta_conv cabs |> Thm.capply cTrueprop
   211     fun tacf [prem] =
   212       rewrite_goals_tac skolem_id_def_raw
   213       THEN rtac ((prem |> rewrite_rule skolem_id_def_raw)
   214                  RS @{thm someI_ex}) 1
   215   in
   216     Goal.prove_internal [ex_tm] conc tacf
   217     |> forall_intr_list frees
   218     |> Thm.forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)
   219     |> Thm.varifyT_global
   220   end
   221 
   222 (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
   223 fun to_nnf th ctxt0 =
   224   let val th1 = th |> transform_elim |> zero_var_indexes
   225       val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
   226       val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
   227                     |> extensionalize
   228                     |> Meson.make_nnf ctxt
   229   in  (th3, ctxt)  end;
   230 
   231 (*Skolemize a named theorem, with Skolem functions as additional premises.*)
   232 fun skolemize_theorem thy th =
   233   let
   234     val ctxt0 = Variable.global_thm_context th
   235     val (nnfth, ctxt) = to_nnf th ctxt0
   236     val sko_ths = map (skolem_theorem_of_def thy) (assume_skolem_funs nnfth)
   237     val (cnfs, ctxt) = Meson.make_cnf sko_ths nnfth ctxt
   238   in
   239     cnfs |> map introduce_combinators
   240          |> Variable.export ctxt ctxt0
   241          |> Meson.finish_cnf
   242          |> map Thm.close_derivation
   243   end
   244   handle THM _ => []
   245 
   246 (* Convert Isabelle theorems into axiom clauses. *)
   247 (* FIXME: is transfer necessary? *)
   248 fun cnf_axiom thy = skolemize_theorem thy o Thm.transfer thy
   249 
   250 
   251 (**** Translate a set of theorems into CNF ****)
   252 
   253 (*The combination of rev and tail recursion preserves the original order*)
   254 fun cnf_rules_pairs thy =
   255   let
   256     fun do_one _ [] = []
   257       | do_one ((name, k), th) (cls :: clss) =
   258         ((name, k), cls) :: do_one ((name, k + 1), th) clss
   259     fun do_all pairs [] = pairs
   260       | do_all pairs ((name, th) :: ths) =
   261         let
   262           val new_pairs = do_one ((name, 0), th) (cnf_axiom thy th)
   263                           handle THM _ => []
   264         in do_all (new_pairs @ pairs) ths end
   265   in do_all [] o rev end
   266 
   267 
   268 (*** Converting a subgoal into negated conjecture clauses. ***)
   269 
   270 fun neg_skolemize_tac ctxt =
   271   EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt]
   272 
   273 val neg_clausify =
   274   single
   275   #> Meson.make_clauses_unsorted
   276   #> map introduce_combinators
   277   #> Meson.finish_cnf
   278 
   279 fun neg_conjecture_clauses ctxt st0 n =
   280   let
   281     (* "Option" is thrown if the assumptions contain schematic variables. *)
   282     val st = Seq.hd (neg_skolemize_tac ctxt n st0) handle Option.Option => st0
   283     val ({params, prems, ...}, _) =
   284       Subgoal.focus (Variable.set_body false ctxt) n st
   285   in (map neg_clausify prems, map (dest_Free o term_of o #2) params) end
   286 
   287 
   288 end;