equal
deleted
inserted
replaced
107 in atoms end; |
107 in atoms end; |
108 |
108 |
109 fun mksimps pairs (_: Proof.context) = |
109 fun mksimps pairs (_: Proof.context) = |
110 map_filter (try mk_eq) o mk_atomize pairs o gen_all; |
110 map_filter (try mk_eq) o mk_atomize pairs o gen_all; |
111 |
111 |
|
112 val simp_legacy_precond = |
|
113 Attrib.setup_config_bool @{binding "simp_legacy_precond"} (K false) |
|
114 |
112 fun unsafe_solver_tac ctxt = |
115 fun unsafe_solver_tac ctxt = |
113 (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN' |
116 let |
114 FIRST' [resolve_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt), |
117 val intros = |
115 atac, etac @{thm FalseE}]; |
118 if Config.get ctxt simp_legacy_precond then [] else [@{thm conjI}] |
|
119 val sol_thms = |
|
120 reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt; |
|
121 fun sol_tac i = |
|
122 FIRST [resolve_tac sol_thms i, atac i , etac @{thm FalseE} i] ORELSE |
|
123 (match_tac intros THEN_ALL_NEW sol_tac) i |
|
124 in |
|
125 (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN' sol_tac |
|
126 end; |
116 |
127 |
117 val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac; |
128 val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac; |
118 |
129 |
119 |
130 |
120 (*No premature instantiation of variables during simplification*) |
131 (*No premature instantiation of variables during simplification*) |