# HG changeset patch # User boehmes # Date 1265906935 -3600 # Node ID 133be405a6f1bde83596de47f3ac21d1075b9232 # Parent a0334d7fb0abbdb18c30924cba78c349a1fab75f unfold quantifiers (Ball, Bex, Ex1) diff -r a0334d7fb0ab -r 133be405a6f1 src/HOL/SMT/Tools/smt_normalize.ML --- a/src/HOL/SMT/Tools/smt_normalize.ML Thu Feb 11 09:14:34 2010 +0100 +++ b/src/HOL/SMT/Tools/smt_normalize.ML Thu Feb 11 17:48:55 2010 +0100 @@ -125,8 +125,15 @@ Conv.rewr_conv @{thm atomize_all} | _ => Conv.all_conv) ct +fun unfold_quants_conv ctxt = + let + val rules = [@{thm Ex1_def}, @{thm Ball_def}, @{thm Bex_def}] + val unfold_conv = Conv.try_conv (More_Conv.rewrs_conv rules) + in More_Conv.top_conv (K unfold_conv) ctxt end + fun normalize_rule ctxt = Conv.fconv_rule ( + unfold_quants_conv ctxt then_conv Thm.beta_conversion true then_conv Thm.eta_conversion then_conv norm_binder_conv ctxt) #>