src/HOL/Tools/res_axioms.ML
changeset 24937 340523598914
parent 24854 0ebcd575d3c6
child 24959 119793c84647
equal deleted inserted replaced
24936:68a36883f0ad 24937:340523598914
     6 *)
     6 *)
     7 
     7 
     8 signature RES_AXIOMS =
     8 signature RES_AXIOMS =
     9 sig
     9 sig
    10   val cnf_axiom: thm -> thm list
    10   val cnf_axiom: thm -> thm list
    11   val meta_cnf_axiom: thm -> thm list
       
    12   val pairname: thm -> string * thm
    11   val pairname: thm -> string * thm
    13   val multi_base_blacklist: string list 
    12   val multi_base_blacklist: string list 
    14   val skolem_thm: thm -> thm list
    13   val skolem_thm: thm -> thm list
    15   val cnf_rules_pairs: (string * thm) list -> (thm * (string * int)) list
    14   val cnf_rules_pairs: (string * thm) list -> (thm * (string * int)) list
    16   val cnf_rules_of_ths: thm list -> thm list
    15   val cnf_rules_of_ths: thm list -> thm list
   292   current version. If called afterward, it will transfer to the final version.*)
   291   current version. If called afterward, it will transfer to the final version.*)
   293 fun transfer_to_ATP_Linkup th =
   292 fun transfer_to_ATP_Linkup th =
   294     transfer (Theory.deref atp_linkup_thy_ref) th handle THM _ => th;
   293     transfer (Theory.deref atp_linkup_thy_ref) th handle THM _ => th;
   295 
   294 
   296 (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
   295 (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
   297 fun to_nnf th =
   296 fun to_nnf th ctxt0 =
   298     th |> transfer_to_ATP_Linkup
   297   let val th1 = th |> transfer_to_ATP_Linkup |> transform_elim |> zero_var_indexes
   299        |> transform_elim |> zero_var_indexes |> freeze_thm
   298       val ((_,[th2]),ctxt) = Variable.import_thms false [th1] ctxt0
   300        |> Conv.fconv_rule ObjectLogic.atomize |> Meson.make_nnf |> strip_lambdas ~1;
   299       val th3 = th2 |> Conv.fconv_rule ObjectLogic.atomize |> Meson.make_nnf |> strip_lambdas ~1
       
   300   in  (th3, ctxt)  end;
   301 
   301 
   302 (*Generate Skolem functions for a theorem supplied in nnf*)
   302 (*Generate Skolem functions for a theorem supplied in nnf*)
   303 fun skolem_of_nnf s th =
   303 fun assume_skolem_of_def s th =
   304   map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
   304   map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
   305 
   305 
   306 fun assert_lambda_free ths msg =
   306 fun assert_lambda_free ths msg =
   307   case filter (not o lambda_free o prop_of) ths of
   307   case filter (not o lambda_free o prop_of) ths of
   308       [] => ()
   308       [] => ()
   319   if PureThy.has_name_hint th then PureThy.get_name_hint th
   319   if PureThy.has_name_hint th then PureThy.get_name_hint th
   320   else string_of_thm th;
   320   else string_of_thm th;
   321 
   321 
   322 (*Skolemize a named theorem, with Skolem functions as additional premises.*)
   322 (*Skolemize a named theorem, with Skolem functions as additional premises.*)
   323 fun skolem_thm th =
   323 fun skolem_thm th =
   324   let val nnfth = to_nnf th and s = fake_name th
   324   let val ctxt0 = Variable.thm_context th
   325   in  Meson.make_cnf (skolem_of_nnf s nnfth) nnfth |>  map combinators |> Meson.finish_cnf
   325       val (nnfth,ctxt1) = to_nnf th ctxt0 and s = fake_name th
   326   end
   326       val (cnfs,ctxt2) = Meson.make_cnf (assume_skolem_of_def s nnfth) nnfth ctxt1
       
   327   in  cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf  end
   327   handle THM _ => [];
   328   handle THM _ => [];
   328 
   329 
   329 (*Declare Skolem functions for a theorem, supplied in nnf and with its name.
   330 (*Declare Skolem functions for a theorem, supplied in nnf and with its name.
   330   It returns a modified theory, unless skolemization fails.*)
   331   It returns a modified theory, unless skolemization fails.*)
   331 fun skolem thy th =
   332 fun skolem thy th =
       
   333   let val ctxt0 = Variable.thm_context th
       
   334   in
   332      Option.map
   335      Option.map
   333         (fn nnfth =>
   336         (fn (nnfth,ctxt1) =>
   334           let val _ = Output.debug (fn () => "skolemizing " ^ name_or_string th ^ ": ")
   337           let val _ = Output.debug (fn () => "skolemizing " ^ name_or_string th ^ ": ")
   335               val _ = Output.debug (fn () => string_of_thm nnfth)
   338               val _ = Output.debug (fn () => string_of_thm nnfth)
   336               val s = fake_name th
   339               val s = fake_name th
   337               val (thy',defs) = declare_skofuns s nnfth thy
   340               val (thy',defs) = declare_skofuns s nnfth thy
   338               val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth
   341               val (cnfs,ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1
   339               val _ = Output.debug (fn () => Int.toString (length cnfs) ^ " clauses yielded")
   342               val _ = Output.debug (fn () => Int.toString (length cnfs) ^ " clauses yielded")
   340               val cnfs' = map combinators cnfs
   343               val cnfs' = cnfs |> map combinators |> Variable.export ctxt2 ctxt0 
   341           in (map Goal.close_result (Meson.finish_cnf cnfs'), thy') end
   344                                |> Meson.finish_cnf |> map Goal.close_result
       
   345           in (cnfs', thy') end
   342           handle Clausify_failure thy_e => ([],thy_e)
   346           handle Clausify_failure thy_e => ([],thy_e)
   343         )
   347         )
   344       (try to_nnf th);
   348       (try (to_nnf th) ctxt0)
       
   349   end;
   345 
   350 
   346 (*The cache prevents repeated clausification of a theorem, and also repeated declaration of
   351 (*The cache prevents repeated clausification of a theorem, and also repeated declaration of
   347   Skolem functions.*)
   352   Skolem functions.*)
   348 structure ThmCache = TheoryDataFun
   353 structure ThmCache = TheoryDataFun
   349 (
   354 (
   527 
   532 
   528 (*** Converting a subgoal into negated conjecture clauses. ***)
   533 (*** Converting a subgoal into negated conjecture clauses. ***)
   529 
   534 
   530 val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac];
   535 val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac];
   531 
   536 
   532 (*finish_cnf removes tautologies and functional reflexivity axioms, but by calling Thm.varifyT
   537 fun neg_clausify sts =
   533   it can introduce TVars, which are useless in conjecture clauses.*)
   538   sts |> Meson.make_clauses |> map combinators |> Meson.finish_cnf;
   534 val no_tvars = null o term_tvars o prop_of;
       
   535 
       
   536 val neg_clausify =
       
   537   filter no_tvars o Meson.finish_cnf o map combinators o Meson.make_clauses;
       
   538 
   539 
   539 fun neg_conjecture_clauses st0 n =
   540 fun neg_conjecture_clauses st0 n =
   540   let val st = Seq.hd (neg_skolemize_tac n st0)
   541   let val st = Seq.hd (neg_skolemize_tac n st0)
   541       val (params,_,_) = strip_context (Logic.nth_prem (n, Thm.prop_of st))
   542       val (params,_,_) = strip_context (Logic.nth_prem (n, Thm.prop_of st))
   542   in (neg_clausify (Option.valOf (metahyps_thms n st)), params) end
   543   in (neg_clausify (Option.valOf (metahyps_thms n st)), params) end