src/HOL/Tools/res_axioms.ML
changeset 24937 340523598914
parent 24854 0ebcd575d3c6
child 24959 119793c84647
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Tue Oct 09 17:11:20 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Tue Oct 09 18:14:00 2007 +0200
     1.3 @@ -8,7 +8,6 @@
     1.4  signature RES_AXIOMS =
     1.5  sig
     1.6    val cnf_axiom: thm -> thm list
     1.7 -  val meta_cnf_axiom: thm -> thm list
     1.8    val pairname: thm -> string * thm
     1.9    val multi_base_blacklist: string list 
    1.10    val skolem_thm: thm -> thm list
    1.11 @@ -294,13 +293,14 @@
    1.12      transfer (Theory.deref atp_linkup_thy_ref) th handle THM _ => th;
    1.13  
    1.14  (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
    1.15 -fun to_nnf th =
    1.16 -    th |> transfer_to_ATP_Linkup
    1.17 -       |> transform_elim |> zero_var_indexes |> freeze_thm
    1.18 -       |> Conv.fconv_rule ObjectLogic.atomize |> Meson.make_nnf |> strip_lambdas ~1;
    1.19 +fun to_nnf th ctxt0 =
    1.20 +  let val th1 = th |> transfer_to_ATP_Linkup |> transform_elim |> zero_var_indexes
    1.21 +      val ((_,[th2]),ctxt) = Variable.import_thms false [th1] ctxt0
    1.22 +      val th3 = th2 |> Conv.fconv_rule ObjectLogic.atomize |> Meson.make_nnf |> strip_lambdas ~1
    1.23 +  in  (th3, ctxt)  end;
    1.24  
    1.25  (*Generate Skolem functions for a theorem supplied in nnf*)
    1.26 -fun skolem_of_nnf s th =
    1.27 +fun assume_skolem_of_def s th =
    1.28    map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
    1.29  
    1.30  fun assert_lambda_free ths msg =
    1.31 @@ -321,27 +321,32 @@
    1.32  
    1.33  (*Skolemize a named theorem, with Skolem functions as additional premises.*)
    1.34  fun skolem_thm th =
    1.35 -  let val nnfth = to_nnf th and s = fake_name th
    1.36 -  in  Meson.make_cnf (skolem_of_nnf s nnfth) nnfth |>  map combinators |> Meson.finish_cnf
    1.37 -  end
    1.38 +  let val ctxt0 = Variable.thm_context th
    1.39 +      val (nnfth,ctxt1) = to_nnf th ctxt0 and s = fake_name th
    1.40 +      val (cnfs,ctxt2) = Meson.make_cnf (assume_skolem_of_def s nnfth) nnfth ctxt1
    1.41 +  in  cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf  end
    1.42    handle THM _ => [];
    1.43  
    1.44  (*Declare Skolem functions for a theorem, supplied in nnf and with its name.
    1.45    It returns a modified theory, unless skolemization fails.*)
    1.46  fun skolem thy th =
    1.47 +  let val ctxt0 = Variable.thm_context th
    1.48 +  in
    1.49       Option.map
    1.50 -        (fn nnfth =>
    1.51 +        (fn (nnfth,ctxt1) =>
    1.52            let val _ = Output.debug (fn () => "skolemizing " ^ name_or_string th ^ ": ")
    1.53                val _ = Output.debug (fn () => string_of_thm nnfth)
    1.54                val s = fake_name th
    1.55                val (thy',defs) = declare_skofuns s nnfth thy
    1.56 -              val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth
    1.57 +              val (cnfs,ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1
    1.58                val _ = Output.debug (fn () => Int.toString (length cnfs) ^ " clauses yielded")
    1.59 -              val cnfs' = map combinators cnfs
    1.60 -          in (map Goal.close_result (Meson.finish_cnf cnfs'), thy') end
    1.61 +              val cnfs' = cnfs |> map combinators |> Variable.export ctxt2 ctxt0 
    1.62 +                               |> Meson.finish_cnf |> map Goal.close_result
    1.63 +          in (cnfs', thy') end
    1.64            handle Clausify_failure thy_e => ([],thy_e)
    1.65          )
    1.66 -      (try to_nnf th);
    1.67 +      (try (to_nnf th) ctxt0)
    1.68 +  end;
    1.69  
    1.70  (*The cache prevents repeated clausification of a theorem, and also repeated declaration of
    1.71    Skolem functions.*)
    1.72 @@ -529,12 +534,8 @@
    1.73  
    1.74  val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac];
    1.75  
    1.76 -(*finish_cnf removes tautologies and functional reflexivity axioms, but by calling Thm.varifyT
    1.77 -  it can introduce TVars, which are useless in conjecture clauses.*)
    1.78 -val no_tvars = null o term_tvars o prop_of;
    1.79 -
    1.80 -val neg_clausify =
    1.81 -  filter no_tvars o Meson.finish_cnf o map combinators o Meson.make_clauses;
    1.82 +fun neg_clausify sts =
    1.83 +  sts |> Meson.make_clauses |> map combinators |> Meson.finish_cnf;
    1.84  
    1.85  fun neg_conjecture_clauses st0 n =
    1.86    let val st = Seq.hd (neg_skolemize_tac n st0)