60 sledgehammer [type_enc = erased, expect = none] (id_apply) |
60 sledgehammer [type_enc = erased, expect = none] (id_apply) |
61 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
61 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
62 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
62 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
63 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
63 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
64 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
64 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
65 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply) |
65 sledgehammer [type_enc = mono_tags?, expect = some] (id_apply) |
66 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply) |
66 sledgehammer [type_enc = mono_tags, expect = some] (id_apply) |
67 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply) |
67 sledgehammer [type_enc = mono_guards?, expect = some] (id_apply) |
68 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply) |
68 sledgehammer [type_enc = mono_guards, expect = some] (id_apply) |
69 by (metis (full_types) id_apply) |
69 by (metis (full_types) id_apply) |
70 |
70 |
71 lemma "id True" |
71 lemma "id True" |
72 sledgehammer [type_enc = erased, expect = some] (id_apply) |
72 sledgehammer [type_enc = erased, expect = some] (id_apply) |
73 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
73 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
74 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
74 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
75 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
75 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
76 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
76 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
77 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply) |
77 sledgehammer [type_enc = mono_tags?, expect = some] (id_apply) |
78 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply) |
78 sledgehammer [type_enc = mono_tags, expect = some] (id_apply) |
79 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply) |
79 sledgehammer [type_enc = mono_guards?, expect = some] (id_apply) |
80 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply) |
80 sledgehammer [type_enc = mono_guards, expect = some] (id_apply) |
81 by (metis_exhaust id_apply) |
81 by (metis_exhaust id_apply) |
82 |
82 |
83 lemma "\<not> id False" |
83 lemma "\<not> id False" |
84 sledgehammer [type_enc = erased, expect = some] (id_apply) |
84 sledgehammer [type_enc = erased, expect = some] (id_apply) |
85 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
85 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
86 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
86 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
87 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
87 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
88 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
88 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
89 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply) |
89 sledgehammer [type_enc = mono_tags?, expect = some] (id_apply) |
90 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply) |
90 sledgehammer [type_enc = mono_tags, expect = some] (id_apply) |
91 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply) |
91 sledgehammer [type_enc = mono_guards?, expect = some] (id_apply) |
92 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply) |
92 sledgehammer [type_enc = mono_guards, expect = some] (id_apply) |
93 by (metis_exhaust id_apply) |
93 by (metis_exhaust id_apply) |
94 |
94 |
95 lemma "x = id True \<or> x = id False" |
95 lemma "x = id True \<or> x = id False" |
96 sledgehammer [type_enc = erased, expect = some] (id_apply) |
96 sledgehammer [type_enc = erased, expect = some] (id_apply) |
97 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
97 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
98 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
98 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
99 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
99 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
100 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
100 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
101 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply) |
101 sledgehammer [type_enc = mono_tags?, expect = some] (id_apply) |
102 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply) |
102 sledgehammer [type_enc = mono_tags, expect = some] (id_apply) |
103 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply) |
103 sledgehammer [type_enc = mono_guards?, expect = some] (id_apply) |
104 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply) |
104 sledgehammer [type_enc = mono_guards, expect = some] (id_apply) |
105 by (metis_exhaust id_apply) |
105 by (metis_exhaust id_apply) |
106 |
106 |
107 lemma "id x = id True \<or> id x = id False" |
107 lemma "id x = id True \<or> id x = id False" |
108 sledgehammer [type_enc = erased, expect = some] (id_apply) |
108 sledgehammer [type_enc = erased, expect = some] (id_apply) |
109 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
109 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
110 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
110 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
111 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
111 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
112 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
112 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
113 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply) |
113 sledgehammer [type_enc = mono_tags?, expect = some] (id_apply) |
114 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply) |
114 sledgehammer [type_enc = mono_tags, expect = some] (id_apply) |
115 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply) |
115 sledgehammer [type_enc = mono_guards?, expect = some] (id_apply) |
116 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply) |
116 sledgehammer [type_enc = mono_guards, expect = some] (id_apply) |
117 by (metis_exhaust id_apply) |
117 by (metis_exhaust id_apply) |
118 |
118 |
119 lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x" |
119 lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x" |
120 sledgehammer [type_enc = erased, expect = none] () |
120 sledgehammer [type_enc = erased, expect = none] () |
121 sledgehammer [type_enc = poly_args, expect = none] () |
121 sledgehammer [type_enc = poly_args, expect = none] () |
122 sledgehammer [type_enc = poly_tags?, expect = some] () |
122 sledgehammer [type_enc = poly_tags?, expect = some] () |
123 sledgehammer [type_enc = poly_tags, expect = some] () |
123 sledgehammer [type_enc = poly_tags, expect = some] () |
124 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
124 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
125 sledgehammer [type_enc = poly_guards, expect = some] () |
125 sledgehammer [type_enc = poly_guards, expect = some] () |
126 sledgehammer [type_enc = mangled_tags?, expect = some] () |
126 sledgehammer [type_enc = mono_tags?, expect = some] () |
127 sledgehammer [type_enc = mangled_tags, expect = some] () |
127 sledgehammer [type_enc = mono_tags, expect = some] () |
128 sledgehammer [type_enc = mangled_guards?, expect = some] () |
128 sledgehammer [type_enc = mono_guards?, expect = some] () |
129 sledgehammer [type_enc = mangled_guards, expect = some] () |
129 sledgehammer [type_enc = mono_guards, expect = some] () |
130 by (metis (full_types)) |
130 by (metis (full_types)) |
131 |
131 |
132 lemma "id (\<not> a) \<Longrightarrow> \<not> id a" |
132 lemma "id (\<not> a) \<Longrightarrow> \<not> id a" |
133 sledgehammer [type_enc = erased, expect = some] (id_apply) |
133 sledgehammer [type_enc = erased, expect = some] (id_apply) |
134 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
134 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
135 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
135 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
136 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
136 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
137 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
137 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
138 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply) |
138 sledgehammer [type_enc = mono_tags?, expect = some] (id_apply) |
139 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply) |
139 sledgehammer [type_enc = mono_tags, expect = some] (id_apply) |
140 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply) |
140 sledgehammer [type_enc = mono_guards?, expect = some] (id_apply) |
141 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply) |
141 sledgehammer [type_enc = mono_guards, expect = some] (id_apply) |
142 by (metis_exhaust id_apply) |
142 by (metis_exhaust id_apply) |
143 |
143 |
144 lemma "id (\<not> \<not> a) \<Longrightarrow> id a" |
144 lemma "id (\<not> \<not> a) \<Longrightarrow> id a" |
145 sledgehammer [type_enc = erased, expect = some] (id_apply) |
145 sledgehammer [type_enc = erased, expect = some] (id_apply) |
146 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
146 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
147 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
147 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
148 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
148 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
149 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
149 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
150 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply) |
150 sledgehammer [type_enc = mono_tags?, expect = some] (id_apply) |
151 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply) |
151 sledgehammer [type_enc = mono_tags, expect = some] (id_apply) |
152 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply) |
152 sledgehammer [type_enc = mono_guards?, expect = some] (id_apply) |
153 sledgehammer [type_enc = mangled_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 id_apply) |
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) |
160 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
160 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
161 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
161 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
162 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply) |
162 sledgehammer [type_enc = mono_tags?, expect = some] (id_apply) |
163 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply) |
163 sledgehammer [type_enc = mono_tags, expect = some] (id_apply) |
164 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply) |
164 sledgehammer [type_enc = mono_guards?, expect = some] (id_apply) |
165 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply) |
165 sledgehammer [type_enc = mono_guards, expect = some] (id_apply) |
166 by (metis_exhaust id_apply) |
166 by (metis_exhaust id_apply) |
167 |
167 |
168 lemma "id (a \<and> b) \<Longrightarrow> id a" |
168 lemma "id (a \<and> b) \<Longrightarrow> id a" |
169 sledgehammer [type_enc = erased, expect = some] (id_apply) |
169 sledgehammer [type_enc = erased, expect = some] (id_apply) |
170 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
170 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
171 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
171 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
172 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
172 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
173 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
173 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
174 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply) |
174 sledgehammer [type_enc = mono_tags?, expect = some] (id_apply) |
175 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply) |
175 sledgehammer [type_enc = mono_tags, expect = some] (id_apply) |
176 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply) |
176 sledgehammer [type_enc = mono_guards?, expect = some] (id_apply) |
177 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply) |
177 sledgehammer [type_enc = mono_guards, expect = some] (id_apply) |
178 by (metis_exhaust id_apply) |
178 by (metis_exhaust id_apply) |
179 |
179 |
180 lemma "id (a \<and> b) \<Longrightarrow> id b" |
180 lemma "id (a \<and> b) \<Longrightarrow> id b" |
181 sledgehammer [type_enc = erased, expect = some] (id_apply) |
181 sledgehammer [type_enc = erased, expect = some] (id_apply) |
182 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
182 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
183 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
183 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
184 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
184 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
185 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
185 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
186 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply) |
186 sledgehammer [type_enc = mono_tags?, expect = some] (id_apply) |
187 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply) |
187 sledgehammer [type_enc = mono_tags, expect = some] (id_apply) |
188 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply) |
188 sledgehammer [type_enc = mono_guards?, expect = some] (id_apply) |
189 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply) |
189 sledgehammer [type_enc = mono_guards, expect = some] (id_apply) |
190 by (metis_exhaust id_apply) |
190 by (metis_exhaust id_apply) |
191 |
191 |
192 lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)" |
192 lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)" |
193 sledgehammer [type_enc = erased, expect = some] (id_apply) |
193 sledgehammer [type_enc = erased, expect = some] (id_apply) |
194 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
194 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
195 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
195 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
196 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
196 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
197 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
197 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
198 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply) |
198 sledgehammer [type_enc = mono_tags?, expect = some] (id_apply) |
199 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply) |
199 sledgehammer [type_enc = mono_tags, expect = some] (id_apply) |
200 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply) |
200 sledgehammer [type_enc = mono_guards?, expect = some] (id_apply) |
201 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply) |
201 sledgehammer [type_enc = mono_guards, expect = some] (id_apply) |
202 by (metis_exhaust id_apply) |
202 by (metis_exhaust id_apply) |
203 |
203 |
204 lemma "id a \<Longrightarrow> id (a \<or> b)" |
204 lemma "id a \<Longrightarrow> id (a \<or> b)" |
205 sledgehammer [type_enc = erased, expect = some] (id_apply) |
205 sledgehammer [type_enc = erased, expect = some] (id_apply) |
206 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
206 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
207 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
207 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
208 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
208 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
209 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
209 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
210 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply) |
210 sledgehammer [type_enc = mono_tags?, expect = some] (id_apply) |
211 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply) |
211 sledgehammer [type_enc = mono_tags, expect = some] (id_apply) |
212 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply) |
212 sledgehammer [type_enc = mono_guards?, expect = some] (id_apply) |
213 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply) |
213 sledgehammer [type_enc = mono_guards, expect = some] (id_apply) |
214 by (metis_exhaust id_apply) |
214 by (metis_exhaust id_apply) |
215 |
215 |
216 lemma "id b \<Longrightarrow> id (a \<or> b)" |
216 lemma "id b \<Longrightarrow> id (a \<or> b)" |
217 sledgehammer [type_enc = erased, expect = some] (id_apply) |
217 sledgehammer [type_enc = erased, expect = some] (id_apply) |
218 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
218 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
219 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
219 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
220 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
220 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
221 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
221 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
222 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply) |
222 sledgehammer [type_enc = mono_tags?, expect = some] (id_apply) |
223 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply) |
223 sledgehammer [type_enc = mono_tags, expect = some] (id_apply) |
224 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply) |
224 sledgehammer [type_enc = mono_guards?, expect = some] (id_apply) |
225 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply) |
225 sledgehammer [type_enc = mono_guards, expect = some] (id_apply) |
226 by (metis_exhaust id_apply) |
226 by (metis_exhaust id_apply) |
227 |
227 |
228 lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))" |
228 lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))" |
229 sledgehammer [type_enc = erased, expect = some] (id_apply) |
229 sledgehammer [type_enc = erased, expect = some] (id_apply) |
230 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
230 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
231 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
231 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
232 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
232 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
233 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
233 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
234 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply) |
234 sledgehammer [type_enc = mono_tags?, expect = some] (id_apply) |
235 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply) |
235 sledgehammer [type_enc = mono_tags, expect = some] (id_apply) |
236 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply) |
236 sledgehammer [type_enc = mono_guards?, expect = some] (id_apply) |
237 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply) |
237 sledgehammer [type_enc = mono_guards, expect = some] (id_apply) |
238 by (metis_exhaust id_apply) |
238 by (metis_exhaust id_apply) |
239 |
239 |
240 lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)" |
240 lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)" |
241 sledgehammer [type_enc = erased, expect = some] (id_apply) |
241 sledgehammer [type_enc = erased, expect = some] (id_apply) |
242 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
242 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
243 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
243 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
244 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
244 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
245 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
245 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
246 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply) |
246 sledgehammer [type_enc = mono_tags?, expect = some] (id_apply) |
247 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply) |
247 sledgehammer [type_enc = mono_tags, expect = some] (id_apply) |
248 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply) |
248 sledgehammer [type_enc = mono_guards?, expect = some] (id_apply) |
249 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply) |
249 sledgehammer [type_enc = mono_guards, expect = some] (id_apply) |
250 by (metis_exhaust id_apply) |
250 by (metis_exhaust id_apply) |
251 |
251 |
252 lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)" |
252 lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)" |
253 sledgehammer [type_enc = erased, expect = some] (id_apply) |
253 sledgehammer [type_enc = erased, expect = some] (id_apply) |
254 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
254 sledgehammer [type_enc = poly_tags?, expect = some] (id_apply) |
255 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
255 sledgehammer [type_enc = poly_tags, expect = some] (id_apply) |
256 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
256 sledgehammer [type_enc = poly_guards?, expect = some] (id_apply) |
257 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
257 sledgehammer [type_enc = poly_guards, expect = some] (id_apply) |
258 sledgehammer [type_enc = mangled_tags?, expect = some] (id_apply) |
258 sledgehammer [type_enc = mono_tags?, expect = some] (id_apply) |
259 sledgehammer [type_enc = mangled_tags, expect = some] (id_apply) |
259 sledgehammer [type_enc = mono_tags, expect = some] (id_apply) |
260 sledgehammer [type_enc = mangled_guards?, expect = some] (id_apply) |
260 sledgehammer [type_enc = mono_guards?, expect = some] (id_apply) |
261 sledgehammer [type_enc = mangled_guards, expect = some] (id_apply) |
261 sledgehammer [type_enc = mono_guards, expect = some] (id_apply) |
262 by (metis_exhaust id_apply) |
262 by (metis_exhaust id_apply) |
263 |
263 |
264 end |
264 end |