736 then result |
736 then result |
737 else mk_repabs lthy (rty, qty) result |
737 else mk_repabs lthy (rty, qty) result |
738 end |
738 end |
739 | _ => |
739 | _ => |
740 (**************************************************) |
740 (**************************************************) |
741 (* new |
741 (* new *) |
742 let |
742 let |
743 val (rhead, rargs) = strip_comb rtrm |
743 val (rhead, rargs) = strip_comb rtrm |
744 val (qhead, qargs) = strip_comb qtrm |
744 val (qhead, qargs) = strip_comb qtrm |
745 val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs) |
745 val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs) |
746 in |
746 in |
763 else list_comb (mk_repabs lthy (T, T') rhead, rargs') |
763 else list_comb (mk_repabs lthy (T, T') rhead, rargs') |
764 | (Abs _, Abs _, _ ) => |
764 | (Abs _, Abs _, _ ) => |
765 list_comb (inj_repabs_trm lthy (rhead, qhead), rargs') |
765 list_comb (inj_repabs_trm lthy (rhead, qhead), rargs') |
766 | _ => raise (LIFT_MATCH "injection") |
766 | _ => raise (LIFT_MATCH "injection") |
767 end |
767 end |
768 *) |
768 (**) |
769 |
769 |
770 (*************************************************) |
770 (*************************************************) |
771 (* old *) |
771 (* old |
772 let |
772 let |
773 val (rhead, rargs) = strip_comb rtrm |
773 val (rhead, rargs) = strip_comb rtrm |
774 val (qhead, qargs) = strip_comb qtrm |
774 val (qhead, qargs) = strip_comb qtrm |
775 val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs) |
775 val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs) |
776 in |
776 in |
790 mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs')) |
790 mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs')) |
791 | (Abs _, Abs _, _ ) => |
791 | (Abs _, Abs _, _ ) => |
792 mk_repabs lthy (rty, qty) (list_comb (inj_repabs_trm lthy (rhead, qhead), rargs')) |
792 mk_repabs lthy (rty, qty) (list_comb (inj_repabs_trm lthy (rhead, qhead), rargs')) |
793 | _ => raise (LIFT_MATCH "injection") |
793 | _ => raise (LIFT_MATCH "injection") |
794 end |
794 end |
795 (**) |
795 *) |
796 end |
796 end |
797 *} |
797 *} |
798 |
798 |
799 section {* RepAbs Injection Tactic *} |
799 section {* RepAbs Injection Tactic *} |
800 |
800 |
1101 (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv |
1102 (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv |
1102 Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) |
1103 Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) |
1103 *} |
1104 *} |
1104 |
1105 |
1105 (* |
1106 (* |
|
1107 TODO: Update |
1106 Cleaning the theorem consists of 5 kinds of rewrites. |
1108 Cleaning the theorem consists of 5 kinds of rewrites. |
1107 These rewrites can be done independently and in any order. |
1109 These rewrites can be done independently and in any order. |
1108 |
1110 |
1109 - LAMBDA_PRS: |
1111 - LAMBDA_PRS: |
1110 (Rep1 ---> Abs2) (\<lambda>x. Rep2 (?f (Abs1 x))) \<equiv> ?f |
1112 (Rep1 ---> Abs2) (\<lambda>x. Rep2 (?f (Abs1 x))) \<equiv> ?f |
1122 The last two are EqSubst (slow). |
1124 The last two are EqSubst (slow). |
1123 *) |
1125 *) |
1124 ML {* |
1126 ML {* |
1125 fun clean_tac lthy quot defs aps = |
1127 fun clean_tac lthy quot defs aps = |
1126 let |
1128 let |
1127 val lower = flat (map (add_lower_defs lthy) defs) |
|
1128 val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower |
|
1129 val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot |
1129 val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot |
|
1130 val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep; |
1130 val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot |
1131 val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot |
1131 val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same |
1132 val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same |
1132 val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps (meta_reps_same @ meta_lower) |
1133 val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps |
1133 val aps_thms = map (applic_prs lthy absrep) aps |
1134 (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs) |
1134 in |
1135 in |
1135 EVERY' [lambda_prs_tac lthy quot, |
1136 EVERY' [lambda_prs_tac lthy quot, |
|
1137 TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot), |
1136 TRY o simp_tac simp_ctxt, |
1138 TRY o simp_tac simp_ctxt, |
1137 TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot), |
|
1138 TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms), |
|
1139 TRY o rtac refl] |
1139 TRY o rtac refl] |
1140 end |
1140 end |
1141 *} |
1141 *} |
1142 |
1142 |
1143 section {* Genralisation of free variables in a goal *} |
1143 section {* Genralisation of free variables in a goal *} |