src/Provers/simplifier.ML
changeset 0 a5a9c433f639
child 1 c6a6e3db5353
equal deleted inserted replaced
-1:000000000000 0:a5a9c433f639
       
     1 infix addsimps addcongs
       
     2       setsolver setloop setmksimps setsubgoaler;
       
     3 
       
     4 signature SIMPLIFIER =
       
     5 sig
       
     6   type simpset
       
     7   val addcongs: simpset * thm list -> simpset
       
     8   val addsimps: simpset * thm list -> simpset
       
     9   val asm_full_simp_tac: simpset -> int -> tactic
       
    10   val asm_simp_tac: simpset -> int -> tactic
       
    11   val empty_ss: simpset
       
    12   val merge_ss: simpset * simpset -> simpset
       
    13   val prems_of_ss: simpset -> thm list
       
    14   val rep_ss: simpset -> {simps: thm list, congs: thm list}
       
    15   val setsolver: simpset * (thm list -> int -> tactic) -> simpset
       
    16   val setloop: simpset * (int -> tactic) -> simpset
       
    17   val setmksimps: simpset * (thm -> thm list) -> simpset
       
    18   val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
       
    19   val simp_tac: simpset -> int -> tactic
       
    20 end;
       
    21 
       
    22 structure Simplifier:SIMPLIFIER =
       
    23 struct
       
    24 
       
    25 datatype simpset =
       
    26   SS of {mss: meta_simpset,
       
    27          simps: thm list,
       
    28          congs: thm list,
       
    29          subgoal_tac: simpset -> int -> tactic,
       
    30          finish_tac: thm list -> int -> tactic,
       
    31          loop_tac: int -> tactic};
       
    32 
       
    33 val empty_ss =
       
    34   SS{mss=empty_mss,
       
    35      simps= [],
       
    36      congs= [],
       
    37      subgoal_tac= K(K no_tac),
       
    38      finish_tac= K(K no_tac),
       
    39      loop_tac= K no_tac};
       
    40 
       
    41 
       
    42 fun (SS{mss,simps,congs,subgoal_tac,finish_tac,...}) setloop loop_tac =
       
    43   SS{mss=mss,
       
    44      simps= simps,
       
    45      congs= congs,
       
    46      subgoal_tac= subgoal_tac,
       
    47      finish_tac=finish_tac,
       
    48      loop_tac=loop_tac};
       
    49 
       
    50 fun (SS{mss,simps,congs,subgoal_tac,loop_tac,...}) setsolver finish_tac =
       
    51   SS{mss=mss,
       
    52      simps= simps,
       
    53      congs= congs,
       
    54      subgoal_tac= subgoal_tac,
       
    55      finish_tac=finish_tac,
       
    56      loop_tac=loop_tac};
       
    57 
       
    58 fun (SS{mss,simps,congs,finish_tac,loop_tac,...}) setsubgoaler subgoal_tac =
       
    59   SS{mss=mss,
       
    60      simps= simps,
       
    61      congs= congs,
       
    62      subgoal_tac= subgoal_tac,
       
    63      finish_tac=finish_tac,
       
    64      loop_tac=loop_tac};
       
    65 
       
    66 fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) setmksimps mk_simps =
       
    67   SS{mss=Thm.set_mk_rews(mss,mk_simps),
       
    68      simps= simps,
       
    69      congs= congs,
       
    70      subgoal_tac= subgoal_tac,
       
    71      finish_tac=finish_tac,
       
    72      loop_tac=loop_tac};
       
    73 
       
    74 fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addsimps rews =
       
    75   let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews)
       
    76   in
       
    77   SS{mss= Thm.add_simps(mss,rews'),
       
    78      simps= rews' @ simps,
       
    79      congs= congs,
       
    80      subgoal_tac= subgoal_tac,
       
    81      finish_tac=finish_tac,
       
    82      loop_tac=loop_tac}
       
    83   end;
       
    84 
       
    85 fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addcongs newcongs =
       
    86   SS{mss= Thm.add_congs(mss,newcongs),
       
    87      simps= simps,
       
    88      congs= newcongs @ congs,
       
    89      subgoal_tac= subgoal_tac,
       
    90      finish_tac=finish_tac,
       
    91      loop_tac=loop_tac};
       
    92 
       
    93 fun merge_ss(SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac},
       
    94              SS{simps=simps2,congs=congs2,...}) =
       
    95   let val simps' = gen_union eq_thm (simps,simps2)
       
    96       val congs' = gen_union eq_thm (congs,congs2)
       
    97       val mss' = Thm.set_mk_rews(empty_mss,Thm.mk_rews_of_mss mss)
       
    98       val mss' = Thm.add_simps(mss',simps')
       
    99       val mss' = Thm.add_congs(mss',congs')
       
   100   in SS{mss=         mss',
       
   101         simps=       simps,
       
   102         congs=       congs',
       
   103         subgoal_tac= subgoal_tac,
       
   104         finish_tac=  finish_tac,
       
   105         loop_tac=    loop_tac}
       
   106   end;
       
   107 
       
   108 fun prems_of_ss(SS{mss,...}) = prems_of_mss mss;
       
   109 
       
   110 fun rep_ss(SS{simps,congs,...}) = {simps=simps,congs=congs};
       
   111 
       
   112 fun add_asms (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) prems =
       
   113   let val rews = flat(map (mk_rews_of_mss mss) prems)
       
   114   in SS{mss= add_prems(add_simps(mss,rews),prems), simps=simps, congs=congs,
       
   115         subgoal_tac=subgoal_tac,finish_tac=finish_tac,
       
   116         loop_tac=loop_tac}
       
   117   end;
       
   118 
       
   119 fun asm_full_simp_tac(SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) =
       
   120   let fun solve_all_tac mss =
       
   121         let val ss = SS{mss=mss,simps=simps,congs=congs,
       
   122                         subgoal_tac=subgoal_tac,
       
   123                         finish_tac=finish_tac, loop_tac=loop_tac}
       
   124             fun solve1 thm = tapply(
       
   125                   STATE(fn state => let val n = nprems_of state
       
   126                     in if n=0 then all_tac
       
   127                        else subgoal_tac ss 1 THEN
       
   128                             COND (has_fewer_prems n) (Tactic solve1) no_tac
       
   129                     end),
       
   130                   thm)
       
   131         in DEPTH_SOLVE(Tactic solve1) end
       
   132 
       
   133       fun simp_loop i thm =
       
   134         tapply(asm_rewrite_goal_tac solve_all_tac mss i THEN
       
   135                (finish_tac (prems_of_mss mss) i  ORELSE  STATE(looper i)),
       
   136                thm)
       
   137       and allsimp i m state =
       
   138         let val n = nprems_of state
       
   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)
       
   143 
       
   144   in simp_loop_tac end;
       
   145 
       
   146 fun asm_simp_tac ss =
       
   147       METAHYPS(fn prems => asm_full_simp_tac (add_asms ss prems) 1);
       
   148 
       
   149 fun simp_tac ss = METAHYPS(fn _ => asm_full_simp_tac ss 1);
       
   150 
       
   151 end;