--- a/src/HOL/Import/shuffler.ML Thu Mar 12 15:31:44 2009 +0100
+++ b/src/HOL/Import/shuffler.ML Thu Mar 12 15:56:32 2009 +0100
@@ -662,7 +662,7 @@
fun search_meth ctxt =
let
val thy = ProofContext.theory_of ctxt
- val prems = Assumption.prems_of ctxt
+ val prems = Assumption.all_prems_of ctxt
in
Method.SIMPLE_METHOD' (gen_shuffle_tac thy true (map (pair "premise") prems))
end
--- a/src/HOL/Statespace/state_space.ML Thu Mar 12 15:31:44 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML Thu Mar 12 15:56:32 2009 +0100
@@ -419,7 +419,7 @@
val expr = ([(suffix valuetypesN name,
(("",false),Expression.Positional (map SOME pars)))],[]);
in
- prove_interpretation_in (ALLGOALS o solve_tac o Assumption.prems_of)
+ prove_interpretation_in (ALLGOALS o solve_tac o Assumption.all_prems_of)
(suffix valuetypesN name, expr) thy
end;
--- a/src/Pure/Isar/args.ML Thu Mar 12 15:31:44 2009 +0100
+++ b/src/Pure/Isar/args.ML Thu Mar 12 15:56:32 2009 +0100
@@ -227,7 +227,7 @@
val bang_facts = Scan.peek (fn context =>
P.position ($$$ "!") >> (fn (_, pos) =>
(warning ("use of prems in proof method" ^ Position.str_of pos);
- Assumption.prems_of (Context.proof_of context))) || Scan.succeed []);
+ Assumption.all_prems_of (Context.proof_of context))) || Scan.succeed []);
val from_to =
P.nat -- ($$$ "-" |-- P.nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
--- a/src/Pure/Isar/local_defs.ML Thu Mar 12 15:31:44 2009 +0100
+++ b/src/Pure/Isar/local_defs.ML Thu Mar 12 15:56:32 2009 +0100
@@ -135,7 +135,7 @@
fun export inner outer = (*beware of closure sizes*)
let
val exp = Assumption.export false inner outer;
- val prems = Assumption.prems_of inner;
+ val prems = Assumption.all_prems_of inner;
in fn th =>
let
val th' = exp th;
--- a/src/Pure/Isar/proof_context.ML Thu Mar 12 15:31:44 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML Thu Mar 12 15:56:32 2009 +0100
@@ -301,7 +301,7 @@
in Display.pretty_thm_aux (Syntax.pp_global thy) true false [] th end;
fun pretty_thm ctxt th =
- let val asms = map Thm.term_of (Assumption.assms_of ctxt)
+ let val asms = map Thm.term_of (Assumption.all_assms_of ctxt)
in Display.pretty_thm_aux (Syntax.pp ctxt) false true asms th end;
fun pretty_thms ctxt [th] = pretty_thm ctxt th
@@ -1370,7 +1370,7 @@
Pretty.commas (map prt_fix fixes))];
(*prems*)
- val prems = Assumption.prems_of ctxt;
+ val prems = Assumption.all_prems_of ctxt;
val len = length prems;
val suppressed = len - ! prems_limit;
val prt_prems = if null prems then []
--- a/src/Pure/Isar/specification.ML Thu Mar 12 15:31:44 2009 +0100
+++ b/src/Pure/Isar/specification.ML Thu Mar 12 15:56:32 2009 +0100
@@ -147,12 +147,16 @@
val subst = Term.subst_atomic (map Free xs ~~ consts);
(*axioms*)
- val (axioms, axioms_thy) = consts_thy |> fold_map (fn ((b, atts), props) =>
- fold_map Thm.add_axiom (* FIXME proper use of binding!? *)
- ((map o apfst) Binding.name (PureThy.name_multi (Binding.name_of b) (map subst props)))
- #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])]))) specs;
+ val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) =>
+ fold_map Thm.add_axiom
+ (map (apfst (fn a => Binding.map_name (K a) b))
+ (PureThy.name_multi (Binding.name_of b) (map subst props)))
+ #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])])));
+
+ (*facts*)
val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK
(Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms);
+
val _ =
if not do_print then ()
else print_consts (ProofContext.init thy') (K false) xs;
@@ -256,15 +260,12 @@
local
-fun subtract_prems ctxt1 ctxt2 =
- Library.drop (length (Assumption.prems_of ctxt1), Assumption.prems_of ctxt2);
-
fun prep_statement prep_att prep_stmt elems concl ctxt =
(case concl of
Element.Shows shows =>
let
val (propp, elems_ctxt) = prep_stmt elems (map snd shows) ctxt;
- val prems = subtract_prems ctxt elems_ctxt;
+ val prems = Assumption.local_prems_of elems_ctxt ctxt;
val stmt = Attrib.map_specs prep_att (map fst shows ~~ propp);
val goal_ctxt = fold (fold (Variable.auto_fixes o fst)) propp elems_ctxt;
in ((prems, stmt, []), goal_ctxt) end
@@ -300,7 +301,7 @@
val atts = map (Attrib.internal o K)
[RuleCases.consumes (~ (length obtains)), RuleCases.case_names case_names];
- val prems = subtract_prems ctxt elems_ctxt;
+ val prems = Assumption.local_prems_of elems_ctxt ctxt;
val stmt = [((Binding.empty, atts), [(thesis, [])])];
val (facts, goal_ctxt) = elems_ctxt
--- a/src/Pure/Isar/theory_target.ML Thu Mar 12 15:31:44 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML Thu Mar 12 15:56:32 2009 +0100
@@ -52,7 +52,7 @@
val fixes =
map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));
val assumes =
- map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])])) (Assumption.assms_of ctxt);
+ map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])])) (Assumption.all_assms_of ctxt);
val elems =
(if null fixes then [] else [Element.Fixes fixes]) @
(if null assumes then [] else [Element.Assumes assumes]);
@@ -109,7 +109,7 @@
val th = Goal.norm_result raw_th;
val (defs, th') = LocalDefs.export ctxt thy_ctxt th;
val concl_conv = MetaSimplifier.rewrite true defs (Thm.cprop_of th);
- val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume) (Assumption.assms_of ctxt);
+ val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume) (Assumption.all_assms_of ctxt);
val nprems = Thm.nprems_of th' - Thm.nprems_of th;
(*export fixes*)
--- a/src/Pure/Tools/find_theorems.ML Thu Mar 12 15:31:44 2009 +0100
+++ b/src/Pure/Tools/find_theorems.ML Thu Mar 12 15:56:32 2009 +0100
@@ -336,7 +336,7 @@
fun find_theorems ctxt opt_goal rem_dups raw_criteria =
let
- val add_prems = Seq.hd o (TRY (Method.insert_tac (Assumption.prems_of ctxt) 1));
+ val add_prems = Seq.hd o (TRY (Method.insert_tac (Assumption.all_prems_of ctxt) 1));
val opt_goal' = Option.map add_prems opt_goal;
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
--- a/src/Pure/assumption.ML Thu Mar 12 15:31:44 2009 +0100
+++ b/src/Pure/assumption.ML Thu Mar 12 15:56:32 2009 +0100
@@ -1,7 +1,7 @@
(* Title: Pure/assumption.ML
Author: Makarius
-Local assumptions, parameterized by export rules.
+Context assumptions, parameterized by export rules.
*)
signature ASSUMPTION =
@@ -10,12 +10,13 @@
val assume_export: export
val presume_export: export
val assume: cterm -> thm
- val assms_of: Proof.context -> cterm list
- val prems_of: Proof.context -> thm list
+ val all_assms_of: Proof.context -> cterm list
+ val all_prems_of: Proof.context -> thm list
val extra_hyps: Proof.context -> thm -> term list
+ val local_assms_of: Proof.context -> Proof.context -> cterm list
+ val local_prems_of: Proof.context -> Proof.context -> thm list
val add_assms: export -> cterm list -> Proof.context -> thm list * Proof.context
val add_assumes: cterm list -> Proof.context -> thm list * Proof.context
- val add_view: Proof.context -> cterm list -> Proof.context -> Proof.context
val export: bool -> Proof.context -> Proof.context -> thm -> thm
val export_term: Proof.context -> Proof.context -> term -> term
val export_morphism: Proof.context -> Proof.context -> morphism
@@ -68,18 +69,31 @@
fun map_data f = Data.map (fn Data {assms, prems} => make_data (f (assms, prems)));
fun rep_data ctxt = Data.get ctxt |> (fn Data args => args);
-val assumptions_of = #assms o rep_data;
-val assms_of = maps #2 o assumptions_of;
-val prems_of = #prems o rep_data;
+
+(* all assumptions *)
+
+val all_assumptions_of = #assms o rep_data;
+val all_assms_of = maps #2 o all_assumptions_of;
+val all_prems_of = #prems o rep_data;
-fun extra_hyps ctxt th = subtract (op aconv) (map Thm.term_of (assms_of ctxt)) (Thm.hyps_of th);
+fun extra_hyps ctxt th =
+ subtract (op aconv) (map Thm.term_of (all_assms_of ctxt)) (Thm.hyps_of th);
+
+(*named prems -- legacy feature*)
+val _ = Context.>>
+ (Context.map_theory (PureThy.add_thms_dynamic (Binding.name "prems",
+ fn Context.Theory _ => [] | Context.Proof ctxt => all_prems_of ctxt)));
-(* named prems -- legacy feature *)
+(* local assumptions *)
+
+fun local_assumptions_of inner outer =
+ Library.drop (length (all_assumptions_of outer), all_assumptions_of inner);
-val _ = Context.>>
- (Context.map_theory (PureThy.add_thms_dynamic (Binding.name "prems",
- fn Context.Theory _ => [] | Context.Proof ctxt => prems_of ctxt)));
+val local_assms_of = maps #2 oo local_assumptions_of;
+
+fun local_prems_of inner outer =
+ Library.drop (length (all_prems_of outer), all_prems_of inner);
(* add assumptions *)
@@ -92,27 +106,18 @@
val add_assumes = add_assms assume_export;
-fun add_view outer view = map_data (fn (asms, prems) =>
- let
- val (asms1, asms2) = chop (length (assumptions_of outer)) asms;
- val asms' = asms1 @ [(assume_export, view)] @ asms2;
- in (asms', prems) end);
-
(* export *)
-fun diff_assms inner outer =
- Library.drop (length (assumptions_of outer), assumptions_of inner);
-
fun export is_goal inner outer =
- let val asms = diff_assms inner outer in
+ let val asms = local_assumptions_of inner outer in
MetaSimplifier.norm_hhf_protect
#> fold_rev (fn (e, As) => #1 (e is_goal As)) asms
#> MetaSimplifier.norm_hhf_protect
end;
fun export_term inner outer =
- fold_rev (fn (e, As) => #2 (e false As)) (diff_assms inner outer);
+ fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer);
fun export_morphism inner outer =
let
--- a/src/Pure/goal.ML Thu Mar 12 15:31:44 2009 +0100
+++ b/src/Pure/goal.ML Thu Mar 12 15:56:32 2009 +0100
@@ -110,7 +110,7 @@
val cert = Thm.cterm_of thy;
val certT = Thm.ctyp_of thy;
- val assms = Assumption.assms_of ctxt;
+ val assms = Assumption.all_assms_of ctxt;
val As = map Thm.term_of assms;
val xs = map Free (fold Term.add_frees (prop :: As) []);
--- a/src/Tools/quickcheck.ML Thu Mar 12 15:31:44 2009 +0100
+++ b/src/Tools/quickcheck.ML Thu Mar 12 15:56:32 2009 +0100
@@ -144,7 +144,7 @@
fun test_goal_auto int state =
let
val ctxt = Proof.context_of state;
- val assms = map term_of (Assumption.assms_of ctxt);
+ val assms = map term_of (Assumption.all_assms_of ctxt);
val Test_Params { size, iterations, default_type } =
(snd o Data.get o Proof.theory_of) state;
fun test () =