src/FOL/simpdata.ML
changeset 5496 42d13691be86
parent 5307 6a699d5cdef4
child 5555 4b9386224084
     1.1 --- a/src/FOL/simpdata.ML	Fri Sep 18 14:33:20 1998 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Fri Sep 18 14:34:06 1998 +0200
     1.3 @@ -6,6 +6,15 @@
     1.4  Simplification data for FOL
     1.5  *)
     1.6  
     1.7 +(* Elimination of True from asumptions: *)
     1.8 +
     1.9 +val True_implies_equals = prove_goal IFOL.thy
    1.10 + "(True ==> PROP P) == PROP P"
    1.11 +(K [rtac equal_intr_rule 1, atac 2,
    1.12 +          METAHYPS (fn prems => resolve_tac prems 1) 1,
    1.13 +          rtac TrueI 1]);
    1.14 +
    1.15 +
    1.16  (*** Rewrite rules ***)
    1.17  
    1.18  fun int_prove_fun s = 
    1.19 @@ -282,6 +291,10 @@
    1.20  fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
    1.21  
    1.22  
    1.23 +val meta_simps =
    1.24 +   [triv_forall_equality,  (* prunes params *)
    1.25 +    True_implies_equals];  (* prune asms `True' *)
    1.26 +
    1.27  val IFOL_simps =
    1.28     [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
    1.29      imp_simps @ iff_simps @ quant_simps;
    1.30 @@ -305,8 +318,10 @@
    1.31  
    1.32  
    1.33  (*intuitionistic simprules only*)
    1.34 -val IFOL_ss = FOL_basic_ss addsimps (IFOL_simps @ int_ex_simps @ int_all_simps)
    1.35 -			   addcongs [imp_cong];
    1.36 +val IFOL_ss = 
    1.37 +    FOL_basic_ss addsimps (meta_simps @ IFOL_simps @ 
    1.38 +			   int_ex_simps @ int_all_simps)
    1.39 +                 addcongs [imp_cong];
    1.40  
    1.41  val cla_simps = 
    1.42      [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2,