1open HolKernel Parse boolLib bossLib numLib pred_setSimps pred_setTheory finite_mapTheory simplifierTheory;
2
3(*------------------------------------------------------------------------------------------------------*)
4(* Additional theorems for finite maps                                                                  *)
5(*------------------------------------------------------------------------------------------------------*)
6
7
8val fupdate_normalizer =
9 let val thm = SPEC_ALL FUPDATE_LT_COMMUTES
10     val pat = lhs(snd(dest_imp(concl thm)))
11 in
12   {name = "Finite map normalization",
13    trace = 2,
14    key = SOME([],pat),
15    conv = let fun reducer tm =
16                 let val (theta,ty_theta) = match_term pat tm
17                     val thm' = INST theta (INST_TYPE ty_theta thm)
18                     val constraint = fst(dest_imp(concl thm'))
19                     val cthm = EQT_ELIM(reduceLib.REDUCE_CONV constraint)
20                 in MP thm' cthm
21                 end
22           in
23               K (K reducer)
24           end}
25 end;
26
27val finmap_conv_frag =
28 simpLib.SSFRAG
29     {convs = [fupdate_normalizer],
30      rewrs = [], ac=[],filter=NONE,dprocs=[],congs=[]};
31
32val finmap_ss = bossLib.std_ss ++ finmap_conv_frag
33                               ++ rewrites [FUPDATE_EQ, FAPPLY_FUPDATE_THM];
34
35val set_ss = std_ss ++ SET_SPEC_ss ++ PRED_SET_ss;
36
37