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