src/Provers/simplifier.ML
changeset 4612 26764de50c74
parent 4366 4d84cdb0df42
child 4668 131989b78417
equal deleted inserted replaced
4611:18a3f33f2097 4612:26764de50c74
   276 
   276 
   277 
   277 
   278 
   278 
   279 (** simplification tactics **)
   279 (** simplification tactics **)
   280 
   280 
   281 fun NEWSUBGOALS tac tacf st0 =
       
   282   st0 |> (tac THEN (fn st1 => tacf (nprems_of st1 - nprems_of st0) st1));
       
   283 
       
   284 fun solve_all_tac (subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac) mss =
   281 fun solve_all_tac (subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac) mss =
   285   let
   282   let
   286     val ss =
   283     val ss =
   287       make_ss (mss, subgoal_tac, loop_tac, unsafe_finish_tac, unsafe_finish_tac);
   284       make_ss (mss, subgoal_tac, loop_tac, unsafe_finish_tac, unsafe_finish_tac);
   288     val solve1_tac =
   285     val solve1_tac = (subgoal_tac ss THEN_ALL_NEW (K no_tac)) 1
   289       NEWSUBGOALS (subgoal_tac ss 1) (fn n => if n < 0 then all_tac else no_tac);
       
   290   in DEPTH_SOLVE solve1_tac end;
   286   in DEPTH_SOLVE solve1_tac end;
   291 
   287 
   292 
   288 
   293 (*not totally safe: may instantiate unknowns that appear also in other subgoals*)
   289 (*not totally safe: may instantiate unknowns that appear also in other subgoals*)
   294 fun basic_gen_simp_tac mode =
   290 fun basic_gen_simp_tac mode =
   295   fn (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac}) =>
   291   fn (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac}) =>
   296     let
   292     let
   297       fun simp_loop_tac i thm =
   293       fun simp_loop_tac i =
   298         (asm_rewrite_goal_tac mode
   294         asm_rewrite_goal_tac mode
   299           (solve_all_tac (subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac)) mss i
   295           (solve_all_tac (subgoal_tac,loop_tac,finish_tac,unsafe_finish_tac))
   300         THEN (finish_tac (prems_of_mss mss) i ORELSE looper i)) thm
   296           mss i
   301       and allsimp i n = EVERY (map (fn j => simp_loop_tac (i + j)) (n downto 0))
   297         THEN (finish_tac (prems_of_mss mss) i ORELSE
   302       and looper i = TRY (NEWSUBGOALS (loop_tac i) (allsimp i));
   298               TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i))
   303   in simp_loop_tac end;
   299     in simp_loop_tac end;
   304 
   300 
   305 fun gen_simp_tac mode (ss as Simpset {unsafe_finish_tac, ...}) =
   301 fun gen_simp_tac mode (ss as Simpset {unsafe_finish_tac, ...}) =
   306   basic_gen_simp_tac mode (ss setSSolver unsafe_finish_tac);
   302   basic_gen_simp_tac mode (ss setSSolver unsafe_finish_tac);
   307 
   303 
   308 
   304