1064 with: f |
1064 with: f |
1065 |
1065 |
1066 It proves the QUOTIENT assumptions by calling quotient_tac |
1066 It proves the QUOTIENT assumptions by calling quotient_tac |
1067 *) |
1067 *) |
1068 ML {* |
1068 ML {* |
|
1069 fun make_inst lhs t = |
|
1070 let |
|
1071 val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; |
|
1072 val _ $ (Abs (_, _, g)) = t; |
|
1073 fun mk_abs i t = |
|
1074 if incr_boundvars i u aconv t then Bound i |
|
1075 else (case t of |
|
1076 t1 $ t2 => mk_abs i t1 $ mk_abs i t2 |
|
1077 | Abs (s, T, t') => Abs (s, T, mk_abs (i+1) t') |
|
1078 | Bound j => if i = j then error "make_inst" else t |
|
1079 | _ => t); |
|
1080 in (f, Abs ("x", T, mk_abs 0 g)) end; |
|
1081 |
1069 fun lambda_prs_conv1 ctxt quot_thms ctrm = |
1082 fun lambda_prs_conv1 ctxt quot_thms ctrm = |
1070 case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) => |
1083 case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) => |
1071 let |
1084 let |
1072 val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1); |
1085 val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1); |
1073 val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2); |
1086 val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2); |
1081 (quotient_tac quot_thms); |
1094 (quotient_tac quot_thms); |
1082 val gc = Drule.strip_imp_concl (cprop_of lpi); |
1095 val gc = Drule.strip_imp_concl (cprop_of lpi); |
1083 val t = Goal.prove_internal [] gc (fn _ => tac 1) |
1096 val t = Goal.prove_internal [] gc (fn _ => tac 1) |
1084 val te = @{thm eq_reflection} OF [t] |
1097 val te = @{thm eq_reflection} OF [t] |
1085 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
1098 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
1086 val tl = Thm.lhs_of ts |
1099 val tl = Thm.lhs_of ts; |
1087 (* val _ = tracing (Syntax.string_of_term @{context} (term_of ctrm));*) |
1100 val (insp, inst) = make_inst (term_of tl) (term_of ctrm); |
1088 (* val _ = tracing (Syntax.string_of_term @{context} (term_of tl));*) |
1101 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts; |
1089 val insts = matching_prs (ProofContext.theory_of ctxt) (term_of tl) (term_of ctrm); |
1102 (* val _ = writeln (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*) |
1090 val ti = Drule.eta_contraction_rule (Drule.instantiate insts ts); |
|
1091 (* val _ = tracing (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*) |
|
1092 in |
1103 in |
1093 Conv.rewr_conv ti ctrm |
1104 Conv.rewr_conv ti ctrm |
1094 end |
1105 end |
1095 (* TODO: We can add a proper error message... *) |
1106 *} |
1096 handle Bind => Conv.all_conv ctrm |
1107 |
1097 |
1108 (* quot stands for the QUOTIENT theorems: *) |
1098 *} |
|
1099 |
|
1100 (* quot stands for the QUOTIENT theorems: *) |
|
1101 (* could be potentially all of them *) |
1109 (* could be potentially all of them *) |
1102 ML {* |
1110 ML {* |
1103 fun lambda_prs_conv ctxt quot ctrm = |
1111 fun lambda_prs_conv ctxt quot ctrm = |
1104 case (term_of ctrm) of |
1112 case (term_of ctrm) of |
1105 (Const (@{const_name "fun_map"}, _) $ _ $ _) $ (Abs _) => |
1113 (Const (@{const_name "fun_map"}, _) $ _ $ _) $ (Abs _) => |
1120 |
1128 |
1121 ML {* |
1129 ML {* |
1122 fun clean_tac lthy quot defs aps = |
1130 fun clean_tac lthy quot defs aps = |
1123 let |
1131 let |
1124 val lower = flat (map (add_lower_defs lthy) defs) |
1132 val lower = flat (map (add_lower_defs lthy) defs) |
|
1133 val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower |
1125 val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot |
1134 val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot |
1126 val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot |
1135 val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot |
|
1136 val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same |
|
1137 val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps (meta_reps_same @ meta_lower) |
1127 val aps_thms = map (applic_prs lthy absrep) aps |
1138 val aps_thms = map (applic_prs lthy absrep) aps |
1128 in |
1139 in |
1129 EVERY' [TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot), |
1140 EVERY' [lambda_prs_tac lthy quot, |
1130 lambda_prs_tac lthy quot, |
1141 TRY o simp_tac simp_ctxt, |
|
1142 TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot), |
1131 TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms), |
1143 TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms), |
1132 TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower), |
1144 rtac refl] |
1133 simp_tac (HOL_ss addsimps reps_same)] |
|
1134 end |
1145 end |
1135 *} |
1146 *} |
1136 |
1147 |
1137 section {* Genralisation of free variables in a goal *} |
1148 section {* Genralisation of free variables in a goal *} |
1138 |
1149 |