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