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