1710 |
1710 |
1711 fun prune proof = |
1711 fun prune proof = |
1712 if Options.default_bool "prune_proofs" then MinProof |
1712 if Options.default_bool "prune_proofs" then MinProof |
1713 else shrink_proof proof; |
1713 else shrink_proof proof; |
1714 |
1714 |
1715 fun prepare_thm_proof thy name shyps hyps concl promises body = |
1715 fun prepare_thm_proof unconstrain thy name shyps hyps concl promises body = |
1716 let |
1716 let |
1717 val named = name <> ""; |
1717 val named = name <> ""; |
1718 |
1718 |
1719 val prop = Logic.list_implies (hyps, concl); |
1719 val prop = Logic.list_implies (hyps, concl); |
1720 val args = prop_args prop; |
1720 val args = prop_args prop; |
1742 |
1742 |
1743 val (i, body') = |
1743 val (i, body') = |
1744 (*non-deterministic, depends on unknown promises*) |
1744 (*non-deterministic, depends on unknown promises*) |
1745 (case strip_combt (fst (strip_combP prf)) of |
1745 (case strip_combt (fst (strip_combP prf)) of |
1746 (PThm (i, ((a, prop', NONE, _), body')), args') => |
1746 (PThm (i, ((a, prop', NONE, _), body')), args') => |
1747 if (a = "" orelse a = name) andalso prop1 = prop' andalso args = args' |
1747 if (a = "" orelse a = name) andalso prop' = prop1 andalso args' = args |
1748 then (i, body' |> (a = "" andalso named) ? Future.map (publish i)) |
1748 then (i, body' |> (a = "" andalso named) ? Future.map (publish i)) |
1749 else new_prf () |
1749 else new_prf () |
1750 | _ => new_prf ()); |
1750 | _ => new_prf ()); |
1751 |
1751 |
|
1752 val pthm = (i, make_thm_node name prop1 body'); |
|
1753 |
1752 val head = PThm (i, ((name, prop1, NONE, open_proof), body')); |
1754 val head = PThm (i, ((name, prop1, NONE, open_proof), body')); |
1753 in ((i, make_thm_node name prop1 body'), head, args, argsP, args1) end; |
1755 val proof = |
|
1756 if unconstrain |
|
1757 then proof_combt' (head, args1) |
|
1758 else proof_combP (proof_combt' (head, args), argsP); |
|
1759 in (pthm, proof) end; |
1754 |
1760 |
1755 in |
1761 in |
1756 |
1762 |
1757 fun thm_proof thy name shyps hyps concl promises body = |
1763 val thm_proof = prepare_thm_proof false; |
1758 let val (pthm, head, args, argsP, _) = prepare_thm_proof thy name shyps hyps concl promises body |
|
1759 in (pthm, proof_combP (proof_combt' (head, args), argsP)) end; |
|
1760 |
1764 |
1761 fun unconstrain_thm_proof thy shyps concl promises body = |
1765 fun unconstrain_thm_proof thy shyps concl promises body = |
1762 let val (pthm, head, _, _, args) = prepare_thm_proof thy "" shyps [] concl promises body |
1766 prepare_thm_proof true thy "" shyps [] concl promises body; |
1763 in (pthm, proof_combt' (head, args)) end; |
|
1764 |
1767 |
1765 end; |
1768 end; |
1766 |
1769 |
1767 |
1770 |
1768 (* approximative PThm name *) |
1771 (* approximative PThm name *) |