821 *} |
821 *} |
822 |
822 |
823 section {* Cleaning of the Theorem *} |
823 section {* Cleaning of the Theorem *} |
824 |
824 |
825 ML {* |
825 ML {* |
|
826 (* expands all ---> except in front of bound variables *) |
826 fun fun_map_simple_conv xs ctxt ctrm = |
827 fun fun_map_simple_conv xs ctxt ctrm = |
827 case (term_of ctrm) of |
828 case (term_of ctrm) of |
828 ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => |
829 ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => |
829 if (member (op=) xs h) |
830 if (member (op=) xs h) |
830 then Conv.all_conv ctrm |
831 then Conv.all_conv ctrm |
842 *} |
843 *} |
843 |
844 |
844 (* Since the patterns for the lhs are different; there are 2 different make-insts *) |
845 (* Since the patterns for the lhs are different; there are 2 different make-insts *) |
845 (* 1: does ? \<rightarrow> id *) |
846 (* 1: does ? \<rightarrow> id *) |
846 (* 2: does ? \<rightarrow> non-id *) |
847 (* 2: does ? \<rightarrow> non-id *) |
847 ML {* |
848 ML {* |
|
849 fun mk_abs u i t = |
|
850 if incr_boundvars i u aconv t then Bound i |
|
851 else (case t of |
|
852 t1 $ t2 => (mk_abs u i t1) $ (mk_abs u i t2) |
|
853 | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t') |
|
854 | Bound j => if i = j then error "make_inst" else t |
|
855 | _ => t) |
|
856 |
848 fun make_inst lhs t = |
857 fun make_inst lhs t = |
849 let |
858 let |
850 val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; |
859 val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; |
851 val _ $ (Abs (_, _, g)) = t; |
860 val _ $ (Abs (_, _, g)) = t; |
852 fun mk_abs i t = |
861 in |
853 if incr_boundvars i u aconv t then Bound i |
862 (f, Abs ("x", T, mk_abs u 0 g)) |
854 else (case t of |
863 end |
855 t1 $ t2 => mk_abs i t1 $ mk_abs i t2 |
864 |
856 | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t') |
|
857 | Bound j => if i = j then error "make_inst" else t |
|
858 | _ => t); |
|
859 in (f, Abs ("x", T, mk_abs 0 g)) end; |
|
860 *} |
|
861 |
|
862 ML {* |
|
863 fun make_inst2 lhs t = |
865 fun make_inst2 lhs t = |
864 let |
866 let |
865 val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; |
867 val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; |
866 val _ $ (Abs (_, _, (_ $ g))) = t; |
868 val _ $ (Abs (_, _, (_ $ g))) = t; |
867 fun mk_abs i t = |
869 in |
868 if incr_boundvars i u aconv t then Bound i |
870 (f, Abs ("x", T, mk_abs u 0 g)) |
869 else (case t of |
871 end |
870 t1 $ t2 => mk_abs i t1 $ mk_abs i t2 |
|
871 | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t') |
|
872 | Bound j => if i = j then error "make_inst" else t |
|
873 | _ => t); |
|
874 in (f, Abs ("x", T, mk_abs 0 g)) end; |
|
875 *} |
872 *} |
876 |
873 |
877 ML {* |
874 ML {* |
878 fun lambda_prs_simple_conv ctxt ctrm = |
875 fun lambda_prs_simple_conv ctxt ctrm = |
879 case (term_of ctrm) of |
876 case (term_of ctrm) of |