equal
deleted
inserted
replaced
3 |
3 |
4 Example that exercises Metis's and Sledgehammer's logical symbol proxies for |
4 Example that exercises Metis's and Sledgehammer's logical symbol proxies for |
5 rudimentary higher-order reasoning. |
5 rudimentary higher-order reasoning. |
6 *) |
6 *) |
7 |
7 |
8 section {* |
8 section \<open> |
9 Example that Exercises Metis's and Sledgehammer's Logical Symbol Proxies for |
9 Example that Exercises Metis's and Sledgehammer's Logical Symbol Proxies for |
10 Rudimentary Higher-Order Reasoning. |
10 Rudimentary Higher-Order Reasoning. |
11 *} |
11 \<close> |
12 |
12 |
13 theory Proxies |
13 theory Proxies |
14 imports Type_Encodings |
14 imports Type_Encodings |
15 begin |
15 begin |
16 |
16 |
17 sledgehammer_params [prover = spass, fact_filter = mepo, timeout = 30, preplay_timeout = 0, |
17 sledgehammer_params [prover = spass, fact_filter = mepo, timeout = 30, preplay_timeout = 0, |
18 dont_minimize] |
18 dont_minimize] |
19 |
19 |
20 text {* Extensionality and set constants *} |
20 text \<open>Extensionality and set constants\<close> |
21 |
21 |
22 lemma plus_1_not_0: "n + (1::nat) \<noteq> 0" |
22 lemma plus_1_not_0: "n + (1::nat) \<noteq> 0" |
23 by simp |
23 by simp |
24 |
24 |
25 definition inc :: "nat \<Rightarrow> nat" where |
25 definition inc :: "nat \<Rightarrow> nat" where |
55 |
55 |
56 lemma "B \<le> C" |
56 lemma "B \<le> C" |
57 sledgehammer [expect = some] |
57 sledgehammer [expect = some] |
58 by (metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I) |
58 by (metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I) |
59 |
59 |
60 text {* Proxies for logical constants *} |
60 text \<open>Proxies for logical constants\<close> |
61 |
61 |
62 lemma "id (op =) x x" |
62 lemma "id (op =) x x" |
63 sledgehammer [type_enc = erased, expect = none] (id_apply) |
63 sledgehammer [type_enc = erased, expect = none] (id_apply) |
64 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply) |
64 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply) |
65 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
65 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |