10 |
10 |
11 sledgehammer_params [prover = e, blocking, isar_proof, timeout = 10] |
11 sledgehammer_params [prover = e, blocking, isar_proof, timeout = 10] |
12 |
12 |
13 lemma "id True" |
13 lemma "id True" |
14 sledgehammer [expect = some] (id_apply) |
14 sledgehammer [expect = some] (id_apply) |
|
15 sledgehammer [type_sys = tags, expect = some] (id_apply) |
|
16 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
15 by (metis id_apply) |
17 by (metis id_apply) |
16 |
18 |
17 lemma "\<not> id False" |
19 lemma "\<not> id False" |
18 sledgehammer [expect = some] (id_apply) |
20 sledgehammer [expect = some] (id_apply) |
|
21 sledgehammer [type_sys = tags, expect = some] (id_apply) |
|
22 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
19 by (metis id_apply) |
23 by (metis id_apply) |
20 |
24 |
21 lemma "x = id True \<or> x = id False" |
25 lemma "x = id True \<or> x = id False" |
22 sledgehammer [expect = some] (id_apply) |
26 sledgehammer [expect = some] (id_apply) |
|
27 sledgehammer [type_sys = tags, expect = some] (id_apply) |
|
28 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
23 by (metis id_apply) |
29 by (metis id_apply) |
24 |
30 |
25 lemma "id x = id True \<or> id x = id False" |
31 lemma "id x = id True \<or> id x = id False" |
26 sledgehammer [expect = some] (id_apply) |
32 sledgehammer [expect = some] (id_apply) |
|
33 sledgehammer [type_sys = tags, expect = some] (id_apply) |
|
34 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
27 by (metis id_apply) |
35 by (metis id_apply) |
28 |
36 |
29 lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x" |
37 lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x" |
30 sledgehammer [expect = none] () |
38 sledgehammer [expect = none] () |
31 sledgehammer [full_types, expect = some] () |
39 sledgehammer [type_sys = tags, expect = some] () |
|
40 sledgehammer [full_types, type_sys = tags, expect = some] () |
32 by metisFT |
41 by metisFT |
33 |
42 |
34 lemma "id (\<not> a) \<Longrightarrow> \<not> id a" |
43 lemma "id (\<not> a) \<Longrightarrow> \<not> id a" |
35 sledgehammer [expect = some] (id_apply) |
44 sledgehammer [expect = some] (id_apply) |
|
45 sledgehammer [type_sys = tags, expect = some] (id_apply) |
|
46 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
36 by (metis id_apply) |
47 by (metis id_apply) |
37 |
48 |
38 lemma "id (\<not> \<not> a) \<Longrightarrow> id a" |
49 lemma "id (\<not> \<not> a) \<Longrightarrow> id a" |
39 sledgehammer [expect = some] () |
50 sledgehammer [expect = some] () |
|
51 sledgehammer [type_sys = tags, expect = some] () |
|
52 sledgehammer [full_types, type_sys = tags, expect = some] () |
40 by metis |
53 by metis |
41 |
54 |
42 lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a" |
55 lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a" |
43 sledgehammer [expect = some] (id_apply) |
56 sledgehammer [expect = some] (id_apply) |
|
57 sledgehammer [type_sys = tags, expect = some] (id_apply) |
|
58 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
44 by (metis id_apply) |
59 by (metis id_apply) |
45 |
60 |
46 lemma "id (a \<and> b) \<Longrightarrow> id a" |
61 lemma "id (a \<and> b) \<Longrightarrow> id a" |
47 sledgehammer [expect = some] (id_apply) |
62 sledgehammer [expect = some] (id_apply) |
|
63 sledgehammer [type_sys = tags, expect = some] (id_apply) |
|
64 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
48 by (metis id_apply) |
65 by (metis id_apply) |
49 |
66 |
50 lemma "id (a \<and> b) \<Longrightarrow> id b" |
67 lemma "id (a \<and> b) \<Longrightarrow> id b" |
51 sledgehammer [expect = some] (id_apply) |
68 sledgehammer [expect = some] (id_apply) |
|
69 sledgehammer [type_sys = tags, expect = some] (id_apply) |
|
70 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
52 by (metis id_apply) |
71 by (metis id_apply) |
53 |
72 |
54 lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)" |
73 lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)" |
55 sledgehammer [expect = some] (id_apply) |
74 sledgehammer [expect = some] (id_apply) |
|
75 sledgehammer [type_sys = tags, expect = some] (id_apply) |
|
76 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
56 by (metis id_apply) |
77 by (metis id_apply) |
57 |
78 |
58 lemma "id a \<Longrightarrow> id (a \<or> b)" |
79 lemma "id a \<Longrightarrow> id (a \<or> b)" |
59 sledgehammer [expect = some] (id_apply) |
80 sledgehammer [expect = some] (id_apply) |
|
81 sledgehammer [type_sys = tags, expect = some] (id_apply) |
|
82 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
60 by (metis id_apply) |
83 by (metis id_apply) |
61 |
84 |
62 lemma "id b \<Longrightarrow> id (a \<or> b)" |
85 lemma "id b \<Longrightarrow> id (a \<or> b)" |
63 sledgehammer [expect = some] (id_apply) |
86 sledgehammer [expect = some] (id_apply) |
|
87 sledgehammer [type_sys = tags, expect = some] (id_apply) |
|
88 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
64 by (metis id_apply) |
89 by (metis id_apply) |
65 |
90 |
66 lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))" |
91 lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))" |
67 sledgehammer [expect = some] (id_apply) |
92 sledgehammer [expect = some] (id_apply) |
|
93 sledgehammer [type_sys = tags, expect = some] (id_apply) |
|
94 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
68 by (metis id_apply) |
95 by (metis id_apply) |
69 |
96 |
70 lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)" |
97 lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)" |
71 sledgehammer [expect = some] (id_apply) |
98 sledgehammer [expect = some] (id_apply) |
|
99 sledgehammer [type_sys = tags, expect = some] (id_apply) |
|
100 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
72 by (metis id_apply) |
101 by (metis id_apply) |
73 |
102 |
74 lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)" |
103 lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)" |
75 sledgehammer [expect = some] (id_apply) |
104 sledgehammer [expect = some] (id_apply) |
|
105 sledgehammer [type_sys = tags, expect = some] (id_apply) |
|
106 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
76 by (metis id_apply) |
107 by (metis id_apply) |
77 |
108 |
78 end |
109 end |