# HG changeset patch # User wenzelm # Date 1153867487 -7200 # Node ID 974d98969ba695d4e822dcb5d9531c0ab9025240 # Parent 90e551baac6ad4738d28bb4a7dd6263e0a3e08a7 moved pprint functions to Isar/proof_display.ML; added primitive add_assumes; tuned internal prems: no names; diff -r 90e551baac6a -r 974d98969ba6 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Wed Jul 26 00:44:46 2006 +0200 +++ b/src/Pure/Isar/proof_context.ML Wed Jul 26 00:44:47 2006 +0200 @@ -127,14 +127,15 @@ 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 -> ((string * attribute list) * (string * string list) list) list -> context -> (bstring * thm list) list * context val add_assms_i: export -> ((string * attribute list) * (term * term list) list) list -> context -> (bstring * thm list) list * context - val assume_export: export - val presume_export: export 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 @@ -152,8 +153,6 @@ val prems_limit: int ref val pretty_ctxt: context -> Pretty.T list val pretty_context: context -> Pretty.T list - val debug: bool ref - val pprint_context: context -> pprint_args -> unit end; structure ProofContext: PROOF_CONTEXT = @@ -179,7 +178,7 @@ consts: Consts.T * Consts.T, (*global/local consts*) assms: ((cterm list * export) list * (*assumes and views: A ==> _*) - (string * thm list) list), (*prems: A |- A*) + thm list), (*prems: A |- A*) thms: thm list NameSpace.table * FactIndex.T, (*local thms*) cases: (string * (RuleCases.T * bool)) list}; (*local contexts*) @@ -244,7 +243,7 @@ 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 = maps #2 o #2 o #assms o rep_context; +val prems_of = #2 o #assms o rep_context; val thms_of = #thms o rep_context; val fact_index_of = #2 o thms_of; @@ -960,44 +959,7 @@ (** assumptions **) -(* generic assms *) - -local - -fun gen_assm ((name, attrs), props) ctxt = - let - val cprops = map (Thm.cterm_of (theory_of ctxt)) props; - val asms = map (Goal.norm_hhf o Thm.assume) cprops; - - val ths = map (fn th => ([th], [])) asms; - val ([(_, thms)], ctxt') = - ctxt - |> auto_bind_facts props - |> note_thmss_i [((name, attrs), ths)]; - in ((cprops, (name, asms), (name, thms)), ctxt') end; - -fun gen_assms prepp exp args ctxt = - let - val (propss, ctxt1) = swap (prepp (ctxt, map snd args)); - val (results, ctxt2) = fold_map gen_assm (map fst args ~~ propss) ctxt1; - - val new_asms = maps #1 results; - val new_prems = map #2 results; - val ctxt3 = ctxt2 - |> map_assms (fn (asms, prems) => (asms @ [(new_asms, exp)], prems @ new_prems)) - val ctxt4 = ctxt3 - |> put_thms_internal (AutoBind.premsN, SOME (prems_of ctxt3)); - in (map #3 results, tap (Variable.warn_extra_tfrees ctxt) ctxt4) end; - -in - -val add_assms = gen_assms (apsnd #1 o bind_propp); -val add_assms_i = gen_assms (apsnd #1 o bind_propp_i); - -end; - - -(* basic assumptions *) +(* basic exports *) (* [A] @@ -1019,6 +981,46 @@ 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 (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; + +in + +val add_assms = gen_assms (apsnd #1 o bind_propp); +val add_assms_i = gen_assms (apsnd #1 o bind_propp_i); + +end; + + (* additional views *) fun add_view outer view = map_assms (fn (asms, prems) => @@ -1259,13 +1261,4 @@ verb single (fn () => Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts))) end; - -(* toplevel pretty printing *) - -val debug = ref false; - -fun pprint_context ctxt = Pretty.pprint - (if ! debug then Pretty.quote (Pretty.big_list "proof context:" (pretty_context ctxt)) - else Pretty.str ""); - end;