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