920 fun all_inj_repabs_tac ctxt = |
920 fun all_inj_repabs_tac ctxt = |
921 REPEAT_ALL_NEW (inj_repabs_tac ctxt) |
921 REPEAT_ALL_NEW (inj_repabs_tac ctxt) |
922 *} |
922 *} |
923 |
923 |
924 section {* Cleaning of the Theorem *} |
924 section {* Cleaning of the Theorem *} |
|
925 |
|
926 ML {* |
|
927 fun fun_map_simple_conv xs ctxt ctrm = |
|
928 case (term_of ctrm) of |
|
929 ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => |
|
930 if (member (op=) xs h) |
|
931 then Conv.all_conv ctrm |
|
932 else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]} ctrm |
|
933 | _ => Conv.all_conv ctrm |
|
934 |
|
935 fun fun_map_conv xs ctxt ctrm = |
|
936 case (term_of ctrm) of |
|
937 _ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv |
|
938 fun_map_simple_conv xs ctxt) ctrm |
|
939 | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm |
|
940 | _ => Conv.all_conv ctrm |
|
941 |
|
942 fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt) |
|
943 *} |
925 |
944 |
926 (* Since the patterns for the lhs are different; there are 3 different make-insts *) |
945 (* Since the patterns for the lhs are different; there are 3 different make-insts *) |
927 (* 1: does ? \<rightarrow> id *) |
946 (* 1: does ? \<rightarrow> id *) |
928 (* 2: does id \<rightarrow> ? *) |
947 (* 2: does id \<rightarrow> ? *) |
929 (* 3: does ? \<rightarrow> ? *) |
948 (* 3: does ? \<rightarrow> ? *) |
1025 More_Conv.top_conv lambda_prs_simple_conv |
1044 More_Conv.top_conv lambda_prs_simple_conv |
1026 |
1045 |
1027 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) |
1046 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) |
1028 *} |
1047 *} |
1029 |
1048 |
1030 (* 1. conversion (is not a pattern) *) |
1049 (* 1. folding of definitions and preservation lemmas; *) |
1031 thm lambda_prs |
1050 (* and simplification with *) |
1032 (* 2. folding of definitions: (rep ---> abs) oldConst == newconst *) |
1051 thm babs_prs all_prs ex_prs |
1033 (* prservation lemma *) |
1052 (* 2. unfolding of ---> in front of everything, except *) |
1034 (* and simplification with *) |
1053 (* bound variables *) |
1035 thm all_prs ex_prs |
1054 thm fun_map_simps |
1036 (* 3. simplification with *) |
1055 (* 3. simplification with *) |
1037 thm fun_map.simps Quotient_abs_rep Quotient_rel_rep id_simps |
1056 thm Quotient_abs_rep Quotient_rel_rep id_simps |
1038 (* 4. Test for refl *) |
1057 (* 4. Test for refl *) |
1039 |
|
1040 ML {* |
|
1041 fun fun_map_simple_conv xs ctxt ctrm = |
|
1042 case (term_of ctrm) of |
|
1043 ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => |
|
1044 if (member (op=) xs h) |
|
1045 then Conv.all_conv ctrm |
|
1046 else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]} ctrm |
|
1047 | _ => Conv.all_conv ctrm |
|
1048 |
|
1049 fun fun_map_conv xs ctxt ctrm = |
|
1050 case (term_of ctrm) of |
|
1051 _ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv |
|
1052 fun_map_simple_conv xs ctxt) ctrm |
|
1053 | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm |
|
1054 | _ => Conv.all_conv ctrm |
|
1055 |
|
1056 fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt) |
|
1057 *} |
|
1058 |
|
1059 |
|
1060 |
1058 |
1061 ML {* |
1059 ML {* |
1062 fun clean_tac lthy = |
1060 fun clean_tac lthy = |
1063 let |
1061 let |
1064 val thy = ProofContext.theory_of lthy; |
1062 val thy = ProofContext.theory_of lthy; |