--- a/src/FOLP/simp.ML Tue May 07 14:24:30 2002 +0200
+++ b/src/FOLP/simp.ML Tue May 07 14:26:32 2002 +0200
@@ -64,7 +64,7 @@
(*** Indexing and filtering of theorems ***)
-fun eq_brl ((b1,th1),(b2,th2)) = b1=b2 andalso eq_thm(th1,th2);
+fun eq_brl ((b1,th1),(b2,th2)) = b1=b2 andalso Drule.eq_thm_prop (th1,th2);
(*insert a thm in a discrimination net by its lhs*)
fun lhs_insert_thm (th,net) =
@@ -247,7 +247,7 @@
(*insert a thm in a thm net*)
fun insert_thm_warn (th,net) =
- Net.insert_term((concl_of th, th), net, eq_thm)
+ Net.insert_term((concl_of th, th), net, Drule.eq_thm_prop)
handle Net.INSERT =>
(writeln"\nDuplicate rewrite or congruence rule:"; print_thm th;
net);
@@ -273,7 +273,7 @@
(*delete a thm from a thm net*)
fun delete_thm_warn (th,net) =
- Net.delete_term((concl_of th, th), net, eq_thm)
+ Net.delete_term((concl_of th, th), net, Drule.eq_thm_prop)
handle Net.DELETE =>
(writeln"\nNo such rewrite or congruence rule:"; print_thm th;
net);
@@ -281,7 +281,7 @@
val delete_thms = foldr delete_thm_warn;
fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
-let val congs' = foldl (gen_rem eq_thm) (congs,thms)
+let val congs' = foldl (gen_rem Drule.eq_thm_prop) (congs,thms)
in SS{auto_tac=auto_tac, congs= congs',
cong_net= delete_thms(map mk_trans thms,cong_net),
mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
@@ -289,7 +289,7 @@
fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
let fun find((p as (th,ths))::ps',ps) =
- if eq_thm(thm,th) then (ths,ps@ps') else find(ps',p::ps)
+ if Drule.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps)
| find([],simps') = (writeln"\nNo such rewrite or congruence rule:";
print_thm thm;
([],simps'))
--- a/src/HOL/Tools/inductive_codegen.ML Tue May 07 14:24:30 2002 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Tue May 07 14:26:32 2002 +0200
@@ -26,7 +26,7 @@
val empty = Symtab.empty;
val copy = I;
val prep_ext = I;
- val merge = Symtab.merge_multi eq_thm;
+ val merge = Symtab.merge_multi Drule.eq_thm_prop;
fun print _ _ = ();
end;
--- a/src/HOL/Tools/meson.ML Tue May 07 14:24:30 2002 +0200
+++ b/src/HOL/Tools/meson.ML Tue May 07 14:26:32 2002 +0200
@@ -266,7 +266,7 @@
(*Convert a list of clauses to (contrapositive) Horn clauses*)
fun make_horns ths =
name_thms "Horn#"
- (gen_distinct eq_thm (foldr (add_contras clause_rules) (ths,[])));
+ (gen_distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) (ths,[])));
(*Could simply use nprems_of, which would count remaining subgoals -- no
discrimination as to their size! With BEST_FIRST, fails for problem 41.*)
--- a/src/HOL/Tools/recfun_codegen.ML Tue May 07 14:24:30 2002 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML Tue May 07 14:26:32 2002 +0200
@@ -24,7 +24,7 @@
val empty = Symtab.empty;
val copy = I;
val prep_ext = I;
- val merge = Symtab.merge_multi eq_thm;
+ val merge = Symtab.merge_multi Drule.eq_thm_prop;
fun print _ _ = ();
end;
--- a/src/Provers/Arith/fast_lin_arith.ML Tue May 07 14:24:30 2002 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Tue May 07 14:26:32 2002 +0200
@@ -107,7 +107,8 @@
{add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2,
lessD = lessD2, simpset = simpset2}) =
{add_mono_thms = Drule.merge_rules (add_mono_thms1, add_mono_thms2),
- mult_mono_thms = gen_merge_lists' (eq_thm o pairself fst) mult_mono_thms1 mult_mono_thms2,
+ mult_mono_thms = gen_merge_lists' (Drule.eq_thm_prop o pairself fst)
+ mult_mono_thms1 mult_mono_thms2,
inj_thms = Drule.merge_rules (inj_thms1, inj_thms2),
lessD = Drule.merge_rules (lessD1, lessD2),
simpset = Simplifier.merge_ss (simpset1, simpset2)};
--- a/src/Provers/classical.ML Tue May 07 14:24:30 2002 +0200
+++ b/src/Provers/classical.ML Tue May 07 14:26:32 2002 +0200
@@ -310,8 +310,8 @@
fun delete x = delete_tagged_list (joinrules x);
fun delete' x = delete_tagged_list (joinrules' x);
-val mem_thm = gen_mem eq_thm
-and rem_thm = gen_rem eq_thm;
+val mem_thm = gen_mem Drule.eq_thm_prop
+and rem_thm = gen_rem Drule.eq_thm_prop;
(*Warn if the rule is already present ELSEWHERE in the claset. The addition
is still allowed.*)
@@ -601,10 +601,10 @@
treatment of priority might get muddled up.*)
fun merge_cs (cs as CS{safeIs, safeEs, hazIs, hazEs, ...},
CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2, swrappers, uwrappers, ...}) =
- let val safeIs' = gen_rems eq_thm (safeIs2,safeIs)
- val safeEs' = gen_rems eq_thm (safeEs2,safeEs)
- val hazIs' = gen_rems eq_thm ( hazIs2, hazIs)
- val hazEs' = gen_rems eq_thm ( hazEs2, hazEs)
+ let val safeIs' = gen_rems Drule.eq_thm_prop (safeIs2,safeIs)
+ val safeEs' = gen_rems Drule.eq_thm_prop (safeEs2,safeEs)
+ val hazIs' = gen_rems Drule.eq_thm_prop (hazIs2, hazIs)
+ val hazEs' = gen_rems Drule.eq_thm_prop (hazEs2, hazEs)
val cs1 = cs addSIs safeIs'
addSEs safeEs'
addIs hazIs'
--- a/src/Provers/induct_method.ML Tue May 07 14:24:30 2002 +0200
+++ b/src/Provers/induct_method.ML Tue May 07 14:26:32 2002 +0200
@@ -260,7 +260,7 @@
val sg = ProofContext.sign_of ctxt;
val cert = Thm.cterm_of sg;
- fun rule_versions r = Seq.cons (r, Seq.filter (not o curry eq_thm r)
+ fun rule_versions r = Seq.cons (r, Seq.filter (not o curry Thm.eq_thm r)
(Seq.make (fn () => Some (localize r, Seq.empty))))
|> Seq.map (rpair (RuleCases.get r));
--- a/src/Provers/simp.ML Tue May 07 14:24:30 2002 +0200
+++ b/src/Provers/simp.ML Tue May 07 14:26:32 2002 +0200
@@ -58,7 +58,7 @@
(*** Indexing and filtering of theorems ***)
-fun eq_brl ((b1,th1),(b2,th2)) = b1=b2 andalso eq_thm(th1,th2);
+fun eq_brl ((b1,th1),(b2,th2)) = b1=b2 andalso Drule.eq_thm_prop(th1,th2);
(*insert a thm in a discrimination net by its lhs*)
fun lhs_insert_thm (th,net) =
@@ -244,7 +244,7 @@
(*insert a thm in a thm net*)
fun insert_thm_warn (th,net) =
- Net.insert_term((concl_of th, th), net, eq_thm)
+ Net.insert_term((concl_of th, th), net, Drule.eq_thm_prop)
handle Net.INSERT =>
(writeln"\nDuplicate rewrite or congruence rule:"; print_thm th;
net);
@@ -289,7 +289,7 @@
(*delete a thm from a thm net*)
fun delete_thm_warn (th,net) =
- Net.delete_term((concl_of th, th), net, eq_thm)
+ Net.delete_term((concl_of th, th), net, Drule.eq_thm_prop)
handle Net.DELETE =>
(writeln"\nNo such rewrite or congruence rule:"; print_thm th;
net);
@@ -298,7 +298,7 @@
fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net,
splits,split_consts}, thms) =
-let val congs' = foldl (gen_rem eq_thm) (congs,thms)
+let val congs' = foldl (gen_rem Drule.eq_thm_prop) (congs,thms)
in SS{auto_tac=auto_tac, congs= congs',
cong_net= delete_thms(map mk_trans thms,cong_net),
mk_simps= normed_rews congs', simps=simps, simp_net=simp_net,
@@ -308,7 +308,7 @@
fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net,
splits,split_consts}, thm) =
let fun find((p as (th,ths))::ps',ps) =
- if eq_thm(thm,th) then (ths,ps@ps') else find(ps',p::ps)
+ if Drule.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps)
| find([],simps') = (writeln"\nNo such rewrite or congruence rule:";
print_thm thm;
([],simps'))
--- a/src/Pure/Isar/context_rules.ML Tue May 07 14:24:30 2002 +0200
+++ b/src/Pure/Isar/context_rules.ML Tue May 07 14:26:32 2002 +0200
@@ -103,7 +103,7 @@
fun del_rule th (rs as Rules {next, rules, netpairs, wrappers}) =
let
- fun eq_th (_, (_, th')) = Thm.eq_thm (th, th');
+ fun eq_th (_, (_, th')) = Drule.eq_thm_prop (th, th');
fun del b netpair = delete_tagged_brl ((b, th), netpair) handle Net.DELETE => netpair;
in
if not (exists eq_th rules) then rs
@@ -135,7 +135,7 @@
let
val wrappers = (gen_merge_lists' eq_snd ws1 ws2, gen_merge_lists' eq_snd ws1' ws2');
val rules = gen_merge_lists' (fn ((_, (k1, th1)), (_, (k2, th2))) =>
- k1 = k2 andalso Thm.eq_thm (th1, th2)) rules1 rules2;
+ k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) rules1 rules2;
val next = ~ (length rules);
val netpairs = foldl (fn (nps, (n, (w, ((i, b), th)))) =>
map_nth_elem i (curry insert_tagged_brl ((w, n), (b, th))) nps)
--- a/src/Pure/Isar/induct_attrib.ML Tue May 07 14:24:30 2002 +0200
+++ b/src/Pure/Isar/induct_attrib.ML Tue May 07 14:26:32 2002 +0200
@@ -84,7 +84,8 @@
type rules = (string * thm) NetRules.T;
val init_rules =
- NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso Thm.eq_thm (th1, th2));
+ NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
+ Drule.eq_thm_prop (th1, th2));
fun lookup_rule (rs: rules) name = Library.assoc (NetRules.rules rs, name);
--- a/src/Pure/Isar/net_rules.ML Tue May 07 14:24:30 2002 +0200
+++ b/src/Pure/Isar/net_rules.ML Tue May 07 14:26:32 2002 +0200
@@ -63,8 +63,8 @@
(* intro/elim rules *)
-val intro = init Thm.eq_thm Thm.concl_of;
-val elim = init Thm.eq_thm Thm.major_prem_of;
+val intro = init Drule.eq_thm_prop Thm.concl_of;
+val elim = init Drule.eq_thm_prop Thm.major_prem_of;
end;
--- a/src/Pure/drule.ML Tue May 07 14:24:30 2002 +0200
+++ b/src/Pure/drule.ML Tue May 07 14:26:32 2002 +0200
@@ -55,8 +55,9 @@
val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
val read_instantiate : (string*string)list -> thm -> thm
val cterm_instantiate : (cterm*cterm)list -> thm -> thm
+ val eq_thm_sg : thm * thm -> bool
+ val eq_thm_prop : thm * thm -> bool
val weak_eq_thm : thm * thm -> bool
- val eq_thm_sg : thm * thm -> bool
val size_of_thm : thm -> int
val reflexive_thm : thm
val symmetric_thm : thm
@@ -490,20 +491,21 @@
[th] => th
| _ => raise THM("COMP", 1, [tha,thb]);
+
(** theorem equality **)
-(*Do the two theorems have the same signature?*)
-fun eq_thm_sg (th1,th2) = Sign.eq_sg(#sign(rep_thm th1), #sign(rep_thm th2));
+val eq_thm_sg = Sign.eq_sg o pairself Thm.sign_of_thm;
+val eq_thm_prop = op aconv o pairself Thm.prop_of;
(*Useful "distance" function for BEST_FIRST*)
val size_of_thm = size_of_term o prop_of;
(*maintain lists of theorems --- preserving canonical order*)
-fun del_rules rs rules = Library.gen_rems Thm.eq_thm (rules, rs);
+fun del_rules rs rules = Library.gen_rems eq_thm_prop (rules, rs);
fun add_rules rs rules = rs @ del_rules rs rules;
val del_rule = del_rules o single;
val add_rule = add_rules o single;
-fun merge_rules (rules1, rules2) = gen_merge_lists' Thm.eq_thm rules1 rules2;
+fun merge_rules (rules1, rules2) = gen_merge_lists' eq_thm_prop rules1 rules2;
(** Mark Staples's weaker version of eq_thm: ignores variable renaming and
@@ -522,9 +524,7 @@
val vars = distinct (term_vars' prop);
in forall_intr_list (map (cterm_of sign) vars) th end;
-fun weak_eq_thm (tha,thb) =
- eq_thm(forall_intr_vars (freezeT tha), forall_intr_vars (freezeT thb));
-
+val weak_eq_thm = Thm.eq_thm o pairself (forall_intr_vars o freezeT);
(*** Meta-Rewriting Rules ***)
--- a/src/Pure/tactic.ML Tue May 07 14:24:30 2002 +0200
+++ b/src/Pure/tactic.ML Tue May 07 14:26:32 2002 +0200
@@ -410,7 +410,7 @@
(*delete one kbrl from the pair of nets*)
local
- fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = eq_thm (th, th')
+ fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Drule.eq_thm_prop (th, th')
in
fun delete_tagged_brl (brl as (eres, th), (inet, enet)) =
if eres then
--- a/src/Sequents/prover.ML Tue May 07 14:24:30 2002 +0200
+++ b/src/Sequents/prover.ML Tue May 07 14:26:32 2002 +0200
@@ -32,15 +32,15 @@
dups);
fun (Pack(safes,unsafes)) add_safes ths =
- let val dups = warn_duplicates (gen_inter eq_thm (ths,safes))
- val ths' = gen_rems eq_thm (ths,dups)
+ let val dups = warn_duplicates (gen_inter Drule.eq_thm_prop (ths,safes))
+ val ths' = gen_rems Drule.eq_thm_prop (ths,dups)
in
Pack(sort (make_ord less) (ths'@safes), unsafes)
end;
fun (Pack(safes,unsafes)) add_unsafes ths =
- let val dups = warn_duplicates (gen_inter eq_thm (ths,unsafes))
- val ths' = gen_rems eq_thm (ths,dups)
+ let val dups = warn_duplicates (gen_inter Drule.eq_thm_prop (ths,unsafes))
+ val ths' = gen_rems Drule.eq_thm_prop (ths,dups)
in
Pack(safes, sort (make_ord less) (ths'@unsafes))
end;
--- a/src/ZF/Tools/typechk.ML Tue May 07 14:24:30 2002 +0200
+++ b/src/ZF/Tools/typechk.ML Tue May 07 14:26:32 2002 +0200
@@ -46,8 +46,8 @@
net: thm Net.net}; (*discrimination net of the same rules*)
-val mem_thm = gen_mem eq_thm
-and rem_thm = gen_rem eq_thm;
+val mem_thm = gen_mem Drule.eq_thm_prop
+and rem_thm = gen_rem Drule.eq_thm_prop;
fun addTC (cs as TC{rules, net}, th) =
if mem_thm (th, rules) then
@@ -61,7 +61,7 @@
fun delTC (cs as TC{rules, net}, th) =
if mem_thm (th, rules) then
- TC{net = Net.delete_term ((concl_of th, th), net, eq_thm),
+ TC{net = Net.delete_term ((concl_of th, th), net, Drule.eq_thm_prop),
rules = rem_thm (rules,th)}
else (warning ("No such type-checking rule\n" ^ (string_of_thm th));
cs);
@@ -110,8 +110,8 @@
fun merge_tc (TC{rules,net}, TC{rules=rules',net=net'}) =
- TC {rules = gen_union eq_thm (rules,rules'),
- net = Net.merge (net, net', eq_thm)};
+ TC {rules = gen_union Drule.eq_thm_prop (rules,rules'),
+ net = Net.merge (net, net', Drule.eq_thm_prop)};
(*print tcsets*)
fun print_tc (TC{rules,...}) =