--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/eqrule_HOL_data.ML Tue Feb 01 18:01:57 2005 +0100
@@ -0,0 +1,68 @@
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
+(* Title: sys/eqrule_HOL_data.ML
+ Author: Lucas Dixon, University of Edinburgh
+ lucas.dixon@ed.ac.uk
+ Modified: 22 July 2004
+ Created: 18 Feb 2004
+*)
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
+(* DESCRIPTION:
+
+ Data for equality rules in the logic
+
+*)
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
+structure HOL_EqRuleData : EQRULE_DATA =
+struct
+
+val eq_reflection = thm "eq_reflection";
+val mp = thm "mp";
+val spec = thm "spec";
+val if_bool_eq_conj = thm "if_bool_eq_conj";
+val iffD1 = thm "iffD1";
+val conjunct2 = thm "conjunct2";
+val conjunct1 = thm "conjunct1";
+
+fun mk_eq th = case concl_of th of
+ Const("==",_)$_$_ => Some (th)
+ | _$(Const("op =",_)$_$_) => Some (th RS eq_reflection)
+ | _ => None;
+
+val tranformation_pairs =
+ [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
+ ("All", [spec]), ("True", []), ("False", []),
+ ("If", [if_bool_eq_conj RS iffD1])];
+
+(*
+val mk_atomize: (string * thm list) list -> thm -> thm list
+looks too specific to move it somewhere else
+*)
+fun mk_atomize pairs =
+ let fun atoms th =
+ (case Thm.concl_of th of
+ Const("Trueprop",_) $ p =>
+ (case Term.head_of p of
+ Const(a,_) =>
+ (case Library.assoc(pairs,a) of
+ Some(rls) => flat (map atoms ([th] RL rls))
+ | None => [th])
+ | _ => [th])
+ | _ => [th])
+ in atoms end;
+
+val prep_meta_eq =
+ (mapfilter
+ mk_eq
+ o (mk_atomize tranformation_pairs)
+ o Drule.gen_all
+ o zero_var_indexes)
+
+end;
+
+structure EqRuleData = HOL_EqRuleData;
+
+structure EQSubstTac =
+ EQSubstTacFUN(structure EqRuleData = EqRuleData);
+
+