equal
deleted
inserted
replaced
1045 thm all_prs ex_prs |
1045 thm all_prs ex_prs |
1046 (* 3. simplification with *) |
1046 (* 3. simplification with *) |
1047 thm fun_map.simps Quotient_abs_rep Quotient_rel_rep id_simps |
1047 thm fun_map.simps Quotient_abs_rep Quotient_rel_rep id_simps |
1048 (* 4. Test for refl *) |
1048 (* 4. Test for refl *) |
1049 |
1049 |
|
1050 thm fun_map.simps |
|
1051 |
|
1052 ML {* Conv.abs_conv; term_of *} |
|
1053 |
|
1054 thm fun_map.simps[THEN eq_reflection] |
|
1055 |
|
1056 ML {* |
|
1057 fun fun_map_conv xs ctxt ctrm = |
|
1058 case (term_of ctrm) of |
|
1059 ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => |
|
1060 (Conv.binop_conv (fun_map_conv xs ctxt) then_conv |
|
1061 (if (member (op=) xs h) |
|
1062 then Conv.all_conv |
|
1063 else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]})) ctrm |
|
1064 | _ $ _ => Conv.comb_conv (fun_map_conv xs ctxt) ctrm |
|
1065 | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm |
|
1066 | _ => Conv.all_conv ctrm |
|
1067 *} |
|
1068 |
|
1069 ML {* |
|
1070 fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt) |
|
1071 *} |
|
1072 |
1050 ML {* |
1073 ML {* |
1051 fun clean_tac lthy = |
1074 fun clean_tac lthy = |
1052 let |
1075 let |
1053 val thy = ProofContext.theory_of lthy; |
1076 val thy = ProofContext.theory_of lthy; |
1054 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
1077 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
1057 val thms2 = @{thms fun_map.simps Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs} |
1080 val thms2 = @{thms fun_map.simps Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs} |
1058 @ (id_simps_get lthy) |
1081 @ (id_simps_get lthy) |
1059 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
1082 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
1060 in |
1083 in |
1061 EVERY' [simp_tac (simps thms1), |
1084 EVERY' [simp_tac (simps thms1), |
|
1085 fun_map_tac lthy, |
1062 lambda_prs_tac lthy, |
1086 lambda_prs_tac lthy, |
1063 simp_tac (simps thms2), |
1087 simp_tac (simps thms2), |
1064 lambda_prs_tac lthy, |
|
1065 TRY o rtac refl] |
1088 TRY o rtac refl] |
1066 end |
1089 end |
1067 *} |
1090 *} |
1068 |
1091 |
1069 section {* Tactic for genralisation of free variables in a goal *} |
1092 section {* Tactic for genralisation of free variables in a goal *} |