1081 t1 $ t2 => mk_abs i t1 $ mk_abs i t2 |
1081 t1 $ t2 => mk_abs i t1 $ mk_abs i t2 |
1082 | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t') |
1082 | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t') |
1083 | Bound j => if i = j then error "make_inst" else t |
1083 | Bound j => if i = j then error "make_inst" else t |
1084 | _ => t); |
1084 | _ => t); |
1085 in (f, Abs ("x", T, mk_abs 0 g)) end; |
1085 in (f, Abs ("x", T, mk_abs 0 g)) end; |
1086 |
1086 *} |
1087 fun lambda_prs_conv1 ctxt quot_thms ctrm = |
1087 |
|
1088 ML {* |
|
1089 fun lambda_prs_simple_conv quot_thms ctxt ctrm = |
1088 case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) => |
1090 case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) => |
1089 let |
1091 let |
1090 val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1); |
1092 val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1); |
1091 val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2); |
1093 val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2); |
1092 val thy = ProofContext.theory_of ctxt; |
1094 val thy = ProofContext.theory_of ctxt; |
1106 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts; |
1108 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts; |
1107 (* val _ = writeln (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*) |
1109 (* val _ = writeln (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*) |
1108 in |
1110 in |
1109 Conv.rewr_conv ti ctrm |
1111 Conv.rewr_conv ti ctrm |
1110 end |
1112 end |
|
1113 | _ => Conv.all_conv ctrm |
1111 *} |
1114 *} |
1112 |
1115 |
1113 (* quot stands for the QUOTIENT theorems: *) |
1116 (* quot stands for the QUOTIENT theorems: *) |
1114 (* could be potentially all of them *) |
1117 (* could be potentially all of them *) |
1115 ML {* |
1118 ML {* |
1116 fun lambda_prs_conv ctxt quot ctrm = |
1119 fun lambda_prs_conv quot = |
1117 case (term_of ctrm) of |
1120 More_Conv.top_conv (lambda_prs_simple_conv quot) |
1118 (Const (@{const_name "fun_map"}, _) $ _ $ _) $ (Abs _) => |
1121 *} |
1119 (Conv.arg_conv (Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt) |
1122 |
1120 then_conv (lambda_prs_conv1 ctxt quot)) ctrm |
1123 ML {* |
1121 | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm |
1124 fun lambda_prs_tac quot ctxt = CONVERSION |
1122 | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm |
|
1123 | _ => Conv.all_conv ctrm |
|
1124 *} |
|
1125 |
|
1126 ML {* |
|
1127 fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) => |
|
1128 CONVERSION |
|
1129 (Conv.params_conv ~1 (fn ctxt => |
1125 (Conv.params_conv ~1 (fn ctxt => |
1130 (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv |
1126 (Conv.prems_conv ~1 (lambda_prs_conv quot ctxt) then_conv |
1131 Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) |
1127 Conv.concl_conv ~1 (lambda_prs_conv quot ctxt))) ctxt) |
1132 *} |
1128 *} |
1133 |
1129 |
1134 (* |
1130 (* |
1135 Cleaning the theorem consists of 6 kinds of rewrites. |
1131 Cleaning the theorem consists of 6 kinds of rewrites. |
1136 The first two need to be done before fun_map is unfolded |
1132 The first two need to be done before fun_map is unfolded |
1168 val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot |
1164 val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot |
1169 val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same |
1165 val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same |
1170 val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps |
1166 val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps |
1171 (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs) |
1167 (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs) |
1172 in |
1168 in |
1173 EVERY' [TRY o lambda_prs_tac lthy quot, |
1169 EVERY' [ |
1174 TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot), |
1170 |
1175 TRY o simp_tac simp_ctxt, |
1171 (* (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f *) |
1176 TRY o rtac refl] |
1172 DT lthy "a" (TRY o lambda_prs_tac quot lthy), |
|
1173 |
|
1174 (* \<forall>x\<in>Respects R. (abs ---> id) f ----> \<forall>x. f *) |
|
1175 DT lthy "b" (TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot)), |
|
1176 |
|
1177 (* NewConst ----> (rep ---> abs) oldConst *) |
|
1178 (* Abs (Rep x) ----> x *) |
|
1179 (* id_simps; fun_map.simps *) |
|
1180 DT lthy "c" (TRY o simp_tac simp_ctxt), |
|
1181 |
|
1182 (* final step *) |
|
1183 DT lthy "d" (TRY o rtac refl) |
|
1184 ] |
1177 end |
1185 end |
1178 *} |
1186 *} |
1179 |
1187 |
1180 section {* Genralisation of free variables in a goal *} |
1188 section {* Genralisation of free variables in a goal *} |
1181 |
1189 |