clarified simpset setup;
authorwenzelm
Fri Apr 22 12:46:48 2011 +0200 (2011-04-22)
changeset 42453cd5005020f4e
parent 42452 f7f796ce5d68
child 42454 12a752aeee98
clarified simpset setup;
discontinued unused old-style FOL_css;
src/FOL/FOL.thy
src/FOL/simpdata.ML
src/HOL/HOL.thy
src/HOL/Tools/simpdata.ML
     1.1 --- a/src/FOL/FOL.thy	Fri Apr 22 00:57:59 2011 +0200
     1.2 +++ b/src/FOL/FOL.thy	Fri Apr 22 12:46:48 2011 +0200
     1.3 @@ -122,7 +122,7 @@
     1.4  
     1.5  (*** Tactics for implication and contradiction ***)
     1.6  
     1.7 -(*Classical <-> elimination.  Proof substitutes P=Q in 
     1.8 +(*Classical <-> elimination.  Proof substitutes P=Q in
     1.9      ~P ==> ~Q    and    P ==> Q  *)
    1.10  lemma iffCE:
    1.11    assumes major: "P<->Q"
    1.12 @@ -305,7 +305,19 @@
    1.13  
    1.14  
    1.15  use "simpdata.ML"
    1.16 -setup simpsetup
    1.17 +ML {*
    1.18 +(*intuitionistic simprules only*)
    1.19 +val IFOL_ss =
    1.20 +  FOL_basic_ss
    1.21 +  addsimps (@{thms meta_simps} @ @{thms IFOL_simps} @ @{thms int_ex_simps} @ @{thms int_all_simps})
    1.22 +  addsimprocs [defALL_regroup, defEX_regroup]
    1.23 +  addcongs [@{thm imp_cong}];
    1.24 +
    1.25 +(*classical simprules too*)
    1.26 +val FOL_ss = IFOL_ss addsimps (@{thms cla_simps} @ @{thms cla_ex_simps} @ @{thms cla_all_simps});
    1.27 +*}
    1.28 +
    1.29 +setup {* Simplifier.map_simpset (K FOL_ss) *}
    1.30  setup "Simplifier.method_setup Splitter.split_modifiers"
    1.31  setup Splitter.setup
    1.32  setup clasimp_setup
     2.1 --- a/src/FOL/simpdata.ML	Fri Apr 22 00:57:59 2011 +0200
     2.2 +++ b/src/FOL/simpdata.ML	Fri Apr 22 12:46:48 2011 +0200
     2.3 @@ -136,19 +136,6 @@
     2.4    in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
     2.5  
     2.6  
     2.7 -(*intuitionistic simprules only*)
     2.8 -val IFOL_ss =
     2.9 -  FOL_basic_ss
    2.10 -  addsimps (@{thms meta_simps} @ @{thms IFOL_simps} @ @{thms int_ex_simps} @ @{thms int_all_simps})
    2.11 -  addsimprocs [defALL_regroup, defEX_regroup]    
    2.12 -  addcongs [@{thm imp_cong}];
    2.13 -
    2.14 -(*classical simprules too*)
    2.15 -val FOL_ss = IFOL_ss addsimps (@{thms cla_simps} @ @{thms cla_ex_simps} @ @{thms cla_all_simps});
    2.16 -
    2.17 -val simpsetup = Simplifier.map_simpset (K FOL_ss);
    2.18 -
    2.19 -
    2.20  (*** integration of simplifier with classical reasoner ***)
    2.21  
    2.22  structure Clasimp = ClasimpFun
    2.23 @@ -160,4 +147,3 @@
    2.24  ML_Antiquote.value "clasimpset"
    2.25    (Scan.succeed "Clasimp.clasimpset_of (ML_Context.the_local_context ())");
    2.26  
    2.27 -val FOL_css = (FOL_cs, FOL_ss);
     3.1 --- a/src/HOL/HOL.thy	Fri Apr 22 00:57:59 2011 +0200
     3.2 +++ b/src/HOL/HOL.thy	Fri Apr 22 12:46:48 2011 +0200
     3.3 @@ -1209,10 +1209,12 @@
     3.4  
     3.5  use "Tools/simpdata.ML"
     3.6  ML {* open Simpdata *}
     3.7 +setup {*
     3.8 +  Simplifier.map_simpset (K (HOL_basic_ss addsimprocs [defALL_regroup, defEX_regroup]))
     3.9 +*}
    3.10  
    3.11  setup {*
    3.12    Simplifier.method_setup Splitter.split_modifiers
    3.13 -  #> Simplifier.map_simpset (K Simpdata.simpset_simprocs)
    3.14    #> Splitter.setup
    3.15    #> clasimp_setup
    3.16    #> EqSubst.setup
     4.1 --- a/src/HOL/Tools/simpdata.ML	Fri Apr 22 00:57:59 2011 +0200
     4.2 +++ b/src/HOL/Tools/simpdata.ML	Fri Apr 22 12:46:48 2011 +0200
     4.3 @@ -191,9 +191,6 @@
     4.4    Simplifier.simproc_global @{theory}
     4.5      "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;
     4.6  
     4.7 -
     4.8 -val simpset_simprocs = HOL_basic_ss addsimprocs [defALL_regroup, defEX_regroup]
     4.9 -
    4.10  end;
    4.11  
    4.12  structure Splitter = Simpdata.Splitter;