src/Provers/simplifier.ML
changeset 1 c6a6e3db5353
parent 0 a5a9c433f639
child 17 b35851cafd3e
equal deleted inserted replaced
0:a5a9c433f639 1:c6a6e3db5353
     1 infix addsimps addcongs
     1 (*  Title:      Provers/simplifier
       
     2     ID:         $Id$
       
     3     Author:     Tobias Nipkow
       
     4     Copyright   1993  TU Munich
       
     5 
       
     6 Generic simplifier, suitable for most logics.
       
     7  
       
     8 *)
       
     9 infix addsimps addeqcongs
     2       setsolver setloop setmksimps setsubgoaler;
    10       setsolver setloop setmksimps setsubgoaler;
     3 
    11 
     4 signature SIMPLIFIER =
    12 signature SIMPLIFIER =
     5 sig
    13 sig
     6   type simpset
    14   type simpset
     7   val addcongs: simpset * thm list -> simpset
    15   val addeqcongs: simpset * thm list -> simpset
     8   val addsimps: simpset * thm list -> simpset
    16   val addsimps: simpset * thm list -> simpset
     9   val asm_full_simp_tac: simpset -> int -> tactic
    17   val asm_full_simp_tac: simpset -> int -> tactic
    10   val asm_simp_tac: simpset -> int -> tactic
    18   val asm_simp_tac: simpset -> int -> tactic
    11   val empty_ss: simpset
    19   val empty_ss: simpset
    12   val merge_ss: simpset * simpset -> simpset
    20   val merge_ss: simpset * simpset -> simpset
    80      subgoal_tac= subgoal_tac,
    88      subgoal_tac= subgoal_tac,
    81      finish_tac=finish_tac,
    89      finish_tac=finish_tac,
    82      loop_tac=loop_tac}
    90      loop_tac=loop_tac}
    83   end;
    91   end;
    84 
    92 
    85 fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addcongs newcongs =
    93 fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addeqcongs newcongs =
    86   SS{mss= Thm.add_congs(mss,newcongs),
    94   SS{mss= Thm.add_congs(mss,newcongs),
    87      simps= simps,
    95      simps= simps,
    88      congs= newcongs @ congs,
    96      congs= newcongs @ congs,
    89      subgoal_tac= subgoal_tac,
    97      subgoal_tac= subgoal_tac,
    90      finish_tac=finish_tac,
    98      finish_tac=finish_tac,
   114   in SS{mss= add_prems(add_simps(mss,rews),prems), simps=simps, congs=congs,
   122   in SS{mss= add_prems(add_simps(mss,rews),prems), simps=simps, congs=congs,
   115         subgoal_tac=subgoal_tac,finish_tac=finish_tac,
   123         subgoal_tac=subgoal_tac,finish_tac=finish_tac,
   116         loop_tac=loop_tac}
   124         loop_tac=loop_tac}
   117   end;
   125   end;
   118 
   126 
       
   127 fun NEWSUBGOALS tac tacf =
       
   128   STATE(fn state0 =>
       
   129     tac THEN STATE(fn state1 => tacf(nprems_of state1 - nprems_of state0)));
       
   130 
   119 fun asm_full_simp_tac(SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) =
   131 fun asm_full_simp_tac(SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) =
   120   let fun solve_all_tac mss =
   132   let fun solve_all_tac mss =
   121         let val ss = SS{mss=mss,simps=simps,congs=congs,
   133         let val ss = SS{mss=mss,simps=simps,congs=congs,
   122                         subgoal_tac=subgoal_tac,
   134                         subgoal_tac=subgoal_tac,
   123                         finish_tac=finish_tac, loop_tac=loop_tac}
   135                         finish_tac=finish_tac, loop_tac=loop_tac}
   124             fun solve1 thm = tapply(
   136             val solve1_tac =
   125                   STATE(fn state => let val n = nprems_of state
   137               NEWSUBGOALS (subgoal_tac ss 1)
   126                     in if n=0 then all_tac
   138                           (fn n => if n<0 then all_tac else no_tac)
   127                        else subgoal_tac ss 1 THEN
   139         in DEPTH_SOLVE(solve1_tac) end
   128                             COND (has_fewer_prems n) (Tactic solve1) no_tac
       
   129                     end),
       
   130                   thm)
       
   131         in DEPTH_SOLVE(Tactic solve1) end
       
   132 
   140 
   133       fun simp_loop i thm =
   141       fun simp_loop i thm =
   134         tapply(asm_rewrite_goal_tac solve_all_tac mss i THEN
   142         tapply(asm_rewrite_goal_tac solve_all_tac mss i THEN
   135                (finish_tac (prems_of_mss mss) i  ORELSE  STATE(looper i)),
   143                (finish_tac (prems_of_mss mss) i  ORELSE  looper i),
   136                thm)
   144                thm)
   137       and allsimp i m state =
   145       and allsimp i n = EVERY(map (fn j => simp_loop_tac (i+j)) (n downto 0))
   138         let val n = nprems_of state
   146       and looper i = TRY(NEWSUBGOALS (loop_tac i) (allsimp i))
   139         in EVERY(map (fn j => simp_loop_tac (i+j)) ((n-m) downto 0)) end
       
   140       and looper i state =
       
   141         TRY(loop_tac i THEN STATE(allsimp i (nprems_of state)))
       
   142       and simp_loop_tac i = Tactic(simp_loop i)
   147       and simp_loop_tac i = Tactic(simp_loop i)
   143 
   148 
   144   in simp_loop_tac end;
   149   in simp_loop_tac end;
   145 
   150 
   146 fun asm_simp_tac ss =
   151 fun asm_simp_tac ss =