# HG changeset patch # User wenzelm # Date 1130531295 -7200 # Node ID f9890c615c0e8b186e8895632629670e832af1aa # Parent 052622286158a5640d0156c1b89be02f268a5482 added fact_tac, some_fact_tac; retrieve_thms: support literal facts; tuned export interfaces; diff -r 052622286158 -r f9890c615c0e src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Fri Oct 28 22:28:13 2005 +0200 +++ b/src/Pure/Isar/proof_context.ML Fri Oct 28 22:28:15 2005 +0200 @@ -67,9 +67,10 @@ val warn_extra_tfrees: context -> context -> context val generalize: context -> context -> term list -> term list val find_free: term -> string -> term option - val export: bool -> context -> context -> thm -> thm Seq.seq - val export_standard: context -> context -> thm -> thm - val export_plain: context -> context -> thm -> thm + val export: context -> context -> thm -> thm + val exports: context -> context -> thm -> thm Seq.seq + val goal_exports: context -> context -> thm -> thm Seq.seq + val export_plain: context -> context -> thm -> thm (* FIXME *) val drop_schematic: indexname * term option -> indexname * term option val add_binds: (indexname * string option) list -> context -> context val add_binds_i: (indexname * term option) list -> context -> context @@ -93,6 +94,8 @@ -> context * (term list list * (context -> context)) val bind_propp_schematic_i: context * (term * (term list * term list)) list list -> context * (term list list * (context -> context)) + val fact_tac: thm list -> int -> tactic + val some_fact_tac: context -> int -> tactic val get_thm: context -> thmref -> thm val get_thm_closure: context -> thmref -> thm val get_thms: context -> thmref -> thm list @@ -123,7 +126,7 @@ -> ((string * context attribute list) * (term * (term list * term list)) list) list -> context -> (bstring * thm list) list * context val add_view: context -> cterm list -> context -> context - val export_standard_view: cterm list -> context -> context -> thm -> thm + val export_view: cterm list -> context -> context -> thm -> thm val read_vars: (string list * string option) -> context -> (string list * typ option) * context val cert_vars: (string list * typ option) -> context -> (string list * typ option) * context val read_vars_liberal: (string list * string option) -> context -> @@ -711,14 +714,14 @@ fun find_free t x = fold_aterms (get_free x) t NONE; -fun export is_goal inner outer = +fun common_exports is_goal inner outer = let val gen = generalize_tfrees inner outer; val fixes = fixed_names_of inner \\ fixed_names_of outer; val asms = Library.drop (length (assumptions_of outer), assumptions_of inner); val exp_asms = map (fn (cprops, exp) => exp is_goal cprops) asms; in - Goal.norm_hhf_rule + Goal.norm_hhf #> Seq.EVERY (rev exp_asms) #> Seq.map (fn rule => let @@ -729,12 +732,15 @@ in rule |> Drule.forall_intr_list frees - |> Goal.norm_hhf_rule + |> Goal.norm_hhf |> (#1 o Drule.tvars_intr_list tfrees) end) end; -(*without varification*) +val exports = common_exports false; +val goal_exports = common_exports true; + +(*without varification*) (* FIXME *) fun export' is_goal inner outer = let val asms = Library.drop (length (assumptions_of outer), assumptions_of inner); @@ -753,8 +759,8 @@ | NONE => sys_error "Failed to export theorem") end; -val export_standard = gen_export export; -val export_plain = gen_export export'; +val export = gen_export common_exports; +val export_plain = gen_export export'; (* FIXME *) @@ -919,25 +925,37 @@ (** theorems **) +(* fact_tac *) + +fun fact_tac facts = Tactic.norm_hhf_tac THEN' Goal.compose_hhf_tac facts; + +fun some_fact_tac ctxt = Tactic.norm_hhf_tac THEN' SUBGOAL (fn (goal, i) => + let + val (_, _, index) = thms_of ctxt; + val facts = FactIndex.could_unify index (Term.strip_all_body goal); + in fact_tac facts i end); + + (* get_thm(s) *) -(*beware of proper order of evaluation!*) -fun retrieve_thms from_thy pick ctxt = - let - val thy_ref = Theory.self_ref (theory_of ctxt); - val (_, (space, tab), _) = thms_of ctxt; - in - fn xthmref => +fun retrieve_thms _ pick ctxt (Fact s) = let - val thy = Theory.deref thy_ref; + val thy = theory_of ctxt; + val th = Goal.prove thy [] [] (read_prop ctxt s) (K (ALLGOALS (some_fact_tac ctxt))) + handle ERROR_MESSAGE msg => + raise CONTEXT (msg ^ "\nFailed to retrieve literal fact.", ctxt); + in pick "" [th] end + | retrieve_thms from_thy pick ctxt xthmref = + let + val thy = theory_of ctxt; + val (_, (space, tab), _) = thms_of ctxt; val thmref = PureThy.map_name_of_thmref (NameSpace.intern space) xthmref; val name = PureThy.name_of_thmref thmref; in (case Symtab.lookup tab name of SOME ths => map (Thm.transfer thy) (PureThy.select_thm thmref ths) | NONE => from_thy thy xthmref) |> pick name - end - end; + end; val get_thm = retrieve_thms PureThy.get_thms PureThy.single_thm; val get_thm_closure = retrieve_thms PureThy.get_thms_closure PureThy.single_thm; @@ -957,8 +975,8 @@ fun lthms_containing ctxt spec = FactIndex.find (fact_index_of ctxt) spec - |> List.filter (valid_thms ctxt) - |> gen_distinct (eq_fst (op =)); + |> map (valid_thms ctxt ? apfst (fn name => + NameSpace.hidden (if name = "" then "unnamed" else name))); (* name space operations *) @@ -982,7 +1000,12 @@ (* put_thms *) -fun put_thms ("", _) ctxt = ctxt +fun put_thms ("", NONE) ctxt = ctxt + | put_thms ("", SOME ths) ctxt = ctxt |> map_context + (fn (syntax, asms, binds, (naming, facts, index), cases, defs) => + let + val index' = FactIndex.add_local (is_known ctxt) ("", ths) index; + in (syntax, asms, binds, (naming, facts, index'), cases, defs) end) | put_thms (bname, NONE) ctxt = ctxt |> map_context (fn (syntax, asms, binds, (naming, (space, tab), index), cases, defs) => let @@ -995,7 +1018,7 @@ val name = NameSpace.full naming bname; val space' = NameSpace.declare naming name space; val tab' = Symtab.update (name, ths) tab; - val index' = FactIndex.add (is_known ctxt) (name, ths) index; + val index' = FactIndex.add_local (is_known ctxt) (name, ths) index; in (syntax, asms, binds, (naming, (space', tab'), index'), cases, defs) end); @@ -1028,7 +1051,7 @@ (* basic exporters *) -fun export_assume true = Seq.single oo Drule.implies_intr_goals +fun export_assume true = Seq.single oo Drule.implies_intr_protected | export_assume false = Seq.single oo Drule.implies_intr_list; fun export_presume _ = export_assume false; @@ -1078,7 +1101,7 @@ fun add_assm ((name, attrs), props) ctxt = let val cprops = map (Thm.cterm_of (theory_of ctxt)) props; - val asms = map (Goal.norm_hhf_rule o Thm.assume) cprops; + val asms = map (Goal.norm_hhf o Thm.assume) cprops; val ths = map (fn th => ([th], [])) asms; val ([(_, thms)], ctxt') = @@ -1119,8 +1142,7 @@ val asms' = asms1 @ [(view, export_assume)] @ asms2; in (syntax, ((asms', prems), fixes), binds, thms, cases, defs) end); -fun export_standard_view view inner outer = - export_standard (add_view outer view inner) outer; +fun export_view view inner outer = export (add_view outer view inner) outer; (* variables *)