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


48 
val trivial_proof: ProofHistory.T > ProofHistory.T


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


60 
val the_theory: string > unit > theory


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


62 
val end_theory: theory > unit


63 
end;


64 


65 
structure IsarThy: ISAR_THY =


66 
struct


67 


68 


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


70 

5959

71 
(* formal comments *) (* FIXME dummy *)


72 


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


74 
val add_chapter = add_text;


75 
val add_section = add_text;


76 
val add_subsection = add_text;


77 
val add_subsubsection = add_text;


78 


79 

5830

80 
(* axioms and defs *)


81 

5915

82 
fun add_axms f args thy =


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


84 


85 
val add_axioms = add_axms PureThy.add_axioms;


86 
val add_defs = add_axms PureThy.add_defs;


87 


88 


89 
(* theorems *)


90 


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


92 
f name (map (attrib x) more_srcs)


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


94 

5830

95 

5915

96 
val have_theorems =


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


98 


99 
val have_lemmas =


100 
#1 oo gen_have_thmss PureThy.get_tthms Attrib.global_attribute


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


102 


103 


104 
val have_thmss =


105 
gen_have_thmss (ProofContext.get_tthms o Proof.context_of)


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


107 


108 
val have_facts = ProofHistory.apply o have_thmss;


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

5830

110 


111 


112 
(* context *)


113 


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


115 


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


117 


118 


119 
(* statements *)


120 


121 
fun global_statement f name tags s thy =


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


123 


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


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


126 


127 
val theorem = global_statement Proof.theorem;


128 
val lemma = global_statement Proof.lemma;


129 
val assume = local_statement Proof.assume;


130 
val show = local_statement Proof.show;


131 
val have = local_statement Proof.have;


132 


133 


134 
(* forward chaining *)


135 


136 
val chain = ProofHistory.apply Proof.chain;


137 


138 


139 
(* end proof *)


140 


141 
fun qed_with (alt_name, alt_tags) prf =


142 
let


143 
val state = ProofHistory.current prf;


144 
val thy = Proof.theory_of state;


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


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


147 


148 
val prt_result = Pretty.block


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


150 
in Pretty.writeln prt_result; thy end;


151 


152 
val qed = qed_with (None, None);


153 


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


155 


156 


157 
(* blocks *)


158 


159 
val begin_block = ProofHistory.apply_open Proof.begin_block;


160 
val next_block = ProofHistory.apply Proof.next_block;


161 


162 


163 
(* backward steps *)


164 


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

5882

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

5830

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


168 
val end_block = ProofHistory.applys_close Method.end_block;


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


170 
val trivial_proof = ProofHistory.applys_close Method.trivial_proof;


171 
val default_proof = ProofHistory.applys_close Method.default_proof;


172 


173 


174 
(* use ML text *)


175 


176 
fun use_mltext txt opt_thy =


177 
let


178 
val save_context = Context.get_context ();


179 
val _ = Context.set_context opt_thy;


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


181 
val opt_thy' = Context.get_context ();


182 
in


183 
Context.set_context save_context;


184 
(case opt_exn of


185 
None => opt_thy'


186 
 Some exn => raise exn)


187 
end;


188 


189 
fun use_mltext_theory txt thy =


190 
(case use_mltext txt (Some thy) of


191 
Some thy' => thy'


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


193 


194 


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


196 


197 
fun use_let name body txt =


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


199 


200 
val use_setup =

5915

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

5830

202 


203 


204 
(* translation functions *)


205 


206 
val parse_ast_translation =


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


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


209 


210 
val parse_translation =


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


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


213 


214 
val print_translation =


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


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


217 


218 
val print_ast_translation =


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


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


221 


222 
val typed_print_translation =


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


224 
"Theory.add_trfunsT typed_print_translation";


225 


226 
val token_translation =


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


228 
"Theory.add_tokentrfuns token_translation";


229 


230 


231 
(* add_oracle *)


232 


233 
fun add_oracle (name, txt) =


234 
use_let


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


236 
"Theory.add_oracle oracle"


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


238 


239 


240 
(* theory init and exit *)


241 


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


243 


244 
fun begin_theory (name, names) () =


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


246 


247 


248 
fun end_theory thy =


249 
let val thy' = PureThy.end_theory thy in


250 
transform_error ThyInfo.store_theory thy'


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


252 
end;


253 


254 


255 
end;
