# HG changeset patch # User wenzelm # Date 1154000592 -7200 # Node ID 7e0693474bcd82004c21eed299c70605a14e9c0a # Parent ece639738db39bcc25c7957b3e3378bdaf781c53 added legacy_pretty_thm (with fall-back on ProtoPure.thy); moved basic assumption operations to assumption.ML; tuned; diff -r ece639738db3 -r 7e0693474bcd src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Jul 27 13:43:11 2006 +0200 +++ b/src/Pure/Isar/proof_context.ML Thu Jul 27 13:43:12 2006 +0200 @@ -4,21 +4,18 @@ The key concept of Isar proof contexts: elevates primitive local reasoning Gamma |- phi to a structured concept, with generic context -elements. +elements. See also structure Variable and Assumption. *) signature PROOF_CONTEXT = sig type context (*= Context.proof*) - type export val theory_of: context -> theory val init: theory -> context val full_name: context -> bstring -> string val consts_of: context -> Consts.T val set_syntax_mode: string * bool -> context -> context val restore_syntax_mode: context -> context -> context - val assms_of: context -> term list - val prems_of: context -> thm list val fact_index_of: context -> FactIndex.T val transfer: theory -> context -> context val map_theory: (theory -> theory) -> context -> context @@ -28,6 +25,7 @@ val pretty_classrel: context -> class list -> Pretty.T val pretty_arity: context -> arity -> Pretty.T val pp: context -> Pretty.pp + val legacy_pretty_thm: bool -> thm -> Pretty.T val pretty_thm: context -> thm -> Pretty.T val pretty_thms: context -> thm list -> Pretty.T val pretty_fact: context -> string * thm list -> Pretty.T @@ -127,17 +125,12 @@ val fix_frees: term -> context -> context val auto_fixes: context * (term list list * 'a) -> context * (term list list * 'a) val bind_fixes: string list -> context -> (term -> term) * context - val assume_export: export - val presume_export: export - val add_assumes: cterm list -> context -> thm list * context - val add_assms: export -> + val add_assms: Assumption.export -> ((string * attribute list) * (string * string list) list) list -> context -> (bstring * thm list) list * context - val add_assms_i: export -> + val add_assms_i: Assumption.export -> ((string * attribute list) * (term * term list) list) list -> context -> (bstring * thm list) list * context - val add_view: context -> cterm list -> context -> context - val export_view: cterm list -> context -> context -> thm -> thm val add_cases: bool -> (string * RuleCases.T option) list -> context -> context val apply_case: RuleCases.T -> context -> (string * term list) list * context val get_case: context -> string -> string option list -> RuleCases.T @@ -169,22 +162,16 @@ (** Isar proof context information **) -type export = bool -> cterm list -> thm -> thm Seq.seq; - datatype ctxt = Ctxt of {naming: NameSpace.naming, (*local naming conventions*) syntax: LocalSyntax.T, (*local syntax*) consts: Consts.T * Consts.T, (*global/local consts*) - assms: - ((cterm list * export) list * (*assumes and views: A ==> _*) - thm list), (*prems: A |- A*) thms: thm list NameSpace.table * FactIndex.T, (*local thms*) cases: (string * (RuleCases.T * bool)) list}; (*local contexts*) -fun make_ctxt (naming, syntax, consts, assms, thms, cases) = - Ctxt {naming = naming, syntax = syntax, consts = consts, assms = assms, - thms = thms, cases = cases}; +fun make_ctxt (naming, syntax, consts, thms, cases) = + Ctxt {naming = naming, syntax = syntax, consts = consts, thms = thms, cases = cases}; val local_naming = NameSpace.default_naming |> NameSpace.add_path "local"; @@ -194,7 +181,7 @@ type T = ctxt; fun init thy = make_ctxt (local_naming, LocalSyntax.init thy, - (Sign.consts_of thy, Sign.consts_of thy), ([], []), + (Sign.consts_of thy, Sign.consts_of thy), (NameSpace.empty_table, FactIndex.empty), []); fun print _ _ = (); ); @@ -204,32 +191,28 @@ fun rep_context ctxt = ContextData.get ctxt |> (fn Ctxt args => args); fun map_context f = - ContextData.map (fn Ctxt {naming, syntax, consts, assms, thms, cases} => - make_ctxt (f (naming, syntax, consts, assms, thms, cases))); + ContextData.map (fn Ctxt {naming, syntax, consts, thms, cases} => + make_ctxt (f (naming, syntax, consts, thms, cases))); fun map_naming f = - map_context (fn (naming, syntax, consts, assms, thms, cases) => - (f naming, syntax, consts, assms, thms, cases)); + map_context (fn (naming, syntax, consts, thms, cases) => + (f naming, syntax, consts, thms, cases)); fun map_syntax f = - map_context (fn (naming, syntax, consts, assms, thms, cases) => - (naming, f syntax, consts, assms, thms, cases)); + map_context (fn (naming, syntax, consts, thms, cases) => + (naming, f syntax, consts, thms, cases)); fun map_consts f = - map_context (fn (naming, syntax, consts, assms, thms, cases) => - (naming, syntax, f consts, assms, thms, cases)); - -fun map_assms f = - map_context (fn (naming, syntax, consts, assms, thms, cases) => - (naming, syntax, consts, f assms, thms, cases)); + map_context (fn (naming, syntax, consts, thms, cases) => + (naming, syntax, f consts, thms, cases)); fun map_thms f = - map_context (fn (naming, syntax, consts, assms, thms, cases) => - (naming, syntax, consts, assms, f thms, cases)); + map_context (fn (naming, syntax, consts, thms, cases) => + (naming, syntax, consts, f thms, cases)); fun map_cases f = - map_context (fn (naming, syntax, consts, assms, thms, cases) => - (naming, syntax, consts, assms, thms, f cases)); + map_context (fn (naming, syntax, consts, thms, cases) => + (naming, syntax, consts, thms, f cases)); val naming_of = #naming o rep_context; val full_name = NameSpace.full o naming_of; @@ -241,10 +224,6 @@ val consts_of = #2 o #consts o rep_context; -val assumptions_of = #1 o #assms o rep_context; -val assms_of = map Thm.term_of o maps #1 o assumptions_of; -val prems_of = #2 o #assms o rep_context; - val thms_of = #thms o rep_context; val fact_index_of = #2 o thms_of; @@ -303,8 +282,16 @@ fun pp ctxt = Pretty.pp (pretty_term ctxt, pretty_typ ctxt, pretty_sort ctxt, pretty_classrel ctxt, pretty_arity ctxt); +fun legacy_pretty_thm quote th = + let + val thy = Thm.theory_of_thm th; + val pp = + if Theory.eq_thy (thy, ProtoPure.thy) then Sign.pp thy + else pp (init thy); + in Display.pretty_thm_aux pp quote false [] th end; + fun pretty_thm ctxt th = - Display.pretty_thm_aux (pp ctxt) false true (assms_of ctxt) th; + Display.pretty_thm_aux (pp ctxt) false true (Assumption.assms_of ctxt) th; fun pretty_thms ctxt [th] = pretty_thm ctxt th | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths)); @@ -563,15 +550,8 @@ (** export theorems **) fun common_exports is_goal inner outer = - let - val asms = Library.drop (length (assumptions_of outer), assumptions_of inner); - val exp_asms = rev (map (fn (cprops, exp) => exp is_goal cprops) asms); - in - map Goal.norm_hhf_protect - #> Seq.map_list (Seq.EVERY exp_asms) - #> Seq.map (Variable.export inner outer) - #> Seq.map (map Goal.norm_hhf_protect) - end; + Assumption.exports is_goal inner outer + #> Seq.map (Variable.export inner outer); val goal_exports = common_exports true; val exports = common_exports false; @@ -959,59 +939,20 @@ (** assumptions **) -(* basic exports *) - -(* - [A] - : - B - -------- - #A ==> B -*) -fun assume_export true = Seq.single oo Drule.implies_intr_protected - | assume_export false = Seq.single oo Drule.implies_intr_list; - -(* - [A] - : - B - ------- - A ==> B -*) -fun presume_export _ = assume_export false; - - -(* plain assumptions *) - -fun new_prems new_asms new_prems = - map_assms (fn (asms, prems) => (asms @ [new_asms], prems @ new_prems)) #> - (fn ctxt => put_thms_internal (AutoBind.premsN, SOME (prems_of ctxt)) ctxt); - -fun add_assumes asms = - let val prems = map (Goal.norm_hhf o Thm.assume) asms - in new_prems (asms, assume_export) prems #> pair prems end; - - -(* generic assms *) - local -fun gen_assm ((name, attrs), props) ctxt = - let - val cprops = map (Thm.cterm_of (theory_of ctxt)) props; - val prems = map (Goal.norm_hhf o Thm.assume) cprops; - val ([(_, thms)], ctxt') = - ctxt - |> auto_bind_facts props - |> note_thmss_i [((name, attrs), map (fn th => ([th], [])) prems)]; - in ((cprops, prems, (name, thms)), ctxt') end; - fun gen_assms prepp exp args ctxt = let + val cert = Thm.cterm_of (theory_of ctxt); val (propss, ctxt1) = swap (prepp (ctxt, map snd args)); - val (results, ctxt2) = fold_map gen_assm (map fst args ~~ propss) ctxt1; - val ctxt3 = new_prems (maps #1 results, exp) (maps #2 results) ctxt2; - in (map #3 results, tap (Variable.warn_extra_tfrees ctxt) ctxt3) end; + val _ = Variable.warn_extra_tfrees ctxt ctxt1; + val (premss, ctxt2) = fold_burrow (Assumption.add_assms exp o map cert) propss ctxt1; + in + ctxt2 + |> auto_bind_facts (flat propss) + |> put_thms_internal (AutoBind.premsN, SOME (Assumption.prems_of ctxt2)) + |> note_thmss_i (map fst args ~~ map (map (fn th => ([th], []))) premss) + end; in @@ -1021,17 +962,6 @@ end; -(* additional views *) - -fun add_view outer view = map_assms (fn (asms, prems) => - let - val (asms1, asms2) = chop (length (assumptions_of outer)) asms; - val asms' = asms1 @ [(view, assume_export)] @ asms2; - in (asms', prems) end); - -fun export_view view inner outer = singleton (export_standard (add_view outer view inner) outer); - - (** cases **) @@ -1215,7 +1145,7 @@ (*prems*) val limit = ! prems_limit; - val prems = prems_of ctxt; + val prems = Assumption.prems_of ctxt; val len = length prems; val prt_prems = if null prems then [] else [Pretty.big_list "prems:" ((if len <= limit then [] else [Pretty.str "..."]) @