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