src/Provers/classical.ML
changeset 16806 916387f7afd2
parent 16424 18a07ad8fea8
child 17057 0934ac31985f
     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 -