45 fun mk_meta_prems ctxt = |
45 fun mk_meta_prems ctxt = |
46 rule_by_tactic ctxt |
46 rule_by_tactic ctxt |
47 (REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}])); |
47 (REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}])); |
48 |
48 |
49 (*Congruence rules for = or <-> (instead of ==)*) |
49 (*Congruence rules for = or <-> (instead of ==)*) |
50 fun mk_meta_cong ss rl = |
50 fun mk_meta_cong ctxt rl = |
51 Drule.zero_var_indexes (mk_meta_eq (mk_meta_prems (Simplifier.the_context ss) rl)) |
51 Drule.zero_var_indexes (mk_meta_eq (mk_meta_prems ctxt rl)) |
52 handle THM _ => |
52 handle THM _ => |
53 error("Premises and conclusion of congruence rules must use =-equality or <->"); |
53 error("Premises and conclusion of congruence rules must use =-equality or <->"); |
54 |
54 |
55 |
55 |
56 (*** Standard simpsets ***) |
56 (*** Standard simpsets ***) |
57 |
57 |
58 val triv_rls = [@{thm FalseL}, @{thm TrueR}, @{thm basic}, @{thm refl}, |
58 val triv_rls = [@{thm FalseL}, @{thm TrueR}, @{thm basic}, @{thm refl}, |
59 @{thm iff_refl}, reflexive_thm]; |
59 @{thm iff_refl}, reflexive_thm]; |
60 |
60 |
61 fun unsafe_solver ss = |
61 fun unsafe_solver ctxt = |
62 FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ss), assume_tac]; |
62 FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ctxt), assume_tac]; |
63 |
63 |
64 (*No premature instantiation of variables during simplification*) |
64 (*No premature instantiation of variables during simplification*) |
65 fun safe_solver ss = |
65 fun safe_solver ctxt = |
66 FIRST' [fn i => DETERM (match_tac (triv_rls @ Simplifier.prems_of ss) i), eq_assume_tac]; |
66 FIRST' [fn i => DETERM (match_tac (triv_rls @ Simplifier.prems_of ctxt) i), eq_assume_tac]; |
67 |
67 |
68 (*No simprules, but basic infrastructure for simplification*) |
68 (*No simprules, but basic infrastructure for simplification*) |
69 val LK_basic_ss = |
69 val LK_basic_ss = |
70 Simplifier.global_context @{theory} empty_ss |
70 empty_simpset @{context} |
71 setSSolver (mk_solver "safe" safe_solver) |
71 setSSolver (mk_solver "safe" safe_solver) |
72 setSolver (mk_solver "unsafe" unsafe_solver) |
72 setSolver (mk_solver "unsafe" unsafe_solver) |
73 |> Simplifier.set_subgoaler asm_simp_tac |
73 |> Simplifier.set_subgoaler asm_simp_tac |
74 |> Simplifier.set_mksimps (K (map mk_meta_eq o atomize o gen_all)) |
74 |> Simplifier.set_mksimps (K (map mk_meta_eq o atomize o gen_all)) |
75 |> Simplifier.set_mkcong mk_meta_cong; |
75 |> Simplifier.set_mkcong mk_meta_cong |
|
76 |> simpset_of; |
76 |
77 |
77 val LK_simps = |
78 val LK_simps = |
78 [@{thm triv_forall_equality}, (* prunes params *) |
79 [@{thm triv_forall_equality}, (* prunes params *) |
79 @{thm refl} RS @{thm P_iff_T}] @ |
80 @{thm refl} RS @{thm P_iff_T}] @ |
80 @{thms conj_simps} @ @{thms disj_simps} @ @{thms not_simps} @ |
81 @{thms conj_simps} @ @{thms disj_simps} @ @{thms not_simps} @ |
82 @{thms all_simps} @ @{thms ex_simps} @ |
83 @{thms all_simps} @ @{thms ex_simps} @ |
83 [@{thm de_Morgan_conj}, @{thm de_Morgan_disj}, @{thm imp_disj1}, @{thm imp_disj2}] @ |
84 [@{thm de_Morgan_conj}, @{thm de_Morgan_disj}, @{thm imp_disj1}, @{thm imp_disj2}] @ |
84 @{thms LK_extra_simps}; |
85 @{thms LK_extra_simps}; |
85 |
86 |
86 val LK_ss = |
87 val LK_ss = |
87 LK_basic_ss addsimps LK_simps |
88 put_simpset LK_basic_ss @{context} addsimps LK_simps |
88 |> Simplifier.add_eqcong @{thm left_cong} |
89 |> Simplifier.add_eqcong @{thm left_cong} |
89 |> Simplifier.add_cong @{thm imp_cong}; |
90 |> Simplifier.add_cong @{thm imp_cong} |
|
91 |> simpset_of; |
90 |
92 |