removed obsolete delta stuff;
authorwenzelm
Wed Jul 13 16:07:27 2005 +0200 (2005-07-13)
changeset 16806916387f7afd2
parent 16805 fadf80952202
child 16807 730cace0ae48
removed obsolete delta stuff;
src/Provers/classical.ML
src/Pure/simplifier.ML
     1.1 --- a/src/Provers/classical.ML	Wed Jul 13 16:07:26 2005 +0200
     1.2 +++ b/src/Provers/classical.ML	Wed Jul 13 16:07:27 2005 +0200
     1.3 @@ -14,13 +14,6 @@
     1.4  the conclusion.
     1.5  *)
     1.6  
     1.7 -
     1.8 -(*added: get_delta_claset, put_delta_claset.
     1.9 -        changed: safe_{dest,elim,intro}_local and haz_{dest,elim,intro}_local
    1.10 -   06/01/05
    1.11 -*)
    1.12 -
    1.13 -
    1.14  (*higher precedence than := facilitates use of references*)
    1.15  infix 4 addSIs addSEs addSDs addIs addEs addDs delrules
    1.16    addSWrapper delSWrapper addWrapper delWrapper
    1.17 @@ -171,10 +164,6 @@
    1.18    val cla_method: (claset -> tactic) -> Method.src -> Proof.context -> Proof.method
    1.19    val cla_method': (claset -> int -> tactic) -> Method.src -> Proof.context -> Proof.method
    1.20    val setup: (theory -> theory) list
    1.21 -
    1.22 -  val get_delta_claset: ProofContext.context -> claset
    1.23 -  val put_delta_claset: claset -> ProofContext.context -> ProofContext.context
    1.24 -
    1.25  end;
    1.26  
    1.27  
    1.28 @@ -899,41 +888,6 @@
    1.29  fun local_claset_of ctxt =
    1.30    context_cs ctxt (get_local_claset ctxt) (get_context_cs ctxt);
    1.31  
    1.32 -(* added for delta_claset: 06/01/05 *)
    1.33 -(* CB: changed "delta clasets" to context data,
    1.34 -       moved counter to here, it is no longer a ref *)
    1.35 -
    1.36 -structure DeltaClasetArgs =
    1.37 -struct
    1.38 -  val name = "Provers/delta_claset";
    1.39 -  type T = claset * int;
    1.40 -  fun init _ = (empty_cs, 0)
    1.41 -  fun print ctxt cs = ();
    1.42 -end;
    1.43 -
    1.44 -structure DeltaClasetData = ProofDataFun(DeltaClasetArgs);
    1.45 -val get_delta_claset = #1 o DeltaClasetData.get;
    1.46 -fun put_delta_claset cs = DeltaClasetData.map (fn (_, i) => (cs, i));
    1.47 -fun delta_increment ctxt =
    1.48 -  let val ctxt' = DeltaClasetData.map (fn (ss, i) => (ss, i+1)) ctxt
    1.49 -  in (ctxt', #2 (DeltaClasetData.get ctxt'))
    1.50 -  end;
    1.51 -
    1.52 -local
    1.53 -fun rename_thm' (ctxt,thm) =
    1.54 -  let val (new_ctxt, new_id) = delta_increment ctxt
    1.55 -      val new_name = "anon_cla_" ^ (string_of_int new_id)
    1.56 -  in
    1.57 -    (new_ctxt, Thm.name_thm(new_name,thm))
    1.58 -end;
    1.59 -
    1.60 -in
    1.61 -
    1.62 -(* rename thm if call_atp is true *)
    1.63 -fun rename_thm (ctxt,thm) = if (!Proof.call_atp) then rename_thm' (ctxt,thm) else (ctxt, thm);
    1.64 -
    1.65 -end
    1.66 -
    1.67  
    1.68  (* attributes *)
    1.69  
    1.70 @@ -953,70 +907,12 @@
    1.71  val haz_intro_global = change_global_cs (op addIs);
    1.72  val rule_del_global = change_global_cs (op delrules) o ContextRules.rule_del_global;
    1.73  
    1.74 -
    1.75 -(* when dest/elim/intro rules are added to local_claset, they are also added to delta_claset in ProofContext.context *)
    1.76 -fun safe_dest_local (ctxt,th) =
    1.77 -    let val thm_name = Thm.name_of_thm th
    1.78 -        val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th)  else (ctxt, th)
    1.79 -        val delta_cs = get_delta_claset ctxt'
    1.80 -        val new_dcs = delta_cs addSDs [th']
    1.81 -        val ctxt'' = put_delta_claset new_dcs ctxt'
    1.82 -    in
    1.83 -        change_local_cs (op addSDs) (ctxt'',th)
    1.84 -    end;
    1.85 -
    1.86 -fun safe_elim_local (ctxt, th)=
    1.87 -    let val thm_name = Thm.name_of_thm th
    1.88 -        val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th)
    1.89 -        val delta_cs = get_delta_claset ctxt'
    1.90 -        val new_dcs = delta_cs addSEs [th']
    1.91 -        val ctxt'' = put_delta_claset new_dcs ctxt'
    1.92 -    in
    1.93 -        change_local_cs (op addSEs) (ctxt'',th)
    1.94 -    end;
    1.95 -
    1.96 -fun safe_intro_local (ctxt, th) =
    1.97 -    let val thm_name = Thm.name_of_thm th
    1.98 -        val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th)
    1.99 -        val delta_cs = get_delta_claset ctxt'
   1.100 -        val new_dcs = delta_cs addSIs [th']
   1.101 -        val ctxt'' = put_delta_claset new_dcs ctxt'
   1.102 -    in
   1.103 -        change_local_cs (op addSIs) (ctxt'',th)
   1.104 -    end;
   1.105 -
   1.106 -fun haz_dest_local (ctxt, th)=
   1.107 -    let val thm_name = Thm.name_of_thm th
   1.108 -        val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th)else (ctxt, th)
   1.109 -        val delta_cs = get_delta_claset ctxt'
   1.110 -        val new_dcs = delta_cs addDs [th']
   1.111 -        val ctxt'' = put_delta_claset new_dcs ctxt'
   1.112 -    in
   1.113 -        change_local_cs (op addDs) (ctxt'',th)
   1.114 -    end;
   1.115 -
   1.116 -fun haz_elim_local (ctxt,th) =
   1.117 -    let val thm_name = Thm.name_of_thm th
   1.118 -        val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th)  else (ctxt, th)
   1.119 -        val delta_cs = get_delta_claset ctxt'
   1.120 -        val new_dcs = delta_cs addEs [th']
   1.121 -        val ctxt'' = put_delta_claset new_dcs ctxt'
   1.122 -    in
   1.123 -        change_local_cs (op addEs) (ctxt'',th)
   1.124 -    end;
   1.125 -
   1.126 -fun haz_intro_local (ctxt,th) =
   1.127 -    let val thm_name = Thm.name_of_thm th
   1.128 -        val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th)  else (ctxt, th)
   1.129 -        val delta_cs = get_delta_claset ctxt'
   1.130 -        val new_dcs = delta_cs addIs [th']
   1.131 -        val ctxt'' = put_delta_claset new_dcs ctxt'
   1.132 -    in
   1.133 -        change_local_cs (op addIs) (ctxt'',th)
   1.134 -    end;
   1.135 -
   1.136 -
   1.137 -(* when a rule is removed from local_claset, it is not removed from delta_claset in ProofContext.context.  But this is unlikely to happen. *)
   1.138 +val safe_dest_local = change_local_cs (op addSDs);
   1.139 +val safe_elim_local = change_local_cs (op addSEs);
   1.140 +val safe_intro_local = change_local_cs (op addSIs);
   1.141 +val haz_dest_local = change_local_cs (op addDs);
   1.142 +val haz_elim_local = change_local_cs (op addEs);
   1.143 +val haz_intro_local = change_local_cs (op addIs);
   1.144  val rule_del_local = change_local_cs (op delrules) o ContextRules.rule_del_local;
   1.145  
   1.146  
   1.147 @@ -1158,8 +1054,7 @@
   1.148  
   1.149  (** theory setup **)
   1.150  
   1.151 -val setup = [GlobalClaset.init, LocalClaset.init, DeltaClasetData.init,
   1.152 -  setup_attrs, setup_methods];
   1.153 +val setup = [GlobalClaset.init, LocalClaset.init, setup_attrs, setup_methods];
   1.154  
   1.155  
   1.156  
   1.157 @@ -1175,4 +1070,3 @@
   1.158  
   1.159  
   1.160  end;
   1.161 -
     2.1 --- a/src/Pure/simplifier.ML	Wed Jul 13 16:07:26 2005 +0200
     2.2 +++ b/src/Pure/simplifier.ML	Wed Jul 13 16:07:27 2005 +0200
     2.3 @@ -6,12 +6,6 @@
     2.4  meta_simplifier.ML for the actual meta-level rewriting engine).
     2.5  *)
     2.6  
     2.7 -(* added: put_delta_simpset, get_delta_simpset
     2.8 -   changed: simp_add_local
     2.9 -   07/01/05
    2.10 -*)
    2.11 -
    2.12 -
    2.13  signature BASIC_SIMPLIFIER =
    2.14  sig
    2.15    include BASIC_META_SIMPLIFIER
    2.16 @@ -98,9 +92,6 @@
    2.17    val method_setup: (Args.T list -> (Method.modifier * Args.T list)) list
    2.18      -> (theory -> theory) list
    2.19    val easy_setup: thm -> thm list -> (theory -> theory) list
    2.20 -
    2.21 -  val get_delta_simpset: ProofContext.context -> Thm.thm list
    2.22 -  val put_delta_simpset: Thm.thm list -> ProofContext.context -> ProofContext.context
    2.23  end;
    2.24  
    2.25  structure Simplifier: SIMPLIFIER =
    2.26 @@ -134,7 +125,7 @@
    2.27    mk_context_simproc name o map (Thm.cterm_of thy o Logic.varify);
    2.28  
    2.29  fun context_simproc thy name =
    2.30 -  context_simproc_i thy name o map (Sign.simple_read_term thy TypeInfer.logicT);
    2.31 +  context_simproc_i thy name o map (Sign.read_term thy);
    2.32  
    2.33  
    2.34  (* datatype context_ss *)
    2.35 @@ -303,44 +294,6 @@
    2.36    context_ss ctxt (get_local_simpset ctxt) (get_context_ss ctxt);
    2.37  
    2.38  
    2.39 -(* Jia: added DeltaSimpsetArgs and DeltaSimpset for delta_simpset
    2.40 -	also added methods to retrieve them. *)
    2.41 -(* CB: changed "delta simpsets" to context data,
    2.42 -       moved counter to here, it is no longer a ref *)
    2.43 -
    2.44 -structure DeltaSimpsetArgs =
    2.45 -struct
    2.46 -  val name = "Pure/delta_simpset";
    2.47 -  type T = Thm.thm list * int;  (*the type is thm list * int*)
    2.48 -  fun init _ = ([], 0);
    2.49 -  fun print ctxt thms = ();
    2.50 -end;
    2.51 -
    2.52 -structure DeltaSimpsetData = ProofDataFun(DeltaSimpsetArgs);
    2.53 -val _ = Context.add_setup [DeltaSimpsetData.init];
    2.54 -
    2.55 -val get_delta_simpset = #1 o DeltaSimpsetData.get;
    2.56 -fun put_delta_simpset ss = DeltaSimpsetData.map (fn (_, i) => (ss, i));
    2.57 -fun delta_increment ctxt =
    2.58 -  let val ctxt' = DeltaSimpsetData.map (fn (ss, i) => (ss, i+1)) ctxt
    2.59 -  in (ctxt', #2 (DeltaSimpsetData.get ctxt'))
    2.60 -  end;
    2.61 -
    2.62 -(* Jia: added to rename a local thm if necessary *) 
    2.63 -local 
    2.64 -fun rename_thm' (ctxt,thm) =
    2.65 -  let val (new_ctxt, new_id) = delta_increment ctxt
    2.66 -      val new_name = "anon_simp_" ^ (string_of_int new_id)
    2.67 -  in
    2.68 -    (new_ctxt, Thm.name_thm(new_name,thm))
    2.69 -end;
    2.70 -
    2.71 -in
    2.72 -
    2.73 -fun rename_thm (ctxt,thm) = if (!Proof.call_atp) then rename_thm' (ctxt,thm) else (ctxt, thm);
    2.74 -
    2.75 -end
    2.76 -
    2.77  (* attributes *)
    2.78  
    2.79  fun change_global_ss f (thy, th) =
    2.80 @@ -353,23 +306,7 @@
    2.81  
    2.82  val simp_add_global = change_global_ss (op addsimps);
    2.83  val simp_del_global = change_global_ss (op delsimps);
    2.84 -
    2.85 -
    2.86 -
    2.87 -
    2.88 -
    2.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 *)
    2.90 -fun simp_add_local (ctxt,th) = 
    2.91 -    let val delta_ss = get_delta_simpset ctxt
    2.92 -	val thm_name = Thm.name_of_thm th
    2.93 -        val (ctxt', th') =
    2.94 -          if (thm_name = "") then rename_thm (ctxt,th)  else (ctxt, th)
    2.95 -	val new_dss = th'::delta_ss
    2.96 -	val ctxt'' = put_delta_simpset new_dss ctxt' 
    2.97 -    in
    2.98 -	change_local_ss (op addsimps) (ctxt'',th)
    2.99 -    end;
   2.100 -
   2.101 +val simp_add_local = change_local_ss (op addsimps);
   2.102  val simp_del_local = change_local_ss (op delsimps);
   2.103  
   2.104  val cong_add_global = change_global_ss (op addcongs);
   2.105 @@ -378,6 +315,8 @@
   2.106  val cong_del_local = change_local_ss (op delcongs);
   2.107  
   2.108  
   2.109 +(* tactics *)
   2.110 +
   2.111  val simp_tac = generic_simp_tac false (false, false, false);
   2.112  val asm_simp_tac = generic_simp_tac false (false, true, false);
   2.113  val full_simp_tac = generic_simp_tac false (true, false, false);
   2.114 @@ -385,8 +324,6 @@
   2.115  val asm_full_simp_tac = generic_simp_tac false (true, true, true);
   2.116  val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true);
   2.117  
   2.118 -
   2.119 -
   2.120  (*the abstraction over the proof state delays the dereferencing*)
   2.121  fun          Simp_tac i st =          simp_tac (simpset ()) i st;
   2.122  fun      Asm_simp_tac i st =      asm_simp_tac (simpset ()) i st;
   2.123 @@ -394,6 +331,9 @@
   2.124  fun   Asm_lr_simp_tac i st =   asm_lr_simp_tac (simpset ()) i st;
   2.125  fun Asm_full_simp_tac i st = asm_full_simp_tac (simpset ()) i st;
   2.126  
   2.127 +
   2.128 +(* conversions *)
   2.129 +
   2.130  val          simplify = simp_thm (false, false, false);
   2.131  val      asm_simplify = simp_thm (false, true, false);
   2.132  val     full_simplify = simp_thm (true, false, false);