5830

1 
(* Title: Pure/Isar/isar_thy.ML


2 
ID: $Id$


3 
Author: Markus Wenzel, TU Muenchen


4 


5 
Derived theory operations.


6 


7 
TODO:

5925

8 
 pure_thy.ML: add_constdefs (atomic!);

5830

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

5882

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

5830

11 
*)


12 


13 
signature ISAR_THY =


14 
sig

5959

15 
val add_text: string > theory > theory


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


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

5915

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


23 
> theory > theory


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


25 
> theory > theory


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


27 
> ProofHistory.T > ProofHistory.T

5830

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

5938

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


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


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


32 
val assume: string > Args.src list > (string * string list) list


33 
> ProofHistory.T > ProofHistory.T


34 
val show: string > Args.src list > string * string list > ProofHistory.T > ProofHistory.T


35 
val have: string > Args.src list > string * string list > ProofHistory.T > ProofHistory.T

5830

36 
val chain: ProofHistory.T > ProofHistory.T

5915

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

5830

38 
val begin_block: ProofHistory.T > ProofHistory.T


39 
val next_block: ProofHistory.T > ProofHistory.T


40 
val end_block: ProofHistory.T > ProofHistory.T


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


42 
val qed: ProofHistory.T > theory


43 
val kill_proof: ProofHistory.T > theory


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

5882

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

5830

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


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

6108

48 
val immediate_proof: ProofHistory.T > ProofHistory.T

5830

49 
val default_proof: ProofHistory.T > ProofHistory.T


50 
val use_mltext: string > theory option > theory option


51 
val use_mltext_theory: string > theory > theory


52 
val use_setup: string > theory > theory


53 
val parse_ast_translation: string > theory > theory


54 
val parse_translation: string > theory > theory


55 
val print_translation: string > theory > theory


56 
val typed_print_translation: string > theory > theory


57 
val print_ast_translation: string > theory > theory


58 
val token_translation: string > theory > theory


59 
val add_oracle: bstring * string > theory > theory

6331

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


61 
val end_theory: theory > theory

6246

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


63 
> Toplevel.transition > Toplevel.transition


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


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

5830

66 
end;


67 


68 
structure IsarThy: ISAR_THY =


69 
struct


70 


71 


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


73 

5959

74 
(* formal comments *) (* FIXME dummy *)


75 


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


77 
val add_chapter = add_text;


78 
val add_section = add_text;


79 
val add_subsection = add_text;


80 
val add_subsubsection = add_text;


81 


82 

5830

83 
(* axioms and defs *)


84 

5915

85 
fun add_axms f args thy =


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


87 


88 
val add_axioms = add_axms PureThy.add_axioms;


89 
val add_defs = add_axms PureThy.add_defs;


90 


91 


92 
(* theorems *)


93 


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


95 
f name (map (attrib x) more_srcs)


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


97 

5830

98 

5915

99 
val have_theorems =

6091

100 
#1 oo gen_have_thmss PureThy.get_thms Attrib.global_attribute PureThy.have_thmss;

5915

101 


102 
val have_lemmas =

6091

103 
#1 oo gen_have_thmss PureThy.get_thms Attrib.global_attribute


104 
(fn name => fn more_atts => PureThy.have_thmss name (more_atts @ [Drule.tag_lemma]));

5915

105 


106 


107 
val have_thmss =

6091

108 
gen_have_thmss (ProofContext.get_thms o Proof.context_of)


109 
(Attrib.local_attribute o Proof.theory_of) Proof.have_thmss;

5915

110 


111 
val have_facts = ProofHistory.apply o have_thmss;


112 
val from_facts = ProofHistory.apply o (Proof.chain oo curry have_thmss ("", []));

5830

113 


114 


115 
(* context *)


116 


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


118 


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


120 


121 


122 
(* statements *)


123 


124 
fun global_statement f name tags s thy =


125 
ProofHistory.init (f name (map (Attrib.global_attribute thy) tags) s thy);


126 


127 
fun local_statement f name tags s = ProofHistory.apply_open (fn state =>


128 
f name (map (Attrib.local_attribute (Proof.theory_of state)) tags) s state);


129 


130 
val theorem = global_statement Proof.theorem;


131 
val lemma = global_statement Proof.lemma;


132 
val assume = local_statement Proof.assume;


133 
val show = local_statement Proof.show;


134 
val have = local_statement Proof.have;


135 


136 


137 
(* forward chaining *)


138 


139 
val chain = ProofHistory.apply Proof.chain;


140 


141 


142 
(* end proof *)


143 


144 
fun qed_with (alt_name, alt_tags) prf =


145 
let


146 
val state = ProofHistory.current prf;


147 
val thy = Proof.theory_of state;


148 
val alt_atts = apsome (map (Attrib.global_attribute thy)) alt_tags;

6091

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

5830

150 


151 
val prt_result = Pretty.block

6091

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

5830

153 
in Pretty.writeln prt_result; thy end;


154 


155 
val qed = qed_with (None, None);


156 


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


158 


159 


160 
(* blocks *)


161 


162 
val begin_block = ProofHistory.apply_open Proof.begin_block;


163 
val next_block = ProofHistory.apply Proof.next_block;


164 


165 


166 
(* backward steps *)


167 


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

5882

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

5830

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


171 
val end_block = ProofHistory.applys_close Method.end_block;


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

6108

173 
val immediate_proof = ProofHistory.applys_close Method.immediate_proof;

5830

174 
val default_proof = ProofHistory.applys_close Method.default_proof;


175 


176 


177 
(* use ML text *)


178 

6331

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


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

5830

181 


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


183 


184 
fun use_let name body txt =


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


186 


187 
val use_setup =

5915

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

5830

189 


190 


191 
(* translation functions *)


192 


193 
val parse_ast_translation =


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


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


196 


197 
val parse_translation =


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


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


200 


201 
val print_translation =


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


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


204 


205 
val print_ast_translation =


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


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


208 


209 
val typed_print_translation =


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


211 
"Theory.add_trfunsT typed_print_translation";


212 


213 
val token_translation =


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


215 
"Theory.add_tokentrfuns token_translation";


216 


217 


218 
(* add_oracle *)


219 


220 
fun add_oracle (name, txt) =


221 
use_let


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


223 
"Theory.add_oracle oracle"


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


225 


226 

6331

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

5830

228 

6331

229 
fun begin_theory name parents files =

6266

230 
let

6331

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


232 
val thy = ThyInfo.begin_theory name parents paths;


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

5830

234 

6331

235 


236 
(* FIXME

5830

237 
fun end_theory thy =


238 
let val thy' = PureThy.end_theory thy in

6331

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

6198

240 
transform_error ThyInfo.put_theory thy'

5830

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


242 
end;

6331

243 
*)

5830

244 

6331

245 
fun end_theory thy =


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


247 


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


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


250 


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

6246

252 


253 


254 
(* context switch *)


255 

6253

256 
fun switch_theory load name =

6246

257 
Toplevel.init_theory

6253

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

6246

259 


260 
val context = switch_theory ThyInfo.use_thy;


261 
val update_context = switch_theory ThyInfo.update_thy;


262 

5830

263 


264 
end;
