Jia Meng: delta simpsets and clasets

--- a/src/HOL/Tools/res_atp.ML	Fri Jan 21 13:55:07 2005 +0100
+++ b/src/HOL/Tools/res_atp.ML	Fri Jan 21 18:00:18 2005 +0100
@@ -4,16 +4,20 @@
 
 ATPs with TPTP format input.
 *)
+
+(*Jia: changed: isar_atp now processes entire proof context.  fetch thms from delta simpset/claset*)
+
 signature RES_ATP = 
 sig
 
 val trace_res : bool ref
 val axiom_file : Path.T
 val hyps_file : Path.T
-val isar_atp : Thm.thm list * Thm.thm -> unit
+val isar_atp : ProofContext.context * Thm.thm -> unit
 val prob_file : Path.T
 val atp_ax_tac : Thm.thm list -> int -> Tactical.tactic
 val atp_tac : int -> Tactical.tactic
+val debug: bool ref
 
 end;
 
@@ -21,6 +25,10 @@
 
 struct
 
+(* used for debug *)
+val debug = ref false;
+
+fun debug_tac tac = (warning "testing";tac);
 (* default value is false *)
 
 val trace_res = ref false;
@@ -46,10 +54,10 @@
 
 
 
-fun tptp_inputs thms = 
+fun tptp_inputs thms n = 
     let val clss = map (ResClause.make_conjecture_clause_thm) thms
 	val tptp_clss = ResLib.flat_noDup(map ResClause.tptp_clause clss) 
-        val probfile = File.sysify_path prob_file
+        val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
 	val out = TextIO.openOut(probfile)
     in
 	(ResLib.writeln_strs out tptp_clss; TextIO.closeOut out; (if !trace_res then (warning probfile) else ()))
@@ -58,12 +66,14 @@
 
 (**** for Isabelle/ML interface  ****)
 
-fun call_atp_tac thms = (tptp_inputs thms; dummy_tac);
+fun call_atp_tac thms n = (tptp_inputs thms n; dummy_tac);
+
 
 
-val atp_tac = SELECT_GOAL
-  (EVERY1 [rtac ccontr, atomize_tac, skolemize_tac, 
-  METAHYPS(fn negs => (call_atp_tac(make_clauses negs)))]);
+
+fun atp_tac n = SELECT_GOAL
+  (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
+  METAHYPS(fn negs => (call_atp_tac (make_clauses negs) n))]) n;
 
 
 fun atp_ax_tac axioms n = 
@@ -97,13 +107,13 @@
 fun repeat_someI_ex thm = repeat_RS thm someI_ex;
 
 
-
+(* convert clauses from "assume" to conjecture. write to file "hyps" *)
 fun isar_atp_h thms =
     let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms
 	val prems' = map repeat_someI_ex prems
 	val prems'' = make_clauses prems'
 	val prems''' = ResAxioms.rm_Eps [] prems''
-	val clss = map ResClause.make_hypothesis_clause prems'''
+	val clss = map ResClause.make_conjecture_clause prems'''
 	val tptp_clss = ResLib.flat_noDup (map ResClause.tptp_clause clss)
         val hypsfile = File.sysify_path hyps_file
 	val out = TextIO.openOut(hypsfile)
@@ -116,21 +126,109 @@
 
 val isar_atp_g = atp_tac;
 
-fun isar_atp_aux thms thm = 
-    (isar_atp_h thms; isar_atp_g 1 thm;());
+
+fun isar_atp_goal' thm k n = 
+    if (k > n) then () else (isar_atp_g k thm; isar_atp_goal' thm (k+1) n);
+
+
+fun isar_atp_goal thm n_subgoals = (if (!debug) then warning (string_of_thm thm) else (isar_atp_goal' thm 1 n_subgoals));
+
+
+
+fun isar_atp_aux thms thm n_subgoals = 
+    (isar_atp_h thms; isar_atp_goal thm n_subgoals); (* convert both to conjecture clauses, but write to different files *)
+
+
+fun isar_atp' (thms, thm) =
+    let val prems = prems_of thm
+    in
+	case prems of [] => (if (!debug) then warning "entering forward, no goal" else ())
+		    | _ => (isar_atp_aux thms thm (length prems))
+    end;
+
+
+
+
+local
+
+fun retr_thms ([]:MetaSimplifier.rrule list) = []
+	  | retr_thms (r::rs) = (#thm r)::(retr_thms rs);
+
+
+fun snds [] = []
+  |   snds ((x,y)::l) = y::(snds l);
+
+
+
+
+fun get_thms_cs claset =
+    let val clsset = rep_cs claset
+	val safeEs = #safeEs clsset
+	val safeIs = #safeIs clsset
+	val hazEs = #hazEs clsset
+	val hazIs = #hazIs clsset
+    in
+	safeEs @ safeIs @ hazEs @ hazIs
+    end;
+
+
+
+fun append_name name [] _ = []
+  | append_name name (thm::thms) k = (Thm.name_thm ((name ^ "_" ^ (string_of_int k)),thm)) :: (append_name name thms (k+1));
+
+fun append_names (name::names) (thms::thmss) =
+    let val thms' = append_name name thms 0
+    in
+	thms'::(append_names names thmss)
+    end;
+
+
+fun get_thms_ss [] = []
+  | get_thms_ss thms =
+    let val names = map Thm.name_of_thm thms 
+        val thms' = map (mksimps mksimps_pairs) thms
+        val thms'' = append_names names thms'
+    in
+	ResLib.flat_noDup thms''
+    end;
+
+
+
+
+in
+
+
+(* convert locally declared rules to axiom clauses *)
+(* write axiom clauses to ax_file *)
+fun isar_local_thms (delta_cs, delta_ss_thms) =
+    let val thms_cs = get_thms_cs delta_cs
+	val thms_ss = get_thms_ss delta_ss_thms
+	val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss))
+	val clauses_strs = ResLib.flat_noDup (map ResClause.tptp_clause thms_clauses) (*string list*)
+	val ax_file = File.sysify_path axiom_file
+	val out = TextIO.openOut ax_file
+    in
+	(ResLib.writeln_strs out clauses_strs; TextIO.closeOut out)
+    end;
 
 
 
 
 
 (* called in Isar automatically *)
-fun isar_atp (thms, thm) =
-    let val prems = prems_of thm
+fun isar_atp (ctxt,thm) =
+    let val prems = ProofContext.prems_of ctxt
+      val d_cs = Classical.get_delta_claset ctxt
+      val d_ss_thms = Simplifier.get_delta_simpset ctxt
     in
-	case prems of [] => () 
-		    | _ => (isar_atp_aux thms thm)
+	(isar_local_thms (d_cs,d_ss_thms); isar_atp' (prems, thm))
     end;
 
+end
+
+
+
+
 end;
 
 Proof.atp_hook := ResAtp.isar_atp;

--- a/src/HOL/Tools/res_clause.ML	Fri Jan 21 13:55:07 2005 +0100
+++ b/src/HOL/Tools/res_clause.ML	Fri Jan 21 18:00:18 2005 +0100
@@ -662,7 +662,7 @@
 	val knd = string_of_arKind arcls
 	val all_lits = concl_lit :: prems_lits
     in
-	"input_clause(" ^ arcls_id ^ "," ^ knd ^ (ResLib.list_to_string' all_lits) ^ ")."
+	"input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ (ResLib.list_to_string' all_lits) ^ ")."
 	
     end;
 
@@ -674,7 +674,7 @@
     let val tvar = "(T)"
     in 
 	case sup of None => "[++" ^ sub ^ tvar ^ "]"
-		  | (Some supcls) =>  "[++" ^ sub ^ tvar ^ ",--" ^ supcls ^ tvar ^ "]"
+		  | (Some supcls) =>  "[--" ^ sub ^ tvar ^ ",++" ^ supcls ^ tvar ^ "]"
     end;
 
 

--- a/src/Provers/classical.ML	Fri Jan 21 13:55:07 2005 +0100
+++ b/src/Provers/classical.ML	Fri Jan 21 18:00:18 2005 +0100
@@ -14,6 +14,13 @@
 the conclusion.
 *)
 
+
+(*added: get_delta_claset, put_delta_claset.
+        changed: safe_{dest,elim,intro}_local and haz_{dest,elim,intro}_local
+   06/01/05
+*)
+
+
 (*higher precedence than := facilitates use of references*)
 infix 4 addSIs addSEs addSDs addIs addEs addDs delrules
   addSWrapper delSWrapper addWrapper delWrapper
@@ -164,6 +171,10 @@
   val cla_method: (claset -> tactic) -> Args.src -> Proof.context -> Proof.method
   val cla_method': (claset -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
   val setup: (theory -> theory) list
+
+  val get_delta_claset: ProofContext.context -> claset
+  val put_delta_claset: claset -> ProofContext.context -> ProofContext.context
+
 end;
 
 
@@ -890,6 +901,37 @@
 fun local_claset_of ctxt =
   context_cs ctxt (get_local_claset ctxt) (get_context_cs ctxt);
 
+(* added for delta_claset: 06/01/05 *)
+
+structure DeltaClasetArgs =
+struct
+  val name = "delta_claset";
+  type T = claset;
+  val empty = empty_cs;
+end;
+
+structure DeltaClaset = DeltaDataFun(DeltaClasetArgs);
+val get_delta_claset = DeltaClaset.get;
+val put_delta_claset = DeltaClaset.put;
+
+val get_new_thm_id = ProofContext.get_delta_count_incr;
+
+
+local 
+fun rename_thm' (ctxt,thm) =
+  let val new_id = get_new_thm_id ctxt
+      val new_name = "anon_" ^ (string_of_int new_id)
+  in
+  Thm.name_thm(new_name,thm)
+end;
+
+in
+
+(* rename thm if call_atp is true *)
+fun rename_thm (ctxt,thm) = if (!Proof.call_atp) then rename_thm' (ctxt,thm) else thm;
+
+end
+     
 
 (* attributes *)
 
@@ -909,12 +951,70 @@
 val haz_intro_global = change_global_cs (op addIs);
 val rule_del_global = change_global_cs (op delrules) o ContextRules.rule_del_global;
 
-val safe_dest_local = change_local_cs (op addSDs);
-val safe_elim_local = change_local_cs (op addSEs);
-val safe_intro_local = change_local_cs (op addSIs);
-val haz_dest_local = change_local_cs (op addDs);
-val haz_elim_local = change_local_cs (op addEs);
-val haz_intro_local = change_local_cs (op addIs);
+
+(* when dest/elim/intro rules are added to local_claset, they are also added to delta_claset in ProofContext.context *)
+fun safe_dest_local (ctxt,th) =
+    let val thm_name = Thm.name_of_thm th
+        val th' = if (thm_name = "") then rename_thm (ctxt,th)  else th
+        val delta_cs = get_delta_claset ctxt
+	val new_dcs = delta_cs addSDs [th']
+	val ctxt' = put_delta_claset new_dcs ctxt 
+    in
+	change_local_cs (op addSDs) (ctxt',th)
+    end;
+
+fun safe_elim_local (ctxt, th)= 
+    let val thm_name = Thm.name_of_thm th
+        val th' = if (thm_name = "") then rename_thm (ctxt,th) else th
+        val delta_cs = get_delta_claset ctxt
+	val new_dcs = delta_cs addSEs [th']
+	val ctxt' = put_delta_claset new_dcs ctxt 
+    in
+	change_local_cs (op addSEs) (ctxt',th)
+    end;
+
+fun safe_intro_local (ctxt, th) = 
+    let val thm_name = Thm.name_of_thm th
+        val th' = if (thm_name = "") then rename_thm (ctxt,th) else th
+        val delta_cs = get_delta_claset ctxt
+	val new_dcs = delta_cs addSIs [th']
+	val ctxt' = put_delta_claset new_dcs ctxt 
+    in
+	change_local_cs (op addSIs) (ctxt',th)
+    end;
+
+fun haz_dest_local (ctxt, th)= 
+    let val thm_name = Thm.name_of_thm th
+        val th' = if (thm_name = "") then rename_thm (ctxt,th)else th
+        val delta_cs = get_delta_claset ctxt
+	val new_dcs = delta_cs addDs [th']
+	val ctxt' = put_delta_claset new_dcs ctxt 
+    in
+	change_local_cs (op addDs) (ctxt',th)
+    end;
+
+fun haz_elim_local (ctxt,th) =
+    let val thm_name = Thm.name_of_thm th
+        val th' = if (thm_name = "") then rename_thm (ctxt,th)  else th
+        val delta_cs = get_delta_claset ctxt
+	val new_dcs = delta_cs addEs [th']
+	val ctxt' = put_delta_claset new_dcs ctxt 
+    in 
+	change_local_cs (op addEs) (ctxt',th)
+    end;
+
+fun haz_intro_local (ctxt,th) = 
+    let val thm_name = Thm.name_of_thm th
+        val th' = if (thm_name = "") then rename_thm (ctxt,th)  else th
+        val delta_cs = get_delta_claset ctxt
+	val new_dcs = delta_cs addIs [th']
+	val ctxt' = put_delta_claset new_dcs ctxt 
+    in 
+	change_local_cs (op addIs) (ctxt',th)
+    end;
+
+
+(* when a rule is removed from local_claset, it is not removed from delta_claset in ProofContext.context.  But this is unlikely to happen. *)
 val rule_del_local = change_local_cs (op delrules) o ContextRules.rule_del_local;
 
 

--- a/src/Provers/simplifier.ML	Fri Jan 21 13:55:07 2005 +0100
+++ b/src/Provers/simplifier.ML	Fri Jan 21 18:00:18 2005 +0100
@@ -6,6 +6,12 @@
 for the actual meta-level rewriting engine.
 *)
 
+(* added: put_delta_simpset, get_delta_simpset
+   changed: simp_add_local
+   07/01/05
+*)
+
+
 signature BASIC_SIMPLIFIER =
 sig
   include BASIC_META_SIMPLIFIER
@@ -93,6 +99,10 @@
   val method_setup: (Args.T list -> (Method.modifier * Args.T list)) list
     -> (theory -> theory) list
   val easy_setup: thm -> thm list -> (theory -> theory) list
+
+  val get_delta_simpset: ProofContext.context -> Thm.thm list
+  val put_delta_simpset: Thm.thm list -> ProofContext.context -> ProofContext.context
+
 end;
 
 structure Simplifier: SIMPLIFIER =
@@ -293,6 +303,37 @@
   context_ss ctxt (get_local_simpset ctxt) (get_context_ss ctxt);
 
 
+(* Jia: added DeltaSimpsetArgs and DeltaSimpset for delta_simpset
+	also added methods to retrieve them. *)
+
+structure DeltaSimpsetArgs =
+struct
+  val name = "delta_simpset";
+  type T = Thm.thm list; (*the type is thm list*)
+  val empty = [];
+end;
+
+structure DeltaSimpset = DeltaDataFun(DeltaSimpsetArgs);
+val get_delta_simpset = DeltaSimpset.get;
+val put_delta_simpset = DeltaSimpset.put;
+
+val get_new_thm_id = ProofContext.get_delta_count_incr;
+
+(* Jia: added to rename a local thm if necessary *) 
+local 
+fun rename_thm' (ctxt,thm) =
+  let val new_id = get_new_thm_id ctxt
+      val new_name = "anon_" ^ (string_of_int new_id)
+  in
+  Thm.name_thm(new_name,thm)
+end;
+
+in
+
+fun rename_thm (ctxt,thm) = if (!Proof.call_atp) then rename_thm' (ctxt,thm) else thm;
+
+end
+
 (* attributes *)
 
 fun change_global_ss f (thy, th) =
@@ -305,7 +346,22 @@
 
 val simp_add_global = change_global_ss (op addsimps);
 val simp_del_global = change_global_ss (op delsimps);
-val simp_add_local = change_local_ss (op addsimps);
+
+
+
+
+
+(* 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 *)
+fun simp_add_local (ctxt,th) = 
+    let val delta_ss = get_delta_simpset ctxt
+	val thm_name = Thm.name_of_thm th
+        val th' = if (thm_name = "") then rename_thm (ctxt,th)  else th
+	val new_dss = th'::delta_ss
+	val ctxt' = put_delta_simpset new_dss ctxt 
+    in
+	change_local_ss (op addsimps) (ctxt',th)
+    end;
+
 val simp_del_local = change_local_ss (op delsimps);
 
 val cong_add_global = change_global_ss (op addcongs);

--- a/src/Pure/Isar/ROOT.ML	Fri Jan 21 13:55:07 2005 +0100
+++ b/src/Pure/Isar/ROOT.ML	Fri Jan 21 18:00:18 2005 +0100
@@ -11,6 +11,7 @@
 use "rule_cases.ML";
 use "proof_context.ML";
 use "proof_data.ML";
+use "delta_data.ML"; (*for delta_{claset,simpset}, part of SPASS interface*)
 use "context_rules.ML";
 use "locale.ML";
 use "proof.ML";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/delta_data.ML	Fri Jan 21 18:00:18 2005 +0100
@@ -0,0 +1,47 @@
+(*  Author: Jia Meng, Cambridge University Computer Laboratory (06/01/05)
+    Copyright 2004 University of Cambridge
+
+Used for delta_simpset and delta_claset
+*)
+
+signature DELTA_DATA_ARGS =
+sig
+  val name: string 
+  type T
+  val empty: T
+end;
+
+signature DELTA_DATA =
+sig
+  type T
+  val get: ProofContext.context -> T
+  val put: T -> ProofContext.context -> ProofContext.context
+end;
+
+functor DeltaDataFun(Args: DELTA_DATA_ARGS): DELTA_DATA =
+struct
+
+type T = Args.T; 
+
+exception Data of T; 
+
+val key = Args.name; 
+
+fun get ctxt =
+    let val delta_tab = ProofContext.get_delta ctxt
+	val delta_data = Symtab.lookup(delta_tab,key) 
+    in
+	case delta_data of (Some (Data d)) => d 
+			 | None => (Args.empty)
+    end;
+
+fun put delta_data ctxt = 
+    let val delta_tab = ProofContext.get_delta ctxt 
+	val new_tab = Symtab.update((key,Data delta_data),delta_tab)
+    in
+	ProofContext.put_delta new_tab ctxt
+    end;
+
+end;
+
+

--- a/src/Pure/Isar/proof.ML	Fri Jan 21 13:55:07 2005 +0100
+++ b/src/Pure/Isar/proof.ML	Fri Jan 21 18:00:18 2005 +0100
@@ -40,7 +40,7 @@
   val assert_forward_or_chain: state -> state
   val assert_backward: state -> state
   val assert_no_chain: state -> state
-  val atp_hook: (Thm.thm list * Thm.thm -> unit) ref
+  val atp_hook: (ProofContext.context * Thm.thm -> unit) ref
   val enter_forward: state -> state
   val verbose: bool ref
   val show_main_goal: bool ref
@@ -284,6 +284,28 @@
   let val (ctxt, (_, ((_, x), _))) = find_goal state
   in (ctxt, x) end;
 
+
+(*
+(* Jia: added here: get all goals from the state 10/01/05 *)
+fun find_all i (state as State (Node {goal = Some goal, ...}, node::nodes)) = 
+    let val others = find_all (i+1) (State (node, nodes))
+    in
+	(context_of state, (i, goal)) :: others
+    end
+  | find_all i (State (Node {goal = None, ...}, node :: nodes)) = find_all (i + 1) (State (node, nodes))
+  | find_all _ (state as State (_, [])) = [];
+
+val find_all_goals = find_all 0;
+
+fun find_all_goals_ctxts state =
+    let val all_goals = find_all_goals state
+	fun find_ctxt_g [] = []
+	  | find_ctxt_g ((ctxt, (_, ((_, (_, thm)), _)))::others) = (ctxt,thm) :: (find_ctxt_g others)
+    in
+	find_ctxt_g all_goals
+    end;
+*)
+
 fun put_goal goal = map_current (fn (ctxt, facts, mode, _) => (ctxt, facts, mode, goal));
 
 fun map_goal f g (State (Node {context, facts, mode, goal = Some goal}, nodes)) =
@@ -327,19 +349,18 @@
 
 
 (*Jia Meng: a hook to be used for calling ATPs. *)
-val atp_hook = ref (fn (prems,state): (Thm.thm list * Thm.thm) => ());
+(* send the entire proof context *)
+val atp_hook = ref (fn ctxt_state: ProofContext.context * Thm.thm => ());
 
 (*Jia Meng: the modified version of enter_forward. *)
 (*Jia Meng: atp: Proof.state -> unit *)
 local
  fun atp state = 
-  let val (ctxt, (_, ((_, (_, thm)), _))) = find_goal state
-      val prems = ProofContext.prems_of ctxt  
-  in
-      (!atp_hook) (prems,thm)          
-  end;
-  
-
+     let val (ctxt, (_, ((_, (_, thm)), _))) = find_goal state
+     in
+	 (!atp_hook) (ctxt,thm)          
+     end;
+     
 in
 
  fun enter_forward state = 

--- a/src/Pure/Isar/proof_context.ML	Fri Jan 21 13:55:07 2005 +0100
+++ b/src/Pure/Isar/proof_context.ML	Fri Jan 21 18:00:18 2005 +0100
@@ -5,6 +5,13 @@
 Proof context information.
 *)
 
+(*Jia: changed: datatype context
+       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
+
+       added: put_delta, get_delta 
+       06/01/05
+*)
+
 val show_structs = ref false;
 
 signature PROOF_CONTEXT =
@@ -141,6 +148,11 @@
   val thms_containing_limit: int ref
   val print_thms_containing: context -> int option -> string list -> unit
   val setup: (theory -> theory) list
+
+  val get_delta: context -> Object.T Symtab.table (* Jia: (claset, simpset) *)
+  val put_delta: Object.T Symtab.table -> context -> context 
+  val get_delta_count_incr: context -> int
+
 end;
 
 signature PRIVATE_PROOF_CONTEXT =
@@ -161,6 +173,7 @@
 
 type exporter = bool -> cterm list -> thm -> thm Seq.seq;
 
+(* note: another field added to context. *)
 datatype context =
   Context of
    {thy: theory,                                              (*current theory*)
@@ -185,17 +198,20 @@
       typ Vartab.table *                                      (*type constraints*)
       sort Vartab.table *                                     (*default sorts*)
       string list *                                           (*used type variables*)
-      term list Symtab.table};                                (*type variable occurrences*)
+      term list Symtab.table,
+      delta: Object.T Symtab.table (* difference between local and global claset and simpset*),
+      delta_count: int ref (* number of local anonymous thms *)
+};                                (*type variable occurrences*)
 
 exception CONTEXT of string * context;
 
 
-fun make_context (thy, syntax, data, asms, binds, thms, cases, defs) =
+fun make_context (thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count) =
   Context {thy = thy, syntax = syntax, data = data, asms = asms, binds = binds,
-    thms = thms, cases = cases, defs = defs};
+    thms = thms, cases = cases, defs = defs, delta = delta, delta_count = delta_count};
 
-fun map_context f (Context {thy, syntax, data, asms, binds, thms, cases, defs}) =
-  make_context (f (thy, syntax, data, asms, binds, thms, cases, defs));
+fun map_context f (Context {thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count}) =
+  make_context (f (thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count));
 
 fun theory_of (Context {thy, ...}) = thy;
 val sign_of = Theory.sign_of o theory_of;
@@ -293,9 +309,30 @@
 
 fun put_data kind f x ctxt =
  (lookup_data ctxt kind;
-  map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
+  map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs, delta,delta_count) =>
     (thy, syntax, Symtab.update ((Object.name_of_kind kind, f x), data),
-      asms, binds, thms, cases, defs)) ctxt);
+      asms, binds, thms, cases, defs, delta, delta_count)) ctxt);
+
+
+(* added get_delta and put_delta *)
+
+fun get_delta (ctxt as Context {delta, ...}) = delta;
+
+fun get_delta_count (ctxt as Context {delta_count, ...}) = !delta_count;
+
+fun get_delta_count_incr (ctxt as Context {delta_count, ...}) =
+  let val current_delta_count = !delta_count
+  in
+    (delta_count:=(!delta_count)+1;current_delta_count)
+end;
+
+fun incr_delta_count (ctxt as Context {delta_count, ...}) = (delta_count:=(!delta_count)+1);
+
+(* replace the old delta by new delta *)
+(* count not changed! *)
+fun put_delta new_delta ctxt =
+    map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs,delta, delta_count) =>
+    (thy, syntax, data, asms, binds, thms, cases, defs, new_delta,delta_count)) ctxt;
 
 
 (* init context *)
@@ -304,7 +341,7 @@
   let val data = Symtab.map (fn (_, (f, _)) => f thy) (ProofDataData.get thy) in
     make_context (thy, (Theory.syn_of thy, [], []), data, (([], []), []), Vartab.empty,
       (false, NameSpace.empty, Symtab.empty, FactIndex.empty), [],
-      (Vartab.empty, Vartab.empty, [], Symtab.empty))
+      (Vartab.empty, Vartab.empty, [], Symtab.empty), Symtab.empty, ref 0)
   end;
 
 
@@ -358,7 +395,7 @@
 in
 
 fun add_syntax decls =
-  map_context (fn (thy, (syn, structs, mixfixed), data, asms, binds, thms, cases, defs) =>
+  map_context (fn (thy, (syn, structs, mixfixed), data, asms, binds, thms, cases, defs, delta, delta_count) =>
     let
       val is_logtype = Sign.is_logtype (Theory.sign_of thy);
       val structs' = structs @ mapfilter prep_struct decls;
@@ -369,7 +406,7 @@
         |> Syntax.extend_const_gram is_logtype ("", false) mxs_output
         |> Syntax.extend_const_gram is_logtype ("", true) mxs
         |> Syntax.extend_trfuns ([], trs, [], []);
-    in (thy, (syn', structs', fixed @ mixfixed), data, asms, binds, thms, cases, defs) end)
+    in (thy, (syn', structs', fixed @ mixfixed), data, asms, binds, thms, cases, defs, delta, delta_count) end)
 
 fun syn_of (Context {syntax = (syn, structs, _), ...}) =
   syn |> Syntax.extend_trfuns (Syntax.struct_trfuns structs);
@@ -666,8 +703,8 @@
       Some T => Vartab.update (((x, ~1), T), types)
     | None => types));
 
-fun map_defaults f = map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
-  (thy, syntax, data, asms, binds, thms, cases, f defs));
+fun map_defaults f = map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count) =>
+  (thy, syntax, data, asms, binds, thms, cases, f defs, delta, delta_count));
 
 fun declare_syn (ctxt, t) =
   ctxt
@@ -790,8 +827,8 @@
 
 fun del_bind (ctxt, xi) =
   ctxt
-  |> map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
-      (thy, syntax, data, asms, Vartab.update ((xi, None), binds), thms, cases, defs));
+  |> map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count) =>
+      (thy, syntax, data, asms, Vartab.update ((xi, None), binds), thms, cases, defs, delta, delta_count));
 
 fun upd_bind (ctxt, ((x, i), t)) =
   let
@@ -802,8 +839,8 @@
   in
     ctxt
     |> declare_term t'
-    |> map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
-      (thy, syntax, data, asms, Vartab.update (((x, i), Some (t', T)), binds), thms, cases, defs))
+    |> map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count) =>
+      (thy, syntax, data, asms, Vartab.update (((x, i), Some (t', T)), binds), thms, cases, defs, delta, delta_count))
   end;
 
 fun del_upd_bind (ctxt, (xi, None)) = del_bind (ctxt, xi)
@@ -968,27 +1005,27 @@
 fun cond_extern (Context {thms = (_, space, _, _), ...}) = NameSpace.cond_extern space;
 
 fun qualified q = map_context (fn (thy, syntax, data, asms, binds,
-    (_, space, tab, index), cases, defs) =>
-  (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs));
+    (_, space, tab, index), cases, defs, delta, delta_count) =>
+  (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs, delta, delta_count));
 
 fun restore_qualified (Context {thms, ...}) = qualified (#1 thms);
 
 fun hide_thms fully names =
-  map_context (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs) =>
+  map_context (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs, delta, delta_count) =>
     (thy, syntax, data, asms, binds, (q, NameSpace.hide fully (space, names), tab, index),
-      cases, defs));
+      cases, defs, delta, delta_count));
 
 
 (* put_thm(s) *)
 
 fun put_thms ("", _) ctxt = ctxt
   | put_thms (name, ths) ctxt = ctxt |> map_context
-      (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs) =>
+      (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs, delta, delta_count) =>
         if not q andalso NameSpace.is_qualified name then
           raise CONTEXT ("Attempt to declare qualified name " ^ quote name, ctxt)
         else (thy, syntax, data, asms, binds, (q, NameSpace.extend (space, [name]),
           Symtab.update ((name, Some ths), tab),
-            FactIndex.add (is_known ctxt) (index, (name, ths))), cases, defs));
+            FactIndex.add (is_known ctxt) (index, (name, ths))), cases, defs, delta, delta_count));
 
 fun put_thm (name, th) = put_thms (name, [th]);
 
@@ -999,9 +1036,9 @@
 (* reset_thms *)
 
 fun reset_thms name =
-  map_context (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs) =>
+  map_context (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs, delta, delta_count) =>
     (thy, syntax, data, asms, binds, (q, space, Symtab.update ((name, None), tab), index),
-      cases, defs));
+      cases, defs, delta,delta_count));
 
 
 (* note_thmss *)
@@ -1100,9 +1137,9 @@
     val asmss = map #2 results;
     val thmss = map #3 results;
     val ctxt3 = ctxt2 |> map_context
-      (fn (thy, syntax, data, ((asms_ct, asms_th), fixes), binds, thms, cases, defs) =>
+      (fn (thy, syntax, data, ((asms_ct, asms_th), fixes), binds, thms, cases, defs, delta, delta_count) =>
         (thy, syntax, data, ((asms_ct @ [(cprops, exp)], asms_th @ asmss), fixes), binds, thms,
-          cases, defs));
+          cases, defs, delta, delta_count));
     val ctxt4 = ctxt3 |> put_thms ("prems", prems_of ctxt3);
   in (warn_extra_tfrees ctxt ctxt4, thmss) end;
 
@@ -1148,8 +1185,8 @@
 local
 
 fun map_fixes f =
-  map_context (fn (thy, syntax, data, (assumes, fixes), binds, thms, cases, defs) =>
-    (thy, syntax, data, (assumes, f fixes), binds, thms, cases, defs));
+  map_context (fn (thy, syntax, data, (assumes, fixes), binds, thms, cases, defs, delta, delta_count) =>
+    (thy, syntax, data, (assumes, f fixes), binds, thms, cases, defs, delta, delta_count));
 
 fun err_dups ctxt xs = raise CONTEXT ("Duplicate variable(s): " ^ commas_quote xs, ctxt);
 
@@ -1241,8 +1278,8 @@
   | Some c => prep_case ctxt name xs c);
 
 
-fun add_cases xs = map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
-  (thy, syntax, data, asms, binds, thms, rev (filter_out (equal "" o #1) xs) @ cases, defs));
+fun add_cases xs = map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs, delta, delta_count) =>
+  (thy, syntax, data, asms, binds, thms, rev (filter_out (equal "" o #1) xs) @ cases, defs, delta, delta_count));