src/FOL/simpdata.ML

     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
 Simplification data for FOL
 *)
+
+(* Elimination of True from asumptions: *)
+
+val True_implies_equals = prove_goal IFOL.thy
+ "(True ==> PROP P) == PROP P"
+(K [rtac equal_intr_rule 1, atac 2,
+          METAHYPS (fn prems => resolve_tac prems 1) 1,
+          rtac TrueI 1]);
+
 
 (*** Rewrite rules ***)
 
 fun int_prove_fun s = 
  (writeln s;  

 
 fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
 fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
 
 
+val meta_simps =
+   [triv_forall_equality,  (* prunes params *)
+    True_implies_equals];  (* prune asms `True' *)
+
 val IFOL_simps =
    [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
     imp_simps @ iff_simps @ quant_simps;
 
 val notFalseI = int_prove_fun "~False";

 			    setmksimps (mksimps mksimps_pairs);
 
 
 
 (*intuitionistic simprules only*)
-val IFOL_ss = FOL_basic_ss addsimps (IFOL_simps @ int_ex_simps @ int_all_simps)
-			   addcongs [imp_cong];
+val IFOL_ss = 
+    FOL_basic_ss addsimps (meta_simps @ IFOL_simps @ 
+			   int_ex_simps @ int_all_simps)
+                 addcongs [imp_cong];
 
 val cla_simps = 
     [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2,
      not_all, not_ex, cases_simp] @
     map prove_fun