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 
TODO:


8 
 'methods' section (proof macros, ML method defs) (!?);

5882

9 
 next_block: ProofHistory open / close (!?);

5830

10 
*)


11 


12 
signature ISAR_THY =


13 
sig

5959

14 
val add_text: string > theory > theory

6354

15 
val add_title: string > string > string > theory > theory

5959

16 
val add_chapter: string > theory > theory


17 
val add_section: string > theory > theory


18 
val add_subsection: string > theory > theory


19 
val add_subsubsection: string > theory > theory

5830

20 
val add_axioms: ((bstring * string) * Args.src list) list > theory > theory

6371

21 
val add_axioms_i: ((bstring * term) * theory attribute list) list > theory > theory

5830

22 
val add_defs: ((bstring * string) * Args.src list) list > theory > theory

6371

23 
val add_defs_i: ((bstring * term) * theory attribute list) list > theory > theory


24 
val add_constdefs: ((bstring * string * mixfix) * string) list > theory > theory


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


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


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

5915

28 
val have_theorems: (bstring * Args.src list) * (xstring * Args.src list) list


29 
> theory > theory

6371

30 
val have_theorems_i: (bstring * theory attribute list) * (thm * theory attribute list) list


31 
> theory > theory

5915

32 
val have_lemmas: (bstring * Args.src list) * (xstring * Args.src list) list


33 
> theory > theory

6371

34 
val have_lemmas_i: (bstring * theory attribute list) * (thm * theory attribute list) list


35 
> theory > theory

5915

36 
val have_facts: (string * Args.src list) * (string * Args.src list) list


37 
> ProofHistory.T > ProofHistory.T

6371

38 
val have_facts_i: (string * Proof.context attribute list) *


39 
(thm * Proof.context attribute list) list > ProofHistory.T > ProofHistory.T


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


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


42 
val chain: ProofHistory.T > ProofHistory.T

5830

43 
val fix: (string * string option) list > ProofHistory.T > ProofHistory.T

6371

44 
val fix_i: (string * typ) list > ProofHistory.T > ProofHistory.T

5938

45 
val match_bind: (string list * string) list > ProofHistory.T > ProofHistory.T

6371

46 
val match_bind_i: (term list * term) list > ProofHistory.T > ProofHistory.T

5938

47 
val theorem: string > Args.src list > string * string list > theory > ProofHistory.T

6371

48 
val theorem_i: bstring > theory attribute list > term * term list > theory > ProofHistory.T

5938

49 
val lemma: string > Args.src list > string * string list > theory > ProofHistory.T

6371

50 
val lemma_i: bstring > theory attribute list > term * term list > 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 


108 
fun add_text (txt:string) (thy:theory) = 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 

6371

187 
fun global_statement f name src s thy =


188 
ProofHistory.init (f name (map (Attrib.global_attribute thy) src) s thy);

5830

189 

6501

190 
fun global_statement_i f name atts t thy = ProofHistory.init (f name atts t thy);


191 


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


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

6371

194 

6501

195 
fun local_statement_i do_open f g name atts t =


196 
ProofHistory.apply_cond_open do_open (f name atts t o g);

5830

197 

6501

198 
val theorem = global_statement Proof.theorem;

6371

199 
val theorem_i = global_statement_i Proof.theorem_i;

6501

200 
val lemma = global_statement Proof.lemma;


201 
val lemma_i = global_statement_i Proof.lemma_i;


202 
val assume = local_statement false Proof.assume I;


203 
val assume_i = local_statement_i false Proof.assume_i I;


204 
val show = local_statement true Proof.show I;


205 
val show_i = local_statement_i true Proof.show_i I;


206 
val have = local_statement true Proof.have I;


207 
val have_i = local_statement_i true Proof.have_i I;


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


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


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


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

5830

212 


213 


214 
(* blocks *)


215 


216 
val begin_block = ProofHistory.apply_open Proof.begin_block;


217 
val next_block = ProofHistory.apply Proof.next_block;

6404

218 
val end_block = ProofHistory.apply_close Proof.end_block;

5830

219 


220 


221 
(* backward steps *)


222 


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

5882

224 
val then_tac = ProofHistory.applys o Method.then_tac;

5830

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

6404

226 


227 


228 
(* local endings *)


229 


230 
val local_qed = Toplevel.proof o ProofHistory.applys_close o Method.local_qed;


231 
val local_terminal_proof = Toplevel.proof o ProofHistory.applys_close o Method.local_terminal_proof;


232 
val local_immediate_proof = Toplevel.proof (ProofHistory.applys_close Method.local_immediate_proof);


233 
val local_default_proof = Toplevel.proof (ProofHistory.applys_close Method.local_default_proof);


234 


235 


236 
(* global endings *)


237 


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


239 


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


241 
let


242 
val state = ProofHistory.current prf;


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


244 
val (thy, (kind, name, thm)) = finish state;


245 


246 
val prt_result = Pretty.block


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


248 
in Pretty.writeln prt_result; thy end);


249 


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


251 
let


252 
val thy = Proof.theory_of state;


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


254 
in Method.global_qed alt_name alt_atts opt_text state end;


255 


256 
val global_qed_with = global_result oo gen_global_qed_with Attrib.global_attribute;


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


258 
val global_qed = global_qed_with (None, None);


259 


260 
val global_terminal_proof = global_result o Method.global_terminal_proof;


261 
val global_immediate_proof = global_result Method.global_immediate_proof;


262 
val global_default_proof = global_result Method.global_default_proof;


263 


264 


265 
(* common endings *)


266 


267 
fun qed opt_text = local_qed opt_text o global_qed opt_text;


268 
fun terminal_proof opt_text = local_terminal_proof opt_text o global_terminal_proof opt_text;


269 
val immediate_proof = local_immediate_proof o global_immediate_proof;


270 
val default_proof = local_default_proof o global_default_proof;

5830

271 


272 


273 
(* use ML text *)


274 

6331

275 
fun use_mltext txt opt_thy = #2 (Context.pass opt_thy (use_text false) txt);


276 
fun use_mltext_theory txt thy = #2 (Context.pass_theory thy (use_text false) txt);

5830

277 


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


279 


280 
fun use_let name body txt =


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


282 


283 
val use_setup =

5915

284 
use_let "setup: (theory > theory) list" "Library.apply setup";

5830

285 


286 


287 
(* translation functions *)


288 


289 
val parse_ast_translation =


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


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


292 


293 
val parse_translation =


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


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


296 


297 
val print_translation =


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


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


300 


301 
val print_ast_translation =


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


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


304 


305 
val typed_print_translation =


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


307 
"Theory.add_trfunsT typed_print_translation";


308 


309 
val token_translation =


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


311 
"Theory.add_tokentrfuns token_translation";


312 


313 


314 
(* add_oracle *)


315 


316 
fun add_oracle (name, txt) =


317 
use_let


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


319 
"Theory.add_oracle oracle"


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


321 


322 

6371

323 
(* theory init and exit *) (* FIXME move? rearrange? *)

5830

324 

6331

325 
fun begin_theory name parents files =

6266

326 
let

6331

327 
val paths = map (apfst Path.unpack) files;


328 
val thy = ThyInfo.begin_theory name parents paths;


329 
in Present.begin_theory name parents paths; thy end;

5830

330 

6331

331 


332 
(* FIXME

5830

333 
fun end_theory thy =


334 
let val thy' = PureThy.end_theory thy in

6331

335 
Present.end_theory (PureThy.get_name thy');

6198

336 
transform_error ThyInfo.put_theory thy'

5830

337 
handle exn => raise PureThy.ROLLBACK (thy', Some exn) (* FIXME !!?? *)


338 
end;

6331

339 
*)

5830

340 

6331

341 
fun end_theory thy =


342 
(Present.end_theory (PureThy.get_name thy); ThyInfo.end_theory thy);


343 


344 
fun bg_theory (name, parents, files) () = begin_theory name parents files;


345 
fun en_theory thy = (end_theory thy; ());


346 


347 
fun theory spec = Toplevel.init_theory (bg_theory spec) en_theory;

6246

348 


349 


350 
(* context switch *)


351 

6483

352 
fun switch_theory load s =


353 
Toplevel.init_theory (fn () => (the (#2 (Context.pass None load s)))) (K ());

6246

354 


355 
val context = switch_theory ThyInfo.use_thy;


356 
val update_context = switch_theory ThyInfo.update_thy;


357 

5830

358 


359 
end;
