author | wenzelm |
Thu, 06 Sep 2007 12:30:11 +0200 | |
changeset 24542 | f13c59e40617 |
parent 24464 | 58d24cbe5fa6 |
child 24557 | 57e2a5fbde86 |
permissions | -rw-r--r-- |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Isar/specification.ML |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
3 |
Author: Makarius |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
4 |
|
21036 | 5 |
Derived local theory specifications --- with type-inference and |
18810 | 6 |
toplevel polymorphism. |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
7 |
*) |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
8 |
|
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
9 |
signature SPECIFICATION = |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
10 |
sig |
20890 | 11 |
val quiet_mode: bool ref |
12 |
val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit |
|
18771 | 13 |
val read_specification: (string * string option * mixfix) list -> |
18954 | 14 |
((string * Attrib.src list) * string list) list -> local_theory -> |
18771 | 15 |
(((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) * |
18954 | 16 |
local_theory |
18771 | 17 |
val cert_specification: (string * typ option * mixfix) list -> |
18954 | 18 |
((string * Attrib.src list) * term list) list -> local_theory -> |
18771 | 19 |
(((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) * |
18954 | 20 |
local_theory |
21 |
val axiomatization: (string * string option * mixfix) list -> |
|
22 |
((bstring * Attrib.src list) * string list) list -> local_theory -> |
|
23 |
(term list * (bstring * thm list) list) * local_theory |
|
24 |
val axiomatization_i: (string * typ option * mixfix) list -> |
|
25 |
((bstring * Attrib.src list) * term list) list -> local_theory -> |
|
26 |
(term list * (bstring * thm list) list) * local_theory |
|
27 |
val definition: |
|
21705 | 28 |
(string * string option * mixfix) option * ((string * Attrib.src list) * string) -> |
29 |
local_theory -> (term * (bstring * thm)) * local_theory |
|
18954 | 30 |
val definition_i: |
21705 | 31 |
(string * typ option * mixfix) option * ((string * Attrib.src list) * term) -> |
32 |
local_theory -> (term * (bstring * thm)) * local_theory |
|
33 |
val abbreviation: Syntax.mode -> (string * string option * mixfix) option * string -> |
|
21532 | 34 |
local_theory -> local_theory |
21705 | 35 |
val abbreviation_i: Syntax.mode -> (string * typ option * mixfix) option * term -> |
21532 | 36 |
local_theory -> local_theory |
21206
2af4c7b3f7ef
replaced const_syntax by notation, which operates on terms;
wenzelm
parents:
21036
diff
changeset
|
37 |
val notation: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory |
2af4c7b3f7ef
replaced const_syntax by notation, which operates on terms;
wenzelm
parents:
21036
diff
changeset
|
38 |
val notation_i: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory |
20914 | 39 |
val theorems: string -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list |
40 |
-> local_theory -> (bstring * thm list) list * local_theory |
|
41 |
val theorems_i: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list |
|
42 |
-> local_theory -> (bstring * thm list) list * local_theory |
|
21036 | 43 |
val theorem: string -> Method.text option -> (thm list list -> local_theory -> local_theory) -> |
44 |
string * Attrib.src list -> Element.context Locale.element list -> Element.statement -> |
|
24452
93b113c5ac33
- theorem(_i) now also takes "interactive" flag as argument
berghofe
parents:
24219
diff
changeset
|
45 |
bool -> local_theory -> Proof.state |
21036 | 46 |
val theorem_i: string -> Method.text option -> (thm list list -> local_theory -> local_theory) -> |
47 |
string * Attrib.src list -> Element.context_i Locale.element list -> Element.statement_i -> |
|
24452
93b113c5ac33
- theorem(_i) now also takes "interactive" flag as argument
berghofe
parents:
24219
diff
changeset
|
48 |
bool -> local_theory -> Proof.state |
93b113c5ac33
- theorem(_i) now also takes "interactive" flag as argument
berghofe
parents:
24219
diff
changeset
|
49 |
val add_theorem_hook: (bool -> Proof.state -> Proof.state) -> Context.generic -> Context.generic |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
50 |
end; |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
51 |
|
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
52 |
structure Specification: SPECIFICATION = |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
53 |
struct |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
54 |
|
21230
abfdce60b371
theorem statements: incorporate Obtain.statement, tuned;
wenzelm
parents:
21206
diff
changeset
|
55 |
|
20890 | 56 |
(* diagnostics *) |
57 |
||
58 |
val quiet_mode = ref false; |
|
59 |
||
60 |
fun print_consts _ _ [] = () |
|
61 |
| print_consts ctxt pred cs = |
|
62 |
if ! quiet_mode then () else Pretty.writeln (ProofDisplay.pretty_consts ctxt pred cs); |
|
63 |
||
21036 | 64 |
fun present_results ctxt res = |
65 |
if ! quiet_mode then () else ProofDisplay.present_results ctxt res; |
|
66 |
||
67 |
fun present_results' ctxt kind res = present_results ctxt ((kind, ""), res); |
|
20914 | 68 |
|
19664 | 69 |
|
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
70 |
(* prepare specification *) |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
71 |
|
18828 | 72 |
fun prep_specification prep_vars prep_propp prep_att raw_vars raw_specs ctxt = |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
73 |
let |
18670 | 74 |
val thy = ProofContext.theory_of ctxt; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
75 |
|
18670 | 76 |
val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars; |
77 |
val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars; |
|
78 |
val ((specs, vs), specs_ctxt) = |
|
19585 | 79 |
prep_propp (params_ctxt, map (map (rpair []) o snd) raw_specs) |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
80 |
|> swap |>> map (map fst) |
18771 | 81 |
||>> fold_map ProofContext.inferred_param xs; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
82 |
|
18771 | 83 |
val params = vs ~~ map #3 vars; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
84 |
val names = map (fst o fst) raw_specs; |
18670 | 85 |
val atts = map (map (prep_att thy) o snd o fst) raw_specs; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
86 |
in ((params, (names ~~ atts) ~~ specs), specs_ctxt) end; |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
87 |
|
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
88 |
fun read_specification x = |
18771 | 89 |
prep_specification ProofContext.read_vars ProofContext.read_propp Attrib.intern_src x; |
21370
d9dd7b4e5e69
replaced Variable.fix_frees by Variable.auto_fixes (depends on body mode);
wenzelm
parents:
21359
diff
changeset
|
90 |
|
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
91 |
fun cert_specification x = |
18670 | 92 |
prep_specification ProofContext.cert_vars ProofContext.cert_propp (K I) x; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
93 |
|
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
94 |
|
18771 | 95 |
(* axiomatization *) |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
96 |
|
20890 | 97 |
fun gen_axioms prep raw_vars raw_specs lthy = |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
98 |
let |
20890 | 99 |
val (vars, specs) = fst (prep raw_vars raw_specs lthy); |
18828 | 100 |
val cs = map fst vars; |
18880
b8a1c3cdf739
axiomatization: retrict parameters to occurrences in specs;
wenzelm
parents:
18828
diff
changeset
|
101 |
val spec_frees = member (op =) (fold (fold Term.add_frees o snd) specs []); |
18786 | 102 |
|
20890 | 103 |
val ((consts, axioms), lthy') = lthy |
104 |
|> LocalTheory.consts spec_frees vars |
|
21370
d9dd7b4e5e69
replaced Variable.fix_frees by Variable.auto_fixes (depends on body mode);
wenzelm
parents:
21359
diff
changeset
|
105 |
||> fold (fold Variable.auto_fixes o snd) specs (* FIXME !? *) |
21435 | 106 |
||>> LocalTheory.axioms Thm.axiomK specs; |
18786 | 107 |
|
20890 | 108 |
(* FIXME generic target!? *) |
109 |
val hs = map (Term.head_of o #2 o Logic.dest_equals o Thm.prop_of o #2) consts; |
|
110 |
val lthy'' = lthy' |> LocalTheory.theory (Theory.add_finals_i false hs); |
|
111 |
||
112 |
val _ = print_consts lthy' spec_frees cs; |
|
113 |
in ((map #1 consts, axioms), lthy'') end; |
|
18786 | 114 |
|
18954 | 115 |
val axiomatization = gen_axioms read_specification; |
116 |
val axiomatization_i = gen_axioms cert_specification; |
|
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
117 |
|
18786 | 118 |
|
119 |
(* definition *) |
|
120 |
||
21705 | 121 |
fun gen_def prep (raw_var, (raw_a, raw_prop)) lthy = |
18786 | 122 |
let |
21705 | 123 |
val (vars, [((raw_name, atts), [prop])]) = |
124 |
fst (prep (the_list raw_var) [(raw_a, [raw_prop])] lthy); |
|
125 |
val (((x, T), rhs), prove) = LocalDefs.derived_def lthy true prop; |
|
126 |
val name = Thm.def_name_optional x raw_name; |
|
127 |
val mx = (case vars of [] => NoSyn | [((x', _), mx)] => |
|
128 |
if x = x' then mx |
|
129 |
else error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote x')); |
|
130 |
val ((lhs, (_, th)), lthy2) = lthy |
|
22923 | 131 |
|> LocalTheory.def Thm.definitionK ((x, mx), ((name ^ "_raw", []), rhs)); |
21705 | 132 |
val ((b, [th']), lthy3) = lthy2 |
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
21860
diff
changeset
|
133 |
|> LocalTheory.note Thm.definitionK |
24219 | 134 |
((name, Code.add_func_attr false :: atts), [prove lthy2 th]); |
18786 | 135 |
|
21705 | 136 |
val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs; |
137 |
val _ = print_consts lthy3 (member (op =) (Term.add_frees lhs' [])) [(x, T)]; |
|
138 |
in ((lhs, (b, th')), lthy3) end; |
|
18786 | 139 |
|
21705 | 140 |
val definition = gen_def read_specification; |
141 |
val definition_i = gen_def cert_specification; |
|
18786 | 142 |
|
19080 | 143 |
|
144 |
(* abbreviation *) |
|
145 |
||
21705 | 146 |
fun gen_abbrev prep mode (raw_var, raw_prop) lthy = |
19080 | 147 |
let |
21705 | 148 |
val ((vars, [(_, [prop])]), _) = |
149 |
prep (the_list raw_var) [(("", []), [raw_prop])] |
|
21729 | 150 |
(lthy |> ProofContext.set_expand_abbrevs false); |
21705 | 151 |
val ((x, T), rhs) = LocalDefs.abs_def (#2 (LocalDefs.cert_def lthy prop)); |
152 |
val mx = (case vars of [] => NoSyn | [((y, _), mx)] => |
|
153 |
if x = y then mx |
|
154 |
else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y)); |
|
155 |
val lthy' = lthy |
|
156 |
|> ProofContext.set_syntax_mode mode (* FIXME !? *) |
|
21793 | 157 |
|> LocalTheory.abbrev mode ((x, mx), rhs) |> snd |
21705 | 158 |
|> ProofContext.restore_syntax_mode lthy; |
159 |
val _ = print_consts lthy' (K false) [(x, T)] |
|
21532 | 160 |
in lthy' end; |
19080 | 161 |
|
21705 | 162 |
val abbreviation = gen_abbrev read_specification; |
163 |
val abbreviation_i = gen_abbrev cert_specification; |
|
19080 | 164 |
|
19664 | 165 |
|
21230
abfdce60b371
theorem statements: incorporate Obtain.statement, tuned;
wenzelm
parents:
21206
diff
changeset
|
166 |
(* notation *) |
19664 | 167 |
|
21206
2af4c7b3f7ef
replaced const_syntax by notation, which operates on terms;
wenzelm
parents:
21036
diff
changeset
|
168 |
fun gen_notation prep_const mode args lthy = |
21746 | 169 |
lthy |> LocalTheory.notation mode (map (apfst (prep_const lthy)) args); |
19664 | 170 |
|
21206
2af4c7b3f7ef
replaced const_syntax by notation, which operates on terms;
wenzelm
parents:
21036
diff
changeset
|
171 |
val notation = gen_notation ProofContext.read_const; |
2af4c7b3f7ef
replaced const_syntax by notation, which operates on terms;
wenzelm
parents:
21036
diff
changeset
|
172 |
val notation_i = gen_notation (K I); |
19664 | 173 |
|
20914 | 174 |
|
21036 | 175 |
(* fact statements *) |
20914 | 176 |
|
177 |
fun gen_theorems prep_thms prep_att kind raw_facts lthy = |
|
178 |
let |
|
179 |
val attrib = prep_att (ProofContext.theory_of lthy); |
|
180 |
val facts = raw_facts |> map (fn ((name, atts), bs) => |
|
181 |
((name, map attrib atts), |
|
21435 | 182 |
bs |> map (fn (b, more_atts) => (prep_thms lthy b, map attrib more_atts)))); |
183 |
val (res, lthy') = lthy |> LocalTheory.notes kind facts; |
|
21036 | 184 |
val _ = present_results' lthy' kind res; |
20914 | 185 |
in (res, lthy') end; |
186 |
||
187 |
val theorems = gen_theorems ProofContext.get_thms Attrib.intern_src; |
|
188 |
val theorems_i = gen_theorems (K I) (K I); |
|
189 |
||
21036 | 190 |
|
21230
abfdce60b371
theorem statements: incorporate Obtain.statement, tuned;
wenzelm
parents:
21206
diff
changeset
|
191 |
(* complex goal statements *) |
21036 | 192 |
|
193 |
local |
|
194 |
||
21450 | 195 |
fun subtract_prems ctxt1 ctxt2 = |
196 |
Library.drop (length (Assumption.prems_of ctxt1), Assumption.prems_of ctxt2); |
|
197 |
||
21236 | 198 |
fun prep_statement prep_att prep_stmt elems concl ctxt = |
199 |
(case concl of |
|
200 |
Element.Shows shows => |
|
21230
abfdce60b371
theorem statements: incorporate Obtain.statement, tuned;
wenzelm
parents:
21206
diff
changeset
|
201 |
let |
21450 | 202 |
val (_, loc_ctxt, elems_ctxt, propp) = prep_stmt elems (map snd shows) ctxt; |
203 |
val prems = subtract_prems loc_ctxt elems_ctxt; |
|
204 |
val stmt = Attrib.map_specs prep_att (map fst shows ~~ propp); |
|
21370
d9dd7b4e5e69
replaced Variable.fix_frees by Variable.auto_fixes (depends on body mode);
wenzelm
parents:
21359
diff
changeset
|
205 |
val goal_ctxt = fold (fold (Variable.auto_fixes o fst)) propp elems_ctxt; |
21450 | 206 |
in ((prems, stmt, []), goal_ctxt) end |
21236 | 207 |
| Element.Obtains obtains => |
21230
abfdce60b371
theorem statements: incorporate Obtain.statement, tuned;
wenzelm
parents:
21206
diff
changeset
|
208 |
let |
21236 | 209 |
val case_names = obtains |> map_index |
210 |
(fn (i, ("", _)) => string_of_int (i + 1) | (_, (name, _)) => name); |
|
211 |
val constraints = obtains |> map (fn (_, (vars, _)) => |
|
212 |
Locale.Elem (Element.Constrains |
|
213 |
(vars |> map_filter (fn (x, SOME T) => SOME (x, T) | _ => NONE)))); |
|
21036 | 214 |
|
21236 | 215 |
val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props); |
21450 | 216 |
val (_, loc_ctxt, elems_ctxt, propp) = prep_stmt (elems @ constraints) raw_propp ctxt; |
21236 | 217 |
|
218 |
val thesis = ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) AutoBind.thesisN; |
|
21036 | 219 |
|
21236 | 220 |
fun assume_case ((name, (vars, _)), asms) ctxt' = |
221 |
let |
|
222 |
val xs = map fst vars; |
|
223 |
val props = map fst asms; |
|
224 |
val (parms, _) = ctxt' |
|
225 |
|> fold Variable.declare_term props |
|
226 |
|> fold_map ProofContext.inferred_param xs; |
|
227 |
val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis)); |
|
228 |
in |
|
229 |
ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs)); |
|
21370
d9dd7b4e5e69
replaced Variable.fix_frees by Variable.auto_fixes (depends on body mode);
wenzelm
parents:
21359
diff
changeset
|
230 |
ctxt' |> Variable.auto_fixes asm |
21236 | 231 |
|> ProofContext.add_assms_i Assumption.assume_export |
232 |
[((name, [ContextRules.intro_query NONE]), [(asm, [])])] |
|
233 |
|>> (fn [(_, [th])] => th) |
|
234 |
end; |
|
235 |
||
21658 | 236 |
val atts = map (Attrib.internal o K) |
21236 | 237 |
[RuleCases.consumes (~ (length obtains)), RuleCases.case_names case_names]; |
21450 | 238 |
val prems = subtract_prems loc_ctxt elems_ctxt; |
21236 | 239 |
val stmt = [(("", atts), [(thesis, [])])]; |
240 |
||
241 |
val (facts, goal_ctxt) = elems_ctxt |
|
242 |
|> (snd o ProofContext.add_fixes_i [(AutoBind.thesisN, NONE, NoSyn)]) |
|
243 |
|> fold_map assume_case (obtains ~~ propp) |
|
21435 | 244 |
|-> (fn ths => ProofContext.note_thmss_i Thm.assumptionK |
245 |
[((Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths); |
|
21450 | 246 |
in ((prems, stmt, facts), goal_ctxt) end); |
21036 | 247 |
|
24452
93b113c5ac33
- theorem(_i) now also takes "interactive" flag as argument
berghofe
parents:
24219
diff
changeset
|
248 |
structure TheoremHook = GenericDataFun |
93b113c5ac33
- theorem(_i) now also takes "interactive" flag as argument
berghofe
parents:
24219
diff
changeset
|
249 |
( |
93b113c5ac33
- theorem(_i) now also takes "interactive" flag as argument
berghofe
parents:
24219
diff
changeset
|
250 |
type T = ((bool -> Proof.state -> Proof.state) * stamp) list; |
93b113c5ac33
- theorem(_i) now also takes "interactive" flag as argument
berghofe
parents:
24219
diff
changeset
|
251 |
val empty = []; |
93b113c5ac33
- theorem(_i) now also takes "interactive" flag as argument
berghofe
parents:
24219
diff
changeset
|
252 |
val extend = I; |
24464 | 253 |
fun merge _ hooks : T = Library.merge (eq_snd op =) hooks; |
24452
93b113c5ac33
- theorem(_i) now also takes "interactive" flag as argument
berghofe
parents:
24219
diff
changeset
|
254 |
); |
93b113c5ac33
- theorem(_i) now also takes "interactive" flag as argument
berghofe
parents:
24219
diff
changeset
|
255 |
|
21036 | 256 |
fun gen_theorem prep_att prep_stmt |
24452
93b113c5ac33
- theorem(_i) now also takes "interactive" flag as argument
berghofe
parents:
24219
diff
changeset
|
257 |
kind before_qed after_qed (name, raw_atts) raw_elems raw_concl int lthy0 = |
21036 | 258 |
let |
21860 | 259 |
val _ = LocalTheory.affirm lthy0; |
21036 | 260 |
val thy = ProofContext.theory_of lthy0; |
21206
2af4c7b3f7ef
replaced const_syntax by notation, which operates on terms;
wenzelm
parents:
21036
diff
changeset
|
261 |
|
21036 | 262 |
val (loc, ctxt, lthy) = |
263 |
(case (TheoryTarget.peek lthy0, exists (fn Locale.Expr _ => true | _ => false) raw_elems) of |
|
264 |
(SOME loc, true) => (* workaround non-modularity of in/includes *) (* FIXME *) |
|
21275 | 265 |
(SOME loc, ProofContext.init thy, LocalTheory.restore lthy0) |
21036 | 266 |
| _ => (NONE, lthy0, lthy0)); |
267 |
||
21435 | 268 |
val attrib = prep_att thy; |
269 |
val atts = map attrib raw_atts; |
|
270 |
||
21532 | 271 |
val elems = raw_elems |> map (Locale.map_elem (Element.map_ctxt_attrib attrib)); |
21450 | 272 |
val ((prems, stmt, facts), goal_ctxt) = |
273 |
prep_statement attrib (prep_stmt loc) elems raw_concl ctxt; |
|
21036 | 274 |
|
275 |
fun after_qed' results goal_ctxt' = |
|
21602 | 276 |
let val results' = |
277 |
burrow (map Goal.norm_result o ProofContext.export goal_ctxt' lthy) results |
|
278 |
in |
|
21036 | 279 |
lthy |
21435 | 280 |
|> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results') |
21036 | 281 |
|> (fn (res, lthy') => |
282 |
(present_results lthy' ((kind, name), res); |
|
21435 | 283 |
if name = "" andalso null atts then lthy' |
284 |
else #2 (LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])] lthy'))) |
|
21036 | 285 |
|> after_qed results' |
286 |
end; |
|
287 |
in |
|
288 |
goal_ctxt |
|
21450 | 289 |
|> ProofContext.note_thmss_i Thm.assumptionK [((AutoBind.assmsN, []), [(prems, [])])] |
290 |
|> snd |
|
21435 | 291 |
|> Proof.theorem_i before_qed after_qed' (map snd stmt) |
24542 | 292 |
|> Library.apply (map (fn (f, _) => f int) (rev (TheoremHook.get (Context.Proof goal_ctxt)))) |
21036 | 293 |
|> Proof.refine_insert facts |
294 |
end; |
|
295 |
||
21230
abfdce60b371
theorem statements: incorporate Obtain.statement, tuned;
wenzelm
parents:
21206
diff
changeset
|
296 |
in |
abfdce60b371
theorem statements: incorporate Obtain.statement, tuned;
wenzelm
parents:
21206
diff
changeset
|
297 |
|
21036 | 298 |
val theorem = gen_theorem Attrib.intern_src Locale.read_context_statement_i; |
299 |
val theorem_i = gen_theorem (K I) Locale.cert_context_statement; |
|
300 |
||
24452
93b113c5ac33
- theorem(_i) now also takes "interactive" flag as argument
berghofe
parents:
24219
diff
changeset
|
301 |
fun add_theorem_hook f = TheoremHook.map (cons (f, stamp ())); |
93b113c5ac33
- theorem(_i) now also takes "interactive" flag as argument
berghofe
parents:
24219
diff
changeset
|
302 |
|
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
303 |
end; |
21036 | 304 |
|
305 |
end; |