# HG changeset patch # User wenzelm # Date 1236869792 -3600 # Node ID b0ce15e4633d4131b1a9147ac7e4adeb9f7c970b # Parent 5e9248e8e2f8c67ffe1e2a5ec83808b34bf5d210# Parent e0b66c11e7e4ef70655568f06504ddc91f9daa78 merged diff -r 5e9248e8e2f8 -r b0ce15e4633d src/HOL/Import/shuffler.ML --- 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 diff -r 5e9248e8e2f8 -r b0ce15e4633d src/HOL/Statespace/state_space.ML --- 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; diff -r 5e9248e8e2f8 -r b0ce15e4633d src/Pure/Isar/args.ML --- 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) || diff -r 5e9248e8e2f8 -r b0ce15e4633d src/Pure/Isar/local_defs.ML --- 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; diff -r 5e9248e8e2f8 -r b0ce15e4633d src/Pure/Isar/proof_context.ML --- 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 [] diff -r 5e9248e8e2f8 -r b0ce15e4633d src/Pure/Isar/specification.ML --- 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 diff -r 5e9248e8e2f8 -r b0ce15e4633d src/Pure/Isar/theory_target.ML --- 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*) diff -r 5e9248e8e2f8 -r b0ce15e4633d src/Pure/Tools/find_theorems.ML --- 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; diff -r 5e9248e8e2f8 -r b0ce15e4633d src/Pure/assumption.ML --- 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 diff -r 5e9248e8e2f8 -r b0ce15e4633d src/Pure/goal.ML --- 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) []); diff -r 5e9248e8e2f8 -r b0ce15e4633d src/Tools/quickcheck.ML --- 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 () =