75 val proof_banner : mode -> string -> string |
75 val proof_banner : mode -> string -> string |
76 val extract_reconstructor : params -> reconstructor -> string * (string * string list) list |
76 val extract_reconstructor : params -> reconstructor -> string * (string * string list) list |
77 val is_reconstructor : string -> bool |
77 val is_reconstructor : string -> bool |
78 val is_atp : theory -> string -> bool |
78 val is_atp : theory -> string -> bool |
79 val is_ho_atp: Proof.context -> string -> bool |
79 val is_ho_atp: Proof.context -> string -> bool |
80 val is_unit_equational_atp : Proof.context -> string -> bool |
|
81 val is_unit_equality : term -> bool |
|
82 val is_appropriate_prop_of_prover : Proof.context -> string -> term -> bool |
|
83 val supported_provers : Proof.context -> unit |
80 val supported_provers : Proof.context -> unit |
84 val kill_provers : unit -> unit |
81 val kill_provers : unit -> unit |
85 val running_provers : unit -> unit |
82 val running_provers : unit -> unit |
86 val messages : int option -> unit |
83 val messages : int option -> unit |
87 val is_fact_chained : (('a * stature) * 'b) -> bool |
84 val is_fact_chained : (('a * stature) * 'b) -> bool |
144 SOME config => |
141 SOME config => |
145 exists (fn (_, ((_, format, _, _, _), _)) => is_format format) (#best_slices (config ()) ctxt) |
142 exists (fn (_, ((_, format, _, _, _), _)) => is_format format) (#best_slices (config ()) ctxt) |
146 | NONE => false) |
143 | NONE => false) |
147 end |
144 end |
148 |
145 |
149 val is_unit_equational_atp = is_atp_of_format (curry (op =) CNF_UEQ) |
|
150 val is_ho_atp = is_atp_of_format is_format_higher_order |
146 val is_ho_atp = is_atp_of_format is_format_higher_order |
151 |
147 |
152 fun remotify_atp_if_supported_and_not_already_remote thy name = |
148 fun remotify_atp_if_supported_and_not_already_remote thy name = |
153 if String.isPrefix remote_prefix name then |
149 if String.isPrefix remote_prefix name then |
154 SOME name |
150 SOME name |
158 end |
154 end |
159 |
155 |
160 fun remotify_atp_if_not_installed thy name = |
156 fun remotify_atp_if_not_installed thy name = |
161 if is_atp thy name andalso is_atp_installed thy name then SOME name |
157 if is_atp thy name andalso is_atp_installed thy name then SOME name |
162 else remotify_atp_if_supported_and_not_already_remote thy name |
158 else remotify_atp_if_supported_and_not_already_remote thy name |
163 |
|
164 fun is_if (@{const_name If}, _) = true |
|
165 | is_if _ = false |
|
166 |
|
167 (* Beware of "if and only if" (which is translated as such) and "If" (which is |
|
168 translated to conditional equations). *) |
|
169 fun is_good_unit_equality T t u = |
|
170 T <> @{typ bool} andalso not (exists (exists_Const is_if) [t, u]) |
|
171 |
|
172 fun is_unit_equality (@{const Trueprop} $ t) = is_unit_equality t |
|
173 | is_unit_equality (Const (@{const_name all}, _) $ Abs (_, _, t)) = |
|
174 is_unit_equality t |
|
175 | is_unit_equality (Const (@{const_name All}, _) $ Abs (_, _, t)) = |
|
176 is_unit_equality t |
|
177 | is_unit_equality (Const (@{const_name "=="}, Type (_, [T, _])) $ t $ u) = |
|
178 is_good_unit_equality T t u |
|
179 | is_unit_equality (Const (@{const_name HOL.eq}, Type (_ , [T, _])) $ t $ u) = |
|
180 is_good_unit_equality T t u |
|
181 | is_unit_equality _ = false |
|
182 |
|
183 fun is_appropriate_prop_of_prover ctxt name = |
|
184 if is_unit_equational_atp ctxt name then is_unit_equality else K true |
|
185 |
159 |
186 fun supported_provers ctxt = |
160 fun supported_provers ctxt = |
187 let |
161 let |
188 val thy = Proof_Context.theory_of ctxt |
162 val thy = Proof_Context.theory_of ctxt |
189 val (remote_provers, local_provers) = |
163 val (remote_provers, local_provers) = |