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;
|