21 setsubgoaler asm_simp_tac |
21 setsubgoaler asm_simp_tac |
22 setmksimps (mksimps []) |
22 setmksimps (mksimps []) |
23 |
23 |
24 (* various helper fuctions *) |
24 (* various helper fuctions *) |
25 |
25 |
26 (* composition of two theorems, used in map *) |
26 (* composition of two theorems, used in maps *) |
27 fun OF1 thm1 thm2 = thm2 RS thm1 |
27 fun OF1 thm1 thm2 = thm2 RS thm1 |
28 |
28 |
29 (* makes sure a subgoal is solved *) |
29 (* makes sure a subgoal is solved *) |
30 fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac) |
30 fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac) |
31 |
31 |
32 (* prints warning, if goal is unsolved *) |
32 (* prints warning, if the subgoal is unsolved *) |
33 fun WARN (tac, msg) i st = |
33 fun WARN (tac, msg) i st = |
34 case Seq.pull ((SOLVES' tac) i st) of |
34 case Seq.pull ((SOLVES' tac) i st) of |
35 NONE => (warning msg; Seq.single st) |
35 NONE => (warning msg; Seq.single st) |
36 | seqcell => Seq.make (fn () => seqcell) |
36 | seqcell => Seq.make (fn () => seqcell) |
37 |
37 |
424 | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm |
424 | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm |
425 | _ => Conv.all_conv ctrm |
425 | _ => Conv.all_conv ctrm |
426 |
426 |
427 fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt) |
427 fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt) |
428 |
428 |
|
429 |
429 fun mk_abs u i t = |
430 fun mk_abs u i t = |
430 if incr_boundvars i u aconv t then Bound i |
431 if incr_boundvars i u aconv t then Bound i |
431 else (case t of |
432 else (case t of |
432 t1 $ t2 => (mk_abs u i t1) $ (mk_abs u i t2) |
433 t1 $ t2 => (mk_abs u i t1) $ (mk_abs u i t2) |
433 | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t') |
434 | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t') |
452 |
453 |
453 (* Simplifies a redex using the 'lambda_prs' theorem. *) |
454 (* Simplifies a redex using the 'lambda_prs' theorem. *) |
454 (* First instantiates the types and known subterms. *) |
455 (* First instantiates the types and known subterms. *) |
455 (* Then solves the quotient assumptions to get Rep2 and Abs1 *) |
456 (* Then solves the quotient assumptions to get Rep2 and Abs1 *) |
456 (* Finally instantiates the function f using make_inst *) |
457 (* Finally instantiates the function f using make_inst *) |
457 (* If Rep2 is identity then the pattern is simpler and *) |
458 (* If Rep2 is an identity then the pattern is simpler and *) |
458 (* make_inst_id is used *) |
459 (* make_inst_id is used *) |
459 fun lambda_prs_simple_conv ctxt ctrm = |
460 fun lambda_prs_simple_conv ctxt ctrm = |
460 case (term_of ctrm) of |
461 case (term_of ctrm) of |
461 (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) => |
462 (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) => |
462 (let |
463 (let |
466 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
467 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
467 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
468 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
468 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]} |
469 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]} |
469 val te = solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi) |
470 val te = solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi) |
470 val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te |
471 val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te |
471 val make_inst = if ty_c = ty_d then make_inst_id else make_inst |
472 val (insp, inst) = |
472 val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) |
473 if ty_c = ty_d |
|
474 then make_inst_id (term_of (Thm.lhs_of ts)) (term_of ctrm) |
|
475 else make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) |
473 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
476 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
474 in |
477 in |
475 Conv.rewr_conv ti ctrm |
478 Conv.rewr_conv ti ctrm |
476 end |
479 end |
477 handle _ => Conv.all_conv ctrm) |
480 handle _ => Conv.all_conv ctrm) |
498 (* thm Quotient_abs_rep Quotient_rel_rep id_simps *) |
501 (* thm Quotient_abs_rep Quotient_rel_rep id_simps *) |
499 (* *) |
502 (* *) |
500 (* 5. test for refl *) |
503 (* 5. test for refl *) |
501 |
504 |
502 fun clean_tac_aux lthy = |
505 fun clean_tac_aux lthy = |
503 let |
506 let |
504 val thy = ProofContext.theory_of lthy; |
507 val thy = ProofContext.theory_of lthy; |
505 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
508 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
506 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
509 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
507 |
510 |
508 val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs} |
511 val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs} |
509 val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy) |
512 val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy) |
510 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
513 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
511 in |
514 in |
512 EVERY' [simp_tac (simps thms1), |
515 EVERY' [simp_tac (simps thms1), |
513 fun_map_tac lthy, |
516 fun_map_tac lthy, |
514 lambda_prs_tac lthy, |
517 lambda_prs_tac lthy, |
515 simp_tac (simps thms2), |
518 simp_tac (simps thms2), |
516 TRY o rtac refl] |
519 TRY o rtac refl] |
517 end |
520 end |
518 |
521 |
519 fun clean_tac lthy = REPEAT o CHANGED o (clean_tac_aux lthy) (* HACK?? *) |
522 fun clean_tac lthy = REPEAT o CHANGED o (clean_tac_aux lthy) (* HACK?? *) |
520 |
523 |
521 |
524 |
522 (********************************************************) |
525 (****************************************************) |
523 (* Tactic for Genralisation of Free Variables in a Goal *) |
526 (* Tactic for Generalising Free Variables in a Goal *) |
524 (********************************************************) |
527 (****************************************************) |
525 |
528 |
526 fun inst_spec ctrm = |
529 fun inst_spec ctrm = |
527 Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} |
530 Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} |
528 |
531 |
529 fun inst_spec_tac ctrms = |
532 fun inst_spec_tac ctrms = |
601 |
604 |
602 (* the tactic leaves three subgoals to be proved *) |
605 (* the tactic leaves three subgoals to be proved *) |
603 fun procedure_tac ctxt rthm = |
606 fun procedure_tac ctxt rthm = |
604 ObjectLogic.full_atomize_tac |
607 ObjectLogic.full_atomize_tac |
605 THEN' gen_frees_tac ctxt |
608 THEN' gen_frees_tac ctxt |
606 THEN' CSUBGOAL (fn (goal, i) => |
609 THEN' SUBGOAL (fn (goal, i) => |
607 let |
610 let |
608 val rthm' = atomize_thm rthm |
611 val rthm' = atomize_thm rthm |
609 val rule = procedure_inst ctxt (prop_of rthm') (term_of goal) |
612 val rule = procedure_inst ctxt (prop_of rthm') goal |
610 in |
613 in |
611 (rtac rule THEN' rtac rthm') i |
614 (rtac rule THEN' rtac rthm') i |
612 end) |
615 end) |
613 |
616 |
614 |
617 |