Jia Meng: delta simpsets and clasets
authorpaulson
Fri Jan 21 18:00:18 2005 +0100 (2005-01-21 ago)
changeset 15452e2a721567f67
parent 15451 c6c8786b9921
child 15453 6318e634e6cc
Jia Meng: delta simpsets and clasets
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_clause.ML
src/Provers/classical.ML
src/Provers/simplifier.ML
src/Pure/Isar/ROOT.ML
src/Pure/Isar/delta_data.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Jan 21 13:55:07 2005 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Jan 21 18:00:18 2005 +0100
     1.3 @@ -4,16 +4,20 @@
     1.4  
     1.5  ATPs with TPTP format input.
     1.6  *)
     1.7 +
     1.8 +(*Jia: changed: isar_atp now processes entire proof context.  fetch thms from delta simpset/claset*)
     1.9 +
    1.10  signature RES_ATP = 
    1.11  sig
    1.12  
    1.13  val trace_res : bool ref
    1.14  val axiom_file : Path.T
    1.15  val hyps_file : Path.T
    1.16 -val isar_atp : Thm.thm list * Thm.thm -> unit
    1.17 +val isar_atp : ProofContext.context * Thm.thm -> unit
    1.18  val prob_file : Path.T
    1.19  val atp_ax_tac : Thm.thm list -> int -> Tactical.tactic
    1.20  val atp_tac : int -> Tactical.tactic
    1.21 +val debug: bool ref
    1.22  
    1.23  end;
    1.24  
    1.25 @@ -21,6 +25,10 @@
    1.26  
    1.27  struct
    1.28  
    1.29 +(* used for debug *)
    1.30 +val debug = ref false;
    1.31 +
    1.32 +fun debug_tac tac = (warning "testing";tac);
    1.33  (* default value is false *)
    1.34  
    1.35  val trace_res = ref false;
    1.36 @@ -46,10 +54,10 @@
    1.37  
    1.38  
    1.39  
    1.40 -fun tptp_inputs thms = 
    1.41 +fun tptp_inputs thms n = 
    1.42      let val clss = map (ResClause.make_conjecture_clause_thm) thms
    1.43  	val tptp_clss = ResLib.flat_noDup(map ResClause.tptp_clause clss) 
    1.44 -        val probfile = File.sysify_path prob_file
    1.45 +        val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
    1.46  	val out = TextIO.openOut(probfile)
    1.47      in
    1.48  	(ResLib.writeln_strs out tptp_clss; TextIO.closeOut out; (if !trace_res then (warning probfile) else ()))
    1.49 @@ -58,12 +66,14 @@
    1.50  
    1.51  (**** for Isabelle/ML interface  ****)
    1.52  
    1.53 -fun call_atp_tac thms = (tptp_inputs thms; dummy_tac);
    1.54 +fun call_atp_tac thms n = (tptp_inputs thms n; dummy_tac);
    1.55 +
    1.56  
    1.57  
    1.58 -val atp_tac = SELECT_GOAL
    1.59 -  (EVERY1 [rtac ccontr, atomize_tac, skolemize_tac, 
    1.60 -  METAHYPS(fn negs => (call_atp_tac(make_clauses negs)))]);
    1.61 +
    1.62 +fun atp_tac n = SELECT_GOAL
    1.63 +  (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
    1.64 +  METAHYPS(fn negs => (call_atp_tac (make_clauses negs) n))]) n;
    1.65  
    1.66  
    1.67  fun atp_ax_tac axioms n = 
    1.68 @@ -97,13 +107,13 @@
    1.69  fun repeat_someI_ex thm = repeat_RS thm someI_ex;
    1.70  
    1.71  
    1.72 -
    1.73 +(* convert clauses from "assume" to conjecture. write to file "hyps" *)
    1.74  fun isar_atp_h thms =
    1.75      let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms
    1.76  	val prems' = map repeat_someI_ex prems
    1.77  	val prems'' = make_clauses prems'
    1.78  	val prems''' = ResAxioms.rm_Eps [] prems''
    1.79 -	val clss = map ResClause.make_hypothesis_clause prems'''
    1.80 +	val clss = map ResClause.make_conjecture_clause prems'''
    1.81  	val tptp_clss = ResLib.flat_noDup (map ResClause.tptp_clause clss)
    1.82          val hypsfile = File.sysify_path hyps_file
    1.83  	val out = TextIO.openOut(hypsfile)
    1.84 @@ -116,21 +126,109 @@
    1.85  
    1.86  val isar_atp_g = atp_tac;
    1.87  
    1.88 -fun isar_atp_aux thms thm = 
    1.89 -    (isar_atp_h thms; isar_atp_g 1 thm;());
    1.90 +
    1.91 +fun isar_atp_goal' thm k n = 
    1.92 +    if (k > n) then () else (isar_atp_g k thm; isar_atp_goal' thm (k+1) n);
    1.93 +
    1.94 +
    1.95 +fun isar_atp_goal thm n_subgoals = (if (!debug) then warning (string_of_thm thm) else (isar_atp_goal' thm 1 n_subgoals));
    1.96 +
    1.97 +
    1.98 +
    1.99 +fun isar_atp_aux thms thm n_subgoals = 
   1.100 +    (isar_atp_h thms; isar_atp_goal thm n_subgoals); (* convert both to conjecture clauses, but write to different files *)
   1.101 +
   1.102 +
   1.103 +fun isar_atp' (thms, thm) =
   1.104 +    let val prems = prems_of thm
   1.105 +    in
   1.106 +	case prems of [] => (if (!debug) then warning "entering forward, no goal" else ())
   1.107 +		    | _ => (isar_atp_aux thms thm (length prems))
   1.108 +    end;
   1.109 +
   1.110 +
   1.111 +
   1.112 +
   1.113 +local
   1.114 +
   1.115 +fun retr_thms ([]:MetaSimplifier.rrule list) = []
   1.116 +	  | retr_thms (r::rs) = (#thm r)::(retr_thms rs);
   1.117 +
   1.118 +
   1.119 +fun snds [] = []
   1.120 +  |   snds ((x,y)::l) = y::(snds l);
   1.121 +
   1.122 +
   1.123 +
   1.124 +
   1.125 +fun get_thms_cs claset =
   1.126 +    let val clsset = rep_cs claset
   1.127 +	val safeEs = #safeEs clsset
   1.128 +	val safeIs = #safeIs clsset
   1.129 +	val hazEs = #hazEs clsset
   1.130 +	val hazIs = #hazIs clsset
   1.131 +    in
   1.132 +	safeEs @ safeIs @ hazEs @ hazIs
   1.133 +    end;
   1.134 +
   1.135 +
   1.136 +
   1.137 +fun append_name name [] _ = []
   1.138 +  | append_name name (thm::thms) k = (Thm.name_thm ((name ^ "_" ^ (string_of_int k)),thm)) :: (append_name name thms (k+1));
   1.139 +
   1.140 +fun append_names (name::names) (thms::thmss) =
   1.141 +    let val thms' = append_name name thms 0
   1.142 +    in
   1.143 +	thms'::(append_names names thmss)
   1.144 +    end;
   1.145 +
   1.146 +
   1.147 +fun get_thms_ss [] = []
   1.148 +  | get_thms_ss thms =
   1.149 +    let val names = map Thm.name_of_thm thms 
   1.150 +        val thms' = map (mksimps mksimps_pairs) thms
   1.151 +        val thms'' = append_names names thms'
   1.152 +    in
   1.153 +	ResLib.flat_noDup thms''
   1.154 +    end;
   1.155 +
   1.156 +
   1.157 +
   1.158 +
   1.159 +in
   1.160 +
   1.161 +
   1.162 +(* convert locally declared rules to axiom clauses *)
   1.163 +(* write axiom clauses to ax_file *)
   1.164 +fun isar_local_thms (delta_cs, delta_ss_thms) =
   1.165 +    let val thms_cs = get_thms_cs delta_cs
   1.166 +	val thms_ss = get_thms_ss delta_ss_thms
   1.167 +	val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss))
   1.168 +	val clauses_strs = ResLib.flat_noDup (map ResClause.tptp_clause thms_clauses) (*string list*)
   1.169 +	val ax_file = File.sysify_path axiom_file
   1.170 +	val out = TextIO.openOut ax_file
   1.171 +    in
   1.172 +	(ResLib.writeln_strs out clauses_strs; TextIO.closeOut out)
   1.173 +    end;
   1.174  
   1.175  
   1.176  
   1.177  
   1.178  
   1.179  (* called in Isar automatically *)
   1.180 -fun isar_atp (thms, thm) =
   1.181 -    let val prems = prems_of thm
   1.182 +fun isar_atp (ctxt,thm) =
   1.183 +    let val prems = ProofContext.prems_of ctxt
   1.184 +      val d_cs = Classical.get_delta_claset ctxt
   1.185 +      val d_ss_thms = Simplifier.get_delta_simpset ctxt
   1.186      in
   1.187 -	case prems of [] => () 
   1.188 -		    | _ => (isar_atp_aux thms thm)
   1.189 +	(isar_local_thms (d_cs,d_ss_thms); isar_atp' (prems, thm))
   1.190      end;
   1.191  
   1.192 +end
   1.193 +
   1.194 +
   1.195 +
   1.196 +
   1.197  end;
   1.198  
   1.199  Proof.atp_hook := ResAtp.isar_atp;
     2.1 --- a/src/HOL/Tools/res_clause.ML	Fri Jan 21 13:55:07 2005 +0100
     2.2 +++ b/src/HOL/Tools/res_clause.ML	Fri Jan 21 18:00:18 2005 +0100
     2.3 @@ -662,7 +662,7 @@
     2.4  	val knd = string_of_arKind arcls
     2.5  	val all_lits = concl_lit :: prems_lits
     2.6      in
     2.7 -	"input_clause(" ^ arcls_id ^ "," ^ knd ^ (ResLib.list_to_string' all_lits) ^ ")."
     2.8 +	"input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ (ResLib.list_to_string' all_lits) ^ ")."
     2.9  	
    2.10      end;
    2.11  
    2.12 @@ -674,7 +674,7 @@
    2.13      let val tvar = "(T)"
    2.14      in 
    2.15  	case sup of None => "[++" ^ sub ^ tvar ^ "]"
    2.16 -		  | (Some supcls) =>  "[++" ^ sub ^ tvar ^ ",--" ^ supcls ^ tvar ^ "]"
    2.17 +		  | (Some supcls) =>  "[--" ^ sub ^ tvar ^ ",++" ^ supcls ^ tvar ^ "]"
    2.18      end;
    2.19  
    2.20  
     3.1 --- a/src/Provers/classical.ML	Fri Jan 21 13:55:07 2005 +0100
     3.2 +++ b/src/Provers/classical.ML	Fri Jan 21 18:00:18 2005 +0100
     3.3 @@ -14,6 +14,13 @@
     3.4  the conclusion.
     3.5  *)
     3.6  
     3.7 +
     3.8 +(*added: get_delta_claset, put_delta_claset.
     3.9 +        changed: safe_{dest,elim,intro}_local and haz_{dest,elim,intro}_local
    3.10 +   06/01/05
    3.11 +*)
    3.12 +
    3.13 +
    3.14  (*higher precedence than := facilitates use of references*)
    3.15  infix 4 addSIs addSEs addSDs addIs addEs addDs delrules
    3.16    addSWrapper delSWrapper addWrapper delWrapper
    3.17 @@ -164,6 +171,10 @@
    3.18    val cla_method: (claset -> tactic) -> Args.src -> Proof.context -> Proof.method
    3.19    val cla_method': (claset -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
    3.20    val setup: (theory -> theory) list
    3.21 +
    3.22 +  val get_delta_claset: ProofContext.context -> claset
    3.23 +  val put_delta_claset: claset -> ProofContext.context -> ProofContext.context
    3.24 +
    3.25  end;
    3.26  
    3.27  
    3.28 @@ -890,6 +901,37 @@
    3.29  fun local_claset_of ctxt =
    3.30    context_cs ctxt (get_local_claset ctxt) (get_context_cs ctxt);
    3.31  
    3.32 +(* added for delta_claset: 06/01/05 *)
    3.33 +
    3.34 +structure DeltaClasetArgs =
    3.35 +struct
    3.36 +  val name = "delta_claset";
    3.37 +  type T = claset;
    3.38 +  val empty = empty_cs;
    3.39 +end;
    3.40 +
    3.41 +structure DeltaClaset = DeltaDataFun(DeltaClasetArgs);
    3.42 +val get_delta_claset = DeltaClaset.get;
    3.43 +val put_delta_claset = DeltaClaset.put;
    3.44 +
    3.45 +val get_new_thm_id = ProofContext.get_delta_count_incr;
    3.46 +
    3.47 +
    3.48 +local 
    3.49 +fun rename_thm' (ctxt,thm) =
    3.50 +  let val new_id = get_new_thm_id ctxt
    3.51 +      val new_name = "anon_" ^ (string_of_int new_id)
    3.52 +  in
    3.53 +  Thm.name_thm(new_name,thm)
    3.54 +end;
    3.55 +
    3.56 +in
    3.57 +
    3.58 +(* rename thm if call_atp is true *)
    3.59 +fun rename_thm (ctxt,thm) = if (!Proof.call_atp) then rename_thm' (ctxt,thm) else thm;
    3.60 +
    3.61 +end
    3.62 +     
    3.63  
    3.64  (* attributes *)
    3.65  
    3.66 @@ -909,12 +951,70 @@
    3.67  val haz_intro_global = change_global_cs (op addIs);
    3.68  val rule_del_global = change_global_cs (op delrules) o ContextRules.rule_del_global;
    3.69  
    3.70 -val safe_dest_local = change_local_cs (op addSDs);
    3.71 -val safe_elim_local = change_local_cs (op addSEs);
    3.72 -val safe_intro_local = change_local_cs (op addSIs);
    3.73 -val haz_dest_local = change_local_cs (op addDs);
    3.74 -val haz_elim_local = change_local_cs (op addEs);
    3.75 -val haz_intro_local = change_local_cs (op addIs);
    3.76 +
    3.77 +(* when dest/elim/intro rules are added to local_claset, they are also added to delta_claset in ProofContext.context *)
    3.78 +fun safe_dest_local (ctxt,th) =
    3.79 +    let val thm_name = Thm.name_of_thm th
    3.80 +        val th' = if (thm_name = "") then rename_thm (ctxt,th)  else th
    3.81 +        val delta_cs = get_delta_claset ctxt
    3.82 +	val new_dcs = delta_cs addSDs [th']
    3.83 +	val ctxt' = put_delta_claset new_dcs ctxt 
    3.84 +    in
    3.85 +	change_local_cs (op addSDs) (ctxt',th)
    3.86 +    end;
    3.87 +
    3.88 +fun safe_elim_local (ctxt, th)= 
    3.89 +    let val thm_name = Thm.name_of_thm th
    3.90 +        val th' = if (thm_name = "") then rename_thm (ctxt,th) else th
    3.91 +        val delta_cs = get_delta_claset ctxt
    3.92 +	val new_dcs = delta_cs addSEs [th']
    3.93 +	val ctxt' = put_delta_claset new_dcs ctxt 
    3.94 +    in
    3.95 +	change_local_cs (op addSEs) (ctxt',th)
    3.96 +    end;
    3.97 +
    3.98 +fun safe_intro_local (ctxt, th) = 
    3.99 +    let val thm_name = Thm.name_of_thm th
   3.100 +        val th' = if (thm_name = "") then rename_thm (ctxt,th) else th
   3.101 +        val delta_cs = get_delta_claset ctxt
   3.102 +	val new_dcs = delta_cs addSIs [th']
   3.103 +	val ctxt' = put_delta_claset new_dcs ctxt 
   3.104 +    in
   3.105 +	change_local_cs (op addSIs) (ctxt',th)
   3.106 +    end;
   3.107 +
   3.108 +fun haz_dest_local (ctxt, th)= 
   3.109 +    let val thm_name = Thm.name_of_thm th
   3.110 +        val th' = if (thm_name = "") then rename_thm (ctxt,th)else th
   3.111 +        val delta_cs = get_delta_claset ctxt
   3.112 +	val new_dcs = delta_cs addDs [th']
   3.113 +	val ctxt' = put_delta_claset new_dcs ctxt 
   3.114 +    in
   3.115 +	change_local_cs (op addDs) (ctxt',th)
   3.116 +    end;
   3.117 +
   3.118 +fun haz_elim_local (ctxt,th) =
   3.119 +    let val thm_name = Thm.name_of_thm th
   3.120 +        val th' = if (thm_name = "") then rename_thm (ctxt,th)  else th
   3.121 +        val delta_cs = get_delta_claset ctxt
   3.122 +	val new_dcs = delta_cs addEs [th']
   3.123 +	val ctxt' = put_delta_claset new_dcs ctxt 
   3.124 +    in 
   3.125 +	change_local_cs (op addEs) (ctxt',th)
   3.126 +    end;
   3.127 +
   3.128 +fun haz_intro_local (ctxt,th) = 
   3.129 +    let val thm_name = Thm.name_of_thm th
   3.130 +        val th' = if (thm_name = "") then rename_thm (ctxt,th)  else th
   3.131 +        val delta_cs = get_delta_claset ctxt
   3.132 +	val new_dcs = delta_cs addIs [th']
   3.133 +	val ctxt' = put_delta_claset new_dcs ctxt 
   3.134 +    in 
   3.135 +	change_local_cs (op addIs) (ctxt',th)
   3.136 +    end;
   3.137 +
   3.138 +
   3.139 +(* when a rule is removed from local_claset, it is not removed from delta_claset in ProofContext.context.  But this is unlikely to happen. *)
   3.140  val rule_del_local = change_local_cs (op delrules) o ContextRules.rule_del_local;
   3.141  
   3.142  
     4.1 --- a/src/Provers/simplifier.ML	Fri Jan 21 13:55:07 2005 +0100
     4.2 +++ b/src/Provers/simplifier.ML	Fri Jan 21 18:00:18 2005 +0100
     4.3 @@ -6,6 +6,12 @@
     4.4  for the actual meta-level rewriting engine.
     4.5  *)
     4.6  
     4.7 +(* added: put_delta_simpset, get_delta_simpset
     4.8 +   changed: simp_add_local
     4.9 +   07/01/05
    4.10 +*)
    4.11 +
    4.12 +
    4.13  signature BASIC_SIMPLIFIER =
    4.14  sig
    4.15    include BASIC_META_SIMPLIFIER
    4.16 @@ -93,6 +99,10 @@
    4.17    val method_setup: (Args.T list -> (Method.modifier * Args.T list)) list
    4.18      -> (theory -> theory) list
    4.19    val easy_setup: thm -> thm list -> (theory -> theory) list
    4.20 +
    4.21 +  val get_delta_simpset: ProofContext.context -> Thm.thm list
    4.22 +  val put_delta_simpset: Thm.thm list -> ProofContext.context -> ProofContext.context
    4.23 +
    4.24  end;
    4.25  
    4.26  structure Simplifier: SIMPLIFIER =
    4.27 @@ -293,6 +303,37 @@
    4.28    context_ss ctxt (get_local_simpset ctxt) (get_context_ss ctxt);
    4.29  
    4.30  
    4.31 +(* Jia: added DeltaSimpsetArgs and DeltaSimpset for delta_simpset
    4.32 +	also added methods to retrieve them. *)
    4.33 +
    4.34 +structure DeltaSimpsetArgs =
    4.35 +struct
    4.36 +  val name = "delta_simpset";
    4.37 +  type T = Thm.thm list; (*the type is thm list*)
    4.38 +  val empty = [];
    4.39 +end;
    4.40 +
    4.41 +structure DeltaSimpset = DeltaDataFun(DeltaSimpsetArgs);
    4.42 +val get_delta_simpset = DeltaSimpset.get;
    4.43 +val put_delta_simpset = DeltaSimpset.put;
    4.44 +
    4.45 +val get_new_thm_id = ProofContext.get_delta_count_incr;
    4.46 +
    4.47 +(* Jia: added to rename a local thm if necessary *) 
    4.48 +local 
    4.49 +fun rename_thm' (ctxt,thm) =
    4.50 +  let val new_id = get_new_thm_id ctxt
    4.51 +      val new_name = "anon_" ^ (string_of_int new_id)
    4.52 +  in
    4.53 +  Thm.name_thm(new_name,thm)
    4.54 +end;
    4.55 +
    4.56 +in
    4.57 +
    4.58 +fun rename_thm (ctxt,thm) = if (!Proof.call_atp) then rename_thm' (ctxt,thm) else thm;
    4.59 +
    4.60 +end
    4.61 +
    4.62  (* attributes *)
    4.63  
    4.64  fun change_global_ss f (thy, th) =
    4.65 @@ -305,7 +346,22 @@
    4.66  
    4.67  val simp_add_global = change_global_ss (op addsimps);
    4.68  val simp_del_global = change_global_ss (op delsimps);
    4.69 -val simp_add_local = change_local_ss (op addsimps);
    4.70 +
    4.71 +
    4.72 +
    4.73 +
    4.74 +
    4.75 +(* 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 *)
    4.76 +fun simp_add_local (ctxt,th) = 
    4.77 +    let val delta_ss = get_delta_simpset ctxt
    4.78 +	val thm_name = Thm.name_of_thm th
    4.79 +        val th' = if (thm_name = "") then rename_thm (ctxt,th)  else th
    4.80 +	val new_dss = th'::delta_ss
    4.81 +	val ctxt' = put_delta_simpset new_dss ctxt 
    4.82 +    in
    4.83 +	change_local_ss (op addsimps) (ctxt',th)
    4.84 +    end;
    4.85 +
    4.86  val simp_del_local = change_local_ss (op delsimps);
    4.87  
    4.88  val cong_add_global = change_global_ss (op addcongs);
     5.1 --- a/src/Pure/Isar/ROOT.ML	Fri Jan 21 13:55:07 2005 +0100
     5.2 +++ b/src/Pure/Isar/ROOT.ML	Fri Jan 21 18:00:18 2005 +0100
     5.3 @@ -11,6 +11,7 @@
     5.4  use "rule_cases.ML";
     5.5  use "proof_context.ML";
     5.6  use "proof_data.ML";
     5.7 +use "delta_data.ML"; (*for delta_{claset,simpset}, part of SPASS interface*)
     5.8  use "context_rules.ML";
     5.9  use "locale.ML";
    5.10  use "proof.ML";
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Pure/Isar/delta_data.ML	Fri Jan 21 18:00:18 2005 +0100
     6.3 @@ -0,0 +1,47 @@
     6.4 +(*  Author: Jia Meng, Cambridge University Computer Laboratory (06/01/05)
     6.5 +    Copyright 2004 University of Cambridge
     6.6 +
     6.7 +Used for delta_simpset and delta_claset
     6.8 +*)
     6.9 +
    6.10 +signature DELTA_DATA_ARGS =
    6.11 +sig
    6.12 +  val name: string 
    6.13 +  type T
    6.14 +  val empty: T
    6.15 +end;
    6.16 +
    6.17 +signature DELTA_DATA =
    6.18 +sig
    6.19 +  type T
    6.20 +  val get: ProofContext.context -> T
    6.21 +  val put: T -> ProofContext.context -> ProofContext.context
    6.22 +end;
    6.23 +
    6.24 +functor DeltaDataFun(Args: DELTA_DATA_ARGS): DELTA_DATA =
    6.25 +struct
    6.26 +
    6.27 +type T = Args.T; 
    6.28 +
    6.29 +exception Data of T; 
    6.30 +
    6.31 +val key = Args.name; 
    6.32 +
    6.33 +fun get ctxt =
    6.34 +    let val delta_tab = ProofContext.get_delta ctxt
    6.35 +	val delta_data = Symtab.lookup(delta_tab,key) 
    6.36 +    in
    6.37 +	case delta_data of (Some (Data d)) => d 
    6.38 +			 | None => (Args.empty)
    6.39 +    end;
    6.40 +
    6.41 +fun put delta_data ctxt = 
    6.42 +    let val delta_tab = ProofContext.get_delta ctxt 
    6.43 +	val new_tab = Symtab.update((key,Data delta_data),delta_tab)
    6.44 +    in
    6.45 +	ProofContext.put_delta new_tab ctxt
    6.46 +    end;
    6.47 +
    6.48 +end;
    6.49 +
    6.50 +
     7.1 --- a/src/Pure/Isar/proof.ML	Fri Jan 21 13:55:07 2005 +0100
     7.2 +++ b/src/Pure/Isar/proof.ML	Fri Jan 21 18:00:18 2005 +0100
     7.3 @@ -40,7 +40,7 @@
     7.4    val assert_forward_or_chain: state -> state
     7.5    val assert_backward: state -> state
     7.6    val assert_no_chain: state -> state
     7.7 -  val atp_hook: (Thm.thm list * Thm.thm -> unit) ref
     7.8 +  val atp_hook: (ProofContext.context * Thm.thm -> unit) ref
     7.9    val enter_forward: state -> state
    7.10    val verbose: bool ref
    7.11    val show_main_goal: bool ref
    7.12 @@ -284,6 +284,28 @@
    7.13    let val (ctxt, (_, ((_, x), _))) = find_goal state
    7.14    in (ctxt, x) end;
    7.15  
    7.16 +
    7.17 +(*
    7.18 +(* Jia: added here: get all goals from the state 10/01/05 *)
    7.19 +fun find_all i (state as State (Node {goal = Some goal, ...}, node::nodes)) = 
    7.20 +    let val others = find_all (i+1) (State (node, nodes))
    7.21 +    in
    7.22 +	(context_of state, (i, goal)) :: others
    7.23 +    end
    7.24 +  | find_all i (State (Node {goal = None, ...}, node :: nodes)) = find_all (i + 1) (State (node, nodes))
    7.25 +  | find_all _ (state as State (_, [])) = [];
    7.26 +
    7.27 +val find_all_goals = find_all 0;
    7.28 +
    7.29 +fun find_all_goals_ctxts state =
    7.30 +    let val all_goals = find_all_goals state
    7.31 +	fun find_ctxt_g [] = []
    7.32 +	  | find_ctxt_g ((ctxt, (_, ((_, (_, thm)), _)))::others) = (ctxt,thm) :: (find_ctxt_g others)
    7.33 +    in
    7.34 +	find_ctxt_g all_goals
    7.35 +    end;
    7.36 +*)
    7.37 +
    7.38  fun put_goal goal = map_current (fn (ctxt, facts, mode, _) => (ctxt, facts, mode, goal));
    7.39  
    7.40  fun map_goal f g (State (Node {context, facts, mode, goal = Some goal}, nodes)) =
    7.41 @@ -327,19 +349,18 @@
    7.42  
    7.43  
    7.44  (*Jia Meng: a hook to be used for calling ATPs. *)
    7.45 -val atp_hook = ref (fn (prems,state): (Thm.thm list * Thm.thm) => ());
    7.46 +(* send the entire proof context *)
    7.47 +val atp_hook = ref (fn ctxt_state: ProofContext.context * Thm.thm => ());
    7.48  
    7.49  (*Jia Meng: the modified version of enter_forward. *)
    7.50  (*Jia Meng: atp: Proof.state -> unit *)
    7.51  local
    7.52   fun atp state = 
    7.53 -  let val (ctxt, (_, ((_, (_, thm)), _))) = find_goal state
    7.54 -      val prems = ProofContext.prems_of ctxt  
    7.55 -  in
    7.56 -      (!atp_hook) (prems,thm)          
    7.57 -  end;
    7.58 -  
    7.59 -
    7.60 +     let val (ctxt, (_, ((_, (_, thm)), _))) = find_goal state
    7.61 +     in
    7.62 +	 (!atp_hook) (ctxt,thm)          
    7.63 +     end;
    7.64 +     
    7.65  in
    7.66  
    7.67   fun enter_forward state = 
     8.1 --- a/src/Pure/Isar/proof_context.ML	Fri Jan 21 13:55:07 2005 +0100
     8.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Jan 21 18:00:18 2005 +0100
     8.3 @@ -5,6 +5,13 @@
     8.4  Proof context information.
     8.5  *)
     8.6  
     8.7 +(*Jia: changed: datatype context
     8.8 +       affected files:  make_context, map_context, init, put_data, add_syntax, map_defaults, del_bind, upd_bind, qualified, hide_thms, put_thms, reset_thms, gen_assms, map_fixes, add_cases
     8.9 +
    8.10 +       added: put_delta, get_delta 
    8.11 +       06/01/05
    8.12 +*)
    8.13 +
    8.14  val show_structs = ref false;
    8.15  
    8.16  signature PROOF_CONTEXT =
    8.17 @@ -141,6 +148,11 @@
    8.18    val thms_containing_limit: int ref
    8.19    val print_thms_containing: context -> int option -> string list -> unit
    8.20    val setup: (theory -> theory) list
    8.21 +
    8.22 +  val get_delta: context -> Object.T Symtab.table (* Jia: (claset, simpset) *)
    8.23 +  val put_delta: Object.T Symtab.table -> context -> context 
    8.24 +  val get_delta_count_incr: context -> int
    8.25 +
    8.26  end;
    8.27  
    8.28  signature PRIVATE_PROOF_CONTEXT =
    8.29 @@ -161,6 +173,7 @@
    8.30  
    8.31  type exporter = bool -> cterm list -> thm -> thm Seq.seq;
    8.32  
    8.33 +(* note: another field added to context. *)
    8.34  datatype context =
    8.35    Context of
    8.36     {thy: theory,                                              (*current theory*)
    8.37 @@ -185,17 +198,20 @@
    8.38        typ Vartab.table *                                      (*type constraints*)
    8.39        sort Vartab.table *                                     (*default sorts*)
    8.40        string list *                                           (*used type variables*)
    8.41 -      term list Symtab.table};                                (*type variable occurrences*)
    8.42 +      term list Symtab.table,
    8.43 +      delta: Object.T Symtab.table (* difference between local and global claset and simpset*),
    8.44 +      delta_count: int ref (* number of local anonymous thms *)
    8.45 +};                                (*type variable occurrences*)
    8.46  
    8.47  exception CONTEXT of string * context;
    8.48  
    8.49  
    8.50 -fun make_context (thy, syntax, data, asms, binds, thms, cases, defs) =
    8.51 +fun make_context (thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count) =
    8.52    Context {thy = thy, syntax = syntax, data = data, asms = asms, binds = binds,
    8.53 -    thms = thms, cases = cases, defs = defs};
    8.54 +    thms = thms, cases = cases, defs = defs, delta = delta, delta_count = delta_count};
    8.55  
    8.56 -fun map_context f (Context {thy, syntax, data, asms, binds, thms, cases, defs}) =
    8.57 -  make_context (f (thy, syntax, data, asms, binds, thms, cases, defs));
    8.58 +fun map_context f (Context {thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count}) =
    8.59 +  make_context (f (thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count));
    8.60  
    8.61  fun theory_of (Context {thy, ...}) = thy;
    8.62  val sign_of = Theory.sign_of o theory_of;
    8.63 @@ -293,9 +309,30 @@
    8.64  
    8.65  fun put_data kind f x ctxt =
    8.66   (lookup_data ctxt kind;
    8.67 -  map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
    8.68 +  map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs, delta,delta_count) =>
    8.69      (thy, syntax, Symtab.update ((Object.name_of_kind kind, f x), data),
    8.70 -      asms, binds, thms, cases, defs)) ctxt);
    8.71 +      asms, binds, thms, cases, defs, delta, delta_count)) ctxt);
    8.72 +
    8.73 +
    8.74 +(* added get_delta and put_delta *)
    8.75 +
    8.76 +fun get_delta (ctxt as Context {delta, ...}) = delta;
    8.77 +
    8.78 +fun get_delta_count (ctxt as Context {delta_count, ...}) = !delta_count;
    8.79 +
    8.80 +fun get_delta_count_incr (ctxt as Context {delta_count, ...}) =
    8.81 +  let val current_delta_count = !delta_count
    8.82 +  in
    8.83 +    (delta_count:=(!delta_count)+1;current_delta_count)
    8.84 +end;
    8.85 +
    8.86 +fun incr_delta_count (ctxt as Context {delta_count, ...}) = (delta_count:=(!delta_count)+1);
    8.87 +
    8.88 +(* replace the old delta by new delta *)
    8.89 +(* count not changed! *)
    8.90 +fun put_delta new_delta ctxt =
    8.91 +    map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs,delta, delta_count) =>
    8.92 +    (thy, syntax, data, asms, binds, thms, cases, defs, new_delta,delta_count)) ctxt;
    8.93  
    8.94  
    8.95  (* init context *)
    8.96 @@ -304,7 +341,7 @@
    8.97    let val data = Symtab.map (fn (_, (f, _)) => f thy) (ProofDataData.get thy) in
    8.98      make_context (thy, (Theory.syn_of thy, [], []), data, (([], []), []), Vartab.empty,
    8.99        (false, NameSpace.empty, Symtab.empty, FactIndex.empty), [],
   8.100 -      (Vartab.empty, Vartab.empty, [], Symtab.empty))
   8.101 +      (Vartab.empty, Vartab.empty, [], Symtab.empty), Symtab.empty, ref 0)
   8.102    end;
   8.103  
   8.104  
   8.105 @@ -358,7 +395,7 @@
   8.106  in
   8.107  
   8.108  fun add_syntax decls =
   8.109 -  map_context (fn (thy, (syn, structs, mixfixed), data, asms, binds, thms, cases, defs) =>
   8.110 +  map_context (fn (thy, (syn, structs, mixfixed), data, asms, binds, thms, cases, defs, delta, delta_count) =>
   8.111      let
   8.112        val is_logtype = Sign.is_logtype (Theory.sign_of thy);
   8.113        val structs' = structs @ mapfilter prep_struct decls;
   8.114 @@ -369,7 +406,7 @@
   8.115          |> Syntax.extend_const_gram is_logtype ("", false) mxs_output
   8.116          |> Syntax.extend_const_gram is_logtype ("", true) mxs
   8.117          |> Syntax.extend_trfuns ([], trs, [], []);
   8.118 -    in (thy, (syn', structs', fixed @ mixfixed), data, asms, binds, thms, cases, defs) end)
   8.119 +    in (thy, (syn', structs', fixed @ mixfixed), data, asms, binds, thms, cases, defs, delta, delta_count) end)
   8.120  
   8.121  fun syn_of (Context {syntax = (syn, structs, _), ...}) =
   8.122    syn |> Syntax.extend_trfuns (Syntax.struct_trfuns structs);
   8.123 @@ -666,8 +703,8 @@
   8.124        Some T => Vartab.update (((x, ~1), T), types)
   8.125      | None => types));
   8.126  
   8.127 -fun map_defaults f = map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
   8.128 -  (thy, syntax, data, asms, binds, thms, cases, f defs));
   8.129 +fun map_defaults f = map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count) =>
   8.130 +  (thy, syntax, data, asms, binds, thms, cases, f defs, delta, delta_count));
   8.131  
   8.132  fun declare_syn (ctxt, t) =
   8.133    ctxt
   8.134 @@ -790,8 +827,8 @@
   8.135  
   8.136  fun del_bind (ctxt, xi) =
   8.137    ctxt
   8.138 -  |> map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
   8.139 -      (thy, syntax, data, asms, Vartab.update ((xi, None), binds), thms, cases, defs));
   8.140 +  |> map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count) =>
   8.141 +      (thy, syntax, data, asms, Vartab.update ((xi, None), binds), thms, cases, defs, delta, delta_count));
   8.142  
   8.143  fun upd_bind (ctxt, ((x, i), t)) =
   8.144    let
   8.145 @@ -802,8 +839,8 @@
   8.146    in
   8.147      ctxt
   8.148      |> declare_term t'
   8.149 -    |> map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
   8.150 -      (thy, syntax, data, asms, Vartab.update (((x, i), Some (t', T)), binds), thms, cases, defs))
   8.151 +    |> map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count) =>
   8.152 +      (thy, syntax, data, asms, Vartab.update (((x, i), Some (t', T)), binds), thms, cases, defs, delta, delta_count))
   8.153    end;
   8.154  
   8.155  fun del_upd_bind (ctxt, (xi, None)) = del_bind (ctxt, xi)
   8.156 @@ -968,27 +1005,27 @@
   8.157  fun cond_extern (Context {thms = (_, space, _, _), ...}) = NameSpace.cond_extern space;
   8.158  
   8.159  fun qualified q = map_context (fn (thy, syntax, data, asms, binds,
   8.160 -    (_, space, tab, index), cases, defs) =>
   8.161 -  (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs));
   8.162 +    (_, space, tab, index), cases, defs, delta, delta_count) =>
   8.163 +  (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs, delta, delta_count));
   8.164  
   8.165  fun restore_qualified (Context {thms, ...}) = qualified (#1 thms);
   8.166  
   8.167  fun hide_thms fully names =
   8.168 -  map_context (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs) =>
   8.169 +  map_context (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs, delta, delta_count) =>
   8.170      (thy, syntax, data, asms, binds, (q, NameSpace.hide fully (space, names), tab, index),
   8.171 -      cases, defs));
   8.172 +      cases, defs, delta, delta_count));
   8.173  
   8.174  
   8.175  (* put_thm(s) *)
   8.176  
   8.177  fun put_thms ("", _) ctxt = ctxt
   8.178    | put_thms (name, ths) ctxt = ctxt |> map_context
   8.179 -      (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs) =>
   8.180 +      (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs, delta, delta_count) =>
   8.181          if not q andalso NameSpace.is_qualified name then
   8.182            raise CONTEXT ("Attempt to declare qualified name " ^ quote name, ctxt)
   8.183          else (thy, syntax, data, asms, binds, (q, NameSpace.extend (space, [name]),
   8.184            Symtab.update ((name, Some ths), tab),
   8.185 -            FactIndex.add (is_known ctxt) (index, (name, ths))), cases, defs));
   8.186 +            FactIndex.add (is_known ctxt) (index, (name, ths))), cases, defs, delta, delta_count));
   8.187  
   8.188  fun put_thm (name, th) = put_thms (name, [th]);
   8.189  
   8.190 @@ -999,9 +1036,9 @@
   8.191  (* reset_thms *)
   8.192  
   8.193  fun reset_thms name =
   8.194 -  map_context (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs) =>
   8.195 +  map_context (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs, delta, delta_count) =>
   8.196      (thy, syntax, data, asms, binds, (q, space, Symtab.update ((name, None), tab), index),
   8.197 -      cases, defs));
   8.198 +      cases, defs, delta,delta_count));
   8.199  
   8.200  
   8.201  (* note_thmss *)
   8.202 @@ -1100,9 +1137,9 @@
   8.203      val asmss = map #2 results;
   8.204      val thmss = map #3 results;
   8.205      val ctxt3 = ctxt2 |> map_context
   8.206 -      (fn (thy, syntax, data, ((asms_ct, asms_th), fixes), binds, thms, cases, defs) =>
   8.207 +      (fn (thy, syntax, data, ((asms_ct, asms_th), fixes), binds, thms, cases, defs, delta, delta_count) =>
   8.208          (thy, syntax, data, ((asms_ct @ [(cprops, exp)], asms_th @ asmss), fixes), binds, thms,
   8.209 -          cases, defs));
   8.210 +          cases, defs, delta, delta_count));
   8.211      val ctxt4 = ctxt3 |> put_thms ("prems", prems_of ctxt3);
   8.212    in (warn_extra_tfrees ctxt ctxt4, thmss) end;
   8.213  
   8.214 @@ -1148,8 +1185,8 @@
   8.215  local
   8.216  
   8.217  fun map_fixes f =
   8.218 -  map_context (fn (thy, syntax, data, (assumes, fixes), binds, thms, cases, defs) =>
   8.219 -    (thy, syntax, data, (assumes, f fixes), binds, thms, cases, defs));
   8.220 +  map_context (fn (thy, syntax, data, (assumes, fixes), binds, thms, cases, defs, delta, delta_count) =>
   8.221 +    (thy, syntax, data, (assumes, f fixes), binds, thms, cases, defs, delta, delta_count));
   8.222  
   8.223  fun err_dups ctxt xs = raise CONTEXT ("Duplicate variable(s): " ^ commas_quote xs, ctxt);
   8.224  
   8.225 @@ -1241,8 +1278,8 @@
   8.226    | Some c => prep_case ctxt name xs c);
   8.227  
   8.228  
   8.229 -fun add_cases xs = map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
   8.230 -  (thy, syntax, data, asms, binds, thms, rev (filter_out (equal "" o #1) xs) @ cases, defs));
   8.231 +fun add_cases xs = map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count) =>
   8.232 +  (thy, syntax, data, asms, binds, thms, rev (filter_out (equal "" o #1) xs) @ cases, defs, delta, delta_count));
   8.233  
   8.234  
   8.235