--- 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;
--- 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 *)
--- 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);
--- 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;
--- 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 =
--- 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;
--- 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;