39 |
39 |
40 definition "A = {xs\<Colon>'a list. True}" |
40 definition "A = {xs\<Colon>'a list. True}" |
41 |
41 |
42 lemma "xs \<in> A" |
42 lemma "xs \<in> A" |
43 sledgehammer [expect = some] |
43 sledgehammer [expect = some] |
44 by (metis_exhaust A_def Collect_def mem_def) |
44 by (metis_exhaust A_def mem_Collect_eq) |
45 |
45 |
46 definition "B (y::int) \<equiv> y \<le> 0" |
46 definition "B (y::int) \<equiv> y \<le> 0" |
47 definition "C (y::int) \<equiv> y \<le> 1" |
47 definition "C (y::int) \<equiv> y \<le> 1" |
48 |
48 |
49 lemma int_le_0_imp_le_1: "x \<le> (0::int) \<Longrightarrow> x \<le> 1" |
49 lemma int_le_0_imp_le_1: "x \<le> (0::int) \<Longrightarrow> x \<le> 1" |
50 by linarith |
50 by linarith |
51 |
51 |
52 lemma "B \<subseteq> C" |
52 lemma "B \<le> C" |
53 sledgehammer [type_enc = poly_args, max_relevant = 100, expect = some] |
53 sledgehammer [type_enc = poly_args, max_relevant = 100, expect = some] |
54 by (metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I) |
54 by (metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I) |
55 |
55 |
56 |
56 |
57 text {* Proxies for logical constants *} |
57 text {* Proxies for logical constants *} |
149 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
149 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
150 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply) |
150 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply) |
151 sledgehammer [type_enc = mono_tags, expect = some] (id_apply) |
151 sledgehammer [type_enc = mono_tags, expect = some] (id_apply) |
152 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply) |
152 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply) |
153 sledgehammer [type_enc = mono_guards, expect = some] (id_apply) |
153 sledgehammer [type_enc = mono_guards, expect = some] (id_apply) |
154 by (metis_exhaust id_apply) |
154 by metis_exhaust |
155 |
155 |
156 lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a" |
156 lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a" |
157 sledgehammer [type_enc = erased, expect = some] (id_apply) |
157 sledgehammer [type_enc = erased, expect = some] (id_apply) |
158 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply) |
158 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply) |
159 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
159 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |