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

5830

61 
val begin_block: ProofHistory.T > ProofHistory.T


62 
val next_block: ProofHistory.T > ProofHistory.T


63 
val end_block: ProofHistory.T > ProofHistory.T


64 
val qed_with: bstring option * Args.src list option > ProofHistory.T > theory

6371

65 
val qed_with_i: bstring option * theory attribute list option > ProofHistory.T > theory

5830

66 
val qed: ProofHistory.T > theory


67 
val kill_proof: ProofHistory.T > theory


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

6371

69 
val tac_i: (Proof.context > Proof.method) > ProofHistory.T > ProofHistory.T

5882

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

6371

71 
val then_tac_i: (Proof.context > Proof.method) > ProofHistory.T > ProofHistory.T

5830

72 
val proof: Method.text option > ProofHistory.T > ProofHistory.T

6371

73 
val proof_i: (Proof.context > Proof.method) option > ProofHistory.T > ProofHistory.T

5830

74 
val terminal_proof: Method.text > ProofHistory.T > ProofHistory.T

6371

75 
val terminal_proof_i: (Proof.context > Proof.method) > ProofHistory.T > ProofHistory.T

6108

76 
val immediate_proof: ProofHistory.T > ProofHistory.T

5830

77 
val default_proof: ProofHistory.T > ProofHistory.T


78 
val use_mltext: string > theory option > theory option


79 
val use_mltext_theory: string > theory > theory


80 
val use_setup: string > theory > theory


81 
val parse_ast_translation: string > theory > theory


82 
val parse_translation: string > theory > theory


83 
val print_translation: string > theory > theory


84 
val typed_print_translation: string > theory > theory


85 
val print_ast_translation: string > theory > theory


86 
val token_translation: string > theory > theory


87 
val add_oracle: bstring * string > theory > theory

6331

88 
val begin_theory: string > string list > (string * bool) list > theory


89 
val end_theory: theory > theory

6246

90 
val theory: string * string list * (string * bool) list


91 
> Toplevel.transition > Toplevel.transition


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


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

5830

94 
end;


95 


96 
structure IsarThy: ISAR_THY =


97 
struct


98 


99 


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


101 

6371

102 
(* formal comments *) (* FIXME dummy *)

5959

103 


104 
fun add_text (txt:string) (thy:theory) = thy;

6354

105 
fun add_title title author date thy = thy;

5959

106 
val add_chapter = add_text;


107 
val add_section = add_text;


108 
val add_subsection = add_text;


109 
val add_subsubsection = add_text;


110 


111 

5830

112 
(* axioms and defs *)


113 

5915

114 
fun add_axms f args thy =


115 
f (map (fn (x, srcs) => (x, map (Attrib.global_attribute thy) srcs)) args) thy;


116 


117 
val add_axioms = add_axms PureThy.add_axioms;

6371

118 
val add_axioms_i = PureThy.add_axioms_i;

5915

119 
val add_defs = add_axms PureThy.add_defs;

6371

120 
val add_defs_i = PureThy.add_defs_i;


121 


122 


123 
(* constdefs *)


124 


125 
fun gen_add_constdefs consts defs args thy =


126 
thy


127 
> consts (map fst args)


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


129 


130 
val add_constdefs = gen_add_constdefs Theory.add_consts add_defs;


131 
val add_constdefs_i = gen_add_constdefs Theory.add_consts_i add_defs_i;

5915

132 


133 


134 
(* theorems *)


135 


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


137 
f name (map (attrib x) more_srcs)


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


139 

6371

140 
fun global_have_thmss x = gen_have_thmss PureThy.get_thms Attrib.global_attribute x;

5915

141 

6371

142 
fun local_have_thmss x =


143 
gen_have_thmss (ProofContext.get_thms o Proof.context_of)


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


145 


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


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


148 


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

5915

150 


151 

6371

152 
fun apply_theorems th_srcs = global_have_thmss PureThy.have_thmss ((None, []), th_srcs);


153 
fun apply_theorems_i th_srcs = have_thmss_i PureThy.have_thmss ((None, []), th_srcs);


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


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


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


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


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


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


160 

5915

161 

6371

162 
(* forward chaining *)


163 


164 
val from_facts =


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


166 


167 
val from_facts_i =


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


169 


170 
val chain = ProofHistory.apply Proof.chain;

5830

171 


172 


173 
(* context *)


174 


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

6371

176 
val fix_i = ProofHistory.apply o Proof.fix_i;

5830

177 
val match_bind = ProofHistory.apply o Proof.match_bind;

6371

178 
val match_bind_i = ProofHistory.apply o Proof.match_bind_i;

5830

179 


180 


181 
(* statements *)


182 

6371

183 
fun global_statement f name src s thy =


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

5830

185 

6371

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


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


188 


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


190 
fun local_statement_i do_open f name atts t = ProofHistory.apply_cond_open do_open (f name atts t);

5830

191 


192 
val theorem = global_statement Proof.theorem;

6371

193 
val theorem_i = global_statement_i Proof.theorem_i;

5830

194 
val lemma = global_statement Proof.lemma;

6371

195 
val lemma_i = global_statement_i Proof.lemma_i;


196 
val assume = local_statement false Proof.assume;


197 
val assume_i = local_statement_i false Proof.assume_i;


198 
val show = local_statement true Proof.show;


199 
val show_i = local_statement_i true Proof.show_i;


200 
val have = local_statement true Proof.have;


201 
val have_i = local_statement_i true Proof.have_i;

5830

202 


203 


204 
(* end proof *)


205 

6371

206 
fun gen_qed_with prep_att (alt_name, raw_atts) prf =

5830

207 
let


208 
val state = ProofHistory.current prf;


209 
val thy = Proof.theory_of state;

6371

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

6091

211 
val (thy', (kind, name, thm)) = Method.qed alt_name alt_atts state;

5830

212 


213 
val prt_result = Pretty.block

6091

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

5830

215 
in Pretty.writeln prt_result; thy end;


216 

6371

217 
val qed_with = gen_qed_with Attrib.global_attribute;


218 
val qed_with_i = gen_qed_with (K I);


219 

5830

220 
val qed = qed_with (None, None);


221 


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


223 


224 


225 
(* blocks *)


226 


227 
val begin_block = ProofHistory.apply_open Proof.begin_block;


228 
val next_block = ProofHistory.apply Proof.next_block;


229 


230 


231 
(* backward steps *)


232 


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

6371

234 
val tac_i = tac o Method.Basic;

5882

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

6371

236 
val then_tac_i = then_tac o Method.Basic;

5830

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

6371

238 
val proof_i = proof o apsome Method.Basic;

5830

239 
val end_block = ProofHistory.applys_close Method.end_block;


240 
val terminal_proof = ProofHistory.applys_close o Method.terminal_proof;

6371

241 
val terminal_proof_i = terminal_proof o Method.Basic;

6108

242 
val immediate_proof = ProofHistory.applys_close Method.immediate_proof;

5830

243 
val default_proof = ProofHistory.applys_close Method.default_proof;


244 


245 


246 
(* use ML text *)


247 

6331

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


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

5830

250 


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


252 


253 
fun use_let name body txt =


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


255 


256 
val use_setup =

5915

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

5830

258 


259 


260 
(* translation functions *)


261 


262 
val parse_ast_translation =


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


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


265 


266 
val parse_translation =


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


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


269 


270 
val print_translation =


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


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


273 


274 
val print_ast_translation =


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


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


277 


278 
val typed_print_translation =


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


280 
"Theory.add_trfunsT typed_print_translation";


281 


282 
val token_translation =


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


284 
"Theory.add_tokentrfuns token_translation";


285 


286 


287 
(* add_oracle *)


288 


289 
fun add_oracle (name, txt) =


290 
use_let


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


292 
"Theory.add_oracle oracle"


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


294 


295 

6371

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

5830

297 

6331

298 
fun begin_theory name parents files =

6266

299 
let

6331

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


301 
val thy = ThyInfo.begin_theory name parents paths;


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

5830

303 

6331

304 


305 
(* FIXME

5830

306 
fun end_theory thy =


307 
let val thy' = PureThy.end_theory thy in

6331

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

6198

309 
transform_error ThyInfo.put_theory thy'

5830

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


311 
end;

6331

312 
*)

5830

313 

6331

314 
fun end_theory thy =


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


316 


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


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


319 


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

6246

321 


322 


323 
(* context switch *)


324 

6253

325 
fun switch_theory load name =

6246

326 
Toplevel.init_theory

6253

327 
(fn () => (Context.save load name; ThyInfo.get_theory name)) (K ());

6246

328 


329 
val context = switch_theory ThyInfo.use_thy;


330 
val update_context = switch_theory ThyInfo.update_thy;


331 

5830

332 


333 
end;
