congruence rules finally use == instead of = and <->
authorpaulson
Wed Jan 13 12:08:51 1999 +0100 (1999-01-13 ago)
changeset 611445958e54d72e
parent 6113 b321f5aaa5f4
child 6115 c70bce7deb0f
congruence rules finally use == instead of = and <->
src/FOL/simpdata.ML
     1.1 --- a/src/FOL/simpdata.ML	Wed Jan 13 12:08:18 1999 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Wed Jan 13 12:08:51 1999 +0100
     1.3 @@ -90,8 +90,15 @@
     1.4    | _ $ (Const("Not",_)$_)      => th RS iff_reflection_F
     1.5    | _                           => th RS iff_reflection_T;
     1.6  
     1.7 -fun mk_meta_cong rl = standard (mk_meta_eq rl); 
     1.8 -(*FIXME: how about the premises?*)
     1.9 +(*Replace premises x=y, X<->Y by X==Y*)
    1.10 +val mk_meta_prems = 
    1.11 +    rule_by_tactic 
    1.12 +      (REPEAT_FIRST (resolve_tac [meta_eq_to_obj_eq, def_imp_iff]));
    1.13 +
    1.14 +fun mk_meta_cong rl =
    1.15 +  standard(mk_meta_eq (mk_meta_prems rl))
    1.16 +  handle THM _ =>
    1.17 +  error("Premises and conclusion of congruence rules must use =-equality or <->");
    1.18  
    1.19  val mksimps_pairs =
    1.20    [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
    1.21 @@ -209,11 +216,6 @@
    1.22      "(ALL x. P(x) & Q(x)) <-> ((ALL x. P(x)) & (ALL x. Q(x)))";
    1.23  
    1.24  
    1.25 -(*Used in ZF, perhaps elsewhere?*)
    1.26 -val meta_eq_to_obj_eq = prove_goal IFOL.thy "x==y ==> x=y"
    1.27 -  (fn [prem] => [rewtac prem, rtac refl 1]);
    1.28 -
    1.29 -
    1.30  (** make simplification procedures for quantifier elimination **)
    1.31  structure Quantifier1 = Quantifier1Fun(
    1.32  struct
    1.33 @@ -307,11 +309,11 @@
    1.34      True_implies_equals];  (* prune asms `True' *)
    1.35  
    1.36  val IFOL_simps =
    1.37 -   [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
    1.38 +    [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
    1.39      imp_simps @ iff_simps @ quant_simps;
    1.40  
    1.41  val notFalseI = int_prove_fun "~False";
    1.42 -val triv_rls = [TrueI,refl,iff_refl,notFalseI];
    1.43 +val triv_rls = [TrueI,refl,reflexive_thm,iff_refl,notFalseI];
    1.44  
    1.45  fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls@prems),
    1.46  				 atac, etac FalseE];