965 *} |
965 *} |
966 |
966 |
967 (* A faster version *) |
967 (* A faster version *) |
968 |
968 |
969 ML {* |
969 ML {* |
970 fun inj_repabs_tac_fast ctxt quot_thms trans2 = SUBGOAL (fn (goal, i) => |
970 fun inj_repabs_tac_fast ctxt trans2 = SUBGOAL (fn (goal, i) => |
971 (case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of |
971 (case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of |
972 ((Const (@{const_name FUN_REL}, _) $ _ $ _) $ (Abs _) $ (Abs _)) |
972 ((Const (@{const_name FUN_REL}, _) $ _ $ _) $ (Abs _) $ (Abs _)) |
973 => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam |
973 => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam |
974 | (Const (@{const_name "op ="},_) $ |
974 | (Const (@{const_name "op ="},_) $ |
975 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
975 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
990 | Const (@{const_name "op ="},_) $ _ $ _ => |
990 | Const (@{const_name "op ="},_) $ _ $ _ => |
991 rtac @{thm refl} ORELSE' |
991 rtac @{thm refl} ORELSE' |
992 (resolve_tac trans2 THEN' RANGE [ |
992 (resolve_tac trans2 THEN' RANGE [ |
993 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]) |
993 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]) |
994 | _ $ _ $ _ => |
994 | _ $ _ $ _ => |
995 instantiate_tac @{thm REP_ABS_RSP} ctxt THEN' RANGE [SOLVES' (quotient_tac ctxt quot_thms)] |
995 instantiate_tac @{thm REP_ABS_RSP} ctxt THEN' RANGE [SOLVES' (quotient_tac ctxt)] |
996 ) i) |
996 ) i) |
997 *} |
997 *} |
998 |
998 |
999 ML {* |
999 ML {* |
1000 fun inj_repabs_tac' ctxt quot_thms rel_refl trans2 = |
1000 fun inj_repabs_tac' ctxt rel_refl trans2 = |
1001 (FIRST' [ |
1001 (FIRST' [ |
1002 inj_repabs_tac_fast ctxt quot_thms trans2, |
1002 inj_repabs_tac_fast ctxt trans2, |
1003 NDT ctxt "A" (APPLY_RSP_TAC ctxt THEN' |
1003 NDT ctxt "A" (APPLY_RSP_TAC ctxt THEN' |
1004 (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms), |
1004 (RANGE [SOLVES' (quotient_tac ctxt), SOLVES' (quotient_tac ctxt), |
1005 quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
1005 quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
1006 NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN' |
1006 NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN' |
1007 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
1007 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
1008 NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam), |
1008 NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam), |
1009 NDT ctxt "E" (atac), |
1009 NDT ctxt "E" (atac), |
1010 NDT ctxt "D" (resolve_tac rel_refl), |
1010 NDT ctxt "D" (resolve_tac rel_refl), |
1011 NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)), |
1011 NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)) |
1012 NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))]) |
1012 (* NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms FUN_REL_EQ LIST_REL_EQ})))*) |
1013 *} |
1013 ]) |
1014 |
1014 *} |
1015 ML {* |
1015 |
1016 fun all_inj_repabs_tac' ctxt quot_thms rel_refl trans2 = |
1016 ML {* |
1017 REPEAT_ALL_NEW (inj_repabs_tac' ctxt quot_thms rel_refl trans2) |
1017 fun all_inj_repabs_tac' ctxt rel_refl trans2 = |
|
1018 REPEAT_ALL_NEW (inj_repabs_tac' ctxt rel_refl trans2) |
1018 *} |
1019 *} |
1019 |
1020 |
1020 |
1021 |
1021 |
1022 |
1022 section {* Cleaning of the theorem *} |
1023 section {* Cleaning of the theorem *} |