src/HOL/eqrule_HOL_data.ML
author wenzelm
Thu, 22 Dec 2005 00:28:36 +0100
changeset 18457 356a9f711899
parent 17521 0f1c48de39f5
child 18591 04b9f2bf5a48
permissions -rw-r--r--
structure ProjectRule; updated auxiliary facts for induct method; tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     1
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
16179
fa7e70be26b0 header;
wenzelm
parents: 15570
diff changeset
     2
(*  Title:      HOL/eqrule_HOL_data.ML
fa7e70be26b0 header;
wenzelm
parents: 15570
diff changeset
     3
    Id:		$Id$
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     4
    Author:     Lucas Dixon, University of Edinburgh
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     5
                lucas.dixon@ed.ac.uk
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     6
    Modified:   22 July 2004
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     7
    Created:    18 Feb 2004
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     8
*)
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
(*  DESCRIPTION:
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
    Data for equality rules in the logic
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
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    17
structure HOL_EqRuleData : EQRULE_DATA =
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    18
struct
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    19
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    20
val eq_reflection = thm "eq_reflection";
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    21
val mp = thm "mp";
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    22
val spec = thm "spec";
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    23
val if_bool_eq_conj = thm "if_bool_eq_conj";
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    24
val iffD1 = thm "iffD1";
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    25
val conjunct2 = thm "conjunct2";
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    26
val conjunct1 = thm "conjunct1";
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    27
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    28
fun mk_eq th = case concl_of th of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15481
diff changeset
    29
        Const("==",_)$_$_       => SOME (th)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15481
diff changeset
    30
    |   _$(Const("op =",_)$_$_) => SOME (th RS eq_reflection)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15481
diff changeset
    31
    |   _ => NONE;
15481
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
val tranformation_pairs =
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    34
  [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    35
   ("All", [spec]), ("True", []), ("False", []),
16587
b34c8aa657a5 Constant "If" is now local
paulson
parents: 16179
diff changeset
    36
   ("HOL.If", [if_bool_eq_conj RS iffD1])];
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    37
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    38
(*
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    39
val mk_atomize:      (string * thm list) list -> thm -> thm list
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    40
looks too specific to move it somewhere else
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    41
*)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    42
fun mk_atomize pairs =
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    43
  let fun atoms th =
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    44
        (case Thm.concl_of th of
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    45
           Const("Trueprop",_) $ p =>
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    46
             (case Term.head_of p of
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    47
                Const(a,_) =>
17521
0f1c48de39f5 introduced AList module in favor of assoc etc.
haftmann
parents: 16587
diff changeset
    48
                  (case AList.lookup (op =) pairs a of
0f1c48de39f5 introduced AList module in favor of assoc etc.
haftmann
parents: 16587
diff changeset
    49
                     SOME rls => List.concat (map atoms ([th] RL rls))
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15481
diff changeset
    50
                   | NONE => [th])
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    51
              | _ => [th])
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    52
         | _ => [th])
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    53
  in atoms end;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    54
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    55
val prep_meta_eq = 
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
    56
    (List.mapPartial  
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    57
       mk_eq
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    58
       o (mk_atomize tranformation_pairs)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    59
       o Drule.gen_all 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    60
       o zero_var_indexes)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    61
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    62
end;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    63
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    64
structure EqRuleData = HOL_EqRuleData;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    65
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    66
structure EQSubstTac = 
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    67
  EQSubstTacFUN(structure EqRuleData = EqRuleData);
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    68
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    69