177 |
177 |
178 ML {* val a1 = lift_thm_lam @{context} @{thm a1} *} |
178 ML {* val a1 = lift_thm_lam @{context} @{thm a1} *} |
179 ML {* val a2 = lift_thm_lam @{context} @{thm a1} *} |
179 ML {* val a2 = lift_thm_lam @{context} @{thm a1} *} |
180 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *} |
180 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *} |
181 |
181 |
182 |
|
183 local_setup {* |
182 local_setup {* |
184 Quotient.note (@{binding "pi_var"}, pi_var) #> snd #> |
183 Quotient.note (@{binding "pi_var"}, pi_var) #> snd #> |
185 Quotient.note (@{binding "pi_app"}, pi_app) #> snd #> |
184 Quotient.note (@{binding "pi_app"}, pi_app) #> snd #> |
186 Quotient.note (@{binding "pi_lam"}, pi_lam) #> snd #> |
185 Quotient.note (@{binding "pi_lam"}, pi_lam) #> snd #> |
187 Quotient.note (@{binding "a1"}, a1) #> snd #> |
186 Quotient.note (@{binding "a1"}, a1) #> snd #> |
217 |
216 |
218 |
217 |
219 |
218 |
220 |
219 |
221 |
220 |
|
221 lemma get_rid: "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))" |
|
222 apply (auto) |
|
223 done |
|
224 |
|
225 lemma get_rid2: "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)" |
|
226 apply (auto) |
|
227 done |
|
228 |
|
229 ML {* val t_a = atomize_thm @{thm alpha.cases} *} |
|
230 prove {* build_regularize_goal t_a rty rel @{context} *} |
|
231 ML_prf {* fun tac ctxt = |
|
232 (FIRST' [ |
|
233 rtac rel_refl, |
|
234 atac, |
|
235 rtac @{thm get_rid}, |
|
236 rtac @{thm get_rid2}, |
|
237 (fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
|
238 [(@{thm equiv_res_forall} OF [rel_eqv]), |
|
239 (@{thm equiv_res_exists} OF [rel_eqv])]) i)), |
|
240 (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl) |
|
241 ]); |
|
242 *} |
|
243 apply (atomize(full)) |
|
244 apply (tactic {* tac @{context} 1 *}) |
|
245 apply (rule get_rid) |
|
246 apply (rule get_rid) |
|
247 apply (rule get_rid2) |
|
248 apply (simp) |
|
249 apply (rule get_rid) |
|
250 apply (rule get_rid2) |
|
251 apply (rule get_rid) |
|
252 apply (rule get_rid2) |
|
253 apply (rule impI) |
|
254 apply (simp) |
|
255 apply (tactic {* tac @{context} 1 *}) |
|
256 apply (rule get_rid2) |
|
257 apply (rule impI) |
|
258 apply (simp) |
|
259 apply (tactic {* tac @{context} 1 *}) |
|
260 apply (simp) |
|
261 apply (rule get_rid2) |
|
262 apply (rule get_rid) |
|
263 apply (rule get_rid) |
|
264 apply (rule get_rid) |
|
265 apply (rule get_rid2) |
|
266 apply (rule impI) |
|
267 apply (simp) |
|
268 apply (tactic {* tac @{context} 1 *}) |
|
269 apply (rule get_rid) |
|
270 apply (rule get_rid2) |
|
271 |
|
272 |
|
273 apply (tactic {* compose_tac (false, @{thm get_rid}, 1) 1 *}) |
|
274 ML_prf {* |
|
275 fun focus_compose t = Subgoal.FOCUS (fn {concl, ...} => |
|
276 rtac t 1) |
|
277 *} |
|
278 thm spec[of _ "x"] |
|
279 apply (rule allI) |
|
280 apply (drule_tac x="a2" in spec) |
|
281 apply (rule impI) |
|
282 apply (erule impE) |
|
283 apply (assumption) |
|
284 apply (rule allI) |
|
285 apply (drule_tac x="P" in spec) |
|
286 apply (atomize(full)) |
|
287 apply (rule allI) |
|
288 apply (rule allI) |
|
289 apply (rule allI) |
|
290 apply (rule impI) |
|
291 apply (rule get_rid2) |
|
292 |
|
293 thm get_rid2 |
|
294 apply (tactic {* compose_tac (false, @{thm get_rid2}, 0) 1 *}) |
|
295 |
|
296 thm spec |
|
297 |
|
298 ML_prf {* val t = snd (Subgoal.focus @{context} 1 (Isar.goal ())) *} |
|
299 ML_prf {* Seq.pull (compose_tac (false, @{thm get_rid}, 2) 1 t) *} |
|
300 |
|
301 |
|
302 thm get_rid |
|
303 apply (rule allI) |
|
304 apply (drule spec) |
|
305 |
|
306 thm spec |
|
307 apply (tactic {* compose_tac (false, @{thm get_rid}, 1) 1 *}) |
|
308 |
|
309 apply (tactic {* tac @{context} 1 *}) |
|
310 apply (tactic {* tac @{context} 1 *}) |
|
311 apply (rule impI) |
|
312 apply (erule impE) |
|
313 apply (assumption) |
|
314 apply (tactic {* tac @{context} 1 *}) |
|
315 apply (rule impI) |
|
316 apply (erule impE) |
|
317 apply (tactic {* tac @{context} 1 *}) |
|
318 apply (tactic {* tac @{context} 1 *}) |
|
319 apply (tactic {* tac @{context} 1 *}) |
|
320 apply (tactic {* tac @{context} 1 *}) |
|
321 |
|
322 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} |
|
323 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
|
324 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *} |
|
325 ML {* val t_a = simp_allex_prs @{context} quot t_l *} |
|
326 ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym |
222 |
327 |
223 |
328 |
224 |
329 |
225 |
330 |
226 fun |
331 fun |