126 type isar_params = |
126 type isar_params = |
127 bool * (string option * string option) * Time.time * real option * bool * bool |
127 bool * (string option * string option) * Time.time * real option * bool * bool |
128 * (term, string) atp_step list * thm |
128 * (term, string) atp_step list * thm |
129 |
129 |
130 val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method] |
130 val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method] |
131 val basic_simp_based_methods = [Auto_Method, Simp_Method, Force_Method] |
131 val basic_simp_based_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method] |
132 val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method] |
132 val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method] |
133 |
133 |
134 val arith_methods = basic_arith_methods @ basic_simp_based_methods @ basic_systematic_methods |
134 val arith_methods = basic_arith_methods @ basic_simp_based_methods @ basic_systematic_methods |
135 val datatype_methods = [Simp_Method, Simp_Size_Method] |
135 val datatype_methods = [Simp_Method, Simp_Size_Method] |
136 val systematic_methods = |
136 val systematic_methods = |
137 basic_systematic_methods @ basic_arith_methods @ basic_simp_based_methods @ |
137 basic_systematic_methods @ basic_arith_methods @ basic_simp_based_methods @ |
138 [Metis_Method (SOME full_typesN, NONE), Metis_Method (SOME no_typesN, NONE)] |
138 [Metis_Method (SOME full_typesN, NONE), Metis_Method (SOME no_typesN, NONE)] |
139 val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods |
139 val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods |
140 fun skolem_methods_of z3 = (basic_systematic_methods, [Skolem_Method]) |> z3 ? swap |> op @ |
140 fun skolem_methods_of z3 = basic_systematic_methods |> z3 ? cons Moura_Method |
141 |
141 |
142 fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params |
142 fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params |
143 (one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) = |
143 (one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) = |
144 let |
144 let |
145 val _ = if debug then Output.urgent_message "Constructing Isar proof..." else () |
145 val _ = if debug then Output.urgent_message "Constructing Isar proof..." else () |