src/FOL/eqrule_FOL_data.ML
author wenzelm
Tue, 13 Sep 2005 22:19:23 +0200
changeset 17339 ab97ccef124a
parent 15570 8d8c70b41bab
child 17521 0f1c48de39f5
permissions -rw-r--r--
tuned Isar interfaces; tuned IsarThy.theorem_i;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     1
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     2
(*  Title:      sys/eqrule_FOL_data.ML
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     3
    Author:     Lucas Dixon, University of Edinburgh
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     4
                lucas.dixon@ed.ac.uk
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     5
    Created:    18 Feb 2004
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     6
*)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     7
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     8
(*  DESCRIPTION:
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     9
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    10
    Data for equality rules in the logic
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    11
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    12
*)   
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    13
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    14
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    15
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    16
structure ZF_EqRuleData : EQRULE_DATA =
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    17
struct
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    18
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    19
fun mk_eq th = case concl_of th of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15481
diff changeset
    20
        Const("==",_)$_$_       => SOME (th)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15481
diff changeset
    21
    |   _$(Const("op <->",_)$_$_) => SOME (th RS iff_reflection)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15481
diff changeset
    22
    |   _$(Const("op =",_)$_$_) => SOME (th RS eq_reflection)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15481
diff changeset
    23
    |   _ => NONE;
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    24
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    25
val tranformation_pairs =
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    26
  [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    27
   ("All", [spec]), ("True", []), ("False", [])];
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    28
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    29
(*
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    30
val mk_atomize:      (string * thm list) list -> thm -> thm list
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    31
looks too specific to move it somewhere else
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    32
*)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    33
fun mk_atomize pairs =
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    34
  let fun atoms th =
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    35
        (case Thm.concl_of th of
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    36
           Const("Trueprop",_) $ p =>
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    37
             (case Term.head_of p of
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    38
                Const(a,_) =>
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    39
                  (case Library.assoc(pairs,a) of
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
    40
                     SOME(rls) => List.concat (map atoms ([th] RL rls))
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15481
diff changeset
    41
                   | NONE => [th])
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    42
              | _ => [th])
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    43
         | _ => [th])
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    44
  in atoms end;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    45
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    46
val prep_meta_eq = 
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
    47
    (List.mapPartial  
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    48
       mk_eq
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    49
       o (mk_atomize tranformation_pairs)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    50
       o Drule.gen_all 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    51
       o zero_var_indexes)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    52
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    53
end;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    54
structure EqRuleData = ZF_EqRuleData;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    55
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    56
structure EQSubstTac = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    57
  EQSubstTacFUN(structure EqRuleData = EqRuleData);