src/FOL/simpdata.ML
changeset 17002 fb9261990ffe
parent 16019 0e1405402d53
child 17325 d9d50222808e
equal deleted inserted replaced
17001:51ff2bc32774 17002:fb9261990ffe
   265 end);
   265 end);
   266 
   266 
   267 end;
   267 end;
   268 
   268 
   269 val defEX_regroup =
   269 val defEX_regroup =
   270   Simplifier.simproc (Theory.sign_of (the_context ()))
   270   Simplifier.simproc (the_context ())
   271     "defined EX" ["EX x. P(x)"] Quantifier1.rearrange_ex;
   271     "defined EX" ["EX x. P(x)"] Quantifier1.rearrange_ex;
   272 
   272 
   273 val defALL_regroup =
   273 val defALL_regroup =
   274   Simplifier.simproc (Theory.sign_of (the_context ()))
   274   Simplifier.simproc (the_context ())
   275     "defined ALL" ["ALL x. P(x)"] Quantifier1.rearrange_all;
   275     "defined ALL" ["ALL x. P(x)"] Quantifier1.rearrange_all;
   276 
   276 
   277 
   277 
   278 (*** Case splitting ***)
   278 (*** Case splitting ***)
   279 
   279 
   335   setSSolver (mk_solver "FOL safe" safe_solver)
   335   setSSolver (mk_solver "FOL safe" safe_solver)
   336   setSolver (mk_solver "FOL unsafe" unsafe_solver)
   336   setSolver (mk_solver "FOL unsafe" unsafe_solver)
   337   setmksimps (mksimps mksimps_pairs)
   337   setmksimps (mksimps mksimps_pairs)
   338   setmkcong mk_meta_cong;
   338   setmkcong mk_meta_cong;
   339 
   339 
       
   340 fun unfold_tac ss ths =
       
   341   ALLGOALS (full_simp_tac
       
   342     (Simplifier.inherit_bounds ss (Simplifier.clear_ss FOL_basic_ss) addsimps ths));
       
   343 
   340 
   344 
   341 (*intuitionistic simprules only*)
   345 (*intuitionistic simprules only*)
   342 val IFOL_ss = FOL_basic_ss
   346 val IFOL_ss = FOL_basic_ss
   343   addsimps (meta_simps @ IFOL_simps @ int_ex_simps @ int_all_simps)
   347   addsimps (meta_simps @ IFOL_simps @ int_ex_simps @ int_all_simps)
   344   addsimprocs [defALL_regroup, defEX_regroup]    
   348   addsimprocs [defALL_regroup, defEX_regroup]