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