# File eqrule_FOL_data.ML

    (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    (*  Title:      sys/eqrule_FOL_data.ML
        Author:     Lucas Dixon, University of Edinburgh
                    lucas.dixon@ed.ac.uk
        Created:    18 Feb 2004
    *)
    (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    (*  DESCRIPTION:

        Data for equality rules in the logic

    *)
    (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)

    (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    structure ZF_EqRuleData : EQRULE_DATA =
    struct

    fun mk_eq th = case concl_of th of
            Const("==",_)$_$_       => SOME (th)
        |   _$(Const("op <->",_)$_$_) => SOME (th RS iff_reflection)
        |   _$(Const("op =",_)$_$_) => SOME (th RS eq_reflection)
        |   _ => NONE;

    val tranformation_pairs =
      [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
       ("All", [spec]), ("True", []), ("False", [])];

    (*
    val mk_atomize:      (string * thm list) list -> thm -> thm list
    looks too specific to move it somewhere else
    *)
    fun mk_atomize pairs =
      let fun atoms th =
            (case Thm.concl_of th of
               Const("Trueprop",_) $ p =>
                 (case Term.head_of p of
                    Const(a,_) =>
                      (case AList.lookup (op =) pairs a of
                         SOME rls => List.concat (map atoms ([th] RL rls))
                       | NONE => [th])
                  | _ => [th])
             | _ => [th])
      in atoms end;

    val prep_meta_eq =
        (List.mapPartial
           mk_eq
           o (mk_atomize tranformation_pairs)
           o Drule.gen_all
           o zero_var_indexes)

    end;
    structure EqRuleData = ZF_EqRuleData;

    structure EQSubstTac =
      EQSubstTacFUN(structure EqRuleData = EqRuleData);