104 val consolidate: thm list -> unit |
104 val consolidate: thm list -> unit |
105 val peek_status: thm -> {oracle: bool, unfinished: bool, failed: bool} |
105 val peek_status: thm -> {oracle: bool, unfinished: bool, failed: bool} |
106 val future: thm future -> cterm -> thm |
106 val future: thm future -> cterm -> thm |
107 val derivation_closed: thm -> bool |
107 val derivation_closed: thm -> bool |
108 val derivation_name: thm -> string |
108 val derivation_name: thm -> string |
109 val name_derivation: string -> thm -> thm |
109 val name_derivation: string * Position.T -> thm -> thm |
110 val close_derivation: thm -> thm |
110 val close_derivation: Position.T -> thm -> thm |
111 val trim_context: thm -> thm |
111 val trim_context: thm -> thm |
112 val axiom: theory -> string -> thm |
112 val axiom: theory -> string -> thm |
113 val axioms_of: theory -> (string * thm) list |
113 val axioms_of: theory -> (string * thm) list |
114 val get_tags: thm -> Properties.T |
114 val get_tags: thm -> Properties.T |
115 val map_tags: (Properties.T -> Properties.T) -> thm -> thm |
115 val map_tags: (Properties.T -> Properties.T) -> thm -> thm |
998 |
998 |
999 (*non-deterministic, depends on unknown promises*) |
999 (*non-deterministic, depends on unknown promises*) |
1000 fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) = |
1000 fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) = |
1001 Proofterm.get_name shyps hyps prop (Proofterm.proof_of body); |
1001 Proofterm.get_name shyps hyps prop (Proofterm.proof_of body); |
1002 |
1002 |
1003 fun name_derivation name = |
1003 fun name_derivation name_pos = |
1004 solve_constraints #> (fn thm as Thm (der, args) => |
1004 solve_constraints #> (fn thm as Thm (der, args) => |
1005 let |
1005 let |
1006 val thy = theory_of_thm thm; |
1006 val thy = theory_of_thm thm; |
1007 |
1007 |
1008 val Deriv {promises, body} = der; |
1008 val Deriv {promises, body} = der; |
1011 fun err msg = raise THM ("name_derivation: " ^ msg, 0, [thm]); |
1011 fun err msg = raise THM ("name_derivation: " ^ msg, 0, [thm]); |
1012 val _ = null tpairs orelse err "bad flex-flex constraints"; |
1012 val _ = null tpairs orelse err "bad flex-flex constraints"; |
1013 |
1013 |
1014 val ps = map (apsnd (Future.map fulfill_body)) promises; |
1014 val ps = map (apsnd (Future.map fulfill_body)) promises; |
1015 val (pthm, proof) = |
1015 val (pthm, proof) = |
1016 Proofterm.thm_proof thy (classrel_proof thy) (arity_proof thy) name shyps hyps prop ps body; |
1016 Proofterm.thm_proof thy (classrel_proof thy) (arity_proof thy) |
|
1017 name_pos shyps hyps prop ps body; |
1017 val der' = make_deriv [] [] [pthm] proof; |
1018 val der' = make_deriv [] [] [pthm] proof; |
1018 in Thm (der', args) end); |
1019 in Thm (der', args) end); |
1019 |
1020 |
1020 val close_derivation = |
1021 fun close_derivation pos = |
1021 solve_constraints #> (fn thm => |
1022 solve_constraints #> (fn thm => |
1022 if derivation_closed thm then thm else name_derivation "" thm); |
1023 if derivation_closed thm then thm else name_derivation ("", pos) thm); |
1023 |
1024 |
1024 val trim_context = solve_constraints #> trim_context_thm; |
1025 val trim_context = solve_constraints #> trim_context_thm; |
1025 |
1026 |
1026 |
1027 |
1027 |
1028 |
1686 val tfrees = rev (Term.add_tfree_names prop []); |
1687 val tfrees = rev (Term.add_tfree_names prop []); |
1687 val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees); |
1688 val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees); |
1688 |
1689 |
1689 val ps = map (apsnd (Future.map fulfill_body)) promises; |
1690 val ps = map (apsnd (Future.map fulfill_body)) promises; |
1690 val (pthm, proof) = |
1691 val (pthm, proof) = |
1691 Proofterm.unconstrain_thm_proof thy (classrel_proof thy) (arity_proof thy) shyps prop ps body; |
1692 Proofterm.unconstrain_thm_proof thy (classrel_proof thy) (arity_proof thy) |
|
1693 shyps prop ps body; |
1692 val der' = make_deriv [] [] [pthm] proof; |
1694 val der' = make_deriv [] [] [pthm] proof; |
1693 val prop' = Proofterm.thm_node_prop (#2 pthm); |
1695 val prop' = Proofterm.thm_node_prop (#2 pthm); |
1694 in |
1696 in |
1695 Thm (der', |
1697 Thm (der', |
1696 {cert = cert, |
1698 {cert = cert, |
2205 (false, |
2207 (false, |
2206 thy2 |
2208 thy2 |
2207 |> (map_classrels o Symreltab.update) ((c1, c2), |
2209 |> (map_classrels o Symreltab.update) ((c1, c2), |
2208 (the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2)) |
2210 (the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2)) |
2209 |> standard_tvars |
2211 |> standard_tvars |
2210 |> close_derivation |
2212 |> close_derivation \<^here> |
2211 |> trim_context)); |
2213 |> trim_context)); |
2212 |
2214 |
2213 val proven = is_classrel thy1; |
2215 val proven = is_classrel thy1; |
2214 val preds = Graph.Keys.fold (fn c1 => proven (c1, c) ? cons c1) all_preds []; |
2216 val preds = Graph.Keys.fold (fn c1 => proven (c1, c) ? cons c1) all_preds []; |
2215 val succs = Graph.Keys.fold (fn c2 => proven (c, c2) ? cons c2) all_succs []; |
2217 val succs = Graph.Keys.fold (fn c2 => proven (c, c2) ? cons c2) all_succs []; |
2238 else |
2240 else |
2239 let |
2241 let |
2240 val th1 = |
2242 val th1 = |
2241 (th RS the_classrel thy (c, c1)) |
2243 (th RS the_classrel thy (c, c1)) |
2242 |> standard_tvars |
2244 |> standard_tvars |
2243 |> close_derivation |
2245 |> close_derivation \<^here> |
2244 |> trim_context; |
2246 |> trim_context; |
2245 in SOME ((t, Ss, c1), (th1, thy_name, ser)) end); |
2247 in SOME ((t, Ss, c1), (th1, thy_name, ser)) end); |
2246 val finished' = finished andalso null completions; |
2248 val finished' = finished andalso null completions; |
2247 val arities' = fold Aritytab.update completions arities; |
2249 val arities' = fold Aritytab.update completions arities; |
2248 in (finished', arities') end; |
2250 in (finished', arities') end; |