src/Pure/simplifier.ML
changeset 16806 916387f7afd2
parent 16709 a4679ac06502
child 16989 1877b00fb4d2
     1.1 --- a/src/Pure/simplifier.ML	Wed Jul 13 16:07:26 2005 +0200
     1.2 +++ b/src/Pure/simplifier.ML	Wed Jul 13 16:07:27 2005 +0200
     1.3 @@ -6,12 +6,6 @@
     1.4  meta_simplifier.ML for the actual meta-level rewriting engine).
     1.5  *)
     1.6  
     1.7 -(* added: put_delta_simpset, get_delta_simpset
     1.8 -   changed: simp_add_local
     1.9 -   07/01/05
    1.10 -*)
    1.11 -
    1.12 -
    1.13  signature BASIC_SIMPLIFIER =
    1.14  sig
    1.15    include BASIC_META_SIMPLIFIER
    1.16 @@ -98,9 +92,6 @@
    1.17    val method_setup: (Args.T list -> (Method.modifier * Args.T list)) list
    1.18      -> (theory -> theory) list
    1.19    val easy_setup: thm -> thm list -> (theory -> theory) list
    1.20 -
    1.21 -  val get_delta_simpset: ProofContext.context -> Thm.thm list
    1.22 -  val put_delta_simpset: Thm.thm list -> ProofContext.context -> ProofContext.context
    1.23  end;
    1.24  
    1.25  structure Simplifier: SIMPLIFIER =
    1.26 @@ -134,7 +125,7 @@
    1.27    mk_context_simproc name o map (Thm.cterm_of thy o Logic.varify);
    1.28  
    1.29  fun context_simproc thy name =
    1.30 -  context_simproc_i thy name o map (Sign.simple_read_term thy TypeInfer.logicT);
    1.31 +  context_simproc_i thy name o map (Sign.read_term thy);
    1.32  
    1.33  
    1.34  (* datatype context_ss *)
    1.35 @@ -303,44 +294,6 @@
    1.36    context_ss ctxt (get_local_simpset ctxt) (get_context_ss ctxt);
    1.37  
    1.38  
    1.39 -(* Jia: added DeltaSimpsetArgs and DeltaSimpset for delta_simpset
    1.40 -	also added methods to retrieve them. *)
    1.41 -(* CB: changed "delta simpsets" to context data,
    1.42 -       moved counter to here, it is no longer a ref *)
    1.43 -
    1.44 -structure DeltaSimpsetArgs =
    1.45 -struct
    1.46 -  val name = "Pure/delta_simpset";
    1.47 -  type T = Thm.thm list * int;  (*the type is thm list * int*)
    1.48 -  fun init _ = ([], 0);
    1.49 -  fun print ctxt thms = ();
    1.50 -end;
    1.51 -
    1.52 -structure DeltaSimpsetData = ProofDataFun(DeltaSimpsetArgs);
    1.53 -val _ = Context.add_setup [DeltaSimpsetData.init];
    1.54 -
    1.55 -val get_delta_simpset = #1 o DeltaSimpsetData.get;
    1.56 -fun put_delta_simpset ss = DeltaSimpsetData.map (fn (_, i) => (ss, i));
    1.57 -fun delta_increment ctxt =
    1.58 -  let val ctxt' = DeltaSimpsetData.map (fn (ss, i) => (ss, i+1)) ctxt
    1.59 -  in (ctxt', #2 (DeltaSimpsetData.get ctxt'))
    1.60 -  end;
    1.61 -
    1.62 -(* Jia: added to rename a local thm if necessary *) 
    1.63 -local 
    1.64 -fun rename_thm' (ctxt,thm) =
    1.65 -  let val (new_ctxt, new_id) = delta_increment ctxt
    1.66 -      val new_name = "anon_simp_" ^ (string_of_int new_id)
    1.67 -  in
    1.68 -    (new_ctxt, Thm.name_thm(new_name,thm))
    1.69 -end;
    1.70 -
    1.71 -in
    1.72 -
    1.73 -fun rename_thm (ctxt,thm) = if (!Proof.call_atp) then rename_thm' (ctxt,thm) else (ctxt, thm);
    1.74 -
    1.75 -end
    1.76 -
    1.77  (* attributes *)
    1.78  
    1.79  fun change_global_ss f (thy, th) =
    1.80 @@ -353,23 +306,7 @@
    1.81  
    1.82  val simp_add_global = change_global_ss (op addsimps);
    1.83  val simp_del_global = change_global_ss (op delsimps);
    1.84 -
    1.85 -
    1.86 -
    1.87 -
    1.88 -
    1.89 -(* Jia: note: when simplifier rules are added to local_simpset, they are also added to delta_simpset in ProofContext.context, but not removed if simp_del_local is called *)
    1.90 -fun simp_add_local (ctxt,th) = 
    1.91 -    let val delta_ss = get_delta_simpset ctxt
    1.92 -	val thm_name = Thm.name_of_thm th
    1.93 -        val (ctxt', th') =
    1.94 -          if (thm_name = "") then rename_thm (ctxt,th)  else (ctxt, th)
    1.95 -	val new_dss = th'::delta_ss
    1.96 -	val ctxt'' = put_delta_simpset new_dss ctxt' 
    1.97 -    in
    1.98 -	change_local_ss (op addsimps) (ctxt'',th)
    1.99 -    end;
   1.100 -
   1.101 +val simp_add_local = change_local_ss (op addsimps);
   1.102  val simp_del_local = change_local_ss (op delsimps);
   1.103  
   1.104  val cong_add_global = change_global_ss (op addcongs);
   1.105 @@ -378,6 +315,8 @@
   1.106  val cong_del_local = change_local_ss (op delcongs);
   1.107  
   1.108  
   1.109 +(* tactics *)
   1.110 +
   1.111  val simp_tac = generic_simp_tac false (false, false, false);
   1.112  val asm_simp_tac = generic_simp_tac false (false, true, false);
   1.113  val full_simp_tac = generic_simp_tac false (true, false, false);
   1.114 @@ -385,8 +324,6 @@
   1.115  val asm_full_simp_tac = generic_simp_tac false (true, true, true);
   1.116  val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true);
   1.117  
   1.118 -
   1.119 -
   1.120  (*the abstraction over the proof state delays the dereferencing*)
   1.121  fun          Simp_tac i st =          simp_tac (simpset ()) i st;
   1.122  fun      Asm_simp_tac i st =      asm_simp_tac (simpset ()) i st;
   1.123 @@ -394,6 +331,9 @@
   1.124  fun   Asm_lr_simp_tac i st =   asm_lr_simp_tac (simpset ()) i st;
   1.125  fun Asm_full_simp_tac i st = asm_full_simp_tac (simpset ()) i st;
   1.126  
   1.127 +
   1.128 +(* conversions *)
   1.129 +
   1.130  val          simplify = simp_thm (false, false, false);
   1.131  val      asm_simplify = simp_thm (false, true, false);
   1.132  val     full_simplify = simp_thm (true, false, false);