use eq_thm_prop instead of slightly inadequate eq_thm;
authorwenzelm
Tue May 07 14:26:32 2002 +0200 (2002-05-07)
changeset 131053d1e7a199bdc
parent 13104 df7aac8543c9
child 13106 f6561b003a35
use eq_thm_prop instead of slightly inadequate eq_thm;
src/FOLP/simp.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/recfun_codegen.ML
src/Provers/Arith/fast_lin_arith.ML
src/Provers/classical.ML
src/Provers/induct_method.ML
src/Provers/simp.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/induct_attrib.ML
src/Pure/Isar/net_rules.ML
src/Pure/drule.ML
src/Pure/tactic.ML
src/Sequents/prover.ML
src/ZF/Tools/typechk.ML
     1.1 --- a/src/FOLP/simp.ML	Tue May 07 14:24:30 2002 +0200
     1.2 +++ b/src/FOLP/simp.ML	Tue May 07 14:26:32 2002 +0200
     1.3 @@ -64,7 +64,7 @@
     1.4  
     1.5  (*** Indexing and filtering of theorems ***)
     1.6  
     1.7 -fun eq_brl ((b1,th1),(b2,th2)) = b1=b2 andalso eq_thm(th1,th2);
     1.8 +fun eq_brl ((b1,th1),(b2,th2)) = b1=b2 andalso Drule.eq_thm_prop (th1,th2);
     1.9  
    1.10  (*insert a thm in a discrimination net by its lhs*)
    1.11  fun lhs_insert_thm (th,net) =
    1.12 @@ -247,7 +247,7 @@
    1.13  
    1.14  (*insert a thm in a thm net*)
    1.15  fun insert_thm_warn (th,net) = 
    1.16 -  Net.insert_term((concl_of th, th), net, eq_thm)
    1.17 +  Net.insert_term((concl_of th, th), net, Drule.eq_thm_prop)
    1.18    handle Net.INSERT => 
    1.19      (writeln"\nDuplicate rewrite or congruence rule:"; print_thm th;
    1.20       net);
    1.21 @@ -273,7 +273,7 @@
    1.22  
    1.23  (*delete a thm from a thm net*)
    1.24  fun delete_thm_warn (th,net) = 
    1.25 -  Net.delete_term((concl_of th, th), net, eq_thm)
    1.26 +  Net.delete_term((concl_of th, th), net, Drule.eq_thm_prop)
    1.27    handle Net.DELETE => 
    1.28      (writeln"\nNo such rewrite or congruence rule:";  print_thm th;
    1.29       net);
    1.30 @@ -281,7 +281,7 @@
    1.31  val delete_thms = foldr delete_thm_warn;
    1.32  
    1.33  fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
    1.34 -let val congs' = foldl (gen_rem eq_thm) (congs,thms)
    1.35 +let val congs' = foldl (gen_rem Drule.eq_thm_prop) (congs,thms)
    1.36  in SS{auto_tac=auto_tac, congs= congs',
    1.37        cong_net= delete_thms(map mk_trans thms,cong_net),
    1.38        mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
    1.39 @@ -289,7 +289,7 @@
    1.40  
    1.41  fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
    1.42  let fun find((p as (th,ths))::ps',ps) =
    1.43 -          if eq_thm(thm,th) then (ths,ps@ps') else find(ps',p::ps)
    1.44 +          if Drule.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps)
    1.45        | find([],simps') = (writeln"\nNo such rewrite or congruence rule:";
    1.46                             print_thm thm;
    1.47                             ([],simps'))
     2.1 --- a/src/HOL/Tools/inductive_codegen.ML	Tue May 07 14:24:30 2002 +0200
     2.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Tue May 07 14:26:32 2002 +0200
     2.3 @@ -26,7 +26,7 @@
     2.4    val empty = Symtab.empty;
     2.5    val copy = I;
     2.6    val prep_ext = I;
     2.7 -  val merge = Symtab.merge_multi eq_thm;
     2.8 +  val merge = Symtab.merge_multi Drule.eq_thm_prop;
     2.9    fun print _ _ = ();
    2.10  end;
    2.11  
     3.1 --- a/src/HOL/Tools/meson.ML	Tue May 07 14:24:30 2002 +0200
     3.2 +++ b/src/HOL/Tools/meson.ML	Tue May 07 14:26:32 2002 +0200
     3.3 @@ -266,7 +266,7 @@
     3.4  (*Convert a list of clauses to (contrapositive) Horn clauses*)
     3.5  fun make_horns ths =
     3.6      name_thms "Horn#"
     3.7 -      (gen_distinct eq_thm (foldr (add_contras clause_rules) (ths,[])));
     3.8 +      (gen_distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) (ths,[])));
     3.9  
    3.10  (*Could simply use nprems_of, which would count remaining subgoals -- no
    3.11    discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
     4.1 --- a/src/HOL/Tools/recfun_codegen.ML	Tue May 07 14:24:30 2002 +0200
     4.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Tue May 07 14:26:32 2002 +0200
     4.3 @@ -24,7 +24,7 @@
     4.4    val empty = Symtab.empty;
     4.5    val copy = I;
     4.6    val prep_ext = I;
     4.7 -  val merge = Symtab.merge_multi eq_thm;
     4.8 +  val merge = Symtab.merge_multi Drule.eq_thm_prop;
     4.9    fun print _ _ = ();
    4.10  end;
    4.11  
     5.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Tue May 07 14:24:30 2002 +0200
     5.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Tue May 07 14:26:32 2002 +0200
     5.3 @@ -107,7 +107,8 @@
     5.4               {add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2,
     5.5                lessD = lessD2, simpset = simpset2}) =
     5.6      {add_mono_thms = Drule.merge_rules (add_mono_thms1, add_mono_thms2),
     5.7 -     mult_mono_thms = gen_merge_lists' (eq_thm o pairself fst) mult_mono_thms1 mult_mono_thms2,
     5.8 +     mult_mono_thms = gen_merge_lists' (Drule.eq_thm_prop o pairself fst)
     5.9 +       mult_mono_thms1 mult_mono_thms2,
    5.10       inj_thms = Drule.merge_rules (inj_thms1, inj_thms2),
    5.11       lessD = Drule.merge_rules (lessD1, lessD2),
    5.12       simpset = Simplifier.merge_ss (simpset1, simpset2)};
     6.1 --- a/src/Provers/classical.ML	Tue May 07 14:24:30 2002 +0200
     6.2 +++ b/src/Provers/classical.ML	Tue May 07 14:26:32 2002 +0200
     6.3 @@ -310,8 +310,8 @@
     6.4  fun delete x = delete_tagged_list (joinrules x);
     6.5  fun delete' x = delete_tagged_list (joinrules' x);
     6.6  
     6.7 -val mem_thm = gen_mem eq_thm
     6.8 -and rem_thm = gen_rem eq_thm;
     6.9 +val mem_thm = gen_mem Drule.eq_thm_prop
    6.10 +and rem_thm = gen_rem Drule.eq_thm_prop;
    6.11  
    6.12  (*Warn if the rule is already present ELSEWHERE in the claset.  The addition
    6.13    is still allowed.*)
    6.14 @@ -601,10 +601,10 @@
    6.15    treatment of priority might get muddled up.*)
    6.16  fun merge_cs (cs as CS{safeIs, safeEs, hazIs, hazEs, ...},
    6.17       CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2, swrappers, uwrappers, ...}) =
    6.18 -  let val safeIs' = gen_rems eq_thm (safeIs2,safeIs)
    6.19 -      val safeEs' = gen_rems eq_thm (safeEs2,safeEs)
    6.20 -      val  hazIs' = gen_rems eq_thm ( hazIs2, hazIs)
    6.21 -      val  hazEs' = gen_rems eq_thm ( hazEs2, hazEs)
    6.22 +  let val safeIs' = gen_rems Drule.eq_thm_prop (safeIs2,safeIs)
    6.23 +      val safeEs' = gen_rems Drule.eq_thm_prop (safeEs2,safeEs)
    6.24 +      val hazIs' = gen_rems Drule.eq_thm_prop (hazIs2, hazIs)
    6.25 +      val hazEs' = gen_rems Drule.eq_thm_prop (hazEs2, hazEs)
    6.26        val cs1   = cs addSIs safeIs'
    6.27                       addSEs safeEs'
    6.28                       addIs  hazIs'
     7.1 --- a/src/Provers/induct_method.ML	Tue May 07 14:24:30 2002 +0200
     7.2 +++ b/src/Provers/induct_method.ML	Tue May 07 14:26:32 2002 +0200
     7.3 @@ -260,7 +260,7 @@
     7.4      val sg = ProofContext.sign_of ctxt;
     7.5      val cert = Thm.cterm_of sg;
     7.6  
     7.7 -    fun rule_versions r = Seq.cons (r, Seq.filter (not o curry eq_thm r)
     7.8 +    fun rule_versions r = Seq.cons (r, Seq.filter (not o curry Thm.eq_thm r)
     7.9          (Seq.make (fn () => Some (localize r, Seq.empty))))
    7.10        |> Seq.map (rpair (RuleCases.get r));
    7.11  
     8.1 --- a/src/Provers/simp.ML	Tue May 07 14:24:30 2002 +0200
     8.2 +++ b/src/Provers/simp.ML	Tue May 07 14:26:32 2002 +0200
     8.3 @@ -58,7 +58,7 @@
     8.4  
     8.5  (*** Indexing and filtering of theorems ***)
     8.6  
     8.7 -fun eq_brl ((b1,th1),(b2,th2)) = b1=b2 andalso eq_thm(th1,th2);
     8.8 +fun eq_brl ((b1,th1),(b2,th2)) = b1=b2 andalso Drule.eq_thm_prop(th1,th2);
     8.9  
    8.10  (*insert a thm in a discrimination net by its lhs*)
    8.11  fun lhs_insert_thm (th,net) =
    8.12 @@ -244,7 +244,7 @@
    8.13  
    8.14  (*insert a thm in a thm net*)
    8.15  fun insert_thm_warn (th,net) = 
    8.16 -  Net.insert_term((concl_of th, th), net, eq_thm)
    8.17 +  Net.insert_term((concl_of th, th), net, Drule.eq_thm_prop)
    8.18    handle Net.INSERT => 
    8.19      (writeln"\nDuplicate rewrite or congruence rule:"; print_thm th;
    8.20       net);
    8.21 @@ -289,7 +289,7 @@
    8.22  
    8.23  (*delete a thm from a thm net*)
    8.24  fun delete_thm_warn (th,net) = 
    8.25 -  Net.delete_term((concl_of th, th), net, eq_thm)
    8.26 +  Net.delete_term((concl_of th, th), net, Drule.eq_thm_prop)
    8.27    handle Net.DELETE => 
    8.28      (writeln"\nNo such rewrite or congruence rule:";  print_thm th;
    8.29       net);
    8.30 @@ -298,7 +298,7 @@
    8.31  
    8.32  fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net,
    8.33                     splits,split_consts}, thms) =
    8.34 -let val congs' = foldl (gen_rem eq_thm) (congs,thms)
    8.35 +let val congs' = foldl (gen_rem Drule.eq_thm_prop) (congs,thms)
    8.36  in SS{auto_tac=auto_tac, congs= congs',
    8.37        cong_net= delete_thms(map mk_trans thms,cong_net),
    8.38        mk_simps= normed_rews congs', simps=simps, simp_net=simp_net,
    8.39 @@ -308,7 +308,7 @@
    8.40  fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net,
    8.41                splits,split_consts}, thm) =
    8.42  let fun find((p as (th,ths))::ps',ps) =
    8.43 -	  if eq_thm(thm,th) then (ths,ps@ps') else find(ps',p::ps)
    8.44 +	  if Drule.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps)
    8.45        | find([],simps') = (writeln"\nNo such rewrite or congruence rule:";
    8.46  			   print_thm thm;
    8.47  			   ([],simps'))
     9.1 --- a/src/Pure/Isar/context_rules.ML	Tue May 07 14:24:30 2002 +0200
     9.2 +++ b/src/Pure/Isar/context_rules.ML	Tue May 07 14:26:32 2002 +0200
     9.3 @@ -103,7 +103,7 @@
     9.4  
     9.5  fun del_rule th (rs as Rules {next, rules, netpairs, wrappers}) =
     9.6    let
     9.7 -    fun eq_th (_, (_, th')) = Thm.eq_thm (th, th');
     9.8 +    fun eq_th (_, (_, th')) = Drule.eq_thm_prop (th, th');
     9.9      fun del b netpair = delete_tagged_brl ((b, th), netpair) handle Net.DELETE => netpair;
    9.10    in
    9.11      if not (exists eq_th rules) then rs
    9.12 @@ -135,7 +135,7 @@
    9.13      let
    9.14        val wrappers = (gen_merge_lists' eq_snd ws1 ws2, gen_merge_lists' eq_snd ws1' ws2');
    9.15        val rules = gen_merge_lists' (fn ((_, (k1, th1)), (_, (k2, th2))) =>
    9.16 -          k1 = k2 andalso Thm.eq_thm (th1, th2)) rules1 rules2;
    9.17 +          k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) rules1 rules2;
    9.18        val next = ~ (length rules);
    9.19        val netpairs = foldl (fn (nps, (n, (w, ((i, b), th)))) =>
    9.20            map_nth_elem i (curry insert_tagged_brl ((w, n), (b, th))) nps)
    10.1 --- a/src/Pure/Isar/induct_attrib.ML	Tue May 07 14:24:30 2002 +0200
    10.2 +++ b/src/Pure/Isar/induct_attrib.ML	Tue May 07 14:26:32 2002 +0200
    10.3 @@ -84,7 +84,8 @@
    10.4  type rules = (string * thm) NetRules.T;
    10.5  
    10.6  val init_rules =
    10.7 -  NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso Thm.eq_thm (th1, th2));
    10.8 +  NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
    10.9 +    Drule.eq_thm_prop (th1, th2));
   10.10  
   10.11  fun lookup_rule (rs: rules) name = Library.assoc (NetRules.rules rs, name);
   10.12  
    11.1 --- a/src/Pure/Isar/net_rules.ML	Tue May 07 14:24:30 2002 +0200
    11.2 +++ b/src/Pure/Isar/net_rules.ML	Tue May 07 14:26:32 2002 +0200
    11.3 @@ -63,8 +63,8 @@
    11.4  
    11.5  (* intro/elim rules *)
    11.6  
    11.7 -val intro = init Thm.eq_thm Thm.concl_of;
    11.8 -val elim = init Thm.eq_thm Thm.major_prem_of;
    11.9 +val intro = init Drule.eq_thm_prop Thm.concl_of;
   11.10 +val elim = init Drule.eq_thm_prop Thm.major_prem_of;
   11.11  
   11.12  
   11.13  end;
    12.1 --- a/src/Pure/drule.ML	Tue May 07 14:24:30 2002 +0200
    12.2 +++ b/src/Pure/drule.ML	Tue May 07 14:26:32 2002 +0200
    12.3 @@ -55,8 +55,9 @@
    12.4    val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
    12.5    val read_instantiate  : (string*string)list -> thm -> thm
    12.6    val cterm_instantiate : (cterm*cterm)list -> thm -> thm
    12.7 +  val eq_thm_sg         : thm * thm -> bool
    12.8 +  val eq_thm_prop	: thm * thm -> bool
    12.9    val weak_eq_thm       : thm * thm -> bool
   12.10 -  val eq_thm_sg         : thm * thm -> bool
   12.11    val size_of_thm       : thm -> int
   12.12    val reflexive_thm     : thm
   12.13    val symmetric_thm     : thm
   12.14 @@ -490,20 +491,21 @@
   12.15          [th] => th
   12.16        | _ =>   raise THM("COMP", 1, [tha,thb]);
   12.17  
   12.18 +
   12.19  (** theorem equality **)
   12.20  
   12.21 -(*Do the two theorems have the same signature?*)
   12.22 -fun eq_thm_sg (th1,th2) = Sign.eq_sg(#sign(rep_thm th1), #sign(rep_thm th2));
   12.23 +val eq_thm_sg = Sign.eq_sg o pairself Thm.sign_of_thm;
   12.24 +val eq_thm_prop = op aconv o pairself Thm.prop_of;
   12.25  
   12.26  (*Useful "distance" function for BEST_FIRST*)
   12.27  val size_of_thm = size_of_term o prop_of;
   12.28  
   12.29  (*maintain lists of theorems --- preserving canonical order*)
   12.30 -fun del_rules rs rules = Library.gen_rems Thm.eq_thm (rules, rs);
   12.31 +fun del_rules rs rules = Library.gen_rems eq_thm_prop (rules, rs);
   12.32  fun add_rules rs rules = rs @ del_rules rs rules;
   12.33  val del_rule = del_rules o single;
   12.34  val add_rule = add_rules o single;
   12.35 -fun merge_rules (rules1, rules2) = gen_merge_lists' Thm.eq_thm rules1 rules2;
   12.36 +fun merge_rules (rules1, rules2) = gen_merge_lists' eq_thm_prop rules1 rules2;
   12.37  
   12.38  
   12.39  (** Mark Staples's weaker version of eq_thm: ignores variable renaming and
   12.40 @@ -522,9 +524,7 @@
   12.41        val vars = distinct (term_vars' prop);
   12.42    in forall_intr_list (map (cterm_of sign) vars) th end;
   12.43  
   12.44 -fun weak_eq_thm (tha,thb) =
   12.45 -    eq_thm(forall_intr_vars (freezeT tha), forall_intr_vars (freezeT thb));
   12.46 -
   12.47 +val weak_eq_thm = Thm.eq_thm o pairself (forall_intr_vars o freezeT);
   12.48  
   12.49  
   12.50  (*** Meta-Rewriting Rules ***)
    13.1 --- a/src/Pure/tactic.ML	Tue May 07 14:24:30 2002 +0200
    13.2 +++ b/src/Pure/tactic.ML	Tue May 07 14:26:32 2002 +0200
    13.3 @@ -410,7 +410,7 @@
    13.4  
    13.5  (*delete one kbrl from the pair of nets*)
    13.6  local
    13.7 -  fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = eq_thm (th, th')
    13.8 +  fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Drule.eq_thm_prop (th, th')
    13.9  in
   13.10  fun delete_tagged_brl (brl as (eres, th), (inet, enet)) =
   13.11    if eres then
    14.1 --- a/src/Sequents/prover.ML	Tue May 07 14:24:30 2002 +0200
    14.2 +++ b/src/Sequents/prover.ML	Tue May 07 14:26:32 2002 +0200
    14.3 @@ -32,15 +32,15 @@
    14.4         dups);
    14.5  
    14.6  fun (Pack(safes,unsafes)) add_safes ths   = 
    14.7 -    let val dups = warn_duplicates (gen_inter eq_thm (ths,safes))
    14.8 -	val ths' = gen_rems eq_thm (ths,dups)
    14.9 +    let val dups = warn_duplicates (gen_inter Drule.eq_thm_prop (ths,safes))
   14.10 +	val ths' = gen_rems Drule.eq_thm_prop (ths,dups)
   14.11      in
   14.12          Pack(sort (make_ord less) (ths'@safes), unsafes)
   14.13      end;
   14.14  
   14.15  fun (Pack(safes,unsafes)) add_unsafes ths = 
   14.16 -    let val dups = warn_duplicates (gen_inter eq_thm (ths,unsafes))
   14.17 -	val ths' = gen_rems eq_thm (ths,dups)
   14.18 +    let val dups = warn_duplicates (gen_inter Drule.eq_thm_prop (ths,unsafes))
   14.19 +	val ths' = gen_rems Drule.eq_thm_prop (ths,dups)
   14.20      in
   14.21  	Pack(safes, sort (make_ord less) (ths'@unsafes))
   14.22      end;
    15.1 --- a/src/ZF/Tools/typechk.ML	Tue May 07 14:24:30 2002 +0200
    15.2 +++ b/src/ZF/Tools/typechk.ML	Tue May 07 14:26:32 2002 +0200
    15.3 @@ -46,8 +46,8 @@
    15.4             net: thm Net.net};   (*discrimination net of the same rules*)
    15.5  
    15.6  
    15.7 -val mem_thm = gen_mem eq_thm
    15.8 -and rem_thm = gen_rem eq_thm;
    15.9 +val mem_thm = gen_mem Drule.eq_thm_prop
   15.10 +and rem_thm = gen_rem Drule.eq_thm_prop;
   15.11  
   15.12  fun addTC (cs as TC{rules, net}, th) =
   15.13    if mem_thm (th, rules) then
   15.14 @@ -61,7 +61,7 @@
   15.15  
   15.16  fun delTC (cs as TC{rules, net}, th) =
   15.17    if mem_thm (th, rules) then
   15.18 -      TC{net = Net.delete_term ((concl_of th, th), net, eq_thm),
   15.19 +      TC{net = Net.delete_term ((concl_of th, th), net, Drule.eq_thm_prop),
   15.20           rules  = rem_thm (rules,th)}
   15.21    else (warning ("No such type-checking rule\n" ^ (string_of_thm th));
   15.22          cs);
   15.23 @@ -110,8 +110,8 @@
   15.24  
   15.25  
   15.26  fun merge_tc (TC{rules,net}, TC{rules=rules',net=net'}) =
   15.27 -    TC {rules = gen_union eq_thm (rules,rules'),
   15.28 -        net = Net.merge (net, net', eq_thm)};
   15.29 +    TC {rules = gen_union Drule.eq_thm_prop (rules,rules'),
   15.30 +        net = Net.merge (net, net', Drule.eq_thm_prop)};
   15.31  
   15.32  (*print tcsets*)
   15.33  fun print_tc (TC{rules,...}) =