author | wenzelm |
Mon, 09 Oct 2006 02:20:01 +0200 | |
changeset 20908 | 5f7458cc4f67 |
parent 20363 | f34c5dbe74d5 |
child 20959 | 34cfe3bbeff4 |
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 |
19632 | 11 |
val add_defs: (bool * bool) * ((bstring * string) * Attrib.src list) list -> theory -> theory |
18418
bf448d999b7e
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset
|
12 |
val apply_theorems: (thmref * Attrib.src list) list -> theory -> thm list * theory |
18728 | 13 |
val apply_theorems_i: (thm list * attribute list) list -> theory -> thm list * theory |
19585 | 14 |
val have: ((string * Attrib.src list) * (string * string list) list) 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
|
15 |
bool -> Proof.state -> Proof.state |
19585 | 16 |
val hence: ((string * Attrib.src list) * (string * string list) list) 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
|
17 |
bool -> Proof.state -> Proof.state |
19585 | 18 |
val show: ((string * Attrib.src list) * (string * string list) list) 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
|
19 |
bool -> Proof.state -> Proof.state |
19585 | 20 |
val thus: ((string * Attrib.src list) * (string * string list) list) list -> |
21 |
bool -> Proof.state -> Proof.state |
|
22 |
val theorem: string -> string * Attrib.src list -> string * string list -> theory -> Proof.state |
|
23 |
val theorem_i: string -> string * attribute list -> term * term list -> theory -> Proof.state |
|
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
24 |
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
|
25 |
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
|
26 |
Toplevel.transition -> Toplevel.transition |
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
27 |
val default_proof: Toplevel.transition -> Toplevel.transition |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
28 |
val immediate_proof: Toplevel.transition -> Toplevel.transition |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
29 |
val done_proof: Toplevel.transition -> Toplevel.transition |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12848
diff
changeset
|
30 |
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
|
31 |
val begin_theory: string -> string list -> (string * bool) list -> bool -> theory |
6331 | 32 |
val end_theory: theory -> theory |
7932 | 33 |
val kill_theory: string -> unit |
6246 | 34 |
val theory: string * string list * (string * bool) list |
35 |
-> Toplevel.transition -> Toplevel.transition |
|
7960 | 36 |
val init_context: ('a -> unit) -> 'a -> Toplevel.transition -> Toplevel.transition |
6246 | 37 |
val context: string -> Toplevel.transition -> Toplevel.transition |
5830 | 38 |
end; |
39 |
||
40 |
structure IsarThy: ISAR_THY = |
|
41 |
struct |
|
42 |
||
20908
5f7458cc4f67
removed theorems, smart_theorems etc. (cf. Specification.theorems);
wenzelm
parents:
20363
diff
changeset
|
43 |
(* axioms *) |
5830 | 44 |
|
5915 | 45 |
fun add_axms f args thy = |
18728 | 46 |
f (map (fn (x, srcs) => (x, map (Attrib.attribute thy) srcs)) args) thy; |
5915 | 47 |
|
18377 | 48 |
val add_axioms = add_axms (snd oo PureThy.add_axioms); |
19632 | 49 |
|
50 |
fun add_defs ((unchecked, overloaded), args) = |
|
51 |
add_axms |
|
52 |
(snd oo (if unchecked then PureThy.add_defs_unchecked else PureThy.add_defs) overloaded) args; |
|
6371 | 53 |
|
54 |
||
20908
5f7458cc4f67
removed theorems, smart_theorems etc. (cf. Specification.theorems);
wenzelm
parents:
20363
diff
changeset
|
55 |
(* facts *) |
9590 | 56 |
|
20908
5f7458cc4f67
removed theorems, smart_theorems etc. (cf. Specification.theorems);
wenzelm
parents:
20363
diff
changeset
|
57 |
fun apply_theorems args thy = |
5f7458cc4f67
removed theorems, smart_theorems etc. (cf. Specification.theorems);
wenzelm
parents:
20363
diff
changeset
|
58 |
let val facts = Attrib.map_facts (Attrib.attribute thy) [(("", []), args)] |
5f7458cc4f67
removed theorems, smart_theorems etc. (cf. Specification.theorems);
wenzelm
parents:
20363
diff
changeset
|
59 |
in apfst (maps snd) (PureThy.note_thmss "" facts thy) end; |
6371 | 60 |
|
20908
5f7458cc4f67
removed theorems, smart_theorems etc. (cf. Specification.theorems);
wenzelm
parents:
20363
diff
changeset
|
61 |
fun apply_theorems_i args = apfst (maps snd) o PureThy.note_thmss_i "" [(("", []), args)]; |
12705 | 62 |
|
5915 | 63 |
|
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
|
64 |
(* goals *) |
10935 | 65 |
|
66 |
local |
|
67 |
||
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
|
68 |
fun local_goal opt_chain goal stmt int = |
18124 | 69 |
opt_chain #> goal NONE (K Seq.single) stmt int; |
12244 | 70 |
|
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
|
71 |
fun global_goal goal kind a propp thy = |
18124 | 72 |
goal kind NONE (K I) (SOME "") a [(("", []), [propp])] (ProofContext.init thy); |
10935 | 73 |
|
74 |
in |
|
75 |
||
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
|
76 |
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
|
77 |
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
|
78 |
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
|
79 |
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
|
80 |
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
|
81 |
val theorem_i = global_goal Proof.theorem_i; |
11890 | 82 |
|
7271 | 83 |
end; |
84 |
||
5830 | 85 |
|
6404 | 86 |
(* local endings *) |
87 |
||
17900 | 88 |
fun local_qed m = Toplevel.proofs (Proof.local_qed (m, true)); |
89 |
val local_terminal_proof = Toplevel.proofs o Proof.local_terminal_proof; |
|
90 |
val local_default_proof = Toplevel.proofs Proof.local_default_proof; |
|
91 |
val local_immediate_proof = Toplevel.proofs Proof.local_immediate_proof; |
|
92 |
val local_done_proof = Toplevel.proofs Proof.local_done_proof; |
|
93 |
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
|
94 |
|
15237
250e9be7a09d
Some changes to allow skipping of proof scripts.
berghofe
parents:
15206
diff
changeset
|
95 |
val skip_local_qed = |
250e9be7a09d
Some changes to allow skipping of proof scripts.
berghofe
parents:
15206
diff
changeset
|
96 |
Toplevel.skip_proof (History.apply (fn i => if i > 1 then i - 1 else raise Toplevel.UNDEF)); |
6404 | 97 |
|
98 |
||
99 |
(* global endings *) |
|
100 |
||
17900 | 101 |
fun global_ending ending = Toplevel.proof_to_theory_context (fn int => fn state => |
20363
f34c5dbe74d5
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
19632
diff
changeset
|
102 |
if can (Proof.assert_bottom true) state then |
f34c5dbe74d5
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
19632
diff
changeset
|
103 |
ending int state |> (fn ctxt' => (ctxt', ProofContext.theory_of ctxt')) |
18678 | 104 |
else raise Toplevel.UNDEF); |
6404 | 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_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
|
107 |
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
|
108 |
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
|
109 |
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
|
110 |
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
|
111 |
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
|
112 |
|
17900 | 113 |
val skip_global_qed = Toplevel.skip_proof_to_theory (equal 1); |
6404 | 114 |
|
115 |
||
116 |
(* common endings *) |
|
117 |
||
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
|
118 |
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
|
119 |
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
|
120 |
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
|
121 |
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
|
122 |
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
|
123 |
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
|
124 |
|
5830 | 125 |
|
6688 | 126 |
(* theory init and exit *) |
5830 | 127 |
|
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
|
128 |
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
|
129 |
ThyInfo.begin_theory Present.begin_theory name imports (map (apfst Path.unpack) uses); |
5830 | 130 |
|
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
|
131 |
val end_theory = (ThyInfo.check_known_thy o Context.theory_name) ? ThyInfo.end_theory; |
7909 | 132 |
|
7932 | 133 |
val kill_theory = ThyInfo.if_known_thy ThyInfo.remove_thy; |
6688 | 134 |
|
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
|
135 |
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
|
136 |
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
|
137 |
(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
|
138 |
(kill_theory o Context.theory_name); |
6246 | 139 |
|
140 |
||
141 |
(* context switch *) |
|
142 |
||
7960 | 143 |
fun fetch_context f x = |
15531 | 144 |
(case Context.pass NONE f x of |
145 |
((), NONE) => raise Toplevel.UNDEF |
|
146 |
| ((), SOME thy) => thy); |
|
7960 | 147 |
|
148 |
fun init_context f x = Toplevel.init_theory (fn _ => fetch_context f x) (K ()) (K ()); |
|
7953 | 149 |
|
150 |
val context = init_context (ThyInfo.quiet_update_thy true); |
|
6246 | 151 |
|
5830 | 152 |
end; |