1049 | Bound j => if i = j then error "make_inst" else t |
1049 | Bound j => if i = j then error "make_inst" else t |
1050 | _ => t); |
1050 | _ => t); |
1051 in (f, Abs ("x", T, mk_abs 0 g)) end; |
1051 in (f, Abs ("x", T, mk_abs 0 g)) end; |
1052 *} |
1052 *} |
1053 |
1053 |
1054 thm lambda_prs |
|
1055 |
|
1056 ML {* |
1054 ML {* |
1057 fun lambda_prs_simple_conv ctxt ctrm = |
1055 fun lambda_prs_simple_conv ctxt ctrm = |
1058 case (term_of ctrm) of |
1056 case (term_of ctrm) of |
1059 ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) => |
1057 ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) => |
1060 let |
1058 let |
1061 val (ty_b, ty_a) = dest_fun_type (fastype_of r1); |
1059 val thy = ProofContext.theory_of ctxt |
1062 val (ty_c, ty_d) = dest_fun_type (fastype_of a2); |
1060 val (ty_b, ty_a) = dest_fun_type (fastype_of r1) |
1063 val thy = ProofContext.theory_of ctxt; |
1061 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
1064 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
1062 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
1065 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
1063 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
1066 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs}; |
1064 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs} |
1067 val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)] |
1065 val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)] |
1068 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
1066 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
1069 val tl = Thm.lhs_of ts; |
1067 val tl = Thm.lhs_of ts |
1070 val (insp, inst) = make_inst (term_of tl) (term_of ctrm); |
1068 val (insp, inst) = make_inst (term_of tl) (term_of ctrm) |
1071 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts; |
1069 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
1072 in |
1070 (*val _ = tracing "lambda_prs" |
1073 Conv.rewr_conv ti ctrm |
1071 val _ = tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm))) |
1074 end |
1072 val _ = tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti)))*) |
|
1073 in |
|
1074 Conv.rewr_conv ti ctrm |
|
1075 end |
1075 | _ => Conv.all_conv ctrm |
1076 | _ => Conv.all_conv ctrm |
1076 *} |
1077 *} |
1077 |
1078 |
1078 ML {* |
1079 ML {* |
1079 val lambda_prs_conv = |
1080 val lambda_prs_conv = |
1081 |
1082 |
1082 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) |
1083 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) |
1083 *} |
1084 *} |
1084 |
1085 |
1085 (* |
1086 (* |
1086 Cleaning the theorem consists of 6 kinds of rewrites. |
1087 Cleaning the theorem consists of three rewriting steps. |
1087 The first two need to be done before fun_map is unfolded |
1088 The first two need to be done before fun_map is unfolded |
1088 |
1089 |
1089 - lambda_prs: |
1090 1) lambda_prs: |
1090 (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f |
1091 (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f |
1091 |
1092 |
1092 - all_prs (and the same for exists: ex_prs) |
1093 Implemented as conversion since it is not a pattern. |
1093 \<forall>x\<in>Respects R. (abs ---> id) f ----> \<forall>x. f |
1094 |
1094 |
1095 2) all_prs (the same for exists): |
1095 - Rewriting with definitions from the argument defs |
1096 Ball (Respects R) ((abs ---> id) f) ----> All f |
1096 NewConst ----> (rep ---> abs) oldConst |
1097 |
1097 |
1098 Rewriting with definitions from the argument defs |
1098 - Quotient_rel_rep: |
1099 (rep ---> abs) oldConst ----> newconst |
1099 Rel (Rep x) (Rep y) ----> x = y |
1100 |
1100 |
1101 3) Quotient_rel_rep: |
1101 - ABS_REP |
1102 Rel (Rep x) (Rep y) ----> x = y |
1102 Abs (Rep x) ----> x |
1103 |
1103 |
1104 Quotient_abs_rep: |
1104 - id_simps; fun_map.simps |
1105 Abs (Rep x) ----> x |
1105 |
1106 |
1106 The first one is implemented as a conversion (fast). |
1107 id_simps; fun_map.simps |
1107 The second one is an EqSubst (slow). |
|
1108 The rest are a simp_tac and are fast. |
|
1109 *) |
1108 *) |
1110 |
1109 |
1111 ML {* |
1110 ML {* |
1112 fun clean_tac lthy = |
1111 fun clean_tac lthy = |
1113 let |
1112 let |
1114 val thy = ProofContext.theory_of lthy; |
1113 val thy = ProofContext.theory_of lthy; |
1115 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
1114 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
|
1115 (* FIXME: shouldn't the definitions already be varified? *) |
1116 val thms1 = @{thms all_prs ex_prs} @ defs |
1116 val thms1 = @{thms all_prs ex_prs} @ defs |
1117 val thms2 = @{thms eq_reflection[OF fun_map.simps]} |
1117 val thms2 = @{thms eq_reflection[OF fun_map.simps]} |
1118 @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} |
1118 @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} |
1119 fun simp_ctxt thms = HOL_basic_ss addsimps thms addSolver quotient_solver |
1119 fun simps thms = HOL_basic_ss addsimps thms addSolver quotient_solver |
1120 (* FIXME: use of someting smaller than HOL_basic_ss *) |
1120 (* FIXME: use of someting smaller than HOL_basic_ss *) |
1121 in |
1121 in |
1122 EVERY' [ |
1122 EVERY' [lambda_prs_tac lthy, |
1123 (* (rep1 ---> abs2) (\<lambda>x. rep2 (f (abs1 x))) ----> f *) |
1123 simp_tac (simps thms1), |
1124 NDT lthy "a" (TRY o lambda_allex_prs_tac lthy), |
1124 simp_tac (simps thms2), |
1125 |
1125 TRY o rtac refl] |
1126 (* Ball (Respects R) ((abs ---> id) f) ----> All f *) |
|
1127 NDT lthy "b" (simp_tac (simp_ctxt thms1)), |
|
1128 |
|
1129 (* NewConst -----> (rep ---> abs) oldConst *) |
|
1130 (* abs (rep x) -----> x *) |
|
1131 (* R (Rep x) (Rep y) -----> x = y *) |
|
1132 (* id_simps; fun_map.simps *) |
|
1133 NDT lthy "c" (simp_tac (simp_ctxt thms2)), |
|
1134 |
|
1135 (* final step *) |
|
1136 NDT lthy "d" (TRY o rtac refl) |
|
1137 ] |
|
1138 end |
1126 end |
1139 *} |
1127 *} |
1140 |
1128 |
1141 section {* Genralisation of free variables in a goal *} |
1129 section {* Genralisation of free variables in a goal *} |
1142 |
1130 |