src/HOL/simpdata.ML
changeset 11162 9e2ec5f02217
parent 11034 568eb11f8d52
child 11200 f43fa07536c0
equal deleted inserted replaced
11161:166f7d87b37f 11162:9e2ec5f02217
   328   might cause exponential blow-up.  But imp_disjL has been in for a while
   328   might cause exponential blow-up.  But imp_disjL has been in for a while
   329   and cannot be removed without affecting existing proofs.  Moreover,
   329   and cannot be removed without affecting existing proofs.  Moreover,
   330   rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the
   330   rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the
   331   grounds that it allows simplification of R in the two cases.*)
   331   grounds that it allows simplification of R in the two cases.*)
   332 
   332 
   333 fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
       
   334 
       
   335 val mksimps_pairs =
   333 val mksimps_pairs =
   336   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
   334   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
   337    ("All", [spec]), ("True", []), ("False", []),
   335    ("All", [spec]), ("True", []), ("False", []),
   338    ("If", [if_bool_eq_conj RS iffD1])];
   336    ("If", [if_bool_eq_conj RS iffD1])];
   339 
   337 
   352                    | None => [th])
   350                    | None => [th])
   353               | _ => [th])
   351               | _ => [th])
   354          | _ => [th])
   352          | _ => [th])
   355   in atoms end;
   353   in atoms end;
   356 
   354 
   357 fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all);
   355 fun mksimps pairs = (map mk_eq o mk_atomize pairs o forall_elim_vars_safe);
   358 
   356 
   359 fun unsafe_solver_tac prems =
   357 fun unsafe_solver_tac prems =
   360   FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE];
   358   FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE];
   361 val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
   359 val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
   362 
   360