author | wenzelm |
Fri, 27 Jan 2006 19:03:16 +0100 | |
changeset 18810 | 6dc5416368e9 |
parent 18804 | d42708f5c186 |
child 19482 | 9f11af8f7ef9 |
permissions | -rw-r--r-- |
5830 | 1 |
(* Title: Pure/Isar/isar_thy.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
||
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
5 |
Derived theory and proof operations. |
5830 | 6 |
*) |
7 |
||
8 |
signature ISAR_THY = |
|
9 |
sig |
|
15703 | 10 |
val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory |
18728 | 11 |
val add_axioms_i: ((bstring * term) * attribute list) list -> theory -> theory |
15703 | 12 |
val add_defs: bool * ((bstring * string) * Attrib.src list) list -> theory -> theory |
18728 | 13 |
val add_defs_i: bool * ((bstring * term) * attribute list) list -> theory -> theory |
18418
bf448d999b7e
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset
|
14 |
val apply_theorems: (thmref * Attrib.src list) list -> theory -> thm list * theory |
18728 | 15 |
val apply_theorems_i: (thm list * attribute list) list -> theory -> thm list * theory |
15703 | 16 |
val theorems: string -> |
17 |
((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list |
|
18418
bf448d999b7e
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset
|
18 |
-> theory -> (string * thm list) list * theory |
12713
c9e3e34dbc45
clarified/added theorems(_i) vs. locale_theorems(_i);
wenzelm
parents:
12705
diff
changeset
|
19 |
val theorems_i: string -> |
18728 | 20 |
((bstring * attribute list) * (thm list * attribute list) list) list |
18418
bf448d999b7e
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset
|
21 |
-> theory -> (string * thm list) list * theory |
12713
c9e3e34dbc45
clarified/added theorems(_i) vs. locale_theorems(_i);
wenzelm
parents:
12705
diff
changeset
|
22 |
val smart_theorems: string -> xstring option -> |
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
23 |
((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list -> |
18804 | 24 |
theory -> Proof.context * theory |
15703 | 25 |
val declare_theorems: xstring option -> |
18804 | 26 |
(thmref * Attrib.src list) list -> theory -> Proof.context * theory |
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
27 |
val have: ((string * Attrib.src list) * (string * (string list * string list)) list) list -> |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
28 |
bool -> Proof.state -> Proof.state |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
29 |
val hence: ((string * Attrib.src list) * (string * (string list * string list)) list) list -> |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
30 |
bool -> Proof.state -> Proof.state |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
31 |
val show: ((string * Attrib.src list) * (string * (string list * string list)) list) list -> |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
32 |
bool -> Proof.state -> Proof.state |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
33 |
val thus: ((string * Attrib.src list) * (string * (string list * string list)) list) list -> |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
34 |
bool -> Proof.state -> Proof.state |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
35 |
val theorem: string -> string * Attrib.src list -> string * (string list * string list) -> |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
36 |
theory -> Proof.state |
18728 | 37 |
val theorem_i: string -> string * attribute list -> term * (term list * term list) -> |
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
38 |
theory -> Proof.state |
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
39 |
val qed: Method.text option -> Toplevel.transition -> Toplevel.transition |
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
40 |
val terminal_proof: Method.text * Method.text option -> |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
41 |
Toplevel.transition -> Toplevel.transition |
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
42 |
val default_proof: Toplevel.transition -> Toplevel.transition |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
43 |
val immediate_proof: Toplevel.transition -> Toplevel.transition |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
44 |
val done_proof: Toplevel.transition -> Toplevel.transition |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
45 |
val skip_proof: Toplevel.transition -> Toplevel.transition |
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
46 |
val begin_theory: string -> string list -> (string * bool) list -> bool -> theory |
6331 | 47 |
val end_theory: theory -> theory |
7932 | 48 |
val kill_theory: string -> unit |
6246 | 49 |
val theory: string * string list * (string * bool) list |
50 |
-> Toplevel.transition -> Toplevel.transition |
|
7960 | 51 |
val init_context: ('a -> unit) -> 'a -> Toplevel.transition -> Toplevel.transition |
6246 | 52 |
val context: string -> Toplevel.transition -> Toplevel.transition |
5830 | 53 |
end; |
54 |
||
55 |
structure IsarThy: ISAR_THY = |
|
56 |
struct |
|
57 |
||
58 |
(* axioms and defs *) |
|
59 |
||
5915 | 60 |
fun add_axms f args thy = |
18728 | 61 |
f (map (fn (x, srcs) => (x, map (Attrib.attribute thy) srcs)) args) thy; |
5915 | 62 |
|
18377 | 63 |
val add_axioms = add_axms (snd oo PureThy.add_axioms); |
64 |
val add_axioms_i = snd oo PureThy.add_axioms_i; |
|
18358 | 65 |
fun add_defs (x, args) = add_axms (snd oo PureThy.add_defs x) args; |
66 |
fun add_defs_i (x, args) = (snd oo PureThy.add_defs_i x) args; |
|
6371 | 67 |
|
68 |
||
5915 | 69 |
(* theorems *) |
70 |
||
18804 | 71 |
fun present_theorems kind (res, thy) = |
72 |
conditional (kind <> "" andalso kind <> PureThy.internalK) (fn () => |
|
73 |
Context.setmp (SOME thy) (Present.results (kind ^ "s")) res); |
|
17108 | 74 |
|
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
75 |
fun theorems kind args thy = thy |
18804 | 76 |
|> PureThy.note_thmss kind (Attrib.map_facts (Attrib.attribute thy) args) |
18418
bf448d999b7e
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset
|
77 |
|> tap (present_theorems kind); |
12713
c9e3e34dbc45
clarified/added theorems(_i) vs. locale_theorems(_i);
wenzelm
parents:
12705
diff
changeset
|
78 |
|
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
79 |
fun theorems_i kind args = |
18804 | 80 |
PureThy.note_thmss_i kind args |
18418
bf448d999b7e
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset
|
81 |
#> tap (present_theorems kind); |
9590 | 82 |
|
18418
bf448d999b7e
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset
|
83 |
fun apply_theorems args = apfst (List.concat o map snd) o theorems "" [(("", []), args)]; |
bf448d999b7e
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset
|
84 |
fun apply_theorems_i args = apfst (List.concat o map snd) o theorems_i "" [(("", []), args)]; |
6371 | 85 |
|
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
86 |
fun smart_theorems kind NONE args thy = thy |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
87 |
|> theorems kind args |
18418
bf448d999b7e
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset
|
88 |
|> tap (present_theorems kind) |
18804 | 89 |
|> (fn (_, thy) => `ProofContext.init thy) |
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
90 |
| smart_theorems kind (SOME loc) args thy = thy |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
91 |
|> Locale.note_thmss kind loc args |
18804 | 92 |
|> tap (fn ((_, res), (_, thy')) => present_theorems kind (res, thy')) |
18421
464c93701351
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18418
diff
changeset
|
93 |
|> #2; |
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
94 |
|
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
95 |
fun declare_theorems opt_loc args = |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
96 |
smart_theorems "" opt_loc [(("", []), args)]; |
12705 | 97 |
|
5915 | 98 |
|
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
99 |
(* goals *) |
10935 | 100 |
|
101 |
local |
|
102 |
||
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
103 |
fun local_goal opt_chain goal stmt int = |
18124 | 104 |
opt_chain #> goal NONE (K Seq.single) stmt int; |
12244 | 105 |
|
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
106 |
fun global_goal goal kind a propp thy = |
18124 | 107 |
goal kind NONE (K I) (SOME "") a [(("", []), [propp])] (ProofContext.init thy); |
10935 | 108 |
|
109 |
in |
|
110 |
||
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
111 |
val have = local_goal I Proof.have; |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
112 |
val hence = local_goal Proof.chain Proof.have; |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
113 |
val show = local_goal I Proof.show; |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
114 |
val thus = local_goal Proof.chain Proof.show; |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
115 |
val theorem = global_goal Proof.theorem; |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
116 |
val theorem_i = global_goal Proof.theorem_i; |
11890 | 117 |
|
7271 | 118 |
end; |
119 |
||
5830 | 120 |
|
6404 | 121 |
(* local endings *) |
122 |
||
17900 | 123 |
fun local_qed m = Toplevel.proofs (Proof.local_qed (m, true)); |
124 |
val local_terminal_proof = Toplevel.proofs o Proof.local_terminal_proof; |
|
125 |
val local_default_proof = Toplevel.proofs Proof.local_default_proof; |
|
126 |
val local_immediate_proof = Toplevel.proofs Proof.local_immediate_proof; |
|
127 |
val local_done_proof = Toplevel.proofs Proof.local_done_proof; |
|
128 |
val local_skip_proof = Toplevel.proofs' Proof.local_skip_proof; |
|
16605
4590c1f79050
added print_mode three_buffersN and corresponding cond_print;
wenzelm
parents:
16529
diff
changeset
|
129 |
|
15237
250e9be7a09d
Some changes to allow skipping of proof scripts.
berghofe
parents:
15206
diff
changeset
|
130 |
val skip_local_qed = |
250e9be7a09d
Some changes to allow skipping of proof scripts.
berghofe
parents:
15206
diff
changeset
|
131 |
Toplevel.skip_proof (History.apply (fn i => if i > 1 then i - 1 else raise Toplevel.UNDEF)); |
6404 | 132 |
|
133 |
||
134 |
(* global endings *) |
|
135 |
||
17900 | 136 |
fun global_ending ending = Toplevel.proof_to_theory_context (fn int => fn state => |
18678 | 137 |
if can (Proof.assert_bottom true) state then ending int state |
138 |
else raise Toplevel.UNDEF); |
|
6404 | 139 |
|
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
140 |
fun global_qed m = global_ending (K (Proof.global_qed (m, true))); |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
141 |
val global_terminal_proof = global_ending o K o Proof.global_terminal_proof; |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
142 |
val global_default_proof = global_ending (K Proof.global_default_proof); |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
143 |
val global_immediate_proof = global_ending (K Proof.global_immediate_proof); |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
144 |
val global_skip_proof = global_ending Proof.global_skip_proof; |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
145 |
val global_done_proof = global_ending (K Proof.global_done_proof); |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
146 |
|
17900 | 147 |
val skip_global_qed = Toplevel.skip_proof_to_theory (equal 1); |
6404 | 148 |
|
149 |
||
150 |
(* common endings *) |
|
151 |
||
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
152 |
fun qed m = local_qed m o global_qed m o skip_local_qed o skip_global_qed; |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
153 |
fun terminal_proof m = local_terminal_proof m o global_terminal_proof m; |
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
154 |
val default_proof = local_default_proof o global_default_proof; |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
155 |
val immediate_proof = local_immediate_proof o global_immediate_proof; |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
156 |
val done_proof = local_done_proof o global_done_proof; |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
157 |
val skip_proof = local_skip_proof o global_skip_proof; |
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
158 |
|
5830 | 159 |
|
6688 | 160 |
(* theory init and exit *) |
5830 | 161 |
|
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
162 |
fun begin_theory name imports uses = |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
163 |
ThyInfo.begin_theory Present.begin_theory name imports (map (apfst Path.unpack) uses); |
5830 | 164 |
|
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
165 |
val end_theory = (ThyInfo.check_known_thy o Context.theory_name) ? ThyInfo.end_theory; |
7909 | 166 |
|
7932 | 167 |
val kill_theory = ThyInfo.if_known_thy ThyInfo.remove_thy; |
6688 | 168 |
|
17354
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
169 |
fun theory (name, imports, uses) = |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
170 |
Toplevel.init_theory (begin_theory name imports uses) |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
171 |
(fn thy => (end_theory thy; ())) |
4d92517aa7f4
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
wenzelm
parents:
17184
diff
changeset
|
172 |
(kill_theory o Context.theory_name); |
6246 | 173 |
|
174 |
||
175 |
(* context switch *) |
|
176 |
||
7960 | 177 |
fun fetch_context f x = |
15531 | 178 |
(case Context.pass NONE f x of |
179 |
((), NONE) => raise Toplevel.UNDEF |
|
180 |
| ((), SOME thy) => thy); |
|
7960 | 181 |
|
182 |
fun init_context f x = Toplevel.init_theory (fn _ => fetch_context f x) (K ()) (K ()); |
|
7953 | 183 |
|
184 |
val context = init_context (ThyInfo.quiet_update_thy true); |
|
6246 | 185 |
|
5830 | 186 |
end; |