author  wenzelm 
Fri, 21 May 1999 11:43:34 +0200  
changeset 6688  f33c89103fb4 
parent 6650  808a3d9e2404 
child 6728  b51b25db7bc6 
permissions  rwrr 
5830  1 
(* Title: Pure/Isar/isar_thy.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

6371  5 
Pure/Isar derived theory operations. 
5830  6 
*) 
7 

8 
signature ISAR_THY = 

9 
sig 

6552  10 
val add_text: Comment.text > theory > theory 
11 
val add_title: Comment.text > Comment.text > Comment.text > theory > theory 

12 
val add_chapter: Comment.text > theory > theory 

13 
val add_section: Comment.text > theory > theory 

14 
val add_subsection: Comment.text > theory > theory 

15 
val add_subsubsection: Comment.text > theory > theory 

5830  16 
val add_axioms: ((bstring * string) * Args.src list) list > theory > theory 
6371  17 
val add_axioms_i: ((bstring * term) * theory attribute list) list > theory > theory 
5830  18 
val add_defs: ((bstring * string) * Args.src list) list > theory > theory 
6371  19 
val add_defs_i: ((bstring * term) * theory attribute list) list > theory > theory 
20 
val add_constdefs: ((bstring * string * mixfix) * string) list > theory > theory 

21 
val add_constdefs_i: ((bstring * typ * mixfix) * term) list > theory > theory 

22 
val apply_theorems: (xstring * Args.src list) list > theory > theory * thm list 

23 
val apply_theorems_i: (thm * theory attribute list) list > theory > theory * thm list 

5915  24 
val have_theorems: (bstring * Args.src list) * (xstring * Args.src list) list 
25 
> theory > theory 

6371  26 
val have_theorems_i: (bstring * theory attribute list) * (thm * theory attribute list) list 
27 
> theory > theory 

5915  28 
val have_lemmas: (bstring * Args.src list) * (xstring * Args.src list) list 
29 
> theory > theory 

6371  30 
val have_lemmas_i: (bstring * theory attribute list) * (thm * theory attribute list) list 
31 
> theory > theory 

5915  32 
val have_facts: (string * Args.src list) * (string * Args.src list) list 
33 
> ProofHistory.T > ProofHistory.T 

6371  34 
val have_facts_i: (string * Proof.context attribute list) * 
35 
(thm * Proof.context attribute list) list > ProofHistory.T > ProofHistory.T 

36 
val from_facts: (string * Args.src list) list > ProofHistory.T > ProofHistory.T 

37 
val from_facts_i: (thm * Proof.context attribute list) list > ProofHistory.T > ProofHistory.T 

38 
val chain: ProofHistory.T > ProofHistory.T 

5830  39 
val fix: (string * string option) list > ProofHistory.T > ProofHistory.T 
6371  40 
val fix_i: (string * typ) list > ProofHistory.T > ProofHistory.T 
5938  41 
val match_bind: (string list * string) list > ProofHistory.T > ProofHistory.T 
6371  42 
val match_bind_i: (term list * term) list > ProofHistory.T > ProofHistory.T 
6688  43 
val theorem: string > Args.src list > string * string list 
44 
> bool > theory > ProofHistory.T 

45 
val theorem_i: bstring > theory attribute list > term * term list 

46 
> bool > theory > ProofHistory.T 

47 
val lemma: string > Args.src list > string * string list 

48 
> bool > theory > ProofHistory.T 

49 
val lemma_i: bstring > theory attribute list > term * term list 

50 
> bool > theory > ProofHistory.T 

5938  51 
val assume: string > Args.src list > (string * string list) list 
52 
> ProofHistory.T > ProofHistory.T 

6371  53 
val assume_i: string > Proof.context attribute list > (term * term list) list 
54 
> ProofHistory.T > ProofHistory.T 

5938  55 
val show: string > Args.src list > string * string list > ProofHistory.T > ProofHistory.T 
6371  56 
val show_i: string > Proof.context attribute list > term * term list 
57 
> ProofHistory.T > ProofHistory.T 

5938  58 
val have: string > Args.src list > string * string list > ProofHistory.T > ProofHistory.T 
6371  59 
val have_i: string > Proof.context attribute list > term * term list 
60 
> ProofHistory.T > ProofHistory.T 

6501  61 
val thus: string > Args.src list > string * string list > ProofHistory.T > ProofHistory.T 
62 
val thus_i: string > Proof.context attribute list > term * term list 

63 
> ProofHistory.T > ProofHistory.T 

64 
val hence: string > Args.src list > string * string list > ProofHistory.T > ProofHistory.T 

65 
val hence_i: string > Proof.context attribute list > term * term list 

66 
> ProofHistory.T > ProofHistory.T 

5830  67 
val begin_block: ProofHistory.T > ProofHistory.T 
68 
val next_block: ProofHistory.T > ProofHistory.T 

69 
val end_block: ProofHistory.T > ProofHistory.T 

70 
val tac: Method.text > ProofHistory.T > ProofHistory.T 

5882  71 
val then_tac: Method.text > ProofHistory.T > ProofHistory.T 
5830  72 
val proof: Method.text option > ProofHistory.T > ProofHistory.T 
6404  73 
val kill_proof: ProofHistory.T > theory 
74 
val global_qed_with: bstring option * Args.src list option > Method.text option 

75 
> Toplevel.transition > Toplevel.transition 

76 
val global_qed_with_i: bstring option * theory attribute list option > Method.text option 

77 
> Toplevel.transition > Toplevel.transition 

78 
val qed: Method.text option > Toplevel.transition > Toplevel.transition 

79 
val terminal_proof: Method.text > Toplevel.transition > Toplevel.transition 

80 
val immediate_proof: Toplevel.transition > Toplevel.transition 

81 
val default_proof: Toplevel.transition > Toplevel.transition 

5830  82 
val use_mltext: string > theory option > theory option 
83 
val use_mltext_theory: string > theory > theory 

84 
val use_setup: string > theory > theory 

85 
val parse_ast_translation: string > theory > theory 

86 
val parse_translation: string > theory > theory 

87 
val print_translation: string > theory > theory 

88 
val typed_print_translation: string > theory > theory 

89 
val print_ast_translation: string > theory > theory 

90 
val token_translation: string > theory > theory 

91 
val add_oracle: bstring * string > theory > theory 

6331  92 
val begin_theory: string > string list > (string * bool) list > theory 
93 
val end_theory: theory > theory 

6246  94 
val theory: string * string list * (string * bool) list 
95 
> Toplevel.transition > Toplevel.transition 

96 
val context: string > Toplevel.transition > Toplevel.transition 

97 
val update_context: string > Toplevel.transition > Toplevel.transition 

5830  98 
end; 
99 

100 
structure IsarThy: ISAR_THY = 

101 
struct 

102 

103 

104 
(** derived theory and proof operations **) 

105 

6371  106 
(* formal comments *) (* FIXME dummy *) 
5959  107 

6552  108 
fun add_text _ thy = thy; 
6354  109 
fun add_title title author date thy = thy; 
5959  110 
val add_chapter = add_text; 
111 
val add_section = add_text; 

112 
val add_subsection = add_text; 

113 
val add_subsubsection = add_text; 

114 

115 

5830  116 
(* axioms and defs *) 
117 

5915  118 
fun add_axms f args thy = 
119 
f (map (fn (x, srcs) => (x, map (Attrib.global_attribute thy) srcs)) args) thy; 

120 

121 
val add_axioms = add_axms PureThy.add_axioms; 

6371  122 
val add_axioms_i = PureThy.add_axioms_i; 
5915  123 
val add_defs = add_axms PureThy.add_defs; 
6371  124 
val add_defs_i = PureThy.add_defs_i; 
125 

126 

127 
(* constdefs *) 

128 

129 
fun gen_add_constdefs consts defs args thy = 

130 
thy 

131 
> consts (map fst args) 

132 
> defs (map (fn ((c, _, mx), s) => ((Thm.def_name (Syntax.const_name c mx), s), [])) args); 

133 

134 
val add_constdefs = gen_add_constdefs Theory.add_consts add_defs; 

135 
val add_constdefs_i = gen_add_constdefs Theory.add_consts_i add_defs_i; 

5915  136 

137 

138 
(* theorems *) 

139 

140 
fun gen_have_thmss get attrib f ((name, more_srcs), th_srcs) x = 

141 
f name (map (attrib x) more_srcs) 

142 
(map (fn (s, srcs) => (get x s, map (attrib x) srcs)) th_srcs) x; 

143 

6371  144 
fun global_have_thmss x = gen_have_thmss PureThy.get_thms Attrib.global_attribute x; 
5915  145 

6371  146 
fun local_have_thmss x = 
147 
gen_have_thmss (ProofContext.get_thms o Proof.context_of) 

148 
(Attrib.local_attribute o Proof.theory_of) x; 

149 

150 
fun have_thmss_i f ((name, more_atts), th_atts) = 

151 
f name more_atts (map (apfst single) th_atts); 

152 

153 
fun have_lemss name atts = PureThy.have_thmss name (atts @ [Drule.tag_lemma]); 

5915  154 

155 

6371  156 
fun apply_theorems th_srcs = global_have_thmss PureThy.have_thmss ((None, []), th_srcs); 
157 
fun apply_theorems_i th_srcs = have_thmss_i PureThy.have_thmss ((None, []), th_srcs); 

158 
val have_theorems = #1 oo global_have_thmss (PureThy.have_thmss o Some); 

159 
val have_theorems_i = #1 oo have_thmss_i (PureThy.have_thmss o Some); 

160 
val have_lemmas = #1 oo global_have_thmss (have_lemss o Some); 

161 
val have_lemmas_i = #1 oo have_thmss_i (have_lemss o Some); 

162 
val have_facts = ProofHistory.apply o local_have_thmss Proof.have_thmss; 

163 
val have_facts_i = ProofHistory.apply o have_thmss_i Proof.have_thmss; 

164 

5915  165 

6371  166 
(* forward chaining *) 
167 

168 
val from_facts = 

169 
ProofHistory.apply o (Proof.chain oo curry (local_have_thmss Proof.have_thmss) ("", [])); 

170 

171 
val from_facts_i = 

172 
ProofHistory.apply o (Proof.chain oo curry (have_thmss_i Proof.have_thmss) ("", [])); 

173 

174 
val chain = ProofHistory.apply Proof.chain; 

5830  175 

176 

177 
(* context *) 

178 

179 
val fix = ProofHistory.apply o Proof.fix; 

6371  180 
val fix_i = ProofHistory.apply o Proof.fix_i; 
5830  181 
val match_bind = ProofHistory.apply o Proof.match_bind; 
6371  182 
val match_bind_i = ProofHistory.apply o Proof.match_bind_i; 
5830  183 

184 

185 
(* statements *) 

186 

6688  187 
fun global_statement f name src s int thy = 
188 
ProofHistory.init (Toplevel.undo_limit int) 

189 
(f name (map (Attrib.global_attribute thy) src) s thy); 

5830  190 

6688  191 
fun global_statement_i f name atts t int thy = 
192 
ProofHistory.init (Toplevel.undo_limit int) (f name atts t thy); 

6501  193 

194 
fun local_statement do_open f g name src s = ProofHistory.apply_cond_open do_open (fn state => 

195 
f name (map (Attrib.local_attribute (Proof.theory_of state)) src) s (g state)); 

6371  196 

6501  197 
fun local_statement_i do_open f g name atts t = 
198 
ProofHistory.apply_cond_open do_open (f name atts t o g); 

5830  199 

6501  200 
val theorem = global_statement Proof.theorem; 
6371  201 
val theorem_i = global_statement_i Proof.theorem_i; 
6501  202 
val lemma = global_statement Proof.lemma; 
203 
val lemma_i = global_statement_i Proof.lemma_i; 

204 
val assume = local_statement false Proof.assume I; 

205 
val assume_i = local_statement_i false Proof.assume_i I; 

206 
val show = local_statement true Proof.show I; 

207 
val show_i = local_statement_i true Proof.show_i I; 

208 
val have = local_statement true Proof.have I; 

209 
val have_i = local_statement_i true Proof.have_i I; 

210 
val thus = local_statement true Proof.show Proof.chain; 

211 
val thus_i = local_statement_i true Proof.show_i Proof.chain; 

212 
val hence = local_statement true Proof.have Proof.chain; 

213 
val hence_i = local_statement_i true Proof.have_i Proof.chain; 

5830  214 

215 

216 
(* blocks *) 

217 

218 
val begin_block = ProofHistory.apply_open Proof.begin_block; 

219 
val next_block = ProofHistory.apply Proof.next_block; 

6404  220 
val end_block = ProofHistory.apply_close Proof.end_block; 
5830  221 

222 

223 
(* backward steps *) 

224 

225 
val tac = ProofHistory.applys o Method.tac; 

5882  226 
val then_tac = ProofHistory.applys o Method.then_tac; 
5830  227 
val proof = ProofHistory.applys o Method.proof; 
6404  228 

229 

230 
(* local endings *) 

231 

6688  232 
val local_qed = Toplevel.proof' o (ProofHistory.applys_close oo Method.local_qed); 
233 
val local_terminal_proof = 

234 
Toplevel.proof' o (ProofHistory.applys_close oo Method.local_terminal_proof); 

235 
val local_immediate_proof = 

236 
Toplevel.proof' (ProofHistory.applys_close o Method.local_immediate_proof); 

237 
val local_default_proof = 

238 
Toplevel.proof' (ProofHistory.applys_close o Method.local_default_proof); 

6404  239 

240 

241 
(* global endings *) 

242 

243 
val kill_proof = Proof.theory_of o ProofHistory.current; 

244 

245 
fun global_result finish = Toplevel.proof_to_theory (fn prf => 

246 
let 

247 
val state = ProofHistory.current prf; 

248 
val _ = if Proof.at_bottom state then () else raise Toplevel.UNDEF; 

6531  249 
val (thy, {kind, name, thm}) = finish state; 
6404  250 

251 
val prt_result = Pretty.block 

252 
[Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Display.pretty_thm thm]; 

253 
in Pretty.writeln prt_result; thy end); 

254 

255 
fun gen_global_qed_with prep_att (alt_name, raw_atts) opt_text state = 

256 
let 

257 
val thy = Proof.theory_of state; 

258 
val alt_atts = apsome (map (prep_att thy)) raw_atts; 

259 
in Method.global_qed alt_name alt_atts opt_text state end; 

260 

261 
val global_qed_with = global_result oo gen_global_qed_with Attrib.global_attribute; 

262 
val global_qed_with_i = global_result oo gen_global_qed_with (K I); 

263 
val global_qed = global_qed_with (None, None); 

264 

265 
val global_terminal_proof = global_result o Method.global_terminal_proof; 

266 
val global_immediate_proof = global_result Method.global_immediate_proof; 

267 
val global_default_proof = global_result Method.global_default_proof; 

268 

269 

270 
(* common endings *) 

271 

272 
fun qed opt_text = local_qed opt_text o global_qed opt_text; 

273 
fun terminal_proof opt_text = local_terminal_proof opt_text o global_terminal_proof opt_text; 

274 
val immediate_proof = local_immediate_proof o global_immediate_proof; 

275 
val default_proof = local_default_proof o global_default_proof; 

5830  276 

277 

278 
(* use ML text *) 

279 

6331  280 
fun use_mltext txt opt_thy = #2 (Context.pass opt_thy (use_text false) txt); 
281 
fun use_mltext_theory txt thy = #2 (Context.pass_theory thy (use_text false) txt); 

5830  282 

283 
fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");"); 

284 

285 
fun use_let name body txt = 

286 
use_context ("let val " ^ name ^ " = " ^ txt ^ " in\n" ^ body ^ " end"); 

287 

288 
val use_setup = 

5915  289 
use_let "setup: (theory > theory) list" "Library.apply setup"; 
5830  290 

291 

292 
(* translation functions *) 

293 

294 
val parse_ast_translation = 

295 
use_let "parse_ast_translation: (string * (Syntax.ast list > Syntax.ast)) list" 

296 
"Theory.add_trfuns (parse_ast_translation, [], [], [])"; 

297 

298 
val parse_translation = 

299 
use_let "parse_translation: (string * (term list > term)) list" 

300 
"Theory.add_trfuns ([], parse_translation, [], [])"; 

301 

302 
val print_translation = 

303 
use_let "print_translation: (string * (term list > term)) list" 

304 
"Theory.add_trfuns ([], [], print_translation, [])"; 

305 

306 
val print_ast_translation = 

307 
use_let "print_ast_translation: (string * (Syntax.ast list > Syntax.ast)) list" 

308 
"Theory.add_trfuns ([], [], [], print_ast_translation)"; 

309 

310 
val typed_print_translation = 

311 
use_let "typed_print_translation: (string * (bool > typ > term list > term)) list" 

312 
"Theory.add_trfunsT typed_print_translation"; 

313 

314 
val token_translation = 

315 
use_let "token_translation: (string * string * (string > string * int)) list" 

316 
"Theory.add_tokentrfuns token_translation"; 

317 

318 

319 
(* add_oracle *) 

320 

321 
fun add_oracle (name, txt) = 

322 
use_let 

323 
"oracle: bstring * (Sign.sg * Object.T > term)" 

324 
"Theory.add_oracle oracle" 

325 
("(" ^ quote name ^ ", " ^ txt ^ ")"); 

326 

327 

6688  328 
(* theory init and exit *) 
5830  329 

6331  330 
fun begin_theory name parents files = 
6266  331 
let 
6331  332 
val paths = map (apfst Path.unpack) files; 
333 
val thy = ThyInfo.begin_theory name parents paths; 

6650
808a3d9e2404
Present.begin_theory now needs an additional argument of type
berghofe
parents:
6552
diff
changeset

334 
in Present.begin_theory name parents paths thy end; 
5830  335 

6331  336 
fun end_theory thy = 
337 
(Present.end_theory (PureThy.get_name thy); ThyInfo.end_theory thy); 

338 

6688  339 
fun kill_theory thy = ThyInfo.remove_thy (PureThy.get_name thy); 
340 

6331  341 
fun bg_theory (name, parents, files) () = begin_theory name parents files; 
342 
fun en_theory thy = (end_theory thy; ()); 

343 

6688  344 
fun theory spec = Toplevel.init_theory (bg_theory spec) en_theory kill_theory; 
6246  345 

346 

347 
(* context switch *) 

348 

6483  349 
fun switch_theory load s = 
6688  350 
Toplevel.init_theory (fn () => (the (#2 (Context.pass None load s)))) (K ()) (K ()); 
6246  351 

352 
val context = switch_theory ThyInfo.use_thy; 

353 
val update_context = switch_theory ThyInfo.update_thy; 

354 

5830  355 

356 
end; 