src/HOL/Tools/res_atp.ML
changeset 26675 fba93ce71435
parent 26662 39483503705f
child 26691 520c99e0b9a0
equal deleted inserted replaced
26674:fe93963ed76d 26675:fba93ce71435
   456   in
   456   in
   457       app (ignore o Polyhash.peekInsert ht) ax_clauses;
   457       app (ignore o Polyhash.peekInsert ht) ax_clauses;
   458       filter (not o known) c_clauses
   458       filter (not o known) c_clauses
   459   end;
   459   end;
   460 
   460 
       
   461 fun valid_facts facts =
       
   462   Facts.dest_table facts
       
   463   |> filter_out (fn (name, _) => !run_blacklist_filter andalso is_package_def name)
       
   464   |> map (apfst (Facts.extern facts))
       
   465   |> filter_out (NameSpace.is_hidden o #1)
       
   466   |> map (apsnd (filter_out ResAxioms.bad_for_atp));
       
   467 
   461 fun all_valid_thms ctxt =
   468 fun all_valid_thms ctxt =
   462   let
   469   let
   463     fun blacklisted s = !run_blacklist_filter andalso is_package_def s
   470     val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
   464 
       
   465     fun extern_valid space (name, ths) =
       
   466       let
       
   467         val is_valid = ProofContext.valid_thms ctxt;
       
   468         val xname = NameSpace.extern space name;
       
   469       in
       
   470         if blacklisted name then I
       
   471         else if is_valid (xname, ths) then cons (xname, filter_out ResAxioms.bad_for_atp ths)
       
   472         else if is_valid (name, ths) then cons (name, filter_out ResAxioms.bad_for_atp ths)
       
   473         else I
       
   474       end;
       
   475     val thy = ProofContext.theory_of ctxt;
       
   476     val all_thys = thy :: Theory.ancestors_of thy;
       
   477 
       
   478     val local_facts = ProofContext.facts_of ctxt;
   471     val local_facts = ProofContext.facts_of ctxt;
   479 
   472   in valid_facts global_facts @ valid_facts local_facts end;
   480     fun dest_valid (space, tab) = Symtab.fold (extern_valid space) tab [];
       
   481   in
       
   482     maps (dest_valid o PureThy.theorems_of) all_thys @
       
   483     fold (extern_valid (Facts.space_of local_facts)) (Facts.dest_table local_facts) []
       
   484   end;
       
   485 
   473 
   486 fun multi_name a (th, (n,pairs)) =
   474 fun multi_name a (th, (n,pairs)) =
   487   (n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs)
   475   (n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs)
   488 
   476 
   489 fun add_single_names ((a, []), pairs) = pairs
   477 fun add_single_names ((a, []), pairs) = pairs