8 |
8 |
9 signature RECONSTRUCT = |
9 signature RECONSTRUCT = |
10 sig |
10 sig |
11 val quiet_mode : bool ref |
11 val quiet_mode : bool ref |
12 val reconstruct_proof : Sign.sg -> term -> Proofterm.proof -> Proofterm.proof |
12 val reconstruct_proof : Sign.sg -> term -> Proofterm.proof -> Proofterm.proof |
|
13 val prop_of' : term list -> Proofterm.proof -> term |
13 val prop_of : Proofterm.proof -> term |
14 val prop_of : Proofterm.proof -> term |
14 val expand_proof : Sign.sg -> string list -> Proofterm.proof -> Proofterm.proof |
15 val expand_proof : Sign.sg -> string list -> Proofterm.proof -> Proofterm.proof |
15 end; |
16 end; |
16 |
17 |
17 structure Reconstruct : RECONSTRUCT = |
18 structure Reconstruct : RECONSTRUCT = |
300 val env' = solve sg cs' env |
301 val env' = solve sg cs' env |
301 in |
302 in |
302 thawf (norm_proof env' prf) |
303 thawf (norm_proof env' prf) |
303 end; |
304 end; |
304 |
305 |
305 fun prop_of prf = |
306 fun prop_of_atom prop Ts = |
306 let |
307 subst_TVars (map fst (term_tvars prop) ~~ Ts) (forall_intr_vfs prop); |
307 fun prop_of_atom prop Ts = |
308 |
308 subst_TVars (map fst (term_tvars prop) ~~ Ts) (forall_intr_vfs prop); |
309 fun prop_of' Hs (PBound i) = nth_elem (i, Hs) |
309 |
310 | prop_of' Hs (Abst (s, Some T, prf)) = |
310 fun prop_of' Hs (PBound i) = nth_elem (i, Hs) |
311 all T $ (Abs (s, T, prop_of' Hs prf)) |
311 | prop_of' Hs (Abst (s, Some T, prf)) = |
312 | prop_of' Hs (AbsP (s, Some t, prf)) = |
312 all T $ (Abs (s, T, prop_of' Hs prf)) |
313 Logic.mk_implies (t, prop_of' (t :: Hs) prf) |
313 | prop_of' Hs (AbsP (s, Some t, prf)) = |
314 | prop_of' Hs (prf % Some t) = (case prop_of' Hs prf of |
314 Logic.mk_implies (t, prop_of' (t :: Hs) prf) |
315 Const ("all", _) $ f => betapply (f, t) |
315 | prop_of' Hs (prf % Some t) = (case prop_of' Hs prf of |
316 | _ => error "prop_of: all expected") |
316 Const ("all", _) $ f => betapply (f, t) |
317 | prop_of' Hs (prf1 %% prf2) = (case prop_of' Hs prf1 of |
317 | _ => error "prop_of: all expected") |
318 Const ("==>", _) $ P $ Q => Q |
318 | prop_of' Hs (prf1 %% prf2) = (case prop_of' Hs prf1 of |
319 | _ => error "prop_of: ==> expected") |
319 Const ("==>", _) $ P $ Q => Q |
320 | prop_of' Hs (Hyp t) = t |
320 | _ => error "prop_of: ==> expected") |
321 | prop_of' Hs (PThm (_, _, prop, Some Ts)) = prop_of_atom prop Ts |
321 | prop_of' Hs (Hyp t) = t |
322 | prop_of' Hs (PAxm (_, prop, Some Ts)) = prop_of_atom prop Ts |
322 | prop_of' Hs (PThm (_, _, prop, Some Ts)) = prop_of_atom prop Ts |
323 | prop_of' Hs (Oracle (_, prop, Some Ts)) = prop_of_atom prop Ts |
323 | prop_of' Hs (PAxm (_, prop, Some Ts)) = prop_of_atom prop Ts |
324 | prop_of' _ _ = error "prop_of: partial proof object"; |
324 | prop_of' Hs (Oracle (_, prop, Some Ts)) = prop_of_atom prop Ts |
325 |
325 | prop_of' _ _ = error "prop_of: partial proof object"; |
326 val prop_of = prop_of' []; |
326 |
|
327 in prop_of' [] prf end; |
|
328 |
327 |
329 |
328 |
330 (******************************************************************************** |
329 (******************************************************************************** |
331 expand and reconstruct subproofs |
330 expand and reconstruct subproofs |
332 *********************************************************************************) |
331 *********************************************************************************) |