equal
deleted
inserted
replaced
1016 in |
1016 in |
1017 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
1017 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
1018 end |
1018 end |
1019 *} |
1019 *} |
1020 |
1020 |
|
1021 (* Rewrites the term with LAMBDA_PRS thm. |
|
1022 |
|
1023 Replaces: (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) |
|
1024 with: f |
|
1025 |
|
1026 It proves the QUOTIENT assumptions by calling quotient_tac |
|
1027 *) |
1021 ML {* |
1028 ML {* |
1022 fun lambda_prs_conv1 ctxt quot_thms ctrm = |
1029 fun lambda_prs_conv1 ctxt quot_thms ctrm = |
1023 case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) => |
1030 case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) => |
1024 let |
1031 let |
1025 val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1); |
1032 val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1); |