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

6246

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


61 
> Toplevel.transition > Toplevel.transition


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


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

5830

64 
end;


65 


66 
structure IsarThy: ISAR_THY =


67 
struct


68 


69 


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


71 

5959

72 
(* formal comments *) (* FIXME dummy *)


73 


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


75 
val add_chapter = add_text;


76 
val add_section = add_text;


77 
val add_subsection = add_text;


78 
val add_subsubsection = add_text;


79 


80 

5830

81 
(* axioms and defs *)


82 

5915

83 
fun add_axms f args thy =


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


85 


86 
val add_axioms = add_axms PureThy.add_axioms;


87 
val add_defs = add_axms PureThy.add_defs;


88 


89 


90 
(* theorems *)


91 


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


93 
f name (map (attrib x) more_srcs)


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


95 

5830

96 

5915

97 
val have_theorems =

6091

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

5915

99 


100 
val have_lemmas =

6091

101 
#1 oo gen_have_thmss PureThy.get_thms Attrib.global_attribute


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

5915

103 


104 


105 
val have_thmss =

6091

106 
gen_have_thmss (ProofContext.get_thms o Proof.context_of)


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

5915

108 


109 
val have_facts = ProofHistory.apply o have_thmss;


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

5830

111 


112 


113 
(* context *)


114 


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


116 


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


118 


119 


120 
(* statements *)


121 


122 
fun global_statement f name tags s thy =


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


124 


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


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


127 


128 
val theorem = global_statement Proof.theorem;


129 
val lemma = global_statement Proof.lemma;


130 
val assume = local_statement Proof.assume;


131 
val show = local_statement Proof.show;


132 
val have = local_statement Proof.have;


133 


134 


135 
(* forward chaining *)


136 


137 
val chain = ProofHistory.apply Proof.chain;


138 


139 


140 
(* end proof *)


141 


142 
fun qed_with (alt_name, alt_tags) prf =


143 
let


144 
val state = ProofHistory.current prf;


145 
val thy = Proof.theory_of state;


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

6091

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

5830

148 


149 
val prt_result = Pretty.block

6091

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

5830

151 
in Pretty.writeln prt_result; thy end;


152 


153 
val qed = qed_with (None, None);


154 


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


156 


157 


158 
(* blocks *)


159 


160 
val begin_block = ProofHistory.apply_open Proof.begin_block;


161 
val next_block = ProofHistory.apply Proof.next_block;


162 


163 


164 
(* backward steps *)


165 


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

5882

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

5830

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


169 
val end_block = ProofHistory.applys_close Method.end_block;


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

6108

171 
val immediate_proof = ProofHistory.applys_close Method.immediate_proof;

5830

172 
val default_proof = ProofHistory.applys_close Method.default_proof;


173 


174 


175 
(* use ML text *)


176 


177 
fun use_mltext txt opt_thy =


178 
let


179 
val save_context = Context.get_context ();


180 
val _ = Context.set_context opt_thy;


181 
val opt_exn = (transform_error (use_text false) txt; None) handle exn => Some exn;


182 
val opt_thy' = Context.get_context ();


183 
in


184 
Context.set_context save_context;


185 
(case opt_exn of


186 
None => opt_thy'


187 
 Some exn => raise exn)


188 
end;


189 


190 
fun use_mltext_theory txt thy =


191 
(case use_mltext txt (Some thy) of


192 
Some thy' => thy'


193 
 None => error "Missing result ML theory context");


194 


195 


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


197 


198 
fun use_let name body txt =


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


200 


201 
val use_setup =

5915

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

5830

203 


204 


205 
(* translation functions *)


206 


207 
val parse_ast_translation =


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


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


210 


211 
val parse_translation =


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


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


214 


215 
val print_translation =


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


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


218 


219 
val print_ast_translation =


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


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


222 


223 
val typed_print_translation =


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


225 
"Theory.add_trfunsT typed_print_translation";


226 


227 
val token_translation =


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


229 
"Theory.add_tokentrfuns token_translation";


230 


231 


232 
(* add_oracle *)


233 


234 
fun add_oracle (name, txt) =


235 
use_let


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


237 
"Theory.add_oracle oracle"


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


239 


240 


241 
(* theory init and exit *)


242 

6246

243 
fun begin_theory (name, parents, files) () =


244 
let val thy = ThyInfo.begin_theory name parents


245 
in seq ThyInfo.use (mapfilter (fn (x, true) => Some x  _ => None) files); thy end;

5830

246 


247 
fun end_theory thy =


248 
let val thy' = PureThy.end_theory thy in

6198

249 
transform_error ThyInfo.put_theory thy'

5830

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


251 
end;


252 

6246

253 
fun theory spec = Toplevel.init_theory (begin_theory spec) end_theory;


254 


255 


256 
(* context switch *)


257 


258 
fun switch_theory require name =


259 
Toplevel.init_theory


260 
(fn () => (Context.save require name; ThyInfo.get_theory name)) (K ());


261 


262 
val context = switch_theory ThyInfo.use_thy;


263 
val update_context = switch_theory ThyInfo.update_thy;


264 

5830

265 


266 
end;
