src/HOL/eqrule_HOL_data.ML
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 16179 fa7e70be26b0
child 17521 0f1c48de39f5
permissions -rw-r--r--
Constant "If" is now local
     1 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     2 (*  Title:      HOL/eqrule_HOL_data.ML
     3     Id:		$Id$
     4     Author:     Lucas Dixon, University of Edinburgh
     5                 lucas.dixon@ed.ac.uk
     6     Modified:   22 July 2004
     7     Created:    18 Feb 2004
     8 *)
     9 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
    10 (*  DESCRIPTION:
    11 
    12     Data for equality rules in the logic
    13 
    14 *)
    15 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    16 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    17 structure HOL_EqRuleData : EQRULE_DATA =
    18 struct
    19 
    20 val eq_reflection = thm "eq_reflection";
    21 val mp = thm "mp";
    22 val spec = thm "spec";
    23 val if_bool_eq_conj = thm "if_bool_eq_conj";
    24 val iffD1 = thm "iffD1";
    25 val conjunct2 = thm "conjunct2";
    26 val conjunct1 = thm "conjunct1";
    27 
    28 fun mk_eq th = case concl_of th of
    29         Const("==",_)$_$_       => SOME (th)
    30     |   _$(Const("op =",_)$_$_) => SOME (th RS eq_reflection)
    31     |   _ => NONE;
    32 
    33 val tranformation_pairs =
    34   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
    35    ("All", [spec]), ("True", []), ("False", []),
    36    ("HOL.If", [if_bool_eq_conj RS iffD1])];
    37 
    38 (*
    39 val mk_atomize:      (string * thm list) list -> thm -> thm list
    40 looks too specific to move it somewhere else
    41 *)
    42 fun mk_atomize pairs =
    43   let fun atoms th =
    44         (case Thm.concl_of th of
    45            Const("Trueprop",_) $ p =>
    46              (case Term.head_of p of
    47                 Const(a,_) =>
    48                   (case Library.assoc(pairs,a) of
    49                      SOME(rls) => List.concat (map atoms ([th] RL rls))
    50                    | NONE => [th])
    51               | _ => [th])
    52          | _ => [th])
    53   in atoms end;
    54 
    55 val prep_meta_eq = 
    56     (List.mapPartial  
    57        mk_eq
    58        o (mk_atomize tranformation_pairs)
    59        o Drule.gen_all 
    60        o zero_var_indexes)
    61 
    62 end;
    63 
    64 structure EqRuleData = HOL_EqRuleData;
    65 
    66 structure EQSubstTac = 
    67   EQSubstTacFUN(structure EqRuleData = EqRuleData);
    68 
    69