# HG changeset patch # User wenzelm # Date 1137880940 -3600 # Node ID 216e3127050999a8c9952b8a013a84c5f943e612 # Parent 6790126ab5f6d308d5fb6bbb7f29aef7fcf63443 simplified type attribute; tuned; diff -r 6790126ab5f6 -r 216e31270509 src/HOL/Hyperreal/transfer.ML --- a/src/HOL/Hyperreal/transfer.ML Sat Jan 21 23:02:14 2006 +0100 +++ b/src/HOL/Hyperreal/transfer.ML Sat Jan 21 23:02:20 2006 +0100 @@ -2,20 +2,20 @@ ID : $Id$ Author : Brian Huffman -Transfer principle tactic for nonstandard analysis +Transfer principle tactic for nonstandard analysis. *) -signature TRANSFER_TAC = +signature TRANSFER = sig - val transfer_tac: thm list -> int -> tactic + val transfer_tac: Proof.context -> thm list -> int -> tactic val add_const: string -> theory -> theory val setup: theory -> theory end; -structure Transfer: TRANSFER_TAC = +structure Transfer: TRANSFER = struct -structure TransferData = TheoryDataFun +structure TransferData = GenericDataFun (struct val name = "HOL/transfer"; type T = { @@ -25,7 +25,6 @@ consts: string list }; val empty = {intros = [], unfolds = [], refolds = [], consts = []}; - val copy = I; val extend = I; fun merge _ ({intros = intros1, unfolds = unfolds1, @@ -59,29 +58,26 @@ val atomizers = map thm ["atomize_all", "atomize_imp", "atomize_eq"] -fun transfer_thm_of thy ths t = +fun transfer_thm_of ctxt ths t = let - val {intros,unfolds,refolds,consts} = TransferData.get thy + val thy = ProofContext.theory_of ctxt; + val {intros,unfolds,refolds,consts} = TransferData.get (Context.Proof ctxt) val (_$_$t') = concl_of (Tactic.rewrite true unfolds (cterm_of thy t)) val u = unstar_term consts t' - val tacs = - [ rewrite_goals_tac (ths @ refolds @ unfolds) - , rewrite_goals_tac atomizers - , match_tac [transitive_thm] 1 - , resolve_tac [transfer_start] 1 - , REPEAT_ALL_NEW (resolve_tac intros) 1 - , match_tac [reflexive_thm] 1 ] - in Goal.prove thy [] [] (Logic.mk_equals (t,u)) (fn _ => EVERY tacs) end + val tac = + rewrite_goals_tac (ths @ refolds @ unfolds) THEN + rewrite_goals_tac atomizers THEN + match_tac [transitive_thm] 1 THEN + resolve_tac [transfer_start] 1 THEN + REPEAT_ALL_NEW (resolve_tac intros) 1 THEN + match_tac [reflexive_thm] 1 + in Goal.prove thy [] [] (Logic.mk_equals (t,u)) (K tac) end -fun transfer_tac ths = +fun transfer_tac ctxt ths = SUBGOAL (fn (t,i) => (fn th => - let val thy = theory_of_thm th - val tr = transfer_thm_of thy ths t - in rewrite_goals_tac [tr] th - end - ) - ) + let val tr = transfer_thm_of ctxt ths t + in rewrite_goals_tac [tr] th end)) local fun map_intros f = TransferData.map @@ -96,46 +92,32 @@ (fn {intros,unfolds,refolds,consts} => {intros=intros, unfolds=unfolds, refolds=f refolds, consts=consts}) in -fun intro_add_global (thy, thm) = (map_intros (Drule.add_rule thm) thy, thm); -fun intro_del_global (thy, thm) = (map_intros (Drule.del_rule thm) thy, thm); +val intro_add = Thm.declaration_attribute (map_intros o Drule.add_rule); +val intro_del = Thm.declaration_attribute (map_intros o Drule.del_rule); -fun unfold_add_global (thy, thm) = (map_unfolds (Drule.add_rule thm) thy, thm); -fun unfold_del_global (thy, thm) = (map_unfolds (Drule.del_rule thm) thy, thm); +val unfold_add = Thm.declaration_attribute (map_unfolds o Drule.add_rule); +val unfold_del = Thm.declaration_attribute (map_unfolds o Drule.del_rule); -fun refold_add_global (thy, thm) = (map_refolds (Drule.add_rule thm) thy, thm); -fun refold_del_global (thy, thm) = (map_refolds (Drule.del_rule thm) thy, thm); +val refold_add = Thm.declaration_attribute (map_refolds o Drule.add_rule); +val refold_del = Thm.declaration_attribute (map_refolds o Drule.del_rule); end -fun add_const c = TransferData.map +fun add_const c = Context.theory_map (TransferData.map (fn {intros,unfolds,refolds,consts} => - {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts}) + {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts})) -local - val undef_local = - Attrib.add_del_args - Attrib.undef_local_attribute - Attrib.undef_local_attribute; -in - val intro_attr = - (Attrib.add_del_args intro_add_global intro_del_global, undef_local); - val unfold_attr = - (Attrib.add_del_args unfold_add_global unfold_del_global, undef_local); - val refold_attr = - (Attrib.add_del_args refold_add_global refold_del_global, undef_local); -end - -val transfer_method = Method.SIMPLE_METHOD' HEADGOAL o transfer_tac; +val transfer_method = Method.thms_ctxt_args (fn ths => fn ctxt => + Method.SIMPLE_METHOD' HEADGOAL (transfer_tac ctxt ths)); val setup = TransferData.init #> Attrib.add_attributes - [("transfer_intro", intro_attr, + [("transfer_intro", Attrib.add_del_args intro_add intro_del, "declaration of transfer introduction rule"), - ("transfer_unfold", unfold_attr, + ("transfer_unfold", Attrib.add_del_args unfold_add unfold_del, "declaration of transfer unfolding rule"), - ("transfer_refold", refold_attr, + ("transfer_refold", Attrib.add_del_args refold_add refold_del, "declaration of transfer refolding rule")] #> - Method.add_method - ("transfer", Method.thms_args transfer_method, "transfer principle"); + Method.add_method ("transfer", transfer_method, "transfer principle"); end; diff -r 6790126ab5f6 -r 216e31270509 src/HOL/Tools/reconstruction.ML --- a/src/HOL/Tools/reconstruction.ML Sat Jan 21 23:02:14 2006 +0100 +++ b/src/HOL/Tools/reconstruction.ML Sat Jan 21 23:02:20 2006 +0100 @@ -7,8 +7,6 @@ (*Attributes for reconstructing external resolution proofs*) structure Reconstruction = -let open Attrib -in struct (**************************************************************) @@ -16,10 +14,10 @@ (**************************************************************) fun mksubstlist [] sublist = sublist - | mksubstlist ((a, (_, b)) :: rest) sublist = + | mksubstlist ((a, (_, b)) :: rest) sublist = let val vartype = type_of b val avar = Var(a,vartype) - val newlist = ((avar,b)::sublist) + val newlist = ((avar,b)::sublist) in mksubstlist rest newlist end; @@ -31,21 +29,15 @@ select_literal (lit1 + 1) cl1 RSN ((lit2 + 1), cl2); -fun binary_syntax ((i, B), j) (x, A) = (x, binary_rule ((A,i), (B,j))); - -fun gen_binary thm = syntax - ((Scan.lift Args.nat -- thm -- Scan.lift Args.nat) >> binary_syntax); -val binary_global = gen_binary global_thm; -val binary_local = gen_binary local_thm; - -(*I have not done the MRR rule because it seems to be identifical to -binary*) +val binary = Attrib.syntax + (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat + >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => binary_rule ((A, i), (B, j))))); fun inst_single sign t1 t2 cl = let val ct1 = cterm_of sign t1 and ct2 = cterm_of sign t2 in hd (Seq.list_of(distinct_subgoals_tac - (cterm_instantiate [(ct1,ct2)] cl))) + (cterm_instantiate [(ct1,ct2)] cl))) end; fun inst_subst sign substs cl = @@ -71,9 +63,8 @@ inst_subst sign (mksubstlist envlist []) cl end; -fun factor_syntax (i, j) (x, A) = (x, factor_rule (A,i,j)); - -fun factor x = syntax ((Scan.lift (Args.nat -- Args.nat)) >> factor_syntax) x; +val factor = Attrib.syntax (Scan.lift (Args.nat -- Args.nat) + >> (fn (i, j) => Thm.rule_attribute (fn _ => fn A => factor_rule (A, i, j)))); (** Paramodulation **) @@ -91,32 +82,24 @@ in Meson.negated_asm_of_head newth' end; -fun paramod_syntax ((i, B), j) (x, A) = (x, paramod_rule ((A,i), (B,j))); - -fun gen_paramod thm = syntax - ((Scan.lift Args.nat -- thm -- Scan.lift Args.nat) >> paramod_syntax); -val paramod_global = gen_paramod global_thm; -val paramod_local = gen_paramod local_thm; +val paramod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat + >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => paramod_rule ((A, i), (B, j))))); (** Demodulation: rewriting of a single literal (Non-Unit Rewriting, SPASS) **) -fun demod_rule ((cl1, lit1), (cl2 , lit2)) = +fun demod_rule ((cl1, lit1), (cl2 , lit2)) = let val eq_lit_th = select_literal (lit1+1) cl1 val mod_lit_th = select_literal (lit2+1) cl2 - val (fmod_th,thaw) = Drule.freeze_thaw_robust mod_lit_th + val (fmod_th,thaw) = Drule.freeze_thaw_robust mod_lit_th val eqsubst = eq_lit_th RSN (2,rev_subst) val newth = Seq.hd(biresolution false [(false, fmod_th)] 1 eqsubst) val offset = #maxidx(rep_thm newth) + 1 - (*ensures "renaming apart" even when Vars are frozen*) + (*ensures "renaming apart" even when Vars are frozen*) in Meson.negated_asm_of_head (thaw offset newth) end; -fun demod_syntax ((i, B), j) (x, A) = (x, demod_rule ((A,i), (B,j))); - -fun gen_demod thm = syntax - ((Scan.lift Args.nat -- thm -- Scan.lift Args.nat) >> demod_syntax); -val demod_global = gen_demod global_thm; -val demod_local = gen_demod local_thm; +val demod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat + >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => demod_rule ((A, i), (B, j))))); (** Conversion of a theorem into clauses **) @@ -124,22 +107,18 @@ (*For efficiency, we rely upon memo-izing in ResAxioms.*) fun clausify_rule (th,i) = List.nth (ResAxioms.meta_cnf_axiom th, i) -fun clausify_syntax i (x, th) = (x, clausify_rule (th,i)); - -fun clausify x = syntax ((Scan.lift Args.nat) >> clausify_syntax) x; +val clausify = Attrib.syntax (Scan.lift Args.nat + >> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i)))); (** theory setup **) val setup = Attrib.add_attributes - [("binary", (binary_global, binary_local), "binary resolution"), - ("paramod", (paramod_global, paramod_local), "paramodulation"), - ("demod", (demod_global, demod_local), "demodulation"), - ("factor", (factor, factor), "factoring"), - ("clausify", (clausify, clausify), "conversion to clauses")]; + [("binary", binary, "binary resolution"), + ("paramod", paramod, "paramodulation"), + ("demod", demod, "demodulation"), + ("factor", factor, "factoring"), + ("clausify", clausify, "conversion to clauses")]; end -end - - diff -r 6790126ab5f6 -r 216e31270509 src/HOL/Tools/specification_package.ML --- a/src/HOL/Tools/specification_package.ML Sat Jan 21 23:02:14 2006 +0100 +++ b/src/HOL/Tools/specification_package.ML Sat Jan 21 23:02:20 2006 +0100 @@ -8,8 +8,8 @@ signature SPECIFICATION_PACKAGE = sig val quiet_mode: bool ref - val add_specification_i: string option -> (bstring * xstring * bool) list -> - theory attribute + val add_specification: string option -> (bstring * xstring * bool) list -> + theory * thm -> theory * thm end structure SpecificationPackage: SPECIFICATION_PACKAGE = @@ -82,11 +82,15 @@ | NONE => mk_definitional cos arg end -fun add_specification_i axiomatic cos arg = +fun add_specification axiomatic cos arg = arg |> apsnd freezeT |> proc_exprop axiomatic cos |> apsnd standard +fun add_spec x y (context, thm) = + (Context.the_theory context, thm) |> add_specification x y |>> Context.Theory; + + (* Collect all intances of constants in term *) fun collect_consts ( t $ u,tms) = collect_consts (u,collect_consts (t,tms)) @@ -200,7 +204,7 @@ args |> apsnd (remove_alls frees) |> apsnd undo_imps |> apsnd standard - |> Thm.apply_attributes (map (Attrib.global_attribute thy) atts) + |> Thm.theory_attributes (map (Attrib.attribute thy) atts) |> add_final |> Library.swap end @@ -224,9 +228,11 @@ arg |> apsnd freezeT |> process_all (zip3 alt_names rew_imps frees) end + fun post_proc (context, th) = + post_process (Context.theory_of context, th) |>> Context.Theory; in IsarThy.theorem_i Drule.internalK - ("", [add_specification_i axiomatic (zip3 names cnames overloaded), post_process]) + ("", [add_spec axiomatic (zip3 names cnames overloaded), post_proc]) (HOLogic.mk_Trueprop ex_prop, ([], [])) thy end