1036 (* 3. simplification with *) |
1036 (* 3. simplification with *) |
1037 thm fun_map.simps Quotient_abs_rep Quotient_rel_rep id_simps |
1037 thm fun_map.simps Quotient_abs_rep Quotient_rel_rep id_simps |
1038 (* 4. Test for refl *) |
1038 (* 4. Test for refl *) |
1039 |
1039 |
1040 ML {* |
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 |
1041 fun fun_map_conv xs ctxt ctrm = |
1049 fun fun_map_conv xs ctxt ctrm = |
1042 case (term_of ctrm) of |
1050 case (term_of ctrm) of |
1043 ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => |
1051 _ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv |
1044 (Conv.binop_conv (fun_map_conv xs ctxt) then_conv |
1052 fun_map_simple_conv xs ctxt) ctrm |
1045 (if (member (op=) xs h) |
|
1046 then Conv.all_conv |
|
1047 else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]})) ctrm |
|
1048 | _ $ _ => Conv.comb_conv (fun_map_conv xs ctxt) ctrm |
|
1049 | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm |
1053 | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm |
1050 | _ => Conv.all_conv ctrm |
1054 | _ => Conv.all_conv ctrm |
1051 |
1055 |
1052 fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt) |
1056 fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt) |
1053 *} |
1057 *} |
|
1058 |
|
1059 |
1054 |
1060 |
1055 ML {* |
1061 ML {* |
1056 fun clean_tac lthy = |
1062 fun clean_tac lthy = |
1057 let |
1063 let |
1058 val thy = ProofContext.theory_of lthy; |
1064 val thy = ProofContext.theory_of lthy; |
1059 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
1065 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
1060 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
1066 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
|
1067 |
1061 val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs} |
1068 val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs} |
1062 val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy) |
1069 val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy) |
1063 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
1070 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
1064 in |
1071 in |
1065 EVERY' [simp_tac (simps thms1), |
1072 EVERY' [simp_tac (simps thms1), |
1066 TRY o REPEAT_ALL_NEW (CHANGED o (fun_map_tac lthy)), |
1073 fun_map_tac lthy, |
1067 lambda_prs_tac lthy, |
1074 lambda_prs_tac lthy, |
1068 simp_tac (simps thms2), |
1075 simp_tac (simps thms2), |
1069 TRY o rtac refl] |
1076 TRY o rtac refl] |
1070 end |
1077 end |
1071 *} |
1078 *} |