src/Provers/classical.ML
changeset 15735 953f188e16c6
parent 15707 80b421d8a8be
child 16424 18a07ad8fea8
     1.1 --- a/src/Provers/classical.ML	Thu Apr 14 19:30:57 2005 +0200
     1.2 +++ b/src/Provers/classical.ML	Fri Apr 15 12:00:00 2005 +0200
     1.3 @@ -902,33 +902,37 @@
     1.4    context_cs ctxt (get_local_claset ctxt) (get_context_cs ctxt);
     1.5  
     1.6  (* added for delta_claset: 06/01/05 *)
     1.7 +(* CB: changed "delta clasets" to context data,
     1.8 +       moved counter to here, it is no longer a ref *)
     1.9  
    1.10  structure DeltaClasetArgs =
    1.11  struct
    1.12 -  val name = "delta_claset";
    1.13 -  type T = claset;
    1.14 -  val empty = empty_cs;
    1.15 +  val name = "Provers/delta_claset";
    1.16 +  type T = claset * int;
    1.17 +  fun init _ = (empty_cs, 0)
    1.18 +  fun print ctxt cs = ();
    1.19  end;
    1.20  
    1.21 -structure DeltaClaset = DeltaDataFun(DeltaClasetArgs);
    1.22 -val get_delta_claset = DeltaClaset.get;
    1.23 -val put_delta_claset = DeltaClaset.put;
    1.24 -
    1.25 -val get_new_thm_id = ProofContext.get_delta_count_incr;
    1.26 -
    1.27 +structure DeltaClasetData = ProofDataFun(DeltaClasetArgs);
    1.28 +val get_delta_claset = #1 o DeltaClasetData.get;
    1.29 +fun put_delta_claset cs = DeltaClasetData.map (fn (_, i) => (cs, i));
    1.30 +fun delta_increment ctxt =
    1.31 +  let val ctxt' = DeltaClasetData.map (fn (ss, i) => (ss, i+1)) ctxt
    1.32 +  in (ctxt', #2 (DeltaClasetData.get ctxt'))
    1.33 +  end;
    1.34  
    1.35  local 
    1.36  fun rename_thm' (ctxt,thm) =
    1.37 -  let val new_id = get_new_thm_id ctxt
    1.38 -      val new_name = "anon_" ^ (string_of_int new_id)
    1.39 +  let val (new_ctxt, new_id) = delta_increment ctxt
    1.40 +      val new_name = "anon_cla_" ^ (string_of_int new_id)
    1.41    in
    1.42 -  Thm.name_thm(new_name,thm)
    1.43 +    (new_ctxt, Thm.name_thm(new_name,thm))
    1.44  end;
    1.45  
    1.46  in
    1.47  
    1.48  (* rename thm if call_atp is true *)
    1.49 -fun rename_thm (ctxt,thm) = if (!Proof.call_atp) then rename_thm' (ctxt,thm) else thm;
    1.50 +fun rename_thm (ctxt,thm) = if (!Proof.call_atp) then rename_thm' (ctxt,thm) else (ctxt, thm);
    1.51  
    1.52  end
    1.53       
    1.54 @@ -955,62 +959,62 @@
    1.55  (* when dest/elim/intro rules are added to local_claset, they are also added to delta_claset in ProofContext.context *)
    1.56  fun safe_dest_local (ctxt,th) =
    1.57      let val thm_name = Thm.name_of_thm th
    1.58 -        val th' = if (thm_name = "") then rename_thm (ctxt,th)  else th
    1.59 -        val delta_cs = get_delta_claset ctxt
    1.60 +        val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th)  else (ctxt, th)
    1.61 +        val delta_cs = get_delta_claset ctxt'
    1.62  	val new_dcs = delta_cs addSDs [th']
    1.63 -	val ctxt' = put_delta_claset new_dcs ctxt 
    1.64 +	val ctxt'' = put_delta_claset new_dcs ctxt'
    1.65      in
    1.66 -	change_local_cs (op addSDs) (ctxt',th)
    1.67 +	change_local_cs (op addSDs) (ctxt'',th)
    1.68      end;
    1.69  
    1.70  fun safe_elim_local (ctxt, th)= 
    1.71      let val thm_name = Thm.name_of_thm th
    1.72 -        val th' = if (thm_name = "") then rename_thm (ctxt,th) else th
    1.73 -        val delta_cs = get_delta_claset ctxt
    1.74 +        val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, th)
    1.75 +        val delta_cs = get_delta_claset ctxt'
    1.76  	val new_dcs = delta_cs addSEs [th']
    1.77 -	val ctxt' = put_delta_claset new_dcs ctxt 
    1.78 +	val ctxt'' = put_delta_claset new_dcs ctxt' 
    1.79      in
    1.80 -	change_local_cs (op addSEs) (ctxt',th)
    1.81 +	change_local_cs (op addSEs) (ctxt'',th)
    1.82      end;
    1.83  
    1.84  fun safe_intro_local (ctxt, th) = 
    1.85      let val thm_name = Thm.name_of_thm th
    1.86 -        val th' = if (thm_name = "") then rename_thm (ctxt,th) else th
    1.87 -        val delta_cs = get_delta_claset ctxt
    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 addSIs [th']
    1.91 -	val ctxt' = put_delta_claset new_dcs ctxt 
    1.92 +	val ctxt'' = put_delta_claset new_dcs ctxt'
    1.93      in
    1.94 -	change_local_cs (op addSIs) (ctxt',th)
    1.95 +	change_local_cs (op addSIs) (ctxt'',th)
    1.96      end;
    1.97  
    1.98  fun haz_dest_local (ctxt, th)= 
    1.99      let val thm_name = Thm.name_of_thm th
   1.100 -        val th' = if (thm_name = "") then rename_thm (ctxt,th)else th
   1.101 -        val delta_cs = get_delta_claset ctxt
   1.102 +        val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th)else (ctxt, th)
   1.103 +        val delta_cs = get_delta_claset ctxt'
   1.104  	val new_dcs = delta_cs addDs [th']
   1.105 -	val ctxt' = put_delta_claset new_dcs ctxt 
   1.106 +	val ctxt'' = put_delta_claset new_dcs ctxt'
   1.107      in
   1.108 -	change_local_cs (op addDs) (ctxt',th)
   1.109 +	change_local_cs (op addDs) (ctxt'',th)
   1.110      end;
   1.111  
   1.112  fun haz_elim_local (ctxt,th) =
   1.113      let val thm_name = Thm.name_of_thm th
   1.114 -        val th' = if (thm_name = "") then rename_thm (ctxt,th)  else th
   1.115 -        val delta_cs = get_delta_claset ctxt
   1.116 +        val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th)  else (ctxt, th)
   1.117 +        val delta_cs = get_delta_claset ctxt'
   1.118  	val new_dcs = delta_cs addEs [th']
   1.119 -	val ctxt' = put_delta_claset new_dcs ctxt 
   1.120 +	val ctxt'' = put_delta_claset new_dcs ctxt'
   1.121      in 
   1.122 -	change_local_cs (op addEs) (ctxt',th)
   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 th' = if (thm_name = "") then rename_thm (ctxt,th)  else th
   1.129 -        val delta_cs = get_delta_claset ctxt
   1.130 +        val (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th)  else (ctxt, th)
   1.131 +        val delta_cs = get_delta_claset ctxt'
   1.132  	val new_dcs = delta_cs addIs [th']
   1.133 -	val ctxt' = put_delta_claset new_dcs ctxt 
   1.134 +	val ctxt'' = put_delta_claset new_dcs ctxt'
   1.135      in 
   1.136 -	change_local_cs (op addIs) (ctxt',th)
   1.137 +	change_local_cs (op addIs) (ctxt'',th)
   1.138      end;
   1.139  
   1.140  
   1.141 @@ -1156,7 +1160,8 @@
   1.142  
   1.143  (** theory setup **)
   1.144  
   1.145 -val setup = [GlobalClaset.init, LocalClaset.init, setup_attrs, setup_methods];
   1.146 +val setup = [GlobalClaset.init, LocalClaset.init, DeltaClasetData.init,
   1.147 +  setup_attrs, setup_methods];
   1.148  
   1.149  
   1.150