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_constdefs (atomic!);


9 
 load theory;


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

5882

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

5830

12 
*)


13 


14 
signature ISAR_THY =


15 
sig


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


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

5915

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


19 
> theory > theory


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


21 
> theory > theory


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


23 
> ProofHistory.T > ProofHistory.T

5830

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


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


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


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


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


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


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


31 
val chain: ProofHistory.T > ProofHistory.T

5915

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

5830

33 
val begin_block: ProofHistory.T > ProofHistory.T


34 
val next_block: ProofHistory.T > ProofHistory.T


35 
val end_block: ProofHistory.T > ProofHistory.T


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


37 
val qed: ProofHistory.T > theory


38 
val kill_proof: ProofHistory.T > theory


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

5882

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

5830

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


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


43 
val trivial_proof: ProofHistory.T > ProofHistory.T


44 
val default_proof: ProofHistory.T > ProofHistory.T


45 
val use_mltext: string > theory option > theory option


46 
val use_mltext_theory: string > theory > theory


47 
val use_setup: string > theory > theory


48 
val parse_ast_translation: string > theory > theory


49 
val parse_translation: string > theory > theory


50 
val print_translation: string > theory > theory


51 
val typed_print_translation: string > theory > theory


52 
val print_ast_translation: string > theory > theory


53 
val token_translation: string > theory > theory


54 
val add_oracle: bstring * string > theory > theory


55 
val the_theory: string > unit > theory


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


57 
val end_theory: theory > unit


58 
end;


59 


60 
structure IsarThy: ISAR_THY =


61 
struct


62 


63 


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


65 


66 
(* axioms and defs *)


67 

5915

68 
fun add_axms f args thy =


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


70 


71 
val add_axioms = add_axms PureThy.add_axioms;


72 
val add_defs = add_axms PureThy.add_defs;


73 


74 


75 
(* theorems *)


76 


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


78 
f name (map (attrib x) more_srcs)


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


80 

5830

81 

5915

82 
val have_theorems =


83 
#1 oo gen_have_thmss PureThy.get_tthms Attrib.global_attribute PureThy.have_tthmss;


84 


85 
val have_lemmas =


86 
#1 oo gen_have_thmss PureThy.get_tthms Attrib.global_attribute


87 
(fn name => fn more_atts => PureThy.have_tthmss name (more_atts @ [Attribute.tag_lemma]));


88 


89 


90 
val have_thmss =


91 
gen_have_thmss (ProofContext.get_tthms o Proof.context_of)


92 
(Attrib.local_attribute o Proof.theory_of) Proof.have_tthmss;


93 


94 
val have_facts = ProofHistory.apply o have_thmss;


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

5830

96 


97 


98 
(* context *)


99 


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


101 


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


103 


104 


105 
(* statements *)


106 


107 
fun global_statement f name tags s thy =


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


109 


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


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


112 


113 
val theorem = global_statement Proof.theorem;


114 
val lemma = global_statement Proof.lemma;


115 
val assume = local_statement Proof.assume;


116 
val show = local_statement Proof.show;


117 
val have = local_statement Proof.have;


118 


119 


120 
(* forward chaining *)


121 


122 
val chain = ProofHistory.apply Proof.chain;


123 


124 


125 
(* end proof *)


126 


127 
fun qed_with (alt_name, alt_tags) prf =


128 
let


129 
val state = ProofHistory.current prf;


130 
val thy = Proof.theory_of state;


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


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


133 


134 
val prt_result = Pretty.block


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


136 
in Pretty.writeln prt_result; thy end;


137 


138 
val qed = qed_with (None, None);


139 


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


141 


142 


143 
(* blocks *)


144 


145 
val begin_block = ProofHistory.apply_open Proof.begin_block;


146 
val next_block = ProofHistory.apply Proof.next_block;


147 


148 


149 
(* backward steps *)


150 


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

5882

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

5830

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


154 
val end_block = ProofHistory.applys_close Method.end_block;


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


156 
val trivial_proof = ProofHistory.applys_close Method.trivial_proof;


157 
val default_proof = ProofHistory.applys_close Method.default_proof;


158 


159 


160 
(* use ML text *)


161 


162 
fun use_mltext txt opt_thy =


163 
let


164 
val save_context = Context.get_context ();


165 
val _ = Context.set_context opt_thy;


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


167 
val opt_thy' = Context.get_context ();


168 
in


169 
Context.set_context save_context;


170 
(case opt_exn of


171 
None => opt_thy'


172 
 Some exn => raise exn)


173 
end;


174 


175 
fun use_mltext_theory txt thy =


176 
(case use_mltext txt (Some thy) of


177 
Some thy' => thy'


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


179 


180 


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


182 


183 
fun use_let name body txt =


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


185 


186 
val use_setup =

5915

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

5830

188 


189 


190 
(* translation functions *)


191 


192 
val parse_ast_translation =


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


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


195 


196 
val parse_translation =


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


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


199 


200 
val print_translation =


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


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


203 


204 
val print_ast_translation =


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


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


207 


208 
val typed_print_translation =


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


210 
"Theory.add_trfunsT typed_print_translation";


211 


212 
val token_translation =


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


214 
"Theory.add_tokentrfuns token_translation";


215 


216 


217 
(* add_oracle *)


218 


219 
fun add_oracle (name, txt) =


220 
use_let


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


222 
"Theory.add_oracle oracle"


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


224 


225 


226 
(* theory init and exit *)


227 


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


229 


230 
fun begin_theory (name, names) () =


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


232 


233 


234 
fun end_theory thy =


235 
let val thy' = PureThy.end_theory thy in


236 
transform_error ThyInfo.store_theory thy'


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


238 
end;


239 


240 


241 
end;
