8 imports Main |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
11 declare [[metis_new_skolemizer]] |
11 declare [[metis_new_skolemizer]] |
12 |
12 |
13 sledgehammer_params [prover = e, blocking, isar_proof, timeout = 10] |
13 sledgehammer_params [prover = e, blocking, timeout = 10] |
14 |
14 |
15 lemma "id True" |
15 lemma "id True" |
16 sledgehammer [expect = some] (id_apply) |
16 sledgehammer [partial_types, type_sys = none, expect = some] (id_apply) |
17 sledgehammer [type_sys = tags, expect = some] (id_apply) |
17 sledgehammer [partial_types, type_sys = tags, expect = some] (id_apply) |
|
18 sledgehammer [partial_types, type_sys = args, expect = some] (id_apply) |
|
19 sledgehammer [partial_types, type_sys = mangled, expect = some] (id_apply) |
|
20 sledgehammer [full_types, type_sys = none, expect = some] (id_apply) |
18 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
21 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
|
22 sledgehammer [full_types, type_sys = args, expect = some] (id_apply) |
|
23 sledgehammer [full_types, type_sys = mangled, expect = some] (id_apply) |
19 by (metis id_apply) |
24 by (metis id_apply) |
20 |
25 |
21 lemma "\<not> id False" |
26 lemma "\<not> id False" |
22 sledgehammer [expect = some] (id_apply) |
27 sledgehammer [partial_types, type_sys = none, expect = some] (id_apply) |
23 sledgehammer [type_sys = tags, expect = some] (id_apply) |
28 sledgehammer [partial_types, type_sys = tags, expect = some] (id_apply) |
|
29 sledgehammer [partial_types, type_sys = args, expect = some] (id_apply) |
|
30 sledgehammer [partial_types, type_sys = mangled, expect = some] (id_apply) |
|
31 sledgehammer [full_types, type_sys = none, expect = some] (id_apply) |
24 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
32 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
|
33 sledgehammer [full_types, type_sys = args, expect = some] (id_apply) |
|
34 sledgehammer [full_types, type_sys = mangled, expect = some] (id_apply) |
25 by (metis id_apply) |
35 by (metis id_apply) |
26 |
36 |
27 lemma "x = id True \<or> x = id False" |
37 lemma "x = id True \<or> x = id False" |
28 sledgehammer [expect = some] (id_apply) |
38 sledgehammer [partial_types, type_sys = none, expect = some] (id_apply) |
29 sledgehammer [type_sys = tags, expect = some] (id_apply) |
39 sledgehammer [partial_types, type_sys = tags, expect = some] (id_apply) |
|
40 sledgehammer [partial_types, type_sys = args, expect = some] (id_apply) |
|
41 sledgehammer [partial_types, type_sys = mangled, expect = some] (id_apply) |
|
42 sledgehammer [full_types, type_sys = none, expect = some] (id_apply) |
30 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
43 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
|
44 sledgehammer [full_types, type_sys = args, expect = some] (id_apply) |
|
45 sledgehammer [full_types, type_sys = mangled, expect = some] (id_apply) |
31 by (metis id_apply) |
46 by (metis id_apply) |
32 |
47 |
33 lemma "id x = id True \<or> id x = id False" |
48 lemma "id x = id True \<or> id x = id False" |
34 sledgehammer [expect = some] (id_apply) |
49 sledgehammer [partial_types, type_sys = none, expect = some] (id_apply) |
35 sledgehammer [type_sys = tags, expect = some] (id_apply) |
50 sledgehammer [partial_types, type_sys = tags, expect = some] (id_apply) |
|
51 sledgehammer [partial_types, type_sys = args, expect = some] (id_apply) |
|
52 sledgehammer [partial_types, type_sys = mangled, expect = some] (id_apply) |
|
53 sledgehammer [full_types, type_sys = none, expect = some] (id_apply) |
36 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
54 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
|
55 sledgehammer [full_types, type_sys = args, expect = some] (id_apply) |
|
56 sledgehammer [full_types, type_sys = mangled, expect = some] (id_apply) |
37 by (metis id_apply) |
57 by (metis id_apply) |
38 |
58 |
39 lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x" |
59 lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x" |
40 sledgehammer [expect = none] () |
60 sledgehammer [partial_types, type_sys = none, expect = none] () |
41 sledgehammer [type_sys = tags, expect = some] () |
61 sledgehammer [partial_types, type_sys = tags, expect = some] () |
|
62 sledgehammer [partial_types, type_sys = args, expect = none] () |
|
63 sledgehammer [partial_types, type_sys = mangled, expect = none] () |
|
64 sledgehammer [full_types, type_sys = none, expect = some] () |
42 sledgehammer [full_types, type_sys = tags, expect = some] () |
65 sledgehammer [full_types, type_sys = tags, expect = some] () |
|
66 sledgehammer [full_types, type_sys = args, expect = some] () |
|
67 sledgehammer [full_types, type_sys = mangled, expect = some] () |
43 by metisFT |
68 by metisFT |
44 |
69 |
45 lemma "id (\<not> a) \<Longrightarrow> \<not> id a" |
70 lemma "id (\<not> a) \<Longrightarrow> \<not> id a" |
46 sledgehammer [expect = some] (id_apply) |
71 sledgehammer [partial_types, type_sys = none, expect = some] (id_apply) |
47 sledgehammer [type_sys = tags, expect = some] (id_apply) |
72 sledgehammer [partial_types, type_sys = tags, expect = some] (id_apply) |
|
73 sledgehammer [partial_types, type_sys = args, expect = some] (id_apply) |
|
74 sledgehammer [partial_types, type_sys = mangled, expect = some] (id_apply) |
|
75 sledgehammer [full_types, type_sys = none, expect = some] (id_apply) |
48 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
76 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
|
77 sledgehammer [full_types, type_sys = args, expect = some] (id_apply) |
|
78 sledgehammer [full_types, type_sys = mangled, expect = some] (id_apply) |
49 by (metis id_apply) |
79 by (metis id_apply) |
50 |
80 |
51 lemma "id (\<not> \<not> a) \<Longrightarrow> id a" |
81 lemma "id (\<not> \<not> a) \<Longrightarrow> id a" |
52 sledgehammer [expect = some] () |
82 sledgehammer [partial_types, type_sys = none, expect = some] (id_apply) |
53 sledgehammer [type_sys = tags, expect = some] () |
83 sledgehammer [partial_types, type_sys = tags, expect = some] (id_apply) |
54 sledgehammer [full_types, type_sys = tags, expect = some] () |
84 sledgehammer [partial_types, type_sys = args, expect = some] (id_apply) |
55 by metis |
85 sledgehammer [partial_types, type_sys = mangled, expect = some] (id_apply) |
|
86 sledgehammer [full_types, type_sys = none, expect = some] (id_apply) |
|
87 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
|
88 sledgehammer [full_types, type_sys = args, expect = some] (id_apply) |
|
89 sledgehammer [full_types, type_sys = mangled, expect = some] (id_apply) |
|
90 by (metis id_apply) |
56 |
91 |
57 lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a" |
92 lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a" |
58 sledgehammer [expect = some] (id_apply) |
93 sledgehammer [partial_types, type_sys = none, expect = some] (id_apply) |
59 sledgehammer [type_sys = tags, expect = some] (id_apply) |
94 sledgehammer [partial_types, type_sys = tags, expect = some] (id_apply) |
|
95 sledgehammer [partial_types, type_sys = args, expect = some] (id_apply) |
|
96 sledgehammer [partial_types, type_sys = mangled, expect = some] (id_apply) |
|
97 sledgehammer [full_types, type_sys = none, expect = some] (id_apply) |
60 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
98 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
|
99 sledgehammer [full_types, type_sys = args, expect = some] (id_apply) |
|
100 sledgehammer [full_types, type_sys = mangled, expect = some] (id_apply) |
61 by (metis id_apply) |
101 by (metis id_apply) |
62 |
102 |
63 lemma "id (a \<and> b) \<Longrightarrow> id a" |
103 lemma "id (a \<and> b) \<Longrightarrow> id a" |
64 sledgehammer [expect = some] (id_apply) |
104 sledgehammer [partial_types, type_sys = none, expect = some] (id_apply) |
65 sledgehammer [type_sys = tags, expect = some] (id_apply) |
105 sledgehammer [partial_types, type_sys = tags, expect = some] (id_apply) |
|
106 sledgehammer [partial_types, type_sys = args, expect = some] (id_apply) |
|
107 sledgehammer [partial_types, type_sys = mangled, expect = some] (id_apply) |
|
108 sledgehammer [full_types, type_sys = none, expect = some] (id_apply) |
66 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
109 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
|
110 sledgehammer [full_types, type_sys = args, expect = some] (id_apply) |
|
111 sledgehammer [full_types, type_sys = mangled, expect = some] (id_apply) |
67 by (metis id_apply) |
112 by (metis id_apply) |
68 |
113 |
69 lemma "id (a \<and> b) \<Longrightarrow> id b" |
114 lemma "id (a \<and> b) \<Longrightarrow> id b" |
70 sledgehammer [expect = some] (id_apply) |
115 sledgehammer [partial_types, type_sys = none, expect = some] (id_apply) |
71 sledgehammer [type_sys = tags, expect = some] (id_apply) |
116 sledgehammer [partial_types, type_sys = tags, expect = some] (id_apply) |
|
117 sledgehammer [partial_types, type_sys = args, expect = some] (id_apply) |
|
118 sledgehammer [partial_types, type_sys = mangled, expect = some] (id_apply) |
|
119 sledgehammer [full_types, type_sys = none, expect = some] (id_apply) |
72 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
120 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
|
121 sledgehammer [full_types, type_sys = args, expect = some] (id_apply) |
|
122 sledgehammer [full_types, type_sys = mangled, expect = some] (id_apply) |
73 by (metis id_apply) |
123 by (metis id_apply) |
74 |
124 |
75 lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)" |
125 lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)" |
76 sledgehammer [expect = some] (id_apply) |
126 sledgehammer [partial_types, type_sys = none, expect = some] (id_apply) |
77 sledgehammer [type_sys = tags, expect = some] (id_apply) |
127 sledgehammer [partial_types, type_sys = tags, expect = some] (id_apply) |
|
128 sledgehammer [partial_types, type_sys = args, expect = some] (id_apply) |
|
129 sledgehammer [partial_types, type_sys = mangled, expect = some] (id_apply) |
|
130 sledgehammer [full_types, type_sys = none, expect = some] (id_apply) |
78 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
131 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
|
132 sledgehammer [full_types, type_sys = args, expect = some] (id_apply) |
|
133 sledgehammer [full_types, type_sys = mangled, expect = some] (id_apply) |
79 by (metis id_apply) |
134 by (metis id_apply) |
80 |
135 |
81 lemma "id a \<Longrightarrow> id (a \<or> b)" |
136 lemma "id a \<Longrightarrow> id (a \<or> b)" |
82 sledgehammer [expect = some] (id_apply) |
137 sledgehammer [partial_types, type_sys = none, expect = some] (id_apply) |
83 sledgehammer [type_sys = tags, expect = some] (id_apply) |
138 sledgehammer [partial_types, type_sys = tags, expect = some] (id_apply) |
|
139 sledgehammer [partial_types, type_sys = args, expect = some] (id_apply) |
|
140 sledgehammer [partial_types, type_sys = mangled, expect = some] (id_apply) |
|
141 sledgehammer [full_types, type_sys = none, expect = some] (id_apply) |
84 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
142 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
|
143 sledgehammer [full_types, type_sys = args, expect = some] (id_apply) |
|
144 sledgehammer [full_types, type_sys = mangled, expect = some] (id_apply) |
85 by (metis id_apply) |
145 by (metis id_apply) |
86 |
146 |
87 lemma "id b \<Longrightarrow> id (a \<or> b)" |
147 lemma "id b \<Longrightarrow> id (a \<or> b)" |
88 sledgehammer [expect = some] (id_apply) |
148 sledgehammer [partial_types, type_sys = none, expect = some] (id_apply) |
89 sledgehammer [type_sys = tags, expect = some] (id_apply) |
149 sledgehammer [partial_types, type_sys = tags, expect = some] (id_apply) |
|
150 sledgehammer [partial_types, type_sys = args, expect = some] (id_apply) |
|
151 sledgehammer [partial_types, type_sys = mangled, expect = some] (id_apply) |
|
152 sledgehammer [full_types, type_sys = none, expect = some] (id_apply) |
90 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
153 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
|
154 sledgehammer [full_types, type_sys = args, expect = some] (id_apply) |
|
155 sledgehammer [full_types, type_sys = mangled, expect = some] (id_apply) |
91 by (metis id_apply) |
156 by (metis id_apply) |
92 |
157 |
93 lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))" |
158 lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))" |
94 sledgehammer [expect = some] (id_apply) |
159 sledgehammer [partial_types, type_sys = none, expect = some] (id_apply) |
95 sledgehammer [type_sys = tags, expect = some] (id_apply) |
160 sledgehammer [partial_types, type_sys = tags, expect = some] (id_apply) |
|
161 sledgehammer [partial_types, type_sys = args, expect = some] (id_apply) |
|
162 sledgehammer [partial_types, type_sys = mangled, expect = some] (id_apply) |
|
163 sledgehammer [full_types, type_sys = none, expect = some] (id_apply) |
96 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
164 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
|
165 sledgehammer [full_types, type_sys = args, expect = some] (id_apply) |
|
166 sledgehammer [full_types, type_sys = mangled, expect = some] (id_apply) |
97 by (metis id_apply) |
167 by (metis id_apply) |
98 |
168 |
99 lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)" |
169 lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)" |
100 sledgehammer [expect = some] (id_apply) |
170 sledgehammer [partial_types, type_sys = none, expect = some] (id_apply) |
101 sledgehammer [type_sys = tags, expect = some] (id_apply) |
171 sledgehammer [partial_types, type_sys = tags, expect = some] (id_apply) |
|
172 sledgehammer [partial_types, type_sys = args, expect = some] (id_apply) |
|
173 sledgehammer [partial_types, type_sys = mangled, expect = some] (id_apply) |
|
174 sledgehammer [full_types, type_sys = none, expect = some] (id_apply) |
102 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
175 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
|
176 sledgehammer [full_types, type_sys = args, expect = some] (id_apply) |
|
177 sledgehammer [full_types, type_sys = mangled, expect = some] (id_apply) |
103 by (metis id_apply) |
178 by (metis id_apply) |
104 |
179 |
105 lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)" |
180 lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)" |
106 sledgehammer [expect = some] (id_apply) |
181 sledgehammer [partial_types, type_sys = none, expect = some] (id_apply) |
107 sledgehammer [type_sys = tags, expect = some] (id_apply) |
182 sledgehammer [partial_types, type_sys = tags, expect = some] (id_apply) |
|
183 sledgehammer [partial_types, type_sys = args, expect = some] (id_apply) |
|
184 sledgehammer [partial_types, type_sys = mangled, expect = some] (id_apply) |
|
185 sledgehammer [full_types, type_sys = none, expect = some] (id_apply) |
108 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
186 sledgehammer [full_types, type_sys = tags, expect = some] (id_apply) |
|
187 sledgehammer [full_types, type_sys = args, expect = some] (id_apply) |
|
188 sledgehammer [full_types, type_sys = mangled, expect = some] (id_apply) |
109 by (metis id_apply) |
189 by (metis id_apply) |
110 |
190 |
111 end |
191 end |