# HG changeset patch # User wenzelm # Date 916144808 -3600 # Node ID e3cdbd929a24c40cc79f71f54343fe8098f1442a # Parent 78c068b838ffe8f69ffb613ab4a8e2e89a5a352f eliminated tthm type and Attribute structure; diff -r 78c068b838ff -r e3cdbd929a24 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Tue Jan 12 13:39:41 1999 +0100 +++ b/src/Pure/Isar/attrib.ML Tue Jan 12 13:40:08 1999 +0100 @@ -21,12 +21,12 @@ val local_attribute': Proof.context -> Args.src -> Proof.context attribute val add_attributes: (bstring * ((Args.src -> theory attribute) * (Args.src -> Proof.context attribute)) * string) list -> theory -> theory - val global_thm: theory * Args.T list -> tthm * (theory * Args.T list) - val global_thms: theory * Args.T list -> tthm list * (theory * Args.T list) - val global_thmss: theory * Args.T list -> tthm list * (theory * Args.T list) - val local_thm: Proof.context * Args.T list -> tthm * (Proof.context * Args.T list) - val local_thms: Proof.context * Args.T list -> tthm list * (Proof.context * Args.T list) - val local_thmss: Proof.context * Args.T list -> tthm list * (Proof.context * Args.T list) + val global_thm: theory * Args.T list -> thm * (theory * Args.T list) + val global_thms: theory * Args.T list -> thm list * (theory * Args.T list) + val global_thmss: theory * Args.T list -> thm list * (theory * Args.T list) + val local_thm: Proof.context * Args.T list -> thm * (Proof.context * Args.T list) + val local_thms: Proof.context * Args.T list -> thm list * (Proof.context * Args.T list) + val local_thmss: Proof.context * Args.T list -> thm list * (Proof.context * Args.T list) val syntax: ('a * Args.T list -> 'a attribute * ('a * Args.T list)) -> Args.src -> 'a attribute val no_args: 'a attribute -> Args.src -> 'a attribute val setup: (theory -> theory) list @@ -127,12 +127,12 @@ Scan.depend (fn st => Args.name -- Args.opt_attribs >> (fn (name, srcs) => app ((st, get st name), map (attrib st) srcs))); -val global_thm = gen_thm PureThy.get_tthm global_attribute Attribute.apply; -val global_thms = gen_thm PureThy.get_tthms global_attribute Attribute.applys; +val global_thm = gen_thm PureThy.get_thm global_attribute Thm.apply_attributes; +val global_thms = gen_thm PureThy.get_thms global_attribute Thm.applys_attributes; val global_thmss = Scan.repeat global_thms >> flat; -val local_thm = gen_thm ProofContext.get_tthm local_attribute' Attribute.apply; -val local_thms = gen_thm ProofContext.get_tthms local_attribute' Attribute.applys; +val local_thm = gen_thm ProofContext.get_thm local_attribute' Thm.apply_attributes; +val local_thms = gen_thm ProofContext.get_thms local_attribute' Thm.applys_attributes; val local_thmss = Scan.repeat local_thms >> flat; @@ -151,13 +151,13 @@ (* tags *) -fun gen_tag x = syntax (tag >> Attribute.tag) x; -fun gen_untag x = syntax (tag >> Attribute.untag) x; +fun gen_tag x = syntax (tag >> Drule.tag) x; +fun gen_untag x = syntax (tag >> Drule.untag) x; (* transfer *) -fun gen_transfer theory_of = no_args (Attribute.rule (fn st => Thm.transfer (theory_of st))); +fun gen_transfer theory_of = no_args (Drule.rule_attribute (fn st => Thm.transfer (theory_of st))); val global_transfer = gen_transfer I; val local_transfer = gen_transfer ProofContext.theory_of; @@ -165,8 +165,7 @@ (* RS *) -fun resolve (i, B) (x, A) = - (x, Attribute.tthm_of (Attribute.thm_of A RSN (i, Attribute.thm_of B))); +fun resolve (i, B) (x, A) = (x, A RSN (i, B)); fun gen_RS thm = syntax (Scan.lift (Scan.optional Args.nat 1) -- thm >> resolve); val global_RS = gen_RS global_thm; @@ -175,8 +174,7 @@ (* APP *) -fun apply Bs (x, A) = - (x, Attribute.tthm_of (Attribute.thms_of Bs MRS Attribute.thm_of A)); +fun apply Bs (x, A) = (x, Bs MRS A); val global_APP = syntax (global_thmss >> apply); val local_APP = syntax (local_thmss >> apply); @@ -207,7 +205,7 @@ fun insts x = Scan.lift (Args.enum "and" (Args.var --| Args.$$$ "=" -- Args.name)) x; -fun gen_where context_of = syntax (insts >> (Attribute.rule o read_instantiate context_of)); +fun gen_where context_of = syntax (insts >> (Drule.rule_attribute o read_instantiate context_of)); val global_where = gen_where ProofContext.init; val local_where = gen_where I; @@ -231,7 +229,7 @@ val inst_args = Scan.repeat inst_arg; fun insts' x = Scan.lift (inst_args -- Scan.optional (concl |-- Args.!!! inst_args) []) x; -fun gen_with context_of = syntax (insts' >> (Attribute.rule o read_instantiate' context_of)); +fun gen_with context_of = syntax (insts' >> (Drule.rule_attribute o read_instantiate' context_of)); val global_with = gen_with ProofContext.init; val local_with = gen_with I; @@ -239,8 +237,8 @@ (* misc rules *) -fun standard x = no_args (Attribute.rule (K Drule.standard)) x; -fun elimify x = no_args (Attribute.rule (K Tactic.make_elim)) x; +fun standard x = no_args (Drule.rule_attribute (K Drule.standard)) x; +fun elimify x = no_args (Drule.rule_attribute (K Tactic.make_elim)) x; diff -r 78c068b838ff -r e3cdbd929a24 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Tue Jan 12 13:39:41 1999 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Tue Jan 12 13:40:08 1999 +0100 @@ -98,19 +98,19 @@ (* print theorems *) fun global_attribs thy ths srcs = - #2 (Attribute.applys ((Theory.copy thy, ths), map (Attrib.global_attribute thy) srcs)); + #2 (Thm.applys_attributes ((Theory.copy thy, ths), map (Attrib.global_attribute thy) srcs)); fun local_attribs st ths srcs = - #2 (Attribute.applys ((Proof.context_of st, ths), + #2 (Thm.applys_attributes ((Proof.context_of st, ths), map (Attrib.local_attribute (Proof.theory_of st)) srcs)); fun print_thms (name, srcs) = Toplevel.keep (fn state => let - val ths = map (apfst (Thm.transfer (Toplevel.theory_of state))) - (Toplevel.node_cases PureThy.get_tthms (ProofContext.get_tthms o Proof.context_of) + val ths = map (Thm.transfer (Toplevel.theory_of state)) + (Toplevel.node_cases PureThy.get_thms (ProofContext.get_thms o Proof.context_of) state name); val ths' = Toplevel.node_cases global_attribs local_attribs state ths srcs; - in Attribute.print_tthms ths' end); + in Display.print_thms ths' end); (* print types, terms and props *) diff -r 78c068b838ff -r e3cdbd929a24 src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Tue Jan 12 13:39:41 1999 +0100 +++ b/src/Pure/Isar/isar_thy.ML Tue Jan 12 13:40:08 1999 +0100 @@ -94,16 +94,16 @@ val have_theorems = - #1 oo gen_have_thmss PureThy.get_tthms Attrib.global_attribute PureThy.have_tthmss; + #1 oo gen_have_thmss PureThy.get_thms Attrib.global_attribute PureThy.have_thmss; val have_lemmas = - #1 oo gen_have_thmss PureThy.get_tthms Attrib.global_attribute - (fn name => fn more_atts => PureThy.have_tthmss name (more_atts @ [Attribute.tag_lemma])); + #1 oo gen_have_thmss PureThy.get_thms Attrib.global_attribute + (fn name => fn more_atts => PureThy.have_thmss name (more_atts @ [Drule.tag_lemma])); val have_thmss = - gen_have_thmss (ProofContext.get_tthms o Proof.context_of) - (Attrib.local_attribute o Proof.theory_of) Proof.have_tthmss; + gen_have_thmss (ProofContext.get_thms o Proof.context_of) + (Attrib.local_attribute o Proof.theory_of) Proof.have_thmss; val have_facts = ProofHistory.apply o have_thmss; val from_facts = ProofHistory.apply o (Proof.chain oo curry have_thmss ("", [])); @@ -143,10 +143,10 @@ val state = ProofHistory.current prf; val thy = Proof.theory_of state; val alt_atts = apsome (map (Attrib.global_attribute thy)) alt_tags; - val (thy', (kind, name, tthm)) = Method.qed alt_name alt_atts state; + val (thy', (kind, name, thm)) = Method.qed alt_name alt_atts state; val prt_result = Pretty.block - [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Attribute.pretty_tthm tthm]; + [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Display.pretty_thm thm]; in Pretty.writeln prt_result; thy end; val qed = qed_with (None, None); diff -r 78c068b838ff -r e3cdbd929a24 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Tue Jan 12 13:39:41 1999 +0100 +++ b/src/Pure/Isar/method.ML Tue Jan 12 13:40:08 1999 +0100 @@ -14,16 +14,16 @@ signature METHOD = sig include BASIC_METHOD - val LIFT: tactic -> thm -> (thm * (indexname * term) list * (string * tthm list) list) Seq.seq - val METHOD: (tthm list -> tactic) -> Proof.method + val LIFT: tactic -> thm -> (thm * (indexname * term) list * (string * thm list) list) Seq.seq + val METHOD: (thm list -> tactic) -> Proof.method val METHOD0: tactic -> Proof.method val fail: Proof.method val succeed: Proof.method val trivial: Proof.method val assumption: Proof.method val forward_chain: thm list -> thm list -> thm Seq.seq - val rule_tac: tthm list -> tthm list -> int -> tactic - val rule: tthm list -> Proof.method + val rule_tac: thm list -> thm list -> int -> tactic + val rule: thm list -> Proof.method exception METHOD_FAIL of (string * Position.T) * exn val method: theory -> Args.src -> Proof.context -> Proof.method val add_methods: (bstring * (Args.src -> Proof.context -> Proof.method) * string) list @@ -40,7 +40,7 @@ (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method val only_sectioned_args: (Args.T list -> Proof.context attribute * Args.T list) list -> (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method - val thms_args: (tthm list -> Proof.method) -> Args.src -> Proof.context -> Proof.method + val thms_args: (thm list -> Proof.method) -> Args.src -> Proof.context -> Proof.method datatype text = Basic of (Proof.context -> Proof.method) | Source of Args.src | @@ -59,7 +59,7 @@ val trivial_proof: Proof.state -> Proof.state Seq.seq val default_proof: Proof.state -> Proof.state Seq.seq val qed: bstring option -> theory attribute list option -> Proof.state - -> theory * (string * string * tthm) + -> theory * (string * string * thm) val setup: (theory -> theory) list end; @@ -86,10 +86,8 @@ fun trivial_tac [] = K all_tac | trivial_tac facts = - let - val thms = Attribute.thms_of facts; - val r = ~ (length facts); - in metacuts_tac thms THEN' rotate_tac r end; + let val r = ~ (length facts); + in metacuts_tac facts THEN' rotate_tac r end; val trivial = METHOD (ALLGOALS o trivial_tac); val assumption = METHOD (fn facts => FIRSTGOAL (trivial_tac facts THEN' assume_tac)); @@ -109,10 +107,10 @@ fun forward_chain facts rules = Seq.flat (Seq.map (multi_resolve facts) (Seq.of_list rules)); -fun rule_tac rules [] = resolve_tac (Attribute.thms_of rules) +fun rule_tac rules [] = resolve_tac rules | rule_tac erules facts = let - val rules = forward_chain (Attribute.thms_of facts) (Attribute.thms_of erules); + val rules = forward_chain facts erules; fun tac i state = Seq.flat (Seq.map (fn rule => Tactic.rtac rule i state) rules); in tac end; @@ -209,7 +207,7 @@ fun thms ss = Scan.unless (sect ss) Attrib.local_thms; fun thmss ss = Scan.repeat (thms ss) >> flat; -fun apply att (ctxt, ths) = Attribute.applys ((ctxt, ths), [att]); +fun apply att (ctxt, ths) = Thm.applys_attributes ((ctxt, ths), [att]); fun section ss = (sect ss -- thmss ss) :-- (fn (att, ths) => Scan.depend (fn ctxt => Scan.succeed (apply att (ctxt, ths)))) >> #2; diff -r 78c068b838ff -r e3cdbd929a24 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Tue Jan 12 13:39:41 1999 +0100 +++ b/src/Pure/Isar/proof.ML Tue Jan 12 13:40:08 1999 +0100 @@ -22,23 +22,23 @@ val context_of: state -> context val theory_of: state -> theory val sign_of: state -> Sign.sg - val the_facts: state -> tthm list - val goal_facts: (state -> tthm list) -> state -> state + val the_facts: state -> thm list + val goal_facts: (state -> thm list) -> state -> state val use_facts: state -> state val reset_facts: state -> state val assert_backward: state -> state val enter_forward: state -> state val print_state: state -> unit type method - val method: (tthm list -> thm -> - (thm * (indexname * term) list * (string * tthm list) list) Seq.seq) -> method + val method: (thm list -> thm -> + (thm * (indexname * term) list * (string * thm list) list) Seq.seq) -> method val refine: (context -> method) -> state -> state Seq.seq val bind: (indexname * string) list -> state -> state val bind_i: (indexname * term) list -> state -> state val match_bind: (string list * string) list -> state -> state val match_bind_i: (term list * term) list -> state -> state - val have_tthmss: string -> context attribute list -> - (tthm list * context attribute list) list -> state -> state + val have_thmss: string -> context attribute list -> + (thm list * context attribute list) list -> state -> state val assume: string -> context attribute list -> (string * string list) list -> state -> state val assume_i: string -> context attribute list -> (term * term list) list -> state -> state val fix: (string * string option) list -> state -> state @@ -48,7 +48,7 @@ val lemma: bstring -> theory attribute list -> string * string list -> theory -> state val lemma_i: bstring -> theory attribute list -> term * term list -> theory -> state val chain: state -> state - val from_facts: tthm list -> state -> state + val from_facts: thm list -> state -> state val show: string -> context attribute list -> string * string list -> state -> state val show_i: string -> context attribute list -> term * term list -> state -> state val have: string -> context attribute list -> string * string list -> state -> state @@ -57,7 +57,7 @@ val next_block: state -> state val end_block: (context -> method) -> state -> state Seq.seq val qed: (context -> method) -> bstring option -> theory attribute list option -> state - -> theory * (string * string * tthm) + -> theory * (string * string * thm) end; signature PROOF_PRIVATE = @@ -87,11 +87,11 @@ fn Theorem _ => "theorem" | Lemma _ => "lemma" | Goal _ => "show" | Aux _ => "have"; type goal = - (kind * (*result kind*) + (kind * (*result kind*) string * (*result name*) cterm list * (*result assumptions*) term) * (*result statement*) - (tthm list * (*use facts*) + (thm list * (*use facts*) thm); (*goal: subgoals ==> statement*) @@ -107,7 +107,7 @@ type node = {context: context, - facts: tthm list option, + facts: thm list option, mode: mode, goal: goal option}; @@ -154,8 +154,8 @@ fun put_data kind f = map_context o ProofContext.put_data kind f; val declare_term = map_context o ProofContext.declare_term; val add_binds = map_context o ProofContext.add_binds_i; -val put_tthms = map_context o ProofContext.put_tthms; -val put_tthmss = map_context o ProofContext.put_tthmss; +val put_thms = map_context o ProofContext.put_thms; +val put_thmss = map_context o ProofContext.put_thmss; (* bind statements *) @@ -164,19 +164,19 @@ let val mk_bind = map (fn (x, t) => ((Syntax.binding x, 0), t)) o ObjectLogic.dest_statement in state |> add_binds (flat (map mk_bind bs)) end; -fun bind_tthms (name, tthms) state = +fun bind_thms (name, thms) state = let - val props = map (#prop o Thm.rep_thm o Attribute.thm_of) tthms; + val props = map (#prop o Thm.rep_thm) thms; val named_props = (case props of [prop] => [(name, prop)] | props => map2 (fn (i, t) => (name ^ string_of_int i, t)) (1 upto length props, props)); in state |> bind_props named_props end; -fun let_tthms name_tthms state = +fun let_thms name_thms state = state - |> put_tthms name_tthms - |> bind_tthms name_tthms; + |> put_thms name_thms + |> bind_thms name_thms; (* facts *) @@ -187,14 +187,14 @@ fun put_facts facts state = state |> map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) - |> let_tthms ("facts", if_none facts []); + |> let_thms ("facts", if_none facts []); val reset_facts = put_facts None; fun have_facts (name, facts) state = state |> put_facts (Some facts) - |> let_tthms (name, facts); + |> let_thms (name, facts); fun these_facts (state, ths) = have_facts ths state; fun fetch_facts (State ({facts, ...}, _)) = put_facts facts; @@ -266,20 +266,19 @@ fun print_state (state as State ({context, facts, mode, goal = _}, nodes)) = let val ref (_, _, begin_goal) = Goals.current_goals_markers; - val prt_tthm = Attribute.pretty_tthm; fun print_facts None = () | print_facts (Some ths) = - Pretty.writeln (Pretty.big_list "Current facts:" (map prt_tthm ths)); + Pretty.writeln (Pretty.big_list "Current facts:" (map Display.pretty_thm ths)); fun levels_up 0 = "" | levels_up i = " (" ^ string_of_int i ^ " levels up)"; fun print_goal (i, ((kind, name, _, _), (_, thm))) = - (writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 1) ^ ":"); (* FIXME *) + (writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 1) ^ ":"); (* FIXME *) Locale.print_goals_marker begin_goal (! goals_limit) thm); in - writeln ("Nesting level: " ^ string_of_int (length nodes div 1)); (* FIXME *) + writeln ("Nesting level: " ^ string_of_int (length nodes div 1)); (* FIXME *) writeln ""; writeln (mode_name mode ^ " mode"); writeln ""; @@ -296,11 +295,11 @@ (* datatype method *) datatype method = Method of - tthm list -> (*use facts*) + thm list -> (*use facts*) thm (*goal: subgoals ==> statement*) -> (thm * (*refined goal*) (indexname * term) list * (*new bindings*) - (string * tthm list) list) (*new thms*) + (string * thm list) list) (*new thms*) Seq.seq; val method = Method; @@ -322,7 +321,7 @@ |> check_sign (sign_of_thm thm') |> map_goal (K (result, (facts, thm'))) |> add_binds new_binds - |> put_tthmss new_thms; + |> put_thmss new_thms; in Seq.map refn (meth facts thm) end; @@ -429,12 +428,12 @@ val match_bind_i = gen_bind ProofContext.match_binds_i; -(* have_tthmss *) +(* have_thmss *) -fun have_tthmss name atts ths_atts state = +fun have_thmss name atts ths_atts state = state |> assert_forward - |> map_context_result (ProofContext.have_tthmss (PureThy.default_name name) atts ths_atts) + |> map_context_result (ProofContext.have_thmss (PureThy.default_name name) atts ths_atts) |> these_facts; @@ -457,7 +456,7 @@ |> assert_forward |> map_context_result (f (PureThy.default_name name) atts props) |> these_facts - |> (fn st => let_tthms ("prems", ProofContext.assumptions (context_of st)) st); + |> (fn st => let_thms ("prems", ProofContext.assumptions (context_of st)) st); val assume = gen_assume ProofContext.assume; val assume_i = gen_assume ProofContext.assume_i; @@ -490,8 +489,7 @@ |> opt_block |> map_context_result (fn c => prepp (c, raw_propp)); - val casms = map (#prop o Thm.crep_thm o Attribute.thm_of) - (ProofContext.assumptions (context_of state')); + val casms = map (#prop o Thm.crep_thm) (ProofContext.assumptions (context_of state')); val asms = map Thm.term_of casms; val prop = Logic.list_implies (asms, concl); @@ -597,7 +595,7 @@ in state |> close_block - |> have_tthmss name atts [([(result, [])], [])] + |> have_thmss name atts [Thm.no_attributes [result]] |> opt_solve end; @@ -626,10 +624,10 @@ val atts = (case kind of Theorem atts => if_none alt_atts atts - | Lemma atts => (if_none alt_atts atts) @ [Attribute.tag_lemma] + | Lemma atts => (if_none alt_atts atts) @ [Drule.tag_lemma] | _ => raise STATE ("No global goal!", state)); - val (thy', result') = PureThy.store_tthm ((name, (result, [])), atts) (theory_of state); + val (thy', result') = PureThy.store_thm ((name, result), atts) (theory_of state); in (thy', (kind_name kind, name, result')) end; fun qed meth_fun alt_name alt_atts state = diff -r 78c068b838ff -r e3cdbd929a24 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Jan 12 13:39:41 1999 +0100 +++ b/src/Pure/Isar/proof_context.ML Tue Jan 12 13:40:08 1999 +0100 @@ -41,21 +41,21 @@ val match_binds_i: (term list * term) list -> context -> context val bind_propp: context * (string * string list) -> context * term val bind_propp_i: context * (term * term list) -> context * term - val thms_closure: context -> xstring -> tthm list option - val get_tthm: context -> string -> tthm - val get_tthms: context -> string -> tthm list - val get_tthmss: context -> string list -> tthm list - val put_tthm: string * tthm -> context -> context - val put_tthms: string * tthm list -> context -> context - val put_tthmss: (string * tthm list) list -> context -> context - val have_tthmss: string -> context attribute list - -> (tthm list * context attribute list) list -> context -> context * (string * tthm list) - val assumptions: context -> tthm list + val thms_closure: context -> xstring -> thm list option + val get_thm: context -> string -> thm + val get_thms: context -> string -> thm list + val get_thmss: context -> string list -> thm list + val put_thm: string * thm -> context -> context + val put_thms: string * thm list -> context -> context + val put_thmss: (string * thm list) list -> context -> context + val have_thmss: string -> context attribute list + -> (thm list * context attribute list) list -> context -> context * (string * thm list) + val assumptions: context -> thm list val fixed_names: context -> string list val assume: string -> context attribute list -> (string * string list) list -> context - -> context * (string * tthm list) + -> context * (string * thm list) val assume_i: string -> context attribute list -> (term * term list) list -> context - -> context * (string * tthm list) + -> context * (string * thm list) val fix: (string * string option) list -> context -> context val fix_i: (string * typ) list -> context -> context val setup: (theory -> theory) list @@ -82,10 +82,10 @@ {thy: theory, (*current theory*) data: Object.T Symtab.table, (*user data*) asms: - (string * tthm list) list * (*assumes: A ==> _*) + (string * thm list) list * (*assumes: A ==> _*) ((string * string) list * string list), (*fixes: !!x. _*) binds: (term * typ) Vartab.table, (*term bindings*) - thms: tthm list Symtab.table, (*local thms*) + thms: thm list Symtab.table, (*local thms*) defs: typ Vartab.table * (*type constraints*) sort Vartab.table * (*default sorts*) @@ -136,7 +136,7 @@ (* local theorems *) fun print_thms (Context {thms, ...}) = - print_items Attribute.pretty_tthm "Local theorems:" (Symtab.dest thms); + print_items Display.pretty_thm "Local theorems:" (Symtab.dest thms); (* main context *) @@ -146,7 +146,6 @@ let val sign = Theory.sign_of thy; - val term_of_tthm = #prop o Thm.rep_thm o Attribute.thm_of; val prt_term = Sign.pretty_term sign; val prt_typ = Sign.pretty_typ sign; val prt_sort = Sign.pretty_sort sign; @@ -173,7 +172,7 @@ in debug Pretty.writeln pretty_thy; Pretty.writeln (Pretty.big_list "Fixed variables:" (map prt_fix (rev fixes))); - print_items (prt_term o term_of_tthm) "Assumptions:" assumes; + print_items (prt_term o #prop o Thm.rep_thm) "Assumptions:" assumes; debug print_binds ctxt; debug print_thms ctxt; debug Pretty.writeln (Pretty.big_list "Type constraints:" (map prt_defT (Vartab.dest types))); @@ -550,44 +549,44 @@ in get end; -(* get_tthm(s) *) +(* get_thm(s) *) -fun get_tthm (ctxt as Context {thy, thms, ...}) name = +fun get_thm (ctxt as Context {thy, thms, ...}) name = (case Symtab.lookup (thms, name) of Some [th] => th | Some _ => raise CONTEXT ("Single theorem expected: " ^ quote name, ctxt) - | None => (PureThy.get_tthm thy name handle THEORY (msg, _) => raise CONTEXT (msg, ctxt))); + | None => (PureThy.get_thm thy name handle THEORY (msg, _) => raise CONTEXT (msg, ctxt))); -fun get_tthms (ctxt as Context {thy, thms, ...}) name = +fun get_thms (ctxt as Context {thy, thms, ...}) name = (case Symtab.lookup (thms, name) of Some ths => ths - | None => (PureThy.get_tthms thy name handle THEORY (msg, _) => raise CONTEXT (msg, ctxt))); + | None => (PureThy.get_thms thy name handle THEORY (msg, _) => raise CONTEXT (msg, ctxt))); -fun get_tthmss ctxt names = flat (map (get_tthms ctxt) names); +fun get_thmss ctxt names = flat (map (get_thms ctxt) names); -(* put_tthm(s) *) +(* put_thm(s) *) -fun put_tthms (name, ths) = map_context +fun put_thms (name, ths) = map_context (fn (thy, data, asms, binds, thms, defs) => (thy, data, asms, binds, Symtab.update ((name, ths), thms), defs)); -fun put_tthm (name, th) = put_tthms (name, [th]); +fun put_thm (name, th) = put_thms (name, [th]); -fun put_tthmss [] ctxt = ctxt - | put_tthmss (th :: ths) ctxt = ctxt |> put_tthms th |> put_tthmss ths; +fun put_thmss [] ctxt = ctxt + | put_thmss (th :: ths) ctxt = ctxt |> put_thms th |> put_thmss ths; -(* have_tthmss *) +(* have_thmss *) -fun have_tthmss name more_attrs ths_attrs ctxt = +fun have_thmss name more_attrs ths_attrs ctxt = let fun app ((ct, ths), (th, attrs)) = - let val (ct', th') = Attribute.applys ((ct, th), attrs @ more_attrs) + let val (ct', th') = Thm.applys_attributes ((ct, th), attrs @ more_attrs) in (ct', th' :: ths) end val (ctxt', rev_thms) = foldl app ((ctxt, []), ths_attrs); val thms = flat (rev rev_thms); - in (ctxt' |> put_tthms (name, thms), (name, thms)) end; + in (ctxt' |> put_thms (name, thms), (name, thms)) end; @@ -606,18 +605,18 @@ val (ctxt', props) = foldl_map prepp (ctxt, raw_prop_pats); val sign = sign_of ctxt'; - val asms = map (Attribute.tthm_of o Thm.assume o Thm.cterm_of sign) props; + val asms = map (Thm.assume o Thm.cterm_of sign) props; val ths = map (fn th => ([th], [])) asms; - val (ctxt'', (_, tthms)) = + val (ctxt'', (_, thms)) = ctxt' - |> have_tthmss name (attrs @ [Attribute.tag_assumption]) ths + |> have_thmss name (attrs @ [Drule.tag_assumption]) ths; val ctxt''' = ctxt'' |> map_context (fn (thy, data, (assumes, fixes), binds, thms, defs) => (thy, data, (assumes @ [(name, asms)], fixes), binds, thms, defs)); - in (ctxt''', (name, tthms)) end; + in (ctxt''', (name, thms)) end; val assume = gen_assume bind_propp; val assume_i = gen_assume bind_propp_i; diff -r 78c068b838ff -r e3cdbd929a24 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Tue Jan 12 13:39:41 1999 +0100 +++ b/src/Pure/pure_thy.ML Tue Jan 12 13:40:08 1999 +0100 @@ -23,18 +23,16 @@ signature PURE_THY = sig include BASIC_PURE_THY - val thms_closure: theory -> xstring -> tthm list option - val get_tthm: theory -> xstring -> tthm - val get_tthms: theory -> xstring -> tthm list - val get_tthmss: theory -> xstring list -> tthm list + val thms_closure: theory -> xstring -> thm list option + val get_thmss: theory -> xstring list -> thm list val thms_containing: theory -> string list -> (string * thm) list val default_name: string -> string - val store_tthm: (bstring * tthm) * theory attribute list -> theory -> theory * tthm + val store_thm: (bstring * thm) * theory attribute list -> theory -> theory * thm val smart_store_thm: (bstring * thm) -> thm - val add_tthms: ((bstring * tthm) * theory attribute list) list -> theory -> theory - val add_tthmss: ((bstring * tthm list) * theory attribute list) list -> theory -> theory - val have_tthmss: bstring -> theory attribute list -> - (tthm list * theory attribute list) list -> theory -> theory * tthm list + val add_thms: ((bstring * thm) * theory attribute list) list -> theory -> theory + val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory -> theory + val have_thmss: bstring -> theory attribute list -> + (thm list * theory attribute list) list -> theory -> theory * thm list val add_axioms: ((bstring * string) * theory attribute list) list -> theory -> theory val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory val add_axiomss: ((bstring * string list) * theory attribute list) list -> theory -> theory @@ -68,8 +66,8 @@ type T = {space: NameSpace.T, - thms_tab: tthm list Symtab.table, - const_idx: int * (int * tthm) list Symtab.table} ref; + thms_tab: thm list Symtab.table, + const_idx: int * (int * thm) list Symtab.table} ref; fun mk_empty _ = ref {space = NameSpace.empty, thms_tab = Symtab.empty, const_idx = (0, Symtab.empty)} : T; @@ -80,7 +78,7 @@ fun print sg (ref {space, thms_tab, const_idx = _}) = let - val prt_thm = Attribute.pretty_tthm o apfst (Thm.transfer_sg sg); + val prt_thm = Display.pretty_thm o Thm.transfer_sg sg; fun prt_thms (name, [th]) = Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt_thm th] | prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths); @@ -125,25 +123,22 @@ fun lookup_thms name thy = thms_closure_aux thy name; -fun get_tthms thy name = +fun get_thms thy name = (case get_first (lookup_thms name) (thy :: Theory.ancestors_of thy) of None => raise THEORY ("Unknown theorem(s) " ^ quote name, [thy]) | Some thms => thms); -fun get_tthm thy name = - (case get_tthms thy name of +fun get_thm thy name = + (case get_thms thy name of [thm] => thm | _ => raise THEORY ("Single theorem expected " ^ quote name, [thy])); -fun get_tthmss thy names = flat (map (get_tthms thy) names); - -fun get_thms thy = Attribute.thms_of o get_tthms thy; -fun get_thm thy = Attribute.thm_of o get_tthm thy; +fun get_thmss thy names = flat (map (get_thms thy) names); (* thms_of *) -fun attach_name (thm, _) = (Thm.name_of_thm thm, thm); +fun attach_name thm = (Thm.name_of_thm thm, thm); fun thms_of thy = let val ref {thms_tab, ...} = get_theorems thy in @@ -158,14 +153,14 @@ val ignore = ["Trueprop", "all", "==>", "=="]; -fun add_const_idx ((next, table), tthm as (thm, _)) = +fun add_const_idx ((next, table), thm) = let val {hyps, prop, ...} = Thm.rep_thm thm; val consts = foldr add_term_consts (hyps, add_term_consts (prop, [])) \\ ignore; fun add (tab, c) = - Symtab.update ((c, (next, tthm) :: Symtab.lookup_multi (tab, c)), tab); + Symtab.update ((c, (next, thm) :: Symtab.lookup_multi (tab, c)), tab); in (next + 1, foldl add (table, consts)) end; fun make_const_idx thm_tab = @@ -214,7 +209,7 @@ fun name_multi name xs = gen_names (length xs) (default_name name) ~~ xs; -(* enter_tthmx *) +(* enter_thmx *) fun cond_warning name msg = if Sign.base_name name = defaultN then () else warning msg; @@ -224,72 +219,68 @@ fun warn_same name = cond_warning name ("Theorem database already contains a copy of " ^ quote name); -fun enter_tthmx sg app_name (bname, tthmx) = +fun enter_thmx sg app_name (bname, thmx) = let val name = Sign.full_name sg bname; - fun name_tthm (nm, (thm, tgs)) = (Thm.name_thm (nm, thm), tgs); - val named_tthms = map name_tthm (app_name name tthmx); - - fun eq_tthm ((th1, _), (th2, _)) = Thm.eq_thm (th1, th2); + val named_thms = map Thm.name_thm (app_name name thmx); val r as ref {space, thms_tab, const_idx} = get_theorems_sg sg; val overwrite = (case Symtab.lookup (thms_tab, name) of None => false - | Some tthms' => - if length tthms' = length named_tthms andalso forall2 eq_tthm (tthms', named_tthms) then + | Some thms' => + if length thms' = length named_thms andalso forall2 Thm.eq_thm (thms', named_thms) then (warn_same name; false) else (warn_overwrite name; true)); val space' = NameSpace.extend (space, [name]); - val thms_tab' = Symtab.update ((name, named_tthms), thms_tab); + val thms_tab' = Symtab.update ((name, named_thms), thms_tab); val const_idx' = if overwrite then make_const_idx thms_tab' - else foldl add_const_idx (const_idx, named_tthms); + else foldl add_const_idx (const_idx, named_thms); in r := {space = space', thms_tab = thms_tab', const_idx = const_idx'}; - named_tthms + named_thms end; -(* add_tthms(s) *) +(* add_thms(s) *) -fun add_tthmx app_name app_att ((bname, tthmx), atts) thy = +fun add_thmx app_name app_att ((bname, thmx), atts) thy = let - val (thy', tthmx') = app_att ((thy, tthmx), atts); - val tthms'' = enter_tthmx (Theory.sign_of thy') app_name (bname, tthmx'); - in (thy', tthms'') end; + val (thy', thmx') = app_att ((thy, thmx), atts); + val thms'' = enter_thmx (Theory.sign_of thy') app_name (bname, thmx'); + in (thy', thms'') end; -fun add_tthmxs name app = Library.apply o map (fst oo add_tthmx name app); +fun add_thmxs name app = Library.apply o map (fst oo add_thmx name app); -val add_tthms = add_tthmxs name_single Attribute.apply; -val add_tthmss = add_tthmxs name_multi Attribute.applys; +val add_thms = add_thmxs name_single Thm.apply_attributes; +val add_thmss = add_thmxs name_multi Thm.applys_attributes; -(* have_tthmss *) +(* have_thmss *) -fun have_tthmss bname more_atts ths_atts thy = +fun have_thmss bname more_atts ths_atts thy = let - fun app (x, (ths, atts)) = Attribute.applys ((x, ths), atts); - val (thy', tthmss') = + fun app (x, (ths, atts)) = Thm.applys_attributes ((x, ths), atts); + val (thy', thmss') = foldl_map app (thy, map (fn (ths, atts) => (ths, atts @ more_atts)) ths_atts); - val tthms'' = enter_tthmx (Theory.sign_of thy') name_multi (bname, flat tthmss'); - in (thy, tthms'') end; + val thms'' = enter_thmx (Theory.sign_of thy') name_multi (bname, flat thmss'); + in (thy, thms'') end; -(* store_tthm *) +(* store_thm *) -fun store_tthm th_atts thy = - let val (thy', [th']) = add_tthmx name_single Attribute.apply th_atts thy +fun store_thm th_atts thy = + let val (thy', [th']) = add_thmx name_single Thm.apply_attributes th_atts thy in (thy', th') end; (* smart_store_thm *) fun smart_store_thm (name, thm) = - let val [(thm', _)] = enter_tthmx (Thm.sign_of_thm thm) name_single (name, Attribute.tthm_of thm) - in thm' end; + hd (enter_thmx (Thm.sign_of_thm thm) name_single (name, thm)); (* store axioms as theorems *) @@ -299,8 +290,8 @@ let val named_axs = app_name name axs; val thy' = add named_axs thy; - val tthms = map (Attribute.tthm_of o Thm.get_axiom thy' o fst) named_axs; - in add_tthmss [((name, tthms), atts)] thy' end; + val thms = map (Thm.get_axiom thy' o fst) named_axs; + in add_thmss [((name, thms), atts)] thy' end; fun add_axs app_name add = Library.apply o map (add_ax app_name add); in @@ -441,7 +432,7 @@ |> Theory.add_modesyntax ("", false) [("Goal", "prop => prop", Mixfix ("_", [0], 0))] |> local_path - |> (add_defs o map Attribute.none) + |> (add_defs o map Thm.no_attributes) [("flexpair_def", "(t =?= u) == (t == u::'a::{})"), ("Goal_def", "GOAL (PROP A) == PROP A")] |> end_theory;