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