remove fixrec_simp attribute; fixrec uses default simpset from theory context instead
authorhuffman
Sat May 22 12:36:50 2010 -0700 (2010-05-22)
changeset 37080a2a1c8a658ef
parent 37079 0cd15d8c90a0
child 37081 3e5146b93218
remove fixrec_simp attribute; fixrec uses default simpset from theory context instead
src/HOLCF/Fixrec.thy
src/HOLCF/Tools/fixrec.ML
     1.1 --- a/src/HOLCF/Fixrec.thy	Sat May 22 10:02:07 2010 -0700
     1.2 +++ b/src/HOLCF/Fixrec.thy	Sat May 22 12:36:50 2010 -0700
     1.3 @@ -586,24 +586,4 @@
     1.4  
     1.5  hide_const (open) return fail run cases
     1.6  
     1.7 -lemmas [fixrec_simp] =
     1.8 -  beta_cfun cont2cont
     1.9 -  run_strict run_fail run_return
    1.10 -  mplus_strict mplus_fail mplus_return
    1.11 -  spair_strict_iff
    1.12 -  sinl_defined_iff
    1.13 -  sinr_defined_iff
    1.14 -  up_defined
    1.15 -  ONE_defined
    1.16 -  dist_eq_tr(1,2)
    1.17 -  match_UU_simps
    1.18 -  match_cpair_simps
    1.19 -  match_spair_simps
    1.20 -  match_sinl_simps
    1.21 -  match_sinr_simps
    1.22 -  match_up_simps
    1.23 -  match_ONE_simps
    1.24 -  match_TT_simps
    1.25 -  match_FF_simps
    1.26 -
    1.27  end
     2.1 --- a/src/HOLCF/Tools/fixrec.ML	Sat May 22 10:02:07 2010 -0700
     2.2 +++ b/src/HOLCF/Tools/fixrec.ML	Sat May 22 12:36:50 2010 -0700
     2.3 @@ -13,8 +13,6 @@
     2.4    val add_fixpat: Thm.binding * term list -> theory -> theory
     2.5    val add_fixpat_cmd: Attrib.binding * string list -> theory -> theory
     2.6    val add_matchers: (string * string) list -> theory -> theory
     2.7 -  val fixrec_simp_add: attribute
     2.8 -  val fixrec_simp_del: attribute
     2.9    val fixrec_simp_tac: Proof.context -> int -> tactic
    2.10    val setup: theory -> theory
    2.11  end;
    2.12 @@ -304,18 +302,14 @@
    2.13  (********************** Proving associated theorems **********************)
    2.14  (*************************************************************************)
    2.15  
    2.16 -structure FixrecSimpData = Generic_Data
    2.17 -(
    2.18 -  type T = simpset;
    2.19 -  val empty = HOL_basic_ss addsimps simp_thms;
    2.20 -  val extend = I;
    2.21 -  val merge = merge_ss;
    2.22 -);
    2.23 +(* tactic to perform eta-contraction on subgoal *)
    2.24 +fun eta_tac (ctxt : Proof.context) : int -> tactic =
    2.25 +  EqSubst.eqsubst_tac ctxt [0] @{thms refl};
    2.26  
    2.27  fun fixrec_simp_tac ctxt =
    2.28    let
    2.29      val tab = FixrecUnfoldData.get (Context.Proof ctxt);
    2.30 -    val ss = Simplifier.context ctxt (FixrecSimpData.get (Context.Proof ctxt));
    2.31 +    val ss = Simplifier.simpset_of ctxt;
    2.32      fun concl t =
    2.33        if Logic.is_all t then concl (snd (Logic.dest_all t))
    2.34        else HOLogic.dest_Trueprop (Logic.strip_imp_concl t);
    2.35 @@ -326,26 +320,18 @@
    2.36          val unfold_thm = the (Symtab.lookup tab c);
    2.37          val rule = unfold_thm RS @{thm ssubst_lhs};
    2.38        in
    2.39 -        CHANGED (rtac rule i THEN asm_simp_tac ss i)
    2.40 +        CHANGED (rtac rule i THEN eta_tac ctxt i THEN asm_simp_tac ss i)
    2.41        end
    2.42    in
    2.43      SUBGOAL (fn ti => the_default no_tac (try tac ti))
    2.44    end;
    2.45  
    2.46 -val fixrec_simp_add : attribute =
    2.47 -  Thm.declaration_attribute
    2.48 -    (fn th => FixrecSimpData.map (fn ss => ss addsimps [th]));
    2.49 -
    2.50 -val fixrec_simp_del : attribute =
    2.51 -  Thm.declaration_attribute
    2.52 -    (fn th => FixrecSimpData.map (fn ss => ss delsimps [th]));
    2.53 -
    2.54  (* proves a block of pattern matching equations as theorems, using unfold *)
    2.55  fun make_simps ctxt (unfold_thm, eqns : (Attrib.binding * term) list) =
    2.56    let
    2.57 -    val ss = Simplifier.context ctxt (FixrecSimpData.get (Context.Proof ctxt));
    2.58 +    val ss = Simplifier.simpset_of ctxt;
    2.59      val rule = unfold_thm RS @{thm ssubst_lhs};
    2.60 -    val tac = rtac rule 1 THEN asm_simp_tac ss 1;
    2.61 +    val tac = rtac rule 1 THEN eta_tac ctxt 1 THEN asm_simp_tac ss 1;
    2.62      fun prove_term t = Goal.prove ctxt [] [] t (K tac);
    2.63      fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t);
    2.64    in
    2.65 @@ -459,11 +445,8 @@
    2.66      (Parse_Spec.specs >> (Toplevel.theory o add_fixpat_cmd));
    2.67  
    2.68  val setup =
    2.69 -  Attrib.setup @{binding fixrec_simp}
    2.70 -                     (Attrib.add_del fixrec_simp_add fixrec_simp_del)
    2.71 -                     "declaration of fixrec simp rule"
    2.72 -  #> Method.setup @{binding fixrec_simp}
    2.73 -                     (Scan.succeed (SIMPLE_METHOD' o fixrec_simp_tac))
    2.74 -                     "pattern prover for fixrec constants";
    2.75 +  Method.setup @{binding fixrec_simp}
    2.76 +    (Scan.succeed (SIMPLE_METHOD' o fixrec_simp_tac))
    2.77 +    "pattern prover for fixrec constants";
    2.78  
    2.79  end;