equal
deleted
inserted
replaced
706 end |
706 end |
707 *} |
707 *} |
708 |
708 |
709 section {* RepAbs Injection Tactic *} |
709 section {* RepAbs Injection Tactic *} |
710 |
710 |
711 (* TODO: check if it still works with first_order_match *) |
|
712 (* FIXME/TODO: do not handle everything *) |
711 (* FIXME/TODO: do not handle everything *) |
713 ML {* |
712 ML {* |
714 fun instantiate_tac thm = |
713 fun instantiate_tac thm = |
715 Subgoal.FOCUS (fn {concl, ...} => |
714 Subgoal.FOCUS (fn {concl, ...} => |
716 let |
715 let |
1022 *} |
1021 *} |
1023 |
1022 |
1024 ML {* |
1023 ML {* |
1025 fun all_inj_repabs_tac ctxt rel_refl trans2 = |
1024 fun all_inj_repabs_tac ctxt rel_refl trans2 = |
1026 REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2) |
1025 REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2) |
|
1026 *} |
|
1027 |
|
1028 ML {* |
|
1029 fun dest_fun_type (Type("fun", [T, S])) = (T, S) |
|
1030 | dest_fun_type _ = error "dest_fun_type" |
|
1031 *} |
|
1032 |
|
1033 ML {* |
|
1034 val rep_abs_rsp_tac = |
|
1035 Subgoal.FOCUS (fn {concl, context, ...} => |
|
1036 case HOLogic.dest_Trueprop (term_of concl) of (rel $ lhs $ (rep $ (abs $ rhs))) => |
|
1037 (let |
|
1038 val thy = ProofContext.theory_of context; |
|
1039 val (ty_a, ty_b) = dest_fun_type (fastype_of abs); |
|
1040 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; |
|
1041 val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; |
|
1042 val thm = Drule.instantiate' ty_inst t_inst @{thm REP_ABS_RSP} |
|
1043 val te = solve_quotient_assums context thm |
|
1044 val t_inst = map (SOME o (cterm_of thy)) [lhs, rhs]; |
|
1045 val thm = Drule.instantiate' [] t_inst te |
|
1046 in |
|
1047 compose_tac (false, thm, 1) 1 |
|
1048 end |
|
1049 handle _ => no_tac) |
|
1050 | _ => no_tac) |
1027 *} |
1051 *} |
1028 |
1052 |
1029 (* A faster version *) |
1053 (* A faster version *) |
1030 |
1054 |
1031 ML {* |
1055 ML {* |
1052 | Const (@{const_name "op ="},_) $ _ $ _ => |
1076 | Const (@{const_name "op ="},_) $ _ $ _ => |
1053 rtac @{thm refl} ORELSE' |
1077 rtac @{thm refl} ORELSE' |
1054 (resolve_tac trans2 THEN' RANGE [ |
1078 (resolve_tac trans2 THEN' RANGE [ |
1055 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]) |
1079 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]) |
1056 | _ $ _ $ _ => |
1080 | _ $ _ $ _ => |
1057 instantiate_tac @{thm REP_ABS_RSP} ctxt THEN' RANGE [SOLVES' (quotient_tac ctxt)] |
1081 rep_abs_rsp_tac ctxt |
|
1082 | _ => error "inj_repabs_tac not a relation" |
1058 ) i) |
1083 ) i) |
1059 *} |
1084 *} |
1060 |
1085 |
1061 ML {* |
1086 ML {* |
1062 fun inj_repabs_tac' ctxt rel_refl trans2 = |
1087 fun inj_repabs_tac' ctxt rel_refl trans2 = |
1104 | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t') |
1129 | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t') |
1105 | Bound j => if i = j then error "make_inst" else t |
1130 | Bound j => if i = j then error "make_inst" else t |
1106 | _ => t); |
1131 | _ => t); |
1107 in (f, Abs ("x", T, mk_abs 0 g)) end; |
1132 in (f, Abs ("x", T, mk_abs 0 g)) end; |
1108 *} |
1133 *} |
1109 |
|
1110 ML {* |
|
1111 fun dest_fun_type (Type("fun", [T, S])) = (T, S) |
|
1112 | dest_fun_type _ = error "dest_fun_type" |
|
1113 *} |
|
1114 |
|
1115 |
1134 |
1116 ML {* |
1135 ML {* |
1117 fun lambda_allex_prs_simple_conv ctxt ctrm = |
1136 fun lambda_allex_prs_simple_conv ctxt ctrm = |
1118 case (term_of ctrm) of |
1137 case (term_of ctrm) of |
1119 ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) => |
1138 ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) => |