248 |> (if failed then enclose "One-line proof reconstruction failed: " "." |
248 |> (if failed then enclose "One-line proof reconstruction failed: " "." |
249 else try_command_line banner ext_time) |
249 else try_command_line banner ext_time) |
250 in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end |
250 in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end |
251 |
251 |
252 (** Hard-core proof reconstruction: structured Isar proofs **) |
252 (** Hard-core proof reconstruction: structured Isar proofs **) |
253 |
|
254 (* Simple simplifications to ensure that sort annotations don't leave a trail of |
|
255 spurious "True"s. *) |
|
256 fun s_not (Const (@{const_name All}, T) $ Abs (s, T', t')) = |
|
257 Const (@{const_name Ex}, T) $ Abs (s, T', s_not t') |
|
258 | s_not (Const (@{const_name Ex}, T) $ Abs (s, T', t')) = |
|
259 Const (@{const_name All}, T) $ Abs (s, T', s_not t') |
|
260 | s_not (@{const HOL.implies} $ t1 $ t2) = @{const HOL.conj} $ t1 $ s_not t2 |
|
261 | s_not (@{const HOL.conj} $ t1 $ t2) = |
|
262 @{const HOL.disj} $ s_not t1 $ s_not t2 |
|
263 | s_not (@{const HOL.disj} $ t1 $ t2) = |
|
264 @{const HOL.conj} $ s_not t1 $ s_not t2 |
|
265 | s_not (@{const False}) = @{const True} |
|
266 | s_not (@{const True}) = @{const False} |
|
267 | s_not (@{const Not} $ t) = t |
|
268 | s_not t = @{const Not} $ t |
|
269 fun s_conj (@{const True}, t2) = t2 |
|
270 | s_conj (t1, @{const True}) = t1 |
|
271 | s_conj p = HOLogic.mk_conj p |
|
272 fun s_disj (@{const False}, t2) = t2 |
|
273 | s_disj (t1, @{const False}) = t1 |
|
274 | s_disj p = HOLogic.mk_disj p |
|
275 fun s_imp (@{const True}, t2) = t2 |
|
276 | s_imp (t1, @{const False}) = s_not t1 |
|
277 | s_imp p = HOLogic.mk_imp p |
|
278 fun s_iff (@{const True}, t2) = t2 |
|
279 | s_iff (t1, @{const True}) = t1 |
|
280 | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2 |
|
281 |
253 |
282 fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t |
254 fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t |
283 fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t |
255 fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t |
284 |
256 |
285 fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS) |
257 fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS) |