src/HOL/simpdata.ML
changeset 21674 8a6bf9d7c751
parent 21551 d276e7d25017
child 22128 cdd92316dd31
     1.1 --- a/src/HOL/simpdata.ML	Wed Dec 06 01:12:51 2006 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Wed Dec 06 01:12:56 2006 +0100
     1.3 @@ -163,19 +163,29 @@
     1.4  
     1.5  structure Splitter = SplitterFun(SplitterData);
     1.6  
     1.7 +val split_tac        = Splitter.split_tac;
     1.8 +val split_inside_tac = Splitter.split_inside_tac;
     1.9 +
    1.10 +val op addsplits     = Splitter.addsplits;
    1.11 +val op delsplits     = Splitter.delsplits;
    1.12 +val Addsplits        = Splitter.Addsplits;
    1.13 +val Delsplits        = Splitter.Delsplits;
    1.14 +
    1.15 +
    1.16  (* integration of simplifier with classical reasoner *)
    1.17  
    1.18  structure Clasimp = ClasimpFun
    1.19   (structure Simplifier = Simplifier and Splitter = Splitter
    1.20    and Classical  = Classical and Blast = Blast
    1.21 -  val iffD1 = thm "iffD1" val iffD2 = thm "iffD2" val notE = thm "notE");
    1.22 +  val iffD1 = thm "iffD1" val iffD2 = thm "iffD2" val notE = thm "notE")
    1.23 +open Clasimp;
    1.24  
    1.25  val mksimps_pairs =
    1.26    [("op -->", [thm "mp"]), ("op &", [thm "conjunct1", thm "conjunct2"]),
    1.27     ("All", [thm "spec"]), ("True", []), ("False", []),
    1.28     ("HOL.If", [thm "if_bool_eq_conj" RS thm "iffD1"])];
    1.29  
    1.30 -val simpset_basic =
    1.31 +val HOL_basic_ss =
    1.32    Simplifier.theory_context (the_context ()) empty_ss
    1.33      setsubgoaler asm_simp_tac
    1.34      setSSolver safe_solver
    1.35 @@ -184,10 +194,10 @@
    1.36      setmkeqTrue mk_eq_True
    1.37      setmkcong mk_meta_cong;
    1.38  
    1.39 -fun simplify rews = Simplifier.full_simplify (simpset_basic addsimps rews);
    1.40 +fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews);
    1.41  
    1.42  fun unfold_tac ths =
    1.43 -  let val ss0 = Simplifier.clear_ss simpset_basic addsimps ths
    1.44 +  let val ss0 = Simplifier.clear_ss HOL_basic_ss addsimps ths
    1.45    in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
    1.46  
    1.47  
    1.48 @@ -338,7 +348,7 @@
    1.49      "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;
    1.50  
    1.51  
    1.52 -val simpset_simprocs = simpset_basic
    1.53 +val simpset_simprocs = HOL_basic_ss
    1.54    addsimprocs [defALL_regroup, defEX_regroup, neq_simproc, let_simproc]
    1.55  
    1.56  end;