src/HOL/Tools/res_atp.ML
changeset 32866 1238cbb7c08f
parent 32552 4d4ee06e9420
child 32952 aeb1e44fbc19
equal deleted inserted replaced
32863:5e8cef567042 32866:1238cbb7c08f
   515 fun isFO thy goal_cls = case linkup_logic_mode of
   515 fun isFO thy goal_cls = case linkup_logic_mode of
   516       Auto => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
   516       Auto => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
   517     | Fol => true
   517     | Fol => true
   518     | Hol => false
   518     | Hol => false
   519 
   519 
       
   520 fun ths_to_cls thy ths =
       
   521   ResAxioms.cnf_rules_pairs thy (filter check_named (map ResAxioms.pairname ths))
       
   522 
   520 fun get_relevant max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
   523 fun get_relevant max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
   521   let
   524   let
   522     val thy = ProofContext.theory_of ctxt
   525     val thy = ProofContext.theory_of ctxt
   523     val isFO = isFO thy goal_cls
   526     val isFO = isFO thy goal_cls
   524     val included_thms = get_clasimp_atp_lemmas ctxt
   527     val included_thms = get_clasimp_atp_lemmas ctxt
   525     val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique
   528     val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique
   526                                      |> restrict_to_logic thy isFO
   529                                      |> restrict_to_logic thy isFO
   527                                      |> remove_unwanted_clauses
   530                                      |> remove_unwanted_clauses
   528     val axcls = relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
   531     val axcls = relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
   529     val white_thms = filter check_named (map ResAxioms.pairname
   532     (* add whitelist *)
   530       (whitelist_fo @ (if isFO then [] else whitelist_ho) @ chain_ths))
   533     val white_cls = ths_to_cls thy (whitelist_fo @ (if isFO then [] else whitelist_ho))
   531     val white_cls = ResAxioms.cnf_rules_pairs thy white_thms
       
   532   in
   534   in
   533     white_cls @ axcls 
   535     white_cls @ axcls 
   534   end;
   536   end;
   535 
   537 
   536 (* prepare for passing to writer,
   538 (* prepare for passing to writer,
   537    create additional clauses based on the information from extra_cls *)
   539    create additional clauses based on the information from extra_cls *)
   538 fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy =
   540 fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy =
   539   let
   541   let
       
   542     (* add chain thms *)
       
   543     val chain_cls = ths_to_cls thy chain_ths
       
   544     val axcls = chain_cls @ axcls
       
   545     val extra_cls = chain_cls @ extra_cls
   540     val isFO = isFO thy goal_cls
   546     val isFO = isFO thy goal_cls
   541     val ccls = subtract_cls goal_cls extra_cls
   547     val ccls = subtract_cls goal_cls extra_cls
   542     val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm_global thy th)) ccls
   548     val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm_global thy th)) ccls
   543     val ccltms = map prop_of ccls
   549     val ccltms = map prop_of ccls
   544     and axtms = map (prop_of o #1) extra_cls
   550     and axtms = map (prop_of o #1) extra_cls