--- 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;
--- 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
-
-
--- 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