author | blanchet |
Mon, 31 Jan 2022 16:09:23 +0100 | |
changeset 75029 | dc6769b86fd6 |
parent 73684 | a63d76ba0a03 |
child 75030 | 919fb49ba201 |
permissions | -rw-r--r-- |
35827 | 1 |
(* Title: HOL/Sledgehammer.thy |
38027 | 2 |
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory |
38028 | 3 |
Author: Jia Meng, Cambridge University Computer Laboratory and NICTA |
35865 | 4 |
Author: Jasmin Blanchette, TU Muenchen |
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
5 |
*) |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
6 |
|
60758 | 7 |
section \<open>Sledgehammer: Isabelle--ATP Linkup\<close> |
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
8 |
|
35827 | 9 |
theory Sledgehammer |
58061 | 10 |
imports Presburger SMT |
63432 | 11 |
keywords |
12 |
"sledgehammer" :: diag and |
|
13 |
"sledgehammer_params" :: thy_decl |
|
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
14 |
begin |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
15 |
|
73418
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
72593
diff
changeset
|
16 |
ML_file \<open>Tools/ATP/system_on_tptp.ML\<close> |
69605 | 17 |
ML_file \<open>Tools/Sledgehammer/async_manager_legacy.ML\<close> |
18 |
ML_file \<open>Tools/Sledgehammer/sledgehammer_util.ML\<close> |
|
19 |
ML_file \<open>Tools/Sledgehammer/sledgehammer_fact.ML\<close> |
|
20 |
ML_file \<open>Tools/Sledgehammer/sledgehammer_proof_methods.ML\<close> |
|
21 |
ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_annotate.ML\<close> |
|
22 |
ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_proof.ML\<close> |
|
23 |
ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_preplay.ML\<close> |
|
24 |
ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_compress.ML\<close> |
|
25 |
ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_minimize.ML\<close> |
|
26 |
ML_file \<open>Tools/Sledgehammer/sledgehammer_isar.ML\<close> |
|
72400 | 27 |
ML_file \<open>Tools/Sledgehammer/sledgehammer_atp_systems.ML\<close> |
69605 | 28 |
ML_file \<open>Tools/Sledgehammer/sledgehammer_prover.ML\<close> |
29 |
ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_atp.ML\<close> |
|
30 |
ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_smt.ML\<close> |
|
31 |
ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_minimize.ML\<close> |
|
32 |
ML_file \<open>Tools/Sledgehammer/sledgehammer_mepo.ML\<close> |
|
33 |
ML_file \<open>Tools/Sledgehammer/sledgehammer_mash.ML\<close> |
|
34 |
ML_file \<open>Tools/Sledgehammer/sledgehammer.ML\<close> |
|
35 |
ML_file \<open>Tools/Sledgehammer/sledgehammer_commands.ML\<close> |
|
73684 | 36 |
ML_file \<open>Tools/Sledgehammer/sledgehammer_tactics.ML\<close> |
48891 | 37 |
|
75029 | 38 |
(* |
39 |
lemma "1 + 1 = 2 \<and> 0 + (x::nat) = x" |
|
40 |
sledgehammer |
|
41 |
*) |
|
42 |
||
43 |
(* |
|
44 |
declare nat_induct[no_atp] |
|
45 |
declare nat_induct_non_zero[no_atp] |
|
46 |
||
47 |
lemma "P 0 \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P n" |
|
48 |
sledgehammer [cvc4] (add: nat.induct) |
|
49 |
*) |
|
50 |
||
51 |
(* |
|
52 |
lemma "1 + 1 = 2 \<and> 0 + (x::nat) = x" |
|
53 |
sledgehammer [verbose, e, dont_preplay, max_facts = 2] (add_0_left one_add_one) |
|
54 |
*) |
|
55 |
||
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
56 |
end |