src/FOL/eqrule_FOL_data.ML
author haftmann
Tue Sep 20 16:17:34 2005 +0200 (2005-09-20)
changeset 17521 0f1c48de39f5
parent 15570 8d8c70b41bab
child 18591 04b9f2bf5a48
permissions -rw-r--r--
introduced AList module in favor of assoc etc.
     1 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     2 (*  Title:      sys/eqrule_FOL_data.ML
     3     Author:     Lucas Dixon, University of Edinburgh
     4                 lucas.dixon@ed.ac.uk
     5     Created:    18 Feb 2004
     6 *)
     7 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     8 (*  DESCRIPTION:
     9 
    10     Data for equality rules in the logic
    11 
    12 *)   
    13 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    14 
    15 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    16 structure ZF_EqRuleData : EQRULE_DATA =
    17 struct
    18 
    19 fun mk_eq th = case concl_of th of
    20         Const("==",_)$_$_       => SOME (th)
    21     |   _$(Const("op <->",_)$_$_) => SOME (th RS iff_reflection)
    22     |   _$(Const("op =",_)$_$_) => SOME (th RS eq_reflection)
    23     |   _ => NONE;
    24 
    25 val tranformation_pairs =
    26   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
    27    ("All", [spec]), ("True", []), ("False", [])];
    28 
    29 (*
    30 val mk_atomize:      (string * thm list) list -> thm -> thm list
    31 looks too specific to move it somewhere else
    32 *)
    33 fun mk_atomize pairs =
    34   let fun atoms th =
    35         (case Thm.concl_of th of
    36            Const("Trueprop",_) $ p =>
    37              (case Term.head_of p of
    38                 Const(a,_) =>
    39                   (case AList.lookup (op =) pairs a of
    40                      SOME rls => List.concat (map atoms ([th] RL rls))
    41                    | NONE => [th])
    42               | _ => [th])
    43          | _ => [th])
    44   in atoms end;
    45 
    46 val prep_meta_eq = 
    47     (List.mapPartial  
    48        mk_eq
    49        o (mk_atomize tranformation_pairs)
    50        o Drule.gen_all 
    51        o zero_var_indexes)
    52 
    53 end;
    54 structure EqRuleData = ZF_EqRuleData;
    55 
    56 structure EQSubstTac = 
    57   EQSubstTacFUN(structure EqRuleData = EqRuleData);