# HG changeset patch # User wenzelm # Date 1121263647 -7200 # Node ID 916387f7afd221cc8daf0c1dbce71a75f46f6707 # Parent fadf80952202f2e30ffc21be7b54852a38e6f9ce removed obsolete delta stuff; diff -r fadf80952202 -r 916387f7afd2 src/Provers/classical.ML --- a/src/Provers/classical.ML Wed Jul 13 16:07:26 2005 +0200 +++ b/src/Provers/classical.ML Wed Jul 13 16:07:27 2005 +0200 @@ -14,13 +14,6 @@ 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 @@ -171,10 +164,6 @@ val cla_method: (claset -> tactic) -> Method.src -> Proof.context -> Proof.method val cla_method': (claset -> int -> tactic) -> Method.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; @@ -899,41 +888,6 @@ fun local_claset_of ctxt = context_cs ctxt (get_local_claset ctxt) (get_context_cs ctxt); -(* added for delta_claset: 06/01/05 *) -(* CB: changed "delta clasets" to context data, - moved counter to here, it is no longer a ref *) - -structure DeltaClasetArgs = -struct - val name = "Provers/delta_claset"; - type T = claset * int; - fun init _ = (empty_cs, 0) - fun print ctxt cs = (); -end; - -structure DeltaClasetData = ProofDataFun(DeltaClasetArgs); -val get_delta_claset = #1 o DeltaClasetData.get; -fun put_delta_claset cs = DeltaClasetData.map (fn (_, i) => (cs, i)); -fun delta_increment ctxt = - let val ctxt' = DeltaClasetData.map (fn (ss, i) => (ss, i+1)) ctxt - in (ctxt', #2 (DeltaClasetData.get ctxt')) - end; - -local -fun rename_thm' (ctxt,thm) = - let val (new_ctxt, new_id) = delta_increment ctxt - val new_name = "anon_cla_" ^ (string_of_int new_id) - in - (new_ctxt, 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 (ctxt, thm); - -end - (* attributes *) @@ -953,70 +907,12 @@ val haz_intro_global = change_global_cs (op addIs); val rule_del_global = change_global_cs (op delrules) o ContextRules.rule_del_global; - -(* 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 (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, 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 (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, 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 (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, 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 (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th)else (ctxt, 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 (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, 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 (ctxt', th') = if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, 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 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); val rule_del_local = change_local_cs (op delrules) o ContextRules.rule_del_local; @@ -1158,8 +1054,7 @@ (** theory setup **) -val setup = [GlobalClaset.init, LocalClaset.init, DeltaClasetData.init, - setup_attrs, setup_methods]; +val setup = [GlobalClaset.init, LocalClaset.init, setup_attrs, setup_methods]; @@ -1175,4 +1070,3 @@ end; - diff -r fadf80952202 -r 916387f7afd2 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Wed Jul 13 16:07:26 2005 +0200 +++ b/src/Pure/simplifier.ML Wed Jul 13 16:07:27 2005 +0200 @@ -6,12 +6,6 @@ meta_simplifier.ML 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 @@ -98,9 +92,6 @@ 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 = @@ -134,7 +125,7 @@ mk_context_simproc name o map (Thm.cterm_of thy o Logic.varify); fun context_simproc thy name = - context_simproc_i thy name o map (Sign.simple_read_term thy TypeInfer.logicT); + context_simproc_i thy name o map (Sign.read_term thy); (* datatype context_ss *) @@ -303,44 +294,6 @@ 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. *) -(* CB: changed "delta simpsets" to context data, - moved counter to here, it is no longer a ref *) - -structure DeltaSimpsetArgs = -struct - val name = "Pure/delta_simpset"; - type T = Thm.thm list * int; (*the type is thm list * int*) - fun init _ = ([], 0); - fun print ctxt thms = (); -end; - -structure DeltaSimpsetData = ProofDataFun(DeltaSimpsetArgs); -val _ = Context.add_setup [DeltaSimpsetData.init]; - -val get_delta_simpset = #1 o DeltaSimpsetData.get; -fun put_delta_simpset ss = DeltaSimpsetData.map (fn (_, i) => (ss, i)); -fun delta_increment ctxt = - let val ctxt' = DeltaSimpsetData.map (fn (ss, i) => (ss, i+1)) ctxt - in (ctxt', #2 (DeltaSimpsetData.get ctxt')) - end; - -(* Jia: added to rename a local thm if necessary *) -local -fun rename_thm' (ctxt,thm) = - let val (new_ctxt, new_id) = delta_increment ctxt - val new_name = "anon_simp_" ^ (string_of_int new_id) - in - (new_ctxt, Thm.name_thm(new_name,thm)) -end; - -in - -fun rename_thm (ctxt,thm) = if (!Proof.call_atp) then rename_thm' (ctxt,thm) else (ctxt, thm); - -end - (* attributes *) fun change_global_ss f (thy, th) = @@ -353,23 +306,7 @@ val simp_add_global = change_global_ss (op addsimps); val simp_del_global = change_global_ss (op delsimps); - - - - - -(* 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 (ctxt', th') = - if (thm_name = "") then rename_thm (ctxt,th) else (ctxt, 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_add_local = change_local_ss (op addsimps); val simp_del_local = change_local_ss (op delsimps); val cong_add_global = change_global_ss (op addcongs); @@ -378,6 +315,8 @@ val cong_del_local = change_local_ss (op delcongs); +(* tactics *) + val simp_tac = generic_simp_tac false (false, false, false); val asm_simp_tac = generic_simp_tac false (false, true, false); val full_simp_tac = generic_simp_tac false (true, false, false); @@ -385,8 +324,6 @@ val asm_full_simp_tac = generic_simp_tac false (true, true, true); val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true); - - (*the abstraction over the proof state delays the dereferencing*) fun Simp_tac i st = simp_tac (simpset ()) i st; fun Asm_simp_tac i st = asm_simp_tac (simpset ()) i st; @@ -394,6 +331,9 @@ fun Asm_lr_simp_tac i st = asm_lr_simp_tac (simpset ()) i st; fun Asm_full_simp_tac i st = asm_full_simp_tac (simpset ()) i st; + +(* conversions *) + val simplify = simp_thm (false, false, false); val asm_simplify = simp_thm (false, true, false); val full_simplify = simp_thm (true, false, false);