--- a/src/HOL/IsaMakefile Fri Jan 16 13:07:44 2009 -0800
+++ b/src/HOL/IsaMakefile Sat Jan 17 10:40:03 2009 -0800
@@ -112,7 +112,7 @@
$(SRC)/Provers/splitter.ML \
$(OUT)/HOL-Base: base.ML $(BASE_DEPENDENCIES)
- @$(ISABELLE_TOOL) usedir -b -f base.ML -g true $(OUT)/Pure HOL-Base
+ @$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base
PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES)\
Datatype.thy \
--- a/src/HOL/Tools/lin_arith.ML Fri Jan 16 13:07:44 2009 -0800
+++ b/src/HOL/Tools/lin_arith.ML Sat Jan 17 10:40:03 2009 -0800
@@ -340,7 +340,7 @@
fun subst_term ([] : (term * term) list) (t : term) = t
| subst_term pairs t =
- (case AList.lookup (op aconv) pairs t of
+ (case AList.lookup Pattern.aeconv pairs t of
SOME new =>
new
| NONE =>
@@ -682,7 +682,7 @@
fun negated_term_occurs_positively (terms : term list) : bool =
List.exists
- (fn (Trueprop $ (Const ("Not", _) $ t)) => member (op aconv) terms (Trueprop $ t)
+ (fn (Trueprop $ (Const ("Not", _) $ t)) => member Pattern.aeconv terms (Trueprop $ t)
| _ => false)
terms;
--- a/src/Pure/General/markup.ML Fri Jan 16 13:07:44 2009 -0800
+++ b/src/Pure/General/markup.ML Sat Jan 17 10:40:03 2009 -0800
@@ -95,17 +95,7 @@
val editN: string val edit: string -> string -> T
val pidN: string
val sessionN: string
- val classN: string
- val messageN: string val message: string -> T
val promptN: string val prompt: T
- val writelnN: string
- val priorityN: string
- val tracingN: string
- val warningN: string
- val errorN: string
- val debugN: string
- val initN: string
- val statusN: string
val no_output: output * output
val default_output: T -> output * output
val add_mode: string -> (T -> output * output) -> unit
@@ -284,19 +274,8 @@
val pidN = "pid";
val sessionN = "session";
-val classN = "class";
-val (messageN, message) = markup_string "message" classN;
-
val (promptN, prompt) = markup_elem "prompt";
-val writelnN = "writeln";
-val priorityN = "priority";
-val tracingN = "tracing";
-val warningN = "warning";
-val errorN = "error";
-val debugN = "debug";
-val initN = "init";
-val statusN = "status";
(* print mode operations *)
--- a/src/Pure/General/markup.scala Fri Jan 16 13:07:44 2009 -0800
+++ b/src/Pure/General/markup.scala Sat Jan 17 10:40:03 2009 -0800
@@ -131,6 +131,21 @@
val SESSION = "session"
val MESSAGE = "message"
+ val CLASS = "class"
+
+ val INIT = "init"
+ val STATUS = "status"
+ val WRITELN = "writeln"
+ val PRIORITY = "priority"
+ val TRACING = "tracing"
+ val WARNING = "warning"
+ val ERROR = "error"
+ val DEBUG = "debug"
+ val SYSTEM = "system"
+ val STDIN = "stdin"
+ val STDOUT = "stdout"
+ val SIGNAL = "signal"
+ val EXIT = "exit"
/* content */
--- a/src/Pure/General/yxml.scala Fri Jan 16 13:07:44 2009 -0800
+++ b/src/Pure/General/yxml.scala Sat Jan 17 10:40:03 2009 -0800
@@ -109,12 +109,21 @@
case _ => err("multiple results")
}
+
+ /* failsafe parsing */
+
+ private def markup_failsafe(source: CharSequence) =
+ XML.Elem (Markup.BAD, Nil,
+ List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
+
+ def parse_body_failsafe(source: CharSequence) = {
+ try { parse_body(source) }
+ catch { case _: RuntimeException => List(markup_failsafe(source)) }
+ }
+
def parse_failsafe(source: CharSequence) = {
try { parse(source) }
- catch {
- case _: RuntimeException => XML.Elem (Markup.BAD, Nil,
- List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
- }
+ catch { case _: RuntimeException => markup_failsafe(source) }
}
}
--- a/src/Pure/Isar/class.ML Fri Jan 16 13:07:44 2009 -0800
+++ b/src/Pure/Isar/class.ML Sat Jan 17 10:40:03 2009 -0800
@@ -45,7 +45,7 @@
|> SOME
end;
-fun raw_morphism thy class sups param_map some_axiom =
+fun calculate_morphism thy class sups param_map some_axiom =
let
val ctxt = ProofContext.init thy;
val (([props], [(_, morph1)], export_morph), _) = ctxt
@@ -58,9 +58,8 @@
$> Element.satisfy_morphism [(Element.prove_witness ctxt prop
(ALLGOALS (ProofContext.fact_tac (the_list some_axiom))))]
| [] => morph2;
- (*FIXME generic amend operation for classes*)
- val morph4 = morph3 $> eq_morph thy (these_defs thy sups);
- in (morph4, export_morph) end;
+ val morph4 = morph3 $> Element.eq_morphism thy (these_defs thy sups);
+ in (morph3, morph4, export_morph) end;
fun calculate_rules thy morph sups base_sort param_map axiom class =
let
@@ -96,13 +95,6 @@
|> Thm.close_derivation;
in (assm_intro, of_class) end;
-fun note_assm_intro class assm_intro thy =
- thy
- |> Sign.sticky_prefix (class_prefix class ^ "_" ^ AxClass.axiomsN)
- |> PureThy.store_thm (AxClass.introN, assm_intro)
- |> snd
- |> Sign.restore_naming thy;
-
(** define classes **)
@@ -110,6 +102,7 @@
fun gen_class_spec prep_class process_decl thy raw_supclasses raw_elems =
let
+ (*FIXME 2009 simplify*)
val supclasses = map (prep_class thy) raw_supclasses;
val supsort = Sign.minimize_sort thy supclasses;
val sups = filter (is_class thy) supsort;
@@ -127,7 +120,7 @@
sups, []);
val constrain = Element.Constrains ((map o apsnd o map_atyps)
(K (TFree (Name.aT, base_sort))) supparams);
- (*FIXME perhaps better: control type variable by explicit
+ (*FIXME 2009 perhaps better: control type variable by explicit
parameter instantiation of import expression*)
val begin_ctxt = begin sups base_sort
#> fold (Variable.declare_constraints o Free) ((map o apsnd o map_atyps)
@@ -148,6 +141,7 @@
fun add_consts bname class base_sort sups supparams global_syntax thy =
let
+ (*FIXME 2009 simplify*)
val supconsts = supparams
|> AList.make (snd o the o AList.lookup (op =) (these_params thy sups))
|> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]);
@@ -177,6 +171,7 @@
fun adjungate_axclass bname class base_sort sups supsort supparams global_syntax thy =
let
+ (*FIXME 2009 simplify*)
fun globalize param_map = map_aterms
(fn Free (v, ty) => Const ((fst o the o AList.lookup (op =) param_map) v, ty)
| t => t);
@@ -191,12 +186,12 @@
|> add_consts bname class base_sort sups supparams global_syntax
|-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
(map (fst o snd) params)
- [(((*Binding.name (bname ^ "_" ^ AxClass.axiomsN*) Binding.empty, []),
+ [((Binding.empty, []),
Option.map (globalize param_map) raw_pred |> the_list)]
#> snd
#> `get_axiom
#-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params
- #> pair (map (Const o snd) param_map, param_map, params, assm_axiom)))
+ #> pair (param_map, params, assm_axiom)))
end;
fun gen_class prep_spec bname raw_supclasses raw_elems thy =
@@ -204,32 +199,20 @@
val class = Sign.full_bname thy bname;
val (((sups, supparams), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
prep_spec thy raw_supclasses raw_elems;
- (*val export_morph = (*FIXME how canonical is this?*)
- Morphism.morphism { binding = I, var = I,
- typ = Logic.varifyT,
- term = (*map_types Logic.varifyT*) I,
- fact = map Thm.varifyT
- } $> Morphism.morphism { binding = I, var = I,
- typ = Logic.type_map TermSubst.zero_var_indexes,
- term = TermSubst.zero_var_indexes,
- fact = Drule.zero_var_indexes_list o map Thm.strip_shyps
- };*)
in
thy
|> Expression.add_locale bname "" supexpr elems
|> snd |> LocalTheory.exit_global
|> adjungate_axclass bname class base_sort sups supsort supparams global_syntax
- |-> (fn (inst, param_map, params, assm_axiom) =>
+ |-> (fn (param_map, params, assm_axiom) =>
`(fn thy => calculate_axiom thy sups base_sort assm_axiom param_map class)
#-> (fn axiom =>
- `(fn thy => raw_morphism thy class sups param_map axiom)
- #-> (fn (morph, export_morph) => Locale.add_registration (class, (morph, export_morph))
+ `(fn thy => calculate_morphism thy class sups param_map axiom)
+ #-> (fn (raw_morph, morph, export_morph) => Locale.add_registration (class, (morph, export_morph))
#> Locale.activate_global_facts (class, morph $> export_morph)
#> `(fn thy => calculate_rules thy morph sups base_sort param_map axiom class)
#-> (fn (assm_intro, of_class) =>
- register class sups params base_sort inst
- morph axiom assm_intro of_class
- (*#> fold (note_assm_intro class) (the_list assm_intro*)))))
+ register class sups params base_sort raw_morph axiom assm_intro of_class))))
|> TheoryTarget.init (SOME class)
|> pair class
end;
@@ -246,12 +229,6 @@
local
-fun prove_sublocale tac (sub, expr) =
- Expression.sublocale sub expr
- #> Proof.global_terminal_proof
- (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
- #> ProofContext.theory_of;
-
fun gen_subclass prep_class do_proof raw_sup lthy =
let
val thy = ProofContext.theory_of lthy;
@@ -259,6 +236,7 @@
val sub = case TheoryTarget.peek lthy
of {is_class = false, ...} => error "Not a class context"
| {target, ...} => target;
+
val _ = if Sign.subsort thy ([sup], [sub])
then error ("Class " ^ Syntax.string_of_sort lthy [sup]
^ " is subclass of class " ^ Syntax.string_of_sort lthy [sub])
@@ -273,15 +251,21 @@
val expr = ([(sup, (("", false), Expression.Positional []))], []);
val (([props], _, _), goal_ctxt) =
Expression.cert_goal_expression expr lthy;
- val some_prop = try the_single props; (*FIXME*)
+ val some_prop = try the_single props;
+
+ fun tac some_thm = ALLGOALS (ProofContext.fact_tac (the_list some_thm));
+ fun prove_sublocale some_thm =
+ Expression.sublocale sub expr
+ #> Proof.global_terminal_proof
+ (Method.Basic (K (Method.SIMPLE_METHOD (tac some_thm)), Position.none), NONE)
+ #> ProofContext.theory_of;
fun after_qed some_thm =
LocalTheory.theory (register_subclass (sub, sup) some_thm)
- #> is_some some_thm ? LocalTheory.theory
- (prove_sublocale (ALLGOALS (ProofContext.fact_tac (the_list some_thm))) (sub, expr))
- #> (TheoryTarget.init (SOME sub) o ProofContext.theory_of);
- in
- do_proof after_qed some_prop lthy
- end;
+ #> is_some some_thm ? LocalTheory.theory (prove_sublocale some_thm)
+ (*FIXME should also go to register_subclass*)
+ #> ProofContext.theory_of
+ #> TheoryTarget.init (SOME sub);
+ in do_proof after_qed some_prop lthy end;
fun user_proof after_qed NONE =
Proof.theorem_i NONE (K (after_qed NONE)) [[]]
--- a/src/Pure/Isar/class_target.ML Fri Jan 16 13:07:44 2009 -0800
+++ b/src/Pure/Isar/class_target.ML Sat Jan 17 10:40:03 2009 -0800
@@ -8,31 +8,27 @@
sig
(*classes*)
val register: class -> class list -> ((string * typ) * (string * typ)) list
- -> sort -> term list -> morphism
- -> thm option -> thm option -> thm -> theory -> theory
+ -> sort -> morphism -> thm option -> thm option -> thm
+ -> theory -> theory
val register_subclass: class * class -> thm option
-> theory -> theory
+ val is_class: theory -> class -> bool
+ val base_sort: theory -> class -> sort
+ val rules: theory -> class -> thm option * thm
+ val these_params: theory -> sort -> (string * (class * (string * typ))) list
+ val these_defs: theory -> sort -> thm list
+ val print_classes: theory -> unit
+
val begin: class list -> sort -> Proof.context -> Proof.context
val init: class -> theory -> Proof.context
val declare: class -> Properties.T
-> (string * mixfix) * term -> theory -> theory
val abbrev: class -> Syntax.mode -> Properties.T
-> (string * mixfix) * term -> theory -> theory
+ val class_prefix: string -> string
val refresh_syntax: class -> Proof.context -> Proof.context
- val intro_classes_tac: thm list -> tactic
- val default_intro_tac: Proof.context -> thm list -> tactic
-
- val class_prefix: string -> string
- val is_class: theory -> class -> bool
- val these_params: theory -> sort -> (string * (class * (string * typ))) list
- val these_defs: theory -> sort -> thm list
- val eq_morph: theory -> thm list -> morphism
- val base_sort: theory -> class -> sort
- val rules: theory -> class -> thm option * thm
- val print_classes: theory -> unit
-
(*instances*)
val init_instantiation: string list * (string * sort) list * sort
-> theory -> local_theory
@@ -50,6 +46,9 @@
val pretty_instantiation: local_theory -> Pretty.T
val type_name: string -> string
+ val intro_classes_tac: thm list -> tactic
+ val default_intro_tac: Proof.context -> thm list -> tactic
+
(*old axclass layer*)
val axclass_cmd: bstring * xstring list
-> (Attrib.binding * string list) list
@@ -116,8 +115,6 @@
consts: (string * string) list
(*locale parameter ~> constant name*),
base_sort: sort,
- inst: term list
- (*canonical interpretation*),
base_morph: Morphism.morphism
(*static part of canonical morphism*),
assm_intro: thm option,
@@ -130,22 +127,22 @@
};
-fun rep_class_data (ClassData d) = d;
-fun mk_class_data ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom),
+fun rep_class_data (ClassData data) = data;
+fun mk_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
(defs, operations)) =
- ClassData { consts = consts, base_sort = base_sort, inst = inst,
+ ClassData { consts = consts, base_sort = base_sort,
base_morph = base_morph, assm_intro = assm_intro, of_class = of_class, axiom = axiom,
defs = defs, operations = operations };
-fun map_class_data f (ClassData { consts, base_sort, inst, base_morph, assm_intro,
+fun map_class_data f (ClassData { consts, base_sort, base_morph, assm_intro,
of_class, axiom, defs, operations }) =
- mk_class_data (f ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom),
+ mk_class_data (f ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
(defs, operations)));
fun merge_class_data _ (ClassData { consts = consts,
- base_sort = base_sort, inst = inst, base_morph = base_morph, assm_intro = assm_intro,
+ base_sort = base_sort, base_morph = base_morph, assm_intro = assm_intro,
of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 },
- ClassData { consts = _, base_sort = _, inst = _, base_morph = _, assm_intro = _,
+ ClassData { consts = _, base_sort = _, base_morph = _, assm_intro = _,
of_class = _, axiom = _, defs = defs2, operations = operations2 }) =
- mk_class_data ((consts, base_sort, inst, base_morph, assm_intro, of_class, axiom),
+ mk_class_data ((consts, base_sort, base_morph, assm_intro, of_class, axiom),
(Thm.merge_thms (defs1, defs2),
AList.merge (op =) (K true) (operations1, operations2)));
@@ -170,11 +167,8 @@
val is_class = is_some oo lookup_class_data;
val ancestry = Graph.all_succs o ClassData.get;
-
val heritage = Graph.all_preds o ClassData.get;
-fun the_inst thy = #inst o the_class_data thy;
-
fun these_params thy =
let
fun params class =
@@ -187,34 +181,22 @@
end;
in maps params o ancestry thy end;
-fun these_assm_intros thy =
+val base_sort = #base_sort oo the_class_data;
+
+fun rules thy class =
+ let val { axiom, of_class, ... } = the_class_data thy class
+ in (axiom, of_class) end;
+
+fun all_assm_intros thy =
Graph.fold (fn (_, (data, _)) => fold (insert Thm.eq_thm)
((the_list o #assm_intro o rep_class_data) data)) (ClassData.get thy) [];
-fun these_defs thy = maps (these o Option.map #defs o lookup_class_data thy) o ancestry thy;
-
-fun these_operations thy =
- maps (#operations o the_class_data thy) o ancestry thy;
-
-val base_sort = #base_sort oo the_class_data;
-
-fun rules thy class = let
- val { axiom, of_class, ... } = the_class_data thy class
- in (axiom, of_class) end;
+fun these_defs thy = maps (#defs o the_class_data thy) o ancestry thy;
+fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy;
-val class_prefix = Logic.const_of_class o Sign.base_name;
-
-fun class_binding_morph class =
- Binding.map_prefix (K (Binding.add_prefix false (class_prefix class)));
-
-fun eq_morph thy thms = (*FIXME how general is this?*)
- Morphism.term_morphism (MetaSimplifier.rewrite_term thy thms [])
- $> Morphism.thm_morphism (MetaSimplifier.rewrite_rule thms);
-
-fun morphism thy class =
- let
- val { base_morph, defs, ... } = the_class_data thy class;
- in base_morph $> eq_morph thy defs end;
+val base_morphism = #base_morph oo the_class_data;
+fun morphism thy class = base_morphism thy class
+ $> Element.eq_morphism thy (these_defs thy [class]);
fun print_classes thy =
let
@@ -236,8 +218,6 @@
(SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"),
(SOME o Pretty.block) [Pretty.str "supersort: ",
(Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
- if is_class thy class then (SOME o Pretty.str)
- ("locale: " ^ Locale.extern thy class) else NONE,
((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks)
(Pretty.str "parameters:" :: ps)) o map mk_param
o these o Option.map #params o try (AxClass.get_info thy)) class,
@@ -254,18 +234,26 @@
(* updaters *)
-fun register class superclasses params base_sort inst morph
+fun register class sups params base_sort morph
axiom assm_intro of_class thy =
let
val operations = map (fn (v_ty as (_, ty), (c, _)) =>
(c, (class, (ty, Free v_ty)))) params;
val add_class = Graph.new_node (class,
mk_class_data (((map o pairself) fst params, base_sort,
- inst, morph, assm_intro, of_class, axiom), ([], operations)))
- #> fold (curry Graph.add_edge class) superclasses;
+ morph, assm_intro, of_class, axiom), ([], operations)))
+ #> fold (curry Graph.add_edge class) sups;
in ClassData.map add_class thy end;
+fun activate_defs class thms thy =
+ let
+ val eq_morph = Element.eq_morphism thy thms;
+ fun amend cls thy = Locale.amend_registration eq_morph
+ (cls, morphism thy cls) thy;
+ in fold amend (heritage thy [class]) thy end;
+
fun register_operation class (c, (t, some_def)) thy =
+ (*FIXME 2009 does this still also work for abbrevs?*)
let
val base_sort = base_sort thy class;
val prep_typ = map_type_tfree
@@ -279,12 +267,11 @@
(fn (defs, operations) =>
(fold cons (the_list some_def) defs,
(c, (class, (ty', t'))) :: operations))
+ |> is_some some_def ? activate_defs class (the_list some_def)
end;
-
-(** tactics and methods **)
-
fun register_subclass (sub, sup) thms thy =
+ (*FIXME should also add subclass interpretation*)
let
val of_class = (snd o rules thy) sup;
val intro = case thms
@@ -293,46 +280,15 @@
([], [sub])], []) of_class;
val classrel = (intro OF (the_list o fst o rules thy) sub)
|> Thm.close_derivation;
- (*FIXME generic amend operation for classes*)
- val amendments = map (fn class => (class, morphism thy class))
- (heritage thy [sub]);
val diff_sort = Sign.complete_sort thy [sup]
|> subtract (op =) (Sign.complete_sort thy [sub]);
- val defs_morph = eq_morph thy (these_defs thy diff_sort);
in
thy
|> AxClass.add_classrel classrel
|> ClassData.map (Graph.add_edge (sub, sup))
- |> fold (Locale.amend_registration defs_morph) amendments
- end;
-
-fun intro_classes_tac facts st =
- let
- val thy = Thm.theory_of_thm st;
- val classes = Sign.all_classes thy;
- val class_trivs = map (Thm.class_triv thy) classes;
- val class_intros = map_filter (try (#intro o AxClass.get_info thy)) classes;
- val assm_intros = these_assm_intros thy;
- in
- Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st
+ |> activate_defs sub (these_defs thy diff_sort)
end;
-fun default_intro_tac ctxt [] =
- intro_classes_tac [] ORELSE Old_Locale.intro_locales_tac true ctxt [] ORELSE
- Locale.intro_locales_tac true ctxt []
- | default_intro_tac _ _ = no_tac;
-
-fun default_tac rules ctxt facts =
- HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
- default_intro_tac ctxt facts;
-
-val _ = Context.>> (Context.map_theory
- (Method.add_methods
- [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
- "back-chain introduction rules of classes"),
- ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
- "apply some intro/elim rule")]));
-
(** classes and class target **)
@@ -393,35 +349,33 @@
(* class target *)
+val class_prefix = Logic.const_of_class o Sign.base_name;
+
fun declare class pos ((c, mx), dict) thy =
let
val prfx = class_prefix class;
val thy' = thy |> Sign.add_path prfx;
+ (*FIXME 2009 use proper name morphism*)
val morph = morphism thy' class;
- val inst = the_inst thy' class;
val params = map (apsnd fst o snd) (these_params thy' [class]);
- val amendments = map (fn class => (class, morphism thy' class))
- (heritage thy' [class]);
val c' = Sign.full_bname thy' c;
val dict' = Morphism.term morph dict;
val ty' = Term.fastype_of dict';
val ty'' = Type.strip_sorts ty';
+ (*FIXME 2009 the tinkering with theorems here is a mess*)
val def_eq = Logic.mk_equals (Const (c', ty'), dict');
- (*FIXME a mess*)
- fun amend def def' (class, morph) thy =
- Locale.amend_registration (eq_morph thy [Thm.varifyT def])
- (class, morph) thy;
fun get_axiom thy = ((Thm.varifyT o Thm.axiom thy) c', thy);
in
thy'
|> Sign.declare_const pos ((Binding.name c, ty''), mx) |> snd
- |> Thm.add_def false false (c, def_eq)
+ |> Thm.add_def false false (c, def_eq) (*FIXME 2009 name of theorem*)
+ (*FIXME 2009 add_def should accept binding*)
|>> Thm.symmetric
||>> get_axiom
|-> (fn (def, def') => register_operation class (c', (dict', SOME (Thm.symmetric def')))
- #> fold (amend def def') amendments
- #> PureThy.store_thm (c ^ "_raw", def') (*FIXME name*)
+ #> PureThy.store_thm (c ^ "_raw", def') (*FIXME 2009 name of theorem*)
+ (*FIXME 2009 store_thm etc. should accept binding*)
#> snd)
|> Sign.restore_naming thy
|> Sign.add_const_constraint (c', SOME ty')
@@ -522,7 +476,7 @@
fun type_name "*" = "prod"
| type_name "+" = "sum"
- | type_name s = sanatize_name (NameSpace.base s); (*FIXME*)
+ | type_name s = sanatize_name (NameSpace.base s);
fun resort_terms pp algebra consts constraints ts =
let
@@ -638,5 +592,35 @@
(Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params)
end;
+
+(** tactics and methods **)
+
+fun intro_classes_tac facts st =
+ let
+ val thy = Thm.theory_of_thm st;
+ val classes = Sign.all_classes thy;
+ val class_trivs = map (Thm.class_triv thy) classes;
+ val class_intros = map_filter (try (#intro o AxClass.get_info thy)) classes;
+ val assm_intros = all_assm_intros thy;
+ in
+ Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st
+ end;
+
+fun default_intro_tac ctxt [] =
+ intro_classes_tac [] ORELSE Old_Locale.intro_locales_tac true ctxt [] ORELSE
+ Locale.intro_locales_tac true ctxt []
+ | default_intro_tac _ _ = no_tac;
+
+fun default_tac rules ctxt facts =
+ HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
+ default_intro_tac ctxt facts;
+
+val _ = Context.>> (Context.map_theory
+ (Method.add_methods
+ [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
+ "back-chain introduction rules of classes"),
+ ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
+ "apply some intro/elim rule")]));
+
end;
--- a/src/Pure/Isar/element.ML Fri Jan 16 13:07:44 2009 -0800
+++ b/src/Pure/Isar/element.ML Sat Jan 17 10:40:03 2009 -0800
@@ -78,6 +78,7 @@
val generalize_facts: Proof.context -> Proof.context ->
(Attrib.binding * (thm list * Attrib.src list) list) list ->
(Attrib.binding * (thm list * Attrib.src list) list) list
+ val eq_morphism: theory -> thm list -> morphism
val transfer_morphism: theory -> morphism
val activate: (typ, term, Facts.ref) ctxt list -> Proof.context -> context_i list * Proof.context
val activate_i: context_i list -> Proof.context -> context_i list * Proof.context
@@ -521,6 +522,14 @@
fun satisfy_facts witns = facts_map (morph_ctxt (satisfy_morphism witns));
+(* rewriting with equalities *)
+
+fun eq_morphism thy thms = Morphism.morphism
+ {binding = I, var = I, typ = I,
+ term = MetaSimplifier.rewrite_term thy thms [],
+ fact = map (MetaSimplifier.rewrite_rule thms)};
+
+
(* generalize type/term parameters *)
val maxidx_atts = fold Args.maxidx_values;
--- a/src/Pure/Isar/expression.ML Fri Jan 16 13:07:44 2009 -0800
+++ b/src/Pure/Isar/expression.ML Sat Jan 17 10:40:03 2009 -0800
@@ -865,9 +865,7 @@
Morphism.thm (export' $> export) #>
LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
Drule.abs_def);
- val eq_morph =
- Morphism.term_morphism (MetaSimplifier.rewrite_term thy thms' []) $>
- Morphism.thm_morphism (MetaSimplifier.rewrite_rule thms');
+ val eq_morph = Element.eq_morphism thy thms';
val eq_attns' = map ((apsnd o map) (Attrib.attribute_i thy)) eq_attns;
in
thy
--- a/src/Pure/Tools/isabelle_process.ML Fri Jan 16 13:07:44 2009 -0800
+++ b/src/Pure/Tools/isabelle_process.ML Sat Jan 17 10:40:03 2009 -0800
@@ -55,9 +55,6 @@
let val clean = clean_string [Symbol.STX, "\n", "\r"]
in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end;
-fun message_text class body =
- YXML.element Markup.messageN [(Markup.classN, class)] [clean_string [Symbol.STX] body];
-
fun message_pos trees = trees |> get_first
(fn XML.Elem (name, atts, ts) =>
if name = Markup.positionN then SOME (Position.of_properties atts)
@@ -69,21 +66,21 @@
in
-fun message _ _ _ "" = ()
- | message out_stream ch class body =
+fun message _ _ "" = ()
+ | message out_stream ch body =
let
val pos = the_default Position.none (message_pos (YXML.parse_body body));
val props =
Position.properties_of (Position.thread_data ())
|> Position.default_properties pos;
- val txt = message_text class body;
+ val txt = clean_string [Symbol.STX] body;
in output out_stream (special ch ^ message_props props ^ txt ^ special_end) end;
fun init_message out_stream =
let
val pid = (Markup.pidN, process_id ());
val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown");
- val text = message_text Markup.initN (Session.welcome ());
+ val text = Session.welcome ();
in output out_stream (special "A" ^ message_props [pid, session] ^ text ^ special_end) end;
end;
@@ -116,13 +113,13 @@
val _ = SimpleThread.fork false (auto_flush out_stream);
val _ = SimpleThread.fork false (auto_flush TextIO.stdErr);
in
- Output.status_fn := message out_stream "B" Markup.statusN;
- Output.writeln_fn := message out_stream "C" Markup.writelnN;
- Output.priority_fn := message out_stream "D" Markup.priorityN;
- Output.tracing_fn := message out_stream "E" Markup.tracingN;
- Output.warning_fn := message out_stream "F" Markup.warningN;
- Output.error_fn := message out_stream "G" Markup.errorN;
- Output.debug_fn := message out_stream "H" Markup.debugN;
+ Output.status_fn := message out_stream "B";
+ Output.writeln_fn := message out_stream "C";
+ Output.priority_fn := message out_stream "D";
+ Output.tracing_fn := message out_stream "E";
+ Output.warning_fn := message out_stream "F";
+ Output.error_fn := message out_stream "G";
+ Output.debug_fn := message out_stream "H";
Output.prompt_fn := ignore;
out_stream
end;
--- a/src/Pure/Tools/isabelle_process.scala Fri Jan 16 13:07:44 2009 -0800
+++ b/src/Pure/Tools/isabelle_process.scala Sat Jan 17 10:40:03 2009 -0800
@@ -50,6 +50,21 @@
('2' : Int) -> Kind.STDOUT,
('3' : Int) -> Kind.SIGNAL,
('4' : Int) -> Kind.EXIT)
+ // message markup
+ val markup = Map(
+ Kind.INIT -> Markup.INIT,
+ Kind.STATUS -> Markup.STATUS,
+ Kind.WRITELN -> Markup.WRITELN,
+ Kind.PRIORITY -> Markup.PRIORITY,
+ Kind.TRACING -> Markup.TRACING,
+ Kind.WARNING -> Markup.WARNING,
+ Kind.ERROR -> Markup.ERROR,
+ Kind.DEBUG -> Markup.DEBUG,
+ Kind.SYSTEM -> Markup.SYSTEM,
+ Kind.STDIN -> Markup.STDIN,
+ Kind.STDOUT -> Markup.STDOUT,
+ Kind.SIGNAL -> Markup.SIGNAL,
+ Kind.EXIT -> Markup.EXIT)
//}}}
def is_raw(kind: Value) =
kind == STDOUT
@@ -67,8 +82,10 @@
class Result(val kind: Kind.Value, val props: Properties, val result: String) {
override def toString = {
- val tree = YXML.parse_failsafe(result)
- val res = if (kind == Kind.STATUS) tree.toString else XML.content(tree).mkString
+ val trees = YXML.parse_body_failsafe(result)
+ val res =
+ if (kind == Kind.STATUS) trees.map(_.toString).mkString
+ else trees.flatMap(XML.content(_).mkString).mkString
if (props == null) kind.toString + " [[" + res + "]]"
else kind.toString + " " + props.toString + " [[" + res + "]]"
}
@@ -77,6 +94,10 @@
def is_system = Kind.is_system(kind)
}
+ def parse_message(kind: Kind.Value, result: String) = {
+ XML.Elem(Markup.MESSAGE, List((Markup.CLASS, Kind.markup(kind))),
+ YXML.parse_body_failsafe(result))
+ }
}
--- a/src/Pure/axclass.ML Fri Jan 16 13:07:44 2009 -0800
+++ b/src/Pure/axclass.ML Sat Jan 17 10:40:03 2009 -0800
@@ -295,7 +295,7 @@
in
thy
|> Sign.primitive_classrel (c1, c2)
- |> put_classrel ((c1, c2), Drule.unconstrainTs th)
+ |> put_classrel ((c1, c2), Thm.close_derivation (Drule.unconstrainTs th))
|> perhaps complete_arities
end;