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:


8 
 add_defs: handle empty name (pure_thy.ML (!?));


9 
 add_constdefs (atomic!);


10 
 have_theorems, have_lemmas;


11 
 load theory;


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


13 
 now_block: ProofHistory open / close (!?);


14 
 from_facts: attribs, args (!?) (beware of termination!!);


15 
*)


16 


17 
signature ISAR_THY =


18 
sig


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


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


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


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


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


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


25 
val assume: string > Args.src list > string list > ProofHistory.T > ProofHistory.T


26 
val show: string > Args.src list > string > ProofHistory.T > ProofHistory.T


27 
val have: string > Args.src list > string > ProofHistory.T > ProofHistory.T


28 
val chain: ProofHistory.T > ProofHistory.T


29 
val from_facts: string list > ProofHistory.T > ProofHistory.T


30 
val begin_block: ProofHistory.T > ProofHistory.T


31 
val next_block: ProofHistory.T > ProofHistory.T


32 
val end_block: ProofHistory.T > ProofHistory.T


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


34 
val qed: ProofHistory.T > theory


35 
val kill_proof: ProofHistory.T > theory


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


37 
val etac: Method.text > ProofHistory.T > ProofHistory.T


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


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


40 
val trivial_proof: ProofHistory.T > ProofHistory.T


41 
val default_proof: ProofHistory.T > ProofHistory.T


42 
val use_mltext: string > theory option > theory option


43 
val use_mltext_theory: string > theory > theory


44 
val use_setup: string > theory > theory


45 
val parse_ast_translation: string > theory > theory


46 
val parse_translation: string > theory > theory


47 
val print_translation: string > theory > theory


48 
val typed_print_translation: string > theory > theory


49 
val print_ast_translation: string > theory > theory


50 
val token_translation: string > theory > theory


51 
val add_oracle: bstring * string > theory > theory


52 
val the_theory: string > unit > theory


53 
val begin_theory: string * string list > unit > theory


54 
val end_theory: theory > unit


55 
end;


56 


57 
structure IsarThy: ISAR_THY =


58 
struct


59 


60 


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


62 


63 
(* axioms and defs *)


64 


65 
fun attributize thy (x, srcs) = (x, map (Attrib.global_attribute thy) srcs);


66 


67 
fun add_axioms axms thy = PureThy.add_axioms (map (attributize thy) axms) thy;


68 
fun add_defs defs thy = PureThy.add_defs (map (attributize thy) defs) thy;


69 


70 


71 
(* context *)


72 


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


74 


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


76 


77 


78 
(* statements *)


79 


80 
fun global_statement f name tags s thy =


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


82 


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


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


85 


86 
val theorem = global_statement Proof.theorem;


87 
val lemma = global_statement Proof.lemma;


88 
val assume = local_statement Proof.assume;


89 
val show = local_statement Proof.show;


90 
val have = local_statement Proof.have;


91 


92 


93 
(* forward chaining *)


94 


95 
val chain = ProofHistory.apply Proof.chain;


96 


97 
fun from_facts names = ProofHistory.apply (fn state =>


98 
state


99 
> Proof.from_facts (ProofContext.get_tthmss (Proof.context_of state) names));


100 


101 


102 
(* end proof *)


103 


104 
fun qed_with (alt_name, alt_tags) prf =


105 
let


106 
val state = ProofHistory.current prf;


107 
val thy = Proof.theory_of state;


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


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


110 


111 
val prt_result = Pretty.block


112 
[Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Attribute.pretty_tthm tthm];


113 
in Pretty.writeln prt_result; thy end;


114 


115 
val qed = qed_with (None, None);


116 


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


118 


119 


120 
(* blocks *)


121 


122 
val begin_block = ProofHistory.apply_open Proof.begin_block;


123 
val next_block = ProofHistory.apply Proof.next_block;


124 


125 


126 
(* backward steps *)


127 


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


129 
val etac = ProofHistory.applys o Method.etac;


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


131 
val end_block = ProofHistory.applys_close Method.end_block;


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


133 
val trivial_proof = ProofHistory.applys_close Method.trivial_proof;


134 
val default_proof = ProofHistory.applys_close Method.default_proof;


135 


136 


137 
(* use ML text *)


138 


139 
fun use_mltext txt opt_thy =


140 
let


141 
val save_context = Context.get_context ();


142 
val _ = Context.set_context opt_thy;


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


144 
val opt_thy' = Context.get_context ();


145 
in


146 
Context.set_context save_context;


147 
(case opt_exn of


148 
None => opt_thy'


149 
 Some exn => raise exn)


150 
end;


151 


152 
fun use_mltext_theory txt thy =


153 
(case use_mltext txt (Some thy) of


154 
Some thy' => thy'


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


156 


157 


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


159 


160 
fun use_let name body txt =


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


162 


163 
val use_setup =


164 
use_let "setup: (theory > theory) list" "Theory.apply setup";


165 


166 


167 
(* translation functions *)


168 


169 
val parse_ast_translation =


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


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


172 


173 
val parse_translation =


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


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


176 


177 
val print_translation =


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


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


180 


181 
val print_ast_translation =


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


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


184 


185 
val typed_print_translation =


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


187 
"Theory.add_trfunsT typed_print_translation";


188 


189 
val token_translation =


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


191 
"Theory.add_tokentrfuns token_translation";


192 


193 


194 
(* add_oracle *)


195 


196 
fun add_oracle (name, txt) =


197 
use_let


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


199 
"Theory.add_oracle oracle"


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


201 


202 


203 
(* theory init and exit *)


204 


205 
fun the_theory name () = ThyInfo.theory name;


206 


207 
fun begin_theory (name, names) () =


208 
PureThy.begin_theory name (map ThyInfo.theory names);


209 


210 


211 
fun end_theory thy =


212 
let val thy' = PureThy.end_theory thy in


213 
transform_error ThyInfo.store_theory thy'


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


215 
end;


216 


217 


218 
end;
