235 apply (induct_tac "l") |
237 apply (induct_tac "l") |
236 apply (simp) |
238 apply (simp) |
237 apply (metis) |
239 apply (metis) |
238 done |
240 done |
239 |
241 |
240 ML {* |
|
241 fun regularize thm rty rel rel_eqv lthy = |
|
242 let |
|
243 val g = build_regularize_goal thm rty rel lthy; |
|
244 fun tac ctxt = |
|
245 (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
|
246 [(@{thm equiv_res_forall} OF [rel_eqv]), |
|
247 (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW |
|
248 (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN' |
|
249 (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt [])); |
|
250 val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1); |
|
251 in |
|
252 cthm OF [thm] |
|
253 end |
|
254 *} |
|
255 |
|
256 |
|
257 prove list_induct_r: {* |
242 prove list_induct_r: {* |
258 build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
243 build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
259 apply (simp only: equiv_res_forall[OF equiv_list_eq]) |
244 apply (simp only: equiv_res_forall[OF equiv_list_eq]) |
260 thm RIGHT_RES_FORALL_REGULAR |
245 thm RIGHT_RES_FORALL_REGULAR |
261 apply (rule RIGHT_RES_FORALL_REGULAR) |
246 apply (rule RIGHT_RES_FORALL_REGULAR) |
262 prefer 2 |
247 prefer 2 |
263 apply (assumption) |
248 apply (assumption) |
264 apply (metis) |
249 apply (metis) |
265 done |
250 done |
266 |
|
267 ML {* |
|
268 fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} => |
|
269 let |
|
270 val pat = Drule.strip_imp_concl (cprop_of thm) |
|
271 val insts = Thm.match (pat, concl) |
|
272 in |
|
273 rtac (Drule.instantiate insts thm) 1 |
|
274 end |
|
275 handle _ => no_tac |
|
276 ) |
|
277 *} |
|
278 |
|
279 ML {* |
|
280 fun res_forall_rsp_tac ctxt = |
|
281 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
|
282 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
|
283 THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' |
|
284 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
|
285 *} |
|
286 |
|
287 ML {* |
|
288 fun res_exists_rsp_tac ctxt = |
|
289 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
|
290 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
|
291 THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN' |
|
292 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
|
293 *} |
|
294 |
|
295 |
|
296 ML {* |
|
297 fun quotient_tac quot_thm = |
|
298 REPEAT_ALL_NEW (FIRST' [ |
|
299 rtac @{thm FUN_QUOTIENT}, |
|
300 rtac quot_thm, |
|
301 rtac @{thm IDENTITY_QUOTIENT} |
|
302 ]) |
|
303 *} |
|
304 |
|
305 ML {* |
|
306 fun LAMBDA_RES_TAC ctxt i st = |
|
307 (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of |
|
308 (_ $ (_ $ (Abs(_,_,_))$(Abs(_,_,_)))) => |
|
309 (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' |
|
310 (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) |
|
311 | _ => fn _ => no_tac) i st |
|
312 *} |
|
313 |
|
314 ML {* |
|
315 fun WEAK_LAMBDA_RES_TAC ctxt i st = |
|
316 (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of |
|
317 (_ $ (_ $ _$(Abs(_,_,_)))) => |
|
318 (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' |
|
319 (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) |
|
320 | (_ $ (_ $ (Abs(_,_,_))$_)) => |
|
321 (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' |
|
322 (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) |
|
323 | _ => fn _ => no_tac) i st |
|
324 *} |
|
325 |
|
326 |
|
327 ML {* |
|
328 fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms = |
|
329 (FIRST' [ |
|
330 rtac @{thm FUN_QUOTIENT}, |
|
331 rtac quot_thm, |
|
332 rtac @{thm IDENTITY_QUOTIENT}, |
|
333 rtac @{thm ext}, |
|
334 rtac trans_thm, |
|
335 LAMBDA_RES_TAC ctxt, |
|
336 res_forall_rsp_tac ctxt, |
|
337 res_exists_rsp_tac ctxt, |
|
338 ( |
|
339 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps (rsp_thms @ @{thms ho_all_prs ho_ex_prs}))) |
|
340 THEN_ALL_NEW (fn _ => no_tac) |
|
341 ), |
|
342 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
|
343 rtac refl, |
|
344 (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
|
345 rtac reflex_thm, |
|
346 atac, |
|
347 ( |
|
348 (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps})) |
|
349 THEN_ALL_NEW (fn _ => no_tac) |
|
350 ), |
|
351 WEAK_LAMBDA_RES_TAC ctxt |
|
352 ]) |
|
353 *} |
|
354 |
251 |
355 ML {* |
252 ML {* |
356 fun repabs_eq lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms = |
253 fun repabs_eq lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms = |
357 let |
254 let |
358 val rt = build_repabs_term lthy thm constructors rty qty; |
255 val rt = build_repabs_term lthy thm constructors rty qty; |
465 apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *}) |
363 apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *}) |
466 apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *}) |
364 apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *}) |
467 done |
365 done |
468 thm HOL.sym[OF lambda_prs_lb_b,simplified] |
366 thm HOL.sym[OF lambda_prs_lb_b,simplified] |
469 |
367 |
470 ML {* |
368 |
471 fun eqsubst_thm ctxt thms thm = |
|
472 let |
|
473 val goalstate = Goal.init (Thm.cprop_of thm) |
|
474 val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of |
|
475 NONE => error "eqsubst_thm" |
|
476 | SOME th => cprem_of th 1 |
|
477 val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1 |
|
478 val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a')) |
|
479 val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac)); |
|
480 in |
|
481 Simplifier.rewrite_rule [rt] thm |
|
482 end |
|
483 *} |
|
484 |
369 |
485 |
370 |
486 ML {* |
371 ML {* |
487 fun simp_lam_prs lthy thm = |
372 fun simp_lam_prs lthy thm = |
488 simp_lam_prs lthy (eqsubst_thm lthy |
373 simp_lam_prs lthy (eqsubst_thm lthy |
562 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})*) |
447 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})*) |
563 ML {* val (g, thm, othm) = |
448 ML {* val (g, thm, othm) = |
564 Toplevel.program (fn () => |
449 Toplevel.program (fn () => |
565 repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
450 repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
566 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
451 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
567 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp} |
452 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp} @ @{thms ho_all_prs ho_ex_prs}) |
568 ) |
453 ) |
569 *} |
454 *} |
570 ML {* |
455 ML {* |
571 fun tac2 ctxt = |
456 fun tac2 ctxt = |
572 (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm])) |
457 (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm])) |
590 ML {* val ind_r_l3 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l2 *} |
475 ML {* val ind_r_l3 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l2 *} |
591 ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *} |
476 ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *} |
592 ML {* val ind_r_a = simp_allex_prs @{context} ind_r_l4 *} |
477 ML {* val ind_r_a = simp_allex_prs @{context} ind_r_l4 *} |
593 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *} |
478 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *} |
594 ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *} |
479 ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *} |
|
480 |
595 ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a1 *} |
481 ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a1 *} |
596 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} |
482 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} |
597 ML {* ObjectLogic.rulify ind_r_s *} |
483 ML {* ObjectLogic.rulify ind_r_s *} |
598 |
484 |
599 ML {* |
485 ML {* |
602 val ind_r_a = atomize_thm thm; |
488 val ind_r_a = atomize_thm thm; |
603 val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context}; |
489 val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context}; |
604 val (g, t, ot) = |
490 val (g, t, ot) = |
605 repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
491 repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
606 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
492 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
607 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp}; |
493 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp} @ @{thms ho_all_prs ho_ex_prs}); |
608 val ind_r_t = repabs_eq2 @{context} (g, t, ot); |
494 val ind_r_t = repabs_eq2 @{context} (g, t, ot); |
609 val ind_r_l = simp_lam_prs @{context} ind_r_t; |
495 val ind_r_l = simp_lam_prs @{context} ind_r_t; |
610 val ind_r_a = simp_allex_prs @{context} ind_r_l; |
496 val ind_r_a = simp_allex_prs @{context} ind_r_l; |
611 val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a; |
497 val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a; |
612 val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d |
498 val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d |
613 in |
499 in |
614 ObjectLogic.rulify ind_r_s |
500 ObjectLogic.rulify ind_r_s |
615 end |
501 end |
616 *} |
502 *} |
|
503 ML fset_defs |
|
504 |
617 |
505 |
618 ML {* lift @{thm m2} *} |
506 ML {* lift @{thm m2} *} |
619 ML {* lift @{thm m1} *} |
507 ML {* lift @{thm m1} *} |
620 ML {* lift @{thm list_eq.intros(4)} *} |
508 ML {* lift @{thm list_eq.intros(4)} *} |
621 ML {* lift @{thm list_eq.intros(5)} *} |
509 ML {* lift @{thm list_eq.intros(5)} *} |