1.1 --- a/src/Pure/Isar/obtain.ML Tue Sep 02 14:10:29 2008 +0200
1.2 +++ b/src/Pure/Isar/obtain.ML Tue Sep 02 14:10:30 2008 +0200
1.3 @@ -40,16 +40,16 @@
1.4 signature OBTAIN =
1.5 sig
1.6 val thatN: string
1.7 - val obtain: string -> (string * string option * mixfix) list ->
1.8 - ((string * Attrib.src list) * (string * string list) list) list ->
1.9 + val obtain: string -> (Name.binding * string option * mixfix) list ->
1.10 + ((Name.binding * Attrib.src list) * (string * string list) list) list ->
1.11 bool -> Proof.state -> Proof.state
1.12 - val obtain_i: string -> (string * typ option * mixfix) list ->
1.13 - ((string * attribute list) * (term * term list) list) list ->
1.14 + val obtain_i: string -> (Name.binding * typ option * mixfix) list ->
1.15 + ((Name.binding * attribute list) * (term * term list) list) list ->
1.16 bool -> Proof.state -> Proof.state
1.17 val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
1.18 (cterm list * thm list) * Proof.context
1.19 - val guess: (string * string option * mixfix) list -> bool -> Proof.state -> Proof.state
1.20 - val guess_i: (string * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
1.21 + val guess: (Name.binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
1.22 + val guess_i: (Name.binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
1.23 end;
1.24
1.25 structure Obtain: OBTAIN =
1.26 @@ -122,7 +122,7 @@
1.27 (*obtain vars*)
1.28 val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
1.29 val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
1.30 - val xs = map #1 vars;
1.31 + val xs = map (Name.name_of o #1) vars;
1.32
1.33 (*obtain asms*)
1.34 val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
1.35 @@ -151,18 +151,19 @@
1.36 fun after_qed _ =
1.37 Proof.local_qed (NONE, false)
1.38 #> Seq.map (`Proof.the_fact #-> (fn rule =>
1.39 - Proof.fix_i (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars)
1.40 + Proof.fix_i vars
1.41 #> Proof.assm_i (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms));
1.42 in
1.43 state
1.44 |> Proof.enter_forward
1.45 - |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, [])])] int
1.46 + |> Proof.have_i NONE (K Seq.single) [((Name.no_binding, []), [(obtain_prop, [])])] int
1.47 |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
1.48 - |> Proof.fix_i [(thesisN, NONE, NoSyn)]
1.49 - |> Proof.assume_i [((that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
1.50 + |> Proof.fix_i [(Name.binding thesisN, NONE, NoSyn)]
1.51 + |> Proof.assume_i
1.52 + [((Name.binding that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
1.53 |> `Proof.the_facts
1.54 ||> Proof.chain_facts chain_facts
1.55 - ||> Proof.show_i NONE after_qed [(("", []), [(thesis, [])])] false
1.56 + ||> Proof.show_i NONE after_qed [((Name.no_binding, []), [(thesis, [])])] false
1.57 |-> Proof.refine_insert
1.58 end;
1.59
1.60 @@ -258,8 +259,10 @@
1.61 val rule'' = Thm.forall_elim (cert (Logic.varify (Free thesis_var))) rule';
1.62 in ((vars', rule''), ctxt') end;
1.63
1.64 -fun inferred_type (x, _, mx) ctxt =
1.65 - let val ((_, T), ctxt') = ProofContext.inferred_param x ctxt
1.66 +fun inferred_type (binding, _, mx) ctxt =
1.67 + let
1.68 + val x = Name.name_of binding;
1.69 + val (T, ctxt') = ProofContext.inferred_param x ctxt
1.70 in ((x, T, mx), ctxt') end;
1.71
1.72 fun polymorphic ctxt vars =
1.73 @@ -291,9 +294,9 @@
1.74 in
1.75 state'
1.76 |> Proof.map_context (K ctxt')
1.77 - |> Proof.fix_i (map (fn ((x, T), mx) => (x, SOME T, mx)) parms)
1.78 - |> `Proof.context_of |-> (fn fix_ctxt =>
1.79 - Proof.assm_i (obtain_export fix_ctxt rule (map cert ts)) [(("", []), asms)])
1.80 + |> Proof.fix_i (map (fn ((x, T), mx) => (Name.binding x, SOME T, mx)) parms)
1.81 + |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i
1.82 + (obtain_export fix_ctxt rule (map cert ts)) [((Name.no_binding, []), asms)])
1.83 |> Proof.add_binds_i AutoBind.no_facts
1.84 end;
1.85
1.86 @@ -308,10 +311,10 @@
1.87 state
1.88 |> Proof.enter_forward
1.89 |> Proof.begin_block
1.90 - |> Proof.fix_i [(AutoBind.thesisN, NONE, NoSyn)]
1.91 + |> Proof.fix_i [(Name.binding AutoBind.thesisN, NONE, NoSyn)]
1.92 |> Proof.chain_facts chain_facts
1.93 |> Proof.local_goal print_result (K I) (apsnd (rpair I))
1.94 - "guess" before_qed after_qed [(("", []), [Logic.mk_term goal, goal])]
1.95 + "guess" before_qed after_qed [((Name.no_binding, []), [Logic.mk_term goal, goal])]
1.96 |> Proof.refine (Method.primitive_text (K (Goal.init (cert thesis)))) |> Seq.hd
1.97 end;
1.98
2.1 --- a/src/Pure/Isar/specification.ML Tue Sep 02 14:10:29 2008 +0200
2.2 +++ b/src/Pure/Isar/specification.ML Tue Sep 02 14:10:30 2008 +0200
2.3 @@ -9,52 +9,53 @@
2.4 signature SPECIFICATION =
2.5 sig
2.6 val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit
2.7 - val check_specification: (string * typ option * mixfix) list ->
2.8 - ((string * Attrib.src list) * term list) list list -> Proof.context ->
2.9 - (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) *
2.10 + val check_specification: (Name.binding * typ option * mixfix) list ->
2.11 + ((Name.binding * Attrib.src list) * term list) list list -> Proof.context ->
2.12 + (((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list) *
2.13 Proof.context
2.14 - val read_specification: (string * string option * mixfix) list ->
2.15 - ((string * Attrib.src list) * string list) list list -> Proof.context ->
2.16 - (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) *
2.17 + val read_specification: (Name.binding * string option * mixfix) list ->
2.18 + ((Name.binding * Attrib.src list) * string list) list list -> Proof.context ->
2.19 + (((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list) *
2.20 Proof.context
2.21 - val check_free_specification: (string * typ option * mixfix) list ->
2.22 - ((string * Attrib.src list) * term list) list -> Proof.context ->
2.23 - (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) *
2.24 + val check_free_specification: (Name.binding * typ option * mixfix) list ->
2.25 + ((Name.binding * Attrib.src list) * term list) list -> Proof.context ->
2.26 + (((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list) *
2.27 Proof.context
2.28 - val read_free_specification: (string * string option * mixfix) list ->
2.29 - ((string * Attrib.src list) * string list) list -> Proof.context ->
2.30 - (((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) *
2.31 + val read_free_specification: (Name.binding * string option * mixfix) list ->
2.32 + ((Name.binding * Attrib.src list) * string list) list -> Proof.context ->
2.33 + (((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list) *
2.34 Proof.context
2.35 - val axiomatization: (string * typ option * mixfix) list ->
2.36 - ((bstring * Attrib.src list) * term list) list -> local_theory ->
2.37 - (term list * (bstring * thm list) list) * local_theory
2.38 - val axiomatization_cmd: (string * string option * mixfix) list ->
2.39 - ((bstring * Attrib.src list) * string list) list -> local_theory ->
2.40 - (term list * (bstring * thm list) list) * local_theory
2.41 + val axiomatization: (Name.binding * typ option * mixfix) list ->
2.42 + ((Name.binding * Attrib.src list) * term list) list -> local_theory ->
2.43 + (term list * (string * thm list) list) * local_theory
2.44 + val axiomatization_cmd: (Name.binding * string option * mixfix) list ->
2.45 + ((Name.binding * Attrib.src list) * string list) list -> local_theory ->
2.46 + (term list * (string * thm list) list) * local_theory
2.47 val definition:
2.48 - (string * typ option * mixfix) option * ((string * Attrib.src list) * term) ->
2.49 - local_theory -> (term * (bstring * thm)) * local_theory
2.50 + (Name.binding * typ option * mixfix) option * ((Name.binding * Attrib.src list) * term) ->
2.51 + local_theory -> (term * (string * thm)) * local_theory
2.52 val definition_cmd:
2.53 - (string * string option * mixfix) option * ((string * Attrib.src list) * string) ->
2.54 - local_theory -> (term * (bstring * thm)) * local_theory
2.55 - val abbreviation: Syntax.mode -> (string * typ option * mixfix) option * term ->
2.56 + (Name.binding * string option * mixfix) option * ((Name.binding * Attrib.src list) * string) ->
2.57 + local_theory -> (term * (string * thm)) * local_theory
2.58 + val abbreviation: Syntax.mode -> (Name.binding * typ option * mixfix) option * term ->
2.59 local_theory -> local_theory
2.60 - val abbreviation_cmd: Syntax.mode -> (string * string option * mixfix) option * string ->
2.61 + val abbreviation_cmd: Syntax.mode -> (Name.binding * string option * mixfix) option * string ->
2.62 local_theory -> local_theory
2.63 val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
2.64 val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
2.65 - val theorems: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
2.66 - local_theory -> (bstring * thm list) list * local_theory
2.67 + val theorems: string ->
2.68 + ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
2.69 + local_theory -> (string * thm list) list * local_theory
2.70 val theorems_cmd: string ->
2.71 - ((bstring * Attrib.src list) * (Facts.ref * Attrib.src list) list) list ->
2.72 - local_theory -> (bstring * thm list) list * local_theory
2.73 + ((Name.binding * Attrib.src list) * (Facts.ref * Attrib.src list) list) list ->
2.74 + local_theory -> (string * thm list) list * local_theory
2.75 val theorem: string -> Method.text option ->
2.76 - (thm list list -> local_theory -> local_theory) ->
2.77 - string * Attrib.src list -> Element.context_i Locale.element list -> Element.statement_i ->
2.78 + (thm list list -> local_theory -> local_theory) -> Name.binding * Attrib.src list ->
2.79 + Element.context_i Locale.element list -> Element.statement_i ->
2.80 bool -> local_theory -> Proof.state
2.81 val theorem_cmd: string -> Method.text option ->
2.82 - (thm list list -> local_theory -> local_theory) ->
2.83 - string * Attrib.src list -> Element.context Locale.element list -> Element.statement ->
2.84 + (thm list list -> local_theory -> local_theory) -> Name.binding * Attrib.src list ->
2.85 + Element.context Locale.element list -> Element.statement ->
2.86 bool -> local_theory -> Proof.state
2.87 val add_theorem_hook: (bool -> Proof.state -> Proof.state) -> Context.generic -> Context.generic
2.88 end;
2.89 @@ -122,8 +123,8 @@
2.90 |> flat |> burrow (Syntax.check_props params_ctxt);
2.91 val specs_ctxt = params_ctxt |> (fold o fold) Variable.declare_term specs;
2.92
2.93 - val vs = specs_ctxt |> fold_map ProofContext.inferred_param xs |> fst;
2.94 - val params = vs ~~ map #3 vars;
2.95 + val Ts = specs_ctxt |> fold_map ProofContext.inferred_param xs |> fst;
2.96 + val params = map2 (fn (b, _, mx) => fn T => ((b, T), mx)) vars Ts;
2.97 val name_atts = map (fn ((name, atts), _) => (name, map (prep_att thy) atts)) (flat raw_specss);
2.98 in ((params, name_atts ~~ specs), specs_ctxt) end;
2.99
2.100 @@ -149,7 +150,8 @@
2.101 val consts' = map (Morphism.term (LocalTheory.target_morphism lthy')) consts;
2.102 val _ =
2.103 if not do_print then ()
2.104 - else print_consts lthy' (member (op =) (fold Term.add_frees consts' [])) (map fst vars);
2.105 + else print_consts lthy' (member (op =) (fold Term.add_frees consts' []))
2.106 + (map (fn ((b, T), _) => (Name.name_of b, T)) vars);
2.107 in ((consts, axioms), lthy') end;
2.108
2.109 val axiomatization = gen_axioms false check_specification;
2.110 @@ -163,21 +165,27 @@
2.111 val (vars, [((raw_name, atts), [prop])]) =
2.112 fst (prep (the_list raw_var) [(raw_a, [raw_prop])] lthy);
2.113 val (((x, T), rhs), prove) = LocalDefs.derived_def lthy true prop;
2.114 - val name = Thm.def_name_optional x raw_name;
2.115 - val mx = (case vars of [] => NoSyn | [((x', _), mx)] =>
2.116 - if x = x' then mx
2.117 - else error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote x'));
2.118 - val ((lhs, (_, th)), lthy2) = lthy
2.119 - |> LocalTheory.define Thm.definitionK ((x, mx), ((name ^ "_raw", []), rhs));
2.120 - val ((b, [th']), lthy3) = lthy2
2.121 - |> LocalTheory.note Thm.definitionK
2.122 - ((name, Code.add_default_func_attr :: atts), [prove lthy2 th]);
2.123 + val name = Name.map_name (Thm.def_name_optional x) raw_name;
2.124 + val var =
2.125 + (case vars of
2.126 + [] => (Name.binding x, NoSyn)
2.127 + | [((b, _), mx)] =>
2.128 + let
2.129 + val y = Name.name_of b;
2.130 + val _ = x = y orelse
2.131 + error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
2.132 + Position.str_of (Name.pos_of b));
2.133 + in (b, mx) end);
2.134 + val ((lhs, (_, th)), lthy2) = lthy |> LocalTheory.define Thm.definitionK
2.135 + (var, ((Name.map_name (suffix "_raw") name, []), rhs));
2.136 + val ((def_name, [th']), lthy3) = lthy2 |> LocalTheory.note Thm.definitionK
2.137 + ((name, Code.add_default_func_attr :: atts), [prove lthy2 th]);
2.138
2.139 val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;
2.140 val _ =
2.141 if not do_print then ()
2.142 else print_consts lthy3 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
2.143 - in ((lhs, (b, th')), lthy3) end;
2.144 + in ((lhs, (def_name, th')), lthy3) end;
2.145
2.146 val definition = gen_def false check_free_specification;
2.147 val definition_cmd = gen_def true read_free_specification;
2.148 @@ -191,12 +199,19 @@
2.149 prep (the_list raw_var) [(("", []), [raw_prop])]
2.150 (lthy |> ProofContext.set_mode ProofContext.mode_abbrev);
2.151 val ((x, T), rhs) = LocalDefs.abs_def (#2 (LocalDefs.cert_def lthy prop));
2.152 - val mx = (case vars of [] => NoSyn | [((y, _), mx)] =>
2.153 - if x = y then mx
2.154 - else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y));
2.155 + val var =
2.156 + (case vars of
2.157 + [] => (Name.binding x, NoSyn)
2.158 + | [((b, _), mx)] =>
2.159 + let
2.160 + val y = Name.name_of b;
2.161 + val _ = x = y orelse
2.162 + error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
2.163 + Position.str_of (Name.pos_of b));
2.164 + in (b, mx) end);
2.165 val lthy' = lthy
2.166 |> ProofContext.set_syntax_mode mode (* FIXME ?!? *)
2.167 - |> LocalTheory.abbrev mode ((x, mx), rhs) |> snd
2.168 + |> LocalTheory.abbrev mode (var, rhs) |> snd
2.169 |> ProofContext.restore_syntax_mode lthy;
2.170
2.171 val _ = if not do_print then () else print_consts lthy' (K false) [(x, T)];
2.172 @@ -249,11 +264,12 @@
2.173 in ((prems, stmt, []), goal_ctxt) end
2.174 | Element.Obtains obtains =>
2.175 let
2.176 - val case_names = obtains |> map_index
2.177 - (fn (i, ("", _)) => string_of_int (i + 1) | (_, (name, _)) => name);
2.178 + val case_names = obtains |> map_index (fn (i, (binding, _)) =>
2.179 + let val name = Name.name_of binding
2.180 + in if name = "" then string_of_int (i + 1) else name end);
2.181 val constraints = obtains |> map (fn (_, (vars, _)) =>
2.182 Locale.Elem (Element.Constrains
2.183 - (vars |> map_filter (fn (x, SOME T) => SOME (x, T) | _ => NONE))));
2.184 + (vars |> map_filter (fn (x, SOME T) => SOME (Name.name_of x, T) | _ => NONE))));
2.185
2.186 val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
2.187 val (_, loc_ctxt, elems_ctxt, propp) = prep_stmt (elems @ constraints) raw_propp ctxt;
2.188 @@ -262,14 +278,15 @@
2.189
2.190 fun assume_case ((name, (vars, _)), asms) ctxt' =
2.191 let
2.192 - val xs = map fst vars;
2.193 + val bs = map fst vars;
2.194 + val xs = map Name.name_of bs;
2.195 val props = map fst asms;
2.196 - val (parms, _) = ctxt'
2.197 + val (Ts, _) = ctxt'
2.198 |> fold Variable.declare_term props
2.199 |> fold_map ProofContext.inferred_param xs;
2.200 - val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis));
2.201 + val asm = Term.list_all_free (xs ~~ Ts, Logic.list_implies (props, thesis));
2.202 in
2.203 - ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs));
2.204 + ctxt' |> (snd o ProofContext.add_fixes_i (map (fn b => (b, NONE, NoSyn)) bs));
2.205 ctxt' |> Variable.auto_fixes asm
2.206 |> ProofContext.add_assms_i Assumption.assume_export
2.207 [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
2.208 @@ -279,13 +296,13 @@
2.209 val atts = map (Attrib.internal o K)
2.210 [RuleCases.consumes (~ (length obtains)), RuleCases.case_names case_names];
2.211 val prems = subtract_prems loc_ctxt elems_ctxt;
2.212 - val stmt = [(("", atts), [(thesis, [])])];
2.213 + val stmt = [((Name.no_binding, atts), [(thesis, [])])];
2.214
2.215 val (facts, goal_ctxt) = elems_ctxt
2.216 - |> (snd o ProofContext.add_fixes_i [(AutoBind.thesisN, NONE, NoSyn)])
2.217 + |> (snd o ProofContext.add_fixes_i [(Name.binding AutoBind.thesisN, NONE, NoSyn)])
2.218 |> fold_map assume_case (obtains ~~ propp)
2.219 |-> (fn ths => ProofContext.note_thmss_i Thm.assumptionK
2.220 - [((Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
2.221 + [((Name.binding Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
2.222 in ((prems, stmt, facts), goal_ctxt) end);
2.223
2.224 structure TheoremHook = GenericDataFun
2.225 @@ -323,14 +340,20 @@
2.226 lthy
2.227 |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
2.228 |> (fn (res, lthy') =>
2.229 - (ProofDisplay.theory_results lthy' ((kind, name), res);
2.230 - if name = "" andalso null atts then lthy'
2.231 - else #2 (LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])] lthy')))
2.232 + if Name.name_of name = "" andalso null atts then
2.233 + (ProofDisplay.theory_results lthy' ((kind, ""), res); lthy')
2.234 + else
2.235 + let
2.236 + val ([(res_name, _)], lthy'') = lthy'
2.237 + |> LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])];
2.238 + val _ = ProofDisplay.theory_results lthy' ((kind, res_name), res);
2.239 + in lthy'' end)
2.240 |> after_qed results'
2.241 end;
2.242 in
2.243 goal_ctxt
2.244 - |> ProofContext.note_thmss_i Thm.assumptionK [((AutoBind.assmsN, []), [(prems, [])])]
2.245 + |> ProofContext.note_thmss_i Thm.assumptionK
2.246 + [((Name.binding AutoBind.assmsN, []), [(prems, [])])]
2.247 |> snd
2.248 |> Proof.theorem_i before_qed after_qed' (map snd stmt)
2.249 |> Proof.refine_insert facts