735 if rty = qty |
735 if rty = qty |
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 (**************************************************) |
|
741 (* new *) |
|
742 let |
740 let |
743 val (rhead, rargs) = strip_comb rtrm |
741 val (rhead, rargs) = strip_comb rtrm |
744 val (qhead, qargs) = strip_comb qtrm |
742 val (qhead, qargs) = strip_comb qtrm |
745 val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs) |
743 val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs) |
746 in |
744 in |
747 case (rhead, qhead, length rargs') of |
745 case (rhead, qhead) of |
748 (Const (_, T), Const (_, T'), 0) => |
746 (Const _, Const _) => |
749 if T = T' |
|
750 then rhead |
|
751 else mk_repabs lthy (T, T') rhead |
|
752 | (Free (_, T), Free (_, T'), 0) => |
|
753 if T = T' |
|
754 then rhead |
|
755 else mk_repabs lthy (T, T') rhead |
|
756 | (Const (_, T), Const (_, T'), _) => (* FIXME/TODO: check this case exactly*) |
|
757 if rty = qty |
747 if rty = qty |
758 then list_comb (rhead, rargs') |
748 then list_comb (rhead, rargs') |
759 else mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) |
749 else mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) |
760 | (Free (x, T), Free (x', T'), _) => |
750 | (Free (x, T), Free (x', T')) => |
761 if T = T' |
751 if T = T' |
762 then list_comb (rhead, rargs') |
752 then list_comb (rhead, rargs') |
763 else list_comb (mk_repabs lthy (T, T') rhead, rargs') |
753 else list_comb (mk_repabs lthy (T, T') rhead, rargs') |
764 | (Abs _, Abs _, _ ) => |
754 | (Abs _, Abs _) => |
765 list_comb (inj_repabs_trm lthy (rhead, qhead), rargs') |
755 list_comb (inj_repabs_trm lthy (rhead, qhead), rargs') |
766 | _ => raise (LIFT_MATCH "injection") |
756 | _ => raise (LIFT_MATCH "injection") |
767 end |
757 end |
768 (**) |
|
769 |
|
770 (*************************************************) |
|
771 (* old |
|
772 let |
|
773 val (rhead, rargs) = strip_comb rtrm |
|
774 val (qhead, qargs) = strip_comb qtrm |
|
775 val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs) |
|
776 in |
|
777 if rty = qty |
|
778 then |
|
779 case (rhead, qhead) of |
|
780 (Free (_, T), Free (_, T')) => |
|
781 if T = T' then list_comb (rhead, rargs') |
|
782 else list_comb (mk_repabs lthy (T, T') rhead, rargs') |
|
783 | _ => list_comb (rhead, rargs') |
|
784 else |
|
785 case (rhead, qhead, length rargs') of |
|
786 (Const _, Const _, 0) => mk_repabs lthy (rty, qty) rhead |
|
787 | (Free (_, T), Free (_, T'), 0) => mk_repabs lthy (T, T') rhead |
|
788 | (Const _, Const _, _) => mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) |
|
789 | (Free (x, T), Free (x', T'), _) => |
|
790 mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs')) |
|
791 | (Abs _, Abs _, _ ) => |
|
792 mk_repabs lthy (rty, qty) (list_comb (inj_repabs_trm lthy (rhead, qhead), rargs')) |
|
793 | _ => raise (LIFT_MATCH "injection") |
|
794 end |
|
795 *) |
|
796 end |
758 end |
797 *} |
759 *} |
798 |
760 |
799 section {* RepAbs Injection Tactic *} |
761 section {* RepAbs Injection Tactic *} |
800 |
762 |
1107 TODO: Update |
1069 TODO: Update |
1108 Cleaning the theorem consists of 5 kinds of rewrites. |
1070 Cleaning the theorem consists of 5 kinds of rewrites. |
1109 These rewrites can be done independently and in any order. |
1071 These rewrites can be done independently and in any order. |
1110 |
1072 |
1111 - LAMBDA_PRS: |
1073 - LAMBDA_PRS: |
1112 (Rep1 ---> Abs2) (\<lambda>x. Rep2 (?f (Abs1 x))) \<equiv> ?f |
1074 (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f |
1113 - Rewriting with definitions from the argument defs |
1075 - Rewriting with definitions from the argument defs |
1114 (Abs) OldConst (Rep Args) \<equiv> NewConst Args |
1076 (Abs) OldConst (Rep Args) ----> NewConst Args |
1115 - QUOTIENT_REL_REP: |
1077 - QUOTIENT_REL_REP: |
1116 Rel (Rep x) (Rep y) \<equiv> x = y |
1078 Rel (Rep x) (Rep y) ----> x = y |
1117 - FORALL_PRS (and the same for exists: EXISTS_PRS) |
1079 - FORALL_PRS (and the same for exists: EXISTS_PRS) |
1118 \<forall>x\<in>Respects R. (abs ---> id) ?f \<equiv> \<forall>x. ?f |
1080 \<forall>x\<in>Respects R. (abs ---> id) f ----> \<forall>x. f |
1119 - applic_prs |
1081 - applic_prs |
1120 Abs1 ((Abs2 --> Rep1) f (Rep2 args)) \<equiv> f args |
1082 Abs1 ((Abs2 --> Rep1) f (Rep2 args)) ----> f args |
1121 |
1083 |
1122 The first one is implemented as a conversion (fast). |
1084 The first one is implemented as a conversion (fast). |
1123 The second and third one are a simp_tac (fast). |
1085 The second and third one are a simp_tac (fast). |
1124 The last two are EqSubst (slow). |
1086 The last two are EqSubst (slow). |
1125 *) |
1087 *) |