106 |
106 |
107 (*** Standard simpsets ***) |
107 (*** Standard simpsets ***) |
108 |
108 |
109 val triv_rls = [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, @{thm notFalseI}]; |
109 val triv_rls = [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, @{thm notFalseI}]; |
110 |
110 |
111 fun unsafe_solver ss = FIRST'[resolve_tac (triv_rls @ prems_of_ss ss), |
111 fun unsafe_solver ss = |
112 atac, etac @{thm FalseE}]; |
112 FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ss), atac, etac @{thm FalseE}]; |
|
113 |
113 (*No premature instantiation of variables during simplification*) |
114 (*No premature instantiation of variables during simplification*) |
114 fun safe_solver ss = FIRST'[match_tac (triv_rls @ prems_of_ss ss), |
115 fun safe_solver ss = |
115 eq_assume_tac, ematch_tac [@{thm FalseE}]]; |
116 FIRST' [match_tac (triv_rls @ Simplifier.prems_of ss), eq_assume_tac, ematch_tac @{thms FalseE}]; |
116 |
117 |
117 (*No simprules, but basic infastructure for simplification*) |
118 (*No simprules, but basic infastructure for simplification*) |
118 val FOL_basic_ss = |
119 val FOL_basic_ss = |
119 Simplifier.global_context @{theory} empty_ss |
120 Simplifier.global_context @{theory} empty_ss |
120 setsubgoaler asm_simp_tac |
121 setsubgoaler asm_simp_tac |