--- a/src/Pure/Isar/obtain.ML Tue Sep 02 14:10:29 2008 +0200
+++ b/src/Pure/Isar/obtain.ML Tue Sep 02 14:10:30 2008 +0200
@@ -40,16 +40,16 @@
signature OBTAIN =
sig
val thatN: string
- val obtain: string -> (string * string option * mixfix) list ->
- ((string * Attrib.src list) * (string * string list) list) list ->
+ val obtain: string -> (Name.binding * string option * mixfix) list ->
+ ((Name.binding * Attrib.src list) * (string * string list) list) list ->
bool -> Proof.state -> Proof.state
- val obtain_i: string -> (string * typ option * mixfix) list ->
- ((string * attribute list) * (term * term list) list) list ->
+ val obtain_i: string -> (Name.binding * typ option * mixfix) list ->
+ ((Name.binding * attribute list) * (term * term list) list) list ->
bool -> Proof.state -> Proof.state
val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
(cterm list * thm list) * Proof.context
- val guess: (string * string option * mixfix) list -> bool -> Proof.state -> Proof.state
- val guess_i: (string * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
+ val guess: (Name.binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
+ val guess_i: (Name.binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
end;
structure Obtain: OBTAIN =
@@ -122,7 +122,7 @@
(*obtain vars*)
val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
- val xs = map #1 vars;
+ val xs = map (Name.name_of o #1) vars;
(*obtain asms*)
val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
@@ -151,18 +151,19 @@
fun after_qed _ =
Proof.local_qed (NONE, false)
#> Seq.map (`Proof.the_fact #-> (fn rule =>
- Proof.fix_i (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars)
+ Proof.fix_i vars
#> Proof.assm_i (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms));
in
state
|> Proof.enter_forward
- |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, [])])] int
+ |> Proof.have_i NONE (K Seq.single) [((Name.no_binding, []), [(obtain_prop, [])])] int
|> Proof.proof (SOME Method.succeed_text) |> Seq.hd
- |> Proof.fix_i [(thesisN, NONE, NoSyn)]
- |> Proof.assume_i [((that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
+ |> Proof.fix_i [(Name.binding thesisN, NONE, NoSyn)]
+ |> Proof.assume_i
+ [((Name.binding that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
|> `Proof.the_facts
||> Proof.chain_facts chain_facts
- ||> Proof.show_i NONE after_qed [(("", []), [(thesis, [])])] false
+ ||> Proof.show_i NONE after_qed [((Name.no_binding, []), [(thesis, [])])] false
|-> Proof.refine_insert
end;
@@ -258,8 +259,10 @@
val rule'' = Thm.forall_elim (cert (Logic.varify (Free thesis_var))) rule';
in ((vars', rule''), ctxt') end;
-fun inferred_type (x, _, mx) ctxt =
- let val ((_, T), ctxt') = ProofContext.inferred_param x ctxt
+fun inferred_type (binding, _, mx) ctxt =
+ let
+ val x = Name.name_of binding;
+ val (T, ctxt') = ProofContext.inferred_param x ctxt
in ((x, T, mx), ctxt') end;
fun polymorphic ctxt vars =
@@ -291,9 +294,9 @@
in
state'
|> Proof.map_context (K ctxt')
- |> Proof.fix_i (map (fn ((x, T), mx) => (x, SOME T, mx)) parms)
- |> `Proof.context_of |-> (fn fix_ctxt =>
- Proof.assm_i (obtain_export fix_ctxt rule (map cert ts)) [(("", []), asms)])
+ |> Proof.fix_i (map (fn ((x, T), mx) => (Name.binding x, SOME T, mx)) parms)
+ |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i
+ (obtain_export fix_ctxt rule (map cert ts)) [((Name.no_binding, []), asms)])
|> Proof.add_binds_i AutoBind.no_facts
end;
@@ -308,10 +311,10 @@
state
|> Proof.enter_forward
|> Proof.begin_block
- |> Proof.fix_i [(AutoBind.thesisN, NONE, NoSyn)]
+ |> Proof.fix_i [(Name.binding AutoBind.thesisN, NONE, NoSyn)]
|> Proof.chain_facts chain_facts
|> Proof.local_goal print_result (K I) (apsnd (rpair I))
- "guess" before_qed after_qed [(("", []), [Logic.mk_term goal, goal])]
+ "guess" before_qed after_qed [((Name.no_binding, []), [Logic.mk_term goal, goal])]
|> Proof.refine (Method.primitive_text (K (Goal.init (cert thesis)))) |> Seq.hd
end;
--- a/src/Pure/Isar/specification.ML Tue Sep 02 14:10:29 2008 +0200
+++ b/src/Pure/Isar/specification.ML Tue Sep 02 14:10:30 2008 +0200
@@ -9,52 +9,53 @@
signature SPECIFICATION =
sig
val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit
- val check_specification: (string * typ option * mixfix) list ->
- ((string * Attrib.src list) * term list) list list -> Proof.context ->
- (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) *
+ val check_specification: (Name.binding * typ option * mixfix) list ->
+ ((Name.binding * Attrib.src list) * term list) list list -> Proof.context ->
+ (((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list) *
Proof.context
- val read_specification: (string * string option * mixfix) list ->
- ((string * Attrib.src list) * string list) list list -> Proof.context ->
- (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) *
+ val read_specification: (Name.binding * string option * mixfix) list ->
+ ((Name.binding * Attrib.src list) * string list) list list -> Proof.context ->
+ (((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list) *
Proof.context
- val check_free_specification: (string * typ option * mixfix) list ->
- ((string * Attrib.src list) * term list) list -> Proof.context ->
- (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) *
+ val check_free_specification: (Name.binding * typ option * mixfix) list ->
+ ((Name.binding * Attrib.src list) * term list) list -> Proof.context ->
+ (((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list) *
Proof.context
- val read_free_specification: (string * string option * mixfix) list ->
- ((string * Attrib.src list) * string list) list -> Proof.context ->
- (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) *
+ val read_free_specification: (Name.binding * string option * mixfix) list ->
+ ((Name.binding * Attrib.src list) * string list) list -> Proof.context ->
+ (((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list) *
Proof.context
- val axiomatization: (string * typ option * mixfix) list ->
- ((bstring * Attrib.src list) * term list) list -> local_theory ->
- (term list * (bstring * thm list) list) * local_theory
- val axiomatization_cmd: (string * string option * mixfix) list ->
- ((bstring * Attrib.src list) * string list) list -> local_theory ->
- (term list * (bstring * thm list) list) * local_theory
+ val axiomatization: (Name.binding * typ option * mixfix) list ->
+ ((Name.binding * Attrib.src list) * term list) list -> local_theory ->
+ (term list * (string * thm list) list) * local_theory
+ val axiomatization_cmd: (Name.binding * string option * mixfix) list ->
+ ((Name.binding * Attrib.src list) * string list) list -> local_theory ->
+ (term list * (string * thm list) list) * local_theory
val definition:
- (string * typ option * mixfix) option * ((string * Attrib.src list) * term) ->
- local_theory -> (term * (bstring * thm)) * local_theory
+ (Name.binding * typ option * mixfix) option * ((Name.binding * Attrib.src list) * term) ->
+ local_theory -> (term * (string * thm)) * local_theory
val definition_cmd:
- (string * string option * mixfix) option * ((string * Attrib.src list) * string) ->
- local_theory -> (term * (bstring * thm)) * local_theory
- val abbreviation: Syntax.mode -> (string * typ option * mixfix) option * term ->
+ (Name.binding * string option * mixfix) option * ((Name.binding * Attrib.src list) * string) ->
+ local_theory -> (term * (string * thm)) * local_theory
+ val abbreviation: Syntax.mode -> (Name.binding * typ option * mixfix) option * term ->
local_theory -> local_theory
- val abbreviation_cmd: Syntax.mode -> (string * string option * mixfix) option * string ->
+ val abbreviation_cmd: Syntax.mode -> (Name.binding * string option * mixfix) option * string ->
local_theory -> local_theory
val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
- val theorems: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
- local_theory -> (bstring * thm list) list * local_theory
+ val theorems: string ->
+ ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
+ local_theory -> (string * thm list) list * local_theory
val theorems_cmd: string ->
- ((bstring * Attrib.src list) * (Facts.ref * Attrib.src list) list) list ->
- local_theory -> (bstring * thm list) list * local_theory
+ ((Name.binding * Attrib.src list) * (Facts.ref * Attrib.src list) list) list ->
+ local_theory -> (string * thm list) list * local_theory
val theorem: string -> Method.text option ->
- (thm list list -> local_theory -> local_theory) ->
- string * Attrib.src list -> Element.context_i Locale.element list -> Element.statement_i ->
+ (thm list list -> local_theory -> local_theory) -> Name.binding * Attrib.src list ->
+ Element.context_i Locale.element list -> Element.statement_i ->
bool -> local_theory -> Proof.state
val theorem_cmd: string -> Method.text option ->
- (thm list list -> local_theory -> local_theory) ->
- string * Attrib.src list -> Element.context Locale.element list -> Element.statement ->
+ (thm list list -> local_theory -> local_theory) -> Name.binding * Attrib.src list ->
+ Element.context Locale.element list -> Element.statement ->
bool -> local_theory -> Proof.state
val add_theorem_hook: (bool -> Proof.state -> Proof.state) -> Context.generic -> Context.generic
end;
@@ -122,8 +123,8 @@
|> flat |> burrow (Syntax.check_props params_ctxt);
val specs_ctxt = params_ctxt |> (fold o fold) Variable.declare_term specs;
- val vs = specs_ctxt |> fold_map ProofContext.inferred_param xs |> fst;
- val params = vs ~~ map #3 vars;
+ val Ts = specs_ctxt |> fold_map ProofContext.inferred_param xs |> fst;
+ val params = map2 (fn (b, _, mx) => fn T => ((b, T), mx)) vars Ts;
val name_atts = map (fn ((name, atts), _) => (name, map (prep_att thy) atts)) (flat raw_specss);
in ((params, name_atts ~~ specs), specs_ctxt) end;
@@ -149,7 +150,8 @@
val consts' = map (Morphism.term (LocalTheory.target_morphism lthy')) consts;
val _ =
if not do_print then ()
- else print_consts lthy' (member (op =) (fold Term.add_frees consts' [])) (map fst vars);
+ else print_consts lthy' (member (op =) (fold Term.add_frees consts' []))
+ (map (fn ((b, T), _) => (Name.name_of b, T)) vars);
in ((consts, axioms), lthy') end;
val axiomatization = gen_axioms false check_specification;
@@ -163,21 +165,27 @@
val (vars, [((raw_name, atts), [prop])]) =
fst (prep (the_list raw_var) [(raw_a, [raw_prop])] lthy);
val (((x, T), rhs), prove) = LocalDefs.derived_def lthy true prop;
- val name = Thm.def_name_optional x raw_name;
- val mx = (case vars of [] => NoSyn | [((x', _), mx)] =>
- if x = x' then mx
- else error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote x'));
- val ((lhs, (_, th)), lthy2) = lthy
- |> LocalTheory.define Thm.definitionK ((x, mx), ((name ^ "_raw", []), rhs));
- val ((b, [th']), lthy3) = lthy2
- |> LocalTheory.note Thm.definitionK
- ((name, Code.add_default_func_attr :: atts), [prove lthy2 th]);
+ val name = Name.map_name (Thm.def_name_optional x) raw_name;
+ val var =
+ (case vars of
+ [] => (Name.binding x, NoSyn)
+ | [((b, _), mx)] =>
+ let
+ val y = Name.name_of b;
+ val _ = x = y orelse
+ error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
+ Position.str_of (Name.pos_of b));
+ in (b, mx) end);
+ val ((lhs, (_, th)), lthy2) = lthy |> LocalTheory.define Thm.definitionK
+ (var, ((Name.map_name (suffix "_raw") name, []), rhs));
+ val ((def_name, [th']), lthy3) = lthy2 |> LocalTheory.note Thm.definitionK
+ ((name, Code.add_default_func_attr :: atts), [prove lthy2 th]);
val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;
val _ =
if not do_print then ()
else print_consts lthy3 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
- in ((lhs, (b, th')), lthy3) end;
+ in ((lhs, (def_name, th')), lthy3) end;
val definition = gen_def false check_free_specification;
val definition_cmd = gen_def true read_free_specification;
@@ -191,12 +199,19 @@
prep (the_list raw_var) [(("", []), [raw_prop])]
(lthy |> ProofContext.set_mode ProofContext.mode_abbrev);
val ((x, T), rhs) = LocalDefs.abs_def (#2 (LocalDefs.cert_def lthy prop));
- val mx = (case vars of [] => NoSyn | [((y, _), mx)] =>
- if x = y then mx
- else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y));
+ val var =
+ (case vars of
+ [] => (Name.binding x, NoSyn)
+ | [((b, _), mx)] =>
+ let
+ val y = Name.name_of b;
+ val _ = x = y orelse
+ error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
+ Position.str_of (Name.pos_of b));
+ in (b, mx) end);
val lthy' = lthy
|> ProofContext.set_syntax_mode mode (* FIXME ?!? *)
- |> LocalTheory.abbrev mode ((x, mx), rhs) |> snd
+ |> LocalTheory.abbrev mode (var, rhs) |> snd
|> ProofContext.restore_syntax_mode lthy;
val _ = if not do_print then () else print_consts lthy' (K false) [(x, T)];
@@ -249,11 +264,12 @@
in ((prems, stmt, []), goal_ctxt) end
| Element.Obtains obtains =>
let
- val case_names = obtains |> map_index
- (fn (i, ("", _)) => string_of_int (i + 1) | (_, (name, _)) => name);
+ val case_names = obtains |> map_index (fn (i, (binding, _)) =>
+ let val name = Name.name_of binding
+ in if name = "" then string_of_int (i + 1) else name end);
val constraints = obtains |> map (fn (_, (vars, _)) =>
Locale.Elem (Element.Constrains
- (vars |> map_filter (fn (x, SOME T) => SOME (x, T) | _ => NONE))));
+ (vars |> map_filter (fn (x, SOME T) => SOME (Name.name_of x, T) | _ => NONE))));
val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
val (_, loc_ctxt, elems_ctxt, propp) = prep_stmt (elems @ constraints) raw_propp ctxt;
@@ -262,14 +278,15 @@
fun assume_case ((name, (vars, _)), asms) ctxt' =
let
- val xs = map fst vars;
+ val bs = map fst vars;
+ val xs = map Name.name_of bs;
val props = map fst asms;
- val (parms, _) = ctxt'
+ val (Ts, _) = ctxt'
|> fold Variable.declare_term props
|> fold_map ProofContext.inferred_param xs;
- val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis));
+ val asm = Term.list_all_free (xs ~~ Ts, Logic.list_implies (props, thesis));
in
- ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs));
+ ctxt' |> (snd o ProofContext.add_fixes_i (map (fn b => (b, NONE, NoSyn)) bs));
ctxt' |> Variable.auto_fixes asm
|> ProofContext.add_assms_i Assumption.assume_export
[((name, [ContextRules.intro_query NONE]), [(asm, [])])]
@@ -279,13 +296,13 @@
val atts = map (Attrib.internal o K)
[RuleCases.consumes (~ (length obtains)), RuleCases.case_names case_names];
val prems = subtract_prems loc_ctxt elems_ctxt;
- val stmt = [(("", atts), [(thesis, [])])];
+ val stmt = [((Name.no_binding, atts), [(thesis, [])])];
val (facts, goal_ctxt) = elems_ctxt
- |> (snd o ProofContext.add_fixes_i [(AutoBind.thesisN, NONE, NoSyn)])
+ |> (snd o ProofContext.add_fixes_i [(Name.binding AutoBind.thesisN, NONE, NoSyn)])
|> fold_map assume_case (obtains ~~ propp)
|-> (fn ths => ProofContext.note_thmss_i Thm.assumptionK
- [((Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
+ [((Name.binding Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
in ((prems, stmt, facts), goal_ctxt) end);
structure TheoremHook = GenericDataFun
@@ -323,14 +340,20 @@
lthy
|> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
|> (fn (res, lthy') =>
- (ProofDisplay.theory_results lthy' ((kind, name), res);
- if name = "" andalso null atts then lthy'
- else #2 (LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])] lthy')))
+ if Name.name_of name = "" andalso null atts then
+ (ProofDisplay.theory_results lthy' ((kind, ""), res); lthy')
+ else
+ let
+ val ([(res_name, _)], lthy'') = lthy'
+ |> LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])];
+ val _ = ProofDisplay.theory_results lthy' ((kind, res_name), res);
+ in lthy'' end)
|> after_qed results'
end;
in
goal_ctxt
- |> ProofContext.note_thmss_i Thm.assumptionK [((AutoBind.assmsN, []), [(prems, [])])]
+ |> ProofContext.note_thmss_i Thm.assumptionK
+ [((Name.binding AutoBind.assmsN, []), [(prems, [])])]
|> snd
|> Proof.theorem_i before_qed after_qed' (map snd stmt)
|> Proof.refine_insert facts