151 val put_name: string -> thm -> thm |
151 val put_name: string -> thm -> thm |
152 val extern_oracles: theory -> xstring list |
152 val extern_oracles: theory -> xstring list |
153 val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory |
153 val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory |
154 end; |
154 end; |
155 |
155 |
156 structure Thm:> THM = |
156 structure Thm: THM = |
157 struct |
157 struct |
158 |
158 |
159 structure Pt = Proofterm; |
159 structure Pt = Proofterm; |
160 |
160 |
161 |
161 |
162 (*** Certified terms and types ***) |
162 (*** Certified terms and types ***) |
163 |
163 |
164 (** certified types **) |
164 (** certified types **) |
165 |
165 |
166 datatype ctyp = Ctyp of |
166 abstype ctyp = Ctyp of |
167 {thy_ref: theory_ref, |
167 {thy_ref: theory_ref, |
168 T: typ, |
168 T: typ, |
169 maxidx: int, |
169 maxidx: int, |
170 sorts: sort OrdList.T}; |
170 sorts: sort OrdList.T} |
|
171 with |
171 |
172 |
172 fun rep_ctyp (Ctyp args) = args; |
173 fun rep_ctyp (Ctyp args) = args; |
173 fun theory_of_ctyp (Ctyp {thy_ref, ...}) = Theory.deref thy_ref; |
174 fun theory_of_ctyp (Ctyp {thy_ref, ...}) = Theory.deref thy_ref; |
174 fun typ_of (Ctyp {T, ...}) = T; |
175 fun typ_of (Ctyp {T, ...}) = T; |
175 |
176 |
187 |
188 |
188 |
189 |
189 (** certified terms **) |
190 (** certified terms **) |
190 |
191 |
191 (*certified terms with checked typ, maxidx, and sorts*) |
192 (*certified terms with checked typ, maxidx, and sorts*) |
192 datatype cterm = Cterm of |
193 abstype cterm = Cterm of |
193 {thy_ref: theory_ref, |
194 {thy_ref: theory_ref, |
194 t: term, |
195 t: term, |
195 T: typ, |
196 T: typ, |
196 maxidx: int, |
197 maxidx: int, |
197 sorts: sort OrdList.T}; |
198 sorts: sort OrdList.T} |
|
199 with |
198 |
200 |
199 exception CTERM of string * cterm list; |
201 exception CTERM of string * cterm list; |
200 |
202 |
201 fun rep_cterm (Cterm args) = args; |
203 fun rep_cterm (Cterm args) = args; |
202 |
204 |
335 |
337 |
336 |
338 |
337 |
339 |
338 (*** Derivations and Theorems ***) |
340 (*** Derivations and Theorems ***) |
339 |
341 |
340 datatype thm = Thm of |
342 abstype thm = Thm of |
341 deriv * (*derivation*) |
343 deriv * (*derivation*) |
342 {thy_ref: theory_ref, (*dynamic reference to theory*) |
344 {thy_ref: theory_ref, (*dynamic reference to theory*) |
343 tags: Properties.T, (*additional annotations/comments*) |
345 tags: Properties.T, (*additional annotations/comments*) |
344 maxidx: int, (*maximum index of any Var or TVar*) |
346 maxidx: int, (*maximum index of any Var or TVar*) |
345 shyps: sort OrdList.T, (*sort hypotheses*) |
347 shyps: sort OrdList.T, (*sort hypotheses*) |
346 hyps: term OrdList.T, (*hypotheses*) |
348 hyps: term OrdList.T, (*hypotheses*) |
347 tpairs: (term * term) list, (*flex-flex pairs*) |
349 tpairs: (term * term) list, (*flex-flex pairs*) |
348 prop: term} (*conclusion*) |
350 prop: term} (*conclusion*) |
349 and deriv = Deriv of |
351 and deriv = Deriv of |
350 {promises: (serial * thm future) OrdList.T, |
352 {promises: (serial * thm future) OrdList.T, |
351 body: Pt.proof_body}; |
353 body: Pt.proof_body} |
|
354 with |
352 |
355 |
353 type conv = cterm -> thm; |
356 type conv = cterm -> thm; |
354 |
357 |
355 (*attributes subsume any kind of rules or context modifiers*) |
358 (*attributes subsume any kind of rules or context modifiers*) |
356 type attribute = Context.generic * thm -> Context.generic * thm; |
359 type attribute = Context.generic * thm -> Context.generic * thm; |