src/HOL/Tools/res_atpset.ML

possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed

(*  ID:         $Id$
    Author:     Jia Meng, NICTA 

Set of rules used for ATPs
*)

signature RES_ATPSET =
sig
    type atpset
    val local_AtpSet_of: Proof.context -> atpset
    val add_atp_rules: atpset * Thm.thm list -> atpset
    val del_atp_rules: atpset * Thm.thm list -> atpset
    val get_AtpSet: theory -> atpset
    val print_local_AtpSet: Proof.context -> unit
    val AtpSet_of: theory -> atpset
    val add_atp_rule: Thm.thm * atpset -> atpset
    val del_atp_rule: Thm.thm * atpset -> atpset
    val print_atpset: atpset -> unit
    val setup: theory -> theory
    val get_local_AtpSet: Proof.context -> atpset
    val rep_as: atpset -> Thm.thm list
    val merge_atpset: atpset * atpset -> atpset
    val add_atp_rule': Thm.thm -> atpset -> atpset
    val del_atp_rule': Thm.thm -> atpset -> atpset
    val Add_AtpRs: Thm.thm list -> unit
    val Del_AtpRs: Thm.thm list -> unit
    val empty_atpset: atpset
    val put_local_AtpSet: atpset -> Proof.context -> Proof.context
    val print_AtpSet: theory -> unit
    val atp_rules_of_thy: theory -> Thm.thm list
    val atp_rules_of_ctxt: Proof.context -> Thm.thm list
end;



structure ResAtpSet : RES_ATPSET =

struct

datatype atpset = AtpSet of thm list


val mem_thm = member Drule.eq_thm_prop;
val rem_thm = remove Drule.eq_thm_prop;

val empty_atpset = AtpSet [];

fun add_atp_rule (thm,AtpSet thms) = 
    if mem_thm thms thm then (warning ("Ignoring duplicate ATP rules\n" ^ string_of_thm thm); AtpSet thms)
    else
	AtpSet (thm::thms);

fun add_atp_rule' thm ars = add_atp_rule (thm,ars);
fun add_atp_rules (ars,thms) =  foldl add_atp_rule ars thms;

fun del_atp_rule (thm,AtpSet thms) = 
    if mem_thm thms thm then AtpSet (rem_thm thm thms)
    else
	(warning "Undeclared rule for ATPs"; AtpSet thms);

fun del_atp_rule' thm ars = del_atp_rule (thm,ars);

fun del_atp_rules (ars,thms) = foldl del_atp_rule ars thms;

fun merge_atpset (ars1, AtpSet thms2) = add_atp_rules (ars1,thms2);

fun print_atpset (AtpSet thms) =
    let val pretty_thms = map Display.pretty_thm in
	[Pretty.big_list "Rules for ATPs:" (pretty_thms thms)]
	    |> Pretty.chunks |> Pretty.writeln
    end;

fun rep_as (AtpSet thms) = thms;

(* global AtpSet *)

structure GlobalAtpSet = TheoryDataFun
(struct
  val name = "AtpSet";
  type T = atpset ref;
  
  val empty = ref empty_atpset;
  fun copy (ref atpst) = ref atpst : T;
  val extend = copy;
  fun merge _ (ref atpst1, ref atpst2) =
      ref (merge_atpset (atpst1, atpst2));
  fun print (thy: Theory.theory) (ref atpst) = print_atpset atpst;
end);

val print_AtpSet = GlobalAtpSet.print; 
val get_AtpSet = ! o GlobalAtpSet.get;

val change_AtpSet_of = change o GlobalAtpSet.get;
fun change_AtpSet f = change_AtpSet_of (Context.the_context ()) f;


fun AtpSet_of thy = get_AtpSet thy;

fun Add_AtpRs args = change_AtpSet (fn ars => add_atp_rules (ars,args));

fun Del_AtpRs args = change_AtpSet (fn ars => del_atp_rules (ars,args));

fun atp_rules_of_thy thy = rep_as (AtpSet_of thy);

(* local AtpSet *)

structure LocalAtpSet = ProofDataFun
(struct
  val name = "AtpSet";
  type T = atpset;
  val init = get_AtpSet;
  fun print _ atpst = print_atpset atpst;
end);

val print_local_AtpSet = LocalAtpSet.print;

val get_local_AtpSet = LocalAtpSet.get;

val put_local_AtpSet = LocalAtpSet.put;

fun local_AtpSet_of ctxt = get_local_AtpSet ctxt;

fun atp_rules_of_ctxt ctxt = rep_as (local_AtpSet_of ctxt);

(* attributes *)
fun attrib f = Thm.declaration_attribute (fn th =>
   fn Context.Theory thy => (change_AtpSet_of thy (f th); Context.Theory thy)
    | Context.Proof ctxt => Context.Proof (LocalAtpSet.map (f th) ctxt));


val add_rule = attrib add_atp_rule';
val del_rule = attrib del_atp_rule';

val atpN = "atp";

val setup_attrs = Attrib.add_attributes
[(atpN, Attrib.add_del_args add_rule del_rule, "declaration of ATP rules")];

val setup = GlobalAtpSet.init #> LocalAtpSet.init #> setup_attrs;

end;